author | paulson |
Fri, 14 Aug 1998 18:37:28 +0200 | |
changeset 5321 | f8848433d240 |
parent 5265 | 9d1d4c43c76d |
child 6046 | 2c8a8be36c94 |
permissions | -rw-r--r-- |
1461 | 1 |
(* Title: ZF/Coind/Map.ML |
915 | 2 |
ID: $Id$ |
1461 | 3 |
Author: Jacob Frost, Cambridge University Computer Laboratory |
915 | 4 |
Copyright 1995 University of Cambridge |
5 |
*) |
|
6 |
||
7 |
open Map; |
|
8 |
||
4841
d275fd349f3d
new thms, really demos of the final coalgebra theorem
paulson
parents:
4152
diff
changeset
|
9 |
(** Some sample proofs of inclusions for the final coalgebra "U" (by lcp) **) |
d275fd349f3d
new thms, really demos of the final coalgebra theorem
paulson
parents:
4152
diff
changeset
|
10 |
|
5265
9d1d4c43c76d
Disjointness reasoning by AddEs [equals0E, sym RS equals0E]
paulson
parents:
5147
diff
changeset
|
11 |
Goalw [TMap_def] "{0,1} <= {1} Un TMap(I, {0,1})"; |
4841
d275fd349f3d
new thms, really demos of the final coalgebra theorem
paulson
parents:
4152
diff
changeset
|
12 |
by (Blast_tac 1); |
d275fd349f3d
new thms, really demos of the final coalgebra theorem
paulson
parents:
4152
diff
changeset
|
13 |
result(); |
d275fd349f3d
new thms, really demos of the final coalgebra theorem
paulson
parents:
4152
diff
changeset
|
14 |
|
5265
9d1d4c43c76d
Disjointness reasoning by AddEs [equals0E, sym RS equals0E]
paulson
parents:
5147
diff
changeset
|
15 |
Goalw [TMap_def] "{0} Un TMap(I,1) <= {1} Un TMap(I, {0} Un TMap(I,1))"; |
4841
d275fd349f3d
new thms, really demos of the final coalgebra theorem
paulson
parents:
4152
diff
changeset
|
16 |
by (Blast_tac 1); |
d275fd349f3d
new thms, really demos of the final coalgebra theorem
paulson
parents:
4152
diff
changeset
|
17 |
result(); |
d275fd349f3d
new thms, really demos of the final coalgebra theorem
paulson
parents:
4152
diff
changeset
|
18 |
|
5265
9d1d4c43c76d
Disjointness reasoning by AddEs [equals0E, sym RS equals0E]
paulson
parents:
5147
diff
changeset
|
19 |
Goalw [TMap_def] "{0,1} Un TMap(I,2) <= {1} Un TMap(I, {0,1} Un TMap(I,2))"; |
4841
d275fd349f3d
new thms, really demos of the final coalgebra theorem
paulson
parents:
4152
diff
changeset
|
20 |
by (Blast_tac 1); |
d275fd349f3d
new thms, really demos of the final coalgebra theorem
paulson
parents:
4152
diff
changeset
|
21 |
result(); |
d275fd349f3d
new thms, really demos of the final coalgebra theorem
paulson
parents:
4152
diff
changeset
|
22 |
|
5265
9d1d4c43c76d
Disjointness reasoning by AddEs [equals0E, sym RS equals0E]
paulson
parents:
5147
diff
changeset
|
23 |
(*TOO SLOW |
5068 | 24 |
Goalw [TMap_def] |
4841
d275fd349f3d
new thms, really demos of the final coalgebra theorem
paulson
parents:
4152
diff
changeset
|
25 |
"{0,1} Un TMap(I,TMap(I,2)) Un TMap(I,2) <= \ |
d275fd349f3d
new thms, really demos of the final coalgebra theorem
paulson
parents:
4152
diff
changeset
|
26 |
\ {1} Un TMap(I, {0,1} Un TMap(I,TMap(I,2)) Un TMap(I,2))"; |
5265
9d1d4c43c76d
Disjointness reasoning by AddEs [equals0E, sym RS equals0E]
paulson
parents:
5147
diff
changeset
|
27 |
by (Blast_tac 1); |
4841
d275fd349f3d
new thms, really demos of the final coalgebra theorem
paulson
parents:
4152
diff
changeset
|
28 |
result(); |
5265
9d1d4c43c76d
Disjointness reasoning by AddEs [equals0E, sym RS equals0E]
paulson
parents:
5147
diff
changeset
|
29 |
*) |
4841
d275fd349f3d
new thms, really demos of the final coalgebra theorem
paulson
parents:
4152
diff
changeset
|
30 |
|
d275fd349f3d
new thms, really demos of the final coalgebra theorem
paulson
parents:
4152
diff
changeset
|
31 |
|
915 | 32 |
(* ############################################################ *) |
33 |
(* Lemmas *) |
|
34 |
(* ############################################################ *) |
|
35 |
||
5137 | 36 |
Goal "a:A ==> Sigma(A,B)``{a} = B(a)"; |
2493 | 37 |
by (Fast_tac 1); |
915 | 38 |
qed "qbeta"; |
39 |
||
5137 | 40 |
Goal "a~:A ==> Sigma(A,B)``{a} = 0"; |
2493 | 41 |
by (Fast_tac 1); |
915 | 42 |
qed "qbeta_emp"; |
43 |
||
5137 | 44 |
Goal "a ~: A ==> Sigma(A,B)``{a}=0"; |
2493 | 45 |
by (Fast_tac 1); |
915 | 46 |
qed "image_Sigma1"; |
47 |
||
48 |
||
49 |
(* ############################################################ *) |
|
50 |
(* Inclusion in Quine Universes *) |
|
51 |
(* ############################################################ *) |
|
52 |
||
53 |
(* Lemmas *) |
|
54 |
||
5068 | 55 |
Goalw [quniv_def] |
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset
|
56 |
"A <= univ(X) ==> Pow(A * Union(quniv(X))) <= quniv(X)"; |
915 | 57 |
by (rtac Pow_mono 1); |
58 |
by (rtac ([Sigma_mono, product_univ] MRS subset_trans) 1); |
|
59 |
by (etac subset_trans 1); |
|
60 |
by (rtac (arg_subset_eclose RS univ_mono) 1); |
|
4091 | 61 |
by (simp_tac (simpset() addsimps [Union_Pow_eq]) 1); |
915 | 62 |
qed "MapQU_lemma"; |
63 |
||
64 |
(* Theorems *) |
|
65 |
||
66 |
val prems = goalw Map.thy [PMap_def,TMap_def] |
|
3840 | 67 |
"[| m:PMap(A,quniv(B)); !!x. x:A ==> x:univ(B) |] ==> m:quniv(B)"; |
915 | 68 |
by (cut_facts_tac prems 1); |
69 |
by (rtac (MapQU_lemma RS subsetD) 1); |
|
70 |
by (rtac subsetI 1); |
|
71 |
by (eresolve_tac prems 1); |
|
2469 | 72 |
by (Fast_tac 1); |
915 | 73 |
qed "mapQU"; |
74 |
||
75 |
(* ############################################################ *) |
|
76 |
(* Monotonicity *) |
|
77 |
(* ############################################################ *) |
|
78 |
||
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5137
diff
changeset
|
79 |
Goalw [PMap_def,TMap_def] "B<=C ==> PMap(A,B)<=PMap(A,C)"; |
2469 | 80 |
by (Fast_tac 1); |
915 | 81 |
qed "map_mono"; |
82 |
||
83 |
(* Rename to pmap_mono *) |
|
84 |
||
85 |
(* ############################################################ *) |
|
86 |
(* Introduction Rules *) |
|
87 |
(* ############################################################ *) |
|
88 |
||
89 |
(** map_emp **) |
|
90 |
||
5068 | 91 |
Goalw [map_emp_def,PMap_def,TMap_def] "map_emp:PMap(A,B)"; |
5265
9d1d4c43c76d
Disjointness reasoning by AddEs [equals0E, sym RS equals0E]
paulson
parents:
5147
diff
changeset
|
92 |
by Auto_tac; |
915 | 93 |
qed "pmap_empI"; |
94 |
||
95 |
(** map_owr **) |
|
96 |
||
1020
76d72126a9e7
Modified proofs for new hyp_subst_tac, and simplified them.
lcp
parents:
915
diff
changeset
|
97 |
|
5068 | 98 |
Goalw [map_owr_def,PMap_def,TMap_def] |
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset
|
99 |
"[| m:PMap(A,B); a:A; b:B |] ==> map_owr(m,a,b):PMap(A,B)"; |
3735 | 100 |
by Safe_tac; |
4091 | 101 |
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [if_iff]))); |
2469 | 102 |
by (Fast_tac 1); |
103 |
by (Fast_tac 1); |
|
104 |
by (Deepen_tac 2 1); |
|
105 |
(*Remaining subgoal*) |
|
915 | 106 |
by (rtac (excluded_middle RS disjE) 1); |
107 |
by (etac image_Sigma1 1); |
|
1075
848bf2e18dff
Modified proofs for new claset primitives. The problem is that they enforce
lcp
parents:
1020
diff
changeset
|
108 |
by (dres_inst_tac [("psi", "?uu ~: B")] asm_rl 1); |
5137 | 109 |
by (asm_full_simp_tac (simpset() addsimps [qbeta]) 1); |
4152 | 110 |
by Safe_tac; |
1075
848bf2e18dff
Modified proofs for new claset primitives. The problem is that they enforce
lcp
parents:
1020
diff
changeset
|
111 |
by (dres_inst_tac [("psi", "?uu ~: B")] asm_rl 3); |
2469 | 112 |
by (ALLGOALS Asm_full_simp_tac); |
113 |
by (Fast_tac 1); |
|
915 | 114 |
qed "pmap_owrI"; |
115 |
||
116 |
(** map_app **) |
|
117 |
||
5068 | 118 |
Goalw [TMap_def,map_app_def] |
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset
|
119 |
"[| m:TMap(A,B); a:domain(m) |] ==> map_app(m,a) ~=0"; |
915 | 120 |
by (etac domainE 1); |
121 |
by (dtac imageI 1); |
|
2469 | 122 |
by (Fast_tac 1); |
915 | 123 |
by (etac not_emptyI 1); |
124 |
qed "tmap_app_notempty"; |
|
125 |
||
5068 | 126 |
Goalw [TMap_def,map_app_def,domain_def] |
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset
|
127 |
"[| m:TMap(A,B); a:domain(m) |] ==> map_app(m,a):B"; |
2493 | 128 |
by (Fast_tac 1); |
915 | 129 |
qed "tmap_appI"; |
130 |
||
5068 | 131 |
Goalw [PMap_def] |
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset
|
132 |
"[| m:PMap(A,B); a:domain(m) |] ==> map_app(m,a):B"; |
915 | 133 |
by (forward_tac [tmap_app_notempty] 1); |
134 |
by (assume_tac 1); |
|
135 |
by (dtac tmap_appI 1); |
|
136 |
by (assume_tac 1); |
|
2469 | 137 |
by (Fast_tac 1); |
915 | 138 |
qed "pmap_appI"; |
139 |
||
140 |
(** domain **) |
|
141 |
||
5068 | 142 |
Goalw [TMap_def] |
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset
|
143 |
"[| m:TMap(A,B); a:domain(m) |] ==> a:A"; |
2493 | 144 |
by (Fast_tac 1); |
915 | 145 |
qed "tmap_domainD"; |
146 |
||
5068 | 147 |
Goalw [PMap_def,TMap_def] |
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset
|
148 |
"[| m:PMap(A,B); a:domain(m) |] ==> a:A"; |
2493 | 149 |
by (Fast_tac 1); |
915 | 150 |
qed "pmap_domainD"; |
151 |
||
152 |
(* ############################################################ *) |
|
4841
d275fd349f3d
new thms, really demos of the final coalgebra theorem
paulson
parents:
4152
diff
changeset
|
153 |
(* Equalities *) |
915 | 154 |
(* ############################################################ *) |
155 |
||
156 |
(** Domain **) |
|
157 |
||
158 |
(* Lemmas *) |
|
159 |
||
5068 | 160 |
Goal "domain(UN x:A. B(x)) = (UN x:A. domain(B(x)))"; |
2493 | 161 |
by (Fast_tac 1); |
915 | 162 |
qed "domain_UN"; |
163 |
||
5068 | 164 |
Goal "domain(Sigma(A,B)) = {x:A. EX y. y:B(x)}"; |
4091 | 165 |
by (simp_tac (simpset() addsimps [domain_UN,domain_0,domain_cons]) 1); |
2493 | 166 |
by (Fast_tac 1); |
915 | 167 |
qed "domain_Sigma"; |
168 |
||
169 |
(* Theorems *) |
|
170 |
||
5068 | 171 |
Goalw [map_emp_def] "domain(map_emp) = 0"; |
2493 | 172 |
by (Fast_tac 1); |
915 | 173 |
qed "map_domain_emp"; |
174 |
||
5068 | 175 |
Goalw [map_owr_def] |
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset
|
176 |
"b ~= 0 ==> domain(map_owr(f,a,b)) = {a} Un domain(f)"; |
4091 | 177 |
by (simp_tac (simpset() addsimps [domain_Sigma]) 1); |
915 | 178 |
by (rtac equalityI 1); |
2493 | 179 |
by (Fast_tac 1); |
915 | 180 |
by (rtac subsetI 1); |
181 |
by (rtac CollectI 1); |
|
182 |
by (assume_tac 1); |
|
183 |
by (etac UnE' 1); |
|
184 |
by (etac singletonE 1); |
|
2469 | 185 |
by (Asm_simp_tac 1); |
2493 | 186 |
by (Fast_tac 1); |
4091 | 187 |
by (fast_tac (claset() addss (simpset())) 1); |
915 | 188 |
qed "map_domain_owr"; |
189 |
||
190 |
(** Application **) |
|
191 |
||
5068 | 192 |
Goalw [map_app_def,map_owr_def] |
915 | 193 |
"map_app(map_owr(f,a,b),a) = b"; |
2034 | 194 |
by (stac qbeta 1); |
2469 | 195 |
by (Fast_tac 1); |
196 |
by (Simp_tac 1); |
|
915 | 197 |
qed "map_app_owr1"; |
198 |
||
5068 | 199 |
Goalw [map_app_def,map_owr_def] |
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset
|
200 |
"c ~= a ==> map_app(map_owr(f,a,b),c)= map_app(f,c)"; |
915 | 201 |
by (rtac (excluded_middle RS disjE) 1); |
2034 | 202 |
by (stac qbeta_emp 1); |
915 | 203 |
by (assume_tac 1); |
2493 | 204 |
by (Fast_tac 1); |
915 | 205 |
by (etac (qbeta RS ssubst) 1); |
2469 | 206 |
by (Asm_simp_tac 1); |
915 | 207 |
qed "map_app_owr2"; |
208 |
||
209 |
||
210 |
||
211 |
||
212 |
||
213 |
||
214 |
||
215 |
||
216 |
||
217 |
||
218 |
||
219 |
||
220 |
||
221 |
||
222 |
||
223 |
||
224 |
||
225 |
||
226 |
||
227 |
||
228 |
||
229 |
||
230 |
||
231 |
||
232 |
||
233 |
||
234 |
||
235 |
||
236 |
||
237 |
||
238 |
||
239 |
||
240 |
||
241 |
||
242 |
||
243 |
||
244 |
||
245 |
||
246 |
||
247 |
||
248 |