424 prove rg |
424 prove rg |
425 apply(atomize(full)) |
425 apply(atomize(full)) |
426 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
426 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
427 done |
427 done |
428 |
428 |
429 ML {* val (g, thm, othm) = |
429 ML {* val ind_r_t = |
430 Toplevel.program (fn () => |
430 Toplevel.program (fn () => |
431 repabs_eq @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"} |
431 repabs @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"} |
432 @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2} |
432 @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2} |
433 (@{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp} @ @{thms ho_all_prs ho_ex_prs}) |
433 (@{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp} @ @{thms ho_all_prs ho_ex_prs}) |
434 ) |
434 ) |
435 *} |
435 *} |
436 |
436 ML {* val ind_r_l = simp_lam_prs @{context} ind_r_t *} |
437 ML {* |
|
438 fun tac2 ctxt = |
|
439 (simp_tac ((Simplifier.context ctxt empty_ss) addsimps [symmetric thm])) |
|
440 THEN' (rtac othm); *} |
|
441 (* ML {* val cthm = Goal.prove @{context} [] [] g (fn x => tac2 (#context x) 1); |
|
442 *} *) |
|
443 |
|
444 ML {* |
|
445 val ind_r_t2 = |
|
446 Toplevel.program (fn () => |
|
447 repabs_eq2 @{context} (g, thm, othm) |
|
448 ) |
|
449 *} |
|
450 ML {* val ind_r_l = simp_lam_prs @{context} ind_r_t2 *} |
|
451 lemma app_prs_for_induct: "(ABS_fset ---> id) f (REP_fset T1) = f T1" |
437 lemma app_prs_for_induct: "(ABS_fset ---> id) f (REP_fset T1) = f T1" |
452 apply (simp add: fun_map.simps QUOT_TYPE_I_fset.thm10) |
438 apply (simp add: fun_map.simps QUOT_TYPE_I_fset.thm10) |
453 done |
439 done |
454 |
440 |
455 ML {* val ind_r_l1 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l *} |
441 ML {* val ind_r_l1 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l *} |
466 ML {* |
452 ML {* |
467 fun lift thm = |
453 fun lift thm = |
468 let |
454 let |
469 val ind_r_a = atomize_thm thm; |
455 val ind_r_a = atomize_thm thm; |
470 val ind_r_r = regularize ind_r_a @{typ "'a List.list"} @{term "op \<approx>"} @{thm equiv_list_eq} @{context}; |
456 val ind_r_r = regularize ind_r_a @{typ "'a List.list"} @{term "op \<approx>"} @{thm equiv_list_eq} @{context}; |
471 val (g, t, ot) = |
457 val ind_r_t = |
472 repabs_eq @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"} |
458 repabs @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"} |
473 @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2} |
459 @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2} |
474 (@{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp} @ @{thms ho_all_prs ho_ex_prs}); |
460 (@{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp} @ @{thms ho_all_prs ho_ex_prs}); |
475 val ind_r_t = repabs_eq2 @{context} (g, t, ot); |
|
476 val ind_r_l = simp_lam_prs @{context} ind_r_t; |
461 val ind_r_l = simp_lam_prs @{context} ind_r_t; |
477 val ind_r_a = simp_allex_prs @{context} quot ind_r_l; |
462 val ind_r_a = simp_allex_prs @{context} quot ind_r_l; |
478 val ind_r_d = repeat_eqsubst_thm @{context} fset_defs_sym ind_r_a; |
463 val ind_r_d = repeat_eqsubst_thm @{context} fset_defs_sym ind_r_a; |
479 val ind_r_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} ind_r_d |
464 val ind_r_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} ind_r_d |
480 in |
465 in |
488 ML {* lift @{thm m1} *} |
473 ML {* lift @{thm m1} *} |
489 ML {* lift @{thm list_eq.intros(4)} *} |
474 ML {* lift @{thm list_eq.intros(4)} *} |
490 ML {* lift @{thm list_eq.intros(5)} *} |
475 ML {* lift @{thm list_eq.intros(5)} *} |
491 ML {* lift @{thm card1_suc} *} |
476 ML {* lift @{thm card1_suc} *} |
492 ML {* lift @{thm map_append} *} |
477 ML {* lift @{thm map_append} *} |
493 |
478 (* ML {* lift @{thm append_assoc} *}*) |
494 (* ML {* lift @{thm append_assoc} *} *) |
479 |
495 |
480 thm |
496 thm |
|
497 |
481 |
498 |
482 |
499 (*notation ( output) "prop" ("#_" [1000] 1000) *) |
483 (*notation ( output) "prop" ("#_" [1000] 1000) *) |
500 notation ( output) "Trueprop" ("#_" [1000] 1000) |
484 notation ( output) "Trueprop" ("#_" [1000] 1000) |
501 |
485 |