469 fun atomize_thm thm = |
469 fun atomize_thm thm = |
470 let |
470 let |
471 val thm' = forall_intr_vars thm |
471 val thm' = forall_intr_vars thm |
472 val thm'' = ObjectLogic.atomize (cprop_of thm') |
472 val thm'' = ObjectLogic.atomize (cprop_of thm') |
473 in |
473 in |
474 Simplifier.rewrite_rule [thm''] thm' |
474 Thm.freezeT (Simplifier.rewrite_rule [thm''] thm') |
475 end |
475 end |
476 *} |
476 *} |
477 |
477 |
|
478 ML {* atomize_thm @{thm list.induct} *} |
478 |
479 |
479 section {* REGULARIZE *} |
480 section {* REGULARIZE *} |
480 |
481 |
481 text {* tyRel takes a type and builds a relation that a quantifier over this |
482 text {* tyRel takes a type and builds a relation that a quantifier over this |
482 type needs to respect. *} |
483 type needs to respect. *} |
701 |
702 |
702 (*fun prove_reg trm \<Rightarrow> thm (we might need some facts to do this) |
703 (*fun prove_reg trm \<Rightarrow> thm (we might need some facts to do this) |
703 trm == new_trm |
704 trm == new_trm |
704 *) |
705 *) |
705 |
706 |
706 section {* TRANSCONV *} |
707 ML {* |
707 |
708 fun build_regularize_goal thm rty rel lthy = |
708 |
709 Logic.mk_implies |
709 ML {* |
710 ((prop_of thm), |
710 fun build_goal_term lthy thm constructors rty qty = |
711 (regularise (prop_of thm) rty rel lthy)) |
|
712 *} |
|
713 |
|
714 section {* RepAbs injection *} |
|
715 |
|
716 |
|
717 ML {* |
|
718 fun build_repabs_term lthy thm constructors rty qty = |
711 let |
719 let |
712 fun mk_rep tm = |
720 fun mk_rep tm = |
713 let |
721 let |
714 val ty = exchange_ty rty qty (fastype_of tm) |
722 val ty = exchange_ty rty qty (fastype_of tm) |
715 in fst (get_fun repF rty qty lthy ty) $ tm end |
723 in fst (get_fun repF rty qty lthy ty) $ tm end |
764 build_aux lthy (Thm.prop_of thm) |
772 build_aux lthy (Thm.prop_of thm) |
765 end |
773 end |
766 *} |
774 *} |
767 |
775 |
768 ML {* |
776 ML {* |
769 fun build_goal ctxt thm cons rty qty = |
777 fun build_repabs_goal ctxt thm cons rty qty = |
770 Logic.mk_equals ((Thm.prop_of thm), (build_goal_term ctxt thm cons rty qty)) |
778 Logic.mk_equals ((Thm.prop_of thm), (build_repabs_term ctxt thm cons rty qty)) |
771 *} |
779 *} |
772 |
780 |
773 |
781 |
774 |
782 |
775 |
783 |
776 |
784 |
777 text {* finite set example *} |
785 section {* finite set example *} |
|
786 |
778 print_syntax |
787 print_syntax |
779 inductive |
788 inductive |
780 list_eq (infix "\<approx>" 50) |
789 list_eq (infix "\<approx>" 50) |
781 where |
790 where |
782 "a#b#xs \<approx> b#a#xs" |
791 "a#b#xs \<approx> b#a#xs" |
1056 val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m2})) |
1065 val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m2})) |
1057 *} |
1066 *} |
1058 |
1067 |
1059 ML {* |
1068 ML {* |
1060 cterm_of @{theory} (prop_of m1_novars); |
1069 cterm_of @{theory} (prop_of m1_novars); |
1061 cterm_of @{theory} (build_goal_term @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"}); |
1070 cterm_of @{theory} (build_repabs_term @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"}); |
1062 *} |
1071 *} |
1063 |
1072 |
1064 |
1073 |
1065 (* Has all the theorems about fset plugged in. These should be parameters to the tactic *) |
1074 (* Has all the theorems about fset plugged in. These should be parameters to the tactic *) |
1066 ML {* |
1075 ML {* |
1079 ]) 1 |
1088 ]) 1 |
1080 *} |
1089 *} |
1081 |
1090 |
1082 ML {* |
1091 ML {* |
1083 val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m1})) |
1092 val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m1})) |
1084 val goal = build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} |
1093 val goal = build_repabs_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} |
1085 val cgoal = cterm_of @{theory} goal |
1094 val cgoal = cterm_of @{theory} goal |
1086 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
1095 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
1087 *} |
1096 *} |
1088 |
1097 |
1089 (*notation ( output) "prop" ("#_" [1000] 1000) *) |
1098 (*notation ( output) "prop" ("#_" [1000] 1000) *) |
1095 done |
1104 done |
1096 |
1105 |
1097 thm length_append (* Not true but worth checking that the goal is correct *) |
1106 thm length_append (* Not true but worth checking that the goal is correct *) |
1098 ML {* |
1107 ML {* |
1099 val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm length_append})) |
1108 val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm length_append})) |
1100 val goal = build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} |
1109 val goal = build_repabs_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} |
1101 val cgoal = cterm_of @{theory} goal |
1110 val cgoal = cterm_of @{theory} goal |
1102 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
1111 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
1103 *} |
1112 *} |
1104 prove {* Thm.term_of cgoal2 *} |
1113 prove {* Thm.term_of cgoal2 *} |
1105 apply (tactic {* transconv_fset_tac' @{context} *}) |
1114 apply (tactic {* transconv_fset_tac' @{context} *}) |
1106 sorry |
1115 sorry |
1107 |
1116 |
1108 thm m2 |
1117 thm m2 |
1109 ML {* |
1118 ML {* |
1110 val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m2})) |
1119 val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m2})) |
1111 val goal = build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} |
1120 val goal = build_repabs_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} |
1112 val cgoal = cterm_of @{theory} goal |
1121 val cgoal = cterm_of @{theory} goal |
1113 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
1122 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
1114 *} |
1123 *} |
1115 prove {* Thm.term_of cgoal2 *} |
1124 prove {* Thm.term_of cgoal2 *} |
1116 apply (tactic {* transconv_fset_tac' @{context} *}) |
1125 apply (tactic {* transconv_fset_tac' @{context} *}) |
1117 done |
1126 done |
1118 |
1127 |
1119 thm list_eq.intros(4) |
1128 thm list_eq.intros(4) |
1120 ML {* |
1129 ML {* |
1121 val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list_eq.intros(4)})) |
1130 val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list_eq.intros(4)})) |
1122 val goal = build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} |
1131 val goal = build_repabs_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} |
1123 val cgoal = cterm_of @{theory} goal |
1132 val cgoal = cterm_of @{theory} goal |
1124 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
1133 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal) |
1125 val cgoal3 = Thm.rhs_of (MetaSimplifier.rewrite true @{thms QUOT_TYPE_I_fset.thm10} cgoal2) |
1134 val cgoal3 = Thm.rhs_of (MetaSimplifier.rewrite true @{thms QUOT_TYPE_I_fset.thm10} cgoal2) |
1126 *} |
1135 *} |
1127 |
1136 |
1139 *) |
1148 *) |
1140 |
1149 |
1141 thm list_eq.intros(5) |
1150 thm list_eq.intros(5) |
1142 ML {* |
1151 ML {* |
1143 val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list_eq.intros(5)})) |
1152 val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list_eq.intros(5)})) |
1144 val goal = build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} |
1153 val goal = build_repabs_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} |
1145 val cgoal = cterm_of @{theory} goal |
1154 val cgoal = cterm_of @{theory} goal |
1146 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal) |
1155 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal) |
1147 *} |
1156 *} |
1148 prove {* Thm.term_of cgoal2 *} |
1157 prove {* Thm.term_of cgoal2 *} |
1149 apply (tactic {* transconv_fset_tac' @{context} *}) |
1158 apply (tactic {* transconv_fset_tac' @{context} *}) |
1158 sorry |
1167 sorry |
1159 |
1168 |
1160 ML {* atomize_thm @{thm list_induct_hol4} *} |
1169 ML {* atomize_thm @{thm list_induct_hol4} *} |
1161 |
1170 |
1162 |
1171 |
1163 ML {* val li = Thm.freezeT (atomize_thm @{thm list_induct_hol4}) *} |
1172 ML {* val li = atomize_thm @{thm list_induct_hol4} *} |
1164 |
1173 |
1165 prove list_induct_r: {* |
1174 prove list_induct_r: {* |
1166 Logic.mk_implies |
1175 build_regularize_goal (atomize_thm @{thm list_induct_hol4}) @{typ "'a List.list"} @{term "op \<approx>"} @{context} *} |
1167 ((prop_of li), |
|
1168 (regularise (prop_of li) @{typ "'a List.list"} @{term "op \<approx>"} @{context})) *} |
|
1169 apply (simp only: equiv_res_forall[OF equiv_list_eq]) |
1176 apply (simp only: equiv_res_forall[OF equiv_list_eq]) |
1170 thm RIGHT_RES_FORALL_REGULAR |
1177 thm RIGHT_RES_FORALL_REGULAR |
1171 apply (rule RIGHT_RES_FORALL_REGULAR) |
1178 apply (rule RIGHT_RES_FORALL_REGULAR) |
1172 prefer 2 |
1179 prefer 2 |
1173 apply (assumption) |
1180 apply (assumption) |
1174 apply (metis) |
1181 apply (metis) |
1175 done |
1182 done |
1176 |
1183 |
1177 ML {* val thm = @{thm list_induct_r} OF [li] *} |
1184 ML {* val thm = @{thm list_induct_r} OF [li] *} |
1178 ML {* val trm_r = build_goal @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *} |
1185 ML {* val trm_r = build_repabs_goal @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *} |
1179 lemmas APPLY_RSP_I = APPLY_RSP[of "(op \<approx> ===> op =) ===> op =" "(ABS_fset ---> id) ---> id" "(REP_fset ---> id) ---> id" "op =" "id" "id"] |
1186 lemmas APPLY_RSP_I = APPLY_RSP[of "(op \<approx> ===> op =) ===> op =" "(ABS_fset ---> id) ---> id" "(REP_fset ---> id) ---> id" "op =" "id" "id"] |
1180 lemmas REP_ABS_RSP_I = REP_ABS_RSP(1)[of "(op \<approx> ===> op =) ===> op =" "(ABS_fset ---> id) ---> id" "(REP_fset ---> id) ---> id"] |
1187 lemmas REP_ABS_RSP_I = REP_ABS_RSP(1)[of "(op \<approx> ===> op =) ===> op =" "(ABS_fset ---> id) ---> id" "(REP_fset ---> id) ---> id"] |
1181 lemmas APPLY_RSP_II = APPLY_RSP[of "op \<approx>" "ABS_fset" "REP_fset" "op \<approx>" "ABS_fset" "REP_fset"] |
1188 lemmas APPLY_RSP_II = APPLY_RSP[of "op \<approx>" "ABS_fset" "REP_fset" "op \<approx>" "ABS_fset" "REP_fset"] |
1182 |
1189 |
1183 ML {* val trm = build_goal_term @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *} |
1190 ML {* val trm = build_repabs_term @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *} |
1184 |
1191 |
1185 |
1192 |
1186 prove list_induct_tr: trm_r |
1193 prove list_induct_tr: trm_r |
1187 apply (atomize(full)) |
1194 apply (atomize(full)) |
1188 apply (simp only: id_def[symmetric]) |
1195 apply (simp only: id_def[symmetric]) |
1382 |
1389 |
1383 ML {* |
1390 ML {* |
1384 fun lift_theorem_fset_aux thm lthy = |
1391 fun lift_theorem_fset_aux thm lthy = |
1385 let |
1392 let |
1386 val ((_, [novars]), lthy2) = Variable.import true [thm] lthy; |
1393 val ((_, [novars]), lthy2) = Variable.import true [thm] lthy; |
1387 val goal = build_goal @{context} novars consts @{typ "'a list"} @{typ "'a fset"}; |
1394 val goal = build_repabs_goal @{context} novars consts @{typ "'a list"} @{typ "'a fset"}; |
1388 val cgoal = cterm_of @{theory} goal; |
1395 val cgoal = cterm_of @{theory} goal; |
1389 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal); |
1396 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal); |
1390 val tac = transconv_fset_tac' @{context}; |
1397 val tac = transconv_fset_tac' @{context}; |
1391 val cthm = Goal.prove_internal [] cgoal2 (fn _ => tac); |
1398 val cthm = Goal.prove_internal [] cgoal2 (fn _ => tac); |
1392 val nthm = MetaSimplifier.rewrite_rule [symmetric cthm] (snd (no_vars (Context.Theory @{theory}, thm))) |
1399 val nthm = MetaSimplifier.rewrite_rule [symmetric cthm] (snd (no_vars (Context.Theory @{theory}, thm))) |