author | nipkow |
Fri, 17 Jan 1997 18:32:24 +0100 | |
changeset 2523 | 0ccea141409b |
parent 2513 | d708d8cdc8e8 |
child 2525 | 477c05586286 |
permissions | -rw-r--r-- |
1300 | 1 |
open Type; |
2 |
||
3 |
Addsimps [mgu_eq,mgu_mg,mgu_free]; |
|
4 |
||
5 |
(* mgu does not introduce new type variables *) |
|
6 |
goalw thy [new_tv_def] |
|
7 |
"!! n. [|mgu t1 t2 = Ok u; new_tv n t1; new_tv n t2|] ==> \ |
|
8 |
\ new_tv n u"; |
|
2513
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
2031
diff
changeset
|
9 |
by (fast_tac (set_cs addDs [mgu_free]) 1); |
1300 | 10 |
qed "mgu_new"; |
11 |
||
12 |
(* application of id_subst does not change type expression *) |
|
13 |
goalw thy [id_subst_def] |
|
1400 | 14 |
"$ id_subst = (%t::typ.t)"; |
1300 | 15 |
by (rtac ext 1); |
1400 | 16 |
by (typ.induct_tac "t" 1); |
1300 | 17 |
by (ALLGOALS Asm_simp_tac); |
18 |
qed "app_subst_id_te"; |
|
19 |
Addsimps [app_subst_id_te]; |
|
20 |
||
21 |
(* application of id_subst does not change list of type expressions *) |
|
22 |
goalw thy [app_subst_list] |
|
1400 | 23 |
"$ id_subst = (%ts::typ list.ts)"; |
1300 | 24 |
by (rtac ext 1); |
1400 | 25 |
by (list.induct_tac "ts" 1); |
1300 | 26 |
by (ALLGOALS Asm_simp_tac); |
27 |
qed "app_subst_id_tel"; |
|
28 |
Addsimps [app_subst_id_tel]; |
|
29 |
||
1751 | 30 |
goalw Type.thy [id_subst_def,o_def] "$s o id_subst = s"; |
2031 | 31 |
by (rtac ext 1); |
32 |
by (Simp_tac 1); |
|
1751 | 33 |
qed "o_id_subst"; |
34 |
Addsimps[o_id_subst]; |
|
35 |
||
1300 | 36 |
goalw thy [dom_def,id_subst_def,empty_def] |
37 |
"dom id_subst = {}"; |
|
38 |
by (Simp_tac 1); |
|
39 |
qed "dom_id_subst"; |
|
40 |
Addsimps [dom_id_subst]; |
|
41 |
||
42 |
goalw thy [cod_def] |
|
43 |
"cod id_subst = {}"; |
|
44 |
by (Simp_tac 1); |
|
45 |
qed "cod_id_subst"; |
|
46 |
Addsimps [cod_id_subst]; |
|
47 |
||
48 |
goalw thy [free_tv_subst] |
|
49 |
"free_tv id_subst = {}"; |
|
50 |
by (Simp_tac 1); |
|
51 |
qed "free_tv_id_subst"; |
|
52 |
Addsimps [free_tv_id_subst]; |
|
53 |
||
54 |
goalw thy [dom_def,cod_def,UNION_def,Bex_def] |
|
55 |
"!!v. [| v : free_tv(s n); v~=n |] ==> v : cod s"; |
|
56 |
by (Simp_tac 1); |
|
57 |
by (safe_tac (empty_cs addSIs [exI,conjI,notI])); |
|
1465 | 58 |
by (assume_tac 2); |
1300 | 59 |
by (rotate_tac 1 1); |
60 |
by (Asm_full_simp_tac 1); |
|
61 |
qed "cod_app_subst"; |
|
62 |
Addsimps [cod_app_subst]; |
|
63 |
||
64 |
||
65 |
(* composition of substitutions *) |
|
66 |
goal thy |
|
1400 | 67 |
"$ g ($ f t::typ) = $ (%x. $ g (f x) ) t"; |
68 |
by (typ.induct_tac "t" 1); |
|
1300 | 69 |
by (ALLGOALS Asm_simp_tac); |
70 |
qed "subst_comp_te"; |
|
71 |
||
72 |
goalw thy [app_subst_list] |
|
1400 | 73 |
"$ g ($ f ts::typ list) = $ (%x. $ g (f x)) ts"; |
74 |
by (list.induct_tac "ts" 1); |
|
1300 | 75 |
(* case [] *) |
76 |
by (Simp_tac 1); |
|
77 |
(* case x#xl *) |
|
78 |
by (asm_full_simp_tac (!simpset addsimps [subst_comp_te]) 1); |
|
79 |
qed "subst_comp_tel"; |
|
80 |
||
81 |
||
82 |
(* constructor laws for app_subst *) |
|
83 |
goalw thy [app_subst_list] |
|
84 |
"$ s [] = []"; |
|
85 |
by (Simp_tac 1); |
|
86 |
qed "app_subst_Nil"; |
|
87 |
||
88 |
goalw thy [app_subst_list] |
|
1400 | 89 |
"$ s (t#ts) = ($ s t)#($ s ts)"; |
1300 | 90 |
by (Simp_tac 1); |
91 |
qed "app_subst_Cons"; |
|
92 |
||
93 |
Addsimps [app_subst_Nil,app_subst_Cons]; |
|
94 |
||
95 |
(* constructor laws for new_tv *) |
|
96 |
goalw thy [new_tv_def] |
|
97 |
"new_tv n (TVar m) = (m<n)"; |
|
98 |
by (fast_tac (HOL_cs addss !simpset) 1); |
|
99 |
qed "new_tv_TVar"; |
|
100 |
||
101 |
goalw thy [new_tv_def] |
|
1400 | 102 |
"new_tv n (t1 -> t2) = (new_tv n t1 & new_tv n t2)"; |
1300 | 103 |
by (fast_tac (HOL_cs addss !simpset) 1); |
104 |
qed "new_tv_Fun"; |
|
105 |
||
106 |
goalw thy [new_tv_def] |
|
107 |
"new_tv n []"; |
|
108 |
by (Simp_tac 1); |
|
109 |
qed "new_tv_Nil"; |
|
110 |
||
111 |
goalw thy [new_tv_def] |
|
1400 | 112 |
"new_tv n (t#ts) = (new_tv n t & new_tv n ts)"; |
1300 | 113 |
by (fast_tac (HOL_cs addss !simpset) 1); |
114 |
qed "new_tv_Cons"; |
|
115 |
||
116 |
Addsimps [new_tv_TVar,new_tv_Fun,new_tv_Nil,new_tv_Cons]; |
|
117 |
||
1751 | 118 |
goalw Type.thy [id_subst_def,new_tv_def,free_tv_subst,dom_def,cod_def] |
119 |
"new_tv n id_subst"; |
|
2031 | 120 |
by (Simp_tac 1); |
1751 | 121 |
qed "new_tv_id_subst"; |
122 |
Addsimps[new_tv_id_subst]; |
|
1300 | 123 |
|
124 |
goalw thy [new_tv_def] |
|
125 |
"new_tv n s = ((!m. n <= m --> (s m = TVar m)) & \ |
|
126 |
\ (! l. l < n --> new_tv n (s l) ))"; |
|
2513
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
2031
diff
changeset
|
127 |
by (safe_tac HOL_cs ); |
1300 | 128 |
(* ==> *) |
2513
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
2031
diff
changeset
|
129 |
by (fast_tac (HOL_cs addDs [leD] addss (!simpset addsimps [free_tv_subst,dom_def])) 1); |
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
2031
diff
changeset
|
130 |
by (subgoal_tac "m:cod s | s l = TVar l" 1); |
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
2031
diff
changeset
|
131 |
by (safe_tac HOL_cs ); |
2031 | 132 |
by (fast_tac (HOL_cs addDs [UnI2] addss (!simpset addsimps [free_tv_subst])) 1); |
133 |
by (dres_inst_tac [("P","%x. m:free_tv x")] subst 1 THEN atac 1); |
|
134 |
by (Asm_full_simp_tac 1); |
|
135 |
by (fast_tac (set_cs addss (!simpset addsimps [free_tv_subst,cod_def,dom_def])) 1); |
|
1300 | 136 |
(* <== *) |
2513
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
2031
diff
changeset
|
137 |
by (rewrite_goals_tac [free_tv_subst,cod_def,dom_def] ); |
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
2031
diff
changeset
|
138 |
by (safe_tac set_cs ); |
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
2031
diff
changeset
|
139 |
by (cut_inst_tac [("m","m"),("n","n")] less_linear 1); |
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
2031
diff
changeset
|
140 |
by (fast_tac (HOL_cs addSIs [less_or_eq_imp_le]) 1); |
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
2031
diff
changeset
|
141 |
by (cut_inst_tac [("m","ma"),("n","n")] less_linear 1); |
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
2031
diff
changeset
|
142 |
by (fast_tac (HOL_cs addSIs [less_or_eq_imp_le]) 1); |
1300 | 143 |
qed "new_tv_subst"; |
144 |
||
145 |
goal thy |
|
146 |
"new_tv n = list_all (new_tv n)"; |
|
1465 | 147 |
by (rtac ext 1); |
2031 | 148 |
by (list.induct_tac "x" 1); |
149 |
by (ALLGOALS Asm_simp_tac); |
|
1300 | 150 |
qed "new_tv_list"; |
151 |
||
152 |
(* substitution affects only variables occurring freely *) |
|
153 |
goal thy |
|
1400 | 154 |
"new_tv n (t::typ) --> $(%x. if x=n then t' else s x) t = $s t"; |
155 |
by (typ.induct_tac "t" 1); |
|
1300 | 156 |
by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if])))); |
157 |
qed "subst_te_new_tv"; |
|
158 |
Addsimps [subst_te_new_tv]; |
|
159 |
||
160 |
goal thy |
|
1400 | 161 |
"new_tv n (ts::typ list) --> $(%x. if x=n then t else s x) ts = $s ts"; |
162 |
by (list.induct_tac "ts" 1); |
|
1300 | 163 |
by (ALLGOALS Asm_full_simp_tac); |
164 |
qed "subst_tel_new_tv"; |
|
165 |
Addsimps [subst_tel_new_tv]; |
|
166 |
||
167 |
(* all greater variables are also new *) |
|
168 |
goal thy |
|
1400 | 169 |
"n<=m --> new_tv n (t::typ) --> new_tv m t"; |
170 |
by (typ.induct_tac "t" 1); |
|
1300 | 171 |
(* case TVar n *) |
2513
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
2031
diff
changeset
|
172 |
by (fast_tac (HOL_cs addIs [less_le_trans] addss !simpset) 1); |
1300 | 173 |
(* case Fun t1 t2 *) |
174 |
by (Asm_simp_tac 1); |
|
1521 | 175 |
qed_spec_mp "new_tv_le"; |
1300 | 176 |
Addsimps [lessI RS less_imp_le RS new_tv_le]; |
177 |
||
178 |
goal thy |
|
1400 | 179 |
"n<=m --> new_tv n (ts::typ list) --> new_tv m ts"; |
2513
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
2031
diff
changeset
|
180 |
by (list.induct_tac "ts" 1); |
1300 | 181 |
(* case [] *) |
2031 | 182 |
by (Simp_tac 1); |
1300 | 183 |
(* case a#al *) |
184 |
by (fast_tac (HOL_cs addIs [new_tv_le] addss !simpset) 1); |
|
1521 | 185 |
qed_spec_mp "new_tv_list_le"; |
1300 | 186 |
Addsimps [lessI RS less_imp_le RS new_tv_list_le]; |
187 |
||
188 |
goal thy |
|
189 |
"!! n. [| n<=m; new_tv n (s::subst) |] ==> new_tv m s"; |
|
190 |
by (asm_full_simp_tac (!simpset addsimps [new_tv_subst]) 1); |
|
191 |
by (rtac conjI 1); |
|
192 |
by (slow_tac (HOL_cs addIs [le_trans]) 1); |
|
193 |
by (safe_tac HOL_cs ); |
|
194 |
by (res_inst_tac [("P","l < n"),("Q","n <= l")] disjE 1); |
|
195 |
by (fast_tac (HOL_cs addss (HOL_ss addsimps [le_def])) 1); |
|
196 |
by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [new_tv_le])) ); |
|
197 |
qed "new_tv_subst_le"; |
|
198 |
Addsimps [lessI RS less_imp_le RS new_tv_subst_le]; |
|
199 |
||
200 |
(* new_tv property remains if a substitution is applied *) |
|
201 |
goal thy |
|
202 |
"!!n. [| n<m; new_tv m (s::subst) |] ==> new_tv m (s n)"; |
|
203 |
by (asm_full_simp_tac (!simpset addsimps [new_tv_subst]) 1); |
|
204 |
qed "new_tv_subst_var"; |
|
205 |
||
206 |
goal thy |
|
1400 | 207 |
"new_tv n s --> new_tv n (t::typ) --> new_tv n ($ s t)"; |
208 |
by (typ.induct_tac "t" 1); |
|
1300 | 209 |
by (ALLGOALS(fast_tac (HOL_cs addss (!simpset addsimps [new_tv_subst])))); |
1521 | 210 |
qed_spec_mp "new_tv_subst_te"; |
1300 | 211 |
Addsimps [new_tv_subst_te]; |
212 |
||
1400 | 213 |
goal thy |
214 |
"new_tv n s --> new_tv n (ts::typ list) --> new_tv n ($ s ts)"; |
|
2513
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
2031
diff
changeset
|
215 |
by (simp_tac (!simpset addsimps [new_tv_list]) 1); |
1400 | 216 |
by (list.induct_tac "ts" 1); |
1300 | 217 |
by (ALLGOALS(fast_tac (HOL_cs addss (!simpset addsimps [new_tv_subst])))); |
1521 | 218 |
qed_spec_mp "new_tv_subst_tel"; |
1300 | 219 |
Addsimps [new_tv_subst_tel]; |
220 |
||
221 |
(* auxilliary lemma *) |
|
222 |
goal thy |
|
1400 | 223 |
"new_tv n ts --> new_tv (Suc n) ((TVar n)#ts)"; |
2513
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
2031
diff
changeset
|
224 |
by (simp_tac (!simpset addsimps [new_tv_list]) 1); |
1400 | 225 |
by (list.induct_tac "ts" 1); |
1300 | 226 |
by (ALLGOALS Asm_full_simp_tac); |
227 |
qed "new_tv_Suc_list"; |
|
228 |
||
229 |
||
230 |
(* composition of substitutions preserves new_tv proposition *) |
|
231 |
goal thy |
|
232 |
"!! n. [| new_tv n (s::subst); new_tv n r |] ==> \ |
|
233 |
\ new_tv n (($ r) o s)"; |
|
234 |
by (asm_full_simp_tac (!simpset addsimps [new_tv_subst]) 1); |
|
235 |
qed "new_tv_subst_comp_1"; |
|
236 |
||
237 |
goal thy |
|
238 |
"!! n. [| new_tv n (s::subst); new_tv n r |] ==> \ |
|
239 |
\ new_tv n (%v.$ r (s v))"; |
|
240 |
by (asm_full_simp_tac (!simpset addsimps [new_tv_subst]) 1); |
|
241 |
qed "new_tv_subst_comp_2"; |
|
242 |
||
243 |
Addsimps [new_tv_subst_comp_1,new_tv_subst_comp_2]; |
|
244 |
||
245 |
(* new type variables do not occur freely in a type structure *) |
|
246 |
goalw thy [new_tv_def] |
|
247 |
"!!n. new_tv n ts ==> n~:(free_tv ts)"; |
|
1619 | 248 |
by (fast_tac (HOL_cs addEs [less_irrefl]) 1); |
1300 | 249 |
qed "new_tv_not_free_tv"; |
250 |
Addsimps [new_tv_not_free_tv]; |
|
251 |
||
252 |
goal thy |
|
1400 | 253 |
"(t::typ) mem ts --> free_tv t <= free_tv ts"; |
254 |
by (list.induct_tac "ts" 1); |
|
1300 | 255 |
(* case [] *) |
256 |
by (Simp_tac 1); |
|
257 |
(* case x#xl *) |
|
258 |
by (fast_tac (set_cs addss (!simpset setloop (split_tac [expand_if]))) 1); |
|
1521 | 259 |
qed_spec_mp "ftv_mem_sub_ftv_list"; |
1300 | 260 |
Addsimps [ftv_mem_sub_ftv_list]; |
261 |
||
262 |
||
263 |
(* if two substitutions yield the same result if applied to a type |
|
264 |
structure the substitutions coincide on the free type variables |
|
265 |
occurring in the type structure *) |
|
266 |
goal thy |
|
1400 | 267 |
"$ s1 (t::typ) = $ s2 t --> n:(free_tv t) --> s1 n = s2 n"; |
268 |
by (typ.induct_tac "t" 1); |
|
1300 | 269 |
(* case TVar n *) |
270 |
by (fast_tac (HOL_cs addss !simpset) 1); |
|
271 |
(* case Fun t1 t2 *) |
|
272 |
by (fast_tac (HOL_cs addss !simpset) 1); |
|
1521 | 273 |
qed_spec_mp "eq_subst_te_eq_free"; |
1300 | 274 |
|
275 |
goal thy |
|
1400 | 276 |
"(!n. n:(free_tv t) --> s1 n = s2 n) --> $ s1 (t::typ) = $ s2 t"; |
277 |
by (typ.induct_tac "t" 1); |
|
1300 | 278 |
(* case TVar n *) |
279 |
by (fast_tac (HOL_cs addss !simpset) 1); |
|
280 |
(* case Fun t1 t2 *) |
|
281 |
by (fast_tac (HOL_cs addss !simpset) 1); |
|
1521 | 282 |
qed_spec_mp "eq_free_eq_subst_te"; |
1300 | 283 |
|
284 |
goal thy |
|
1400 | 285 |
"$s1 (ts::typ list) = $s2 ts --> n:(free_tv ts) --> s1 n = s2 n"; |
286 |
by (list.induct_tac "ts" 1); |
|
1300 | 287 |
(* case [] *) |
288 |
by (fast_tac (HOL_cs addss !simpset) 1); |
|
289 |
(* case x#xl *) |
|
290 |
by (fast_tac (HOL_cs addIs [eq_subst_te_eq_free] addss (!simpset)) 1); |
|
1521 | 291 |
qed_spec_mp "eq_subst_tel_eq_free"; |
1300 | 292 |
|
293 |
goal thy |
|
1400 | 294 |
"(!n. n:(free_tv ts) --> s1 n = s2 n) --> $s1 (ts::typ list) = $s2 ts"; |
295 |
by (list.induct_tac "ts" 1); |
|
1300 | 296 |
(* case [] *) |
297 |
by (fast_tac (HOL_cs addss !simpset) 1); |
|
298 |
(* case x#xl *) |
|
299 |
by (fast_tac (HOL_cs addIs [eq_free_eq_subst_te] addss (!simpset)) 1); |
|
1521 | 300 |
qed_spec_mp "eq_free_eq_subst_tel"; |
1300 | 301 |
|
302 |
(* some useful theorems *) |
|
303 |
goalw thy [free_tv_subst] |
|
304 |
"!!v. v : cod s ==> v : free_tv s"; |
|
2513
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
2031
diff
changeset
|
305 |
by (fast_tac set_cs 1); |
1300 | 306 |
qed "codD"; |
307 |
||
308 |
goalw thy [free_tv_subst,dom_def] |
|
309 |
"!! x. x ~: free_tv s ==> s x = TVar x"; |
|
2513
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
2031
diff
changeset
|
310 |
by (fast_tac set_cs 1); |
1300 | 311 |
qed "not_free_impl_id"; |
312 |
||
313 |
goalw thy [new_tv_def] |
|
314 |
"!! n. [| new_tv n t; m:free_tv t |] ==> m<n"; |
|
2513
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
2031
diff
changeset
|
315 |
by (fast_tac HOL_cs 1 ); |
1300 | 316 |
qed "free_tv_le_new_tv"; |
317 |
||
318 |
goal thy |
|
319 |
"free_tv (s (v::nat)) <= cod s Un {v}"; |
|
2513
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
2031
diff
changeset
|
320 |
by (cut_inst_tac [("P","v:dom s")] excluded_middle 1); |
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
2031
diff
changeset
|
321 |
by (safe_tac (HOL_cs addSIs [subsetI]) ); |
1300 | 322 |
by (fast_tac (set_cs addss (!simpset addsimps [dom_def])) 1); |
323 |
by (fast_tac (set_cs addss (!simpset addsimps [cod_def])) 1); |
|
324 |
qed "free_tv_subst_var"; |
|
325 |
||
326 |
goal thy |
|
1400 | 327 |
"free_tv ($ s (t::typ)) <= cod s Un free_tv t"; |
2513
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
2031
diff
changeset
|
328 |
by (typ.induct_tac "t" 1); |
1300 | 329 |
(* case TVar n *) |
2513
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
2031
diff
changeset
|
330 |
by (simp_tac (!simpset addsimps [free_tv_subst_var]) 1); |
1300 | 331 |
(* case Fun t1 t2 *) |
2513
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
2031
diff
changeset
|
332 |
by (fast_tac (set_cs addss !simpset) 1); |
1300 | 333 |
qed "free_tv_app_subst_te"; |
334 |
||
335 |
goal thy |
|
1400 | 336 |
"free_tv ($ s (ts::typ list)) <= cod s Un free_tv ts"; |
2513
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
2031
diff
changeset
|
337 |
by (list.induct_tac "ts" 1); |
1300 | 338 |
(* case [] *) |
339 |
by (Simp_tac 1); |
|
340 |
(* case a#al *) |
|
2513
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
2031
diff
changeset
|
341 |
by (cut_facts_tac [free_tv_app_subst_te] 1); |
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
2031
diff
changeset
|
342 |
by (fast_tac (set_cs addss !simpset) 1); |
1300 | 343 |
qed "free_tv_app_subst_tel"; |
344 |
||
1521 | 345 |
goalw thy [free_tv_subst,dom_def] |
346 |
"free_tv (%u::nat. $ s1 (s2 u) :: typ) <= \ |
|
347 |
\ free_tv s1 Un free_tv s2"; |
|
2513
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
2031
diff
changeset
|
348 |
by (fast_tac (set_cs addSDs [free_tv_app_subst_te RS subsetD, |
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
2031
diff
changeset
|
349 |
free_tv_subst_var RS subsetD] |
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
2031
diff
changeset
|
350 |
addss (!simpset delsimps bex_simps |
d708d8cdc8e8
New miniscoping rules for the bounded quantifiers and UN/INT operators
paulson
parents:
2031
diff
changeset
|
351 |
addsimps [cod_def,dom_def])) 1); |
1521 | 352 |
qed "free_tv_comp_subst"; |
353 |