Isabelle/Isar（その２）

　それでは使ってみましょう．前回同様にjeditを起動すると，デフォルトでユーザーホームディレクトリのScratch.thyというファイルが（なければ作成され）ロードされますので，まずは

theory Scratch
imports Complex_Main
begin

end

と入力してください．

１行目のScratchというのは本来はこれから書く理論の名前ですがjeditやProof-Generalでは（ピリオドと拡張子を除いた）ファイル名でないとエラーが出ます．別名にするには，例えば

theory Betsumei

としたのち，ファイルメニューから名前を付けて保存を選択，ファイル名をBetsumei.thyとして保存すればOKです．

２行目は証明で参照する既存の定理（推論規則も含む）が収められているtheory名（（ピリオドと拡張子を除いた）ファイル名）で，複数指定の場合はスペースで区切ります．ただし，デフォルトでいきなり呼べるのは，イザベルホームディレクトリ~~に対して，~~/src/HOL/にあるものだけで，その他は例えば

imports Complex_Main "~~/src/HOL/Library/Sum_of_Squares"

のように指定します（「ファイルがない」と言う場合，一度保存してリロードすると認識してくれます）．Complex_Mainがあれば複素数の範囲で初等的な一通りのことが出来ますが，派手な有理式の処理などには上記のSum_of_Squaresが便利かも知れません．

あとは，beginとendとの間に定理，証明などを書くだけです．