proof method周辺
proof method, tactic, rule, proof script, proof command あたり。
proof commandの定義はない。commandの分類に、theory command, proof commandとかあって、lemmaはproofコマンドに分類されてる。「lemmaはゴールコマンドだ」とかの記述もあった。コマンド→証明コマンド→ゴールコマンドのような階層的分類体系があるようだ、説明はないけど。
コマンドはキーワードと同じかな？ Pureの定義を見てみる（最後に貼り付け）。セオリーにより導入されるキーワード＝コマンド名らしい、だいたいは。キーワード＝コマンドの実装はMLの関数なんだと思う。型宣言がないキーワードは言語としてのキーワードで、型宣言があるのは、引数を持つ関数なのかな？
applyは宣言によると証明スクリプトを引数に取ることになっている。証明スクリプトと証明メソッドはたぶん同義語だろう。applyの引数に渡すときは証明メソッドと呼ぶのだろう、たぶん。とにかく定義がないけど。
タクティクは、もともとは語尾が_tacで終わるML関数のこと（歴史）。ruleとかeruleとかもタクティクなんだと思う。で、ruleタクティク（だとして）の場合、さらに引数としてルール名を取る。で、ルールとは何かというと、論理の推論ルールの意味もあるが、それまでに蓄積された知識ベース（Isabelleではたぶんfactsかcontexがソレだろう）内の定理がルールだろう。
定理がルールってのも変だが、1990-manualの"1.2.2 The type of theorems and its operations"によると：
The inference rules, theorems, and axioms of a logic have type thm. Theorems and axioms can be regarded as rules with no premises, so let us speak just of rules.
定理や公理も前提（premises）がないルールと見なすようだ。で、ルールは型理論の型判断と同じだから、ルールの前提＝コンテキストなのかも知れない。バックグラウンド（background）もコンテキストのこと＝ルールの前提のこと、みたいだ。定義はないけど。
ところで、ルールと言えば、Prologでもルールって言葉を使っていて、goal, fact(s), rule(s) はProlog由来かも知れない。一方で、シーケントをルールと言っている気配もある。
ハッキリ「＝」とまでは断言できないが、
- Prolog流のルール≒シーケント≒自然演繹の推論ルール≒知識ベースのエントリー
エントリーは一項目の意味、実際どっかでentryは使っていた。
ここらでまとめると：色々あるコマンドのなかで証明コマンドに分類されるapplyコマンドは、証明スクリプトを引数に取ってそのスクリプトをを実行するが、特にapplyの引数を証明メソッドと呼び、メソッドのひとつにruleメソッドがあり、その実体はruleタクティクであり、ruleタクティクは知識ベース内のルールを引数に取るが、このルールとは定理のことでもあり、定理とルールは同一視され、定理＝ルールの前提はまたコンテキストとかバックグラウンドとか環境とかも呼ぶ。
ほぼ気違い沙汰だな。解釈にどんたけ苦労すればいいんだよ。
theory Pure
keywords
"!!" "!" "+" "--" ":" ";" "<" "<=" "=" "=>" "?" "[" "―" "≡"
"↽" "⇀" "⇌"
"⊆" "]" "assumes" "attach" "binder" "constrains"
"defines" "rewrites" "fixes" "for" "identifier" "if" "in" "includes" "infix"
"infixl" "infixr" "is" "notes" "obtains" "open" "output"
"overloaded" "pervasive" "premises" "private" "qualified" "rewrites"
"shows" "structure" "unchecked" "where" "when" "|"
and "text" "txt" :: document_body
and "text_raw" :: document_raw
and "default_sort" :: thy_decl == ""
and "typedecl" "type_synonym" "nonterminal" "judgment"
"consts" "syntax" "no_syntax" "translations" "no_translations"
"definition" "abbreviation" "type_notation" "no_type_notation" "notation"
"no_notation" "axiomatization" "lemmas" "declare"
"hide_class" "hide_type" "hide_const" "hide_fact" :: thy_decl
and "SML_file" "SML_file_debug" "SML_file_no_debug" :: thy_load % "ML"
and "SML_import" "SML_export" :: thy_decl % "ML"
and "ML" :: thy_decl % "ML"
and "ML_prf" :: prf_decl % "proof" (* FIXME % "ML" ?? *)
and "ML_val" "ML_command" :: diag % "ML"
and "simproc_setup" :: thy_decl % "ML" == ""
and "setup" "local_setup" "attribute_setup" "method_setup"
"declaration" "syntax_declaration"
"parse_ast_translation" "parse_translation" "print_translation"
"typed_print_translation" "print_ast_translation" "oracle" :: thy_decl % "ML"
and "bundle" :: thy_decl
and "include" "including" :: prf_decl
and "print_bundles" :: diag
and "context" "locale" "experiment" :: thy_decl_block
and "interpret" :: prf_goal % "proof"
and "interpretation" "global_interpretation" "sublocale" :: thy_goal
and "class" :: thy_decl_block
and "subclass" :: thy_goal
and "instantiation" :: thy_decl_block
and "instance" :: thy_goal
and "overloading" :: thy_decl_block
and "code_datatype" :: thy_decl
and "theorem" "lemma" "corollary" "proposition" :: thy_goal
and "schematic_goal" :: thy_goal
and "notepad" :: thy_decl_block
and "have" :: prf_goal % "proof"
and "hence" :: prf_goal % "proof" == "then have"
and "show" :: prf_asm_goal % "proof"
and "thus" :: prf_asm_goal % "proof" == "then show"
and "then" "from" "with" :: prf_chain % "proof"
and "note" :: prf_decl % "proof"
and "supply" :: prf_script % "proof"
and "using" "unfolding" :: prf_decl % "proof"
and "fix" "assume" "presume" "def" :: prf_asm % "proof"
and "consider" :: prf_goal % "proof"
and "obtain" :: prf_asm_goal % "proof"
and "guess" :: prf_script_asm_goal % "proof"
and "let" "write" :: prf_decl % "proof"
and "case" :: prf_asm % "proof"
and "{" :: prf_open % "proof"
and "}" :: prf_close % "proof"
and "next" :: next_block % "proof"
and "qed" :: qed_block % "proof"
and "by" ".." "." "sorry" :: "qed" % "proof"
and "done" :: "qed_script" % "proof"
and "oops" :: qed_global % "proof"
and "defer" "prefer" "apply" :: prf_script % "proof"
and "apply_end" :: prf_script % "proof" == ""
and "subgoal" :: prf_script_goal % "proof"
and "proof" :: prf_block % "proof"
and "also" "moreover" :: prf_decl % "proof"
and "finally" "ultimately" :: prf_chain % "proof"
and "back" :: prf_script % "proof"
and "help" "print_commands" "print_options" "print_context" "print_theory"
"print_definitions" "print_syntax" "print_abbrevs" "print_defn_rules"
"print_theorems" "print_locales" "print_classes" "print_locale"
"print_interps" "print_dependencies" "print_attributes"
"print_simpset" "print_rules" "print_trans_rules" "print_methods"
"print_antiquotations" "print_ML_antiquotations" "thy_deps"
"locale_deps" "class_deps" "thm_deps" "print_term_bindings"
"print_facts" "print_cases" "print_statement" "thm" "prf" "full_prf"
"prop" "term" "typ" "print_codesetup" "unused_thms" :: diag
and "display_drafts" "print_state" :: diag
and "welcome" :: diag
and "end" :: thy_end % "theory"
and "realizers" :: thy_decl == ""
and "realizability" :: thy_decl == ""
and "extract_type" "extract" :: thy_decl
and "find_theorems" "find_consts" :: diag
and "named_theorems" :: thy_decl
begin
