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