equal
deleted
inserted
replaced
431 ML {* val t_al = MetaSimplifier.rewrite_rule (allthms) t_d *} |
431 ML {* val t_al = MetaSimplifier.rewrite_rule (allthms) t_d *} |
432 ML {* val t_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} t_al *} |
432 ML {* val t_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} t_al *} |
433 ML {* ObjectLogic.rulify t_s *} |
433 ML {* ObjectLogic.rulify t_s *} |
434 |
434 |
435 ML {* val gl = @{term "P (x :: 'a list) (EMPTY :: 'a fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l"} *} |
435 ML {* val gl = @{term "P (x :: 'a list) (EMPTY :: 'a fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l"} *} |
436 ML {* val vars = map Free (Term.add_frees gl []) *} |
436 ML {* val gla = atomize_goal @{theory} gl *} |
437 ML {* fun lambda_all (var as Free(_, T)) trm = (Term.all T) $ lambda var trm *} |
437 |
438 ML {* val gla = fold lambda_all vars gl *} |
438 prove t_r: {* mk_REGULARIZE_goal @{context} (prop_of t_a) gla *} |
439 ML {* val glf = Type.legacy_freeze gla *} |
|
440 ML {* val glac = (snd o Thm.dest_equals o cprop_of) (ObjectLogic.atomize (cterm_of @{theory} glf)) *} |
|
441 |
|
442 prove t_r: {* mk_REGULARIZE_goal @{context} (prop_of t_a) (term_of glac) *} |
|
443 |
439 |
444 ML_prf {* fun tac ctxt = FIRST' [ |
440 ML_prf {* fun tac ctxt = FIRST' [ |
445 rtac rel_refl, |
441 rtac rel_refl, |
446 atac, |
442 atac, |
447 rtac @{thm universal_twice}, |
443 rtac @{thm universal_twice}, |
459 apply (tactic {* REPEAT_ALL_NEW (tac @{context}) 1 *}) |
455 apply (tactic {* REPEAT_ALL_NEW (tac @{context}) 1 *}) |
460 done |
456 done |
461 |
457 |
462 ML {* val t_r = @{thm t_r} OF [t_a] *} |
458 ML {* val t_r = @{thm t_r} OF [t_a] *} |
463 |
459 |
464 ML {* val ttt = mk_inj_REPABS_goal @{context} (prop_of t_r, term_of glac) *} |
460 ML {* val ttt = mk_inj_REPABS_goal @{context} (prop_of t_r, gla) *} |
465 ML {* val si = simp_ids_trm (cterm_of @{theory} ttt) *} |
461 ML {* val si = simp_ids_trm (cterm_of @{theory} ttt) *} |
466 prove t_t: {* term_of si *} |
462 prove t_t: {* term_of si *} |
467 ML_prf {* fun r_mk_comb_tac_fset lthy = r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms *} |
463 ML_prf {* fun r_mk_comb_tac_fset lthy = r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms *} |
468 apply(atomize(full)) |
464 apply(atomize(full)) |
469 apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *}) |
465 apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *}) |