1251 ML_prf {* |
1251 ML_prf {* |
1252 val goal = hd (prems_of (Isar.goal ())) |
1252 val goal = hd (prems_of (Isar.goal ())) |
1253 val goalc = Logic.strip_assums_concl goal |
1253 val goalc = Logic.strip_assums_concl goal |
1254 *} |
1254 *} |
1255 ML_prf {* |
1255 ML_prf {* |
|
1256 val goalct = cterm_of @{theory} (hd ( prems_of (Isar.goal ()))) |
|
1257 *} |
|
1258 |
|
1259 ML_prf {* |
1256 val ps = Logic.strip_params goal |
1260 val ps = Logic.strip_params goal |
1257 val goal' = cterm_of @{theory} (Term.list_abs (ps, goalc)) |
1261 val goal' = cterm_of @{theory} (Term.list_abs (ps, goalc)) |
1258 *} |
1262 val goal'' = cterm_of @{theory} (Term.subst_bounds ((map Free ps), goalc)) |
1259 ML_prf {* ct; goal' *} |
1263 *} |
1260 |
1264 ML_prf {* ct; goal'' *} |
1261 *) |
1265 |
|
1266 ML_prf {* val nlct = cterm_of @{theory} (concl_of @{thm "APPLY_RSP_I2" }) *} |
|
1267 ML_prf {* Thm.match (nlct, goal'') *} |
|
1268 ML_prf {* t *} |
|
1269 |
|
1270 |
|
1271 (*apply (tactic {*Cong_Tac.cong_tac @{thm APPLY_RSP_I2} 1 *}) *) |
1262 ML_prf {* |
1272 ML_prf {* |
1263 val pat = @{cpat "\<lambda>x y. (?f6 x y (?x6 x y) = ?g6 x y (?y6 x y))"} |
1273 Toplevel.program (fn () => |
1264 val arg = @{cterm "\<lambda>x y. (x [] = y [])"} |
1274 Drule.instantiate' [] [NONE, SOME @{cterm "\<lambda>(x\<Colon>'a list \<Rightarrow> bool) (y\<Colon>'a list \<Rightarrow> bool). []"}] t |
1265 *} |
1275 ) |
|
1276 *} |
|
1277 |
|
1278 |
1266 |
1279 |
1267 ML_prf {* |
1280 ML_prf {* |
1268 val pat = @{cpat "(?f6 x y (?x6) = ?g6 x y (?y6))"} |
1281 val pat = @{cpat "?f6 x y"} |
1269 val arg = @{cterm "(x [] = y [])"} |
1282 val arg = @{cterm "[]"} |
1270 *} |
1283 *} |
|
1284 |
1271 |
1285 |
1272 ML_prf {* |
1286 ML_prf {* |
1273 val m = Thm.match (pat, arg) |
1287 val m = Thm.match (pat, arg) |
1274 *} |
1288 *} |
1275 |
1289 |