781 mk_rep(mk_abs(list_comb(opp,tms))) |
785 mk_rep(mk_abs(list_comb(opp,tms))) |
782 else if tms = [] then opp |
786 else if tms = [] then opp |
783 else list_comb(opp, tms) |
787 else list_comb(opp, tms) |
784 end |
788 end |
785 in |
789 in |
786 build_aux lthy (Thm.prop_of thm) |
790 MetaSimplifier.rewrite_term @{theory} @{thms id_def_sym} [] |
|
791 (build_aux lthy (Thm.prop_of thm)) |
787 end |
792 end |
788 *} |
793 *} |
789 |
794 |
790 text {* Assumes that it is given a regularized theorem *} |
795 text {* Assumes that it is given a regularized theorem *} |
791 ML {* |
796 ML {* |
1029 THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI} |
1034 THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI} |
1030 THEN' instantiate_tac @{thm RES_FORALL_RSP} ctxt THEN' |
1035 THEN' instantiate_tac @{thm RES_FORALL_RSP} ctxt THEN' |
1031 (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps})) |
1036 (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps})) |
1032 *} |
1037 *} |
1033 |
1038 |
1034 ML {* |
|
1035 |
|
1036 ((simp_tac ((Simplifier.context @{context} HOL_ss) addsimps @{thms FUN_REL.simps})) THEN' (fn _ => no_tac)) |
|
1037 *} |
|
1038 |
|
1039 ML {* ((simp_tac ((Simplifier.context @{context} HOL_ss) addsimps @{thms FUN_REL.simps})) THEN_ALL_NEW (fn _ => no_tac)) *} |
|
1040 ML {* RANGE *} |
|
1041 |
1039 |
1042 ML {* |
1040 ML {* |
1043 fun quotient_tac quot_thm = |
1041 fun quotient_tac quot_thm = |
1044 REPEAT_ALL_NEW (FIRST' [ |
1042 REPEAT_ALL_NEW (FIRST' [ |
1045 rtac @{thm FUN_QUOTIENT}, |
1043 rtac @{thm FUN_QUOTIENT}, |
1075 ML {* val trm_r = build_repabs_goal @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *} |
1073 ML {* val trm_r = build_repabs_goal @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *} |
1076 ML {* val trm = build_repabs_term @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *} |
1074 ML {* val trm = build_repabs_term @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *} |
1077 |
1075 |
1078 prove list_induct_tr: trm_r |
1076 prove list_induct_tr: trm_r |
1079 apply (atomize(full)) |
1077 apply (atomize(full)) |
1080 apply (simp only: id_def[symmetric]) |
|
1081 (* APPLY_RSP_TAC *) |
1078 (* APPLY_RSP_TAC *) |
1082 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
1079 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1083 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
|
1084 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
|
1085 (* LAMBDA_RES_TAC *) |
1080 (* LAMBDA_RES_TAC *) |
1086 apply (simp only: FUN_REL.simps) |
1081 apply (simp only: FUN_REL.simps) |
1087 apply (rule allI) |
1082 apply (rule allI) |
1088 apply (rule allI) |
1083 apply (rule allI) |
1089 apply (rule impI) |
1084 apply (rule impI) |
1098 (* MK_COMB_TAC *) |
1093 (* MK_COMB_TAC *) |
1099 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) |
1094 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) |
1100 (* REFL_TAC *) |
1095 (* REFL_TAC *) |
1101 apply (simp) |
1096 apply (simp) |
1102 (* APPLY_RSP_TAC *) |
1097 (* APPLY_RSP_TAC *) |
1103 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
|
1104 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
|
1105 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1098 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1106 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1099 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1107 apply (simp only: FUN_REL.simps) |
1100 apply (simp only: FUN_REL.simps) |
1108 apply (rule allI) |
1101 apply (rule allI) |
1109 apply (rule allI) |
1102 apply (rule allI) |
1113 (* MK_COMB_TAC *) |
1106 (* MK_COMB_TAC *) |
1114 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) |
1107 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) |
1115 (* REFL_TAC *) |
1108 (* REFL_TAC *) |
1116 apply (simp) |
1109 apply (simp) |
1117 (* APPLY_RSP *) |
1110 (* APPLY_RSP *) |
1118 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
|
1119 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
|
1120 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1111 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1121 (* MK_COMB_TAC *) |
1112 (* MK_COMB_TAC *) |
1122 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) |
1113 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) |
1123 (* REFL_TAC *) |
1114 (* REFL_TAC *) |
1124 apply (simp) |
1115 apply (simp) |
1125 (* W(C (curry op THEN) (G... *) |
1116 (* W(C (curry op THEN) (G... *) |
1126 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
|
1127 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
|
1128 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1117 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1129 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
|
1130 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
|
1131 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
|
1132 (* CONS respects *) |
1118 (* CONS respects *) |
1133 apply (simp add: FUN_REL.simps) |
1119 apply (simp add: FUN_REL.simps) |
1134 apply (rule allI) |
1120 apply (rule allI) |
1135 apply (rule allI) |
1121 apply (rule allI) |
1136 apply (rule allI) |
1122 apply (rule allI) |
1137 apply (rule impI) |
1123 apply (rule impI) |
1138 apply (rule cons_preserves) |
1124 apply (rule cons_preserves) |
1139 apply (assumption) |
1125 apply (assumption) |
1140 apply (simp) |
|
1141 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1126 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1142 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
|
1143 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
|
1144 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *}) |
|
1145 apply (simp only: FUN_REL.simps) |
1127 apply (simp only: FUN_REL.simps) |
1146 apply (rule allI) |
1128 apply (rule allI) |
1147 apply (rule allI) |
1129 apply (rule allI) |
1148 apply (rule impI) |
1130 apply (rule impI) |
1149 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1131 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
1156 |
1138 |
1157 ML {* val nthm = MetaSimplifier.rewrite_rule fset_defs_sym (snd (no_vars (Context.Theory @{theory}, @{thm list_induct_t}))) *} |
1139 ML {* val nthm = MetaSimplifier.rewrite_rule fset_defs_sym (snd (no_vars (Context.Theory @{theory}, @{thm list_induct_t}))) *} |
1158 |
1140 |
1159 thm list.recs(2) |
1141 thm list.recs(2) |
1160 |
1142 |
|
1143 ML {* atomize_thm @{thm m2} *} |
|
1144 |
|
1145 prove m2_r_p: {* |
|
1146 build_regularize_goal (atomize_thm @{thm m2}) @{typ "'a List.list"} @{term "op \<approx>"} @{context} *} |
|
1147 apply (simp add: equiv_res_forall[OF equiv_list_eq]) |
|
1148 done |
|
1149 |
|
1150 ML {* val m2_r = @{thm m2_r_p} OF [atomize_thm @{thm m2}] *} |
|
1151 ML {* val m2_t_g = build_repabs_goal @{context} m2_r consts @{typ "'a list"} @{typ "'a fset"} *} |
|
1152 ML {* val m2_t = build_repabs_term @{context} m2_r consts @{typ "'a list"} @{typ "'a fset"} *} |
|
1153 prove m2_t_p: m2_t_g |
|
1154 apply (atomize(full)) |
|
1155 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
|
1156 apply (simp add: FUN_REL.simps) |
|
1157 prefer 2 |
|
1158 apply (simp only: FUN_REL.simps) |
|
1159 apply (rule allI) |
|
1160 apply (rule allI) |
|
1161 apply (rule impI) |
|
1162 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
|
1163 prefer 2 |
|
1164 apply (simp only: FUN_REL.simps) |
|
1165 apply (rule allI) |
|
1166 apply (rule allI) |
|
1167 apply (rule impI) |
|
1168 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
|
1169 apply (simp only: FUN_REL.simps) |
|
1170 apply (rule allI) |
|
1171 apply (rule allI) |
|
1172 apply (rule impI) |
|
1173 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
|
1174 apply (simp only: FUN_REL.simps) |
|
1175 apply (rule allI) |
|
1176 apply (rule allI) |
|
1177 apply (rule impI) |
|
1178 apply (rule allI) |
|
1179 apply (rule allI) |
|
1180 apply (rule impI) |
|
1181 apply (simp add:mem_respects) |
|
1182 apply (simp only: FUN_REL.simps) |
|
1183 apply (rule allI) |
|
1184 apply (rule allI) |
|
1185 apply (rule impI) |
|
1186 apply (rule allI) |
|
1187 apply (rule allI) |
|
1188 apply (rule impI) |
|
1189 apply (simp add:cons_preserves) |
|
1190 apply (simp only: FUN_REL.simps) |
|
1191 apply (rule allI) |
|
1192 apply (rule allI) |
|
1193 apply (rule impI) |
|
1194 apply (rule allI) |
|
1195 apply (rule allI) |
|
1196 apply (rule impI) |
|
1197 apply (simp add:mem_respects) |
|
1198 apply (auto) |
|
1199 done |
|
1200 |
|
1201 prove m2_t: m2_t |
|
1202 apply (simp only: m2_t_p[symmetric]) |
|
1203 apply (tactic {* rtac m2_r 1 *}) |
|
1204 done |
|
1205 |
|
1206 thm LAMBDA_PRS |
|
1207 ML {* |
|
1208 val t = prop_of @{thm LAMBDA_PRS} |
|
1209 val tt = Drule.instantiate' [SOME @{ctyp "'a list"}, SOME @{ctyp "'a fset"}] [] @{thm LAMBDA_PRS} |
|
1210 val ttt = tt OF [@{thm QUOTIENT_fset}, @{thm IDENTITY_QUOTIENT}] |
|
1211 *} |
|
1212 ML {* val tttt = @{thm "HOL.sym"} OF [ttt] *} |
|
1213 ML {* val zzzz = MetaSimplifier.rewrite_rule [tttt] @{thm m2_t} *} |
|
1214 |
|
1215 |
|
1216 thm m2_t |
|
1217 ML {* @{thm m2_t} *} |
1161 |
1218 |
1162 ML {* val card1_suc_f = Thm.freezeT (atomize_thm @{thm card1_suc}) *} |
1219 ML {* val card1_suc_f = Thm.freezeT (atomize_thm @{thm card1_suc}) *} |
1163 |
1220 |
1164 prove card1_suc_r: {* |
1221 prove card1_suc_r: {* |
1165 Logic.mk_implies |
1222 Logic.mk_implies |