4 Copyright 1991 University of Cambridge |
4 Copyright 1991 University of Cambridge |
5 |
5 |
6 Cantor's Theorem; the Schroeder-Berstein Theorem. |
6 Cantor's Theorem; the Schroeder-Berstein Theorem. |
7 *) |
7 *) |
8 |
8 |
9 |
9 (*These two are cited in Benzmueller and Kohlhase's system description of LEO, |
10 writeln"File HOL/ex/set."; |
|
11 |
|
12 context Lfp.thy; |
|
13 |
|
14 (*These two are cited in Benzmueller and Kohlhash's system description of LEO, |
|
15 CADE-15, 1998 (page 139-143) as theorems LEO could not prove.*) |
10 CADE-15, 1998 (page 139-143) as theorems LEO could not prove.*) |
16 |
11 |
17 Goal "(X = Y Un Z) = (Y<=X & Z<=X & (ALL V. Y<=V & Z<=V --> X<=V))"; |
12 Goal "(X = Y Un Z) = (Y<=X & Z<=X & (ALL V. Y<=V & Z<=V --> X<=V))"; |
18 by (Blast_tac 1); |
13 by (Blast_tac 1); |
19 result(); |
14 qed ""; |
20 |
15 |
21 Goal "(X = Y Int Z) = (X<=Y & X<=Z & (ALL V. V<=Y & V<=Z --> V<=X))"; |
16 Goal "(X = Y Int Z) = (X<=Y & X<=Z & (ALL V. V<=Y & V<=Z --> V<=X))"; |
22 by (Blast_tac 1); |
17 by (Blast_tac 1); |
23 result(); |
18 qed ""; |
24 |
19 |
25 (*trivial example of term synthesis: apparently hard for some provers!*) |
20 (*trivial example of term synthesis: apparently hard for some provers!*) |
26 Goal "a ~= b ==> a:?X & b ~: ?X"; |
21 Goal "a ~= b ==> a:?X & b ~: ?X"; |
27 by (Blast_tac 1); |
22 by (Blast_tac 1); |
28 result(); |
23 qed ""; |
29 |
24 |
30 (** Examples for the Blast_tac paper **) |
25 (** Examples for the Blast_tac paper **) |
31 |
26 |
32 (*Union-image, called Un_Union_image on equalities.ML*) |
27 (*Union-image, called Un_Union_image on equalities.ML*) |
33 Goal "(UN x:C. f(x) Un g(x)) = Union(f``C) Un Union(g``C)"; |
28 Goal "(UN x:C. f(x) Un g(x)) = Union(f``C) Un Union(g``C)"; |
34 by (Blast_tac 1); |
29 by (Blast_tac 1); |
35 result(); |
30 qed ""; |
36 |
31 |
37 (*Inter-image, called Int_Inter_image on equalities.ML*) |
32 (*Inter-image, called Int_Inter_image on equalities.ML*) |
38 Goal "(INT x:C. f(x) Int g(x)) = Inter(f``C) Int Inter(g``C)"; |
33 Goal "(INT x:C. f(x) Int g(x)) = Inter(f``C) Int Inter(g``C)"; |
39 by (Blast_tac 1); |
34 by (Blast_tac 1); |
40 result(); |
35 qed ""; |
41 |
36 |
42 (*Singleton I. Nice demonstration of blast_tac--and its limitations*) |
37 (*Singleton I. Nice demonstration of blast_tac--and its limitations*) |
43 Goal "!!S::'a set set. ALL x:S. ALL y:S. x<=y ==> EX z. S <= {z}"; |
38 Goal "!!S::'a set set. ALL x:S. ALL y:S. x<=y ==> EX z. S <= {z}"; |
44 (*for some unfathomable reason, UNIV_I increases the search space greatly*) |
39 (*for some unfathomable reason, UNIV_I increases the search space greatly*) |
45 by (blast_tac (claset() delrules [UNIV_I]) 1); |
40 by (blast_tac (claset() delrules [UNIV_I]) 1); |
46 result(); |
41 qed ""; |
47 |
42 |
48 (*Singleton II. variant of the benchmark above*) |
43 (*Singleton II. variant of the benchmark above*) |
49 Goal "ALL x:S. Union(S) <= x ==> EX z. S <= {z}"; |
44 Goal "ALL x:S. Union(S) <= x ==> EX z. S <= {z}"; |
50 by (blast_tac (claset() delrules [UNIV_I]) 1); |
45 by (blast_tac (claset() delrules [UNIV_I]) 1); |
51 (*just Blast_tac takes 5 seconds instead of 1*) |
46 (*just Blast_tac takes 5 seconds instead of 1*) |
52 result(); |
47 qed ""; |
53 |
48 |
54 (*** A unique fixpoint theorem --- fast/best/meson all fail ***) |
49 (*** A unique fixpoint theorem --- fast/best/meson all fail ***) |
55 |
50 |
56 Goal "?!x. f(g(x))=x ==> ?!y. g(f(y))=y"; |
51 Goal "?!x. f(g(x))=x ==> ?!y. g(f(y))=y"; |
57 by (EVERY1[etac ex1E, rtac ex1I, etac arg_cong, |
52 by (EVERY1[etac ex1E, rtac ex1I, etac arg_cong, |
58 rtac subst, atac, etac allE, rtac arg_cong, etac mp, etac arg_cong]); |
53 rtac subst, atac, etac allE, rtac arg_cong, etac mp, etac arg_cong]); |
59 result(); |
54 qed ""; |
|
55 |
60 |
56 |
61 (*** Cantor's Theorem: There is no surjection from a set to its powerset. ***) |
57 (*** Cantor's Theorem: There is no surjection from a set to its powerset. ***) |
62 |
58 |
63 goal Set.thy "~ (? f:: 'a=>'a set. ! S. ? x. f(x) = S)"; |
59 Goal "~ (? f:: 'a=>'a set. ! S. ? x. f(x) = S)"; |
64 (*requires best-first search because it is undirectional*) |
60 (*requires best-first search because it is undirectional*) |
65 by (best_tac (claset() addSEs [equalityCE]) 1); |
61 by (best_tac (claset() addSEs [equalityCE]) 1); |
66 qed "cantor1"; |
62 qed "cantor1"; |
67 |
63 |
68 (*This form displays the diagonal term*) |
64 (*This form displays the diagonal term*) |
69 goal Set.thy "! f:: 'a=>'a set. ! x. f(x) ~= ?S(f)"; |
65 Goal "! f:: 'a=>'a set. ! x. f(x) ~= ?S(f)"; |
70 by (best_tac (claset() addSEs [equalityCE]) 1); |
66 by (best_tac (claset() addSEs [equalityCE]) 1); |
71 uresult(); |
67 uresult(); |
72 |
68 |
73 (*This form exploits the set constructs*) |
69 (*This form exploits the set constructs*) |
74 goal Set.thy "?S ~: range(f :: 'a=>'a set)"; |
70 Goal "?S ~: range(f :: 'a=>'a set)"; |
75 by (rtac notI 1); |
71 by (rtac notI 1); |
76 by (etac rangeE 1); |
72 by (etac rangeE 1); |
77 by (etac equalityCE 1); |
73 by (etac equalityCE 1); |
78 by (dtac CollectD 1); |
74 by (dtac CollectD 1); |
79 by (contr_tac 1); |
75 by (contr_tac 1); |
80 by (swap_res_tac [CollectI] 1); |
76 by (swap_res_tac [CollectI] 1); |
81 by (assume_tac 1); |
77 by (assume_tac 1); |
82 |
78 |
83 choplev 0; |
79 choplev 0; |
84 by (best_tac (claset() addSEs [equalityCE]) 1); |
80 by (best_tac (claset() addSEs [equalityCE]) 1); |
|
81 qed ""; |
85 |
82 |
86 |
83 |
87 (*** The Schroder-Berstein Theorem ***) |
84 (*** The Schroder-Berstein Theorem ***) |
88 |
85 |
89 Goal "[| -(f``X) = g``(-X); f(a)=g(b); a:X |] ==> b:X"; |
86 Goal "[| -(f``X) = g``(-X); f(a)=g(b); a:X |] ==> b:X"; |