275 |
275 |
276 ML {* |
276 ML {* |
277 fun regularize thm rty rel rel_eqv lthy = |
277 fun regularize thm rty rel rel_eqv lthy = |
278 let |
278 let |
279 val g = build_regularize_goal thm rty rel lthy; |
279 val g = build_regularize_goal thm rty rel lthy; |
280 val tac = |
280 fun tac ctxt = |
281 atac ORELSE' (simp_tac ((Simplifier.context lthy HOL_ss) addsimps |
281 (asm_full_simp_tac ((Simplifier.context ctxt HOL_ss) addsimps |
282 [(@{thm equiv_res_forall} OF [rel_eqv]), |
282 [(@{thm equiv_res_forall} OF [rel_eqv]), |
283 (@{thm equiv_res_exists} OF [rel_eqv])])) THEN_ALL_NEW |
283 (@{thm equiv_res_exists} OF [rel_eqv])])) THEN_ALL_NEW |
284 ((rtac @{thm RIGHT_RES_FORALL_REGULAR}) THEN' |
284 (((rtac @{thm RIGHT_RES_FORALL_REGULAR}) THEN' (RANGE [fn _ => all_tac, atac])) ORELSE' |
285 (RANGE [fn _ => all_tac, atac]) THEN' (MetisTools.metis_tac lthy [])); |
285 (MetisTools.metis_tac ctxt [])); |
286 val cgoal = cterm_of (ProofContext.theory_of lthy) g; |
286 val cthm = Goal.prove lthy [] [] g (fn x => tac (#context x) 1); |
287 val cthm = Goal.prove_internal [] cgoal (fn _ => tac 1); |
|
288 in |
287 in |
289 cthm OF [thm] |
288 cthm OF [thm] |
290 end |
289 end |
291 *} |
290 *} |
292 |
291 |
553 ML {* val rthm = MetaSimplifier.rewrite_rule fset_defs_sym ithm *} |
550 ML {* val rthm = MetaSimplifier.rewrite_rule fset_defs_sym ithm *} |
554 ML {* val qthm = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} rthm *} |
551 ML {* val qthm = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} rthm *} |
555 ML {* ObjectLogic.rulify qthm *} |
552 ML {* ObjectLogic.rulify qthm *} |
556 |
553 |
557 thm fold1.simps(2) |
554 thm fold1.simps(2) |
558 |
555 thm list.recs(2) |
559 |
556 |
560 ML {* val ind_r_a = atomize_thm @{thm fold1.simps(2)} *} |
557 ML {* val ind_r_a = atomize_thm @{thm m2} *} |
|
558 (* prove {* build_regularize_goal ind_r_a @{typ "'a List.list"} @{term "op \<approx>"} @{context} *} |
|
559 apply (simp add: equiv_res_forall[OF equiv_list_eq] equiv_res_exists[OF equiv_list_eq]) done *) |
|
560 |
561 ML {* val ind_r_r = regularize ind_r_a @{typ "'a List.list"} @{term "op \<approx>"} @{thm equiv_list_eq} @{context} *} |
561 ML {* val ind_r_r = regularize ind_r_a @{typ "'a List.list"} @{term "op \<approx>"} @{thm equiv_list_eq} @{context} *} |
562 ML {* |
562 ML {* |
563 val rt = build_repabs_term @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"} |
563 val rt = build_repabs_term @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"} |
564 val rg = Logic.mk_equals ((Thm.prop_of ind_r_r), rt); |
564 val rg = Logic.mk_equals ((Thm.prop_of ind_r_r), rt); |
565 *} |
565 *} |
566 (*prove rg |
566 (*prove rg |
567 apply(atomize(full)) |
567 apply(atomize(full)) |
568 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})*) |
568 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})*) |
569 ML {* val (g, thm, othm) = |
569 ML {* val (g, thm, othm) = |
570 Toplevel.program (fn () => |
570 Toplevel.program (fn () => |
571 repabs_eq @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"} |
571 repabs_eq @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"} |
572 @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2} |
572 @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2} |
573 @{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp} |
573 @{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp} |
612 |
612 |
613 ML {* lift @{thm m2} *} |
613 ML {* lift @{thm m2} *} |
614 ML {* lift @{thm m1} *} |
614 ML {* lift @{thm m1} *} |
615 ML {* lift @{thm list_eq.intros(4)} *} |
615 ML {* lift @{thm list_eq.intros(4)} *} |
616 ML {* lift @{thm list_eq.intros(5)} *} |
616 ML {* lift @{thm list_eq.intros(5)} *} |
617 |
617 (* ML {* lift @{thm length_append} *} *) |
618 (* Has all the theorems about fset plugged in. These should be parameters to the tactic *) |
|
619 ML {* |
|
620 fun transconv_fset_tac' ctxt = |
|
621 (LocalDefs.unfold_tac @{context} fset_defs) THEN |
|
622 ObjectLogic.full_atomize_tac 1 THEN |
|
623 REPEAT_ALL_NEW (FIRST' [ |
|
624 rtac @{thm list_eq_refl}, |
|
625 rtac @{thm cons_preserves}, |
|
626 rtac @{thm memb_rsp}, |
|
627 rtac @{thm card1_rsp}, |
|
628 rtac @{thm QUOT_TYPE_I_fset.R_trans2}, |
|
629 CHANGED o (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms QUOT_TYPE_I_fset.REP_ABS_rsp})), |
|
630 Cong_Tac.cong_tac @{thm cong}, |
|
631 rtac @{thm ext} |
|
632 ]) 1 |
|
633 *} |
|
634 |
|
635 ML {* |
|
636 val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m1})) |
|
637 val goal = build_repabs_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} |
|
638 val cgoal = cterm_of @{theory} goal |
|
639 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
|
640 *} |
|
641 |
618 |
642 (*notation ( output) "prop" ("#_" [1000] 1000) *) |
619 (*notation ( output) "prop" ("#_" [1000] 1000) *) |
643 notation ( output) "Trueprop" ("#_" [1000] 1000) |
620 notation ( output) "Trueprop" ("#_" [1000] 1000) |
644 |
|
645 |
|
646 prove {* (Thm.term_of cgoal2) *} |
|
647 apply (tactic {* transconv_fset_tac' @{context} *}) |
|
648 done |
|
649 |
|
650 thm length_append (* Not true but worth checking that the goal is correct *) |
|
651 ML {* |
|
652 val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm length_append})) |
|
653 val goal = build_repabs_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} |
|
654 val cgoal = cterm_of @{theory} goal |
|
655 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
|
656 *} |
|
657 prove {* Thm.term_of cgoal2 *} |
|
658 apply (tactic {* transconv_fset_tac' @{context} *}) |
|
659 sorry |
|
660 |
|
661 thm m2 |
|
662 ML {* |
|
663 val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m2})) |
|
664 val goal = build_repabs_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} |
|
665 val cgoal = cterm_of @{theory} goal |
|
666 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
|
667 *} |
|
668 prove {* Thm.term_of cgoal2 *} |
|
669 apply (tactic {* transconv_fset_tac' @{context} *}) |
|
670 done |
|
671 |
|
672 thm list_eq.intros(4) |
|
673 ML {* |
|
674 val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list_eq.intros(4)})) |
|
675 val goal = build_repabs_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} |
|
676 val cgoal = cterm_of @{theory} goal |
|
677 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
|
678 val cgoal3 = Thm.rhs_of (MetaSimplifier.rewrite true @{thms QUOT_TYPE_I_fset.thm10} cgoal2) |
|
679 *} |
|
680 |
|
681 (* It is the same, but we need a name for it. *) |
|
682 prove zzz : {* Thm.term_of cgoal3 *} |
|
683 apply (tactic {* transconv_fset_tac' @{context} *}) |
|
684 done |
|
685 |
|
686 (*lemma zzz' : |
|
687 "(REP_fset (INSERT a (INSERT a (ABS_fset xs))) \<approx> REP_fset (INSERT a (ABS_fset xs)))" |
|
688 using list_eq.intros(4) by (simp only: zzz) |
|
689 |
|
690 thm QUOT_TYPE_I_fset.REPS_same |
|
691 ML {* val zzz'' = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} @{thm zzz'} *} |
|
692 *) |
|
693 |
|
694 thm list_eq.intros(5) |
|
695 (* prove {* build_repabs_goal @{context} (atomize_thm @{thm list_eq.intros(5)}) consts @{typ "'a list"} @{typ "'a fset"} *} *) |
|
696 ML {* |
|
697 val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list_eq.intros(5)})) |
|
698 val goal = build_repabs_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} |
|
699 val cgoal = cterm_of @{theory} goal |
|
700 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal) |
|
701 *} |
|
702 prove {* Thm.term_of cgoal2 *} |
|
703 apply (tactic {* transconv_fset_tac' @{context} *}) |
|
704 done |
|
705 |
621 |
706 ML {* |
622 ML {* |
707 fun lift_theorem_fset_aux thm lthy = |
623 fun lift_theorem_fset_aux thm lthy = |
708 let |
624 let |
709 val ((_, [novars]), lthy2) = Variable.import true [thm] lthy; |
625 val ((_, [novars]), lthy2) = Variable.import true [thm] lthy; |