diff -r 971d1be5d5ce -r fe769a0fcc96 src/HOL/ex/Set_Theory.thy
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Set_Theory.thy Thu Aug 18 13:10:24 2011 +0200
@@ -0,0 +1,227 @@
+(* Title: HOL/ex/Set_Theory.thy
+ 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_Theory
+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 \ Z) =
+ (Y \ X \ Z \ X \ (\V. Y \ V \ Z \ V \ X \ V))"
+ by blast
+
+lemma "(X = Y \ Z) =
+ (X \ Y \ X \ Z \ (\V. V \ Y \ V \ Z \ V \ X))"
+ by blast
+
+text {*
+ Trivial example of term synthesis: apparently hard for some provers!
+*}
+
+schematic_lemma "a \ b \ a \ ?X \ b \ ?X"
+ by blast
+
+
+subsection {* Examples for the @{text blast} paper *}
+
+lemma "(\x \ C. f x \ g x) = \(f ` C) \ \(g ` C)"
+ -- {* Union-image, called @{text Un_Union_image} in Main HOL *}
+ by blast
+
+lemma "(\x \ C. f x \ g x) = \(f ` C) \ \(g ` C)"
+ -- {* Inter-image, called @{text Int_Inter_image} in Main HOL *}
+ 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}"
+ -- {*Variant of the problem above. *}
+ by blast
+
+lemma "\!x. f (g x) = x \ \!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: "\ (\f:: 'a \ 'a set. \S. \x. f x = S)"
+ -- {* Requires best-first search because it is undirectional. *}
+ by best
+
+schematic_lemma "\f:: 'a \ 'a set. \x. f x \ ?S f"
+ -- {*This form displays the diagonal term. *}
+ by best
+
+schematic_lemma "?S \ range (f :: 'a \ 'a set)"
+ -- {* This form exploits the set constructs. *}
+ by (rule notI, erule rangeE, best)
+
+schematic_lemma "?S \ range (f :: 'a \ 'a set)"
+ -- {* Or just this! *}
+ by best
+
+
+subsection {* The SchrÃ¶der-Berstein Theorem *}
+
+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 = (\z. if z \ X then f z else g z) \ inj h \ 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)
+ \ \h:: 'a \ 'b. inj h \ 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)
+ --{*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 \ 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 `card A \ 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.. 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 `finite A` by simp
+ have "?N b <= ?n - 2" using ab `a\b` `finite A` card_mono[OF 4 3] by simp
+ then show False using Nb `card A \ 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 "\A. (\x \ A. x \ (0::int))"
+ -- {* Example 1, page 295. *}
+ by force
+
+lemma "D \ F \ \G. \A \ G. \B \ F. A \ B"
+ -- {* Example 2. *}
+ by force
+
+lemma "P a \ \A. (\x \ A. P x) \ (\y. y \ A)"
+ -- {* Example 3. *}
+ by force
+
+lemma "a < b \ b < (c::int) \ \A. a \ A \ b \ A \ c \ A"
+ -- {* Example 4. *}
+ by force
+
+lemma "P (f b) \ \s A. (\x \ A. P x) \ f s \ A"
+ -- {*Example 5, page 298. *}
+ by force
+
+lemma "P (f b) \ \s A. (\x \ A. P x) \ f s \ A"
+ -- {* Example 6. *}
+ by force
+
+lemma "\A. a \ A"
+ -- {* Example 7. *}
+ by force
+
+lemma "(\u v. u < (0::int) \ u \ abs v)
+ \ (\A::int set. (\y. abs y \ A) \ -2 \ 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 "(\A. 0 \ A \ (\x \ A. Suc x \ A) \ n \ A) \
+ P 0 \ (\x. P x \ P (Suc x)) \ P n"
+ -- {* Example 11: needs a hint. *}
+by(metis nat.induct)
+
+lemma
+ "(\A. (0, 0) \ A \ (\x y. (x, y) \ A \ (Suc x, Suc y) \ A) \ (n, m) \ A)
+ \ P n \ P m"
+ -- {* Example 12. *}
+ by auto
+
+lemma
+ "(\x. (\u. x = 2 * u) = (\ (\v. Suc x = 2 * v))) \
+ (\A. \x. (x \ A) = (Suc x \ A))"
+ -- {* Example EO1: typo in article, and with the obvious fix it seems
+ to require arithmetic reasoning. *}
+ apply clarify
+ apply (rule_tac x = "{x. \u. x = 2 * u}" in exI, auto)
+ apply metis+
+ done
+
+end