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