1262 val goal'' = cterm_of @{theory} (Term.subst_bounds ((map Free ps), goalc)) |
1262 val goal'' = cterm_of @{theory} (Term.subst_bounds ((map Free ps), goalc)) |
1263 *} |
1263 *} |
1264 ML_prf {* ct; goal'' *} |
1264 ML_prf {* ct; goal'' *} |
1265 |
1265 |
1266 ML_prf {* val nlct = cterm_of @{theory} (concl_of @{thm "APPLY_RSP_I2" }) *} |
1266 ML_prf {* val nlct = cterm_of @{theory} (concl_of @{thm "APPLY_RSP_I2" }) *} |
|
1267 |
1267 ML_prf {* Thm.match (nlct, goal'') *} |
1268 ML_prf {* Thm.match (nlct, goal'') *} |
|
1269 ML_prf {* ct *} |
|
1270 |
|
1271 |
|
1272 (*apply (tactic {*Cong_Tac.cong_tac @{thm APPLY_RSP_I2} 1 *}) *) |
1268 ML_prf {* t *} |
1273 ML_prf {* t *} |
1269 |
|
1270 |
|
1271 (*apply (tactic {*Cong_Tac.cong_tac @{thm APPLY_RSP_I2} 1 *}) *) |
|
1272 ML_prf {* |
1274 ML_prf {* |
1273 Toplevel.program (fn () => |
1275 val man_inst = |
1274 Drule.instantiate' [] [NONE, SOME @{cterm "\<lambda>(x\<Colon>'a list \<Rightarrow> bool) (y\<Colon>'a list \<Rightarrow> bool). []"}] t |
1276 Drule.instantiate' [SOME @{ctyp 'a}, SOME @{ctyp bool}] |
1275 ) |
1277 [ |
1276 *} |
1278 SOME @{cterm "\<lambda>(x\<Colon>'a list \<Rightarrow> bool) (y\<Colon>'a list \<Rightarrow> bool). y"}, |
1277 |
1279 SOME @{cterm "\<lambda>(x\<Colon>'a list \<Rightarrow> bool) (y\<Colon>'a list \<Rightarrow> bool). (ABS_fset ---> id) ((REP_fset ---> id) x)"}, |
1278 |
1280 SOME @{cterm "\<lambda>(x\<Colon>'a list \<Rightarrow> bool) (y\<Colon>'a list \<Rightarrow> bool). ([]::'a list)"}, |
1279 |
1281 SOME @{cterm "\<lambda>(x\<Colon>'a list \<Rightarrow> bool) (y\<Colon>'a list \<Rightarrow> bool). (REP_fset (ABS_fset ([]::'a list)))"} |
1280 ML_prf {* |
1282 ] t |
1281 val pat = @{cpat "?f6 x y"} |
1283 *} |
1282 val arg = @{cterm "[]"} |
1284 |
1283 *} |
1285 apply (tactic {* rtac man_inst 1 *}) |
1284 |
|
1285 |
|
1286 ML_prf {* |
|
1287 val m = Thm.match (pat, arg) |
|
1288 *} |
|
1289 |
|
1290 ML_prf {* |
|
1291 val m = Thm.match (ct, goal') |
|
1292 val t2 = Drule.instantiate m @{thm "APPLY_RSP_I2" } |
|
1293 *} |
|
1294 apply (tactic {* rtac t2 1 *}) |
|
1295 |
1286 |
1296 thm APPLY_RSP |
1287 thm APPLY_RSP |
1297 sorry |
1288 sorry |
1298 |
1289 |
1299 thm list.recs(2) |
1290 thm list.recs(2) |