# Theory First_Order_Logic

theory First_Order_Logic
imports Pure
`(*  Title:      FOL/ex/First_Order_Logic.thy    Author:     Markus Wenzel, TU Munich*)header {* A simple formulation of First-Order Logic *}theory First_Order_Logic imports Pure begintext {*  The subsequent theory development illustrates single-sorted  intuitionistic first-order logic with equality, formulated within  the Pure framework.  Actually this is not an example of  Isabelle/FOL, but of Isabelle/Pure.*}subsection {* Syntax *}typedecl itypedecl ojudgment  Trueprop :: "o => prop"    ("_" 5)subsection {* Propositional logic *}axiomatization  false :: o  ("⊥") and  imp :: "o => o => o"  (infixr "-->" 25) and  conj :: "o => o => o"  (infixr "∧" 35) and  disj :: "o => o => o"  (infixr "∨" 30)where  falseE [elim]: "⊥ ==> A" and  impI [intro]: "(A ==> B) ==> A --> B" and  mp [dest]: "A --> B ==> A ==> B" and  conjI [intro]: "A ==> B ==> A ∧ B" and  conjD1: "A ∧ B ==> A" and  conjD2: "A ∧ B ==> B" and  disjE [elim]: "A ∨ B ==> (A ==> C) ==> (B ==> C) ==> C" and  disjI1 [intro]: "A ==> A ∨ B" and  disjI2 [intro]: "B ==> A ∨ B"theorem conjE [elim]:  assumes "A ∧ B"  obtains A and Bproof  from `A ∧ B` show A by (rule conjD1)  from `A ∧ B` show B by (rule conjD2)qeddefinition  true :: o  ("\<top>") where  "\<top> ≡ ⊥ --> ⊥"definition  not :: "o => o"  ("¬ _" [40] 40) where  "¬ A ≡ A --> ⊥"definition  iff :: "o => o => o"  (infixr "<->" 25) where  "A <-> B ≡ (A --> B) ∧ (B --> A)"theorem trueI [intro]: \<top>proof (unfold true_def)  show "⊥ --> ⊥" ..qedtheorem notI [intro]: "(A ==> ⊥) ==> ¬ A"proof (unfold not_def)  assume "A ==> ⊥"  then show "A --> ⊥" ..qedtheorem notE [elim]: "¬ A ==> A ==> B"proof (unfold not_def)  assume "A --> ⊥" and A  then have ⊥ .. then show B ..qedtheorem iffI [intro]: "(A ==> B) ==> (B ==> A) ==> A <-> B"proof (unfold iff_def)  assume "A ==> B" then have "A --> B" ..  moreover assume "B ==> A" then have "B --> A" ..  ultimately show "(A --> B) ∧ (B --> A)" ..qedtheorem iff1 [elim]: "A <-> B ==> A ==> B"proof (unfold iff_def)  assume "(A --> B) ∧ (B --> A)"  then have "A --> B" ..  then show "A ==> B" ..qedtheorem iff2 [elim]: "A <-> B ==> B ==> A"proof (unfold iff_def)  assume "(A --> B) ∧ (B --> A)"  then have "B --> A" ..  then show "B ==> A" ..qedsubsection {* 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)qedsubsection {* Quantifiers *}axiomatization  All :: "(i => o) => o"  (binder "∀" 10) and  Ex :: "(i => o) => o"  (binder "∃" 10)where  allI [intro]: "(!!x. P x) ==> ∀x. P x" and  allD [dest]: "∀x. P x ==> P a" and  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 show "∃y. P y"  proof    fix x assume "P (f x)"    then show ?thesis ..  qedqedlemma "(∃x. ∀y. R x y) --> (∀y. ∃x. R x y)"proof  assume "∃x. ∀y. R x y"  then show "∀y. ∃x. R x y"  proof    fix x assume a: "∀y. R x y"    show ?thesis    proof      fix y from a have "R x y" ..      then show "∃x. R x y" ..    qed  qedqedend`