何度も同じことを繰り返し書くが、そのときどきの現状報告 assertion あまり使われてない claim 構文範疇のclaimはある thesis - "?theis"というシェマ変数（schematic variable）はある。哲学用語だと「ヘーゲルの弁証法の正」、命題、テーゼだとか。複数形…

どう違う？

print_options 便利。

http://isabelle.in.tum.de/library/HOL/HOL-Isar_Examples/outline.pdf では、 引用符をやめている。 ハイフンを名前に使っている。

オールドスタイルの証明コマンド／証明メソッドは、isar-refの"9.2 Basic proof tools"にある。

次は最初から使える。 typedecl 型または型構成子を導入できる。型レベルでの定数（＝型名）と定関数（＝型構成子）のシグネチャ宣言のようなもの。 class 型クラスは使える。「class 名前だけ」というのも特別にあって、これでユニバーサルな型クラスを定義…

lemmas（複数形！）というコマンドがある。lemmas G = A B C のように書いて、複数の定理をグルーピングできる。lemmas X = A なら、定理Aに別名Xを与えることが出来る。これを使うと、特定の名前Aの定理の内容を目視できる。ダミーの名前 X を使って、lemma…

シグネチャ（って言うかどうか知らんが）の宣言のとき、foo: "'a => 'a => X" (infix "$$" 70) のようにしてmixfix構文と優先度を指定できる。シグネチャで指定し忘れても、後からmixfixの宣言だけ出来る。 notation 名前 ( mixfix指定 )と書けばいい。mixfi…

definition はPureレベルで使える。definitionは定数定義、関数定義に使えるが、形式としては、等号的公理の追加になる。"左辺 == 右辺" で、「右辺により左辺が定義される」と読むようだ。左辺は定数、関数・演算子の呼び出し形式とか。書き換え規則を定義…

NGと書いてあるところだけダメ。 (* on top of Pure *) axiomatization A:: "'a ⇒ prop" and B:: "'a ⇒ prop" and P :: "prop" and Q :: "prop" term "op ==> P Q" term "P ==> Q" (* NG *) term "(A a)" term "(B b)" term "op ==> (A a) (B b)" term "(A a…

論理の説明が論理的にされることはほぼないので、用語法がイイカゲンで、曖昧・多義的・気分次第・行き当たりばったりであることはショーガナイとは思っているが、なんかガイドラインくらいは欲しい。どこにもガイドラインはない。自分で作ろう。多義的で注…

歴史を調べないと分からない処理系、てのも困ったもんだが、 エジンバラLFが「ロジカルフレーム」として先行か？ λPrologってのもある。 スコットのLCF理論が背景 ミルナーのMLで実装 CoqはIsabelleの後: Isabelle 1986年、Coq 1989年 3年後 [追記] "Logic o…

IFOL上のセオリーだと、term "(%x. (%y. x)) a" がエラーになる。その理由は、setup Pure_Thy.old_appl_syntax_setupというコマンドが実行されており、これによって、Pureの併置による適用の構文がキャンセルされて、x(y) という形でないと適用とはみなされ…

空列はPureの項ではない。 任意の識別子は項になる。 型推論される。 勝手な識別子の型は型変数 'a とされる。型総称な変数ということだろう。 併置は適用演算のはず。 ラムダ抽象は %x. A 、ピリオドの直後の空白は必須。 η変換は自動で行う。 β変換も自動…

proof method, tactic, rule, proof script, proof command あたり。proof commandの定義はない。commandの分類に、theory command, proof commandとかあって、lemmaはproofコマンドに分類されてる。「lemmaはゴールコマンドだ」とかの記述もあった。コマン…

文書指向へと舵を切ったウェンツェルだが、まだまだ全然だし、先は長いし、苦難が予想される。 用語法、メンタルモデルがスクリプト指向のまま。 ウェンツェル自身もfact, goalを多用している。 論理の概念・用語法と、ソフトウェアとしての証明系の用語・文…

infix operatorの優先度の一覧が欲しいだけど、isabelle infix operator precedence とかでググッてもあんまり分からん。Coqだと、公開されているHTMLマニュアルが引っかかったけど、Isabelleは粒度がでかいPDFだからなーー。[追記] introの"4.1.1 Infix Ann…

ここにまとめることにする。追加情報は追記していく。配布に付いているPDF文書、同梱文書と呼ぶことにする。略称はファイルのベース名。 タイトル ページ数 略称 Programming and Proving in Isabelle/HOL 63 prog-prove A Proof Assistant for Higher-Order…

やっと分かった、refinement という言葉。定義はなかった。「悟れ」ということらしい。要するに、未完成の証明図を考えて、未完成部分に「・・・」のようなマーカーがあるとして、そのマーカー部分＝未完成の部分を埋める作業をrefinementと言っているらしい…

いつものことだが、証明支援系や論理の話が、だいたいイイカゲンで論理的でもフォーマルでもない記述が多くて困る。[追記]研究対象→曖昧な用語法の研究 - 檜山正幸のキマイラ飼育記 メモ編[/追記]テクニカルタームと説明の地の文の区別がつかない。at show t…

writeln "\<alpha>" とかはアプリケーションレベルでのサポート。よって、#"a" はcharだが、#"\<alpha>" はcharにならない。Poly/MLのUnicodeサポート状況によるが、Unicode文字を文字および文字列に使えるはずだが、ASCII頭で凝り固まっている。</alpha></alpha>

Isabelleについて： 証明支援系は何を目指し、どこへ向かうのか - 檜山正幸のキマイラ飼育記 ウェンツェルの目標と志には全面的に賛同するが、なんか考えがとっちらかっている（一貫性がない、混乱している、中途半端）んじゃないの。 宣言的文書がほんとに…

タクティク、タクティカル（証明コンビネータ、推論コンビネータ）、ゴールなどは手続き的証明遂行の用語だよな。 ファクト、ゴール、サブゴールとかを宣言的証明の文脈で使われても意味わからん。 ファクトって何だよ？ ゴールって意味不明だろ→Coqの証明ゲ…

Isar = Intelligible semi-automated reasoning ってのは後付のコジツケだろう。MizarプロジェクトとIsabelleのIsaからだろう。Mizarは自然言語（英語）に近い、と言われている。ASCIIだけで数学記号を使ってないので、冗長でイヤンナル感じもする。let n be…

動詞：have, show, obtain, assume など 副詞：then, hence, finally, also, moreover, thus など 接続詞：and など その他： proof, qed, theorem, lemma など

letter ::= 名前開始文字 = ラテン文字|ギリシャ文字 名前文字 ::= 名前開始文字|数字|"_"|"'" ラテン文字とは普通の英字大文字小文字。まー、普通。ところが、名前内に下付き添字（subscript）が使える。添字は範囲ではなくて、1文字ずつ前置マークアップす…

「*&frasl;」OK、だが裏ワザ過ぎるよ 「*\/」ダメ、\/ がそのまま見える 「*&#47;」ダメ、すべてそのまま見える 「*&#x2f;」ダメ、すべてそのまま見える 「*\if\endif/」 OK 「*@if@endif/」 なぜかダメ 「*\」の2文字になる。たぶんバグ。

外部構文もセオリーで定義して拡張できる。valueは~~/src/HOL/Code_Evaluation.thyで定義されている。つまり、imports Code_Evaluation でvalueが利用可能となる。Pureだと、funもtermも使えない。

fun plus x y = x + y; (* OK *) val plus = fn x => fn y => x + y; (* OK *) val plus = fn (x, y) => x + y; (* OK *) val plus = fn x y => x + y; (* NG *) 最後がNGなのが納得がいかない！ が、そうなんだから仕方ない。最初のような書き方をするしか…

@attention と @warning があり、どちらもそれらしく表示されるが、使い分けがワカラン。まー、自分で決めるってことだろう。