1226 |
1226 |
1227 ML {* val thm = @{thm list_induct_r} OF [li] *} |
1227 ML {* val thm = @{thm list_induct_r} OF [li] *} |
1228 ML {* val trm_r = build_goal @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *} |
1228 ML {* val trm_r = build_goal @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *} |
1229 lemmas APPLY_RSP_I = APPLY_RSP[of "(op \<approx> ===> op =) ===> op =" "(ABS_fset ---> id) ---> id" "(REP_fset ---> id) ---> id" "op =" "id" "id"] |
1229 lemmas APPLY_RSP_I = APPLY_RSP[of "(op \<approx> ===> op =) ===> op =" "(ABS_fset ---> id) ---> id" "(REP_fset ---> id) ---> id" "op =" "id" "id"] |
1230 lemmas REP_ABS_RSP_I = REP_ABS_RSP(1)[of "(op \<approx> ===> op =) ===> op =" "(ABS_fset ---> id) ---> id" "(REP_fset ---> id) ---> id"] |
1230 lemmas REP_ABS_RSP_I = REP_ABS_RSP(1)[of "(op \<approx> ===> op =) ===> op =" "(ABS_fset ---> id) ---> id" "(REP_fset ---> id) ---> id"] |
|
1231 lemmas APPLY_RSP_II = APPLY_RSP[of "op \<approx>" "ABS_fset" "REP_fset" "op \<approx>" "ABS_fset" "REP_fset"] |
1231 |
1232 |
1232 ML {* val trm = build_goal_term @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *} |
1233 ML {* val trm = build_goal_term @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *} |
|
1234 |
1233 |
1235 |
1234 prove list_induct_tr: trm_r |
1236 prove list_induct_tr: trm_r |
1235 apply (atomize(full)) |
1237 apply (atomize(full)) |
1236 apply (simp only: id_def[symmetric]) |
1238 apply (simp only: id_def[symmetric]) |
1237 |
1239 |
1340 apply (simp only: FUN_REL.simps) |
1342 apply (simp only: FUN_REL.simps) |
1341 prefer 2 |
1343 prefer 2 |
1342 apply (rule REP_ABS_RSP(1)[of "op \<approx>" "ABS_fset" "REP_fset"]) |
1344 apply (rule REP_ABS_RSP(1)[of "op \<approx>" "ABS_fset" "REP_fset"]) |
1343 apply (rule QUOTIENT_fset) |
1345 apply (rule QUOTIENT_fset) |
1344 (* APPLY_RSP *) |
1346 (* APPLY_RSP *) |
1345 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"] ) |
1347 |
|
1348 |
|
1349 |
|
1350 ML_prf {* |
|
1351 val goal = hd (prems_of (Isar.goal ())); |
|
1352 val goalc = Logic.strip_assums_concl goal |
|
1353 val ps = rev (Logic.strip_params goal); |
|
1354 val (_, gc') = Thm.dest_comb (cterm_of @{theory} (Term.subst_bounds ((map Free ps), goalc))); |
|
1355 val (_, tc') = Thm.dest_comb (cterm_of @{theory} (concl_of @{thm "APPLY_RSP_II" })) |
|
1356 *} |
|
1357 |
|
1358 ML_prf {* |
|
1359 val m = Thm.match (tc', gc') |
|
1360 *} |
|
1361 (* FAILS: t2 = Drule.instantiate m @{thm "APPLY_RSP_II" }; rtac t2 1 *) |
|
1362 (* Works but why does it take a string? *} |
|
1363 apply (tactic {* res_inst_tac @{context} [(("f",0),"\<lambda>x. h # x"),(("g",0),"\<lambda>x. h # x")] @{thm "APPLY_RSP_II" } 1 *}) |
|
1364 (*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"] )*) |
|
1365 |
1346 apply (rule QUOTIENT_fset) |
1366 apply (rule QUOTIENT_fset) |
1347 apply (rule QUOTIENT_fset) |
1367 apply (rule QUOTIENT_fset) |
1348 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"]) |
1368 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"]) |
1349 apply (rule IDENTITY_QUOTIENT) |
1369 apply (rule IDENTITY_QUOTIENT) |
1350 (* CONS respects *) |
1370 (* CONS respects *) |