伊莎贝尔的'real_of_int'和'真实'？

Question

什么是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))

所以我希望能够理解这些意思.

Answer 1

当使用Complex_Main(或基于它的逻辑,如HOL-Analysis,HOL-Probability等)时,Isabelle支持将nat,int和rat强制转换为实数.如果类型不适合,则会自动添加这些内容.

即,如果HOL-Analysis,HOL-Probability和f :: real ? real:

f n ? f (real n)
f i ? f (real_of_int i)

其中n :: nat是i :: int对real :: nat ? real胁迫(对于of_nat的缩写其中该范围被固定到实数)和nat对于缩写real其中该范围被固定到真实.

该强制转换是不同的数字类型之间实质上态射,所以有可供他们许多射引理:of_nat等等,最好是只使用搜索他们real_of_int :: real ? int和of_int,而不是of_nat (l + n) = of_nat l + of_nat n缩写.