276 ML {* val t_r = regularize t_a rty rel rel_eqv rel_refl @{context} *} |
276 ML {* val t_r = regularize t_a rty rel rel_eqv rel_refl @{context} *} |
277 ML {* |
277 ML {* |
278 val rt = build_repabs_term @{context} t_r consts rty qty |
278 val rt = build_repabs_term @{context} t_r consts rty qty |
279 val rg = Logic.mk_equals ((Thm.prop_of t_r), rt); |
279 val rg = Logic.mk_equals ((Thm.prop_of t_r), rt); |
280 *} |
280 *} |
281 *) |
281 |
282 |
282 |
283 lemma foldl_rsp: |
283 lemma foldl_rsp: |
284 "((IntEx.intrel ===> IntEx.intrel ===> IntEx.intrel) ===> |
284 "((IntEx.intrel ===> IntEx.intrel ===> IntEx.intrel) ===> |
285 IntEx.intrel ===> op = ===> IntEx.intrel) |
285 IntEx.intrel ===> op = ===> IntEx.intrel) |
286 foldl foldl" |
286 foldl foldl" |
310 ML {* val abs = findabs rty (prop_of t_a) *} |
310 ML {* val abs = findabs rty (prop_of t_a) *} |
311 ML {* val aps = findaps rty (prop_of t_a); *} |
311 ML {* val aps = findaps rty (prop_of t_a); *} |
312 ML {* val simp_lam_prs_thms = map (make_simp_prs_thm @{context} quot @{thm LAMBDA_PRS}) abs *} |
312 ML {* val simp_lam_prs_thms = map (make_simp_prs_thm @{context} quot @{thm LAMBDA_PRS}) abs *} |
313 |
313 |
314 (*ML {* val t_t = repabs @{context} @{thm t_r} consts rty qty quot rel_refl trans2 rsp_thms *}*) |
314 (*ML {* val t_t = repabs @{context} @{thm t_r} consts rty qty quot rel_refl trans2 rsp_thms *}*) |
315 ML {* val (alls, exs) = findallex rty qty (prop_of t_a) *} |
315 ML findallex |
|
316 ML {* val (alls, exs) = findallex @{context} rty qty (prop_of t_a) *} |
316 ML {* val allthms = map (make_allex_prs_thm @{context} quot @{thm FORALL_PRS}) alls *} |
317 ML {* val allthms = map (make_allex_prs_thm @{context} quot @{thm FORALL_PRS}) alls *} |
317 ML {* val t_a = MetaSimplifier.rewrite_rule (allthms) t_t *} |
318 ML {* val t_a = MetaSimplifier.rewrite_rule (allthms) t_t *} |
318 ML {* val t_l = repeat_eqsubst_thm @{context} simp_lam_prs_thms t_a *} |
319 ML {* val t_l = repeat_eqsubst_thm @{context} simp_lam_prs_thms t_a *} |
319 ML {* val defs_sym = add_lower_defs @{context} defs *} |
320 ML {* val defs_sym = flat (map (add_lower_defs @{context}) defs) *} |
320 ML {* val t_d = repeat_eqsubst_thm @{context} defs_sym t_l *} |
321 ML {* val t_d = repeat_eqsubst_thm @{context} defs_sym t_l *} |
321 ML {* val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d *} |
322 ML {* val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d *} |
322 ML {* ObjectLogic.rulify t_r *} |
323 ML {* ObjectLogic.rulify t_r *} |