|
1 theory Tactical |
|
2 imports Advanced |
|
3 begin |
|
4 |
|
5 ML {* |
|
6 fun my_print_tac ctxt thm = |
|
7 let |
|
8 val _ = tracing (Pretty.string_of (pretty_thm_no_vars ctxt thm)) |
|
9 in |
|
10 Seq.single thm |
|
11 end |
|
12 *} |
|
13 |
|
14 ML {* |
|
15 let |
|
16 val ctxt = @{context} |
|
17 val goal = @{prop "P \<or> Q \<Longrightarrow> Q \<or> P"} |
|
18 in |
|
19 Goal.prove ctxt ["x", "y", "u", "v", "P", "Q"] [@{prop "x = y"}, @{prop "u = v"}] goal |
|
20 (fn {prems = pms, context = ctxt} => |
|
21 (my_print_tac ctxt) |
|
22 THEN etac @{thm disjE} 1 THEN |
|
23 (my_print_tac ctxt) |
|
24 THEN rtac @{thm disjI2} 1 |
|
25 THEN (my_print_tac ctxt) |
|
26 THEN atac 1 |
|
27 THEN rtac @{thm disjI1} 1 |
|
28 THEN atac 1) |
|
29 end |
|
30 *} |
|
31 |
|
32 ML {* |
|
33 Goal.prove |
|
34 *} |
|
35 |
|
36 ML {* |
|
37 fun pretty_cterms ctxt ctrms = |
|
38 Pretty.block (Pretty.commas (map (pretty_cterm ctxt) ctrms)) |
|
39 *} |
|
40 |
|
41 ML {* |
|
42 fun foc_tac {prems, params, asms, concl, context, schematics} = |
|
43 let |
|
44 fun assgn1 f1 f2 xs = |
|
45 let |
|
46 val out = map (fn (x, y) => Pretty.enum ":=" "" "" [f1 x, f2 y]) xs |
|
47 in |
|
48 Pretty.list "" "" out |
|
49 end |
|
50 fun assgn2 f xs = assgn1 f f xs |
|
51 val pps = map (fn (s, pp) => Pretty.block [Pretty.str s, pp]) |
|
52 [("params: ", assgn1 Pretty.str (pretty_cterm context) params), |
|
53 ("assumptions: ", pretty_cterms context asms), |
|
54 ("conclusion: ", pretty_cterm context concl), |
|
55 ("premises: ", pretty_thms_no_vars context prems), |
|
56 ("schematics: ", assgn2 (pretty_cterm context) (snd schematics))] |
|
57 in |
|
58 tracing (Pretty.string_of (Pretty.chunks pps)); all_tac |
|
59 end |
|
60 *} |
|
61 |
|
62 notation (output) "prop" ("#_" [1000] 1000) |
|
63 |
|
64 end |