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