equal
deleted
inserted
replaced
307 @{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp} |
307 @{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp} |
308 @ @{thms ho_all_prs ho_ex_prs} *} |
308 @ @{thms ho_all_prs ho_ex_prs} *} |
309 |
309 |
310 ML {* fun lift_thm_fset lthy t = lift_thm lthy qty "fset" rsp_thms defs t *} |
310 ML {* fun lift_thm_fset lthy t = lift_thm lthy qty "fset" rsp_thms defs t *} |
311 |
311 |
312 lemma eq_r: "a = b \<Longrightarrow> a \<approx> b" |
|
313 by (simp add: list_eq_refl) |
|
314 |
|
315 (* ML {* lift_thm_fset @{context} @{thm neq_Nil_conv} *} *) |
312 (* ML {* lift_thm_fset @{context} @{thm neq_Nil_conv} *} *) |
316 ML {* lift_thm_fset @{context} @{thm m1} *} |
313 ML {* lift_thm_fset @{context} @{thm m1} *} |
317 ML {* lift_thm_fset @{context} @{thm m2} *} |
314 ML {* lift_thm_fset @{context} @{thm m2} *} |
318 ML {* lift_thm_fset @{context} @{thm list_eq.intros(4)} *} |
315 ML {* lift_thm_fset @{context} @{thm list_eq.intros(4)} *} |
319 ML {* lift_thm_fset @{context} @{thm list_eq.intros(5)} *} |
316 ML {* lift_thm_fset @{context} @{thm list_eq.intros(5)} *} |
320 ML {* lift_thm_fset @{context} @{thm card1_suc} *} |
317 ML {* lift_thm_fset @{context} @{thm card1_suc} *} |
321 (*ML {* lift_thm_fset @{context} @{thm map_append} *}*) |
318 (*ML {* lift_thm_fset @{context} @{thm map_append} *}*) |
322 ML {* lift_thm_fset @{context} @{thm append_assoc} *} |
319 ML {* lift_thm_fset @{context} @{thm append_assoc} *} |
|
320 ML {* lift_thm_fset @{context} @{thm list.induct} *} |
323 |
321 |
324 thm fold1.simps(2) |
322 thm fold1.simps(2) |
325 thm list.recs(2) |
323 thm list.recs(2) |
326 thm list.cases |
324 thm list.cases |
327 |
325 |
341 ]); |
339 ]); |
342 *} |
340 *} |
343 apply (atomize(full)) |
341 apply (atomize(full)) |
344 apply (tactic {* tac @{context} 1 *}) *) |
342 apply (tactic {* tac @{context} 1 *}) *) |
345 ML {* val ind_r_r = regularize ind_r_a rty rel rel_eqv rel_refl @{context} *} |
343 ML {* val ind_r_r = regularize ind_r_a rty rel rel_eqv rel_refl @{context} *} |
346 (* ML {* |
344 (*ML {* |
347 val rt = build_repabs_term @{context} ind_r_r consts rty qty |
345 val rt = build_repabs_term @{context} ind_r_r consts rty qty |
348 val rg = Logic.mk_equals ((Thm.prop_of ind_r_r), rt); |
346 val rg = Logic.mk_equals ((Thm.prop_of ind_r_r), rt); |
349 *} |
347 *} |
350 prove rg |
348 prove rg |
351 apply(atomize(full)) |
349 apply(atomize(full)) |
352 ML_prf {* fun r_mk_comb_tac_fset lthy = r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms *} |
350 ML_prf {* fun r_mk_comb_tac_fset lthy = r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms *} |
353 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
|
354 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
|
355 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
|
356 |
|
357 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
351 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
358 done*) |
352 done*) |
359 ML {* val ind_r_t = |
353 ML {* val ind_r_t = |
360 Toplevel.program (fn () => |
354 Toplevel.program (fn () => |
361 repabs @{context} ind_r_r consts rty qty quot rel_refl trans2 rsp_thms |
355 repabs @{context} ind_r_r consts rty qty quot rel_refl trans2 rsp_thms |
363 *} |
357 *} |
364 |
358 |
365 ML {* val abs = findabs rty (prop_of (atomize_thm @{thm list.induct})) *} |
359 ML {* val abs = findabs rty (prop_of (atomize_thm @{thm list.induct})) *} |
366 ML {* val aps = findaps rty (prop_of (atomize_thm @{thm list.induct})) *} |
360 ML {* val aps = findaps rty (prop_of (atomize_thm @{thm list.induct})) *} |
367 ML {* val simp_app_prs_thms = map (make_simp_prs_thm @{context} quot @{thm APP_PRS}) aps *} |
361 ML {* val simp_app_prs_thms = map (make_simp_prs_thm @{context} quot @{thm APP_PRS}) aps *} |
|
362 thm APP_PRS |
|
363 ML aps |
368 ML {* val simp_lam_prs_thms = map (make_simp_prs_thm @{context} quot @{thm LAMBDA_PRS}) abs *} |
364 ML {* val simp_lam_prs_thms = map (make_simp_prs_thm @{context} quot @{thm LAMBDA_PRS}) abs *} |
369 ML {* val ind_r_l = repeat_eqsubst_thm @{context} (simp_app_prs_thms @ simp_lam_prs_thms) ind_r_t *} |
365 ML {* val ind_r_l = repeat_eqsubst_thm @{context} (simp_app_prs_thms @ simp_lam_prs_thms) ind_r_t *} |
370 ML {* val thm = @{thm FORALL_PRS[OF FUN_QUOTIENT[OF QUOTIENT_fset IDENTITY_QUOTIENT]]} *} |
366 ML {* val thm = @{thm FORALL_PRS[OF FUN_QUOTIENT[OF QUOTIENT_fset IDENTITY_QUOTIENT]]} *} |
371 ML {* val ind_r_a = simp_allex_prs quot [thm] ind_r_l *} |
367 ML {* val ind_r_a = simp_allex_prs quot [thm] ind_r_l *} |
372 ML {* val defs_sym = add_lower_defs @{context} defs *} |
368 ML {* val defs_sym = add_lower_defs @{context} defs *} |