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 ML {* val ind_r_a = atomize_thm @{thm list.induct} *} |
326 ML {* val ind_r_a = atomize_thm @{thm m2} *} |
326 (* prove {* build_regularize_goal ind_r_a rty rel @{context} *} |
327 prove {* build_regularize_goal ind_r_a rty rel @{context} *} |
327 ML_prf {* fun tac ctxt = |
328 ML_prf {* fun tac ctxt = |
|
329 (FIRST' [ |
328 (FIRST' [ |
330 rtac rel_refl, |
329 rtac rel_refl, |
331 atac, |
330 atac, |
332 (rtac @{thm allI} THEN' dtac @{thm spec}), |
331 rtac @{thm get_rid}, |
|
332 rtac @{thm get_rid2}, |
333 (fn i => CHANGED (asm_full_simp_tac ((Simplifier.context ctxt HOL_ss) addsimps |
333 (fn i => CHANGED (asm_full_simp_tac ((Simplifier.context ctxt HOL_ss) addsimps |
334 [(@{thm equiv_res_forall} OF [rel_eqv]), |
334 [(@{thm equiv_res_forall} OF [rel_eqv]), |
335 (@{thm equiv_res_exists} OF [rel_eqv])]) i)), |
335 (@{thm equiv_res_exists} OF [rel_eqv])]) i)), |
336 MetisTools.metis_tac ctxt [], |
336 (rtac @{thm impI} THEN' (asm_full_simp_tac (Simplifier.context ctxt HOL_ss)) THEN' rtac rel_refl), |
337 rtac (@{thm eq_rr} OF [rel_refl]), |
337 (rtac @{thm RIGHT_RES_FORALL_REGULAR}) |
338 ((rtac @{thm RIGHT_RES_FORALL_REGULAR}) THEN' (RANGE [fn _ => all_tac, atac])) |
|
339 ]); |
338 ]); |
340 *} |
339 *} |
341 apply (tactic {* tac @{context} 1 *}) |
340 apply (atomize(full)) |
342 apply (tactic {* tac @{context} 1 *}) |
341 apply (tactic {* tac @{context} 1 *}) *) |
343 apply (tactic {* tac @{context} 1 *}) |
342 ML {* val ind_r_r = regularize ind_r_a rty rel rel_eqv rel_refl @{context} *} |
344 |
|
345 |
|
346 ML {* val ind_r_r = regularize ind_r_a rty rel rel_eqv @{context} *} |
|
347 ML {* |
343 ML {* |
348 val rt = build_repabs_term @{context} ind_r_r consts rty qty |
344 val rt = build_repabs_term @{context} ind_r_r consts rty qty |
349 val rg = Logic.mk_equals ((Thm.prop_of ind_r_r), rt); |
345 val rg = Logic.mk_equals ((Thm.prop_of ind_r_r), rt); |
350 *} |
346 *} |
351 (*prove rg |
347 (*prove rg |