paulson@13058: (* Title: HOL/ex/set.thy paulson@13058: ID: $Id$ paulson@13058: Author: Tobias Nipkow and Lawrence C Paulson paulson@13058: Copyright 1991 University of Cambridge wenzelm@13107: *) paulson@13058: ballarin@19982: header {* Set Theory examples: Cantor's Theorem, Schröder-Bernstein Theorem, etc. *} wenzelm@9100: haftmann@16417: theory set imports Main begin wenzelm@9100: wenzelm@13107: text{* wenzelm@13107: These two are cited in Benzmueller and Kohlhase's system description wenzelm@13107: of LEO, CADE-15, 1998 (pages 139-143) as theorems LEO could not wenzelm@13107: prove. wenzelm@13107: *} paulson@13058: wenzelm@13107: lemma "(X = Y \ Z) = wenzelm@13107: (Y \ X \ Z \ X \ (\V. Y \ V \ Z \ V \ X \ V))" wenzelm@13107: by blast paulson@13058: wenzelm@13107: lemma "(X = Y \ Z) = wenzelm@13107: (X \ Y \ X \ Z \ (\V. V \ Y \ V \ Z \ V \ X))" wenzelm@13107: by blast paulson@13058: wenzelm@13107: text {* wenzelm@13107: Trivial example of term synthesis: apparently hard for some provers! wenzelm@13107: *} paulson@13058: wenzelm@13107: lemma "a \ b \ a \ ?X \ b \ ?X" wenzelm@13107: by blast wenzelm@13107: wenzelm@13107: wenzelm@13107: subsection {* Examples for the @{text blast} paper *} paulson@13058: wenzelm@13107: lemma "(\x \ C. f x \ g x) = \(f ` C) \ \(g ` C)" wenzelm@13107: -- {* Union-image, called @{text Un_Union_image} in Main HOL *} wenzelm@13107: by blast paulson@13058: wenzelm@13107: lemma "(\x \ C. f x \ g x) = \(f ` C) \ \(g ` C)" wenzelm@13107: -- {* Inter-image, called @{text Int_Inter_image} in Main HOL *} wenzelm@13107: by blast paulson@13058: paulson@16898: lemma singleton_example_1: paulson@16898: "\S::'a set set. \x \ S. \y \ S. x \ y \ \z. S \ {z}" paulson@18391: by blast paulson@16898: paulson@16898: lemma singleton_example_2: paulson@16898: "\x \ S. \S \ x \ \z. S \ {z}" paulson@16898: -- {*Variant of the problem above. *} paulson@18391: by blast wenzelm@13107: wenzelm@13107: lemma "\!x. f (g x) = x \ \!y. g (f y) = y" wenzelm@13107: -- {* A unique fixpoint theorem --- @{text fast}/@{text best}/@{text meson} all fail. *} paulson@24573: by metis paulson@13058: paulson@13058: wenzelm@13107: subsection {* Cantor's Theorem: There is no surjection from a set to its powerset *} paulson@13058: wenzelm@13107: lemma cantor1: "\ (\f:: 'a \ 'a set. \S. \x. f x = S)" wenzelm@13107: -- {* Requires best-first search because it is undirectional. *} wenzelm@13107: by best paulson@13058: wenzelm@13107: lemma "\f:: 'a \ 'a set. \x. f x \ ?S f" wenzelm@13107: -- {*This form displays the diagonal term. *} wenzelm@13107: by best paulson@13058: wenzelm@13107: lemma "?S \ range (f :: 'a \ 'a set)" wenzelm@13107: -- {* This form exploits the set constructs. *} wenzelm@13107: by (rule notI, erule rangeE, best) paulson@13058: wenzelm@13107: lemma "?S \ range (f :: 'a \ 'a set)" wenzelm@13107: -- {* Or just this! *} wenzelm@13107: by best wenzelm@13107: paulson@13058: wenzelm@13107: subsection {* The Schröder-Berstein Theorem *} paulson@13058: wenzelm@13107: lemma disj_lemma: "- (f ` X) = g ` (-X) \ f a = g b \ a \ X \ b \ X" wenzelm@13107: by blast paulson@13058: paulson@13058: lemma surj_if_then_else: wenzelm@13107: "-(f ` X) = g ` (-X) \ surj (\z. if z \ X then f z else g z)" wenzelm@13107: by (simp add: surj_def) blast paulson@13058: wenzelm@13107: lemma bij_if_then_else: wenzelm@13107: "inj_on f X \ inj_on g (-X) \ -(f ` X) = g ` (-X) \ wenzelm@13107: h = (\z. if z \ X then f z else g z) \ inj h \ surj h" wenzelm@13107: apply (unfold inj_on_def) wenzelm@13107: apply (simp add: surj_if_then_else) wenzelm@13107: apply (blast dest: disj_lemma sym) wenzelm@13107: done paulson@13058: wenzelm@13107: lemma decomposition: "\X. X = - (g ` (- (f ` X)))" wenzelm@13107: apply (rule exI) wenzelm@13107: apply (rule lfp_unfold) wenzelm@13107: apply (rule monoI, blast) wenzelm@13107: done paulson@13058: wenzelm@13107: theorem Schroeder_Bernstein: wenzelm@13107: "inj (f :: 'a \ 'b) \ inj (g :: 'b \ 'a) wenzelm@13107: \ \h:: 'a \ 'b. inj h \ surj h" paulson@15488: apply (rule decomposition [where f=f and g=g, THEN exE]) paulson@15488: apply (rule_tac x = "(\z. if z \ x then f z else inv g z)" in exI) paulson@15488: --{*The term above can be synthesized by a sufficiently detailed proof.*} wenzelm@13107: apply (rule bij_if_then_else) wenzelm@13107: apply (rule_tac [4] refl) wenzelm@13107: apply (rule_tac [2] inj_on_inv) nipkow@15306: apply (erule subset_inj_on [OF _ subset_UNIV]) paulson@15488: apply blast paulson@15488: apply (erule ssubst, subst double_complement, erule inv_image_comp [symmetric]) wenzelm@13107: done paulson@13058: paulson@13058: wenzelm@13107: text {* wenzelm@13107: From W. W. Bledsoe and Guohui Feng, SET-VAR. JAR 11 (3), 1993, pages wenzelm@13107: 293-314. wenzelm@13107: wenzelm@13107: Isabelle can prove the easy examples without any special mechanisms, wenzelm@13107: but it can't prove the hard ones. paulson@13058: *} paulson@13058: wenzelm@13107: lemma "\A. (\x \ A. x \ (0::int))" wenzelm@13107: -- {* Example 1, page 295. *} wenzelm@13107: by force paulson@13058: wenzelm@13107: lemma "D \ F \ \G. \A \ G. \B \ F. A \ B" wenzelm@13107: -- {* Example 2. *} wenzelm@13107: by force paulson@13058: wenzelm@13107: lemma "P a \ \A. (\x \ A. P x) \ (\y. y \ A)" wenzelm@13107: -- {* Example 3. *} wenzelm@13107: by force paulson@13058: wenzelm@13107: lemma "a < b \ b < (c::int) \ \A. a \ A \ b \ A \ c \ A" wenzelm@13107: -- {* Example 4. *} wenzelm@13107: by force paulson@13058: wenzelm@13107: lemma "P (f b) \ \s A. (\x \ A. P x) \ f s \ A" wenzelm@13107: -- {*Example 5, page 298. *} wenzelm@13107: by force paulson@13058: wenzelm@13107: lemma "P (f b) \ \s A. (\x \ A. P x) \ f s \ A" wenzelm@13107: -- {* Example 6. *} wenzelm@13107: by force paulson@13058: wenzelm@13107: lemma "\A. a \ A" wenzelm@13107: -- {* Example 7. *} wenzelm@13107: by force paulson@13058: wenzelm@13107: lemma "(\u v. u < (0::int) \ u \ abs v) wenzelm@13107: \ (\A::int set. (\y. abs y \ A) \ -2 \ A)" paulson@14353: -- {* Example 8 now needs a small hint. *} paulson@14353: by (simp add: abs_if, force) paulson@14353: -- {* not @{text blast}, which can't simplify @{text "-2 < 0"} *} paulson@13058: wenzelm@13107: text {* Example 9 omitted (requires the reals). *} paulson@13058: wenzelm@13107: text {* The paper has no Example 10! *} paulson@13058: wenzelm@13107: lemma "(\A. 0 \ A \ (\x \ A. Suc x \ A) \ n \ A) \ wenzelm@13107: P 0 \ (\x. P x \ P (Suc x)) \ P n" wenzelm@13107: -- {* Example 11: needs a hint. *} wenzelm@13107: apply clarify wenzelm@13107: apply (drule_tac x = "{x. P x}" in spec) wenzelm@13107: apply force wenzelm@13107: done paulson@13058: wenzelm@13107: lemma wenzelm@13107: "(\A. (0, 0) \ A \ (\x y. (x, y) \ A \ (Suc x, Suc y) \ A) \ (n, m) \ A) wenzelm@13107: \ P n \ P m" wenzelm@13107: -- {* Example 12. *} wenzelm@13107: by auto paulson@13058: wenzelm@13107: lemma wenzelm@13107: "(\x. (\u. x = 2 * u) = (\ (\v. Suc x = 2 * v))) \ wenzelm@13107: (\A. \x. (x \ A) = (Suc x \ A))" wenzelm@13107: -- {* Example EO1: typo in article, and with the obvious fix it seems wenzelm@13107: to require arithmetic reasoning. *} wenzelm@13107: apply clarify wenzelm@13107: apply (rule_tac x = "{x. \u. x = 2 * u}" in exI, auto) wenzelm@13107: apply (case_tac v, auto) wenzelm@13107: apply (drule_tac x = "Suc v" and P = "\x. ?a x \ ?b x" in spec, force) wenzelm@13107: done paulson@13058: wenzelm@9100: end