本文介绍了Isabelle 中的“real_of_int"和“real"?的处理方法,对大家解决问题具有一定的参考价值,需要的朋友们下面随着小编来一起学习吧!

问题描述

Isabelle 中的 real_of_intrealint 是什么?它们听起来有点像类型,但通常类型的写法类似于 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-AnalysisHOL-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 :: nati :: int:

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

where real :: nat ⇒ realnatreal 的强制转换(of_nat 的缩写,其中范围固定为实数),real_of_int :: real ⇒ intof_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_natof_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"?的文章就介绍到这了,希望我们推荐的答案对大家有所帮助,也希望大家多多支持!

09-14 08:17