author  nipkow 
Fri, 17 Jan 1997 18:32:24 +0100  
changeset 2523  0ccea141409b 
parent 2513  d708d8cdc8e8 
child 2525  477c05586286 
permissions  rwrr 
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 