Theory Higher_Order_Logic

theory Higher_Order_Logic
imports Pure
(*  Title:      HOL/Isar_Examples/Higher_Order_Logic.thy
    Author:     Makarius
*)

section ‹Foundations of HOL›

theory Higher_Order_Logic
  imports Pure
begin

text ‹
  The following theory development illustrates the foundations of Higher-Order
  Logic. The ``HOL'' logic that is given here resembles @{cite
  "Gordon:1985:HOL"} and its predecessor @{cite "church40"}, but the order of
  axiomatizations and defined connectives has be adapted to modern
  presentations of ‹λ›-calculus and Constructive Type Theory. Thus it fits
  nicely to the underlying Natural Deduction framework of Isabelle/Pure and
  Isabelle/Isar.
›


section ‹HOL syntax within Pure›

class type
default_sort type

typedecl o
instance o :: type ..
instance "fun" :: (type, type) type ..

judgment Trueprop :: "o ⇒ prop"  ("_" 5)


section ‹Minimal logic (axiomatization)›

axiomatization imp :: "o ⇒ o ⇒ o"  (infixr "⟶" 25)
  where impI [intro]: "(A ⟹ B) ⟹ A ⟶ B"
    and impE [dest, trans]: "A ⟶ B ⟹ A ⟹ B"

axiomatization All :: "('a ⇒ o) ⇒ o"  (binder "∀" 10)
  where allI [intro]: "(⋀x. P x) ⟹ ∀x. P x"
    and allE [dest]: "∀x. P x ⟹ P a"

lemma atomize_imp [atomize]: "(A ⟹ B) ≡ Trueprop (A ⟶ B)"
  by standard (fact impI, fact impE)

lemma atomize_all [atomize]: "(⋀x. P x) ≡ Trueprop (∀x. P x)"
  by standard (fact allI, fact allE)


subsubsection ‹Derived connectives›

definition False :: o
  where "False ≡ ∀A. A"

lemma FalseE [elim]:
  assumes "False"
  shows A
proof -
  from ‹False› have "∀A. A" by (simp only: False_def)
  then show A ..
qed


definition True :: o
  where "True ≡ False ⟶ False"

lemma TrueI [intro]: True
  unfolding True_def ..


definition not :: "o ⇒ o"  ("¬ _" [40] 40)
  where "not ≡ λA. A ⟶ False"

lemma notI [intro]:
  assumes "A ⟹ False"
  shows "¬ A"
  using assms unfolding not_def ..

lemma notE [elim]:
  assumes "¬ A" and A
  shows B
proof -
  from ‹¬ A› have "A ⟶ False" by (simp only: not_def)
  from this and ‹A› have "False" ..
  then show B ..
qed

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

lemmas contradiction = notE notE'   ‹proof by contradiction in any order›


definition conj :: "o ⇒ o ⇒ o"  (infixr "∧" 35)
  where "A ∧ B ≡ ∀C. (A ⟶ B ⟶ C) ⟶ C"

lemma conjI [intro]:
  assumes A and B
  shows "A ∧ B"
  unfolding conj_def
proof
  fix C
  show "(A ⟶ B ⟶ C) ⟶ C"
  proof
    assume "A ⟶ B ⟶ C"
    also note ‹A›
    also note ‹B›
    finally show C .
  qed
qed

lemma conjE [elim]:
  assumes "A ∧ B"
  obtains A and B
proof
  from ‹A ∧ B› have *: "(A ⟶ B ⟶ C) ⟶ C" for C
    unfolding conj_def ..
  show A
  proof -
    note * [of A]
    also have "A ⟶ B ⟶ A"
    proof
      assume A
      then show "B ⟶ A" ..
    qed
    finally show ?thesis .
  qed
  show B
  proof -
    note * [of B]
    also have "A ⟶ B ⟶ B"
    proof
      show "B ⟶ B" ..
    qed
    finally show ?thesis .
  qed
qed


definition disj :: "o ⇒ o ⇒ o"  (infixr "∨" 30)
  where "A ∨ B ≡ ∀C. (A ⟶ C) ⟶ (B ⟶ C) ⟶ C"

lemma disjI1 [intro]:
  assumes A
  shows "A ∨ B"
  unfolding disj_def
proof
  fix C
  show "(A ⟶ C) ⟶ (B ⟶ C) ⟶ C"
  proof
    assume "A ⟶ C"
    from this and ‹A› have C ..
    then show "(B ⟶ C) ⟶ C" ..
  qed
qed

lemma disjI2 [intro]:
  assumes B
  shows "A ∨ B"
  unfolding disj_def
proof
  fix C
  show "(A ⟶ C) ⟶ (B ⟶ C) ⟶ C"
  proof
    show "(B ⟶ C) ⟶ C"
    proof
      assume "B ⟶ C"
      from this and ‹B› show C ..
    qed
  qed
qed

lemma disjE [elim]:
  assumes "A ∨ B"
  obtains (a) A | (b) B
proof -
  from ‹A ∨ B› have "(A ⟶ thesis) ⟶ (B ⟶ thesis) ⟶ thesis"
    unfolding disj_def ..
  also have "A ⟶ thesis"
  proof
    assume A
    then show thesis by (rule a)
  qed
  also have "B ⟶ thesis"
  proof
    assume B
    then show thesis by (rule b)
  qed
  finally show thesis .
qed


definition Ex :: "('a ⇒ o) ⇒ o"  (binder "∃" 10)
  where "∃x. P x ≡ ∀C. (∀x. P x ⟶ C) ⟶ C"

lemma exI [intro]: "P a ⟹ ∃x. P x"
  unfolding Ex_def
proof
  fix C
  assume "P a"
  show "(∀x. P x ⟶ C) ⟶ C"
  proof
    assume "∀x. P x ⟶ C"
    then have "P a ⟶ C" ..
    from this and ‹P a› show C ..
  qed
qed

lemma exE [elim]:
  assumes "∃x. P x"
  obtains (that) x where "P x"
proof -
  from ‹∃x. P x› have "(∀x. P x ⟶ thesis) ⟶ thesis"
    unfolding Ex_def ..
  also have "∀x. P x ⟶ thesis"
  proof
    fix x
    show "P x ⟶ thesis"
    proof
      assume "P x"
      then show thesis by (rule that)
    qed
  qed
  finally show thesis .
qed


subsubsection ‹Extensional equality›

axiomatization equal :: "'a ⇒ 'a ⇒ o"  (infixl "=" 50)
  where refl [intro]: "x = x"
    and subst: "x = y ⟹ P x ⟹ P y"

abbreviation not_equal :: "'a ⇒ 'a ⇒ o"  (infixl "≠" 50)
  where "x ≠ y ≡ ¬ (x = y)"

abbreviation iff :: "o ⇒ o ⇒ o"  (infixr "⟷" 25)
  where "A ⟷ B ≡ A = B"

axiomatization
  where ext [intro]: "(⋀x. f x = g x) ⟹ f = g"
    and iff [intro]: "(A ⟹ B) ⟹ (B ⟹ A) ⟹ A ⟷ B"

lemma sym [sym]: "y = x" if "x = y"
  using that by (rule subst) (rule refl)

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

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

lemma arg_cong: "f x = f y" if "x = y"
  using that by (rule subst) (rule refl)

lemma fun_cong: "f x = g x" if "f = g"
  using that by (rule subst) (rule refl)

lemma trans [trans]: "x = y ⟹ y = z ⟹ x = z"
  by (rule subst)

lemma iff1 [elim]: "A ⟷ B ⟹ A ⟹ B"
  by (rule subst)

lemma iff2 [elim]: "A ⟷ B ⟹ B ⟹ A"
  by (rule subst) (rule sym)


subsection ‹Cantor's Theorem›

text ‹
  Cantor's Theorem states that there is no surjection from a set to its
  powerset. The subsequent formulation uses elementary ‹λ›-calculus and
  predicate logic, with standard introduction and elimination rules.
›

lemma iff_contradiction:
  assumes *: "¬ A ⟷ A"
  shows C
proof (rule notE)
  show "¬ A"
  proof
    assume A
    with * have "¬ A" ..
    from this and ‹A› show False ..
  qed
  with * show A ..
qed

theorem Cantor: "¬ (∃f :: 'a ⇒ 'a ⇒ o. ∀A. ∃x. A = f x)"
proof
  assume "∃f :: 'a ⇒ 'a ⇒ o. ∀A. ∃x. A = f x"
  then obtain f :: "'a ⇒ 'a ⇒ o" where *: "∀A. ∃x. A = f x" ..
  let ?D = "λx. ¬ f x x"
  from * have "∃x. ?D = f x" ..
  then obtain a where "?D = f a" ..
  then have "?D a ⟷ f a a" using refl by (rule subst)
  then have "¬ f a a ⟷ f a a" .
  then show False by (rule iff_contradiction)
qed


subsection ‹Characterization of Classical Logic›

text ‹
  The subsequent rules of classical reasoning are all equivalent.
›

locale classical =
  assumes classical: "(¬ A ⟹ A) ⟹ A"
   ‹predicate definition and hypothetical context›
begin

lemma classical_contradiction:
  assumes "¬ A ⟹ False"
  shows A
proof (rule classical)
  assume "¬ A"
  then have False by (rule assms)
  then show A ..
qed

lemma double_negation:
  assumes "¬ ¬ A"
  shows A
proof (rule classical_contradiction)
  assume "¬ A"
  with ‹¬ ¬ A› show False by (rule contradiction)
qed

lemma tertium_non_datur: "A ∨ ¬ A"
proof (rule double_negation)
  show "¬ ¬ (A ∨ ¬ A)"
  proof
    assume "¬ (A ∨ ¬ A)"
    have "¬ A"
    proof
      assume A then have "A ∨ ¬ A" ..
      with ‹¬ (A ∨ ¬ A)› show False by (rule contradiction)
    qed
    then have "A ∨ ¬ A" ..
    with ‹¬ (A ∨ ¬ A)› show False by (rule contradiction)
  qed
qed

lemma classical_cases:
  obtains A | "¬ A"
  using tertium_non_datur
proof
  assume A
  then show thesis ..
next
  assume "¬ A"
  then show thesis ..
qed

end

lemma classical_if_cases: classical
  if cases: "⋀A C. (A ⟹ C) ⟹ (¬ A ⟹ C) ⟹ C"
proof
  fix A
  assume *: "¬ A ⟹ A"
  show A
  proof (rule cases)
    assume A
    then show A .
  next
    assume "¬ A"
    then show A by (rule *)
  qed
qed


section ‹Peirce's Law›

text ‹
  Peirce's Law is another characterization of classical reasoning. Its
  statement only requires implication.
›

theorem (in classical) Peirce's_Law: "((A ⟶ B) ⟶ A) ⟶ A"
proof
  assume *: "(A ⟶ B) ⟶ A"
  show A
  proof (rule classical)
    assume "¬ A"
    have "A ⟶ B"
    proof
      assume A
      with ‹¬ A› show B by (rule contradiction)
    qed
    with * show A ..
  qed
qed


section ‹Hilbert's choice operator (axiomatization)›

axiomatization Eps :: "('a ⇒ o) ⇒ 'a"
  where someI: "P x ⟹ P (Eps P)"

syntax "_Eps" :: "pttrn ⇒ o ⇒ 'a"  ("(3SOME _./ _)" [0, 10] 10)
translations "SOME x. P"  "CONST Eps (λx. P)"

text ‹
  ┉
  It follows a derivation of the classical law of tertium-non-datur by
  means of Hilbert's choice operator (due to Berghofer, Beeson, Harrison,
  based on a proof by Diaconescu).
  ┉
›

theorem Diaconescu: "A ∨ ¬ A"
proof -
  let ?P = "λx. (A ∧ x) ∨ ¬ x"
  let ?Q = "λx. (A ∧ ¬ x) ∨ x"

  have a: "?P (Eps ?P)"
  proof (rule someI)
    have "¬ False" ..
    then show "?P False" ..
  qed
  have b: "?Q (Eps ?Q)"
  proof (rule someI)
    have True ..
    then show "?Q True" ..
  qed

  from a show ?thesis
  proof
    assume "A ∧ Eps ?P"
    then have A ..
    then show ?thesis ..
  next
    assume "¬ Eps ?P"
    from b show ?thesis
    proof
      assume "A ∧ ¬ Eps ?Q"
      then have A ..
      then show ?thesis ..
    next
      assume "Eps ?Q"
      have neq: "?P ≠ ?Q"
      proof
        assume "?P = ?Q"
        then have "Eps ?P ⟷ Eps ?Q" by (rule arg_cong)
        also note ‹Eps ?Q›
        finally have "Eps ?P" .
        with ‹¬ Eps ?P› show False by (rule contradiction)
      qed
      have "¬ A"
      proof
        assume A
        have "?P = ?Q"
        proof (rule ext)
          show "?P x ⟷ ?Q x" for x
          proof
            assume "?P x"
            then show "?Q x"
            proof
              assume "¬ x"
              with ‹A› have "A ∧ ¬ x" ..
              then show ?thesis ..
            next
              assume "A ∧ x"
              then have x ..
              then show ?thesis ..
            qed
          next
            assume "?Q x"
            then show "?P x"
            proof
              assume "A ∧ ¬ x"
              then have "¬ x" ..
              then show ?thesis ..
            next
              assume x
              with ‹A› have "A ∧ x" ..
              then show ?thesis ..
            qed
          qed
        qed
        with neq show False by (rule contradiction)
      qed
      then show ?thesis ..
    qed
  qed
qed

text ‹
  This means, the hypothetical predicate @{const classical} always holds
  unconditionally (with all consequences).
›

interpretation classical
proof (rule classical_if_cases)
  fix A C
  assume *: "A ⟹ C"
    and **: "¬ A ⟹ C"
  from Diaconescu [of A] show C
  proof
    assume A
    then show C by (rule *)
  next
    assume "¬ A"
    then show C by (rule **)
  qed
qed

thm classical
  classical_contradiction
  double_negation
  tertium_non_datur
  classical_cases
  Peirce's_Law

end