公理と定義

axiomatizationは、シグニチャ部と公理（の論理式）部からなる。

IFOL.thy :

axiomatization
  eq :: "['a, 'a] ⇒ o"  (infixl "=" 50)
where
  refl: "a = a" and
  subst: "a = b ==> P(a) ==> P(b)"

構造は、localeやclassと同じだが、fixes/assumes ではなくて、無名節/where節。構文がバラバラ。

シグニチャは省略（空白）可能で：

IFOL.thy :

axiomatization where  ― ‹Reflection, admissible›
  eq_reflection: "(x = y) ==> (x ≡ y)" and
  iff_reflection: "(P <--> Q) ==> (P ≡ Q)"

definitionの直後に≡を含む命題、またはaxiomatizationと同じ 無名節/where節の構造。だが、シグニチャ定義で、型（プロファイル）が付いてないのがある。こんなんもありなのか？ whereの後の論理式は≡を含むもので一個に限るのだろう（そうでないと解釈できない）。

definition "True ≡ False --> False"

definition Not ("¬ _" [40] 40)
  where not_def: "¬ P ≡ P --> False"

definition iff  (infixr "<-->" 25)
  where "P <--> Q ≡ (P --> Q) ∧ (Q --> P)"

definition Ex1 :: "('a ⇒ o) ⇒ o"  (binder "∃!" 10)
  where ex1_def: "∃!x. P(x) ≡ ∃x. P(x) ∧ (∀y. P(y) --> y = x)"

次の例は組み込み等号じゃなくて、ユーザー定義等号を使っている。これでもいいらしい。

Fun.thy :

definition id :: "'a ⇒ 'a" where
  "id = (λx. x)"

略記が定義とどう違うか？ わかってない。

Fun.thy :

abbreviation
  "inj f ≡ inj_on f UNIV"

abbreviation surj :: "('a ⇒ 'b) ⇒ bool" where ― "surjective"
  "surj f ≡ (range f = UNIV)"