author | paulson |
Wed, 02 Apr 1997 15:26:52 +0200 | |
changeset 2871 | ba585d52ea4e |
parent 2493 | bdeb5024353a |
child 3735 | bed0ba7bff2f |
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 |
||
9 |
(* ############################################################ *) |
|
10 |
(* Lemmas *) |
|
11 |
(* ############################################################ *) |
|
12 |
||
13 |
goal Map.thy "!!A. a:A ==> Sigma(A,B)``{a} = B(a)"; |
|
2493 | 14 |
by (Fast_tac 1); |
915 | 15 |
qed "qbeta"; |
16 |
||
17 |
goal Map.thy "!!A. a~:A ==> Sigma(A,B)``{a} = 0"; |
|
2493 | 18 |
by (Fast_tac 1); |
915 | 19 |
qed "qbeta_emp"; |
20 |
||
21 |
goal Map.thy "!!A.a ~: A ==> Sigma(A,B)``{a}=0"; |
|
2493 | 22 |
by (Fast_tac 1); |
915 | 23 |
qed "image_Sigma1"; |
24 |
||
25 |
goal Map.thy "0``A = 0"; |
|
2493 | 26 |
by (Fast_tac 1); |
915 | 27 |
qed "image_02"; |
28 |
||
29 |
(* ############################################################ *) |
|
30 |
(* Inclusion in Quine Universes *) |
|
31 |
(* ############################################################ *) |
|
32 |
||
33 |
(* Lemmas *) |
|
34 |
||
35 |
goalw Map.thy [quniv_def] |
|
36 |
"!!A. A <= univ(X) ==> Pow(A * Union(quniv(X))) <= quniv(X)"; |
|
37 |
by (rtac Pow_mono 1); |
|
38 |
by (rtac ([Sigma_mono, product_univ] MRS subset_trans) 1); |
|
39 |
by (etac subset_trans 1); |
|
40 |
by (rtac (arg_subset_eclose RS univ_mono) 1); |
|
2469 | 41 |
by (simp_tac (!simpset addsimps [Union_Pow_eq]) 1); |
915 | 42 |
qed "MapQU_lemma"; |
43 |
||
44 |
(* Theorems *) |
|
45 |
||
46 |
val prems = goalw Map.thy [PMap_def,TMap_def] |
|
47 |
"[| m:PMap(A,quniv(B)); !!x.x:A ==> x:univ(B) |] ==> m:quniv(B)"; |
|
48 |
by (cut_facts_tac prems 1); |
|
49 |
by (rtac (MapQU_lemma RS subsetD) 1); |
|
50 |
by (rtac subsetI 1); |
|
51 |
by (eresolve_tac prems 1); |
|
2469 | 52 |
by (Fast_tac 1); |
915 | 53 |
qed "mapQU"; |
54 |
||
55 |
(* ############################################################ *) |
|
56 |
(* Monotonicity *) |
|
57 |
(* ############################################################ *) |
|
58 |
||
59 |
goalw Map.thy [PMap_def,TMap_def] "!!A.B<=C ==> PMap(A,B)<=PMap(A,C)"; |
|
2469 | 60 |
by (Fast_tac 1); |
915 | 61 |
qed "map_mono"; |
62 |
||
63 |
(* Rename to pmap_mono *) |
|
64 |
||
65 |
(* ############################################################ *) |
|
66 |
(* Introduction Rules *) |
|
67 |
(* ############################################################ *) |
|
68 |
||
69 |
(** map_emp **) |
|
70 |
||
71 |
goalw Map.thy [map_emp_def,PMap_def,TMap_def] "map_emp:PMap(A,B)"; |
|
2469 | 72 |
by (safe_tac (!claset)); |
915 | 73 |
by (rtac image_02 1); |
74 |
qed "pmap_empI"; |
|
75 |
||
76 |
(** map_owr **) |
|
77 |
||
1020
76d72126a9e7
Modified proofs for new hyp_subst_tac, and simplified them.
lcp
parents:
915
diff
changeset
|
78 |
|
915 | 79 |
goalw Map.thy [map_owr_def,PMap_def,TMap_def] |
80 |
"!! A.[| m:PMap(A,B); a:A; b:B |] ==> map_owr(m,a,b):PMap(A,B)"; |
|
2469 | 81 |
by (Step_tac 1); |
82 |
by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [if_iff]))); |
|
83 |
by (Fast_tac 1); |
|
84 |
by (Fast_tac 1); |
|
85 |
by (Deepen_tac 2 1); |
|
86 |
(*Remaining subgoal*) |
|
915 | 87 |
by (rtac (excluded_middle RS disjE) 1); |
88 |
by (etac image_Sigma1 1); |
|
1075
848bf2e18dff
Modified proofs for new claset primitives. The problem is that they enforce
lcp
parents:
1020
diff
changeset
|
89 |
by (dres_inst_tac [("psi", "?uu ~: B")] asm_rl 1); |
848bf2e18dff
Modified proofs for new claset primitives. The problem is that they enforce
lcp
parents:
1020
diff
changeset
|
90 |
by (asm_full_simp_tac |
2469 | 91 |
(!simpset addsimps [qbeta] setloop split_tac [expand_if]) 1); |
92 |
by (safe_tac (!claset)); |
|
1075
848bf2e18dff
Modified proofs for new claset primitives. The problem is that they enforce
lcp
parents:
1020
diff
changeset
|
93 |
by (dres_inst_tac [("psi", "?uu ~: B")] asm_rl 3); |
2469 | 94 |
by (ALLGOALS Asm_full_simp_tac); |
95 |
by (Fast_tac 1); |
|
915 | 96 |
qed "pmap_owrI"; |
97 |
||
98 |
(** map_app **) |
|
99 |
||
100 |
goalw Map.thy [TMap_def,map_app_def] |
|
101 |
"!!m.[| m:TMap(A,B); a:domain(m) |] ==> map_app(m,a) ~=0"; |
|
102 |
by (etac domainE 1); |
|
103 |
by (dtac imageI 1); |
|
2469 | 104 |
by (Fast_tac 1); |
915 | 105 |
by (etac not_emptyI 1); |
106 |
qed "tmap_app_notempty"; |
|
107 |
||
108 |
goalw Map.thy [TMap_def,map_app_def,domain_def] |
|
109 |
"!!m.[| m:TMap(A,B); a:domain(m) |] ==> map_app(m,a):B"; |
|
2493 | 110 |
by (Fast_tac 1); |
915 | 111 |
qed "tmap_appI"; |
112 |
||
113 |
goalw Map.thy [PMap_def] |
|
114 |
"!!m.[| m:PMap(A,B); a:domain(m) |] ==> map_app(m,a):B"; |
|
115 |
by (forward_tac [tmap_app_notempty] 1); |
|
116 |
by (assume_tac 1); |
|
117 |
by (dtac tmap_appI 1); |
|
118 |
by (assume_tac 1); |
|
2469 | 119 |
by (Fast_tac 1); |
915 | 120 |
qed "pmap_appI"; |
121 |
||
122 |
(** domain **) |
|
123 |
||
124 |
goalw Map.thy [TMap_def] |
|
125 |
"!!m.[| m:TMap(A,B); a:domain(m) |] ==> a:A"; |
|
2493 | 126 |
by (Fast_tac 1); |
915 | 127 |
qed "tmap_domainD"; |
128 |
||
129 |
goalw Map.thy [PMap_def,TMap_def] |
|
130 |
"!!m.[| m:PMap(A,B); a:domain(m) |] ==> a:A"; |
|
2493 | 131 |
by (Fast_tac 1); |
915 | 132 |
qed "pmap_domainD"; |
133 |
||
134 |
(* ############################################################ *) |
|
135 |
(* Equalitites *) |
|
136 |
(* ############################################################ *) |
|
137 |
||
138 |
(** Domain **) |
|
139 |
||
140 |
(* Lemmas *) |
|
141 |
||
142 |
goal Map.thy "domain(UN x:A.B(x)) = (UN x:A.domain(B(x)))"; |
|
2493 | 143 |
by (Fast_tac 1); |
915 | 144 |
qed "domain_UN"; |
145 |
||
146 |
goal Map.thy "domain(Sigma(A,B)) = {x:A.EX y.y:B(x)}"; |
|
2469 | 147 |
by (simp_tac (!simpset addsimps [domain_UN,domain_0,domain_cons]) 1); |
2493 | 148 |
by (Fast_tac 1); |
915 | 149 |
qed "domain_Sigma"; |
150 |
||
151 |
(* Theorems *) |
|
152 |
||
153 |
goalw Map.thy [map_emp_def] "domain(map_emp) = 0"; |
|
2493 | 154 |
by (Fast_tac 1); |
915 | 155 |
qed "map_domain_emp"; |
156 |
||
157 |
goalw Map.thy [map_owr_def] |
|
158 |
"!!a.b ~= 0 ==> domain(map_owr(f,a,b)) = {a} Un domain(f)"; |
|
2469 | 159 |
by (simp_tac (!simpset addsimps [domain_Sigma]) 1); |
915 | 160 |
by (rtac equalityI 1); |
2493 | 161 |
by (Fast_tac 1); |
915 | 162 |
by (rtac subsetI 1); |
163 |
by (rtac CollectI 1); |
|
164 |
by (assume_tac 1); |
|
165 |
by (etac UnE' 1); |
|
166 |
by (etac singletonE 1); |
|
2469 | 167 |
by (Asm_simp_tac 1); |
2493 | 168 |
by (Fast_tac 1); |
169 |
by (fast_tac (!claset addss (!simpset)) 1); |
|
915 | 170 |
qed "map_domain_owr"; |
171 |
||
172 |
(** Application **) |
|
173 |
||
174 |
goalw Map.thy [map_app_def,map_owr_def] |
|
175 |
"map_app(map_owr(f,a,b),a) = b"; |
|
2034 | 176 |
by (stac qbeta 1); |
2469 | 177 |
by (Fast_tac 1); |
178 |
by (Simp_tac 1); |
|
915 | 179 |
qed "map_app_owr1"; |
180 |
||
181 |
goalw Map.thy [map_app_def,map_owr_def] |
|
182 |
"!!a.c ~= a ==> map_app(map_owr(f,a,b),c)= map_app(f,c)"; |
|
183 |
by (rtac (excluded_middle RS disjE) 1); |
|
2034 | 184 |
by (stac qbeta_emp 1); |
915 | 185 |
by (assume_tac 1); |
2493 | 186 |
by (Fast_tac 1); |
915 | 187 |
by (etac (qbeta RS ssubst) 1); |
2469 | 188 |
by (Asm_simp_tac 1); |
915 | 189 |
qed "map_app_owr2"; |
190 |
||
191 |
||
192 |
||
193 |
||
194 |
||
195 |
||
196 |
||
197 |
||
198 |
||
199 |
||
200 |
||
201 |
||
202 |
||
203 |
||
204 |
||
205 |
||
206 |
||
207 |
||
208 |
||
209 |
||
210 |
||
211 |
||
212 |
||
213 |
||
214 |
||
215 |
||
216 |
||
217 |
||
218 |
||
219 |
||
220 |
||
221 |
||
222 |
||
223 |
||
224 |
||
225 |
||
226 |
||
227 |
||
228 |
||
229 |
||
230 |