Theory First_Order_Logic

(*  Title:      Pure/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