イザベルでreal_of_int,real、intとは何ですか？彼らはタイプのようなビットを鳴らしますが、通常タイプはx ::realのように書かれ、これらはreal xのように書かれています。イザベルで 'real_of_int'と 'real'？
私は、次のステートメントを証明する問題が発生した
"S ((n*x)+(-x)) = S (n*x)*C (-x) + C (n*x)*S (-x)"
と私はイザベルのようにそれを書き込みことに気づいています：私はこれらが何を意味するか理解できるようにしたいと思い
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からの強制変換を実数にサポートします。タイプが適合しない場合、これらは自動的に追加されます。
I.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)
。
強制型変換は本質的に異なる数字タイプ間の射されているので、彼らのために利用可能な多く射補題がありますof_nat (l + n) = of_nat l + of_nat nなど最高のは、ちょうどof_natとof_intなくreal_…略語を使用してそれらを検索することです。