194 FV_kind_def FV_ty_def FV_trm_def perm_kind_def perm_ty_def perm_trm_def} |
194 FV_kind_def FV_ty_def FV_trm_def perm_kind_def perm_ty_def perm_trm_def} |
195 *} |
195 *} |
196 ML {* val consts = lookup_quot_consts defs *} |
196 ML {* val consts = lookup_quot_consts defs *} |
197 |
197 |
198 thm akind_aty_atrm.induct |
198 thm akind_aty_atrm.induct |
|
199 |
|
200 ML {* |
|
201 fun regularize_monos_tac lthy eqvs = |
|
202 let |
|
203 val subs1 = map (fn x => @{thm equiv_res_forall} OF [x]) eqvs |
|
204 val subs2 = map (fn x => @{thm equiv_res_exists} OF [x]) eqvs |
|
205 in |
|
206 REPEAT_ALL_NEW (FIRST' [ |
|
207 (rtac @{thm impI} THEN' atac), |
|
208 (rtac @{thm my_equiv_res_forallR}), |
|
209 (rtac @{thm my_equiv_res_forallL}), |
|
210 (rtac @{thm Set.imp_mono}), |
|
211 (resolve_tac (Inductive.get_monos lthy)), |
|
212 (EqSubst.eqsubst_tac lthy [0] (subs1 @ subs2)) |
|
213 ]) |
|
214 end |
|
215 *} |
|
216 |
|
217 ML {* |
|
218 val subs1 = map (fn x => @{thm eq_reflection} OF [@{thm equiv_res_forall} OF [x]]) @{thms alpha_EQUIVs} |
|
219 *} |
|
220 |
|
221 ML {* |
|
222 fun regularize_tac ctxt rel_eqvs rel_refls = |
|
223 let |
|
224 val subs1 = map (fn x => @{thm equiv_res_forall} OF [x]) rel_eqvs |
|
225 val subs2 = map (fn x => @{thm equiv_res_exists} OF [x]) rel_eqvs |
|
226 in |
|
227 (ObjectLogic.full_atomize_tac) THEN' |
|
228 REPEAT_ALL_NEW (FIRST' [ |
|
229 FIRST' (map rtac rel_refls), |
|
230 atac, |
|
231 rtac @{thm universal_twice}, |
|
232 rtac @{thm impI} THEN' atac, |
|
233 rtac @{thm implication_twice}, |
|
234 EqSubst.eqsubst_tac ctxt [0] (subs1 @ subs2), |
|
235 (* For a = b \<longrightarrow> a \<approx> b *) |
|
236 (rtac @{thm RIGHT_RES_FORALL_REGULAR}) |
|
237 ]) |
|
238 end |
|
239 *} |
|
240 thm RIGHT_RES_FORALL_REGULAR |
|
241 thm my_equiv_res_forallR |
|
242 |
|
243 (* |
|
244 lemma "\<And>i j xb\<Colon>trm \<Rightarrow> trm \<Rightarrow> bool. Respects (atrm ===> atrm ===> op =) xb \<Longrightarrow> (\<forall>m\<Colon>trm \<Rightarrow> trm\<in>Respects (atrm ===> atrm). xb (Const i) (m (Const j))) \<longrightarrow> (\<forall>m\<Colon>trm \<Rightarrow> trm. xb (Const i) (m (Const j)))" |
|
245 apply (simp add: Ball_def IN_RESPECTS Respects_def) |
|
246 apply (metis COMBK_def al_refl(3)) |
|
247 *) |
|
248 |
|
249 lemma move_quant: "((\<forall>y. \<forall>x\<in>P. A x y) \<longrightarrow> (\<forall>y. \<forall>x. B x y)) \<Longrightarrow> ((\<forall>x\<in>P. \<forall>y. A x y) \<longrightarrow> (\<forall>x. \<forall>y. B x y))" |
|
250 by auto |
199 |
251 |
200 lemma "\<lbrakk>P1 TYP TYP; \<And>A A' K K' x. \<lbrakk>(A::TY) = A'; P2 A A'; (K::KIND) = K'; P1 K K'\<rbrakk> \<Longrightarrow> P1 (KPI A x K) (KPI A' x K'); |
252 lemma "\<lbrakk>P1 TYP TYP; \<And>A A' K K' x. \<lbrakk>(A::TY) = A'; P2 A A'; (K::KIND) = K'; P1 K K'\<rbrakk> \<Longrightarrow> P1 (KPI A x K) (KPI A' x K'); |
201 \<And>A A' K x x' K'. |
253 \<And>A A' K x x' K'. |
202 \<lbrakk>(A ::TY) = A'; P2 A A'; (K :: KIND) = ([(x, x')] \<bullet> K'); P1 K ([(x, x')] \<bullet> K'); x \<notin> FV_ty A'; x \<notin> FV_kind K' - {x'}\<rbrakk> |
254 \<lbrakk>(A ::TY) = A'; P2 A A'; (K :: KIND) = ([(x, x')] \<bullet> K'); P1 K ([(x, x')] \<bullet> K'); x \<notin> FV_ty A'; x \<notin> FV_kind K' - {x'}\<rbrakk> |
203 \<Longrightarrow> P1 (KPI A x K) (KPI A' x' K'); |
255 \<Longrightarrow> P1 (KPI A x K) (KPI A' x' K'); |
214 \<lbrakk>(A ::TY) = A'; P2 A A'; (M :: TRM) = ([(x, x')] \<bullet> M'); P3 M ([(x, x')] \<bullet> M'); x \<notin> FV_ty B'; x \<notin> FV_trm M' - {x'}\<rbrakk> |
266 \<lbrakk>(A ::TY) = A'; P2 A A'; (M :: TRM) = ([(x, x')] \<bullet> M'); P3 M ([(x, x')] \<bullet> M'); x \<notin> FV_ty B'; x \<notin> FV_trm M' - {x'}\<rbrakk> |
215 \<Longrightarrow> P3 (LAM A x M) (LAM A' x' M')\<rbrakk> |
267 \<Longrightarrow> P3 (LAM A x M) (LAM A' x' M')\<rbrakk> |
216 \<Longrightarrow> ((x1 :: KIND) = x2 \<longrightarrow> P1 x1 x2) \<and> |
268 \<Longrightarrow> ((x1 :: KIND) = x2 \<longrightarrow> P1 x1 x2) \<and> |
217 ((x3 ::TY) = x4 \<longrightarrow> P2 x3 x4) \<and> ((x5 :: TRM) = x6 \<longrightarrow> P3 x5 x6)" |
269 ((x3 ::TY) = x4 \<longrightarrow> P2 x3 x4) \<and> ((x5 :: TRM) = x6 \<longrightarrow> P3 x5 x6)" |
218 apply(tactic {* procedure_tac @{context} @{thm akind_aty_atrm.induct} 1 *}) |
270 apply(tactic {* procedure_tac @{context} @{thm akind_aty_atrm.induct} 1 *}) |
|
271 apply(tactic {* (simp_tac ((Simplifier.context @{context} empty_ss) addsimps (subs1))) 1 *}) |
219 apply(atomize (full)) |
272 apply(atomize (full)) |
220 apply(rule my_equiv_res_forallR) |
273 apply(rule RIGHT_RES_FORALL_REGULAR) |
221 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
274 apply(rule RIGHT_RES_FORALL_REGULAR) |
222 apply(rule my_equiv_res_forallR) |
275 apply(rule RIGHT_RES_FORALL_REGULAR) |
223 apply(tactic {* REPEAT_ALL_NEW (resolve_tac (Inductive.get_monos @{context})) 1 *}) |
276 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
224 apply(rule my_equiv_res_forallR) |
277 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
225 apply(tactic {* REPEAT_ALL_NEW (resolve_tac (Inductive.get_monos @{context})) 1 *}) |
278 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
226 apply(rule my_equiv_res_forallR) |
279 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
227 apply(tactic {* REPEAT_ALL_NEW (resolve_tac (Inductive.get_monos @{context})) 1 *}) |
280 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
228 apply(rule my_equiv_res_forallR) |
281 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
229 apply(tactic {* REPEAT_ALL_NEW (resolve_tac (Inductive.get_monos @{context})) 1 *}) |
282 apply(rule Set.imp_mono) |
230 apply(rule my_equiv_res_forallR) |
283 apply(rule impI) apply(assumption) |
231 apply(tactic {* REPEAT_ALL_NEW (resolve_tac (Inductive.get_monos @{context})) 1 *}) |
284 apply(rule Set.imp_mono) |
232 apply(rule my_equiv_res_forallR) |
285 apply(rule impI) apply(assumption) |
233 apply(tactic {* REPEAT_ALL_NEW (resolve_tac (Inductive.get_monos @{context})) 1 *}) |
286 apply(rule Set.imp_mono) |
234 apply(rule my_equiv_res_forallR) |
287 apply(rule impI) apply(assumption) |
235 apply(tactic {* REPEAT_ALL_NEW (resolve_tac (Inductive.get_monos @{context})) 1 *}) |
288 apply(rule Set.imp_mono) |
236 apply(rule my_equiv_res_forallR) |
289 apply(rule impI) apply(assumption) |
237 apply(tactic {* (resolve_tac (Inductive.get_monos @{context})) 1 *}) |
290 apply(rule Set.imp_mono) |
238 apply(rule Set.imp_mono) |
291 apply(rule impI) apply(assumption) |
239 apply(rule impI) |
292 apply(rule Set.imp_mono) |
240 apply(assumption) |
293 apply(rule impI) apply(assumption) |
241 apply(rule Set.imp_mono) |
294 apply(rule Set.imp_mono) |
242 |
295 apply(rule impI) apply(assumption) |
243 |
296 apply(rule Set.imp_mono) |
|
297 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
298 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
299 apply (simp add: Ball_def IN_RESPECTS Respects_def) |
|
300 apply (metis COMBK_def al_refl(3)) |
|
301 apply(rule Set.imp_mono) |
|
302 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
303 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
304 apply (simp add: Ball_def IN_RESPECTS Respects_def) |
|
305 apply (metis COMBK_def al_refl(3)) |
|
306 apply(rule Set.imp_mono) |
|
307 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
308 apply(rule move_quant) |
|
309 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
310 apply(rule move_quant) |
|
311 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
312 apply(rule move_quant) |
|
313 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *}) |
|
314 apply (simp add: Ball_def IN_RESPECTS Respects_def) |
|
315 apply (metis COMBK_def al_refl(3)) |
|
316 apply(rule impI) apply(assumption) |
244 |
317 |
245 ML {* |
318 ML {* |
246 val rty_qty_rel = |
319 val rty_qty_rel = |
247 [(@{typ kind}, (@{typ KIND}, @{term akind})), |
320 [(@{typ kind}, (@{typ KIND}, @{term akind})), |
248 (@{typ ty}, (@{typ TY}, @{term aty})), |
321 (@{typ ty}, (@{typ TY}, @{term aty})), |
249 (@{typ trm}, (@{typ TRM}, @{term atrm}))] |
322 (@{typ trm}, (@{typ TRM}, @{term atrm}))] |
250 *} |
323 *} |
251 |
324 |
252 print_quotients |
325 print_quotients |
253 |
326 |
254 ML {* val rty = [@{typ }] |
327 ML {* val rty = [@{typ }] *} |
255 ML {* val defs_sym = flat (map (add_lower_defs @{context}) defs) *} |
328 ML {* val defs_sym = flat (map (add_lower_defs @{context}) defs) *} |
256 ML {* val t_a = atomize_thm @{thm akind_aty_atrm.induct} *} |
329 ML {* val t_a = atomize_thm @{thm akind_aty_atrm.induct} *} |
257 prove {* build_regularize_goal t_a rty rel @{context} |
330 prove {* build_regularize_goal t_a rty rel @{context} |
258 |
331 |
259 end |
332 end |