Quelle Higher_Order_Logic.thy Sprache: Isabelle

(*  Title:      Pure/Examples/Higher_Order_Logic.thy
    Author:     Makarius
*)

section \<open>Foundations of HOL\<close>

theory Higher_Order_Logic
  imports Pure
begin

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

section \<open>HOL syntax within Pure\<close>

class type
default_sort type

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

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

section \<open>Minimal logic (axiomatization)\<close>

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 \<open>Derived connectives\<close>

definition False :: o
  where "False \ \A. A"

lemma FalseE [elim]:
  assumes "False"
  shows A
proof -
  from \<open>False\<close> have "\<forall>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 \<open>\<not> A\<close> have "A \<longrightarrow> False" by (simp only: not_def)
  from this and \<open>A\<close> 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 \<open>A\<close>
    also note \<open>B\<close>
    finally show C .
  qed
qed

lemma conjE [elim]:
  assumes "A \ B"
  obtains A and B
proof
  from \<open>A \<and> B\<close> have *: "(A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> 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 \<open>A\<close> 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 \<open>B\<close> show C ..
    qed
  qed
qed

lemma disjE [elim]:
  assumes "A \ B"
  obtains (a) A | (b) B
proof -
  from \<open>A \<or> B\<close> have "(A \<longrightarrow> thesis) \<longrightarrow> (B \<longrightarrow> thesis) \<longrightarrow> 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 \<open>P a\<close> show C ..
  qed
qed

lemma exE [elim]:
  assumes "\x. P x"
  obtains (that) x where "P x"
proof -
  from \<open>\<exists>x. P x\<close> have "(\<forall>x. P x \<longrightarrow> thesis) \<longrightarrow> 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 \<open>Extensional equality\<close>

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"
  for f g :: "'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 \<open>Cantor's Theorem\<close>

text \<open>
  Cantor's Theorem states that there is no surjection from a set to its
  powerset. The subsequent formulation uses elementary \<open>\<lambda>\<close>-calculus and
  predicate logic, with standard introduction and elimination rules.
\<close>

lemma iff_contradiction:
  assumes *: "\ A \ A"
  shows C
proof (rule notE)
  show "\ A"
  proof
    assume A
    with * have "\ A" ..
    from this and \<open>A\<close> 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 \<open>Characterization of Classical Logic\<close>

text \<open>
  The subsequent rules of classical reasoning are all equivalent.
\<close>

locale classical =
  assumes classical: "(\ A \ A) \ A"
  \<comment> \<open>predicate definition and hypothetical context\<close>
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 \<open>\<not> \<not> A\<close> 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 \<open>\<not> (A \<or> \<not> A)\<close> show False by (rule contradiction)
    qed
    then have "A \ \ A" ..
    with \<open>\<not> (A \<or> \<not> A)\<close> 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 \<open>Peirce's Law\<close>

text \<open>
  Peirce's Law is another characterization of classical reasoning. Its
  statement only requires implication.
\<close>

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 \<open>\<not> A\<close> show B by (rule contradiction)
    qed
    with * show A ..
  qed
qed

section \<open>Hilbert's choice operator (axiomatization)\<close>

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

syntax "_Eps" :: "pttrn \ o \ 'a" (\(\indent=3 notation=\binder SOME\\SOME _./ _)\ [0, 10] 10)
syntax_consts "_Eps" \<rightleftharpoons> Eps
translations "SOME x. P" \<rightleftharpoons> "CONST Eps (\<lambda>x. P)"

text \<open>
  \<^medskip>
  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).
  \<^medskip>
\<close>

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 \<open>Eps ?Q\<close>
        finally have "Eps ?P" .
        with \<open>\<not> Eps ?P\<close> 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 \<open>A\<close> have "A \<and> \<not> 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 \<open>A\<close> have "A \<and> x" ..
              then show ?thesis ..
            qed
          qed
        qed
        with neq show False by (rule contradiction)
      qed
      then show ?thesis ..
    qed
  qed
qed

text \<open>
  This means, the hypothetical predicate \<^const>\<open>classical\<close> always holds
  unconditionally (with all consequences).
\<close>

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

quality100%

¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.