types之伊莎贝尔的 'real_of_int' 和 'real'

Isabelle 中的real_of_int、real 和int 是什么？它们听起来有点像类型，但通常类型的写法类似于 x::real，而这些写法类似于 real x。

我无法证明以下陈述，

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

我注意到 Isabelle 是这样写的:

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 到实数的强制转换。如果类型不适合，这些将自动添加。

即如果 f::real ⇒ real，n::nat 和 i::int:

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

real::nat ⇒ real 是 nat 到 real 的强制转换(of_nat 的缩写，其中范围固定为实数)，real_of_int::real ⇒ int 是 of_int 的缩写，其中范围固定为实数。

强制转换本质上是不同数字类型之间的态射，因此有许多可用的态射引理:of_nat (l + n) = of_nat l + of_nat n 等。最好是搜索对他们来说，只使用 of_nat 和 of_int 而不是 real_... 缩写。