|
1 theory ML_Tactic |
|
2 imports Base Main |
|
3 begin |
|
4 |
|
5 chapter {* ML tactic expressions *} |
|
6 |
|
7 text {* |
|
8 Isar Proof methods closely resemble traditional tactics, when used |
|
9 in unstructured sequences of @{command "apply"} commands. |
|
10 Isabelle/Isar provides emulations for all major ML tactics of |
|
11 classic Isabelle --- mostly for the sake of easy porting of existing |
|
12 developments, as actual Isar proof texts would demand much less |
|
13 diversity of proof methods. |
|
14 |
|
15 Unlike tactic expressions in ML, Isar proof methods provide proper |
|
16 concrete syntax for additional arguments, options, modifiers etc. |
|
17 Thus a typical method text is usually more concise than the |
|
18 corresponding ML tactic. Furthermore, the Isar versions of classic |
|
19 Isabelle tactics often cover several variant forms by a single |
|
20 method with separate options to tune the behavior. For example, |
|
21 method @{method simp} replaces all of @{ML simp_tac}~/ @{ML |
|
22 asm_simp_tac}~/ @{ML full_simp_tac}~/ @{ML asm_full_simp_tac}, there |
|
23 is also concrete syntax for augmenting the Simplifier context (the |
|
24 current ``simpset'') in a convenient way. |
|
25 *} |
|
26 |
|
27 |
|
28 section {* Resolution tactics *} |
|
29 |
|
30 text {* |
|
31 Classic Isabelle provides several variant forms of tactics for |
|
32 single-step rule applications (based on higher-order resolution). |
|
33 The space of resolution tactics has the following main dimensions. |
|
34 |
|
35 \begin{enumerate} |
|
36 |
|
37 \item The ``mode'' of resolution: intro, elim, destruct, or forward |
|
38 (e.g.\ @{ML resolve_tac}, @{ML eresolve_tac}, @{ML dresolve_tac}, |
|
39 @{ML forward_tac}). |
|
40 |
|
41 \item Optional explicit instantiation (e.g.\ @{ML resolve_tac} vs.\ |
|
42 @{ML res_inst_tac}). |
|
43 |
|
44 \item Abbreviations for singleton arguments (e.g.\ @{ML resolve_tac} |
|
45 vs.\ @{ML rtac}). |
|
46 |
|
47 \end{enumerate} |
|
48 |
|
49 Basically, the set of Isar tactic emulations @{method rule_tac}, |
|
50 @{method erule_tac}, @{method drule_tac}, @{method frule_tac} (see |
|
51 \secref{sec:tactics}) would be sufficient to cover the four modes, |
|
52 either with or without instantiation, and either with single or |
|
53 multiple arguments. Although it is more convenient in most cases to |
|
54 use the plain @{method_ref (Pure) rule} method, or any of its |
|
55 ``improper'' variants @{method erule}, @{method drule}, @{method |
|
56 frule}. Note that explicit goal addressing is only supported by the |
|
57 actual @{method rule_tac} version. |
|
58 |
|
59 With this in mind, plain resolution tactics correspond to Isar |
|
60 methods as follows. |
|
61 |
|
62 \medskip |
|
63 \begin{tabular}{lll} |
|
64 @{ML rtac}~@{text "a 1"} & & @{text "rule a"} \\ |
|
65 @{ML resolve_tac}~@{text "[a\<^sub>1, \<dots>] 1"} & & @{text "rule a\<^sub>1 \<dots>"} \\ |
|
66 @{ML res_inst_tac}~@{text "ctxt [(x\<^sub>1, t\<^sub>1), \<dots>] a 1"} & & |
|
67 @{text "rule_tac x\<^sub>1 = t\<^sub>1 \<AND> \<dots> \<IN> a"} \\[0.5ex] |
|
68 @{ML rtac}~@{text "a i"} & & @{text "rule_tac [i] a"} \\ |
|
69 @{ML resolve_tac}~@{text "[a\<^sub>1, \<dots>] i"} & & @{text "rule_tac [i] a\<^sub>1 \<dots>"} \\ |
|
70 @{ML res_inst_tac}~@{text "ctxt [(x\<^sub>1, t\<^sub>1), \<dots>] a i"} & & |
|
71 @{text "rule_tac [i] x\<^sub>1 = t\<^sub>1 \<AND> \<dots> \<IN> a"} \\ |
|
72 \end{tabular} |
|
73 \medskip |
|
74 |
|
75 Note that explicit goal addressing may be usually avoided by |
|
76 changing the order of subgoals with @{command "defer"} or @{command |
|
77 "prefer"} (see \secref{sec:tactic-commands}). |
|
78 *} |
|
79 |
|
80 |
|
81 section {* Simplifier tactics *} |
|
82 |
|
83 text {* The main Simplifier tactics @{ML simp_tac} and variants are |
|
84 all covered by the @{method simp} and @{method simp_all} methods |
|
85 (see \secref{sec:simplifier}). Note that there is no individual |
|
86 goal addressing available, simplification acts either on the first |
|
87 goal (@{method simp}) or all goals (@{method simp_all}). |
|
88 |
|
89 \medskip |
|
90 \begin{tabular}{lll} |
|
91 @{ML asm_full_simp_tac}~@{text "@{context} 1"} & & @{method simp} \\ |
|
92 @{ML ALLGOALS}~(@{ML asm_full_simp_tac}~@{text "@{context}"}) & & @{method simp_all} \\[0.5ex] |
|
93 @{ML simp_tac}~@{text "@{context} 1"} & & @{method simp}~@{text "(no_asm)"} \\ |
|
94 @{ML asm_simp_tac}~@{text "@{context} 1"} & & @{method simp}~@{text "(no_asm_simp)"} \\ |
|
95 @{ML full_simp_tac}~@{text "@{context} 1"} & & @{method simp}~@{text "(no_asm_use)"} \\ |
|
96 @{ML asm_lr_simp_tac}~@{text "@{context} 1"} & & @{method simp}~@{text "(asm_lr)"} \\ |
|
97 \end{tabular} |
|
98 \medskip |
|
99 *} |
|
100 |
|
101 |
|
102 section {* Classical Reasoner tactics *} |
|
103 |
|
104 text {* The Classical Reasoner provides a rather large number of |
|
105 variations of automated tactics, such as @{ML blast_tac}, @{ML |
|
106 fast_tac}, @{ML clarify_tac} etc. The corresponding Isar methods |
|
107 usually share the same base name, such as @{method blast}, @{method |
|
108 fast}, @{method clarify} etc.\ (see \secref{sec:classical}). *} |
|
109 |
|
110 |
|
111 section {* Miscellaneous tactics *} |
|
112 |
|
113 text {* |
|
114 There are a few additional tactics defined in various theories of |
|
115 Isabelle/HOL, some of these also in Isabelle/FOL or Isabelle/ZF. |
|
116 The most common ones of these may be ported to Isar as follows. |
|
117 |
|
118 \medskip |
|
119 \begin{tabular}{lll} |
|
120 @{ML stac}~@{text "a 1"} & & @{text "subst a"} \\ |
|
121 @{ML hyp_subst_tac}~@{text 1} & & @{text hypsubst} \\ |
|
122 @{ML split_all_tac}~@{text 1} & & @{text "simp (no_asm_simp) only: split_tupled_all"} \\ |
|
123 & @{text "\<approx>"} & @{text "simp only: split_tupled_all"} \\ |
|
124 & @{text "\<lless>"} & @{text "clarify"} \\ |
|
125 \end{tabular} |
|
126 *} |
|
127 |
|
128 |
|
129 section {* Tacticals *} |
|
130 |
|
131 text {* |
|
132 Classic Isabelle provides a huge amount of tacticals for combination |
|
133 and modification of existing tactics. This has been greatly reduced |
|
134 in Isar, providing the bare minimum of combinators only: ``@{text |
|
135 ","}'' (sequential composition), ``@{text "|"}'' (alternative |
|
136 choices), ``@{text "?"}'' (try), ``@{text "+"}'' (repeat at least |
|
137 once). These are usually sufficient in practice; if all fails, |
|
138 arbitrary ML tactic code may be invoked via the @{method tactic} |
|
139 method (see \secref{sec:tactics}). |
|
140 |
|
141 \medskip Common ML tacticals may be expressed directly in Isar as |
|
142 follows: |
|
143 |
|
144 \medskip |
|
145 \begin{tabular}{lll} |
|
146 @{text "tac\<^sub>1"}~@{ML_text THEN}~@{text "tac\<^sub>2"} & & @{text "meth\<^sub>1, meth\<^sub>2"} \\ |
|
147 @{text "tac\<^sub>1"}~@{ML_text ORELSE}~@{text "tac\<^sub>2"} & & @{text "meth\<^sub>1 | meth\<^sub>2"} \\ |
|
148 @{ML TRY}~@{text tac} & & @{text "meth?"} \\ |
|
149 @{ML REPEAT1}~@{text tac} & & @{text "meth+"} \\ |
|
150 @{ML REPEAT}~@{text tac} & & @{text "(meth+)?"} \\ |
|
151 @{ML EVERY}~@{text "[tac\<^sub>1, \<dots>]"} & & @{text "meth\<^sub>1, \<dots>"} \\ |
|
152 @{ML FIRST}~@{text "[tac\<^sub>1, \<dots>]"} & & @{text "meth\<^sub>1 | \<dots>"} \\ |
|
153 \end{tabular} |
|
154 \medskip |
|
155 |
|
156 \medskip @{ML CHANGED} (see \cite{isabelle-implementation}) is |
|
157 usually not required in Isar, since most basic proof methods already |
|
158 fail unless there is an actual change in the goal state. |
|
159 Nevertheless, ``@{text "?"}'' (try) may be used to accept |
|
160 \emph{unchanged} results as well. |
|
161 |
|
162 \medskip @{ML ALLGOALS}, @{ML SOMEGOAL} etc.\ (see |
|
163 \cite{isabelle-implementation}) are not available in Isar, since |
|
164 there is no direct goal addressing. Nevertheless, some basic |
|
165 methods address all goals internally, notably @{method simp_all} |
|
166 (see \secref{sec:simplifier}). Also note that @{ML ALLGOALS} can be |
|
167 often replaced by ``@{text "+"}'' (repeat at least once), although |
|
168 this usually has a different operational behavior: subgoals are |
|
169 solved in a different order. |
|
170 |
|
171 \medskip Iterated resolution, such as |
|
172 @{ML_text "REPEAT (FIRSTGOAL (resolve_tac ...))"}, is usually better |
|
173 expressed using the @{method intro} and @{method elim} methods of |
|
174 Isar (see \secref{sec:classical}). |
|
175 *} |
|
176 |
|
177 end |