imports Pure

(* Title: HOL/Isar_Examples/First_Order_Logic.thy Author: Makarius *) section ‹A simple formulation of First-Order Logic› text ‹ The subsequent theory development illustrates single-sorted intuitionistic first-order logic with equality, formulated within the Pure framework. › theory First_Order_Logic imports Pure begin subsection ‹Abstract syntax› typedecl i typedecl o judgment Trueprop :: "o ⇒ prop" ("_" 5) subsection ‹Propositional logic› axiomatization false :: o ("⊥") where falseE [elim]: "⊥ ⟹ A" axiomatization imp :: "o ⇒ o ⇒ o" (infixr "⟶" 25) where impI [intro]: "(A ⟹ B) ⟹ A ⟶ B" and mp [dest]: "A ⟶ B ⟹ A ⟹ B" axiomatization conj :: "o ⇒ o ⇒ o" (infixr "∧" 35) where conjI [intro]: "A ⟹ B ⟹ A ∧ B" and conjD1: "A ∧ B ⟹ A" and conjD2: "A ∧ B ⟹ B" theorem conjE [elim]: assumes "A ∧ B" obtains A and B proof from ‹A ∧ B› show A by (rule conjD1) from ‹A ∧ B› show B by (rule conjD2) qed axiomatization disj :: "o ⇒ o ⇒ o" (infixr "∨" 30) where disjE [elim]: "A ∨ B ⟹ (A ⟹ C) ⟹ (B ⟹ C) ⟹ C" and disjI1 [intro]: "A ⟹ A ∨ B" and disjI2 [intro]: "B ⟹ A ∨ B" definition true :: o ("⊤") where "⊤ ≡ ⊥ ⟶ ⊥" theorem trueI [intro]: ⊤ unfolding true_def .. definition not :: "o ⇒ o" ("¬ _" [40] 40) where "¬ A ≡ A ⟶ ⊥" theorem notI [intro]: "(A ⟹ ⊥) ⟹ ¬ A" unfolding not_def .. theorem notE [elim]: "¬ A ⟹ A ⟹ B" unfolding not_def proof - assume "A ⟶ ⊥" and A then have ⊥ .. then show B .. qed definition iff :: "o ⇒ o ⇒ o" (infixr "⟷" 25) where "A ⟷ B ≡ (A ⟶ B) ∧ (B ⟶ A)" theorem iffI [intro]: assumes "A ⟹ B" and "B ⟹ A" shows "A ⟷ B" unfolding iff_def proof from ‹A ⟹ B› show "A ⟶ B" .. from ‹B ⟹ A› show "B ⟶ A" .. qed theorem iff1 [elim]: assumes "A ⟷ B" and A shows B proof - from ‹A ⟷ B› have "(A ⟶ B) ∧ (B ⟶ A)" unfolding iff_def . then have "A ⟶ B" .. from this and ‹A› show B .. qed theorem iff2 [elim]: assumes "A ⟷ B" and B shows A proof - from ‹A ⟷ B› have "(A ⟶ B) ∧ (B ⟶ A)" unfolding iff_def . then have "B ⟶ A" .. from this and ‹B› show A .. qed subsection ‹Equality› axiomatization equal :: "i ⇒ i ⇒ o" (infixl "=" 50) where refl [intro]: "x = x" and subst: "x = y ⟹ P x ⟹ P y" theorem trans [trans]: "x = y ⟹ y = z ⟹ x = z" by (rule subst) theorem sym [sym]: "x = y ⟹ y = x" proof - assume "x = y" from this and refl show "y = x" by (rule subst) qed subsection ‹Quantifiers› axiomatization All :: "(i ⇒ o) ⇒ o" (binder "∀" 10) where allI [intro]: "(⋀x. P x) ⟹ ∀x. P x" and allD [dest]: "∀x. P x ⟹ P a" axiomatization Ex :: "(i ⇒ o) ⇒ o" (binder "∃" 10) where exI [intro]: "P a ⟹ ∃x. P x" and exE [elim]: "∃x. P x ⟹ (⋀x. P x ⟹ C) ⟹ C" lemma "(∃x. P (f x)) ⟶ (∃y. P y)" proof assume "∃x. P (f x)" then obtain x where "P (f x)" .. then show "∃y. P y" .. qed lemma "(∃x. ∀y. R x y) ⟶ (∀y. ∃x. R x y)" proof assume "∃x. ∀y. R x y" then obtain x where "∀y. R x y" .. show "∀y. ∃x. R x y" proof fix y from ‹∀y. R x y› have "R x y" .. then show "∃x. R x y" .. qed qed end