Isabelle/Isar（その６）

　Isabelle/Isarのセッションは，theoryモード，proofモードからなっています．

　まず，theory-beginまで入力すると，theoryモードに入ります．theoryモードはIsarが「これから定義や定理，証明を書いてください」と言っている状態です．またシステムのパラメータなどの設定もこのモードでしか行えません．要は証明を外から見るモードです．

　theoryモードでlemma（あるいはtheoremあるいはcorollary）-shows "..."まで入力すると，proofモードのうち，証明待ちのproof(prove)モードに入ります．そこで使えるコマンドは，証明のmethodを引数にもつ

　using ... apply,　using ... proof,　using ... by

の何れかで，usingは参照する定理...（複数の場合はスペースで区切る）を指定するオプショナルコマンドです．これらの特徴は

　applyは引数のmethod適用後もproof(prove)モードにあり（つまり，証明の反復），証明完了後はdoneコマンドで，theoryモードに抜ける
　proofは引数のmethod適用後は，次に証明すべき内容の表明待ち，すなわち，proof(state)モードに入り，その時点で証明すべきゴールがなければ（つまり証明完了なら）qedコマンドでtheoryモードに抜ける（qedの引数に最後に使うmethodを廻せることは前述の通り），まだ残っているなら，次に証明するサブゴールを表明する為のコマンドhaveまたは，全体のゴールを表明するコマンドshowを受付け，それら実行後，証明待ちのproof(prove)モードに入る
　by m1 m2 は proof m1 qed m2 と等価

という点です．

　他に必要に応じてstateモードの頭に「参照する性質を指定する」為のchainモードを付けることも出来，そこでは次回以降述べるfrom，finally，ultimatelyといったコマンドが使えます．