# Theory First_Order_Logic

Up to index of Isabelle/FOL/ex

theory First_Order_Logic
imports Pure
begin

    (*  Title:      FOL/ex/First_Order_Logic.thy
        ID:         $Id: First_Order_Logic.thy,v 1.4 2005/06/17 14:15:08 haftmann Exp $
        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 *}

    consts
      false :: o    ("⊥")
      imp :: "o => o => o"    (infixr "-->" 25)
      conj :: "o => o => o"    (infixr "∧" 35)
      disj :: "o => o => o"    (infixr "∨" 30)

    axioms
      falseE [elim]: "⊥ ==> A"

      impI [intro]: "(A ==> B) ==> A --> B"
      mp [dest]: "A --> B ==> A ==> B"

      conjI [intro]: "A ==> B ==> A ∧ B"
      conjD1: "A ∧ B ==> A"
      conjD2: "A ∧ B ==> B"

      disjE [elim]: "A ∨ B ==> (A ==> C) ==> (B ==> C) ==> C"
      disjI1 [intro]: "A ==> A ∨ B"
      disjI2 [intro]: "B ==> A ∨ B"

    theorem conjE [elim]: "A ∧ B ==> (A ==> B ==> C) ==> C"
    proof -
      assume ab: "A ∧ B"
      assume r: "A ==> B ==> C"
      show C
      proof (rule r)
        from ab show A by (rule conjD1)
        from ab show B by (rule conjD2)
      qed
    qed

    constdefs
      true :: o    ("\<top>")
      "\<top> ≡ ⊥ --> ⊥"
      not :: "o => o"    ("¬ _" [40] 40)
      "¬ A ≡ A --> ⊥"
      iff :: "o => o => o"    (infixr "<->" 25)
      "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 ==> ⊥"
      thus "A --> ⊥" ..
    qed

    theorem notE [elim]: "¬ A ==> A ==> B"
    proof (unfold not_def)
      assume "A --> ⊥" and A
      hence ⊥ .. thus B ..
    qed

    theorem iffI [intro]: "(A ==> B) ==> (B ==> A) ==> A <-> B"
    proof (unfold iff_def)
      assume "A ==> B" hence "A --> B" ..
      moreover assume "B ==> A" hence "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)"
      hence "A --> B" ..
      thus "A ==> B" ..
    qed

    theorem iff2 [elim]: "A <-> B ==> B ==> A"
    proof (unfold iff_def)
      assume "(A --> B) ∧ (B --> A)"
      hence "B --> A" ..
      thus "B ==> A" ..
    qed

    subsection {* Equality *}

    consts
      equal :: "i => i => o"    (infixl "=" 50)

    axioms
      refl [intro]: "x = x"
      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 *}

    consts
      All :: "(i => o) => o"    (binder "∀" 10)
      Ex :: "(i => o) => o"    (binder "∃" 10)

    axioms
      allI [intro]: "(!!x. P(x)) ==> ∀x. P(x)"
      allD [dest]: "∀x. P(x) ==> P(a)"

      exI [intro]: "P(a) ==> ∃x. P(x)"
      exE [elim]: "∃x. P(x) ==> (!!x. P(x) ==> C) ==> C"

    lemma "(∃x. P(f(x))) --> (∃y. P(y))"
    proof
      assume "∃x. P(f(x))"
      thus "∃y. P(y)"
      proof
        fix x assume "P(f(x))"
        thus ?thesis ..
      qed
    qed

    lemma "(∃x. ∀y. R(x, y)) --> (∀y. ∃x. R(x, y))"
    proof
      assume "∃x. ∀y. R(x, y)"
      thus "∀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)" ..
          thus "∃x. R(x, y)" ..
        qed
      qed
    qed

    end

### Syntax

### Propositional logic

theorem conjE:

      [| A ∧ B; [| A; B |] ==> C |] ==> C

theorem trueI:

      \<top>

theorem notI:

      (A ==> ⊥) ==> ¬ A

theorem notE:

      [| ¬ A; A |] ==> B

theorem iffI:

      [| A ==> B; B ==> A |] ==> A <-> B

theorem iff1:

      [| A <-> B; A |] ==> B

theorem iff2:

      [| A <-> B; B |] ==> A

### Equality

theorem trans:

      [| x = y; y = z |] ==> x = z

theorem sym:

      x = y ==> y = x

### Quantifiers

lemma

      (∃x. P(f(x))) --> (∃y. P(y))

lemma

      (∃x. ∀y. R(x, y)) --> (∀y. ∃x. R(x, y))