829 @{const_name "card1"}] |
829 @{const_name "card1"}] |
830 *} |
830 *} |
831 |
831 |
832 ML {* val qty = @{typ "'a fset"} *} |
832 ML {* val qty = @{typ "'a fset"} *} |
833 ML {* val tt = Type ("fun", [Type ("fun", [qty, @{typ "prop"}]), @{typ "prop"}]) *} |
833 ML {* val tt = Type ("fun", [Type ("fun", [qty, @{typ "prop"}]), @{typ "prop"}]) *} |
834 ML {* val fall = Const(@{const_name all}, tt) *} |
834 ML {* val fall = Const(@{const_name all}, dummyT) *} |
835 |
835 |
836 ML {* |
836 ML {* Syntax.check_term *} |
837 fun build_goal ctxt thm constructors rty qty mk_rep mk_abs = |
837 |
|
838 ML {* |
|
839 fun build_goal_term ctxt thm constructors rty qty mk_rep mk_abs = |
838 let |
840 let |
839 fun mk_rep_abs x = mk_rep (mk_abs x); |
841 fun mk_rep_abs x = mk_rep (mk_abs x); |
840 |
842 |
841 fun is_constructor (Const (x, _)) = member (op =) constructors x |
843 fun is_constructor (Const (x, _)) = member (op =) constructors x |
842 | is_constructor _ = false; |
844 | is_constructor _ = false; |
848 if fastype_of t = rty then mk_rep_abs t else t |
850 if fastype_of t = rty then mk_rep_abs t else t |
849 end; |
851 end; |
850 |
852 |
851 fun is_all (Const ("all", Type("fun", [Type("fun", [ty, _]), _]))) = ty = rty |
853 fun is_all (Const ("all", Type("fun", [Type("fun", [ty, _]), _]))) = ty = rty |
852 | is_all _ = false; |
854 | is_all _ = false; |
|
855 |
|
856 fun is_ex (Const ("Ex", Type("fun", [Type("fun", [ty, _]), _]))) = ty = rty |
|
857 | is_ex _ = false; |
853 |
858 |
854 fun build_aux ctxt1 tm = |
859 fun build_aux ctxt1 tm = |
855 let |
860 let |
856 val (head, args) = Term.strip_comb tm; |
861 val (head, args) = Term.strip_comb tm; |
857 val args' = map (build_aux ctxt1) args; |
862 val args' = map (build_aux ctxt1) args; |
871 val ([x'], ctxt2) = Variable.variant_fixes [x] ctxt1; |
876 val ([x'], ctxt2) = Variable.variant_fixes [x] ctxt1; |
872 val v = Free (x', T); |
877 val v = Free (x', T); |
873 val t' = subst_bound (v, t); |
878 val t' = subst_bound (v, t); |
874 val rec_term = build_aux ctxt2 t'; |
879 val rec_term = build_aux ctxt2 t'; |
875 in Term.lambda_name (x, v) rec_term end |
880 in Term.lambda_name (x, v) rec_term end |
876 | _ => |
881 | _ => (* I assume that we never lift 'prop' since it is not of sort type *) |
877 if is_all head then (* I assume that we never lift 'prop' since it is not of sort type *) |
882 if is_all head then |
878 list_comb (fall, args') |
883 list_comb (Const(@{const_name all}, dummyT), args') |> Syntax.check_term ctxt1 |
|
884 else if is_ex head then |
|
885 list_comb (Const(@{const_name Ex}, dummyT), args') |> Syntax.check_term ctxt1 |
879 else if is_constructor head then |
886 else if is_constructor head then |
880 maybe_mk_rep_abs (list_comb (head, map maybe_mk_rep_abs args')) |
887 maybe_mk_rep_abs (list_comb (head, map maybe_mk_rep_abs args')) |
881 else |
888 else |
882 maybe_mk_rep_abs (list_comb (head, args')) |
889 maybe_mk_rep_abs (list_comb (head, args')) |
883 ) |
890 ) |
884 end; |
891 end; |
885 |
|
886 val concl2 = Thm.prop_of thm; |
|
887 in |
892 in |
888 Logic.mk_equals (build_aux ctxt concl2, concl2) |
893 build_aux ctxt (Thm.prop_of thm) |
889 end |
894 end |
890 *} |
895 *} |
|
896 |
|
897 ML {* |
|
898 fun build_goal ctxt thm cons rty qty mk_rep mk_abs = |
|
899 Logic.mk_equals ((build_goal_term ctxt thm cons rty qty mk_rep mk_abs), (Thm.prop_of thm)) |
|
900 *} |
|
901 |
891 |
902 |
892 ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def} *} |
903 ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def} *} |
893 ML {* val fset_defs_sym = map (fn t => symmetric (unlam_def @{context} t)) fset_defs *} |
904 ML {* val fset_defs_sym = map (fn t => symmetric (unlam_def @{context} t)) fset_defs *} |
894 |
905 |
895 ML {* |
906 ML {* |
989 rtac @{thm mem_respects}, |
1000 rtac @{thm mem_respects}, |
990 rtac @{thm card1_rsp}, |
1001 rtac @{thm card1_rsp}, |
991 rtac @{thm QUOT_TYPE_I_fset.R_trans2}, |
1002 rtac @{thm QUOT_TYPE_I_fset.R_trans2}, |
992 CHANGED o (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms QUOT_TYPE_I_fset.REP_ABS_rsp})), |
1003 CHANGED o (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms QUOT_TYPE_I_fset.REP_ABS_rsp})), |
993 Cong_Tac.cong_tac @{thm cong}, |
1004 Cong_Tac.cong_tac @{thm cong}, |
994 rtac @{thm ext}, |
1005 rtac @{thm ext} |
995 (* rtac @{thm eq_reflection},*) |
1006 (* rtac @{thm eq_reflection},*) |
996 CHANGED o (ObjectLogic.full_atomize_tac) |
1007 (* CHANGED o (ObjectLogic.full_atomize_tac)*) |
997 ]) |
1008 ]) |
998 *} |
1009 *} |
999 |
1010 |
1000 ML {* |
1011 ML {* |
1001 val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m1})) |
1012 val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m1})) |
1039 val cgoal = cterm_of @{theory} goal |
1051 val cgoal = cterm_of @{theory} goal |
1040 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
1052 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
1041 *} |
1053 *} |
1042 prove {* Thm.term_of cgoal2 *} |
1054 prove {* Thm.term_of cgoal2 *} |
1043 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
1055 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
|
1056 apply (atomize(full)) |
1044 apply (tactic {* foo_tac' @{context} 1 *}) |
1057 apply (tactic {* foo_tac' @{context} 1 *}) |
1045 sorry |
1058 sorry |
1046 |
1059 |
1047 thm m2 |
1060 thm m2 |
1048 ML {* |
1061 ML {* |
1051 val cgoal = cterm_of @{theory} goal |
1064 val cgoal = cterm_of @{theory} goal |
1052 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
1065 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
1053 *} |
1066 *} |
1054 prove {* Thm.term_of cgoal2 *} |
1067 prove {* Thm.term_of cgoal2 *} |
1055 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
1068 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
|
1069 apply (atomize(full)) |
1056 apply (tactic {* foo_tac' @{context} 1 *}) |
1070 apply (tactic {* foo_tac' @{context} 1 *}) |
1057 done |
1071 done |
1058 |
1072 |
1059 thm list_eq.intros(4) |
1073 thm list_eq.intros(4) |
1060 ML {* |
1074 ML {* |
1066 *} |
1080 *} |
1067 |
1081 |
1068 (* It is the same, but we need a name for it. *) |
1082 (* It is the same, but we need a name for it. *) |
1069 prove zzz : {* Thm.term_of cgoal3 *} |
1083 prove zzz : {* Thm.term_of cgoal3 *} |
1070 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
1084 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
|
1085 apply (atomize(full)) |
1071 apply (tactic {* foo_tac' @{context} 1 *}) |
1086 apply (tactic {* foo_tac' @{context} 1 *}) |
1072 done |
1087 done |
1073 |
1088 |
1074 lemma zzz' : |
1089 lemma zzz' : |
1075 "(REP_fset (INSERT a (INSERT a (ABS_fset xs))) \<approx> REP_fset (INSERT a (ABS_fset xs)))" |
1090 "(REP_fset (INSERT a (INSERT a (ABS_fset xs))) \<approx> REP_fset (INSERT a (ABS_fset xs)))" |
1093 ML {* |
1108 ML {* |
1094 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal) |
1109 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal) |
1095 *} |
1110 *} |
1096 prove {* Thm.term_of cgoal2 *} |
1111 prove {* Thm.term_of cgoal2 *} |
1097 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
1112 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
|
1113 apply (atomize(full)) |
1098 apply (tactic {* foo_tac' @{context} 1 *}) |
1114 apply (tactic {* foo_tac' @{context} 1 *}) |
1099 done |
1115 done |
1100 |
1116 |
1101 thm list.induct |
1117 thm list.induct |
1102 |
1118 |
1103 ML {* |
1119 ML {* |
1104 val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list.induct})) |
1120 val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list.induct})) |
1105 *} |
1121 *} |
|
1122 |
1106 ML {* |
1123 ML {* |
1107 val goal = |
1124 val goal = |
1108 Toplevel.program (fn () => |
1125 Toplevel.program (fn () => |
1109 build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs |
1126 build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs |
1110 ) |
1127 ) |
1117 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal) |
1134 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal) |
1118 *} |
1135 *} |
1119 |
1136 |
1120 prove {* (Thm.term_of cgoal2) *} |
1137 prove {* (Thm.term_of cgoal2) *} |
1121 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
1138 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
|
1139 apply (atomize(full)) |
1122 apply (tactic {* foo_tac' @{context} 1 *}) |
1140 apply (tactic {* foo_tac' @{context} 1 *}) |
1123 sorry |
1141 sorry |
1124 |
1142 |
1125 ML {* |
1143 ML {* |
1126 fun lift_theorem_fset_aux thm lthy = |
1144 fun lift_theorem_fset_aux thm lthy = |
1127 let |
1145 let |
1128 val ((_, [novars]), lthy2) = Variable.import true [thm] lthy; |
1146 val ((_, [novars]), lthy2) = Variable.import true [thm] lthy; |
1129 val goal = build_goal @{context} novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs; |
1147 val goal = build_goal @{context} novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs; |
1130 val cgoal = cterm_of @{theory} goal; |
1148 val cgoal = cterm_of @{theory} goal; |
1131 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal); |
1149 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal); |
1132 val tac = (LocalDefs.unfold_tac @{context} fset_defs) THEN (foo_tac' @{context}) 1; |
1150 val tac = (LocalDefs.unfold_tac @{context} fset_defs) THEN (ObjectLogic.full_atomize_tac 1) THEN (foo_tac' @{context}) 1; |
1133 val cthm = Goal.prove_internal [] cgoal2 (fn _ => tac); |
1151 val cthm = Goal.prove_internal [] cgoal2 (fn _ => tac); |
1134 val nthm = MetaSimplifier.rewrite_rule [symmetric cthm] (snd (no_vars (Context.Theory @{theory}, thm))) |
1152 val nthm = MetaSimplifier.rewrite_rule [symmetric cthm] (snd (no_vars (Context.Theory @{theory}, thm))) |
1135 val nthm2 = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same QUOT_TYPE_I_fset.thm10} nthm; |
1153 val nthm2 = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same QUOT_TYPE_I_fset.thm10} nthm; |
1136 val [nthm3] = ProofContext.export lthy2 lthy [nthm2] |
1154 val [nthm3] = ProofContext.export lthy2 lthy [nthm2] |
1137 in |
1155 in |
1153 |
1171 |
1154 local_setup {* lift_theorem_fset @{binding "m1_lift"} @{thm m1} *} |
1172 local_setup {* lift_theorem_fset @{binding "m1_lift"} @{thm m1} *} |
1155 local_setup {* lift_theorem_fset @{binding "leqi4_lift"} @{thm list_eq.intros(4)} *} |
1173 local_setup {* lift_theorem_fset @{binding "leqi4_lift"} @{thm list_eq.intros(4)} *} |
1156 local_setup {* lift_theorem_fset @{binding "leqi5_lift"} @{thm list_eq.intros(5)} *} |
1174 local_setup {* lift_theorem_fset @{binding "leqi5_lift"} @{thm list_eq.intros(5)} *} |
1157 local_setup {* lift_theorem_fset @{binding "m2_lift"} @{thm m2} *} |
1175 local_setup {* lift_theorem_fset @{binding "m2_lift"} @{thm m2} *} |
1158 (*local_setup {* lift_theorem_fset @{binding "card_suc"} @{thm card1_suc} *}*) |
1176 (*ML {* Toplevel.program (fn () => lift_theorem_fset @{binding "card_suc"} @{thm card1_suc} @{context}) *} |
|
1177 local_setup {* lift_theorem_fset @{binding "card_suc"} @{thm card1_suc} *}*) |
1159 |
1178 |
1160 thm m1_lift |
1179 thm m1_lift |
1161 thm leqi4_lift |
1180 thm leqi4_lift |
1162 thm leqi5_lift |
1181 thm leqi5_lift |
1163 thm m2_lift |
1182 thm m2_lift |
1220 *} |
1239 *} |
1221 ML {* @{term "\<exists>x. P x"} *} |
1240 ML {* @{term "\<exists>x. P x"} *} |
1222 ML {* Thm.bicompose *} |
1241 ML {* Thm.bicompose *} |
1223 prove aaa: {* (Thm.term_of cgoal2) *} |
1242 prove aaa: {* (Thm.term_of cgoal2) *} |
1224 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
1243 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
|
1244 apply (atomize(full)) |
1225 apply (tactic {* foo_tac' @{context} 1 *}) |
1245 apply (tactic {* foo_tac' @{context} 1 *}) |
1226 done |
1246 done |
1227 |
|
1228 thm aaa |
|
1229 |
1247 |
1230 (* |
1248 (* |
1231 datatype obj1 = |
1249 datatype obj1 = |
1232 OVAR1 "string" |
1250 OVAR1 "string" |
1233 | OBJ1 "(string * (string \<Rightarrow> obj1)) list" |
1251 | OBJ1 "(string * (string \<Rightarrow> obj1)) list" |