1348 |
1348 |
1349 |
1349 |
1350 ML_prf {* |
1350 ML_prf {* |
1351 val goal = hd (prems_of (Isar.goal ())); |
1351 val goal = hd (prems_of (Isar.goal ())); |
1352 val goalc = Logic.strip_assums_concl goal |
1352 val goalc = Logic.strip_assums_concl goal |
1353 val ps = rev (Logic.strip_params goal); |
1353 val ps = rev (map Free (Logic.strip_params goal)); |
1354 val (_, gc') = Thm.dest_comb (cterm_of @{theory} (Term.subst_bounds ((map Free ps), goalc))); |
1354 val (_, gc') = Thm.dest_comb (cterm_of @{theory} (Term.subst_bounds (ps, goalc))); |
1355 val (_, tc') = Thm.dest_comb (cterm_of @{theory} (concl_of @{thm "APPLY_RSP_II" })) |
1355 val (_, tc') = Thm.dest_comb (cterm_of @{theory} (concl_of @{thm "APPLY_RSP_II" })) |
1356 *} |
1356 *} |
1357 |
1357 ML_prf fold |
1358 ML_prf {* |
1358 ML_prf {* |
1359 val m = Thm.match (tc', gc') |
1359 val m = Thm.match (tc', gc') |
1360 *} |
1360 val l = map (fst) (snd m); |
|
1361 val f_inst = map (term_of o snd) (snd m); |
|
1362 val f_abs = map (fold lambda ps) f_inst |
|
1363 *} |
|
1364 ML_prf {* val f_abs_c = map (cterm_of @{theory}) f_abs *} |
|
1365 ML_prf {* val insts = l ~~ f_abs_c *} |
|
1366 ML_prf {* val t = Thm.lift_rule (hd (cprems_of (Isar.goal ()))) @{thm "APPLY_RSP_II" } *} |
|
1367 ML_prf {* Toplevel.program (fn () => cterm_instantiate insts t) *} |
|
1368 |
|
1369 ML_prf {* Toplevel.program (fn () => Drule.instantiate' [] [SOME f_abs_c, SOME f_abs_c] t) *} |
|
1370 |
|
1371 |
|
1372 |
|
1373 . |
1361 (* FAILS: t2 = Drule.instantiate m @{thm "APPLY_RSP_II" }; rtac t2 1 *) |
1374 (* FAILS: t2 = Drule.instantiate m @{thm "APPLY_RSP_II" }; rtac t2 1 *) |
1362 (* Works but why does it take a string? *) |
1375 (* Works but why does it take a string? *) |
1363 ML_prf {* |
1376 ML_prf {* |
1364 val t_inst = snd m; |
1377 val t_inst = snd m; |
1365 val t_insts = map (fn (a, b) => (fst (dest_Var (term_of a)), (Syntax.string_of_term @{context} (term_of b)))) t_inst |
1378 val t_insts = map (fn (a, b) => (fst (dest_Var (term_of a)), (Syntax.string_of_term @{context} (term_of b)))) t_inst |