src/HOL/ex/set.thy

no longer declare .psimps rules as [simp].

This regularly caused confusion (e.g., they show up in simp traces
when the regular simp rules are disabled). In the few places where the
rules are used, explicitly mentioning them actually clarifies the
proof text.

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

header {* Set Theory examples: Cantor's Theorem, Schröder-Bernstein Theorem, etc. *}

theory set imports Main begin

text{*
  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.
*}

lemma "(X = Y \<union> 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 \<inter> 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 {*
  Trivial example of term synthesis: apparently hard for some provers!
*}

schematic_lemma "a \<noteq> b \<Longrightarrow> a \<in> ?X \<and> b \<notin> ?X"
  by blast


subsection {* Examples for the @{text blast} paper *}

lemma "(\<Union>x \<in> C. f x \<union> g x) = \<Union>(f ` C)  \<union>  \<Union>(g ` C)"
  -- {* Union-image, called @{text Un_Union_image} in Main HOL *}
  by blast

lemma "(\<Inter>x \<in> C. f x \<inter> g x) = \<Inter>(f ` C) \<inter> \<Inter>(g ` C)"
  -- {* Inter-image, called @{text Int_Inter_image} in Main HOL *}
  by blast

lemma singleton_example_1:
     "\<And>S::'a set set. \<forall>x \<in> S. \<forall>y \<in> S. x \<subseteq> y \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
  by blast

lemma singleton_example_2:
     "\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
  -- {*Variant of the problem above. *}
  by blast

lemma "\<exists>!x. f (g x) = x \<Longrightarrow> \<exists>!y. g (f y) = y"
  -- {* A unique fixpoint theorem --- @{text fast}/@{text best}/@{text meson} all fail. *}
  by metis


subsection {* Cantor's Theorem: There is no surjection from a set to its powerset *}

lemma cantor1: "\<not> (\<exists>f:: 'a \<Rightarrow> 'a set. \<forall>S. \<exists>x. f x = S)"
  -- {* Requires best-first search because it is undirectional. *}
  by best

schematic_lemma "\<forall>f:: 'a \<Rightarrow> 'a set. \<forall>x. f x \<noteq> ?S f"
  -- {*This form displays the diagonal term. *}
  by best

schematic_lemma "?S \<notin> range (f :: 'a \<Rightarrow> 'a set)"
  -- {* This form exploits the set constructs. *}
  by (rule notI, erule rangeE, best)

schematic_lemma "?S \<notin> range (f :: 'a \<Rightarrow> 'a set)"
  -- {* Or just this! *}
  by best


subsection {* The Schröder-Berstein Theorem *}

lemma disj_lemma: "- (f ` X) = g ` (-X) \<Longrightarrow> f a = g b \<Longrightarrow> a \<in> X \<Longrightarrow> b \<in> X"
  by blast

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

lemma bij_if_then_else:
  "inj_on f X \<Longrightarrow> inj_on g (-X) \<Longrightarrow> -(f ` X) = g ` (-X) \<Longrightarrow>
    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: "\<exists>X. X = - (g ` (- (f ` X)))"
  apply (rule exI)
  apply (rule lfp_unfold)
  apply (rule monoI, blast)
  done

theorem Schroeder_Bernstein:
  "inj (f :: 'a \<Rightarrow> 'b) \<Longrightarrow> inj (g :: 'b \<Rightarrow> '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 = "(\<lambda>z. if z \<in> x then f z else inv g z)" in exI) 
    --{*The term above can be synthesized by a sufficiently detailed proof.*}
  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 inv_image_comp [symmetric])
  done


subsection {* A simple party theorem *}

text{* \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.) *}

lemma equal_number_of_acquaintances:
assumes "Domain R <= A" and "sym R" and "card A \<ge> 2"
shows "\<not> inj_on (%a. card(R `` {a} - {a})) A"
proof -
  let ?N = "%a. card(R `` {a} - {a})"
  let ?n = "card A"
  have "finite A" using `card A \<ge> 2` by(auto intro:ccontr)
  have 0: "R `` A <= A" using `sym R` `Domain R <= A`
    unfolding Domain_def sym_def by blast
  have h: "ALL a:A. R `` {a} <= A" using 0 by blast
  hence 1: "ALL a:A. finite(R `` {a})" using `finite A`
    by(blast intro: finite_subset)
  have sub: "?N ` A <= {0..<?n}"
  proof -
    have "ALL a:A. R `` {a} - {a} < A" using h by blast
    thus ?thesis using psubset_card_mono[OF `finite A`] 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 `finite A` 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 \<ge> 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 \<noteq> b" using Na Nb `card A \<ge> 2` by auto
    have "R `` {a} - {a} = {}" by (metis 1 Na ab card_eq_0_iff finite_Diff)
    hence "b \<notin> R `` {a}" using `a\<noteq>b` by blast
    hence "a \<notin> 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 `finite A` by simp
    have "?N b <= ?n - 2" using ab `a\<noteq>b` `finite A` card_mono[OF 4 3] by simp
    then show False using Nb `card A \<ge>  2` by arith
  qed
qed

text {*
  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.
*}

lemma "\<exists>A. (\<forall>x \<in> A. x \<le> (0::int))"
  -- {* Example 1, page 295. *}
  by force

lemma "D \<in> F \<Longrightarrow> \<exists>G. \<forall>A \<in> G. \<exists>B \<in> F. A \<subseteq> B"
  -- {* Example 2. *}
  by force

lemma "P a \<Longrightarrow> \<exists>A. (\<forall>x \<in> A. P x) \<and> (\<exists>y. y \<in> A)"
  -- {* Example 3. *}
  by force

lemma "a < b \<and> b < (c::int) \<Longrightarrow> \<exists>A. a \<notin> A \<and> b \<in> A \<and> c \<notin> A"
  -- {* Example 4. *}
  by force

lemma "P (f b) \<Longrightarrow> \<exists>s A. (\<forall>x \<in> A. P x) \<and> f s \<in> A"
  -- {*Example 5, page 298. *}
  by force

lemma "P (f b) \<Longrightarrow> \<exists>s A. (\<forall>x \<in> A. P x) \<and> f s \<in> A"
  -- {* Example 6. *}
  by force

lemma "\<exists>A. a \<notin> A"
  -- {* Example 7. *}
  by force

lemma "(\<forall>u v. u < (0::int) \<longrightarrow> u \<noteq> abs v)
    \<longrightarrow> (\<exists>A::int set. (\<forall>y. abs y \<notin> A) \<and> -2 \<in> A)"
  -- {* Example 8 now needs a small hint. *}
  by (simp add: abs_if, force)
    -- {* not @{text blast}, which can't simplify @{text "-2 < 0"} *}

text {* Example 9 omitted (requires the reals). *}

text {* The paper has no Example 10! *}

lemma "(\<forall>A. 0 \<in> A \<and> (\<forall>x \<in> A. Suc x \<in> A) \<longrightarrow> n \<in> A) \<and>
  P 0 \<and> (\<forall>x. P x \<longrightarrow> P (Suc x)) \<longrightarrow> P n"
  -- {* Example 11: needs a hint. *}
by(metis Nat.induct)

lemma
  "(\<forall>A. (0, 0) \<in> A \<and> (\<forall>x y. (x, y) \<in> A \<longrightarrow> (Suc x, Suc y) \<in> A) \<longrightarrow> (n, m) \<in> A)
    \<and> P n \<longrightarrow> P m"
  -- {* Example 12. *}
  by auto

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

end