'real_of_int' and 'real' in Isabelle?

Question

What are real_of_int, real and int in Isabelle? They sound a bit like types, but usually types are written something like x ::real and these are written like real x.

I am having trouble proving the following statement,

 "S ((n*x)+(-x)) = S (n*x)*C (-x) + C (n*x)*S (-x)"

and I noticed that Isabelle writes it as:

S (real_of_int (int (n * x) + - int x)) =
S (real (n * x)) * C (real_of_int (- int x)) + C (real (n * x)) * S (real_of_int (- int x))

so I'd like to be able to understand what these mean.

Answer 1

When one uses Complex_Main (or a logic based on it like HOL-Analysis, HOL-Probability etc) Isabelle supports coercions from nat, int and rat into reals. These are added automatically if the types do not fit.

I.e. if f :: real ⇒ real, n :: nat and i :: int:

f n ↝ f (real n)
f i ↝ f (real_of_int i)

where real :: nat ⇒ real is the nat to real coercion (an abbreviation for of_nat where the range is fixed to real) and real_of_int :: real ⇒ int is the abbreviation for of_int where the range is fixed to real.

The coercions are essentially morphisms between the different numeral types, so there are many morphism lemmas available for them: of_nat (l + n) = of_nat l + of_nat n etc. The best is to search for them using just of_nat and of_int and not the real_… abbreviations.