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 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