Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Cantor.thy Sprache: Isabelle

Original von: Isabelle^©

(*  Title:      HOL/Examples/Cantor.thy
    Author:     Makarius
*)

section \<open>Cantor's Theorem\<close>

theory Cantor
  imports Main
begin

subsection \<open>Mathematical statement and proof\<close>

text \<open>
  Cantor's Theorem states that there is no surjection from
  a set to its powerset.  The proof works by diagonalization.  E.g.\ see
  \<^item> \<^url>\<open>http://mathworld.wolfram.com/CantorDiagonalMethod.html\<close>
  \<^item> \<^url>\<open>https://en.wikipedia.org/wiki/Cantor's_diagonal_argument\<close>
\<close>

theorem Cantor: "\f :: 'a \ 'a set. \A. \x. A = f x"
proof
  assume "\f :: 'a \ 'a set. \A. \x. A = f x"
  then obtain f :: "'a \ 'a set" where *: "\A. \x. A = f x" ..
  let ?D = "{x. x \ f x}"
  from * obtain a where "?D = f a" by blast
  moreover have "a \ ?D \ a \ f a" by blast
  ultimately show False by blast
qed

subsection \<open>Automated proofs\<close>

text \<open>
  These automated proofs are much shorter, but lack information why and how it
  works.
\<close>

theorem "\f :: 'a \ 'a set. \A. \x. f x = A"
  by best

theorem "\f :: 'a \ 'a set. \A. \x. f x = A"
  by force

subsection \<open>Elementary version in higher-order predicate logic\<close>

text \<open>
  The subsequent formulation bypasses set notation of HOL; it uses elementary
  \<open>\<lambda>\<close>-calculus and predicate logic, with standard introduction and elimination
  rules. This also shows that the proof does not require classical reasoning.
\<close>

lemma iff_contradiction:
  assumes *: "\ A \ A"
  shows False
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 \ bool. \A. \x. A = f x"
proof
  assume "\f :: 'a \ 'a \ bool. \A. \x. A = f x"
  then obtain f :: "'a \ 'a \ bool" 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" by (rule arg_cong)
  then have "\ f a a \ f a a" .
  then show False by (rule iff_contradiction)
qed

subsection \<open>Classic Isabelle/HOL example\<close>

text \<open>
  The following treatment of Cantor's Theorem follows the classic example from
  the early 1990s, e.g.\ see the file \<^verbatim>\<open>92/HOL/ex/set.ML\<close> in
  Isabelle92 or @{cite \<open>\S18.7\<close> "paulson-isa-book"}. The old tactic scripts
  synthesize key information of the proof by refinement of schematic goal
  states. In contrast, the Isar proof needs to say explicitly what is proven.

  \<^bigskip>
  Cantor's Theorem states that every set has more subsets than it has
  elements. It has become a favourite basic example in pure higher-order logic
  since it is so easily expressed:

  @{text [display]
  \<open>\<forall>f::\<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool. \<exists>S::\<alpha> \<Rightarrow> bool. \<forall>x::\<alpha>. f x \<noteq> S\<close>}

  Viewing types as sets, \<open>\<alpha> \<Rightarrow> bool\<close> represents the powerset of \<open>\<alpha>\<close>. This
  version of the theorem states that for every function from \<open>\<alpha>\<close> to its
  powerset, some subset is outside its range. The Isabelle/Isar proofs below
  uses HOL's set theory, with the type \\ set\ and the operator \range :: (\ \
  \<beta>) \<Rightarrow> \<beta> set\<close>.
\<close>

theorem "\S. S \ range (f :: 'a \ 'a set)"
proof
  let ?S = "{x. x \ f x}"
  show "?S \ range f"
  proof
    assume "?S \ range f"
    then obtain y where "?S = f y" ..
    then show False
    proof (rule equalityCE)
      assume "y \ f y"
      assume "y \ ?S"
      then have "y \ f y" ..
      with \<open>y \<in> f y\<close> show ?thesis by contradiction
    next
      assume "y \ ?S"
      assume "y \ f y"
      then have "y \ ?S" ..
      with \<open>y \<notin> ?S\<close> show ?thesis by contradiction
    qed
  qed
qed

text \<open>
  How much creativity is required? As it happens, Isabelle can prove this
  theorem automatically using best-first search. Depth-first search would
  diverge, but best-first search successfully navigates through the large
  search space. The context of Isabelle's classical prover contains rules for
  the relevant constructs of HOL's set theory.
\<close>

theorem "\S. S \ range (f :: 'a \ 'a set)"
  by best

end

¤ Dauer der Verarbeitung: 0.18 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.