Isabelle 中的“real_of_int"和“real"? [英] 'real_of_int' and 'real' in Isabelle?

问题描述

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

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.

我无法证明以下陈述，

 "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.

推荐答案

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

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.

即if f :: real ⇒ real, n :: nat 和 i :: int:

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

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

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.

强制转换本质上是不同数字类型之间的态射，因此有许多态射引理可供它们使用:of_nat (l + n) = of_nat l + of_nat n 等等.最好是搜索对于他们来说，只使用 of_nat 和 of_int 而不是 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.

这篇关于Isabelle 中的“real_of_int"和“real"?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！