1162 prefer 2 |
1162 prefer 2 |
1163 apply (assumption) |
1163 apply (assumption) |
1164 apply (metis) |
1164 apply (metis) |
1165 done |
1165 done |
1166 |
1166 |
1167 ML {* val thm = @{thm list_induct_r} OF [li] *} |
1167 ML {* |
|
1168 fun instantiate_tac thm = (Subgoal.FOCUS (fn {concl, context, ...} => |
|
1169 let |
|
1170 val pat = cterm_of (ProofContext.theory_of context) (concl_of thm) |
|
1171 val insts = Thm.match (pat, concl) |
|
1172 in |
|
1173 rtac (Drule.instantiate insts thm) 1 |
|
1174 end)) |
|
1175 *} |
|
1176 |
|
1177 |
|
1178 |
|
1179 ML {* val thm = @{thm list_induct_r} OF [atomize_thm @{thm list_induct_hol4}] *} |
1168 ML {* val trm_r = build_repabs_goal @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *} |
1180 ML {* val trm_r = build_repabs_goal @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *} |
1169 lemmas APPLY_RSP_I = APPLY_RSP[of "(op \<approx> ===> op =) ===> op =" "(ABS_fset ---> id) ---> id" "(REP_fset ---> id) ---> id" "op =" "id" "id"] |
1181 lemmas APPLY_RSP_I = APPLY_RSP[of "(op \<approx> ===> op =) ===> op =" "(ABS_fset ---> id) ---> id" "(REP_fset ---> id) ---> id" "op =" "id" "id"] |
1170 lemmas REP_ABS_RSP_I = REP_ABS_RSP(1)[of "(op \<approx> ===> op =) ===> op =" "(ABS_fset ---> id) ---> id" "(REP_fset ---> id) ---> id"] |
1182 lemmas REP_ABS_RSP_I = REP_ABS_RSP(1)[of "(op \<approx> ===> op =) ===> op =" "(ABS_fset ---> id) ---> id" "(REP_fset ---> id) ---> id"] |
1171 lemmas APPLY_RSP_II = APPLY_RSP[of "op \<approx>" "ABS_fset" "REP_fset" "op \<approx>" "ABS_fset" "REP_fset"] |
1183 lemmas APPLY_RSP_II = APPLY_RSP[of "op \<approx>" "ABS_fset" "REP_fset" "op \<approx>" "ABS_fset" "REP_fset"] |
1172 |
1184 |
1176 prove list_induct_tr: trm_r |
1188 prove list_induct_tr: trm_r |
1177 apply (atomize(full)) |
1189 apply (atomize(full)) |
1178 apply (simp only: id_def[symmetric]) |
1190 apply (simp only: id_def[symmetric]) |
1179 |
1191 |
1180 (* APPLY_RSP_TAC *) |
1192 (* APPLY_RSP_TAC *) |
1181 ML_prf {* |
1193 apply (tactic {* instantiate_tac @{thm APPLY_RSP[of "(op \<approx> ===> op =) ===> op =" "(ABS_fset ---> id) ---> id" "(REP_fset ---> id) ---> id" "op =" "id" "id"]} @{context} 1 *}) |
1182 val (_, gc') = Thm.dest_comb (Subgoal.focus @{context} 1 (Isar.goal ()) |> fst |> #concl) |
|
1183 val (_, tc') = Thm.dest_comb (cterm_of @{theory} (concl_of @{thm "APPLY_RSP_I" })) |
|
1184 val m = Thm.match (tc', gc') |
|
1185 val t2 = Drule.instantiate m @{thm "APPLY_RSP_I" } |
|
1186 *} |
|
1187 thm APPLY_RSP_I |
|
1188 apply (tactic {* rtac t2 1 *}) |
|
1189 prefer 2 |
1194 prefer 2 |
1190 apply (rule IDENTITY_QUOTIENT) |
1195 apply (rule IDENTITY_QUOTIENT) |
1191 prefer 3 |
1196 prefer 3 |
1192 (* ABS_REP_RSP_TAC *) |
1197 (* ABS_REP_RSP_TAC *) |
1193 ML_prf {* |
1198 apply (tactic {* instantiate_tac @{thm REP_ABS_RSP(1)[of "(op \<approx> ===> op =) ===> op =" "(ABS_fset ---> id) ---> id" "(REP_fset ---> id) ---> id"]} @{context} 1 *}) |
1194 val (_, gc') = Thm.dest_comb (Subgoal.focus @{context} 1 (Isar.goal ()) |> fst |> #concl) |
|
1195 val (_, tc') = Thm.dest_comb (cterm_of @{theory} (concl_of @{thm "REP_ABS_RSP_I" })) |
|
1196 val m = Thm.match (tc', gc') |
|
1197 val t2 = Drule.instantiate m @{thm "REP_ABS_RSP_I" } |
|
1198 *} |
|
1199 apply (tactic {* rtac t2 1 *}) |
|
1200 prefer 2 |
1199 prefer 2 |
1201 |
|
1202 (* LAMBDA_RES_TAC *) |
1200 (* LAMBDA_RES_TAC *) |
1203 apply (simp only: FUN_REL.simps) |
1201 apply (simp only: FUN_REL.simps) |
1204 apply (rule allI) |
1202 apply (rule allI) |
1205 apply (rule allI) |
1203 apply (rule allI) |
1206 apply (rule impI) |
1204 apply (rule impI) |
1207 |
|
1208 (* MK_COMB_TAC *) |
1205 (* MK_COMB_TAC *) |
1209 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) |
1206 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) |
1210 (* MK_COMB_TAC *) |
1207 (* MK_COMB_TAC *) |
1211 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) |
1208 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) |
1212 (* REFL_TAC *) |
1209 (* REFL_TAC *) |
1216 (* MK_COMB_TAC *) |
1213 (* MK_COMB_TAC *) |
1217 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) |
1214 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) |
1218 (* REFL_TAC *) |
1215 (* REFL_TAC *) |
1219 apply (simp) |
1216 apply (simp) |
1220 (* APPLY_RSP_TAC *) |
1217 (* APPLY_RSP_TAC *) |
1221 apply (rule_tac APPLY_RSP[of "op \<approx>" "ABS_fset" "REP_fset" "op =" "id" "id"]) |
1218 apply (rule APPLY_RSP[of "op \<approx>" "ABS_fset" "REP_fset" "op =" "id" "id"]) |
1222 apply (rule QUOTIENT_fset) |
1219 apply (rule QUOTIENT_fset) |
1223 apply (rule IDENTITY_QUOTIENT) |
1220 apply (rule IDENTITY_QUOTIENT) |
|
1221 apply (tactic {* instantiate_tac @{thm REP_ABS_RSP(1)} @{context} 1 *}) |
|
1222 prefer 2 |
|
1223 apply (simp only: FUN_REL.simps) |
1224 prefer 2 |
1224 prefer 2 |
1225 (* ABS_REP_RSP *) |
1225 (* ABS_REP_RSP *) |
1226 apply (rule REP_ABS_RSP(1)[of "op \<approx>" "ABS_fset" "REP_fset"]) |
1226 apply (rule REP_ABS_RSP(1)[of "op \<approx>" "ABS_fset" "REP_fset"]) |
1227 apply (rule QUOTIENT_fset) |
1227 apply (rule QUOTIENT_fset) |
1228 (* MINE *) |
1228 (* MINE *) |
1229 apply (rule list_eq_refl ) |
1229 apply (rule list_eq_refl ) |
1230 (* ABS_REP_RSP *) |
|
1231 apply (rule REP_ABS_RSP(1)[of "op \<approx> ===> op =" "REP_fset ---> id" "ABS_fset ---> id"]) |
|
1232 prefer 2 |
1230 prefer 2 |
1233 (* MINE *) |
1231 apply (tactic {* instantiate_tac @{thm APPLY_RSP[of "op \<approx> ===> op =" "REP_fset ---> id" "ABS_fset ---> id" "op =" "id" "id"]} @{context} 1 *}) |
1234 apply (simp only: FUN_REL.simps) |
|
1235 prefer 2 |
|
1236 (* APPLY_RSP *) |
|
1237 apply (rule_tac APPLY_RSP[of "op \<approx> ===> op =" "REP_fset ---> id" "ABS_fset ---> id" "op =" "id" "id" "Ball (Respects op \<approx>)" "Ball (Respects op \<approx>)"]) |
|
1238 prefer 2 |
1232 prefer 2 |
1239 apply (rule IDENTITY_QUOTIENT) |
1233 apply (rule IDENTITY_QUOTIENT) |
1240 (* 2: ho_respects *) |
1234 (* 2: ho_respects *) |
1241 prefer 3 |
1235 prefer 3 |
1242 (* ABS_REP_RSP *) |
1236 (* ABS_REP_RSP *) |
1282 apply (simp only: FUN_REL.simps) |
1276 apply (simp only: FUN_REL.simps) |
1283 prefer 2 |
1277 prefer 2 |
1284 apply (rule REP_ABS_RSP(1)[of "op \<approx>" "ABS_fset" "REP_fset"]) |
1278 apply (rule REP_ABS_RSP(1)[of "op \<approx>" "ABS_fset" "REP_fset"]) |
1285 apply (rule QUOTIENT_fset) |
1279 apply (rule QUOTIENT_fset) |
1286 (* APPLY_RSP *) |
1280 (* APPLY_RSP *) |
1287 |
1281 apply (tactic {* instantiate_tac @{thm APPLY_RSP[of "op \<approx>" "ABS_fset" "REP_fset" "op \<approx>" "ABS_fset" "REP_fset"]} @{context} 1 *}) |
1288 |
|
1289 |
|
1290 ML_prf {* |
|
1291 val goal = hd (prems_of (Isar.goal ())); |
|
1292 val goalc = Logic.strip_assums_concl goal |
|
1293 val ps = rev (map Free (Logic.strip_params goal)); |
|
1294 val (_, gc') = Thm.dest_comb (cterm_of @{theory} (Term.subst_bounds (ps, goalc))); |
|
1295 val (_, tc') = Thm.dest_comb (cterm_of @{theory} (concl_of @{thm "APPLY_RSP_II" })) |
|
1296 *} |
|
1297 ML_prf fold |
|
1298 ML_prf {* |
|
1299 val m = Thm.match (tc', gc') |
|
1300 val l = map (fst) (snd m); |
|
1301 val f_inst = map (term_of o snd) (snd m); |
|
1302 val f_abs = map (fold lambda ps) f_inst |
|
1303 *} |
|
1304 ML_prf {* val f_abs_c = map (cterm_of @{theory}) f_abs *} |
|
1305 ML_prf {* val insts = l ~~ f_abs_c *} |
|
1306 ML_prf {* val t = Thm.lift_rule (hd (cprems_of (Isar.goal ()))) @{thm "APPLY_RSP_II" } *} |
|
1307 ML_prf {* Toplevel.program (fn () => cterm_instantiate insts t) *} |
|
1308 |
|
1309 |
|
1310 |
|
1311 |
|
1312 . |
|
1313 (* FAILS: t2 = Drule.instantiate m @{thm "APPLY_RSP_II" }; rtac t2 1 *) |
|
1314 (* Works but why does it take a string? *) |
|
1315 ML_prf {* |
|
1316 val t_inst = snd m; |
|
1317 val t_insts = map (fn (a, b) => (fst (dest_Var (term_of a)), (Syntax.string_of_term @{context} (term_of b)))) t_inst |
|
1318 |
|
1319 *} |
|
1320 ML_prf dest_Var |
|
1321 apply (tactic {* res_inst_tac @{context} [(("f",0),"op # h"),(("g",0),"op # h")] @{thm "APPLY_RSP_II" } 1 *}) |
|
1322 ML_prf induct_tac |
|
1323 (*apply (rule_tac ?f="\<lambda>x. h # x" and ?g="\<lambda>x. h # x" in APPLY_RSP[of "op \<approx>" "ABS_fset" "REP_fset" "op \<approx>" "ABS_fset" "REP_fset"] )*) |
|
1324 |
|
1325 apply (rule QUOTIENT_fset) |
1282 apply (rule QUOTIENT_fset) |
1326 apply (rule QUOTIENT_fset) |
1283 apply (rule QUOTIENT_fset) |
1327 apply (rule_tac ?f="op #" and ?g="op #" in APPLY_RSP[of "op =" "id" "id" "op \<approx> ===> op \<approx>" "REP_fset ---> ABS_fset" "ABS_fset ---> REP_fset"]) |
1284 apply (tactic {* instantiate_tac @{thm APPLY_RSP[of "op =" "id" "id" "op \<approx> ===> op \<approx>" "REP_fset ---> ABS_fset" "ABS_fset ---> REP_fset"]} @{context} 1 *}) |
1328 apply (rule IDENTITY_QUOTIENT) |
1285 apply (rule IDENTITY_QUOTIENT) |
1329 (* CONS respects *) |
1286 (* CONS respects *) |
1330 prefer 2 |
1287 prefer 2 |
1331 apply (simp add: FUN_REL.simps) |
1288 apply (simp add: FUN_REL.simps) |
1332 apply (rule allI) |
1289 apply (rule allI) |
1335 apply (rule impI) |
1292 apply (rule impI) |
1336 apply (rule cons_preserves) |
1293 apply (rule cons_preserves) |
1337 apply (assumption) |
1294 apply (assumption) |
1338 prefer 2 |
1295 prefer 2 |
1339 apply (simp) |
1296 apply (simp) |
|
1297 prefer 2 |
|
1298 apply (rule REP_ABS_RSP(1)[of "op \<approx>" "ABS_fset" "REP_fset"]) |
|
1299 apply (rule QUOTIENT_fset) |
|
1300 apply (assumption) |
1340 sorry |
1301 sorry |
1341 |
1302 |
1342 prove list_induct_t: trm |
1303 prove list_induct_t: trm |
1343 apply (simp only: list_induct_tr[symmetric]) |
1304 apply (simp only: list_induct_tr[symmetric]) |
1344 apply (tactic {* rtac thm 1 *}) |
1305 apply (tactic {* rtac thm 1 *}) |