# Theory Higher_Order_Logic

Up to index of Isabelle/HOL/ex

theory Higher_Order_Logic
imports CPure
begin

    (*  Title:      HOL/ex/Higher_Order_Logic.thy
        ID:         $Id: Higher_Order_Logic.thy,v 1.6 2005/06/17 14:12:49 haftmann Exp $
        Author:     Gertrud Bauer and Markus Wenzel, TU Muenchen
    *)

    header {* Foundations of HOL *}

    theory Higher_Order_Logic imports CPure begin

    text {*
      The following theory development demonstrates Higher-Order Logic
      itself, represented directly within the Pure framework of Isabelle.
      The ``HOL'' logic given here is essentially that of Gordon
      \cite{Gordon:1985:HOL}, although we prefer to present basic concepts
      in a slightly more conventional manner oriented towards plain
      Natural Deduction.
    *}

    subsection {* Pure Logic *}

    classes type
    defaultsort type

    typedecl o
    arities
      o :: type
      fun :: (type, type) type

    subsubsection {* Basic logical connectives *}

    judgment
      Trueprop :: "o => prop"    ("_" 5)

    consts
      imp :: "o => o => o"    (infixr "-->" 25)
      All :: "('a => o) => o"    (binder "∀" 10)

    axioms
      impI [intro]: "(A ==> B) ==> A --> B"
      impE [dest, trans]: "A --> B ==> A ==> B"
      allI [intro]: "(!!x. P x) ==> ∀x. P x"
      allE [dest]: "∀x. P x ==> P a"

    subsubsection {* Extensional equality *}

    consts
      equal :: "'a => 'a => o"   (infixl "=" 50)

    axioms
      refl [intro]: "x = x"
      subst: "x = y ==> P x ==> P y"
      ext [intro]: "(!!x. f x = g x) ==> f = g"
      iff [intro]: "(A ==> B) ==> (B ==> A) ==> A = B"

    theorem sym [sym]: "x = y ==> y = x"
    proof -
      assume "x = y"
      thus "y = x" by (rule subst) (rule refl)
    qed

    lemma [trans]: "x = y ==> P y ==> P x"
      by (rule subst) (rule sym)

    lemma [trans]: "P x ==> x = y ==> P y"
      by (rule subst)

    theorem trans [trans]: "x = y ==> y = z ==> x = z"
      by (rule subst)

    theorem iff1 [elim]: "A = B ==> A ==> B"
      by (rule subst)

    theorem iff2 [elim]: "A = B ==> B ==> A"
      by (rule subst) (rule sym)

    subsubsection {* Derived connectives *}

    constdefs
      false :: o    ("⊥")
      "⊥ ≡ ∀A. A"
      true :: o    ("\<top>")
      "\<top> ≡ ⊥ --> ⊥"
      not :: "o => o"     ("¬ _" [40] 40)
      "not ≡ λA. A --> ⊥"
      conj :: "o => o => o"    (infixr "∧" 35)
      "conj ≡ λA B. ∀C. (A --> B --> C) --> C"
      disj :: "o => o => o"    (infixr "∨" 30)
      "disj ≡ λA B. ∀C. (A --> C) --> (B --> C) --> C"
      Ex :: "('a => o) => o"    (binder "∃" 10)
      "Ex ≡ λP. ∀C. (∀x. P x --> C) --> C"

    syntax
      "_not_equal" :: "'a => 'a => o"    (infixl "≠" 50)
    translations
      "x ≠ y"  \<rightleftharpoons>  "¬ (x = y)"

    theorem falseE [elim]: "⊥ ==> A"
    proof (unfold false_def)
      assume "∀A. A"
      thus A ..
    qed

    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 --> ⊥"
      also assume A
      finally have ⊥ ..
      thus B ..
    qed

    lemma notE': "A ==> ¬ A ==> B"
      by (rule notE)

    lemmas contradiction = notE notE'  -- {* proof by contradiction in any order *}

    theorem conjI [intro]: "A ==> B ==> A ∧ B"
    proof (unfold conj_def)
      assume A and B
      show "∀C. (A --> B --> C) --> C"
      proof
        fix C show "(A --> B --> C) --> C"
        proof
          assume "A --> B --> C"
          also have A .
          also have B .
          finally show C .
        qed
      qed
    qed

    theorem conjE [elim]: "A ∧ B ==> (A ==> B ==> C) ==> C"
    proof (unfold conj_def)
      assume c: "∀C. (A --> B --> C) --> C"
      assume "A ==> B ==> C"
      moreover {
        from c have "(A --> B --> A) --> A" ..
        also have "A --> B --> A"
        proof
          assume A
          thus "B --> A" ..
        qed
        finally have A .
      } moreover {
        from c have "(A --> B --> B) --> B" ..
        also have "A --> B --> B"
        proof
          show "B --> B" ..
        qed
        finally have B .
      } ultimately show C .
    qed

    theorem disjI1 [intro]: "A ==> A ∨ B"
    proof (unfold disj_def)
      assume A
      show "∀C. (A --> C) --> (B --> C) --> C"
      proof
        fix C show "(A --> C) --> (B --> C) --> C"
        proof
          assume "A --> C"
          also have A .
          finally have C .
          thus "(B --> C) --> C" ..
        qed
      qed
    qed

    theorem disjI2 [intro]: "B ==> A ∨ B"
    proof (unfold disj_def)
      assume B
      show "∀C. (A --> C) --> (B --> C) --> C"
      proof
        fix C show "(A --> C) --> (B --> C) --> C"
        proof
          show "(B --> C) --> C"
          proof
            assume "B --> C"
            also have B .
            finally show C .
          qed
        qed
      qed
    qed

    theorem disjE [elim]: "A ∨ B ==> (A ==> C) ==> (B ==> C) ==> C"
    proof (unfold disj_def)
      assume c: "∀C. (A --> C) --> (B --> C) --> C"
      assume r1: "A ==> C" and r2: "B ==> C"
      from c have "(A --> C) --> (B --> C) --> C" ..
      also have "A --> C"
      proof
        assume A thus C by (rule r1)
      qed
      also have "B --> C"
      proof
        assume B thus C by (rule r2)
      qed
      finally show C .
    qed

    theorem exI [intro]: "P a ==> ∃x. P x"
    proof (unfold Ex_def)
      assume "P a"
      show "∀C. (∀x. P x --> C) --> C"
      proof
        fix C show "(∀x. P x --> C) --> C"
        proof
          assume "∀x. P x --> C"
          hence "P a --> C" ..
          also have "P a" .
          finally show C .
        qed
      qed
    qed

    theorem exE [elim]: "∃x. P x ==> (!!x. P x ==> C) ==> C"
    proof (unfold Ex_def)
      assume c: "∀C. (∀x. P x --> C) --> C"
      assume r: "!!x. P x ==> C"
      from c have "(∀x. P x --> C) --> C" ..
      also have "∀x. P x --> C"
      proof
        fix x show "P x --> C"
        proof
          assume "P x"
          thus C by (rule r)
        qed
      qed
      finally show C .
    qed

    subsection {* Classical logic *}

    locale classical =
      assumes classical: "(¬ A ==> A) ==> A"

    theorem (in classical)
      Peirce's_Law: "((A --> B) --> A) --> A"
    proof
      assume a: "(A --> B) --> A"
      show A
      proof (rule classical)
        assume "¬ A"
        have "A --> B"
        proof
          assume A
          thus B by (rule contradiction)
        qed
        with a show A ..
      qed
    qed

    theorem (in classical)
      double_negation: "¬ ¬ A ==> A"
    proof -
      assume "¬ ¬ A"
      show A
      proof (rule classical)
        assume "¬ A"
        thus ?thesis by (rule contradiction)
      qed
    qed

    theorem (in classical)
      tertium_non_datur: "A ∨ ¬ A"
    proof (rule double_negation)
      show "¬ ¬ (A ∨ ¬ A)"
      proof
        assume "¬ (A ∨ ¬ A)"
        have "¬ A"
        proof
          assume A hence "A ∨ ¬ A" ..
          thus ⊥ by (rule contradiction)
        qed
        hence "A ∨ ¬ A" ..
        thus ⊥ by (rule contradiction)
      qed
    qed

    theorem (in classical)
      classical_cases: "(A ==> C) ==> (¬ A ==> C) ==> C"
    proof -
      assume r1: "A ==> C" and r2: "¬ A ==> C"
      from tertium_non_datur show C
      proof
        assume A
        thus ?thesis by (rule r1)
      next
        assume "¬ A"
        thus ?thesis by (rule r2)
      qed
    qed

    lemma (in classical) "(¬ A ==> A) ==> A"  (* FIXME *)
    proof -
      assume r: "¬ A ==> A"
      show A
      proof (rule classical_cases)
        assume A thus A .
      next
        assume "¬ A" thus A by (rule r)
      qed
    qed

    end

### Pure Logic

#### Basic logical connectives

#### Extensional equality

theorem sym:

      x = y ==> y = x

lemma

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

lemma

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

theorem trans:

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

theorem iff1:

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

theorem iff2:

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

#### Derived connectives

theorem falseE:

      ⊥ ==> A

theorem trueI:

      \<top>

theorem notI:

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

theorem notE:

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

lemma notE':

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

lemmas contradiction:

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

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

lemmas contradiction:

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

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

theorem conjI:

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

theorem conjE:

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

theorem disjI1:

      A ==> A ∨ B

theorem disjI2:

      B ==> A ∨ B

theorem disjE:

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

theorem exI:

      P a ==> ∃x. P x

theorem exE:

      [| ∃x. P x; !!x. P x ==> C |] ==> C

### Classical logic

theorem Peirce's_Law:

      PROP classical ==> ((A --> B) --> A) --> A

theorem double_negation:

      [| PROP classical; ¬ ¬ A |] ==> A

theorem tertium_non_datur:

      PROP classical ==> A ∨ ¬ A

theorem classical_cases:

      [| PROP classical; A ==> C; ¬ A ==> C |] ==> C

lemma

      [| PROP classical; ¬ A ==> A |] ==> A