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