author | berghofe |
Fri, 11 Jul 2003 14:55:17 +0200 | |
changeset 14102 | 8af7334af4b3 |
parent 13339 | 0f89104dd377 |
child 14120 | 3a73850c6c7d |
permissions | -rw-r--r-- |
11399 | 1 |
(* Title: ZF/ex/misc.ML |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1993 University of Cambridge |
|
5 |
||
6 |
Miscellaneous examples for Zermelo-Fraenkel Set Theory |
|
7 |
Composition of homomorphisms, Pastre's examples, ... |
|
8 |
*) |
|
9 |
||
10 |
theory misc = Main: |
|
11 |
||
12 |
||
13 |
||
14 |
(*These two are cited in Benzmueller and Kohlhase's system description of LEO, |
|
15 |
CADE-15, 1998 (page 139-143) as theorems LEO could not prove.*) |
|
16 |
lemma "(X = Y Un Z) <-> (Y \<subseteq> X & Z \<subseteq> X & (\<forall>V. Y \<subseteq> V & Z \<subseteq> V --> X \<subseteq> V))" |
|
17 |
by (blast intro!: equalityI) |
|
18 |
||
19 |
(*the dual of the previous one*) |
|
20 |
lemma "(X = Y Int Z) <-> (X \<subseteq> Y & X \<subseteq> Z & (\<forall>V. V \<subseteq> Y & V \<subseteq> Z --> V \<subseteq> X))" |
|
21 |
by (blast intro!: equalityI) |
|
22 |
||
23 |
(*trivial example of term synthesis: apparently hard for some provers!*) |
|
24 |
lemma "a \<noteq> b ==> a:?X & b \<notin> ?X" |
|
25 |
by blast |
|
26 |
||
27 |
(*Nice Blast_tac benchmark. Proved in 0.3s; old tactics can't manage it!*) |
|
28 |
lemma "\<forall>x \<in> S. \<forall>y \<in> S. x \<subseteq> y ==> \<exists>z. S \<subseteq> {z}" |
|
29 |
by blast |
|
30 |
||
31 |
(*variant of the benchmark above*) |
|
32 |
lemma "\<forall>x \<in> S. Union(S) \<subseteq> x ==> \<exists>z. S \<subseteq> {z}" |
|
33 |
by blast |
|
34 |
||
35 |
(*Example 12 (credited to Peter Andrews) from |
|
36 |
W. Bledsoe. A Maximal Method for Set Variables in Automatic Theorem-proving. |
|
37 |
In: J. Hayes and D. Michie and L. Mikulich, eds. Machine Intelligence 9. |
|
38 |
Ellis Horwood, 53-100 (1979). *) |
|
39 |
lemma "(\<forall>F. {x} \<in> F --> {y} \<in> F) --> (\<forall>A. x \<in> A --> y \<in> A)" |
|
40 |
by best |
|
41 |
||
42 |
||
43 |
(*** Composition of homomorphisms is a homomorphism ***) |
|
44 |
||
45 |
(*Given as a challenge problem in |
|
46 |
R. Boyer et al., |
|
47 |
Set Theory in First-Order Logic: Clauses for G\"odel's Axioms, |
|
48 |
JAR 2 (1986), 287-327 |
|
49 |
*) |
|
50 |
||
51 |
(*collecting the relevant lemmas*) |
|
52 |
declare comp_fun [simp] SigmaI [simp] apply_funtype [simp] |
|
53 |
||
54 |
(*Force helps prove conditions of rewrites such as comp_fun_apply, since |
|
55 |
rewriting does not instantiate Vars.*) |
|
56 |
lemma "(\<forall>A f B g. hom(A,f,B,g) = |
|
57 |
{H \<in> A->B. f \<in> A*A->A & g \<in> B*B->B & |
|
58 |
(\<forall>x \<in> A. \<forall>y \<in> A. H`(f`<x,y>) = g`<H`x,H`y>)}) --> |
|
59 |
J \<in> hom(A,f,B,g) & K \<in> hom(B,g,C,h) --> |
|
60 |
(K O J) \<in> hom(A,f,C,h)" |
|
61 |
by force |
|
62 |
||
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
11399
diff
changeset
|
63 |
(*Another version, with meta-level rewriting*) |
11399 | 64 |
lemma "(!! A f B g. hom(A,f,B,g) == |
65 |
{H \<in> A->B. f \<in> A*A->A & g \<in> B*B->B & |
|
66 |
(\<forall>x \<in> A. \<forall>y \<in> A. H`(f`<x,y>) = g`<H`x,H`y>)}) |
|
67 |
==> J \<in> hom(A,f,B,g) & K \<in> hom(B,g,C,h) --> (K O J) \<in> hom(A,f,C,h)" |
|
68 |
by force |
|
69 |
||
70 |
||
71 |
||
72 |
(** A characterization of functions suggested by Tobias Nipkow **) |
|
73 |
||
74 |
lemma "r \<in> domain(r)->B <-> r \<subseteq> domain(r)*B & (\<forall>X. r `` (r -`` X) \<subseteq> X)" |
|
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
11399
diff
changeset
|
75 |
by (unfold Pi_def function_def, best) |
11399 | 76 |
|
77 |
(**** From D Pastre. Automatic theorem proving in set theory. |
|
78 |
Artificial Intelligence, 10:1--27, 1978. |
|
79 |
||
80 |
Previously, these were done using ML code, but blast manages fine. |
|
81 |
****) |
|
82 |
||
83 |
lemmas compIs [intro] = comp_surj comp_inj comp_fun [intro] |
|
84 |
lemmas compDs [dest] = comp_mem_injD1 comp_mem_surjD1 |
|
85 |
comp_mem_injD2 comp_mem_surjD2 |
|
86 |
||
87 |
lemma pastre1: |
|
88 |
"[| (h O g O f) \<in> inj(A,A); |
|
89 |
(f O h O g) \<in> surj(B,B); |
|
90 |
(g O f O h) \<in> surj(C,C); |
|
91 |
f \<in> A->B; g \<in> B->C; h \<in> C->A |] ==> h \<in> bij(C,A)"; |
|
92 |
by (unfold bij_def, blast) |
|
93 |
||
94 |
lemma pastre3: |
|
95 |
"[| (h O g O f) \<in> surj(A,A); |
|
96 |
(f O h O g) \<in> surj(B,B); |
|
97 |
(g O f O h) \<in> inj(C,C); |
|
98 |
f \<in> A->B; g \<in> B->C; h \<in> C->A |] ==> h \<in> bij(C,A)" |
|
99 |
by (unfold bij_def, blast) |
|
100 |
||
101 |
lemma pastre4: |
|
102 |
"[| (h O g O f) \<in> surj(A,A); |
|
103 |
(f O h O g) \<in> inj(B,B); |
|
104 |
(g O f O h) \<in> inj(C,C); |
|
105 |
f \<in> A->B; g \<in> B->C; h \<in> C->A |] ==> h \<in> bij(C,A)" |
|
106 |
by (unfold bij_def, blast) |
|
107 |
||
108 |
lemma pastre5: |
|
109 |
"[| (h O g O f) \<in> inj(A,A); |
|
110 |
(f O h O g) \<in> surj(B,B); |
|
111 |
(g O f O h) \<in> inj(C,C); |
|
112 |
f \<in> A->B; g \<in> B->C; h \<in> C->A |] ==> h \<in> bij(C,A)" |
|
113 |
by (unfold bij_def, blast) |
|
114 |
||
115 |
lemma pastre6: |
|
116 |
"[| (h O g O f) \<in> inj(A,A); |
|
117 |
(f O h O g) \<in> inj(B,B); |
|
118 |
(g O f O h) \<in> surj(C,C); |
|
119 |
f \<in> A->B; g \<in> B->C; h \<in> C->A |] ==> h \<in> bij(C,A)" |
|
120 |
by (unfold bij_def, blast) |
|
121 |
||
122 |
||
123 |
(** Yet another example... **) |
|
124 |
||
125 |
lemma Pow_sum_bij: |
|
126 |
"(\<lambda>Z \<in> Pow(A+B). <{x \<in> A. Inl(x) \<in> Z}, {y \<in> B. Inr(y) \<in> Z}>) |
|
127 |
\<in> bij(Pow(A+B), Pow(A)*Pow(B))" |
|
128 |
apply (rule_tac d = "%<X,Y>. {Inl (x). x \<in> X} Un {Inr (y). y \<in> Y}" |
|
129 |
in lam_bijective) |
|
130 |
apply force+ |
|
131 |
done |
|
132 |
||
133 |
(*As a special case, we have bij(Pow(A*B), A -> Pow B) *) |
|
134 |
lemma Pow_Sigma_bij: |
|
135 |
"(\<lambda>r \<in> Pow(Sigma(A,B)). \<lambda>x \<in> A. r``{x}) |
|
136 |
\<in> bij(Pow(Sigma(A,B)), \<Pi>x \<in> A. Pow(B(x)))" |
|
137 |
apply (rule_tac d = "%f. \<Union>x \<in> A. \<Union>y \<in> f`x. {<x,y>}" in lam_bijective) |
|
138 |
apply (blast intro: lam_type) |
|
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
11399
diff
changeset
|
139 |
apply (blast dest: apply_type, simp_all) |
11399 | 140 |
apply fast (*strange, but blast can't do it*) |
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
11399
diff
changeset
|
141 |
apply (rule fun_extension, auto) |
11399 | 142 |
by blast |
143 |
||
144 |
end |
|
145 |