1273 ML_prf {* t *} |
1273 ML_prf {* t *} |
1274 ML_prf {* |
1274 ML_prf {* |
1275 val man_inst = |
1275 val man_inst = |
1276 Drule.instantiate' [SOME @{ctyp 'a}, SOME @{ctyp bool}] |
1276 Drule.instantiate' [SOME @{ctyp 'a}, SOME @{ctyp bool}] |
1277 [ |
1277 [ |
1278 SOME @{cterm "\<lambda>(x\<Colon>'a list \<Rightarrow> bool) (y\<Colon>'a list \<Rightarrow> bool). y"}, |
1278 SOME @{cterm "\<lambda>(x\<Colon>'a list \<Rightarrow> bool) (y\<Colon>'a list \<Rightarrow> bool). x"}, |
1279 SOME @{cterm "\<lambda>(x\<Colon>'a list \<Rightarrow> bool) (y\<Colon>'a list \<Rightarrow> bool). (ABS_fset ---> id) ((REP_fset ---> id) x)"}, |
1279 SOME @{cterm "\<lambda>(x\<Colon>'a list \<Rightarrow> bool) (y\<Colon>'a list \<Rightarrow> bool). (ABS_fset ---> id) ((REP_fset ---> id) y)"}, |
1280 SOME @{cterm "\<lambda>(x\<Colon>'a list \<Rightarrow> bool) (y\<Colon>'a list \<Rightarrow> bool). ([]::'a list)"}, |
1280 SOME @{cterm "\<lambda>(x\<Colon>'a list \<Rightarrow> bool) (y\<Colon>'a list \<Rightarrow> bool). ([]::'a list)"}, |
1281 SOME @{cterm "\<lambda>(x\<Colon>'a list \<Rightarrow> bool) (y\<Colon>'a list \<Rightarrow> bool). (REP_fset (ABS_fset ([]::'a list)))"} |
1281 SOME @{cterm "\<lambda>(x\<Colon>'a list \<Rightarrow> bool) (y\<Colon>'a list \<Rightarrow> bool). (REP_fset (ABS_fset ([]::'a list)))"} |
1282 ] t |
1282 ] t |
1283 *} |
1283 *} |
1284 |
1284 ML_prf {* |
1285 apply (tactic {* rtac man_inst 1 *}) |
1285 val (tc') = (Logic.strip_assums_concl (prop_of man_inst)); |
1286 |
1286 val ps = Logic.strip_params (prop_of man_inst) |
1287 thm APPLY_RSP |
1287 val tt = Term.list_abs (ps, tc') |
|
1288 val ct = cterm_of @{theory} tt |
|
1289 *} |
|
1290 ML_prf {* |
|
1291 fun dest_cbinop t = |
|
1292 let |
|
1293 val (t2, rhs) = Thm.dest_comb t; |
|
1294 val (bop, lhs) = Thm.dest_comb t2; |
|
1295 in |
|
1296 (bop, (lhs, rhs)) |
|
1297 end |
|
1298 *} |
|
1299 |
|
1300 |
|
1301 ML_prf {* val (a, b) = (snd (Thm.dest_abs NONE ct), (snd (Thm.dest_abs NONE goal'))) *} |
|
1302 ML_prf {* val (a, b) = (snd (Thm.dest_abs NONE a), (snd (Thm.dest_abs NONE b))) *} |
|
1303 ML_prf {* val (a, b) = (snd (Thm.dest_comb a), snd (Thm.dest_comb b)) *} |
|
1304 ML_prf {* val (a, b) = ((fst o snd) (dest_cbinop a), (fst o snd) (dest_cbinop b)) *} |
|
1305 ML_prf {* (term_of a, term_of b) *} |
|
1306 ML_prf {* (Envir.beta_norm (term_of a), term_of b) *} |
|
1307 ML_prf {* Thm.beta_conv *} |
|
1308 ML_prf man_inst |
|
1309 thm APPLY_RSP_I2 |
|
1310 apply (tactic {* compose_tac (false,man_inst,0) 1 *}) |
|
1311 |
1288 sorry |
1312 sorry |
1289 |
1313 |
1290 thm list.recs(2) |
1314 thm list.recs(2) |
1291 |
1315 |
1292 |
1316 |