real_of_int, real와 이사벨의 int 무엇입니까? 그들은 유형처럼 조금 소리가 있지만, 일반적으로 유형 x ::real 같은 것을 작성하는 이들은 real x 같이 기록됩니다. 그래서 나는이 무슨 뜻인지 이해할 수 있도록하고 싶습니다이자벨에서 'real_of_int'와 'real'?
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))
:
"S ((n*x)+(-x)) = S (n*x)*C (-x) + C (n*x)*S (-x)"
나는 문제가 다음과 같은 성명을 증명하는 데 문제
는, 나는 이사벨이로 쓰는 것으로 나타났습니다.
Complex_Main (또는 HOL-Analysis, HOL-Probability 등의 논리를 기반으로하는 논리)을 사용하면 Isabelle은 nat, int 및 rat에서부터 reals에 대한 변환을 지원합니다. 유형이 맞지 않으면 자동으로 추가됩니다.
e.e. f :: real ⇒ real, n :: nat 및 i :: int 경우 :
real :: nat ⇒ real가
nat
real에 강압 및
real_of_int :: real ⇒ int의 범위가 실제에 고정
of_int 대한 약어 (범위는 실제에 고정 of_nat 약자)이다
f n ↝ f (real n)
f i ↝ f (real_of_int i)
.
강제 변환은 본질적으로 morphisms 다른 숫자 유형 사이, 그래서 가능한 많은 morphism에의 보조 정리는 그들을 위해이 있습니다 : of_nat (l + n) = of_nat l + of_nat n 등 최고의 그들을 그냥 of_nat 및 of_int 아닌 real_… 약어를 사용하여 검색하는 것입니다.