Isar statement formatとローカル＆グローバルはコンテキスト
isar-refのp.46に書いてある話。
コンテキストとは、処理系が持っている定理＆ルールのデータベースのことだとする。このコンテキストが見えないことがわかりにくさの大きな原因だ。さらに、コンテキストは入れ子になる。
Isarでは、コンテキストを可視化するためにassumes/shows構文を使っている。これで明示されるのは単一の定理（の候補である命題）をリーズニングする過程で使うローカルコンテキストだけ。定理の外にあるグローバルなコンテキストは暗黙のまま。
ともかく、ローカルコンテキストであっても明示できる（可視化できる）のは大きなメリット：
- assumes Γ shows φ が、メタな判断 Γ |- φ に対応する
- リーズニングの最中には、これは判断ではなくて問題だから Γ ?- φ と解釈される。
問題文が提示され、リーズニングが成功すると、問題文に対応する判断文が主張され、それが受理される。問題文の提示が処理系との対話のなかで「状況として」なされる。このときのコンテキストも明らかではない。だから、分かりにくい。
提示と受理を表すためにモード（セオリーモード、証明モード）や証明責務とその履行（discharge）の概念があるのだろう。
- 問題文の提示が、処理系が問題状況（モード）に入ることにより表現される
- 問題の解決過程はリーズニングとなる。
- リーズニングの成果物は証明オブジェクト。
- 証明オブジェクトは機械的な検証が可能。
- 検証が通ると、問題文は判断主張文となる。
- 判断主張文が受理されると、処理系のグローバルコンテキストが変わる。
