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 begin

text {*

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 i

typedecl o

judgment

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 B

proof

from `A ∧ B` show A by (rule conjD1)

from `A ∧ B` show B by (rule conjD2)

qed

definition

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 "⊥ --> ⊥" ..

qed

theorem notI [intro]: "(A ==> ⊥) ==> ¬ A"

proof (unfold not_def)

assume "A ==> ⊥"

then show "A --> ⊥" ..

qed

theorem notE [elim]: "¬ A ==> A ==> B"

proof (unfold not_def)

assume "A --> ⊥" and A

then have ⊥ .. then show B ..

qed

theorem 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)" ..

qed

theorem iff1 [elim]: "A <-> B ==> A ==> B"

proof (unfold iff_def)

assume "(A --> B) ∧ (B --> A)"

then have "A --> B" ..

then show "A ==> B" ..

qed

theorem iff2 [elim]: "A <-> B ==> B ==> A"

proof (unfold iff_def)

assume "(A --> B) ∧ (B --> A)"

then have "B --> A" ..

then show "B ==> 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) 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 ..

qed

qed

lemma "(∃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

qed

qed

end