307 ML {* fun lift_thm_fset lthy t = lift_thm lthy qty "fset" rsp_thms defs t *} |
307 ML {* fun lift_thm_fset lthy t = lift_thm lthy qty "fset" rsp_thms defs t *} |
308 |
308 |
309 lemma eq_r: "a = b \<Longrightarrow> a \<approx> b" |
309 lemma eq_r: "a = b \<Longrightarrow> a \<approx> b" |
310 by (simp add: list_eq_refl) |
310 by (simp add: list_eq_refl) |
311 |
311 |
|
312 (* ML {* lift_thm_fset @{context} @{thm neq_Nil_conv} *} *) |
312 ML {* lift_thm_fset @{context} @{thm m1} *} |
313 ML {* lift_thm_fset @{context} @{thm m1} *} |
313 ML {* lift_thm_fset @{context} @{thm m2} *} |
314 ML {* lift_thm_fset @{context} @{thm m2} *} |
314 ML {* lift_thm_fset @{context} @{thm list_eq.intros(4)} *} |
315 ML {* lift_thm_fset @{context} @{thm list_eq.intros(4)} *} |
315 ML {* lift_thm_fset @{context} @{thm list_eq.intros(5)} *} |
316 ML {* lift_thm_fset @{context} @{thm list_eq.intros(5)} *} |
316 ML {* lift_thm_fset @{context} @{thm card1_suc} *} |
317 ML {* lift_thm_fset @{context} @{thm card1_suc} *} |
317 ML {* lift_thm_fset @{context} @{thm map_append} *} |
318 ML {* lift_thm_fset @{context} @{thm map_append} *} |
318 ML {* lift_thm_fset @{context} @{thm eq_r[OF append_assoc]} *} |
319 ML {* lift_thm_fset @{context} @{thm eq_r[OF append_assoc]} *} |
319 |
320 |
320 thm fold1.simps(2) |
321 thm fold1.simps(2) |
321 thm list.recs(2) |
322 thm list.recs(2) |
|
323 thm list.cases |
|
324 |
322 |
325 |
323 ML {* val ind_r_a = atomize_thm @{thm list.induct} *} |
326 ML {* val ind_r_a = atomize_thm @{thm list.induct} *} |
324 (* prove {* build_regularize_goal ind_r_a rty rel @{context} *} |
327 (*prove {* build_regularize_goal ind_r_a rty rel @{context} *} |
325 ML_prf {* fun tac ctxt = |
328 ML_prf {* fun tac ctxt = |
326 (asm_full_simp_tac ((Simplifier.context ctxt HOL_ss) addsimps |
329 (asm_full_simp_tac ((Simplifier.context ctxt HOL_ss) addsimps |
327 [(@{thm equiv_res_forall} OF [rel_eqv]), |
330 [(@{thm equiv_res_forall} OF [rel_eqv]), |
328 (@{thm equiv_res_exists} OF [rel_eqv])])) THEN_ALL_NEW |
331 (@{thm equiv_res_exists} OF [rel_eqv])])) THEN_ALL_NEW |
329 (((rtac @{thm RIGHT_RES_FORALL_REGULAR}) THEN' (RANGE [fn _ => all_tac, atac]) THEN' |
332 (((rtac @{thm RIGHT_RES_FORALL_REGULAR}) THEN' (RANGE [fn _ => all_tac, atac]) THEN' |
330 (MetisTools.metis_tac ctxt [])) ORELSE' (MetisTools.metis_tac ctxt [])); *} |
333 (MetisTools.metis_tac ctxt [])) ORELSE' (MetisTools.metis_tac ctxt [])); *} |
331 apply (tactic {* tac @{context} 1 *}) *) |
334 apply (tactic {* tac @{context} 1 *})*) |
332 ML {* val ind_r_r = regularize ind_r_a rty rel rel_eqv @{context} *} |
335 ML {* val ind_r_r = regularize ind_r_a rty rel rel_eqv @{context} *} |
333 ML {* |
336 ML {* |
334 val rt = build_repabs_term @{context} ind_r_r consts rty qty |
337 val rt = build_repabs_term @{context} ind_r_r consts rty qty |
335 val rg = Logic.mk_equals ((Thm.prop_of ind_r_r), rt); |
338 val rg = Logic.mk_equals ((Thm.prop_of ind_r_r), rt); |
336 *} |
339 *} |