# Theory First_Order_Logic

theory First_Order_Logic
imports Pure
```(*  Title:      HOL/Isar_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
```