278 *} |
278 *} |
279 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_lam @{context}) 1 *}) |
279 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_lam @{context}) 1 *}) |
280 *) |
280 *) |
281 |
281 |
282 ML {* val t_t = repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms *} |
282 ML {* val t_t = repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms *} |
283 |
|
284 ML {* val abs = findabs rty (prop_of (atomize_thm @{thm alpha.induct})) *} |
283 ML {* val abs = findabs rty (prop_of (atomize_thm @{thm alpha.induct})) *} |
285 ML {* val aps = findaps rty (prop_of (atomize_thm @{thm alpha.induct})) *} |
284 ML {* val aps = findaps rty (prop_of (atomize_thm @{thm alpha.induct})) *} |
|
285 ML {* prop_of (atomize_thm @{thm alpha.induct}) *} |
|
286 ML {* |
|
287 fun findall_all rty qty tm = |
|
288 case tm of |
|
289 Const (@{const_name All}, T) $ (s as (Abs(_, _, b))) => |
|
290 let |
|
291 val tys = findall_all rty qty s |
|
292 in if needs_lift rty T then |
|
293 (( T) :: tys) |
|
294 else tys end |
|
295 | Abs(_, T, b) => |
|
296 findall_all rty qty (subst_bound ((Free ("x", T)), b)) |
|
297 | f $ a => (findall_all rty qty f) @ (findall_all rty qty a) |
|
298 | _ => []; |
|
299 fun findall rty qty tm = |
|
300 map domain_type ( |
|
301 map (old_exchange_ty rty qty) |
|
302 (distinct (op =) (findall_all rty qty tm)) |
|
303 ) |
|
304 *} |
|
305 ML {* val alls = findall rty qty (prop_of (atomize_thm @{thm alpha.induct})) *} |
|
306 |
|
307 ML {* |
|
308 fun make_simp_all_prs_thm lthy quot_thm thm typ = |
|
309 let |
|
310 val (_, [lty, rty]) = dest_Type typ; |
|
311 val thy = ProofContext.theory_of lthy; |
|
312 val (lcty, rcty) = (ctyp_of thy lty, ctyp_of thy rty) |
|
313 val inst = [NONE, SOME lcty]; |
|
314 val lpi = Drule.instantiate' inst [] thm; |
|
315 val tac = |
|
316 (compose_tac (false, lpi, 1)) THEN_ALL_NEW |
|
317 (quotient_tac quot_thm); |
|
318 val gc = Drule.strip_imp_concl (cprop_of lpi); |
|
319 val t = Goal.prove_internal [] gc (fn _ => tac 1) |
|
320 in |
|
321 MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] t |
|
322 end |
|
323 *} |
|
324 ML {* val simp_app_prs_thms = map (make_simp_prs_thm @{context} quot @{thm APP_PRS}) aps *} |
286 ML {* val aps = @{typ "LamEx.rlam \<Rightarrow> bool"} :: aps; *} |
325 ML {* val aps = @{typ "LamEx.rlam \<Rightarrow> bool"} :: aps; *} |
287 ML {* val thm = |
326 ML {* val simp_lam_prs_thms = map (make_simp_prs_thm @{context} quot @{thm LAMBDA_PRS}) abs *} |
|
327 ML {* val t_l = repeat_eqsubst_thm @{context} (simp_app_prs_thms @ simp_lam_prs_thms) t_a *} |
|
328 ML {* val typ = hd (alls) *} |
|
329 |
|
330 |
|
331 ML {* |
|
332 val (_, [lty, rty]) = dest_Type typ; |
|
333 val thy = @{theory}; |
|
334 val (lcty, rcty) = (ctyp_of thy lty, ctyp_of thy rty) |
|
335 val inst = [NONE, SOME lcty]; |
|
336 val lpi = Drule.instantiate' inst [] @{thm FORALL_PRS}; |
|
337 val tac = |
|
338 (compose_tac (false, lpi, 1)) THEN_ALL_NEW |
|
339 (quotient_tac quot); |
|
340 val gc = Drule.strip_imp_concl (cprop_of lpi); |
|
341 *} |
|
342 prove tst: {*term_of gc*} |
|
343 apply (tactic {*compose_tac (false, lpi, 1) 1 *}) |
|
344 apply (tactic {*quotient_tac quot 1 *}) |
|
345 done |
|
346 thm tst |
|
347 |
|
348 |
|
349 |
|
350 |
|
351 |
|
352 ML {* val thms = (make_simp_all_prs_thm @{context} quot @{thm FORALL_PRS} o domain_type) (hd (rev alls)) *} |
|
353 ML {* val thm = |
288 @{thm FORALL_PRS[OF FUN_QUOTIENT[OF QUOTIENT_lam FUN_QUOTIENT[OF QUOTIENT_lam IDENTITY_QUOTIENT]]]} *} |
354 @{thm FORALL_PRS[OF FUN_QUOTIENT[OF QUOTIENT_lam FUN_QUOTIENT[OF QUOTIENT_lam IDENTITY_QUOTIENT]]]} *} |
289 ML {* val t_a = simp_allex_prs quot [thm] t_t *} |
355 ML {* val t_a = simp_allex_prs quot [thm] t_t *} |
290 ML {* val simp_app_prs_thms = map (make_simp_prs_thm @{context} quot @{thm APP_PRS}) aps *} |
|
291 ML {* val simp_lam_prs_thms = map (make_simp_prs_thm @{context} quot @{thm LAMBDA_PRS}) abs *} |
|
292 |
|
293 ML {* val t_l = repeat_eqsubst_thm @{context} (simp_app_prs_thms @ simp_lam_prs_thms) t_a *} |
|
294 ML {* val defs_sym = add_lower_defs @{context} defs; *} |
356 ML {* val defs_sym = add_lower_defs @{context} defs; *} |
295 ML {* val defs_sym_eq = map (fn x => eq_reflection OF [x]) defs_sym *} |
357 ML {* val defs_sym_eq = map (fn x => eq_reflection OF [x]) defs_sym *} |
296 ML t_l |
358 ML t_l |
297 ML {* val t_d0 = MetaSimplifier.rewrite_rule defs_sym_eq t_l *} |
359 ML {* val t_d0 = MetaSimplifier.rewrite_rule defs_sym_eq t_l *} |
298 ML {* val t_d = repeat_eqsubst_thm @{context} defs_sym t_d0 *} |
360 ML {* val t_d = repeat_eqsubst_thm @{context} defs_sym t_d0 *} |