349 ML {* val defs_sym = add_lower_defs @{context} defs *} |
346 ML {* val defs_sym = add_lower_defs @{context} defs *} |
350 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
347 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
351 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset" *} |
348 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset" *} |
352 |
349 |
353 |
350 |
354 ML {* val ind_r_a = atomize_thm @{thm map_append} *} |
351 ML {* val t_a = atomize_thm @{thm map_append} *} |
355 prove {* build_regularize_goal ind_r_a rty rel @{context} *} |
352 (* prove {* build_regularize_goal t_a rty rel @{context} *} |
356 ML_prf {* fun tac ctxt = |
353 ML_prf {* fun tac ctxt = FIRST' [ |
357 (FIRST' [ |
|
358 rtac rel_refl, |
354 rtac rel_refl, |
359 atac, |
355 atac, |
360 rtac @{thm get_rid}, |
356 rtac @{thm universal_twice}, |
361 rtac @{thm get_rid2}, |
357 (rtac @{thm impI} THEN' atac), |
362 (fn i => CHANGED (asm_full_simp_tac ((Simplifier.context ctxt HOL_ss) addsimps |
358 rtac @{thm implication_twice}, |
|
359 (*rtac @{thm equality_twice},*) |
|
360 EqSubst.eqsubst_tac ctxt [0] |
363 [(@{thm equiv_res_forall} OF [rel_eqv]), |
361 [(@{thm equiv_res_forall} OF [rel_eqv]), |
364 (@{thm equiv_res_exists} OF [rel_eqv])]) i)), |
362 (@{thm equiv_res_exists} OF [rel_eqv])], |
365 (rtac @{thm impI} THEN' (asm_full_simp_tac (Simplifier.context ctxt HOL_ss)) THEN' rtac rel_refl), |
363 (rtac @{thm impI} THEN' (asm_full_simp_tac (Simplifier.context ctxt HOL_ss)) THEN' rtac rel_refl), |
366 (rtac @{thm RIGHT_RES_FORALL_REGULAR}) |
364 (rtac @{thm RIGHT_RES_FORALL_REGULAR}) |
367 ]); |
365 ]; *} |
368 *} |
|
369 apply (atomize(full)) |
366 apply (atomize(full)) |
370 apply (tactic {* tac @{context} 1 *}) *) |
367 apply (tactic {* REPEAT_ALL_NEW (tac @{context}) 1 *}) |
371 ML {* val ind_r_r = regularize ind_r_a rty rel rel_eqv rel_refl @{context} *} |
368 done*) |
|
369 |
|
370 ML {* val t_r = regularize t_a rty rel rel_eqv rel_refl @{context} *} |
372 ML {* |
371 ML {* |
373 val rt = build_repabs_term @{context} ind_r_r consts rty qty |
372 val rt = build_repabs_term @{context} t_r consts rty qty |
374 val rg = Logic.mk_equals ((Thm.prop_of ind_r_r), rt); |
373 val rg = Logic.mk_equals ((Thm.prop_of t_r), rt); |
375 *} |
374 *} |
|
375 |
|
376 ML {* val ttt = snd (dest_Free (term_of @{cpat "f :: ?'a list \<Rightarrow> ?'a list"})) *} |
|
377 ML {* old_get_fun repF @{typ "'a list"} @{typ "'a fset"} @{context} @{typ "'a list \<Rightarrow> 'a list"} *} |
|
378 |
376 prove rg |
379 prove rg |
377 apply(atomize(full)) |
380 apply(atomize(full)) |
378 ML_prf {* fun r_mk_comb_tac_fset lthy = r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms *} |
381 ML_prf {* fun r_mk_comb_tac_fset lthy = r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms *} |
379 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
382 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
380 done |
383 done |
381 ML {* val ind_r_t = |
384 ML {* val t_t = |
382 Toplevel.program (fn () => |
385 Toplevel.program (fn () => |
383 repabs @{context} ind_r_r consts rty qty quot rel_refl trans2 rsp_thms |
386 repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms |
384 ) |
387 ) |
385 *} |
388 *} |
386 |
389 |
387 ML {* val abs = findabs rty (prop_of (atomize_thm @{thm list.induct})) *} |
390 ML {* val abs = findabs rty (prop_of (atomize_thm @{thm list.induct})) *} |
388 ML {* val aps = findaps rty (prop_of (atomize_thm @{thm list.induct})) *} |
391 ML {* val aps = findaps rty (prop_of (atomize_thm @{thm list.induct})) *} |
389 ML {* val simp_lam_prs_thms = map (make_simp_prs_thm @{context} quot @{thm LAMBDA_PRS}) abs *} |
392 ML {* val lam_prs_thms = map (make_simp_prs_thm @{context} quot @{thm LAMBDA_PRS}) abs *} |
390 ML {* val ind_r_l = repeat_eqsubst_thm @{context} (simp_app_prs_thms @ simp_lam_prs_thms) ind_r_t *} |
393 ML {* val app_prs_thms = map (applic_prs @{context} rty qty absrep) aps *} |
391 ML {* val thm = @{thm FORALL_PRS[OF FUN_QUOTIENT[OF QUOTIENT_fset IDENTITY_QUOTIENT]]} *} |
394 ML {* val app_prs_thms = map Thm.freezeT app_prs_thms *} |
392 ML {* val ind_r_a = simp_allex_prs quot [thm] ind_r_l *} |
395 ML {* val t_l = repeat_eqsubst_thm @{context} (app_prs_thms @ lam_prs_thms) t_t *} |
|
396 ML {* val (alls, exs) = findallex rty qty (prop_of t_a); *} |
|
397 ML {* val allthms = map (make_allex_prs_thm @{context} quot @{thm FORALL_PRS}) alls *} |
|
398 ML {* val allthmsv = map Thm.varifyT allthms *} |
|
399 ML {* val t_a = MetaSimplifier.rewrite_rule (allthmsv) t_l *} |
393 ML {* val defs_sym = add_lower_defs @{context} defs *} |
400 ML {* val defs_sym = add_lower_defs @{context} defs *} |
394 ML {* val ind_r_d = repeat_eqsubst_thm @{context} defs_sym ind_r_a *} |
401 ML {* val t_d = repeat_eqsubst_thm @{context} defs_sym t_a *} |
395 ML {* val ind_r_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} ind_r_d *} |
402 ML {* val t_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} t_d *} |
396 ML {* ObjectLogic.rulify ind_r_s *} |
403 ML {* ObjectLogic.rulify t_s *} |
397 |
404 |
398 ML {* |
405 ML {* |
399 fun lift_thm_fset_note name thm lthy = |
406 fun lift_thm_fset_note name thm lthy = |
400 let |
407 let |
401 val lifted_thm = lift_thm_fset lthy thm; |
408 val lifted_thm = lift_thm_fset lthy thm; |