factの解読
- isar-overviewのBNFによる構文範疇としては、fact ::= label 。labelの定義はないが、たぶん識別子だろう。論理式を識別する名前がラベルとすれば、factは論理式の名前ってことになる。
- tutorialにはfactの定義はない。
- isar-refには、logical contentとは、types, terms, facts だと書いてある。この言い方からすると、factsはpropositionsじゃないとオカシイ。
- 組み合わせて解釈すると、名前で参照可能な命題がfactかな。
- implementation文書のp.63の脚注に"facts (proof constants)"と書いてあった。proof constantの意味がワカランが、constantというからには名前がある、ってことだろう。
- implementation文書のp.88に"basic facts of Isabelle/HOL: HOL.impI, HOL.conjE, HOL.conjI etc." 。これは、推論規則だが、Pureレベルでは公理、つまり命題。推論規則も含めて、証明行為（リーズニング）の最中に名前で参照できる論理的リソースは何でもfactなのか？
- isar-refの"1.1.2 Facts"に、"A fact is a simultaneous list of theorems."、これじゃワカラン。
- factの生成は、assumption, proof, abbreviationで行う、とある。assumptionがラムダ抽象、proofとabbreviationがlet束縛に相当すると書いてある。薄っすらと分かるようなワカランような。
- factの参照は、名前（ラベル）か、暗黙に名前（this）か、リテラル（論理式そのもの）か、と書いてある。となると、やはりfactは論理式で、多くの場合は名前が付いていて、参照するものらしい。
- assumeコマンドとnoteコマンドがfactの操作に使う、とある。
- "Isar facts consist of multiple theorems"ともある。theorem＝propositionなんだろう。
- "The fact produced by the last entry of a block is exported into the outer context."、entryって何だ？ また新しい用語が。
- "fact this ― the last result produced in the text" resultがまたよくワカランのだが、textはproof textのことだろう。
- by fact というのがあるので、byコマンドの引数に渡すようなものがfactなのだろう。
- "Previous facts and new claims" ウーム。
- "unification of fact and goal statements against rules" ユニフィケーションに関係するか。
- "the current fact shall be used in the next step" 現在のファクトが次のステップで使われる。ということは、既に証明済みか仮定した命題がfactか。
- "(propositions, facts, and goals)" エエエエ、またワカランことを。propositionとfactって同じじゃなかったの？
- Simultaneous propositions or facts may be separated by the and keyword.ウーン、ここでもpropositionとfactを区別している。それとも、類義語、同義語を並べたorか。
- いきなり、fact expressions って。やめてくれよ。
factを多用しているのはウェンツェルだけで、ポールソンは使ってない。これだけ重要らしき概念を定義なしに導入するって神経がよく分からない。
