The functions KroneckerDelta[Sin[Pi x]] and KroneckerDelta[SawtoothWave[x]] behave disappointingly with respect to derivation and integration:

D[KroneckerDelta[Sin[Pi x]], x]
D[KroneckerDelta[SawtoothWave[x]], x]
Integrate[KroneckerDelta[Sin[Pi x]], x]
Integrate[KroneckerDelta[SawtoothWave[x]], x]

The same for Boole[Element[x, Integers]], which also does not evaluate on floating point integers, such as Boole[Element[1., Integers]]

I was going to add this from the docs of D[]:

D returns generic results that may not account for discontinuities, cusps or other special points

This is the case for Kronecker[x]. However, the following seems wrong (should be Pi*x, not 2*Pi*x, right?):

D[SawtoothWave[x], x]
(*  Piecewise[{{1, Sin[2*Pi*x] != 0}}, Indeterminate]  *)

Otherwise, we could use SawtoothWave[x] + SawtoothWave[1 - x] for Ceiling[x] - Floor[x].

Further, @Daniel may like this integral better:

Integrate[KroneckerDelta[Sin[Pi x]], {x, 0, x}]
(*  ConditionalExpression[0, x \[Element] Reals]  *)

Okay, maybe my response was irrelevant, but I'm not convinced, so let me try again. I see your point about my example using concrete values while you're only interested in the abstraction provided by variables. But Mathematica doesn't want to give an untrue answer (as much as reasonable, there are in fact weird edge cases that one could consider untrue, but I don't think we need to go into that). So, if it were to "solve" the problem with variables but a user wanted to use the solution with values (in particular the values I used as examples), well then they'd get very incorrect results.

As for your questions...

I would like Wolfram to be able to convert an expression Ceiling[x] - Floor[x] - 1 into a function that has zero everywhere except the set of integers, where it has -1.

That's easy. We can just use your expression directly:

myFunc[x_] := Ceiling[x] - Floor[x] - 1;
Table[myFunc[x], {x, -2, 2, 1/4}]
(* {-1, 0, 0, 0, -1, 0, 0, 0, -1, 0, 0, 0, -1, 0, 0, 0, -1} *)

There are probably many ways to define such a function, there may even be a built in function for that.

to what extent can Wolfram help in theoretical mathematics?

I'm not the right person to answer that, but as far as I can tell there are many people doing sophisticated mathematics with Wolfram.

I'm sorry, but I've lost the plot. I don't understand where you're going with this. I don't understand why my answers are confusing, and so I don't know how to improve them. Have you been able to get something to actually work? Have you tried the suggestions offered here, and have they worked or not? I'd really prefer to help you reach your specific objective rather than rathole on some quirk of Mathematica's Simplify implementation.

What do you mean? Here's another example:

In:  1 \[Element] Rationals
Out: True

In:  Ceiling[x] == 1 + Floor[x] /. x -> 12/5
Out: True

In:  FullSimplify[Ceiling[x] == 1 + Floor[x], x \[Element] Rationals]
Out: Ceiling[x] == 1 + Floor[x]

I think Hans Milton provided a good example, and your reply to that doesn't seem relevant. Here's another way to look at it:

FullSimplify[Ceiling[x] == Floor[x], x \[Element] Integers]
(* True *)

FullSimplify[Ceiling[x] == Floor[x], x \[Element] Reals]
(* Ceiling[x] == Floor[x] *)

So, you can interpret that as meaning, "when x is real, Mathematica cannot find a simplification that resolves the equality to true or false". And of course, like Hans showed, one example is 2.0. Indeed, we have

2 \[Element] Reals
(* True *)

So, we don't even need an expression with Real as its Head. Furthermore, consider this

2. \[Element] Integers
(* 2. \[Element] Integers *)

2. \[NotElement] Integers
(* 2. \[NotElement] Integers *)

meaning that Mathematica withholds commitment about the integer-valued-ness for a value that you expect to satisfy your assumptions. I think the answer to your original question depends upon the reason for that.