伊莎贝尔中的“real_of_int”和“real”？

什么是real_of_int, real and int在伊莎贝尔？它们听起来有点像类型，但通常类型的写法类似于x ::real这些写法就像real x.

我无法证明以下陈述，

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

我注意到伊莎贝尔这样写：

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))

所以我希望能够理解这些意味着什么。

当一个人使用 Complex_Main （或基于它的逻辑，例如HOL-Analysis, HOL-Probability等）Isabelle 支持从 nat、int 和rat 到 real 的强制转换。如果类型不适合，则会自动添加这些。

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强制（缩写为of_nat其中范围固定为实数）和real_of_int :: real ⇒ int是缩写of_int其中范围固定为实数。

强制转换本质上是不同数字类型之间的态射，因此有许多态射引理可供它们使用：of_nat (l + n) = of_nat l + of_nat n等等。最好的方法是使用以下命令来搜索它们：of_nat and of_int而不是real_…缩写。