11 J. Functional Programming. |
11 J. Functional Programming. |
12 *} |
12 *} |
13 |
13 |
14 method_setup depth_solve = {* |
14 method_setup depth_solve = {* |
15 Attrib.thms >> (fn thms => K (METHOD (fn facts => |
15 Attrib.thms >> (fn thms => K (METHOD (fn facts => |
16 (DEPTH_SOLVE (HEADGOAL (ares_tac (facts @ thms))))))) |
16 (DEPTH_SOLVE (HEADGOAL (ares_tac (facts @ thms))))))) |
17 *} "" |
17 *} |
18 |
18 |
19 method_setup depth_solve1 = {* |
19 method_setup depth_solve1 = {* |
20 Attrib.thms >> (fn thms => K (METHOD (fn facts => |
20 Attrib.thms >> (fn thms => K (METHOD (fn facts => |
21 (DEPTH_SOLVE_1 (HEADGOAL (ares_tac (facts @ thms))))))) |
21 (DEPTH_SOLVE_1 (HEADGOAL (ares_tac (facts @ thms))))))) |
22 *} "" |
22 *} |
23 |
23 |
24 method_setup strip_asms = {* |
24 method_setup strip_asms = {* |
25 Attrib.thms >> (fn thms => K (METHOD (fn facts => |
25 Attrib.thms >> (fn thms => K (METHOD (fn facts => |
26 REPEAT (resolve_tac [@{thm strip_b}, @{thm strip_s}] 1 THEN |
26 REPEAT (resolve_tac [@{thm strip_b}, @{thm strip_s}] 1 THEN |
27 DEPTH_SOLVE_1 (ares_tac (facts @ thms) 1))))) |
27 DEPTH_SOLVE_1 (ares_tac (facts @ thms) 1))))) |
28 *} "" |
28 *} |
29 |
29 |
30 |
30 |
31 subsection {* Simple types *} |
31 subsection {* Simple types *} |
32 |
32 |
33 schematic_lemma "A:* |- A->A : ?T" |
33 schematic_lemma "A:* |- A->A : ?T" |