75 apply(subst thm11[symmetric]) |
75 apply(subst thm11[symmetric]) |
76 apply(simp add: equiv[simplified EQUIV_def]) |
76 apply(simp add: equiv[simplified EQUIV_def]) |
77 done |
77 done |
78 |
78 |
79 lemma R_trans: |
79 lemma R_trans: |
80 assumes ab: "R a b" |
80 assumes ab: "R a b" |
81 and bc: "R b c" |
81 and bc: "R b c" |
82 shows "R a c" |
82 shows "R a c" |
83 proof - |
83 proof - |
84 have tr: "TRANS R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp |
84 have tr: "TRANS R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp |
85 moreover have ab: "R a b" by fact |
85 moreover have ab: "R a b" by fact |
86 moreover have bc: "R b c" by fact |
86 moreover have bc: "R b c" by fact |
87 ultimately show "R a c" unfolding TRANS_def by blast |
87 ultimately show "R a c" unfolding TRANS_def by blast |
88 qed |
88 qed |
89 |
89 |
90 lemma R_sym: |
90 lemma R_sym: |
91 assumes ab: "R a b" |
91 assumes ab: "R a b" |
92 shows "R b a" |
92 shows "R b a" |
93 proof - |
93 proof - |
94 have re: "SYM R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp |
94 have re: "SYM R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp |
95 then show "R b a" using ab unfolding SYM_def by blast |
95 then show "R b a" using ab unfolding SYM_def by blast |
96 qed |
96 qed |
97 |
97 |
98 lemma R_trans2: |
98 lemma R_trans2: |
99 assumes ac: "R a c" |
99 assumes ac: "R a c" |
100 and bd: "R b d" |
100 and bd: "R b d" |
101 shows "R a b = R c d" |
101 shows "R a b = R c d" |
102 proof |
102 proof |
103 assume "R a b" |
103 assume "R a b" |
104 then have "R b a" using R_sym by blast |
104 then have "R b a" using R_sym by blast |
113 then show "R a b" using R_sym by blast |
113 then show "R a b" using R_sym by blast |
114 qed |
114 qed |
115 |
115 |
116 lemma REPS_same: |
116 lemma REPS_same: |
117 shows "R (REP a) (REP b) \<equiv> (a = b)" |
117 shows "R (REP a) (REP b) \<equiv> (a = b)" |
118 apply (rule eq_reflection) |
118 proof - |
119 proof |
119 have "R (REP a) (REP b) = (a = b)" |
120 assume as: "R (REP a) (REP b)" |
120 proof |
121 from rep_prop |
121 assume as: "R (REP a) (REP b)" |
122 obtain x y |
122 from rep_prop |
123 where eqs: "Rep a = R x" "Rep b = R y" by blast |
123 obtain x y |
124 from eqs have "R (Eps (R x)) (Eps (R y))" using as unfolding REP_def by simp |
124 where eqs: "Rep a = R x" "Rep b = R y" by blast |
125 then have "R x (Eps (R y))" using lem9 by simp |
125 from eqs have "R (Eps (R x)) (Eps (R y))" using as unfolding REP_def by simp |
126 then have "R (Eps (R y)) x" using R_sym by blast |
126 then have "R x (Eps (R y))" using lem9 by simp |
127 then have "R y x" using lem9 by simp |
127 then have "R (Eps (R y)) x" using R_sym by blast |
128 then have "R x y" using R_sym by blast |
128 then have "R y x" using lem9 by simp |
129 then have "ABS x = ABS y" using thm11 by simp |
129 then have "R x y" using R_sym by blast |
130 then have "Abs (Rep a) = Abs (Rep b)" using eqs unfolding ABS_def by simp |
130 then have "ABS x = ABS y" using thm11 by simp |
131 then show "a = b" using rep_inverse by simp |
131 then have "Abs (Rep a) = Abs (Rep b)" using eqs unfolding ABS_def by simp |
132 next |
132 then show "a = b" using rep_inverse by simp |
133 assume ab: "a = b" |
133 next |
134 have "REFL R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp |
134 assume ab: "a = b" |
135 then show "R (REP a) (REP b)" unfolding REFL_def using ab by auto |
135 have "REFL R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp |
|
136 then show "R (REP a) (REP b)" unfolding REFL_def using ab by auto |
|
137 qed |
|
138 then show "R (REP a) (REP b) \<equiv> (a = b)" by simp |
136 qed |
139 qed |
137 |
140 |
138 end |
141 end |
139 |
142 |
140 section {* type definition for the quotient type *} |
143 section {* type definition for the quotient type *} |
674 lemma mem_cons: |
677 lemma mem_cons: |
675 fixes x :: "'a" |
678 fixes x :: "'a" |
676 fixes xs :: "'a list" |
679 fixes xs :: "'a list" |
677 assumes a : "x memb xs" |
680 assumes a : "x memb xs" |
678 shows "x # xs \<approx> xs" |
681 shows "x # xs \<approx> xs" |
679 using a apply (induct xs) |
682 using a |
680 apply (simp_all) |
683 apply (induct xs) |
681 apply (meson) |
684 apply (auto intro: list_eq.intros) |
682 apply (simp_all add: list_eq.intros(4)) |
685 done |
683 proof - |
|
684 fix a :: "'a" |
|
685 fix xs :: "'a list" |
|
686 assume a1 : "x # xs \<approx> xs" |
|
687 assume a2 : "x memb xs" |
|
688 have a3 : "x # a # xs \<approx> a # x # xs" using list_eq.intros(1)[of "x"] by blast |
|
689 have a4 : "a # x # xs \<approx> a # xs" using a1 list_eq.intros(5)[of "x # xs" "xs"] by simp |
|
690 then show "x # a # xs \<approx> a # xs" using a3 list_eq.intros(6) by blast |
|
691 qed |
|
692 |
686 |
693 lemma card1_suc: |
687 lemma card1_suc: |
694 fixes xs :: "'a list" |
688 fixes xs :: "'a list" |
695 fixes n :: "nat" |
689 fixes n :: "nat" |
696 assumes c: "card1 xs = Suc n" |
690 assumes c: "card1 xs = Suc n" |
697 shows "\<exists>a ys. ~(a memb ys) \<and> xs \<approx> (a # ys)" |
691 shows "\<exists>a ys. ~(a memb ys) \<and> xs \<approx> (a # ys)" |
698 using c apply (induct xs) |
692 using c |
699 apply (simp) |
693 apply(induct xs) |
700 (* apply (rule allI)*) |
694 apply (metis Suc_neq_Zero card1_0) |
701 proof - |
695 apply (metis QUOT_TYPE_I_fset.R_trans QuotMain.card1_cons list_eq_sym mem_cons) |
702 fix a :: "'a" |
696 done |
703 fix xs :: "'a list" |
|
704 fix n :: "nat" |
|
705 assume a1: "card1 xs = Suc n \<Longrightarrow> \<exists>a ys. \<not> a memb ys \<and> xs \<approx> a # ys" |
|
706 assume a2: "card1 (a # xs) = Suc n" |
|
707 from a1 a2 show "\<exists>aa ys. \<not> aa memb ys \<and> a # xs \<approx> aa # ys" |
|
708 apply - |
|
709 apply (rule True_or_False [of "a memb xs", THEN disjE]) |
|
710 apply (simp_all add: card1_cons if_True simp_thms) |
|
711 proof - |
|
712 assume a1: "\<exists>a ys. \<not> a memb ys \<and> xs \<approx> a # ys" |
|
713 assume a2: "card1 xs = Suc n" |
|
714 assume a3: "a memb xs" |
|
715 from a1 obtain b ys where a5: "\<not> b memb ys \<and> xs \<approx> b # ys" by blast |
|
716 from a2 a3 a5 show "\<exists>aa ys. \<not> aa memb ys \<and> a # xs \<approx> aa # ys" |
|
717 apply - |
|
718 apply (rule_tac x = "b" in exI) |
|
719 apply (rule_tac x = "ys" in exI) |
|
720 apply (simp_all) |
|
721 proof - |
|
722 assume a1: "a memb xs" |
|
723 assume a2: "\<not> b memb ys \<and> xs \<approx> b # ys" |
|
724 then have a3: "xs \<approx> b # ys" by simp |
|
725 have "a # xs \<approx> xs" using a1 mem_cons[of "a" "xs"] by simp |
|
726 then show "a # xs \<approx> b # ys" using a3 list_eq.intros(6) by blast |
|
727 qed |
|
728 next |
|
729 assume a2: "\<not> a memb xs" |
|
730 from a2 show "\<exists>aa ys. \<not> aa memb ys \<and> a # xs \<approx> aa # ys" |
|
731 apply - |
|
732 apply (rule_tac x = "a" in exI) |
|
733 apply (rule_tac x = "xs" in exI) |
|
734 apply (simp) |
|
735 apply (rule list_eq_sym) |
|
736 done |
|
737 qed |
|
738 qed |
|
739 |
697 |
740 lemma cons_preserves: |
698 lemma cons_preserves: |
741 fixes z |
699 fixes z |
742 assumes a: "xs \<approx> ys" |
700 assumes a: "xs \<approx> ys" |
743 shows "(z # xs) \<approx> (z # ys)" |
701 shows "(z # xs) \<approx> (z # ys)" |
870 let |
826 let |
871 val _ = writeln ("Maybe: " ^ Syntax.string_of_term @{context} t) |
827 val _ = writeln ("Maybe: " ^ Syntax.string_of_term @{context} t) |
872 in |
828 in |
873 if type_of t = lifted_type then mk_rep_abs t else t |
829 if type_of t = lifted_type then mk_rep_abs t else t |
874 end |
830 end |
875 (* handle TYPE _ => t*) |
831 handle TYPE _ => t |
876 fun build_aux (Abs (s, t, tr)) = |
832 fun build_aux (Abs (s, t, tr)) = (Abs (s, t, build_aux tr)) |
877 let |
|
878 val [(fresh_s, _)] = Variable.variant_frees @{context} [] [(s, ())]; |
|
879 val newv = Free (fresh_s, t); |
|
880 val str = subst_bound (newv, tr); |
|
881 val rec_term = build_aux str; |
|
882 val bound_term = lambda newv rec_term |
|
883 in |
|
884 bound_term |
|
885 end |
|
886 | build_aux (f $ a) = |
833 | build_aux (f $ a) = |
887 let |
834 let |
888 val (f, args) = strip_comb (f $ a) |
835 val (f, args) = strip_comb (f $ a) |
889 val _ = writeln (Syntax.string_of_term @{context} f) |
836 val _ = writeln (Syntax.string_of_term @{context} f) |
890 in |
837 in |
896 val concl2 = term_of (#prop (crep_thm thm)) |
843 val concl2 = term_of (#prop (crep_thm thm)) |
897 in |
844 in |
898 Logic.mk_equals ((build_aux concl2), concl2) |
845 Logic.mk_equals ((build_aux concl2), concl2) |
899 end *} |
846 end *} |
900 |
847 |
|
848 ML {* val emptyt = symmetric (unlam_def @{context} @{thm EMPTY_def}) *} |
|
849 ML {* val in_t = symmetric (unlam_def @{context} @{thm IN_def}) *} |
|
850 ML {* val uniont = symmetric (unlam_def @{context} @{thm UNION_def}) *} |
|
851 ML {* val cardt = symmetric (unlam_def @{context} @{thm card_def}) *} |
|
852 ML {* val insertt = symmetric (unlam_def @{context} @{thm INSERT_def}) *} |
901 ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def} *} |
853 ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def} *} |
902 ML {* val fset_defs_sym = map (fn t => symmetric (unlam_def @{context} t)) fset_defs *} |
854 ML {* val fset_defs_sym = [emptyt, in_t, uniont, cardt, insertt] *} |
903 |
855 |
904 ML {* |
856 ML {* |
905 fun dest_cbinop t = |
857 fun dest_cbinop t = |
906 let |
858 let |
907 val (t2, rhs) = Thm.dest_comb t; |
859 val (t2, rhs) = Thm.dest_comb t; |
908 val (bop, lhs) = Thm.dest_comb t2; |
860 val (bop, lhs) = Thm.dest_comb t2; |
909 in |
861 in |
910 (bop, (lhs, rhs)) |
862 (bop, (lhs, rhs)) |
911 end |
863 end |
912 *} |
864 *} |
|
865 |
913 ML {* |
866 ML {* |
914 fun dest_ceq t = |
867 fun dest_ceq t = |
915 let |
868 let |
916 val (bop, pair) = dest_cbinop t; |
869 val (bop, pair) = dest_cbinop t; |
917 val (bop_s, _) = Term.dest_Const (Thm.term_of bop); |
870 val (bop_s, _) = Term.dest_Const (Thm.term_of bop); |
918 in |
871 in |
919 if bop_s = "op =" then pair else (raise CTERM ("Not an equality", [t])) |
872 if bop_s = "op =" then pair else (raise CTERM ("Not an equality", [t])) |
920 end |
873 end |
921 *} |
874 *} |
|
875 |
922 ML Thm.instantiate |
876 ML Thm.instantiate |
923 ML {*@{thm arg_cong2}*} |
877 ML {*@{thm arg_cong2}*} |
924 ML {*@{thm arg_cong2[of _ _ _ _ "op ="]} *} |
878 ML {*@{thm arg_cong2[of _ _ _ _ "op ="]} *} |
925 ML {* val cT = @{cpat "op ="} |> Thm.ctyp_of_term |> Thm.dest_ctyp |> hd *} |
879 ML {* val cT = @{cpat "op ="} |> Thm.ctyp_of_term |> Thm.dest_ctyp |> hd *} |
926 ML {* |
880 ML {* |
927 Toplevel.program (fn () => |
881 Toplevel.program (fn () => |
928 Drule.instantiate' [SOME cT, SOME cT, SOME @{ctyp bool}] [NONE, NONE, NONE, NONE, SOME (@{cpat "op ="})] @{thm arg_cong2} |
882 Drule.instantiate' [SOME cT,SOME cT,SOME @{ctyp bool}] [NONE,NONE,NONE,NONE,SOME (@{cpat "op ="})] @{thm arg_cong2} |
929 ) |
883 ) |
930 *} |
884 *} |
931 |
885 |
932 ML {* |
886 ML {* |
933 fun split_binop_conv t = |
887 fun foo_conv t = |
934 let |
888 let |
935 val _ = tracing (Syntax.string_of_term @{context} (term_of t)) |
|
936 val (lhs, rhs) = dest_ceq t; |
889 val (lhs, rhs) = dest_ceq t; |
937 val (bop, _) = dest_cbinop lhs; |
890 val (bop, _) = dest_cbinop lhs; |
938 val [clT, cr2] = bop |> Thm.ctyp_of_term |> Thm.dest_ctyp; |
891 val [clT, cr2] = bop |> Thm.ctyp_of_term |> Thm.dest_ctyp; |
939 val [cmT, crT] = Thm.dest_ctyp cr2; |
892 val [cmT, crT] = Thm.dest_ctyp cr2; |
940 in |
893 in |
941 Drule.instantiate' [SOME clT, SOME cmT, SOME crT] [NONE, NONE, NONE, NONE, SOME bop] @{thm arg_cong2} |
894 Drule.instantiate' [SOME clT,SOME cmT,SOME crT] [NONE,NONE,NONE,NONE,SOME bop] @{thm arg_cong2} |
942 end |
895 end |
943 *} |
896 *} |
944 |
897 |
945 ML {* |
898 ML {* |
946 fun split_arg_conv t = |
899 fun foo_tac n thm = |
947 let |
|
948 val (lhs, rhs) = dest_ceq t; |
|
949 val (lop, larg) = Thm.dest_comb lhs; |
|
950 val [caT, crT] = lop |> Thm.ctyp_of_term |> Thm.dest_ctyp; |
|
951 in |
|
952 Drule.instantiate' [SOME caT, SOME crT] [NONE, NONE, SOME lop] @{thm arg_cong} |
|
953 end |
|
954 *} |
|
955 |
|
956 ML {* |
|
957 fun split_binop_tac n thm = |
|
958 let |
900 let |
959 val concl = Thm.cprem_of thm n; |
901 val concl = Thm.cprem_of thm n; |
960 val (_, cconcl) = Thm.dest_comb concl; |
902 val (_, cconcl) = Thm.dest_comb concl; |
961 val rewr = split_binop_conv cconcl; |
903 val rewr = foo_conv cconcl; |
962 in |
904 (* val _ = tracing (Display.string_of_thm @{context} rewr) |
963 rtac rewr n thm |
905 val _ = tracing (Display.string_of_thm @{context} thm)*) |
964 end |
|
965 handle CTERM _ => Seq.empty |
|
966 *} |
|
967 |
|
968 ML {* |
|
969 fun split_arg_tac n thm = |
|
970 let |
|
971 val concl = Thm.cprem_of thm n; |
|
972 val (_, cconcl) = Thm.dest_comb concl; |
|
973 val rewr = split_arg_conv cconcl; |
|
974 in |
906 in |
975 rtac rewr n thm |
907 rtac rewr n thm |
976 end |
908 end |
977 handle CTERM _ => Seq.empty |
909 handle CTERM _ => Seq.empty |
978 *} |
910 *} |
988 REPEAT_ALL_NEW (FIRST' [ |
920 REPEAT_ALL_NEW (FIRST' [ |
989 rtac @{thm trueprop_cong}, |
921 rtac @{thm trueprop_cong}, |
990 rtac @{thm list_eq_sym}, |
922 rtac @{thm list_eq_sym}, |
991 rtac @{thm cons_preserves}, |
923 rtac @{thm cons_preserves}, |
992 rtac @{thm mem_respects}, |
924 rtac @{thm mem_respects}, |
993 rtac @{thm card1_rsp}, |
|
994 rtac @{thm QUOT_TYPE_I_fset.R_trans2}, |
925 rtac @{thm QUOT_TYPE_I_fset.R_trans2}, |
995 CHANGED o (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms QUOT_TYPE_I_fset.REP_ABS_rsp})), |
926 CHANGED o (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms QUOT_TYPE_I_fset.REP_ABS_rsp})), |
996 DatatypeAux.cong_tac, |
927 foo_tac, |
997 rtac @{thm ext}, |
|
998 (* rtac @{thm eq_reflection}*) |
|
999 CHANGED o (ObjectLogic.full_atomize_tac) |
928 CHANGED o (ObjectLogic.full_atomize_tac) |
1000 ]) |
929 ]) |
1001 *} |
930 *} |
1002 |
931 |
1003 ML {* |
932 ML {* |
1004 val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m1})) |
933 val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm m1})) |
1005 val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs |
934 val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs |
1006 val cgoal = cterm_of @{theory} goal |
935 val cgoal = cterm_of @{theory} goal |
1007 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
936 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
1008 *} |
937 *} |
1009 |
938 |
1065 using list_eq.intros(4) by (simp only: zzz) |
994 using list_eq.intros(4) by (simp only: zzz) |
1066 |
995 |
1067 thm QUOT_TYPE_I_fset.REPS_same |
996 thm QUOT_TYPE_I_fset.REPS_same |
1068 ML {* val zzz'' = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} @{thm zzz'} *} |
997 ML {* val zzz'' = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} @{thm zzz'} *} |
1069 |
998 |
|
999 ML Drule.instantiate' |
|
1000 ML {* zzz'' *} |
|
1001 text {* |
|
1002 A variable export will still be necessary in the end, but this is already the final theorem. |
|
1003 *} |
|
1004 ML {* |
|
1005 Toplevel.program (fn () => |
|
1006 MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.thm10} ( |
|
1007 Drule.instantiate' [] [NONE,SOME (@{cpat "REP_fset x"})] zzz'' |
|
1008 ) |
|
1009 ) |
|
1010 *} |
|
1011 |
|
1012 |
1070 thm list_eq.intros(5) |
1013 thm list_eq.intros(5) |
1071 ML {* |
1014 ML {* |
1072 val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list_eq.intros(5)})) |
1015 val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm list_eq.intros(5)})) |
1073 val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs |
1016 val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs |
1074 *} |
1017 *} |
1075 ML {* |
1018 ML {* |
1076 val cgoal = |
1019 val cgoal = |
1077 Toplevel.program (fn () => |
1020 Toplevel.program (fn () => |
1078 cterm_of @{theory} goal |
1021 cterm_of @{theory} goal |
1079 ) |
1022 ) |
1080 *} |
1023 *} |
1081 ML {* |
1024 ML {* |
1082 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal) |
1025 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
1083 *} |
1026 *} |
1084 prove {* Thm.term_of cgoal2 *} |
1027 prove {* Thm.term_of cgoal2 *} |
1085 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
1028 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
1086 apply (tactic {* foo_tac' @{context} 1 *}) |
1029 apply (tactic {* foo_tac' @{context} 1 *}) |
1087 done |
1030 done |
1088 |
1031 |
1089 thm list.induct |
1032 thm list.induct |
1090 |
1033 ML {* Logic.list_implies ((Thm.prems_of @{thm list.induct}), (Thm.concl_of @{thm list.induct})) *} |
1091 ML {* |
1034 |
1092 val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list.induct})) |
1035 ML {* |
|
1036 val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm list.induct})) |
1093 *} |
1037 *} |
1094 ML {* |
1038 ML {* |
1095 val goal = |
1039 val goal = |
1096 Toplevel.program (fn () => |
1040 Toplevel.program (fn () => |
1097 build_goal m1_novars consts @{typ "'a list"} mk_rep_abs |
1041 build_goal m1_novars consts @{typ "'a list"} mk_rep_abs |
1098 ) |
1042 ) |
1099 *} |
1043 *} |
1100 ML {* |
1044 ML {* |
1101 val cgoal = cterm_of @{theory} goal |
1045 val cgoal = cterm_of @{theory} goal |
1102 *} |
1046 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
1103 ML {* |
1047 *} |
1104 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal) |
1048 ML fset_defs_sym |
1105 *} |
|
1106 |
|
1107 prove {* (Thm.term_of cgoal2) *} |
1049 prove {* (Thm.term_of cgoal2) *} |
1108 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
1050 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
1109 apply (tactic {* foo_tac' @{context} 1 *}) |
1051 apply (atomize(full)) |
|
1052 apply (rule_tac trueprop_cong) |
|
1053 apply (atomize(full)) |
|
1054 apply (tactic {* foo_tac' @{context} 1 *}) |
|
1055 apply (rule_tac f = "P" in arg_cong) |
1110 sorry |
1056 sorry |
1111 |
1057 |
1112 ML {* |
|
1113 fun lift_theorem_fset_aux thm lthy = |
|
1114 let |
|
1115 val ((_, [novars]), lthy2) = Variable.import true [thm] lthy; |
|
1116 val goal = build_goal novars consts @{typ "'a list"} mk_rep_abs; |
|
1117 val cgoal = cterm_of @{theory} goal; |
|
1118 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal); |
|
1119 val tac = (LocalDefs.unfold_tac @{context} fset_defs) THEN (foo_tac' @{context}) 1; |
|
1120 val cthm = Goal.prove_internal [] cgoal2 (fn _ => tac); |
|
1121 val nthm = MetaSimplifier.rewrite_rule [symmetric cthm] (snd (no_vars (Context.Theory @{theory}, thm))) |
|
1122 val nthm2 = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same QUOT_TYPE_I_fset.thm10} nthm; |
|
1123 val [nthm3] = ProofContext.export lthy2 lthy [nthm2] |
|
1124 in |
|
1125 nthm3 |
|
1126 end |
|
1127 *} |
|
1128 |
|
1129 ML {* lift_theorem_fset_aux @{thm m1} @{context} *} |
|
1130 |
|
1131 ML {* |
|
1132 fun lift_theorem_fset name thm lthy = |
|
1133 let |
|
1134 val lifted_thm = lift_theorem_fset_aux thm lthy; |
|
1135 val (_, lthy2) = note_thm (name, lifted_thm) lthy; |
|
1136 in |
|
1137 lthy2 |
|
1138 end; |
|
1139 *} |
|
1140 |
|
1141 local_setup {* lift_theorem_fset @{binding "m1_lift"} @{thm m1} *} |
|
1142 local_setup {* lift_theorem_fset @{binding "leqi4_lift"} @{thm list_eq.intros(4)} *} |
|
1143 local_setup {* lift_theorem_fset @{binding "leqi5_lift"} @{thm list_eq.intros(5)} *} |
|
1144 local_setup {* lift_theorem_fset @{binding "m2_lift"} @{thm m2} *} |
|
1145 |
|
1146 thm m1_lift |
|
1147 thm leqi4_lift |
|
1148 thm leqi5_lift |
|
1149 thm m2_lift |
|
1150 |
|
1151 ML Drule.instantiate' |
|
1152 text {* |
|
1153 We lost the schematic variable again :(. |
|
1154 Another variable export will still be necessary... |
|
1155 *} |
|
1156 ML {* |
|
1157 Toplevel.program (fn () => |
|
1158 MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.thm10} ( |
|
1159 Drule.instantiate' [] [NONE, NONE, SOME (@{cpat "REP_fset x"})] @{thm m2_lift} |
|
1160 ) |
|
1161 ) |
|
1162 *} |
|
1163 |
|
1164 |
|
1165 |
|
1166 |
|
1167 ML {* MRS *} |
|
1168 thm card1_suc |
1058 thm card1_suc |
1169 |
1059 |
1170 ML {* |
1060 ML {* |
1171 val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm card1_suc})) |
1061 val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm card1_suc})) |
1172 *} |
1062 *} |
1173 ML {* |
1063 ML {* |
1174 val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs |
1064 val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs |
1175 *} |
1065 *} |
1176 ML {* |
1066 ML {* |
1177 val cgoal = cterm_of @{theory} goal |
1067 val cgoal = cterm_of @{theory} goal |
1178 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal) |
1068 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
1179 *} |
1069 *} |
1180 ML {* @{term "\<exists>x. P x"} *} |
|
1181 prove {* (Thm.term_of cgoal2) *} |
1070 prove {* (Thm.term_of cgoal2) *} |
1182 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
1071 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
1183 apply (tactic {* foo_tac' @{context} 1 *}) |
1072 |
1184 done |
|
1185 |
1073 |
1186 |
1074 |
1187 (* |
1075 (* |
1188 datatype obj1 = |
1076 datatype obj1 = |
1189 OVAR1 "string" |
1077 OVAR1 "string" |