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