314 ML {* lift_thm_fset @{context} @{thm m2} *} |
314 ML {* lift_thm_fset @{context} @{thm m2} *} |
315 ML {* lift_thm_fset @{context} @{thm list_eq.intros(4)} *} |
315 ML {* lift_thm_fset @{context} @{thm list_eq.intros(4)} *} |
316 ML {* lift_thm_fset @{context} @{thm list_eq.intros(5)} *} |
316 ML {* lift_thm_fset @{context} @{thm list_eq.intros(5)} *} |
317 ML {* lift_thm_fset @{context} @{thm card1_suc} *} |
317 ML {* lift_thm_fset @{context} @{thm card1_suc} *} |
318 ML {* lift_thm_fset @{context} @{thm map_append} *} |
318 ML {* lift_thm_fset @{context} @{thm map_append} *} |
319 ML {* lift_thm_fset @{context} @{thm eq_r[OF append_assoc]} *} |
319 ML {* lift_thm_fset @{context} @{thm append_assoc} *} |
320 |
320 |
321 thm fold1.simps(2) |
321 thm fold1.simps(2) |
322 thm list.recs(2) |
322 thm list.recs(2) |
323 thm list.cases |
323 thm list.cases |
324 |
324 |
325 |
325 |
326 ML {* val ind_r_a = atomize_thm @{thm list.induct} *} |
326 ML {* val ind_r_a = atomize_thm @{thm m2} *} |
327 (*prove {* build_regularize_goal ind_r_a rty rel @{context} *} |
327 prove {* build_regularize_goal ind_r_a rty rel @{context} *} |
328 ML_prf {* fun tac ctxt = |
328 ML_prf {* fun tac ctxt = |
329 (asm_full_simp_tac ((Simplifier.context ctxt HOL_ss) addsimps |
329 (FIRST' [ |
|
330 rtac rel_refl, |
|
331 atac, |
|
332 (rtac @{thm allI} THEN' dtac @{thm spec}), |
|
333 (fn i => CHANGED (asm_full_simp_tac ((Simplifier.context ctxt HOL_ss) addsimps |
330 [(@{thm equiv_res_forall} OF [rel_eqv]), |
334 [(@{thm equiv_res_forall} OF [rel_eqv]), |
331 (@{thm equiv_res_exists} OF [rel_eqv])])) THEN_ALL_NEW |
335 (@{thm equiv_res_exists} OF [rel_eqv])]) i)), |
332 (((rtac @{thm RIGHT_RES_FORALL_REGULAR}) THEN' (RANGE [fn _ => all_tac, atac]) THEN' |
336 MetisTools.metis_tac ctxt [], |
333 (MetisTools.metis_tac ctxt [])) ORELSE' (MetisTools.metis_tac ctxt [])); *} |
337 rtac (@{thm eq_rr} OF [rel_refl]), |
334 apply (tactic {* tac @{context} 1 *})*) |
338 ((rtac @{thm RIGHT_RES_FORALL_REGULAR}) THEN' (RANGE [fn _ => all_tac, atac])) |
|
339 ]); |
|
340 *} |
|
341 apply (tactic {* tac @{context} 1 *}) |
|
342 apply (tactic {* tac @{context} 1 *}) |
|
343 apply (tactic {* tac @{context} 1 *}) |
|
344 |
|
345 |
335 ML {* val ind_r_r = regularize ind_r_a rty rel rel_eqv @{context} *} |
346 ML {* val ind_r_r = regularize ind_r_a rty rel rel_eqv @{context} *} |
336 ML {* |
347 ML {* |
337 val rt = build_repabs_term @{context} ind_r_r consts rty qty |
348 val rt = build_repabs_term @{context} ind_r_r consts rty qty |
338 val rg = Logic.mk_equals ((Thm.prop_of ind_r_r), rt); |
349 val rg = Logic.mk_equals ((Thm.prop_of ind_r_r), rt); |
339 *} |
350 *} |