src/HOL/ex/set.ML
 changeset 13058 ad6106d7b4bb parent 13057 805de10ca485 child 13059 d78d2089e163
```     1.1 --- a/src/HOL/ex/set.ML	Thu Mar 14 16:00:29 2002 +0100
1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,123 +0,0 @@
1.4 -(*  Title:      HOL/ex/set.ML
1.5 -    ID:         \$Id\$
1.6 -    Author:     Tobias Nipkow, Cambridge University Computer Laboratory
1.7 -    Copyright   1991  University of Cambridge
1.8 -
1.9 -Cantor's Theorem; the Schroeder-Berstein Theorem.
1.10 -*)
1.11 -
1.12 -(*These two are cited in Benzmueller and Kohlhase's system description of LEO,
1.13 -  CADE-15, 1998 (page 139-143) as theorems LEO could not prove.*)
1.14 -
1.15 -Goal "(X = Y Un Z) = (Y<=X & Z<=X & (ALL V. Y<=V & Z<=V --> X<=V))";
1.16 -by (Blast_tac 1);
1.17 -qed "";
1.18 -
1.19 -Goal "(X = Y Int Z) = (X<=Y & X<=Z & (ALL V. V<=Y & V<=Z --> V<=X))";
1.20 -by (Blast_tac 1);
1.21 -qed "";
1.22 -
1.23 -(*trivial example of term synthesis: apparently hard for some provers!*)
1.24 -Goal "a ~= b ==> a:?X & b ~: ?X";
1.25 -by (Blast_tac 1);
1.26 -qed "";
1.27 -
1.28 -(** Examples for the Blast_tac paper **)
1.29 -
1.30 -(*Union-image, called Un_Union_image on equalities.ML*)
1.31 -Goal "(UN x:C. f(x) Un g(x)) = Union(f`C)  Un  Union(g`C)";
1.32 -by (Blast_tac 1);
1.33 -qed "";
1.34 -
1.35 -(*Inter-image, called Int_Inter_image on equalities.ML*)
1.36 -Goal "(INT x:C. f(x) Int g(x)) = Inter(f`C) Int Inter(g`C)";
1.37 -by (Blast_tac 1);
1.38 -qed "";
1.39 -
1.40 -(*Singleton I.  Nice demonstration of blast_tac--and its limitations*)
1.41 -Goal "!!S::'a set set. ALL x:S. ALL y:S. x<=y ==> EX z. S <= {z}";
1.42 -(*for some unfathomable reason, UNIV_I increases the search space greatly*)
1.43 -by (blast_tac (claset() delrules [UNIV_I]) 1);
1.44 -qed "";
1.45 -
1.46 -(*Singleton II.  variant of the benchmark above*)
1.47 -Goal "ALL x:S. Union(S) <= x ==> EX z. S <= {z}";
1.48 -by (blast_tac (claset() delrules [UNIV_I]) 1);
1.49 -(*just Blast_tac takes 5 seconds instead of 1*)
1.50 -qed "";
1.51 -
1.52 -(*** A unique fixpoint theorem --- fast/best/meson all fail ***)
1.53 -
1.54 -Goal "EX! x. f(g(x))=x ==> EX! y. g(f(y))=y";
1.55 -by (EVERY1[etac ex1E, rtac ex1I, etac arg_cong,
1.56 -          rtac subst, atac, etac allE, rtac arg_cong, etac mp, etac arg_cong]);
1.57 -qed "";
1.58 -
1.59 -
1.60 -(*** Cantor's Theorem: There is no surjection from a set to its powerset. ***)
1.61 -
1.62 -Goal "~ (EX f:: 'a=>'a set. ALL S. EX x. f(x) = S)";
1.63 -(*requires best-first search because it is undirectional*)
1.64 -by (Best_tac 1);
1.65 -qed "cantor1";
1.66 -
1.67 -(*This form displays the diagonal term*)
1.68 -Goal "ALL f:: 'a=>'a set. ALL x. f(x) ~= ?S(f)";
1.69 -by (Best_tac 1);
1.70 -uresult();
1.71 -
1.72 -(*This form exploits the set constructs*)
1.73 -Goal "?S ~: range(f :: 'a=>'a set)";
1.74 -by (rtac notI 1);
1.75 -by (etac rangeE 1);
1.76 -by (etac equalityCE 1);
1.77 -by (dtac CollectD 1);
1.78 -by (contr_tac 1);
1.79 -by (swap_res_tac [CollectI] 1);
1.80 -by (assume_tac 1);
1.81 -
1.82 -choplev 0;
1.83 -by (Best_tac 1);
1.84 -qed "";
1.85 -
1.86 -
1.87 -(*** The Schroeder-Berstein Theorem ***)
1.88 -
1.89 -Goal "[| -(f`X) = g`(-X);  f(a)=g(b);  a:X |] ==> b:X";
1.90 -by (Blast_tac 1);
1.91 -qed "disj_lemma";
1.92 -
1.93 -Goal "-(f`X) = g`(-X) ==> surj(%z. if z:X then f(z) else g(z))";
1.94 -by (asm_simp_tac (simpset() addsimps [surj_def]) 1);
1.95 -by (Blast_tac 1);
1.96 -qed "surj_if_then_else";
1.97 -
1.98 -Goalw [inj_on_def]
1.99 -     "[| inj_on f X;  inj_on g (-X);  -(f`X) = g`(-X); \
1.100 -\        h = (%z. if z:X then f(z) else g(z)) |]       \
1.101 -\     ==> inj(h) & surj(h)";
1.102 -by (asm_simp_tac (simpset() addsimps [surj_if_then_else]) 1);
1.103 -by (blast_tac (claset() addDs [disj_lemma, sym]) 1);
1.104 -qed "bij_if_then_else";
1.105 -
1.106 -Goal "EX X. X = - (g`(- (f`X)))";
1.107 -by (rtac exI 1);
1.108 -by (rtac lfp_unfold 1);
1.109 -by (REPEAT (ares_tac [monoI, image_mono, Compl_anti_mono] 1));
1.110 -qed "decomposition";
1.111 -
1.112 -val [injf,injg] = goal (the_context ())
1.113 -   "[| inj (f:: 'a=>'b);  inj (g:: 'b=>'a) |] \
1.114 -\   ==> EX h:: 'a=>'b. inj(h) & surj(h)";
1.115 -by (rtac (decomposition RS exE) 1);
1.116 -by (rtac exI 1);
1.117 -by (rtac bij_if_then_else 1);
1.118 -by (rtac refl 4);
1.119 -by (rtac inj_on_inv 2);
1.120 -by (rtac ([subset_UNIV, injf] MRS subset_inj_on) 1);
1.121 -  (**tricky variable instantiations!**)
1.122 -by (EVERY1 [etac ssubst, stac double_complement, rtac subsetI,
1.123 -            etac imageE, etac ssubst, rtac rangeI]);
1.124 -by (EVERY1 [etac ssubst, stac double_complement,
1.125 -            rtac (injg RS inv_image_comp RS sym)]);
1.126 -qed "schroeder_bernstein";
```