1243 ML_prf {* Isar.goal () *}

  1243 thm APPLY_RSP

  1244 ML_prf {* val t = Thm.lift_rule (hd (cprems_of (Isar.goal ()))) @{thm "APPLY_RSP_I2" } *}

  1244 apply (rule_tac APPLY_RSP[of "op \<approx>" "ABS_fset" "REP_fset" "op =" "id" "id"])

  1245 ML_prf {*

  1246   val (tc') = (Logic.strip_assums_concl (prop_of t));

  1247   val ps = Logic.strip_params (prop_of t)

  1248   val tt = Term.list_abs (ps, tc')

  1249   val ct = cterm_of @{theory} tt

  1250 *}

  1251 ML_prf {*

  1252   val goal = hd (prems_of (Isar.goal ()))

  1253   val goalc = Logic.strip_assums_concl goal

  1254 *}

  1255 ML_prf {*

  1256   val goalct = cterm_of @{theory} (hd ( prems_of (Isar.goal ())))

  1257 *}

  1258 

  1259 ML_prf {*

  1260   val ps = Logic.strip_params goal

  1261   val goal' = cterm_of @{theory} (Term.list_abs (ps, goalc))

  1262   val goal'' = cterm_of @{theory} (Term.subst_bounds ((map Free ps), goalc))

  1263 *}

  1264 ML_prf {* ct; goal'' *}

  1265 

  1266 ML_prf {* val nlct = cterm_of @{theory} (concl_of @{thm "APPLY_RSP_I2" }) *}

  1267 

  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 *}) *)

  1273 ML_prf {* t *}

  1274 ML_prf {*

  1275   val man_inst =

  1276     Drule.instantiate' [SOME @{ctyp 'a}, SOME @{ctyp bool}] 

  1277       [

  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) y)"},

  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)))"}

  1282       ] t

  1283 *}

  1284 ML_prf {*

  1285   val (tc') = (Logic.strip_assums_concl (prop_of man_inst));

  1286   val ps = Logic.strip_params (prop_of man_inst)

  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 {* val man_inst_norm_r = Drule.beta_eta_conversion (cprop_of man_inst) *}

  1308 ML_prf {* val man_inst_norm = MetaSimplifier.rewrite_rule [man_inst_norm_r] man_inst *}

  1309 ML_prf {*

  1310   val (tc') = (Logic.strip_assums_concl (prop_of man_inst_norm));

  1311   val ps = Logic.strip_params (prop_of man_inst_norm)

  1312   val tt = Term.list_abs (ps, tc')

  1313   val ct = cterm_of @{theory} tt

  1314 *}

  1315 ML_prf {* Thm.match (ct, goal') *}

  1316 ML_prf {* PRIMSEQ *}

  1317 ML_prf {* man_inst_norm *}

  1318 apply (tactic {* compose_tac (false, man_inst_norm, 4) 1 *})

  1319 

  1339 thm APPLY_RSP

  1262 thm APPLY_RSP[of "op \<approx>" "ABS_fset" "REP_fset" "op =" "id" "id"]

  1263 apply (rule APPLY_RSP[of "op \<approx>" "ABS_fset" "REP_fset" "op =" "id" "id"])