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 paulson@13058: paulson@13058: Set Theory examples: Cantor's Theorem, Schroeder-Berstein Theorem, etc. paulson@13058: *) wenzelm@9100: wenzelm@9100: theory set = Main: wenzelm@9100: paulson@13058: text{*These two are cited in Benzmueller and Kohlhase's system description paulson@13058: of LEO, CADE-15, 1998 (pages 139-143) as theorems LEO could not prove.*} paulson@13058: paulson@13058: lemma "(X = Y Un Z) = (Y<=X & Z<=X & (ALL V. Y<=V & Z<=V --> X<=V))" paulson@13058: by blast paulson@13058: paulson@13058: lemma "(X = Y Int Z) = (X<=Y & X<=Z & (ALL V. V<=Y & V<=Z --> V<=X))" paulson@13058: by blast paulson@13058: paulson@13058: text{*trivial example of term synthesis: apparently hard for some provers!*} paulson@13058: lemma "a ~= b ==> a:?X & b ~: ?X" paulson@13058: by blast paulson@13058: paulson@13058: (** Examples for the Blast_tac paper **) paulson@13058: paulson@13058: text{*Union-image, called Un_Union_image on equalities.ML*} paulson@13058: lemma "(UN x:C. f(x) Un g(x)) = Union(f`C) Un Union(g`C)" paulson@13058: by blast paulson@13058: paulson@13058: text{*Inter-image, called Int_Inter_image on equalities.ML*} paulson@13058: lemma "(INT x:C. f(x) Int g(x)) = Inter(f`C) Int Inter(g`C)" paulson@13058: by blast paulson@13058: paulson@13058: text{*Singleton I. Nice demonstration of blast_tac--and its limitations. paulson@13058: For some unfathomable reason, UNIV_I increases the search space greatly*} paulson@13058: lemma "!!S::'a set set. ALL x:S. ALL y:S. x<=y ==> EX z. S <= {z}" paulson@13058: by (blast del: UNIV_I) paulson@13058: paulson@13058: text{*Singleton II. variant of the benchmark above*} paulson@13058: lemma "ALL x:S. Union(S) <= x ==> EX z. S <= {z}" paulson@13058: by (blast del: UNIV_I) paulson@13058: paulson@13058: text{* A unique fixpoint theorem --- fast/best/meson all fail *} paulson@13058: paulson@13058: lemma "EX! x. f(g(x))=x ==> EX! y. g(f(y))=y" paulson@13058: apply (erule ex1E, rule ex1I, erule arg_cong) paulson@13058: apply (rule subst, assumption, erule allE, rule arg_cong, erule mp) paulson@13058: apply (erule arg_cong) paulson@13058: done paulson@13058: paulson@13058: paulson@13058: paulson@13058: text{* Cantor's Theorem: There is no surjection from a set to its powerset. *} paulson@13058: paulson@13058: text{*requires best-first search because it is undirectional*} paulson@13058: lemma cantor1: "~ (EX f:: 'a=>'a set. ALL S. EX x. f(x) = S)" paulson@13058: by best paulson@13058: paulson@13058: text{*This form displays the diagonal term*} paulson@13058: lemma "ALL f:: 'a=>'a set. ALL x. f(x) ~= ?S(f)" paulson@13058: by best paulson@13058: paulson@13058: text{*This form exploits the set constructs*} paulson@13058: lemma "?S ~: range(f :: 'a=>'a set)" paulson@13058: by (rule notI, erule rangeE, best) paulson@13058: paulson@13058: text{*Or just this!*} paulson@13058: lemma "?S ~: range(f :: 'a=>'a set)" paulson@13058: by best paulson@13058: paulson@13058: text{* The Schroeder-Berstein Theorem *} paulson@13058: paulson@13058: lemma disj_lemma: "[| -(f`X) = g`(-X); f(a)=g(b); a:X |] ==> b:X" paulson@13058: by blast paulson@13058: paulson@13058: lemma surj_if_then_else: paulson@13058: "-(f`X) = g`(-X) ==> surj(%z. if z:X then f(z) else g(z))" paulson@13058: by (simp add: surj_def, blast) paulson@13058: paulson@13058: lemma bij_if_then_else: paulson@13058: "[| inj_on f X; inj_on g (-X); -(f`X) = g`(-X); paulson@13058: h = (%z. if z:X then f(z) else g(z)) |] paulson@13058: ==> inj(h) & surj(h)" paulson@13058: apply (unfold inj_on_def) paulson@13058: apply (simp add: surj_if_then_else) paulson@13058: apply (blast dest: disj_lemma sym) paulson@13058: done paulson@13058: paulson@13058: lemma decomposition: "EX X. X = - (g`(- (f`X)))" paulson@13058: apply (rule exI) paulson@13058: apply (rule lfp_unfold) paulson@13058: apply (rule monoI, blast) paulson@13058: done paulson@13058: paulson@13058: text{*Schroeder-Bernstein Theorem*} paulson@13058: lemma "[| inj (f:: 'a=>'b); inj (g:: 'b=>'a) |] paulson@13058: ==> EX h:: 'a=>'b. inj(h) & surj(h)" paulson@13058: apply (rule decomposition [THEN exE]) paulson@13058: apply (rule exI) paulson@13058: apply (rule bij_if_then_else) paulson@13058: apply (rule_tac [4] refl) paulson@13058: apply (rule_tac [2] inj_on_inv) paulson@13058: apply (erule subset_inj_on [OF subset_UNIV]) paulson@13058: txt{*tricky variable instantiations!*} paulson@13058: apply (erule ssubst, subst double_complement) paulson@13058: apply (rule subsetI, erule imageE, erule ssubst, rule rangeI) paulson@13058: apply (erule ssubst, subst double_complement, erule inv_image_comp [symmetric]) paulson@13058: done paulson@13058: paulson@13058: paulson@13058: text{*Set variable instantiation examples from paulson@13058: W. W. Bledsoe and Guohui Feng, SET-VAR. paulson@13058: JAR 11 (3), 1993, pages 293-314. paulson@13058: paulson@13058: Isabelle can prove the easy examples without any special mechanisms, but it paulson@13058: can't prove the hard ones. paulson@13058: *} paulson@13058: paulson@13058: text{*Example 1, page 295.*} paulson@13058: lemma "(EX A. (ALL x:A. x <= (0::int)))" paulson@13058: by force paulson@13058: paulson@13058: text{*Example 2*} paulson@13058: lemma "D : F --> (EX G. (ALL A:G. EX B:F. A <= B))"; paulson@13058: by force paulson@13058: paulson@13058: text{*Example 3*} paulson@13058: lemma "P(a) --> (EX A. (ALL x:A. P(x)) & (EX y. y:A))"; paulson@13058: by force paulson@13058: paulson@13058: text{*Example 4*} paulson@13058: lemma "a (EX A. a~:A & b:A & c~: A)" paulson@13058: by force paulson@13058: paulson@13058: text{*Example 5, page 298.*} paulson@13058: lemma "P(f(b)) --> (EX s A. (ALL x:A. P(x)) & f(s):A)"; paulson@13058: by force paulson@13058: paulson@13058: text{*Example 6*} paulson@13058: lemma "P(f(b)) --> (EX s A. (ALL x:A. P(x)) & f(s):A)"; paulson@13058: by force paulson@13058: paulson@13058: text{*Example 7*} paulson@13058: lemma "EX A. a ~: A" paulson@13058: by force paulson@13058: paulson@13058: text{*Example 8*} paulson@13058: lemma "(ALL u v. u < (0::int) --> u ~= abs v) --> (EX A::int set. (ALL y. abs y ~: A) & -2 : A)" paulson@13058: by force text{*not blast, which can't simplify -2<0*} paulson@13058: paulson@13058: text{*Example 9 omitted (requires the reals)*} paulson@13058: paulson@13058: text{*The paper has no Example 10!*} paulson@13058: paulson@13058: text{*Example 11: needs a hint*} paulson@13058: lemma "(ALL A. 0:A & (ALL x:A. Suc(x):A) --> n:A) & paulson@13058: P(0) & (ALL x. P(x) --> P(Suc(x))) --> P(n)" paulson@13058: apply clarify paulson@13058: apply (drule_tac x="{x. P x}" in spec) paulson@13058: by force paulson@13058: paulson@13058: text{*Example 12*} paulson@13058: lemma "(ALL A. (0,0):A & (ALL x y. (x,y):A --> (Suc(x),Suc(y)):A) --> (n,m):A) paulson@13058: & P(n) --> P(m)" paulson@13058: by auto paulson@13058: paulson@13058: text{*Example EO1: typo in article, and with the obvious fix it seems paulson@13058: to require arithmetic reasoning.*} paulson@13058: lemma "(ALL x. (EX u. x=2*u) = (~(EX v. Suc x = 2*v))) --> paulson@13058: (EX A. ALL x. (x : A) = (Suc x ~: A))" paulson@13058: apply clarify paulson@13058: apply (rule_tac x="{x. EX u. x = 2*u}" in exI, auto) paulson@13058: apply (case_tac v, auto) paulson@13058: apply (drule_tac x="Suc v" and P="%x. ?a(x) ~= ?b(x)" in spec, force) paulson@13058: done paulson@13058: wenzelm@9100: end