equal
deleted
inserted
replaced
1357 |
1357 |
1358 ML_prf {* |
1358 ML_prf {* |
1359 val m = Thm.match (tc', gc') |
1359 val m = Thm.match (tc', gc') |
1360 *} |
1360 *} |
1361 (* FAILS: t2 = Drule.instantiate m @{thm "APPLY_RSP_II" }; rtac t2 1 *) |
1361 (* FAILS: t2 = Drule.instantiate m @{thm "APPLY_RSP_II" }; rtac t2 1 *) |
1362 (* Works but why does it take a string? *} |
1362 (* Works but why does it take a string? *) |
1363 apply (tactic {* res_inst_tac @{context} [(("f",0),"\<lambda>x. h # x"),(("g",0),"\<lambda>x. h # x")] @{thm "APPLY_RSP_II" } 1 *}) |
1363 ML_prf {* |
|
1364 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 |
|
1366 |
|
1367 *} |
|
1368 ML_prf dest_Var |
|
1369 apply (tactic {* res_inst_tac @{context} [(("f",0),"op # h"),(("g",0),"op # h")] @{thm "APPLY_RSP_II" } 1 *}) |
|
1370 ML_prf induct_tac |
1364 (*apply (rule_tac ?f="\<lambda>x. h # x" and ?g="\<lambda>x. h # x" in APPLY_RSP[of "op \<approx>" "ABS_fset" "REP_fset" "op \<approx>" "ABS_fset" "REP_fset"] )*) |
1371 (*apply (rule_tac ?f="\<lambda>x. h # x" and ?g="\<lambda>x. h # x" in APPLY_RSP[of "op \<approx>" "ABS_fset" "REP_fset" "op \<approx>" "ABS_fset" "REP_fset"] )*) |
1365 |
1372 |
1366 apply (rule QUOTIENT_fset) |
1373 apply (rule QUOTIENT_fset) |
1367 apply (rule QUOTIENT_fset) |
1374 apply (rule QUOTIENT_fset) |
1368 apply (rule_tac ?f="op #" and ?g="op #" in APPLY_RSP[of "op =" "id" "id" "op \<approx> ===> op \<approx>" "REP_fset ---> ABS_fset" "ABS_fset ---> REP_fset"]) |
1375 apply (rule_tac ?f="op #" and ?g="op #" in APPLY_RSP[of "op =" "id" "id" "op \<approx> ===> op \<approx>" "REP_fset ---> ABS_fset" "ABS_fset ---> REP_fset"]) |