Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: Set_Theory.thy Sprache: Isabelle

Original von: Isabelle^©

(*  Title:      HOL/ex/Set_Theory.thy
    Author:     Tobias Nipkow and Lawrence C Paulson
    Copyright   1991  University of Cambridge
*)

section \<open>Set Theory examples: Cantor's Theorem, Schröder-Bernstein Theorem, etc.\<close>

theory Set_Theory
imports Main
begin

text\<open>
  These two are cited in Benzmueller and Kohlhase's system description
  of LEO, CADE-15, 1998 (pages 139-143) as theorems LEO could not
  prove.
\<close>

lemma "(X = Y \ Z) =
    (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))"
  by blast

lemma "(X = Y \ Z) =
    (X \<subseteq> Y \<and> X \<subseteq> Z \<and> (\<forall>V. V \<subseteq> Y \<and> V \<subseteq> Z \<longrightarrow> V \<subseteq> X))"
  by blast

text \<open>
  Trivial example of term synthesis: apparently hard for some provers!
\<close>

schematic_goal "a \ b \ a \ ?X \ b \ ?X"
  by blast

subsection \<open>Examples for the \<open>blast\<close> paper\<close>

lemma "(\x \ C. f x \ g x) = \(f ` C) \ \(g ` C)"
  \<comment> \<open>Union-image, called \<open>Un_Union_image\<close> in Main HOL\<close>
  by blast

lemma "(\x \ C. f x \ g x) = \(f ` C) \ \(g ` C)"
  \<comment> \<open>Inter-image, called \<open>Int_Inter_image\<close> in Main HOL\<close>
  by blast

lemma singleton_example_1:
     "\S::'a set set. \x \ S. \y \ S. x \ y \ \z. S \ {z}"
  by blast

lemma singleton_example_2:
     "\x \ S. \S \ x \ \z. S \ {z}"
  \<comment> \<open>Variant of the problem above.\<close>
  by blast

lemma "\!x. f (g x) = x \ \!y. g (f y) = y"
  \<comment> \<open>A unique fixpoint theorem --- \<open>fast\<close>/\<open>best\<close>/\<open>meson\<close> all fail.\<close>
  by metis

subsection \<open>Cantor's Theorem: There is no surjection from a set to its powerset\<close>

lemma cantor1: "\ (\f:: 'a \ 'a set. \S. \x. f x = S)"
  \<comment> \<open>Requires best-first search because it is undirectional.\<close>
  by best

schematic_goal "\f:: 'a \ 'a set. \x. f x \ ?S f"
  \<comment> \<open>This form displays the diagonal term.\<close>
  by best

schematic_goal "?S \ range (f :: 'a \ 'a set)"
  \<comment> \<open>This form exploits the set constructs.\<close>
  by (rule notI, erule rangeE, best)

schematic_goal "?S \ range (f :: 'a \ 'a set)"
  \<comment> \<open>Or just this!\<close>
  by best

subsection \<open>The Schröder-Bernstein Theorem\<close>

lemma disj_lemma: "- (f ` X) = g' ` (-X) \ f a = g' b \ a \ X \ b \ X"
  by blast

lemma surj_if_then_else:
  "-(f ` X) = g' ` (-X) \ surj (\z. if z \ X then f z else g' z)"
  by (simp add: surj_def) blast

lemma bij_if_then_else:
  "inj_on f X \ inj_on g' (-X) \ -(f ` X) = g' ` (-X) \
    h = (\<lambda>z. if z \<in> X then f z else g' z) \<Longrightarrow> inj h \<and> surj h"
  apply (unfold inj_on_def)
  apply (simp add: surj_if_then_else)
  apply (blast dest: disj_lemma sym)
  done

lemma decomposition: "\X. X = - (g ` (- (f ` X)))"
  apply (rule exI)
  apply (rule lfp_unfold)
  apply (rule monoI, blast)
  done

theorem Schroeder_Bernstein:
  "inj (f :: 'a \ 'b) \ inj (g :: 'b \ 'a)
    \<Longrightarrow> \<exists>h:: 'a \<Rightarrow> 'b. inj h \<and> surj h"
  apply (rule decomposition [where f=f and g=g, THEN exE])
  apply (rule_tac x = "(\z. if z \ x then f z else inv g z)" in exI)
    \<comment> \<open>The term above can be synthesized by a sufficiently detailed proof.\<close>
  apply (rule bij_if_then_else)
     apply (rule_tac [4] refl)
    apply (rule_tac [2] inj_on_inv_into)
    apply (erule subset_inj_on [OF _ subset_UNIV])
   apply blast
  apply (erule ssubst, subst double_complement, erule image_inv_f_f [symmetric])
  done

subsection \<open>A simple party theorem\<close>

text\<open>\emph{At any party there are two people who know the same
number of people}. Provided the party consists of at least two people
and the knows relation is symmetric. Knowing yourself does not count
--- otherwise knows needs to be reflexive. (From Freek Wiedijk's talk
at TPHOLs 2007.)\<close>

lemma equal_number_of_acquaintances:
assumes "Domain R <= A" and "sym R" and "card A \ 2"
shows "\ inj_on (%a. card(R `` {a} - {a})) A"
proof -
  let ?N = "%a. card(R `` {a} - {a})"
  let ?n = "card A"
  have "finite A" using \<open>card A \<ge> 2\<close> by(auto intro:ccontr)
  have 0: "R `` A <= A" using \<open>sym R\<close> \<open>Domain R <= A\<close>
    unfolding Domain_unfold sym_def by blast
  have h: "\a\A. R `` {a} <= A" using 0 by blast
  hence 1: "\a\A. finite(R `` {a})" using \finite A\
    by(blast intro: finite_subset)
  have sub: "?N ` A <= {0..
  proof -
    have "\a\A. R `` {a} - {a} < A" using h by blast
    thus ?thesis using psubset_card_mono[OF \<open>finite A\<close>] by auto
  qed
  show "~ inj_on ?N A" (is "~ ?I")
  proof
    assume ?I
    hence "?n = card(?N ` A)" by(rule card_image[symmetric])
    with sub \<open>finite A\<close> have 2[simp]: "?N ` A = {0..<?n}"
      using subset_card_intvl_is_intvl[of _ 0] by(auto)
    have "0 \ ?N ` A" and "?n - 1 \ ?N ` A" using \card A \ 2\ by simp+
    then obtain a b where ab: "a\A" "b\A" and Na: "?N a = 0" and Nb: "?N b = ?n - 1"
      by (auto simp del: 2)
    have "a \ b" using Na Nb \card A \ 2\ by auto
    have "R `` {a} - {a} = {}" by (metis 1 Na ab card_eq_0_iff finite_Diff)
    hence "b \ R `` {a}" using \a\b\ by blast
    hence "a \ R `` {b}" by (metis Image_singleton_iff assms(2) sym_def)
    hence 3: "R `` {b} - {b} <= A - {a,b}" using 0 ab by blast
    have 4: "finite (A - {a,b})" using \<open>finite A\<close> by simp
    have "?N b <= ?n - 2" using ab \<open>a\<noteq>b\<close> \<open>finite A\<close> card_mono[OF 4 3] by simp
    then show False using Nb \<open>card A \<ge>  2\<close> by arith
  qed
qed

text \<open>
  From W. W. Bledsoe and Guohui Feng, SET-VAR. JAR 11 (3), 1993, pages
  293-314.

  Isabelle can prove the easy examples without any special mechanisms,
  but it can't prove the hard ones.
\<close>

lemma "\A. (\x \ A. x \ (0::int))"
  \<comment> \<open>Example 1, page 295.\<close>
  by force

lemma "D \ F \ \G. \A \ G. \B \ F. A \ B"
  \<comment> \<open>Example 2.\<close>
  by force

lemma "P a \ \A. (\x \ A. P x) \ (\y. y \ A)"
  \<comment> \<open>Example 3.\<close>
  by force

lemma "a < b \ b < (c::int) \ \A. a \ A \ b \ A \ c \ A"
  \<comment> \<open>Example 4.\<close>
  by auto \<comment> \<open>slow\<close>

lemma "P (f b) \ \s A. (\x \ A. P x) \ f s \ A"
  \<comment> \<open>Example 5, page 298.\<close>
  by force

lemma "P (f b) \ \s A. (\x \ A. P x) \ f s \ A"
  \<comment> \<open>Example 6.\<close>
  by force

lemma "\A. a \ A"
  \<comment> \<open>Example 7.\<close>
  by force

lemma "(\u v. u < (0::int) \ u \ \v\)
    \<longrightarrow> (\<exists>A::int set. -2 \<in> A & (\<forall>y. \<bar>y\<bar> \<notin> A))"
  \<comment> \<open>Example 8 needs a small hint.\<close>
  by force
    \<comment> \<open>not \<open>blast\<close>, which can't simplify \<open>-2 < 0\<close>\<close>

text \<open>Example 9 omitted (requires the reals).\<close>

text \<open>The paper has no Example 10!\<close>

lemma "(\A. 0 \ A \ (\x \ A. Suc x \ A) \ n \ A) \
  P 0 \<and> (\<forall>x. P x \<longrightarrow> P (Suc x)) \<longrightarrow> P n"
  \<comment> \<open>Example 11: needs a hint.\<close>
by(metis nat.induct)

lemma
  "(\A. (0, 0) \ A \ (\x y. (x, y) \ A \ (Suc x, Suc y) \ A) \ (n, m) \ A)
    \<and> P n \<longrightarrow> P m"
  \<comment> \<open>Example 12.\<close>
  by auto

lemma
  "(\x. (\u. x = 2 * u) = (\ (\v. Suc x = 2 * v))) \
    (\<exists>A. \<forall>x. (x \<in> A) = (Suc x \<notin> A))"
  \<comment> \<open>Example EO1: typo in article, and with the obvious fix it seems
      to require arithmetic reasoning.\<close>
  apply clarify
  apply (rule_tac x = "{x. \u. x = 2 * u}" in exI, auto)
   apply metis+
  done

end

¤ Dauer der Verarbeitung: 0.22 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.