772 ML {* (* Test: *) @{thm IN_def}; unabs_def @{context} @{thm IN_def} *} |
772 ML {* (* Test: *) @{thm IN_def}; unabs_def @{context} @{thm IN_def} *} |
773 |
773 |
774 ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def} *} |
774 ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def} *} |
775 ML {* val fset_defs_sym = map (fn t => symmetric (unabs_def @{context} t)) fset_defs *} |
775 ML {* val fset_defs_sym = map (fn t => symmetric (unabs_def @{context} t)) fset_defs *} |
776 |
776 |
777 (* Has all the theorems about fset plugged in. These should be parameters to the tactic *) |
|
778 ML {* |
|
779 fun transconv_fset_tac' ctxt = |
|
780 REPEAT_ALL_NEW (FIRST' [ |
|
781 rtac @{thm list_eq_refl}, |
|
782 rtac @{thm cons_preserves}, |
|
783 rtac @{thm mem_respects}, |
|
784 rtac @{thm card1_rsp}, |
|
785 rtac @{thm QUOT_TYPE_I_fset.R_trans2}, |
|
786 CHANGED o (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms QUOT_TYPE_I_fset.REP_ABS_rsp})), |
|
787 Cong_Tac.cong_tac @{thm cong}, |
|
788 rtac @{thm ext} |
|
789 ]) |
|
790 *} |
|
791 |
|
792 ML {* |
|
793 val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m1})) |
|
794 val goal = build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs |
|
795 val cgoal = cterm_of @{theory} goal |
|
796 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
|
797 *} |
|
798 |
|
799 (*notation ( output) "prop" ("#_" [1000] 1000) *) |
|
800 notation ( output) "Trueprop" ("#_" [1000] 1000) |
|
801 |
|
802 lemma atomize_eqv[atomize]: |
777 lemma atomize_eqv[atomize]: |
803 shows "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)" |
778 shows "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)" |
804 proof |
779 proof |
805 assume "A \<equiv> B" |
780 assume "A \<equiv> B" |
806 then show "Trueprop A \<equiv> Trueprop B" by unfold |
781 then show "Trueprop A \<equiv> Trueprop B" by unfold |
817 then show "A = B" using * by auto |
792 then show "A = B" using * by auto |
818 qed |
793 qed |
819 then show "A \<equiv> B" by (rule eq_reflection) |
794 then show "A \<equiv> B" by (rule eq_reflection) |
820 qed |
795 qed |
821 |
796 |
|
797 (* Has all the theorems about fset plugged in. These should be parameters to the tactic *) |
|
798 ML {* |
|
799 fun transconv_fset_tac' ctxt = |
|
800 (LocalDefs.unfold_tac @{context} fset_defs) THEN |
|
801 ObjectLogic.full_atomize_tac 1 THEN |
|
802 REPEAT_ALL_NEW (FIRST' [ |
|
803 rtac @{thm list_eq_refl}, |
|
804 rtac @{thm cons_preserves}, |
|
805 rtac @{thm mem_respects}, |
|
806 rtac @{thm card1_rsp}, |
|
807 rtac @{thm QUOT_TYPE_I_fset.R_trans2}, |
|
808 CHANGED o (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms QUOT_TYPE_I_fset.REP_ABS_rsp})), |
|
809 Cong_Tac.cong_tac @{thm cong}, |
|
810 rtac @{thm ext} |
|
811 ]) 1 |
|
812 *} |
|
813 |
|
814 ML {* |
|
815 val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m1})) |
|
816 val goal = build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs |
|
817 val cgoal = cterm_of @{theory} goal |
|
818 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
|
819 *} |
|
820 |
|
821 (*notation ( output) "prop" ("#_" [1000] 1000) *) |
|
822 notation ( output) "Trueprop" ("#_" [1000] 1000) |
|
823 |
|
824 |
822 prove {* (Thm.term_of cgoal2) *} |
825 prove {* (Thm.term_of cgoal2) *} |
823 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
826 apply (tactic {* transconv_fset_tac' @{context} *}) |
824 apply (atomize(full)) |
|
825 apply (tactic {* transconv_fset_tac' @{context} 1 *}) |
|
826 done |
827 done |
827 |
828 |
828 thm length_append (* Not true but worth checking that the goal is correct *) |
829 thm length_append (* Not true but worth checking that the goal is correct *) |
829 ML {* |
830 ML {* |
830 val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm length_append})) |
831 val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm length_append})) |
831 val goal = build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs |
832 val goal = build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs |
832 val cgoal = cterm_of @{theory} goal |
833 val cgoal = cterm_of @{theory} goal |
833 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
834 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
834 *} |
835 *} |
835 prove {* Thm.term_of cgoal2 *} |
836 prove {* Thm.term_of cgoal2 *} |
836 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
837 apply (tactic {* transconv_fset_tac' @{context} *}) |
837 apply (atomize(full)) |
|
838 apply (tactic {* transconv_fset_tac' @{context} 1 *}) |
|
839 sorry |
838 sorry |
840 |
839 |
841 thm m2 |
840 thm m2 |
842 ML {* |
841 ML {* |
843 val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m2})) |
842 val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m2})) |
844 val goal = build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs |
843 val goal = build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs |
845 val cgoal = cterm_of @{theory} goal |
844 val cgoal = cterm_of @{theory} goal |
846 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
845 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
847 *} |
846 *} |
848 prove {* Thm.term_of cgoal2 *} |
847 prove {* Thm.term_of cgoal2 *} |
849 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
848 apply (tactic {* transconv_fset_tac' @{context} *}) |
850 apply (atomize(full)) |
|
851 apply (tactic {* transconv_fset_tac' @{context} 1 *}) |
|
852 done |
849 done |
853 |
850 |
854 thm list_eq.intros(4) |
851 thm list_eq.intros(4) |
855 ML {* |
852 ML {* |
856 val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list_eq.intros(4)})) |
853 val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list_eq.intros(4)})) |
860 val cgoal3 = Thm.rhs_of (MetaSimplifier.rewrite true @{thms QUOT_TYPE_I_fset.thm10} cgoal2) |
857 val cgoal3 = Thm.rhs_of (MetaSimplifier.rewrite true @{thms QUOT_TYPE_I_fset.thm10} cgoal2) |
861 *} |
858 *} |
862 |
859 |
863 (* It is the same, but we need a name for it. *) |
860 (* It is the same, but we need a name for it. *) |
864 prove zzz : {* Thm.term_of cgoal3 *} |
861 prove zzz : {* Thm.term_of cgoal3 *} |
865 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
862 apply (tactic {* transconv_fset_tac' @{context} *}) |
866 apply (atomize(full)) |
|
867 apply (tactic {* transconv_fset_tac' @{context} 1 *}) |
|
868 done |
863 done |
869 |
864 |
870 lemma zzz' : |
865 lemma zzz' : |
871 "(REP_fset (INSERT a (INSERT a (ABS_fset xs))) \<approx> REP_fset (INSERT a (ABS_fset xs)))" |
866 "(REP_fset (INSERT a (INSERT a (ABS_fset xs))) \<approx> REP_fset (INSERT a (ABS_fset xs)))" |
872 using list_eq.intros(4) by (simp only: zzz) |
867 using list_eq.intros(4) by (simp only: zzz) |
873 |
868 |
874 thm QUOT_TYPE_I_fset.REPS_same |
869 thm QUOT_TYPE_I_fset.REPS_same |
875 ML {* val zzz'' = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} @{thm zzz'} *} |
870 ML {* val zzz'' = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} @{thm zzz'} *} |
876 |
871 |
877 |
|
878 thm list_eq.intros(5) |
872 thm list_eq.intros(5) |
879 ML {* |
873 ML {* |
880 val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list_eq.intros(5)})) |
874 val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list_eq.intros(5)})) |
881 val goal = build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs |
875 val goal = build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs |
882 *} |
876 val cgoal = cterm_of @{theory} goal |
883 ML {* |
|
884 val cgoal = |
|
885 Toplevel.program (fn () => |
|
886 cterm_of @{theory} goal |
|
887 ) |
|
888 *} |
|
889 ML {* |
|
890 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal) |
877 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal) |
891 *} |
878 *} |
892 prove {* Thm.term_of cgoal2 *} |
879 prove {* Thm.term_of cgoal2 *} |
893 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
880 apply (tactic {* transconv_fset_tac' @{context} *}) |
894 apply (atomize(full)) |
|
895 apply (tactic {* transconv_fset_tac' @{context} 1 *}) |
|
896 done |
881 done |
897 |
882 |
898 section {* handling quantifiers - regularize *} |
883 section {* handling quantifiers - regularize *} |
899 |
884 |
900 text {* tyRel takes a type and builds a relation that a quantifier over this |
885 text {* tyRel takes a type and builds a relation that a quantifier over this |