93
+ − 1
theory Tactical
99
+ − 2
imports Base FirstSteps
93
+ − 3
begin
+ − 4
+ − 5
chapter {* Tactical Reasoning\label{chp:tactical} *}
+ − 6
+ − 7
text {*
213
+ − 8
One of the main reason for descending to the ML-level of Isabelle is to be able to
105
+ − 9
implement automatic proof procedures. Such proof procedures usually lessen
+ − 10
considerably the burden of manual reasoning, for example, when introducing
+ − 11
new definitions. These proof procedures are centred around refining a goal
+ − 12
state using tactics. This is similar to the \isacommand{apply}-style
157
+ − 13
reasoning at the user-level, where goals are modified in a sequence of proof
105
+ − 14
steps until all of them are solved. However, there are also more structured
+ − 15
operations available on the ML-level that help with the handling of
+ − 16
variables and assumptions.
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 17
93
+ − 18
*}
+ − 19
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 20
section {* Basics of Reasoning with Tactics*}
93
+ − 21
+ − 22
text {*
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 23
To see how tactics work, let us first transcribe a simple \isacommand{apply}-style proof
108
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 24
into ML. Suppose the following proof.
93
+ − 25
*}
+ − 26
+ − 27
lemma disj_swap: "P \<or> Q \<Longrightarrow> Q \<or> P"
+ − 28
apply(erule disjE)
+ − 29
apply(rule disjI2)
+ − 30
apply(assumption)
+ − 31
apply(rule disjI1)
+ − 32
apply(assumption)
+ − 33
done
+ − 34
+ − 35
text {*
+ − 36
This proof translates to the following ML-code.
+ − 37
+ − 38
@{ML_response_fake [display,gray]
+ − 39
"let
+ − 40
val ctxt = @{context}
+ − 41
val goal = @{prop \"P \<or> Q \<Longrightarrow> Q \<or> P\"}
+ − 42
in
+ − 43
Goal.prove ctxt [\"P\", \"Q\"] [] goal
+ − 44
(fn _ =>
+ − 45
etac @{thm disjE} 1
+ − 46
THEN rtac @{thm disjI2} 1
+ − 47
THEN atac 1
+ − 48
THEN rtac @{thm disjI1} 1
+ − 49
THEN atac 1)
+ − 50
end" "?P \<or> ?Q \<Longrightarrow> ?Q \<or> ?P"}
+ − 51
+ − 52
To start the proof, the function @{ML "Goal.prove"}~@{text "ctxt xs As C
99
+ − 53
tac"} sets up a goal state for proving the goal @{text C}
+ − 54
(that is @{prop "P \<or> Q \<Longrightarrow> Q \<or> P"} in the proof at hand) under the
+ − 55
assumptions @{text As} (happens to be empty) with the variables
93
+ − 56
@{text xs} that will be generalised once the goal is proved (in our case
+ − 57
@{text P} and @{text Q}). The @{text "tac"} is the tactic that proves the goal;
+ − 58
it can make use of the local assumptions (there are none in this example).
120
+ − 59
The functions @{ML etac}, @{ML rtac} and @{ML atac} in the code above correspond to
93
+ − 60
@{text erule}, @{text rule} and @{text assumption}, respectively.
105
+ − 61
The operator @{ML THEN} strings the tactics together.
93
+ − 62
+ − 63
\begin{readmore}
99
+ − 64
To learn more about the function @{ML Goal.prove} see \isccite{sec:results}
108
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 65
and the file @{ML_file "Pure/goal.ML"}. See @{ML_file
99
+ − 66
"Pure/tactic.ML"} and @{ML_file "Pure/tctical.ML"} for the code of basic
+ − 67
tactics and tactic combinators; see also Chapters 3 and 4 in the old
162
+ − 68
Isabelle Reference Manual, and Chapter 3 in the Isabelle/Isar Implementation Manual.
93
+ − 69
\end{readmore}
+ − 70
120
+ − 71
Note that in the code above we use antiquotations for referencing the theorems. Many theorems
105
+ − 72
also have ML-bindings with the same name. Therefore, we could also just have
118
+ − 73
written @{ML "etac disjE 1"}, or in case where there are no ML-binding obtain
107
+ − 74
the theorem dynamically using the function @{ML thm}; for example
109
+ − 75
\mbox{@{ML "etac (thm \"disjE\") 1"}}. Both ways however are considered bad style!
107
+ − 76
The reason
105
+ − 77
is that the binding for @{ML disjE} can be re-assigned by the user and thus
+ − 78
one does not have complete control over which theorem is actually
+ − 79
applied. This problem is nicely prevented by using antiquotations, because
+ − 80
then the theorems are fixed statically at compile-time.
93
+ − 81
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 82
During the development of automatic proof procedures, you will often find it
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 83
necessary to test a tactic on examples. This can be conveniently
93
+ − 84
done with the command \isacommand{apply}@{text "(tactic \<verbopen> \<dots> \<verbclose>)"}.
+ − 85
Consider the following sequence of tactics
+ − 86
*}
+ − 87
+ − 88
ML{*val foo_tac =
+ − 89
(etac @{thm disjE} 1
+ − 90
THEN rtac @{thm disjI2} 1
+ − 91
THEN atac 1
+ − 92
THEN rtac @{thm disjI1} 1
+ − 93
THEN atac 1)*}
+ − 94
+ − 95
text {* and the Isabelle proof: *}
+ − 96
+ − 97
lemma "P \<or> Q \<Longrightarrow> Q \<or> P"
+ − 98
apply(tactic {* foo_tac *})
+ − 99
done
+ − 100
+ − 101
text {*
104
+ − 102
By using @{text "tactic \<verbopen> \<dots> \<verbclose>"} you can call from the
157
+ − 103
user-level of Isabelle the tactic @{ML foo_tac} or
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 104
any other function that returns a tactic.
93
+ − 105
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 106
The tactic @{ML foo_tac} is just a sequence of simple tactics stringed
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 107
together by @{ML THEN}. As can be seen, each simple tactic in @{ML foo_tac}
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 108
has a hard-coded number that stands for the subgoal analysed by the
105
+ − 109
tactic (@{text "1"} stands for the first, or top-most, subgoal). This hard-coding
+ − 110
of goals is sometimes wanted, but usually it is not. To avoid the explicit numbering,
107
+ − 111
you can write\label{tac:footacprime}
93
+ − 112
*}
+ − 113
+ − 114
ML{*val foo_tac' =
+ − 115
(etac @{thm disjE}
+ − 116
THEN' rtac @{thm disjI2}
+ − 117
THEN' atac
+ − 118
THEN' rtac @{thm disjI1}
+ − 119
THEN' atac)*}
+ − 120
+ − 121
text {*
213
+ − 122
where @{ML THEN'} is used instead of @{ML THEN}. With @{ML foo_tac'} you can give
+ − 123
the number for the subgoal explicitly when the tactic is
105
+ − 124
called. So in the next proof you can first discharge the second subgoal, and
109
+ − 125
subsequently the first.
93
+ − 126
*}
+ − 127
+ − 128
lemma "P1 \<or> Q1 \<Longrightarrow> Q1 \<or> P1"
+ − 129
and "P2 \<or> Q2 \<Longrightarrow> Q2 \<or> P2"
+ − 130
apply(tactic {* foo_tac' 2 *})
+ − 131
apply(tactic {* foo_tac' 1 *})
+ − 132
done
+ − 133
+ − 134
text {*
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 135
This kind of addressing is more difficult to achieve when the goal is
108
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 136
hard-coded inside the tactic. For most operators that combine tactics
105
+ − 137
(@{ML THEN} is only one such operator) a ``primed'' version exists.
99
+ − 138
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 139
The tactics @{ML foo_tac} and @{ML foo_tac'} are very specific for
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 140
analysing goals being only of the form @{prop "P \<or> Q \<Longrightarrow> Q \<or> P"}. If the goal is not
186
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 141
of this form, then these tactics return the error message:
99
+ − 142
+ − 143
\begin{isabelle}
+ − 144
@{text "*** empty result sequence -- proof command failed"}\\
+ − 145
@{text "*** At command \"apply\"."}
+ − 146
\end{isabelle}
+ − 147
186
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 148
This means they failed. The reason for this error message is that tactics
109
+ − 149
are functions mapping a goal state to a (lazy) sequence of successor states.
+ − 150
Hence the type of a tactic is:
+ − 151
*}
93
+ − 152
109
+ − 153
ML{*type tactic = thm -> thm Seq.seq*}
93
+ − 154
109
+ − 155
text {*
+ − 156
By convention, if a tactic fails, then it should return the empty sequence.
+ − 157
Therefore, if you write your own tactics, they should not raise exceptions
+ − 158
willy-nilly; only in very grave failure situations should a tactic raise the
+ − 159
exception @{text THM}.
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 160
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 161
The simplest tactics are @{ML no_tac} and @{ML all_tac}. The first returns
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 162
the empty sequence and is defined as
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 163
*}
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 164
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 165
ML{*fun no_tac thm = Seq.empty*}
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 166
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 167
text {*
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 168
which means @{ML no_tac} always fails. The second returns the given theorem wrapped
173
+ − 169
in a single member sequence; it is defined as
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 170
*}
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 171
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 172
ML{*fun all_tac thm = Seq.single thm*}
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 173
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 174
text {*
109
+ − 175
which means @{ML all_tac} always succeeds, but also does not make any progress
+ − 176
with the proof.
93
+ − 177
109
+ − 178
The lazy list of possible successor goal states shows through at the user-level
99
+ − 179
of Isabelle when using the command \isacommand{back}. For instance in the
108
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 180
following proof there are two possibilities for how to apply
107
+ − 181
@{ML foo_tac'}: either using the first assumption or the second.
93
+ − 182
*}
+ − 183
+ − 184
lemma "\<lbrakk>P \<or> Q; P \<or> Q\<rbrakk> \<Longrightarrow> Q \<or> P"
+ − 185
apply(tactic {* foo_tac' 1 *})
+ − 186
back
+ − 187
done
+ − 188
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 189
93
+ − 190
text {*
99
+ − 191
By using \isacommand{back}, we construct the proof that uses the
109
+ − 192
second assumption. While in the proof above, it does not really matter which
+ − 193
assumption is used, in more interesting cases provability might depend
+ − 194
on exploring different possibilities.
99
+ − 195
93
+ − 196
\begin{readmore}
+ − 197
See @{ML_file "Pure/General/seq.ML"} for the implementation of lazy
109
+ − 198
sequences. In day-to-day Isabelle programming, however, one rarely
+ − 199
constructs sequences explicitly, but uses the predefined tactics and
+ − 200
tactic combinators instead.
93
+ − 201
\end{readmore}
+ − 202
104
+ − 203
It might be surprising that tactics, which transform
109
+ − 204
one goal state to the next, are functions from theorems to theorem
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 205
(sequences). The surprise resolves by knowing that every
104
+ − 206
goal state is indeed a theorem. To shed more light on this,
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 207
let us modify the code of @{ML all_tac} to obtain the following
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 208
tactic
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 209
*}
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 210
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 211
ML{*fun my_print_tac ctxt thm =
132
+ − 212
let
194
+ − 213
val _ = warning (str_of_thm_no_vars ctxt thm)
132
+ − 214
in
+ − 215
Seq.single thm
+ − 216
end*}
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 217
109
+ − 218
text_raw {*
+ − 219
\begin{figure}[p]
173
+ − 220
\begin{boxedminipage}{\textwidth}
109
+ − 221
\begin{isabelle}
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 222
*}
105
+ − 223
lemma shows "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B"
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 224
apply(tactic {* my_print_tac @{context} *})
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 225
109
+ − 226
txt{* \begin{minipage}{\textwidth}
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 227
@{subgoals [display]}
109
+ − 228
\end{minipage}\medskip
+ − 229
+ − 230
\begin{minipage}{\textwidth}
+ − 231
\small\colorbox{gray!20}{
+ − 232
\begin{tabular}{@ {}l@ {}}
+ − 233
internal goal state:\\
108
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 234
@{text "(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B)"}
109
+ − 235
\end{tabular}}
+ − 236
\end{minipage}\medskip
93
+ − 237
*}
+ − 238
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 239
apply(rule conjI)
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 240
apply(tactic {* my_print_tac @{context} *})
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 241
109
+ − 242
txt{* \begin{minipage}{\textwidth}
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 243
@{subgoals [display]}
109
+ − 244
\end{minipage}\medskip
+ − 245
+ − 246
\begin{minipage}{\textwidth}
+ − 247
\small\colorbox{gray!20}{
+ − 248
\begin{tabular}{@ {}l@ {}}
+ − 249
internal goal state:\\
108
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 250
@{text "(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> B) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B)"}
109
+ − 251
\end{tabular}}
+ − 252
\end{minipage}\medskip
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 253
*}
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 254
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 255
apply(assumption)
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 256
apply(tactic {* my_print_tac @{context} *})
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 257
109
+ − 258
txt{* \begin{minipage}{\textwidth}
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 259
@{subgoals [display]}
109
+ − 260
\end{minipage}\medskip
+ − 261
+ − 262
\begin{minipage}{\textwidth}
+ − 263
\small\colorbox{gray!20}{
+ − 264
\begin{tabular}{@ {}l@ {}}
+ − 265
internal goal state:\\
108
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 266
@{text "(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> B) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B)"}
109
+ − 267
\end{tabular}}
+ − 268
\end{minipage}\medskip
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 269
*}
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 270
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 271
apply(assumption)
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 272
apply(tactic {* my_print_tac @{context} *})
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 273
109
+ − 274
txt{* \begin{minipage}{\textwidth}
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 275
@{subgoals [display]}
109
+ − 276
\end{minipage}\medskip
+ − 277
+ − 278
\begin{minipage}{\textwidth}
+ − 279
\small\colorbox{gray!20}{
+ − 280
\begin{tabular}{@ {}l@ {}}
+ − 281
internal goal state:\\
108
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 282
@{text "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B"}
109
+ − 283
\end{tabular}}
+ − 284
\end{minipage}\medskip
+ − 285
*}
+ − 286
done
+ − 287
text_raw {*
+ − 288
\end{isabelle}
173
+ − 289
\end{boxedminipage}
118
+ − 290
\caption{The figure shows a proof where each intermediate goal state is
+ − 291
printed by the Isabelle system and by @{ML my_print_tac}. The latter shows
+ − 292
the goal state as represented internally (highlighted boxes). This
173
+ − 293
tactic shows that every goal state in Isabelle is represented by a theorem:
156
+ − 294
when you start the proof of \mbox{@{text "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B"}} the theorem is
+ − 295
@{text "(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B)"}; when you finish the proof the
118
+ − 296
theorem is @{text "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B"}.\label{fig:goalstates}}
109
+ − 297
\end{figure}
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 298
*}
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 299
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 300
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 301
text {*
109
+ − 302
which prints out the given theorem (using the string-function defined in
+ − 303
Section~\ref{sec:printing}) and then behaves like @{ML all_tac}. With this
+ − 304
tactic we are in the position to inspect every goal state in a
+ − 305
proof. Consider now the proof in Figure~\ref{fig:goalstates}: as can be seen,
+ − 306
internally every goal state is an implication of the form
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 307
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 308
@{text[display] "A\<^isub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^isub>n \<Longrightarrow> (C)"}
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 309
109
+ − 310
where @{term C} is the goal to be proved and the @{term "A\<^isub>i"} are
+ − 311
the subgoals. So after setting up the lemma, the goal state is always of the
+ − 312
form @{text "C \<Longrightarrow> (C)"}; when the proof is finished we are left with @{text
+ − 313
"(C)"}. Since the goal @{term C} can potentially be an implication, there is
213
+ − 314
a ``protector'' wrapped around it (the wrapper is the outermost constant @{text
120
+ − 315
"Const (\"prop\", bool \<Rightarrow> bool)"}; however this constant
149
+ − 316
is invisible in the figure). This wrapper prevents that premises of @{text C} are
109
+ − 317
mis-interpreted as open subgoals. While tactics can operate on the subgoals
+ − 318
(the @{text "A\<^isub>i"} above), they are expected to leave the conclusion
+ − 319
@{term C} intact, with the exception of possibly instantiating schematic
+ − 320
variables. If you use the predefined tactics, which we describe in the next
+ − 321
section, this will always be the case.
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 322
108
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 323
\begin{readmore}
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 324
For more information about the internals of goals see \isccite{sec:tactical-goals}.
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 325
\end{readmore}
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 326
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 327
*}
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 328
194
+ − 329
section {* Simple Tactics\label{sec:simpletacs} *}
93
+ − 330
99
+ − 331
text {*
173
+ − 332
Let us start with explaining the simple tactic @{ML print_tac}, which is quite useful
+ − 333
for low-level debugging of tactics. It just prints out a message and the current
+ − 334
goal state. Unlike @{ML my_print_tac} shown earlier, it prints the goal state
+ − 335
as the user would see it. For example, processing the proof
105
+ − 336
*}
+ − 337
+ − 338
lemma shows "False \<Longrightarrow> True"
+ − 339
apply(tactic {* print_tac "foo message" *})
109
+ − 340
txt{*gives:\medskip
+ − 341
+ − 342
\begin{minipage}{\textwidth}\small
107
+ − 343
@{text "foo message"}\\[3mm]
+ − 344
@{prop "False \<Longrightarrow> True"}\\
+ − 345
@{text " 1. False \<Longrightarrow> True"}\\
+ − 346
\end{minipage}
+ − 347
*}
105
+ − 348
(*<*)oops(*>*)
+ − 349
+ − 350
text {*
213
+ − 351
A simple tactic for easy discharge of any proof obligations is
192
+ − 352
@{ML SkipProof.cheat_tac}. This tactic corresponds to
+ − 353
the Isabelle command \isacommand{sorry} and is sometimes useful
+ − 354
during the development of tactics.
+ − 355
*}
+ − 356
213
+ − 357
lemma shows "False" and "Goldbach_conjecture"
192
+ − 358
apply(tactic {* SkipProof.cheat_tac @{theory} *})
+ − 359
txt{*\begin{minipage}{\textwidth}
+ − 360
@{subgoals [display]}
+ − 361
\end{minipage}*}
+ − 362
(*<*)oops(*>*)
+ − 363
+ − 364
text {*
105
+ − 365
Another simple tactic is the function @{ML atac}, which, as shown in the previous
+ − 366
section, corresponds to the assumption command.
99
+ − 367
*}
+ − 368
+ − 369
lemma shows "P \<Longrightarrow> P"
93
+ − 370
apply(tactic {* atac 1 *})
109
+ − 371
txt{*\begin{minipage}{\textwidth}
+ − 372
@{subgoals [display]}
+ − 373
\end{minipage}*}
+ − 374
(*<*)oops(*>*)
93
+ − 375
99
+ − 376
text {*
+ − 377
Similarly, @{ML rtac}, @{ML dtac}, @{ML etac} and @{ML ftac} correspond
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 378
to @{text rule}, @{text drule}, @{text erule} and @{text frule},
213
+ − 379
respectively. Each of them take a theorem as argument and attempt to
109
+ − 380
apply it to a goal. Below are three self-explanatory examples.
99
+ − 381
*}
+ − 382
+ − 383
lemma shows "P \<and> Q"
93
+ − 384
apply(tactic {* rtac @{thm conjI} 1 *})
104
+ − 385
txt{*\begin{minipage}{\textwidth}
+ − 386
@{subgoals [display]}
+ − 387
\end{minipage}*}
93
+ − 388
(*<*)oops(*>*)
+ − 389
99
+ − 390
lemma shows "P \<and> Q \<Longrightarrow> False"
93
+ − 391
apply(tactic {* etac @{thm conjE} 1 *})
104
+ − 392
txt{*\begin{minipage}{\textwidth}
+ − 393
@{subgoals [display]}
+ − 394
\end{minipage}*}
93
+ − 395
(*<*)oops(*>*)
+ − 396
+ − 397
lemma shows "False \<and> True \<Longrightarrow> False"
+ − 398
apply(tactic {* dtac @{thm conjunct2} 1 *})
104
+ − 399
txt{*\begin{minipage}{\textwidth}
+ − 400
@{subgoals [display]}
+ − 401
\end{minipage}*}
93
+ − 402
(*<*)oops(*>*)
+ − 403
+ − 404
text {*
105
+ − 405
The function @{ML resolve_tac} is similar to @{ML rtac}, except that it
+ − 406
expects a list of theorems as arguments. From this list it will apply the
+ − 407
first applicable theorem (later theorems that are also applicable can be
+ − 408
explored via the lazy sequences mechanism). Given the code
93
+ − 409
*}
+ − 410
99
+ − 411
ML{*val resolve_tac_xmp = resolve_tac [@{thm impI}, @{thm conjI}]*}
+ − 412
+ − 413
text {*
+ − 414
an example for @{ML resolve_tac} is the following proof where first an outermost
+ − 415
implication is analysed and then an outermost conjunction.
+ − 416
*}
+ − 417
+ − 418
lemma shows "C \<longrightarrow> (A \<and> B)" and "(A \<longrightarrow> B) \<and> C"
+ − 419
apply(tactic {* resolve_tac_xmp 1 *})
+ − 420
apply(tactic {* resolve_tac_xmp 2 *})
104
+ − 421
txt{*\begin{minipage}{\textwidth}
+ − 422
@{subgoals [display]}
+ − 423
\end{minipage}*}
99
+ − 424
(*<*)oops(*>*)
+ − 425
+ − 426
text {*
186
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 427
Similar versions taking a list of theorems exist for the tactics
109
+ − 428
@{ML dtac} (@{ML dresolve_tac}), @{ML etac} (@{ML eresolve_tac}) and so on.
+ − 429
105
+ − 430
107
+ − 431
Another simple tactic is @{ML cut_facts_tac}. It inserts a list of theorems
109
+ − 432
into the assumptions of the current goal state. For example
107
+ − 433
*}
99
+ − 434
107
+ − 435
lemma shows "True \<noteq> False"
+ − 436
apply(tactic {* cut_facts_tac [@{thm True_def}, @{thm False_def}] 1 *})
109
+ − 437
txt{*produces the goal state\medskip
+ − 438
+ − 439
\begin{minipage}{\textwidth}
107
+ − 440
@{subgoals [display]}
+ − 441
\end{minipage}*}
+ − 442
(*<*)oops(*>*)
+ − 443
+ − 444
text {*
105
+ − 445
Since rules are applied using higher-order unification, an automatic proof
108
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 446
procedure might become too fragile, if it just applies inference rules as
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 447
shown above. The reason is that a number of rules introduce meta-variables
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 448
into the goal state. Consider for example the proof
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 449
*}
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 450
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 451
lemma shows "\<forall>x\<in>A. P x \<Longrightarrow> Q x"
118
+ − 452
apply(tactic {* dtac @{thm bspec} 1 *})
108
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 453
txt{*\begin{minipage}{\textwidth}
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 454
@{subgoals [display]}
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 455
\end{minipage}*}
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 456
(*<*)oops(*>*)
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 457
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 458
text {*
149
+ − 459
where the application of rule @{text bspec} generates two subgoals involving the
109
+ − 460
meta-variable @{text "?x"}. Now, if you are not careful, tactics
108
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 461
applied to the first subgoal might instantiate this meta-variable in such a
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 462
way that the second subgoal becomes unprovable. If it is clear what the @{text "?x"}
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 463
should be, then this situation can be avoided by introducing a more
109
+ − 464
constraint version of the @{text bspec}-rule. Such constraints can be given by
+ − 465
pre-instantiating theorems with other theorems. One function to do this is
+ − 466
@{ML RS}
105
+ − 467
+ − 468
@{ML_response_fake [display,gray]
+ − 469
"@{thm disjI1} RS @{thm conjI}" "\<lbrakk>?P1; ?Q\<rbrakk> \<Longrightarrow> (?P1 \<or> ?Q1) \<and> ?Q"}
+ − 470
109
+ − 471
which in the example instantiates the first premise of the @{text conjI}-rule
+ − 472
with the rule @{text disjI1}. If the instantiation is impossible, as in the
+ − 473
case of
107
+ − 474
+ − 475
@{ML_response_fake_both [display,gray]
+ − 476
"@{thm conjI} RS @{thm mp}"
+ − 477
"*** Exception- THM (\"RSN: no unifiers\", 1,
+ − 478
[\"\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q\", \"\<lbrakk>?P \<longrightarrow> ?Q; ?P\<rbrakk> \<Longrightarrow> ?Q\"]) raised"}
+ − 479
109
+ − 480
then the function raises an exception. The function @{ML RSN} is similar to @{ML RS}, but
+ − 481
takes an additional number as argument that makes explicit which premise
107
+ − 482
should be instantiated.
+ − 483
213
+ − 484
To improve readability of the theorems we shall produce below, we will use the
158
d7944bdf7b3f
removed infix_conv and moved function no_vars into the FirstSteps chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 485
function @{ML no_vars} from Section~\ref{sec:printing}, which transforms
d7944bdf7b3f
removed infix_conv and moved function no_vars into the FirstSteps chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 486
schematic variables into free ones. Using this function for the first @{ML
d7944bdf7b3f
removed infix_conv and moved function no_vars into the FirstSteps chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 487
RS}-expression above produces the more readable result:
105
+ − 488
+ − 489
@{ML_response_fake [display,gray]
+ − 490
"no_vars @{context} (@{thm disjI1} RS @{thm conjI})" "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> (P \<or> Qa) \<and> Q"}
+ − 491
107
+ − 492
If you want to instantiate more than one premise of a theorem, you can use
+ − 493
the function @{ML MRS}:
105
+ − 494
+ − 495
@{ML_response_fake [display,gray]
+ − 496
"no_vars @{context} ([@{thm disjI1}, @{thm disjI2}] MRS @{thm conjI})"
+ − 497
"\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> (P \<or> Qa) \<and> (Pa \<or> Q)"}
+ − 498
+ − 499
If you need to instantiate lists of theorems, you can use the
109
+ − 500
functions @{ML RL} and @{ML MRL}. For example in the code below,
+ − 501
every theorem in the second list is instantiated with every
+ − 502
theorem in the first.
105
+ − 503
+ − 504
@{ML_response_fake [display,gray]
209
+ − 505
"map (no_vars @{context})
+ − 506
([@{thm impI}, @{thm disjI2}] RL [@{thm conjI}, @{thm disjI1}])"
105
+ − 507
"[\<lbrakk>P \<Longrightarrow> Q; Qa\<rbrakk> \<Longrightarrow> (P \<longrightarrow> Q) \<and> Qa,
+ − 508
\<lbrakk>Q; Qa\<rbrakk> \<Longrightarrow> (P \<or> Q) \<and> Qa,
+ − 509
(P \<Longrightarrow> Q) \<Longrightarrow> (P \<longrightarrow> Q) \<or> Qa,
+ − 510
Q \<Longrightarrow> (P \<or> Q) \<or> Qa]"}
+ − 511
+ − 512
\begin{readmore}
+ − 513
The combinators for instantiating theorems are defined in @{ML_file "Pure/drule.ML"}.
+ − 514
\end{readmore}
95
+ − 515
109
+ − 516
Often proofs on the ML-level involve elaborate operations on assumptions and
+ − 517
@{text "\<And>"}-quantified variables. To do such operations using the basic tactics
128
+ − 518
shown so far is very unwieldy and brittle. Some convenience and
99
+ − 519
safety is provided by the tactic @{ML SUBPROOF}. This tactic fixes the parameters
109
+ − 520
and binds the various components of a goal state to a record.
105
+ − 521
To see what happens, assume the function defined in Figure~\ref{fig:sptac}, which
109
+ − 522
takes a record and just prints out the content of this record (using the
+ − 523
string transformation functions from in Section~\ref{sec:printing}). Consider
+ − 524
now the proof:
95
+ − 525
*}
+ − 526
99
+ − 527
text_raw{*
173
+ − 528
\begin{figure}[t]
177
+ − 529
\begin{minipage}{\textwidth}
99
+ − 530
\begin{isabelle}
+ − 531
*}
95
+ − 532
ML{*fun sp_tac {prems, params, asms, concl, context, schematics} =
132
+ − 533
let
+ − 534
val str_of_params = str_of_cterms context params
+ − 535
val str_of_asms = str_of_cterms context asms
+ − 536
val str_of_concl = str_of_cterm context concl
194
+ − 537
val str_of_prems = str_of_thms_no_vars context prems
132
+ − 538
val str_of_schms = str_of_cterms context (snd schematics)
95
+ − 539
132
+ − 540
val _ = (warning ("params: " ^ str_of_params);
+ − 541
warning ("schematics: " ^ str_of_schms);
+ − 542
warning ("assumptions: " ^ str_of_asms);
+ − 543
warning ("conclusion: " ^ str_of_concl);
+ − 544
warning ("premises: " ^ str_of_prems))
+ − 545
in
+ − 546
no_tac
+ − 547
end*}
99
+ − 548
text_raw{*
+ − 549
\end{isabelle}
177
+ − 550
\end{minipage}
99
+ − 551
\caption{A function that prints out the various parameters provided by the tactic
105
+ − 552
@{ML SUBPROOF}. It uses the functions defined in Section~\ref{sec:printing} for
+ − 553
extracting strings from @{ML_type cterm}s and @{ML_type thm}s.\label{fig:sptac}}
99
+ − 554
\end{figure}
+ − 555
*}
95
+ − 556
+ − 557
99
+ − 558
lemma shows "\<And>x y. A x y \<Longrightarrow> B y x \<longrightarrow> C (?z y) x"
95
+ − 559
apply(tactic {* SUBPROOF sp_tac @{context} 1 *})?
+ − 560
+ − 561
txt {*
109
+ − 562
The tactic produces the following printout:
95
+ − 563
99
+ − 564
\begin{quote}\small
95
+ − 565
\begin{tabular}{ll}
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 566
params: & @{term x}, @{term y}\\
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 567
schematics: & @{term z}\\
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 568
assumptions: & @{term "A x y"}\\
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 569
conclusion: & @{term "B y x \<longrightarrow> C (z y) x"}\\
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 570
premises: & @{term "A x y"}
95
+ − 571
\end{tabular}
99
+ − 572
\end{quote}
+ − 573
149
+ − 574
Notice in the actual output the brown colour of the variables @{term x} and
105
+ − 575
@{term y}. Although they are parameters in the original goal, they are fixed inside
109
+ − 576
the subproof. By convention these fixed variables are printed in brown colour.
+ − 577
Similarly the schematic variable @{term z}. The assumption, or premise,
105
+ − 578
@{prop "A x y"} is bound as @{ML_type cterm} to the record-variable
109
+ − 579
@{text asms}, but also as @{ML_type thm} to @{text prems}.
95
+ − 580
109
+ − 581
Notice also that we had to append @{text [quotes] "?"} to the
+ − 582
\isacommand{apply}-command. The reason is that @{ML SUBPROOF} normally
+ − 583
expects that the subgoal is solved completely. Since in the function @{ML
+ − 584
sp_tac} we returned the tactic @{ML no_tac}, the subproof obviously
+ − 585
fails. The question-mark allows us to recover from this failure in a
+ − 586
graceful manner so that the warning messages are not overwritten by an
+ − 587
``empty sequence'' error message.
99
+ − 588
+ − 589
If we continue the proof script by applying the @{text impI}-rule
95
+ − 590
*}
+ − 591
+ − 592
apply(rule impI)
+ − 593
apply(tactic {* SUBPROOF sp_tac @{context} 1 *})?
+ − 594
+ − 595
txt {*
118
+ − 596
then the tactic prints out:
95
+ − 597
99
+ − 598
\begin{quote}\small
95
+ − 599
\begin{tabular}{ll}
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 600
params: & @{term x}, @{term y}\\
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 601
schematics: & @{term z}\\
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 602
assumptions: & @{term "A x y"}, @{term "B y x"}\\
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 603
conclusion: & @{term "C (z y) x"}\\
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 604
premises: & @{term "A x y"}, @{term "B y x"}
95
+ − 605
\end{tabular}
99
+ − 606
\end{quote}
95
+ − 607
*}
+ − 608
(*<*)oops(*>*)
+ − 609
99
+ − 610
text {*
109
+ − 611
Now also @{term "B y x"} is an assumption bound to @{text asms} and @{text prems}.
99
+ − 612
105
+ − 613
One convenience of @{ML SUBPROOF} is that we can apply the assumptions
99
+ − 614
using the usual tactics, because the parameter @{text prems}
109
+ − 615
contains them as theorems. With this you can easily
+ − 616
implement a tactic that behaves almost like @{ML atac}:
99
+ − 617
*}
+ − 618
104
+ − 619
ML{*val atac' = SUBPROOF (fn {prems, ...} => resolve_tac prems 1)*}
107
+ − 620
+ − 621
text {*
109
+ − 622
If you apply @{ML atac'} to the next lemma
107
+ − 623
*}
+ − 624
109
+ − 625
lemma shows "\<lbrakk>B x y; A x y; C x y\<rbrakk> \<Longrightarrow> A x y"
104
+ − 626
apply(tactic {* atac' @{context} 1 *})
109
+ − 627
txt{* it will produce
99
+ − 628
@{subgoals [display]} *}
+ − 629
(*<*)oops(*>*)
+ − 630
104
+ − 631
text {*
109
+ − 632
The restriction in this tactic which is not present in @{ML atac} is
+ − 633
that it cannot instantiate any
107
+ − 634
schematic variable. This might be seen as a defect, but it is actually
104
+ − 635
an advantage in the situations for which @{ML SUBPROOF} was designed:
109
+ − 636
the reason is that, as mentioned before, instantiation of schematic variables can affect
104
+ − 637
several goals and can render them unprovable. @{ML SUBPROOF} is meant
+ − 638
to avoid this.
+ − 639
109
+ − 640
Notice that @{ML atac'} inside @{ML SUBPROOF} calls @{ML resolve_tac} with
+ − 641
the subgoal number @{text "1"} and also the outer call to @{ML SUBPROOF} in
+ − 642
the \isacommand{apply}-step uses @{text "1"}. This is another advantage
+ − 643
of @{ML SUBPROOF}: the addressing inside it is completely
+ − 644
local to the tactic inside the subproof. It is therefore possible to also apply
107
+ − 645
@{ML atac'} to the second goal by just writing:
104
+ − 646
*}
+ − 647
109
+ − 648
lemma shows "True" and "\<lbrakk>B x y; A x y; C x y\<rbrakk> \<Longrightarrow> A x y"
104
+ − 649
apply(tactic {* atac' @{context} 2 *})
105
+ − 650
apply(rule TrueI)
+ − 651
done
104
+ − 652
95
+ − 653
93
+ − 654
text {*
105
+ − 655
\begin{readmore}
+ − 656
The function @{ML SUBPROOF} is defined in @{ML_file "Pure/subgoal.ML"} and
+ − 657
also described in \isccite{sec:results}.
+ − 658
\end{readmore}
+ − 659
151
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 660
Similar but less powerful functions than @{ML SUBPROOF} are @{ML SUBGOAL}
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 661
and @{ML CSUBGOAL}. They allow you to inspect a given subgoal (the former
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 662
presents the subgoal as a @{ML_type term}, while the latter as a @{ML_type
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 663
cterm}). With this you can implement a tactic that applies a rule according
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 664
to the topmost logic connective in the subgoal (to illustrate this we only
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 665
analyse a few connectives). The code of the tactic is as
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 666
follows.\label{tac:selecttac}
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 667
93
+ − 668
*}
+ − 669
151
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 670
ML %linenosgray{*fun select_tac (t, i) =
99
+ − 671
case t of
151
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 672
@{term "Trueprop"} $ t' => select_tac (t', i)
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 673
| @{term "op \<Longrightarrow>"} $ _ $ t' => select_tac (t', i)
99
+ − 674
| @{term "op \<and>"} $ _ $ _ => rtac @{thm conjI} i
+ − 675
| @{term "op \<longrightarrow>"} $ _ $ _ => rtac @{thm impI} i
+ − 676
| @{term "Not"} $ _ => rtac @{thm notI} i
+ − 677
| Const (@{const_name "All"}, _) $ _ => rtac @{thm allI} i
104
+ − 678
| _ => all_tac*}
99
+ − 679
105
+ − 680
text {*
109
+ − 681
The input of the function is a term representing the subgoal and a number
186
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 682
specifying the subgoal of interest. In Line 3 you need to descend under the
109
+ − 683
outermost @{term "Trueprop"} in order to get to the connective you like to
+ − 684
analyse. Otherwise goals like @{prop "A \<and> B"} are not properly
+ − 685
analysed. Similarly with meta-implications in the next line. While for the
+ − 686
first five patterns we can use the @{text "@term"}-antiquotation to
+ − 687
construct the patterns, the pattern in Line 8 cannot be constructed in this
+ − 688
way. The reason is that an antiquotation would fix the type of the
+ − 689
quantified variable. So you really have to construct the pattern using the
156
+ − 690
basic term-constructors. This is not necessary in other cases, because their
+ − 691
type is always fixed to function types involving only the type @{typ
+ − 692
bool}. (See Section \ref{sec:terms_types_manually} about constructing terms
+ − 693
manually.) For the catch-all pattern, we chose to just return @{ML all_tac}.
+ − 694
Consequently, @{ML select_tac} never fails.
+ − 695
105
+ − 696
107
+ − 697
Let us now see how to apply this tactic. Consider the four goals:
105
+ − 698
*}
+ − 699
+ − 700
+ − 701
lemma shows "A \<and> B" and "A \<longrightarrow> B \<longrightarrow>C" and "\<forall>x. D x" and "E \<Longrightarrow> F"
104
+ − 702
apply(tactic {* SUBGOAL select_tac 4 *})
+ − 703
apply(tactic {* SUBGOAL select_tac 3 *})
+ − 704
apply(tactic {* SUBGOAL select_tac 2 *})
99
+ − 705
apply(tactic {* SUBGOAL select_tac 1 *})
107
+ − 706
txt{* \begin{minipage}{\textwidth}
+ − 707
@{subgoals [display]}
+ − 708
\end{minipage} *}
99
+ − 709
(*<*)oops(*>*)
+ − 710
+ − 711
text {*
107
+ − 712
where in all but the last the tactic applied an introduction rule.
109
+ − 713
Note that we applied the tactic to the goals in ``reverse'' order.
+ − 714
This is a trick in order to be independent from the subgoals that are
+ − 715
produced by the rule. If we had applied it in the other order
105
+ − 716
*}
+ − 717
+ − 718
lemma shows "A \<and> B" and "A \<longrightarrow> B \<longrightarrow>C" and "\<forall>x. D x" and "E \<Longrightarrow> F"
+ − 719
apply(tactic {* SUBGOAL select_tac 1 *})
+ − 720
apply(tactic {* SUBGOAL select_tac 3 *})
+ − 721
apply(tactic {* SUBGOAL select_tac 4 *})
+ − 722
apply(tactic {* SUBGOAL select_tac 5 *})
+ − 723
(*<*)oops(*>*)
99
+ − 724
105
+ − 725
text {*
109
+ − 726
then we have to be careful to not apply the tactic to the two subgoals produced by
+ − 727
the first goal. To do this can result in quite messy code. In contrast,
107
+ − 728
the ``reverse application'' is easy to implement.
104
+ − 729
151
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 730
Of course, this example is
149
+ − 731
contrived: there are much simpler methods available in Isabelle for
+ − 732
implementing a proof procedure analysing a goal according to its topmost
+ − 733
connective. These simpler methods use tactic combinators, which we will
+ − 734
explain in the next section.
147
+ − 735
105
+ − 736
*}
+ − 737
+ − 738
section {* Tactic Combinators *}
+ − 739
+ − 740
text {*
109
+ − 741
The purpose of tactic combinators is to build compound tactics out of
+ − 742
smaller tactics. In the previous section we already used @{ML THEN}, which
+ − 743
just strings together two tactics in a sequence. For example:
93
+ − 744
*}
+ − 745
105
+ − 746
lemma shows "(Foo \<and> Bar) \<and> False"
+ − 747
apply(tactic {* rtac @{thm conjI} 1 THEN rtac @{thm conjI} 1 *})
+ − 748
txt {* \begin{minipage}{\textwidth}
+ − 749
@{subgoals [display]}
+ − 750
\end{minipage} *}
+ − 751
(*<*)oops(*>*)
99
+ − 752
105
+ − 753
text {*
213
+ − 754
If you want to avoid the hard-coded subgoal addressing, then, as
+ − 755
seen earlier, you can use
108
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 756
the ``primed'' version of @{ML THEN}. For example:
105
+ − 757
*}
93
+ − 758
99
+ − 759
lemma shows "(Foo \<and> Bar) \<and> False"
105
+ − 760
apply(tactic {* (rtac @{thm conjI} THEN' rtac @{thm conjI}) 1 *})
+ − 761
txt {* \begin{minipage}{\textwidth}
+ − 762
@{subgoals [display]}
+ − 763
\end{minipage} *}
93
+ − 764
(*<*)oops(*>*)
+ − 765
105
+ − 766
text {*
213
+ − 767
Here you have to specify the subgoal of interest only once and
109
+ − 768
it is consistently applied to the component tactics.
107
+ − 769
For most tactic combinators such a ``primed'' version exists and
+ − 770
in what follows we will usually prefer it over the ``unprimed'' one.
+ − 771
+ − 772
If there is a list of tactics that should all be tried out in
+ − 773
sequence, you can use the combinator @{ML EVERY'}. For example
109
+ − 774
the function @{ML foo_tac'} from page~\pageref{tac:footacprime} can also
108
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 775
be written as:
107
+ − 776
*}
+ − 777
+ − 778
ML{*val foo_tac'' = EVERY' [etac @{thm disjE}, rtac @{thm disjI2},
+ − 779
atac, rtac @{thm disjI1}, atac]*}
105
+ − 780
107
+ − 781
text {*
109
+ − 782
There is even another way of implementing this tactic: in automatic proof
+ − 783
procedures (in contrast to tactics that might be called by the user) there
+ − 784
are often long lists of tactics that are applied to the first
+ − 785
subgoal. Instead of writing the code above and then calling @{ML "foo_tac'' 1"},
+ − 786
you can also just write
107
+ − 787
*}
+ − 788
+ − 789
ML{*val foo_tac1 = EVERY1 [etac @{thm disjE}, rtac @{thm disjI2},
108
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 790
atac, rtac @{thm disjI1}, atac]*}
107
+ − 791
+ − 792
text {*
118
+ − 793
and call @{ML foo_tac1}.
109
+ − 794
+ − 795
With the combinators @{ML THEN'}, @{ML EVERY'} and @{ML EVERY1} it must be
+ − 796
guaranteed that all component tactics successfully apply; otherwise the
+ − 797
whole tactic will fail. If you rather want to try out a number of tactics,
+ − 798
then you can use the combinator @{ML ORELSE'} for two tactics, and @{ML
+ − 799
FIRST'} (or @{ML FIRST1}) for a list of tactics. For example, the tactic
+ − 800
105
+ − 801
*}
+ − 802
131
+ − 803
ML{*val orelse_xmp = rtac @{thm disjI1} ORELSE' rtac @{thm conjI}*}
99
+ − 804
105
+ − 805
text {*
107
+ − 806
will first try out whether rule @{text disjI} applies and after that
109
+ − 807
@{text conjI}. To see this consider the proof
105
+ − 808
*}
+ − 809
99
+ − 810
lemma shows "True \<and> False" and "Foo \<or> Bar"
108
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 811
apply(tactic {* orelse_xmp 2 *})
99
+ − 812
apply(tactic {* orelse_xmp 1 *})
107
+ − 813
txt {* which results in the goal state
+ − 814
+ − 815
\begin{minipage}{\textwidth}
+ − 816
@{subgoals [display]}
+ − 817
\end{minipage}
+ − 818
*}
93
+ − 819
(*<*)oops(*>*)
+ − 820
+ − 821
+ − 822
text {*
109
+ − 823
Using @{ML FIRST'} we can simplify our @{ML select_tac} from Page~\pageref{tac:selecttac}
+ − 824
as follows:
107
+ − 825
*}
+ − 826
+ − 827
ML{*val select_tac' = FIRST' [rtac @{thm conjI}, rtac @{thm impI},
+ − 828
rtac @{thm notI}, rtac @{thm allI}, K all_tac]*}
+ − 829
+ − 830
text {*
108
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 831
Since we like to mimic the behaviour of @{ML select_tac} as closely as possible,
109
+ − 832
we must include @{ML all_tac} at the end of the list, otherwise the tactic will
118
+ − 833
fail if no rule applies (we also have to wrap @{ML all_tac} using the
109
+ − 834
@{ML K}-combinator, because it does not take a subgoal number as argument). You can
+ − 835
test the tactic on the same goals:
107
+ − 836
*}
+ − 837
+ − 838
lemma shows "A \<and> B" and "A \<longrightarrow> B \<longrightarrow>C" and "\<forall>x. D x" and "E \<Longrightarrow> F"
+ − 839
apply(tactic {* select_tac' 4 *})
+ − 840
apply(tactic {* select_tac' 3 *})
+ − 841
apply(tactic {* select_tac' 2 *})
+ − 842
apply(tactic {* select_tac' 1 *})
+ − 843
txt{* \begin{minipage}{\textwidth}
+ − 844
@{subgoals [display]}
+ − 845
\end{minipage} *}
+ − 846
(*<*)oops(*>*)
+ − 847
+ − 848
text {*
109
+ − 849
Since such repeated applications of a tactic to the reverse order of
+ − 850
\emph{all} subgoals is quite common, there is the tactic combinator
+ − 851
@{ML ALLGOALS} that simplifies this. Using this combinator you can simply
108
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 852
write: *}
107
+ − 853
+ − 854
lemma shows "A \<and> B" and "A \<longrightarrow> B \<longrightarrow>C" and "\<forall>x. D x" and "E \<Longrightarrow> F"
+ − 855
apply(tactic {* ALLGOALS select_tac' *})
+ − 856
txt{* \begin{minipage}{\textwidth}
+ − 857
@{subgoals [display]}
+ − 858
\end{minipage} *}
+ − 859
(*<*)oops(*>*)
+ − 860
+ − 861
text {*
109
+ − 862
Remember that we chose to implement @{ML select_tac'} so that it
+ − 863
always succeeds. This can be potentially very confusing for the user,
+ − 864
for example, in cases where the goal is the form
107
+ − 865
*}
+ − 866
+ − 867
lemma shows "E \<Longrightarrow> F"
+ − 868
apply(tactic {* select_tac' 1 *})
+ − 869
txt{* \begin{minipage}{\textwidth}
+ − 870
@{subgoals [display]}
+ − 871
\end{minipage} *}
+ − 872
(*<*)oops(*>*)
+ − 873
+ − 874
text {*
109
+ − 875
In this case no rule applies. The problem for the user is that there is little
+ − 876
chance to see whether or not progress in the proof has been made. By convention
+ − 877
therefore, tactics visible to the user should either change something or fail.
+ − 878
+ − 879
To comply with this convention, we could simply delete the @{ML "K all_tac"}
+ − 880
from the end of the theorem list. As a result @{ML select_tac'} would only
+ − 881
succeed on goals where it can make progress. But for the sake of argument,
+ − 882
let us suppose that this deletion is \emph{not} an option. In such cases, you can
+ − 883
use the combinator @{ML CHANGED} to make sure the subgoal has been changed
+ − 884
by the tactic. Because now
+ − 885
107
+ − 886
*}
+ − 887
+ − 888
lemma shows "E \<Longrightarrow> F"
+ − 889
apply(tactic {* CHANGED (select_tac' 1) *})(*<*)?(*>*)
109
+ − 890
txt{* gives the error message:
108
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 891
\begin{isabelle}
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 892
@{text "*** empty result sequence -- proof command failed"}\\
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 893
@{text "*** At command \"apply\"."}
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 894
\end{isabelle}
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 895
*}(*<*)oops(*>*)
105
+ − 896
+ − 897
107
+ − 898
text {*
109
+ − 899
We can further extend @{ML select_tac'} so that it not just applies to the topmost
+ − 900
connective, but also to the ones immediately ``underneath'', i.e.~analyse the goal
+ − 901
completely. For this you can use the tactic combinator @{ML REPEAT}. As an example
+ − 902
suppose the following tactic
108
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 903
*}
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 904
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 905
ML{*val repeat_xmp = REPEAT (CHANGED (select_tac' 1)) *}
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 906
109
+ − 907
text {* which applied to the proof *}
108
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 908
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 909
lemma shows "((\<not>A) \<and> (\<forall>x. B x)) \<and> (C \<longrightarrow> D)"
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 910
apply(tactic {* repeat_xmp *})
109
+ − 911
txt{* produces
+ − 912
+ − 913
\begin{minipage}{\textwidth}
108
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 914
@{subgoals [display]}
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 915
\end{minipage} *}
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 916
(*<*)oops(*>*)
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 917
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 918
text {*
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 919
Here it is crucial that @{ML select_tac'} is prefixed with @{ML CHANGED},
109
+ − 920
because otherwise @{ML REPEAT} runs into an infinite loop (it applies the
+ − 921
tactic as long as it succeeds). The function
108
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 922
@{ML REPEAT1} is similar, but runs the tactic at least once (failing if
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 923
this is not possible).
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 924
156
+ − 925
If you are after the ``primed'' version of @{ML repeat_xmp}, then you
109
+ − 926
need to implement it as
108
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 927
*}
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 928
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 929
ML{*val repeat_xmp' = REPEAT o CHANGED o select_tac'*}
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 930
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 931
text {*
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 932
since there are no ``primed'' versions of @{ML REPEAT} and @{ML CHANGED}.
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 933
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 934
If you look closely at the goal state above, the tactics @{ML repeat_xmp}
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 935
and @{ML repeat_xmp'} are not yet quite what we are after: the problem is
109
+ − 936
that goals 2 and 3 are not analysed. This is because the tactic
+ − 937
is applied repeatedly only to the first subgoal. To analyse also all
+ − 938
resulting subgoals, you can use the tactic combinator @{ML REPEAT_ALL_NEW}.
108
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 939
Suppose the tactic
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 940
*}
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 941
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 942
ML{*val repeat_all_new_xmp = REPEAT_ALL_NEW (CHANGED o select_tac')*}
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 943
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 944
text {*
109
+ − 945
you see that the following goal
108
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 946
*}
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 947
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 948
lemma shows "((\<not>A) \<and> (\<forall>x. B x)) \<and> (C \<longrightarrow> D)"
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 949
apply(tactic {* repeat_all_new_xmp 1 *})
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 950
txt{* \begin{minipage}{\textwidth}
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 951
@{subgoals [display]}
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 952
\end{minipage} *}
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 953
(*<*)oops(*>*)
93
+ − 954
108
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 955
text {*
109
+ − 956
is completely analysed according to the theorems we chose to
120
+ − 957
include in @{ML select_tac'}.
109
+ − 958
+ − 959
Recall that tactics produce a lazy sequence of successor goal states. These
108
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 960
states can be explored using the command \isacommand{back}. For example
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 961
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 962
*}
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 963
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 964
lemma "\<lbrakk>P1 \<or> Q1; P2 \<or> Q2\<rbrakk> \<Longrightarrow> R"
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 965
apply(tactic {* etac @{thm disjE} 1 *})
109
+ − 966
txt{* applies the rule to the first assumption yielding the goal state:\smallskip
108
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 967
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 968
\begin{minipage}{\textwidth}
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 969
@{subgoals [display]}
109
+ − 970
\end{minipage}\smallskip
+ − 971
+ − 972
After typing
+ − 973
*}
108
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 974
(*<*)
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 975
oops
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 976
lemma "\<lbrakk>P1 \<or> Q1; P2 \<or> Q2\<rbrakk> \<Longrightarrow> R"
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 977
apply(tactic {* etac @{thm disjE} 1 *})
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 978
(*>*)
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 979
back
109
+ − 980
txt{* the rule now applies to the second assumption.\smallskip
108
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 981
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 982
\begin{minipage}{\textwidth}
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 983
@{subgoals [display]}
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 984
\end{minipage} *}
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 985
(*<*)oops(*>*)
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 986
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 987
text {*
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 988
Sometimes this leads to confusing behaviour of tactics and also has
109
+ − 989
the potential to explode the search space for tactics.
+ − 990
These problems can be avoided by prefixing the tactic with the tactic
+ − 991
combinator @{ML DETERM}.
108
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 992
*}
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 993
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 994
lemma "\<lbrakk>P1 \<or> Q1; P2 \<or> Q2\<rbrakk> \<Longrightarrow> R"
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 995
apply(tactic {* DETERM (etac @{thm disjE} 1) *})
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 996
txt {*\begin{minipage}{\textwidth}
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 997
@{subgoals [display]}
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 998
\end{minipage} *}
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 999
(*<*)oops(*>*)
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1000
text {*
118
+ − 1001
This combinator will prune the search space to just the first successful application.
108
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1002
Attempting to apply \isacommand{back} in this goal states gives the
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1003
error message:
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1004
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1005
\begin{isabelle}
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1006
@{text "*** back: no alternatives"}\\
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1007
@{text "*** At command \"back\"."}
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1008
\end{isabelle}
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1009
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1010
\begin{readmore}
109
+ − 1011
Most tactic combinators described in this section are defined in @{ML_file "Pure/tctical.ML"}.
108
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1012
\end{readmore}
107
+ − 1013
105
+ − 1014
*}
+ − 1015
158
d7944bdf7b3f
removed infix_conv and moved function no_vars into the FirstSteps chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1016
section {* Simplifier Tactics *}
105
+ − 1017
+ − 1018
text {*
152
+ − 1019
A lot of convenience in the reasoning with Isabelle derives from its
162
+ − 1020
powerful simplifier. The power of simplifier is a strength and a weakness at
+ − 1021
the same time, because you can easily make the simplifier to run into a loop and its
+ − 1022
behaviour can be difficult to predict. There is also a multitude
+ − 1023
of options that you can configurate to control the behaviour of the simplifier.
+ − 1024
We describe some of them in this and the next section.
157
+ − 1025
+ − 1026
There are the following five main tactics behind
162
+ − 1027
the simplifier (in parentheses is their user-level counterpart):
152
+ − 1028
+ − 1029
\begin{isabelle}
157
+ − 1030
\begin{center}
152
+ − 1031
\begin{tabular}{l@ {\hspace{2cm}}l}
+ − 1032
@{ML simp_tac} & @{text "(simp (no_asm))"} \\
+ − 1033
@{ML asm_simp_tac} & @{text "(simp (no_asm_simp))"} \\
+ − 1034
@{ML full_simp_tac} & @{text "(simp (no_asm_use))"} \\
+ − 1035
@{ML asm_lr_simp_tac} & @{text "(simp (asm_lr))"} \\
+ − 1036
@{ML asm_full_simp_tac} & @{text "(simp)"}
+ − 1037
\end{tabular}
157
+ − 1038
\end{center}
152
+ − 1039
\end{isabelle}
+ − 1040
162
+ − 1041
All of the tactics take a simpset and an interger as argument (the latter as usual
+ − 1042
to specify the goal to be analysed). So the proof
152
+ − 1043
*}
+ − 1044
+ − 1045
lemma "Suc (1 + 2) < 3 + 2"
+ − 1046
apply(simp)
+ − 1047
done
+ − 1048
+ − 1049
text {*
157
+ − 1050
corresponds on the ML-level to the tactic
152
+ − 1051
*}
+ − 1052
+ − 1053
lemma "Suc (1 + 2) < 3 + 2"
+ − 1054
apply(tactic {* asm_full_simp_tac @{simpset} 1 *})
+ − 1055
done
+ − 1056
+ − 1057
text {*
162
+ − 1058
If the simplifier cannot make any progress, then it leaves the goal unchanged,
209
+ − 1059
i.e., does not raise any error message. That means if you use it to unfold a
162
+ − 1060
definition for a constant and this constant is not present in the goal state,
+ − 1061
you can still safely apply the simplifier.
152
+ − 1062
162
+ − 1063
When using the simplifier, the crucial information you have to provide is
+ − 1064
the simpset. If this information is not handled with care, then the
+ − 1065
simplifier can easily run into a loop. Therefore a good rule of thumb is to
+ − 1066
use simpsets that are as minimal as possible. It might be surprising that a
+ − 1067
simpset is more complex than just a simple collection of theorems used as
+ − 1068
simplification rules. One reason for the complexity is that the simplifier
+ − 1069
must be able to rewrite inside terms and should also be able to rewrite
+ − 1070
according to rules that have precoditions.
157
+ − 1071
+ − 1072
+ − 1073
The rewriting inside terms requires congruence rules, which
+ − 1074
are meta-equalities typical of the form
152
+ − 1075
+ − 1076
\begin{isabelle}
157
+ − 1077
\begin{center}
162
+ − 1078
\mbox{\inferrule{@{text "t\<^isub>1 \<equiv> s\<^isub>1 \<dots> t\<^isub>n \<equiv> s\<^isub>n"}}
157
+ − 1079
{@{text "constr t\<^isub>1\<dots>t\<^isub>n \<equiv> constr s\<^isub>1\<dots>s\<^isub>n"}}}
+ − 1080
\end{center}
152
+ − 1081
\end{isabelle}
+ − 1082
162
+ − 1083
with @{text "constr"} being a term-constructor, like @{const "If"} or @{const "Let"}.
+ − 1084
Every simpset contains only
157
+ − 1085
one concruence rule for each term-constructor, which however can be
+ − 1086
overwritten. The user can declare lemmas to be congruence rules using the
+ − 1087
attribute @{text "[cong]"}. In HOL, the user usually states these lemmas as
+ − 1088
equations, which are then internally transformed into meta-equations.
+ − 1089
+ − 1090
+ − 1091
The rewriting with rules involving preconditions requires what is in
+ − 1092
Isabelle called a subgoaler, a solver and a looper. These can be arbitrary
162
+ − 1093
tactics that can be installed in a simpset and which are called during
+ − 1094
various stages during simplification. However, simpsets also include
157
+ − 1095
simprocs, which can produce rewrite rules on demand (see next
+ − 1096
section). Another component are split-rules, which can simplify for example
+ − 1097
the ``then'' and ``else'' branches of if-statements under the corresponding
+ − 1098
precoditions.
+ − 1099
162
+ − 1100
157
+ − 1101
\begin{readmore}
+ − 1102
For more information about the simplifier see @{ML_file "Pure/meta_simplifier.ML"}
+ − 1103
and @{ML_file "Pure/simplifier.ML"}. The simplifier for HOL is set up in
+ − 1104
@{ML_file "HOL/Tools/simpdata.ML"}. Generic splitters are implemented in
+ − 1105
@{ML_file "Provers/splitter.ML"}.
+ − 1106
\end{readmore}
152
+ − 1107
160
cc9359bfacf4
redefined the functions warning and tracing in order to properly match more antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1108
\begin{readmore}
209
+ − 1109
FIXME: Find the right place: Discrimination nets are implemented
160
cc9359bfacf4
redefined the functions warning and tracing in order to properly match more antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1110
in @{ML_file "Pure/net.ML"}.
cc9359bfacf4
redefined the functions warning and tracing in order to properly match more antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1111
\end{readmore}
cc9359bfacf4
redefined the functions warning and tracing in order to properly match more antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1112
209
+ − 1113
The most common combinators to modify simpsets are:
152
+ − 1114
+ − 1115
\begin{isabelle}
+ − 1116
\begin{tabular}{ll}
157
+ − 1117
@{ML addsimps} & @{ML delsimps}\\
+ − 1118
@{ML addcongs} & @{ML delcongs}\\
+ − 1119
@{ML addsimprocs} & @{ML delsimprocs}\\
152
+ − 1120
\end{tabular}
+ − 1121
\end{isabelle}
+ − 1122
157
+ − 1123
(FIXME: What about splitters? @{ML addsplits}, @{ML delsplits})
+ − 1124
*}
+ − 1125
+ − 1126
text_raw {*
173
+ − 1127
\begin{figure}[t]
177
+ − 1128
\begin{minipage}{\textwidth}
157
+ − 1129
\begin{isabelle}*}
163
2319cff107f0
removed rep_ss, and used dest_ss instead; some very slight changes to simple_inductive
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1130
ML{*fun print_ss ctxt ss =
157
+ − 1131
let
163
2319cff107f0
removed rep_ss, and used dest_ss instead; some very slight changes to simple_inductive
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1132
val {simps, congs, procs, ...} = MetaSimplifier.dest_ss ss
157
+ − 1133
+ − 1134
fun name_thm (nm, thm) =
194
+ − 1135
" " ^ nm ^ ": " ^ (str_of_thm_no_vars ctxt thm)
163
2319cff107f0
removed rep_ss, and used dest_ss instead; some very slight changes to simple_inductive
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1136
fun name_ctrm (nm, ctrm) =
2319cff107f0
removed rep_ss, and used dest_ss instead; some very slight changes to simple_inductive
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1137
" " ^ nm ^ ": " ^ (str_of_cterms ctxt ctrm)
157
+ − 1138
210
+ − 1139
val s = ["Simplification rules:"] @ (map name_thm simps) @
+ − 1140
["Congruences rules:"] @ (map name_thm congs) @
+ − 1141
["Simproc patterns:"] @ (map name_ctrm procs)
157
+ − 1142
in
210
+ − 1143
s |> separate "\n"
+ − 1144
|> implode
+ − 1145
|> warning
157
+ − 1146
end*}
+ − 1147
text_raw {*
+ − 1148
\end{isabelle}
177
+ − 1149
\end{minipage}
163
2319cff107f0
removed rep_ss, and used dest_ss instead; some very slight changes to simple_inductive
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1150
\caption{The function @{ML MetaSimplifier.dest_ss} returns a record containing
2319cff107f0
removed rep_ss, and used dest_ss instead; some very slight changes to simple_inductive
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1151
all printable information stored in a simpset. We are here only interested in the
2319cff107f0
removed rep_ss, and used dest_ss instead; some very slight changes to simple_inductive
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1152
simplifcation rules, congruence rules and simprocs.\label{fig:printss}}
157
+ − 1153
\end{figure} *}
+ − 1154
+ − 1155
text {*
186
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1156
To see how they work, consider the function in Figure~\ref{fig:printss}, which
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1157
prints out some parts of a simpset. If you use it to print out the components of the
209
+ − 1158
empty simpset, i.e., @{ML empty_ss}
157
+ − 1159
+ − 1160
@{ML_response_fake [display,gray]
163
2319cff107f0
removed rep_ss, and used dest_ss instead; some very slight changes to simple_inductive
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1161
"print_ss @{context} empty_ss"
157
+ − 1162
"Simplification rules:
163
2319cff107f0
removed rep_ss, and used dest_ss instead; some very slight changes to simple_inductive
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1163
Congruences rules:
2319cff107f0
removed rep_ss, and used dest_ss instead; some very slight changes to simple_inductive
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1164
Simproc patterns:"}
157
+ − 1165
+ − 1166
you can see it contains nothing. This simpset is usually not useful, except as a
+ − 1167
building block to build bigger simpsets. For example you can add to @{ML empty_ss}
+ − 1168
the simplification rule @{thm [source] Diff_Int} as follows:
152
+ − 1169
*}
+ − 1170
157
+ − 1171
ML{*val ss1 = empty_ss addsimps [@{thm Diff_Int} RS @{thm eq_reflection}] *}
+ − 1172
+ − 1173
text {*
162
+ − 1174
Printing then out the components of the simpset gives:
153
+ − 1175
157
+ − 1176
@{ML_response_fake [display,gray]
163
2319cff107f0
removed rep_ss, and used dest_ss instead; some very slight changes to simple_inductive
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1177
"print_ss @{context} ss1"
157
+ − 1178
"Simplification rules:
158
d7944bdf7b3f
removed infix_conv and moved function no_vars into the FirstSteps chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1179
??.unknown: A - B \<inter> C \<equiv> A - B \<union> (A - C)
163
2319cff107f0
removed rep_ss, and used dest_ss instead; some very slight changes to simple_inductive
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1180
Congruences rules:
2319cff107f0
removed rep_ss, and used dest_ss instead; some very slight changes to simple_inductive
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1181
Simproc patterns:"}
157
+ − 1182
158
d7944bdf7b3f
removed infix_conv and moved function no_vars into the FirstSteps chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1183
(FIXME: Why does it print out ??.unknown)
d7944bdf7b3f
removed infix_conv and moved function no_vars into the FirstSteps chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1184
162
+ − 1185
Adding also the congruence rule @{thm [source] UN_cong}
153
+ − 1186
*}
+ − 1187
157
+ − 1188
ML{*val ss2 = ss1 addcongs [@{thm UN_cong} RS @{thm eq_reflection}] *}
+ − 1189
+ − 1190
text {*
+ − 1191
gives
+ − 1192
+ − 1193
@{ML_response_fake [display,gray]
163
2319cff107f0
removed rep_ss, and used dest_ss instead; some very slight changes to simple_inductive
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1194
"print_ss @{context} ss2"
157
+ − 1195
"Simplification rules:
158
d7944bdf7b3f
removed infix_conv and moved function no_vars into the FirstSteps chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1196
??.unknown: A - B \<inter> C \<equiv> A - B \<union> (A - C)
157
+ − 1197
Congruences rules:
163
2319cff107f0
removed rep_ss, and used dest_ss instead; some very slight changes to simple_inductive
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1198
UNION: \<lbrakk>A = B; \<And>x. x \<in> B \<Longrightarrow> C x = D x\<rbrakk> \<Longrightarrow> \<Union>x\<in>A. C x \<equiv> \<Union>x\<in>B. D x
2319cff107f0
removed rep_ss, and used dest_ss instead; some very slight changes to simple_inductive
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1199
Simproc patterns:"}
157
+ − 1200
+ − 1201
Notice that we had to add these lemmas as meta-equations. The @{ML empty_ss}
+ − 1202
expects this form of the simplification and congruence rules. However, even
162
+ − 1203
when adding these lemmas to @{ML empty_ss} we do not end up with anything useful yet.
157
+ − 1204
162
+ − 1205
In the context of HOL, the first really useful simpset is @{ML HOL_basic_ss}. While
157
+ − 1206
printing out the components of this simpset
+ − 1207
+ − 1208
@{ML_response_fake [display,gray]
163
2319cff107f0
removed rep_ss, and used dest_ss instead; some very slight changes to simple_inductive
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1209
"print_ss @{context} HOL_basic_ss"
157
+ − 1210
"Simplification rules:
163
2319cff107f0
removed rep_ss, and used dest_ss instead; some very slight changes to simple_inductive
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1211
Congruences rules:
2319cff107f0
removed rep_ss, and used dest_ss instead; some very slight changes to simple_inductive
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1212
Simproc patterns:"}
157
+ − 1213
+ − 1214
also produces ``nothing'', the printout is misleading. In fact
162
+ − 1215
the @{ML HOL_basic_ss} is setup so that it can solve goals of the
186
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1216
form
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1217
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1218
\begin{isabelle}
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1219
@{thm TrueI}, @{thm refl[no_vars]}, @{term "t \<equiv> t"} and @{thm FalseE[no_vars]};
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1220
\end{isabelle}
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1221
162
+ − 1222
and also resolve with assumptions. For example:
157
+ − 1223
*}
+ − 1224
+ − 1225
lemma
+ − 1226
"True" and "t = t" and "t \<equiv> t" and "False \<Longrightarrow> Foo" and "\<lbrakk>A; B; C\<rbrakk> \<Longrightarrow> A"
+ − 1227
apply(tactic {* ALLGOALS (simp_tac HOL_basic_ss) *})
+ − 1228
done
+ − 1229
+ − 1230
text {*
162
+ − 1231
This behaviour is not because of simplification rules, but how the subgoaler, solver
186
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1232
and looper are set up in @{ML HOL_basic_ss}.
157
+ − 1233
162
+ − 1234
The simpset @{ML HOL_ss} is an extention of @{ML HOL_basic_ss} containing
+ − 1235
already many useful simplification and congruence rules for the logical
+ − 1236
connectives in HOL.
157
+ − 1237
+ − 1238
@{ML_response_fake [display,gray]
163
2319cff107f0
removed rep_ss, and used dest_ss instead; some very slight changes to simple_inductive
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1239
"print_ss @{context} HOL_ss"
157
+ − 1240
"Simplification rules:
158
d7944bdf7b3f
removed infix_conv and moved function no_vars into the FirstSteps chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1241
Pure.triv_forall_equality: (\<And>x. PROP V) \<equiv> PROP V
d7944bdf7b3f
removed infix_conv and moved function no_vars into the FirstSteps chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1242
HOL.the_eq_trivial: THE x. x = y \<equiv> y
d7944bdf7b3f
removed infix_conv and moved function no_vars into the FirstSteps chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1243
HOL.the_sym_eq_trivial: THE ya. y = ya \<equiv> y
157
+ − 1244
\<dots>
+ − 1245
Congruences rules:
+ − 1246
HOL.simp_implies: \<dots>
158
d7944bdf7b3f
removed infix_conv and moved function no_vars into the FirstSteps chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1247
\<Longrightarrow> (PROP P =simp=> PROP Q) \<equiv> (PROP P' =simp=> PROP Q')
163
2319cff107f0
removed rep_ss, and used dest_ss instead; some very slight changes to simple_inductive
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1248
op -->: \<lbrakk>P \<equiv> P'; P' \<Longrightarrow> Q \<equiv> Q'\<rbrakk> \<Longrightarrow> P \<longrightarrow> Q \<equiv> P' \<longrightarrow> Q'
2319cff107f0
removed rep_ss, and used dest_ss instead; some very slight changes to simple_inductive
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1249
Simproc patterns:
2319cff107f0
removed rep_ss, and used dest_ss instead; some very slight changes to simple_inductive
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1250
\<dots>"}
157
+ − 1251
+ − 1252
162
+ − 1253
The simplifier is often used to unfold definitions in a proof. For this the
+ − 1254
simplifier contains the @{ML rewrite_goals_tac}. Suppose for example the
+ − 1255
definition
+ − 1256
*}
+ − 1257
+ − 1258
definition "MyTrue \<equiv> True"
+ − 1259
186
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1260
text {*
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1261
then in the following proof we can unfold this constant
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1262
*}
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1263
162
+ − 1264
lemma shows "MyTrue \<Longrightarrow> True \<and> True"
+ − 1265
apply(rule conjI)
213
+ − 1266
apply(tactic {* rewrite_goals_tac @{thms MyTrue_def} *})
186
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1267
txt{* producing the goal state
162
+ − 1268
+ − 1269
\begin{minipage}{\textwidth}
+ − 1270
@{subgoals [display]}
+ − 1271
\end{minipage} *}
+ − 1272
(*<*)oops(*>*)
+ − 1273
+ − 1274
text {*
+ − 1275
As you can see, the tactic unfolds the definitions in all subgoals.
153
+ − 1276
*}
+ − 1277
+ − 1278
157
+ − 1279
text_raw {*
173
+ − 1280
\begin{figure}[p]
+ − 1281
\begin{boxedminipage}{\textwidth}
157
+ − 1282
\begin{isabelle} *}
+ − 1283
types prm = "(nat \<times> nat) list"
+ − 1284
consts perm :: "prm \<Rightarrow> 'a \<Rightarrow> 'a" ("_ \<bullet> _" [80,80] 80)
+ − 1285
+ − 1286
primrec (perm_nat)
+ − 1287
"[]\<bullet>c = c"
162
+ − 1288
"(ab#pi)\<bullet>c = (if (pi\<bullet>c)=fst ab then snd ab
+ − 1289
else (if (pi\<bullet>c)=snd ab then fst ab else (pi\<bullet>c)))"
153
+ − 1290
157
+ − 1291
primrec (perm_prod)
+ − 1292
"pi\<bullet>(x, y) = (pi\<bullet>x, pi\<bullet>y)"
+ − 1293
+ − 1294
primrec (perm_list)
+ − 1295
"pi\<bullet>[] = []"
+ − 1296
"pi\<bullet>(x#xs) = (pi\<bullet>x)#(pi\<bullet>xs)"
+ − 1297
+ − 1298
lemma perm_append[simp]:
+ − 1299
fixes c::"nat" and pi\<^isub>1 pi\<^isub>2::"prm"
+ − 1300
shows "((pi\<^isub>1@pi\<^isub>2)\<bullet>c) = (pi\<^isub>1\<bullet>(pi\<^isub>2\<bullet>c))"
+ − 1301
by (induct pi\<^isub>1) (auto)
+ − 1302
+ − 1303
lemma perm_eq[simp]:
+ − 1304
fixes c::"nat" and pi::"prm"
+ − 1305
shows "(pi\<bullet>c = pi\<bullet>d) = (c = d)"
+ − 1306
by (induct pi) (auto)
153
+ − 1307
157
+ − 1308
lemma perm_rev[simp]:
+ − 1309
fixes c::"nat" and pi::"prm"
+ − 1310
shows "pi\<bullet>((rev pi)\<bullet>c) = c"
+ − 1311
by (induct pi arbitrary: c) (auto)
+ − 1312
+ − 1313
lemma perm_compose:
+ − 1314
fixes c::"nat" and pi\<^isub>1 pi\<^isub>2::"prm"
+ − 1315
shows "pi\<^isub>1\<bullet>(pi\<^isub>2\<bullet>c) = (pi\<^isub>1\<bullet>pi\<^isub>2)\<bullet>(pi\<^isub>1\<bullet>c)"
+ − 1316
by (induct pi\<^isub>2) (auto)
+ − 1317
text_raw {*
173
+ − 1318
\end{isabelle}
+ − 1319
\end{boxedminipage}
157
+ − 1320
\caption{A simple theory about permutations over @{typ nat}. The point is that the
+ − 1321
lemma @{thm [source] perm_compose} cannot be directly added to the simplifier, as
+ − 1322
it would cause the simplifier to loop. It can still be used as a simplification
+ − 1323
rule if the permutation is sufficiently protected.\label{fig:perms}
+ − 1324
(FIXME: Uses old primrec.)}
+ − 1325
\end{figure} *}
+ − 1326
+ − 1327
+ − 1328
text {*
162
+ − 1329
The simplifier is often used in order to bring terms into a normal form.
+ − 1330
Unfortunately, often the situation arises that the corresponding
+ − 1331
simplification rules will cause the simplifier to run into an infinite
+ − 1332
loop. Consider for example the simple theory about permutations over natural
+ − 1333
numbers shown in Figure~\ref{fig:perms}. The purpose of the lemmas is to
+ − 1334
push permutations as far inside as possible, where they might disappear by
+ − 1335
Lemma @{thm [source] perm_rev}. However, to fully normalise all instances,
+ − 1336
it would be desirable to add also the lemma @{thm [source] perm_compose} to
+ − 1337
the simplifier for pushing permutations over other permutations. Unfortunately,
+ − 1338
the right-hand side of this lemma is again an instance of the left-hand side
209
+ − 1339
and so causes an infinite loop. There seems to be no easy way to reformulate
162
+ − 1340
this rule and so one ends up with clunky proofs like:
153
+ − 1341
*}
+ − 1342
157
+ − 1343
lemma
+ − 1344
fixes c d::"nat" and pi\<^isub>1 pi\<^isub>2::"prm"
+ − 1345
shows "pi\<^isub>1\<bullet>(c, pi\<^isub>2\<bullet>((rev pi\<^isub>1)\<bullet>d)) = (pi\<^isub>1\<bullet>c, (pi\<^isub>1\<bullet>pi\<^isub>2)\<bullet>d)"
+ − 1346
apply(simp)
+ − 1347
apply(rule trans)
+ − 1348
apply(rule perm_compose)
+ − 1349
apply(simp)
+ − 1350
done
153
+ − 1351
+ − 1352
text {*
162
+ − 1353
It is however possible to create a single simplifier tactic that solves
157
+ − 1354
such proofs. The trick is to introduce an auxiliary constant for permutations
162
+ − 1355
and split the simplification into two phases (below actually three). Let
+ − 1356
assume the auxiliary constant is
157
+ − 1357
*}
+ − 1358
+ − 1359
definition
+ − 1360
perm_aux :: "prm \<Rightarrow> 'a \<Rightarrow> 'a" ("_ \<bullet>aux _" [80,80] 80)
+ − 1361
where
+ − 1362
"pi \<bullet>aux c \<equiv> pi \<bullet> c"
+ − 1363
162
+ − 1364
text {* Now the two lemmas *}
157
+ − 1365
+ − 1366
lemma perm_aux_expand:
+ − 1367
fixes c::"nat" and pi\<^isub>1 pi\<^isub>2::"prm"
+ − 1368
shows "pi\<^isub>1\<bullet>(pi\<^isub>2\<bullet>c) = pi\<^isub>1 \<bullet>aux (pi\<^isub>2\<bullet>c)"
+ − 1369
unfolding perm_aux_def by (rule refl)
+ − 1370
+ − 1371
lemma perm_compose_aux:
+ − 1372
fixes c::"nat" and pi\<^isub>1 pi\<^isub>2::"prm"
+ − 1373
shows "pi\<^isub>1\<bullet>(pi\<^isub>2\<bullet>aux c) = (pi\<^isub>1\<bullet>pi\<^isub>2) \<bullet>aux (pi\<^isub>1\<bullet>c)"
+ − 1374
unfolding perm_aux_def by (rule perm_compose)
+ − 1375
+ − 1376
text {*
+ − 1377
are simple consequence of the definition and @{thm [source] perm_compose}.
+ − 1378
More importantly, the lemma @{thm [source] perm_compose_aux} can be safely
+ − 1379
added to the simplifier, because now the right-hand side is not anymore an instance
162
+ − 1380
of the left-hand side. In a sense it freezes all redexes of permutation compositions
+ − 1381
after one step. In this way, we can split simplification of permutations
213
+ − 1382
into three phases without the user noticing anything about the auxiliary
162
+ − 1383
contant. We first freeze any instance of permutation compositions in the term using
+ − 1384
lemma @{thm [source] "perm_aux_expand"} (Line 9);
213
+ − 1385
then simplifiy all other permutations including pushing permutations over
162
+ − 1386
other permutations by rule @{thm [source] perm_compose_aux} (Line 10); and
+ − 1387
finally ``unfreeze'' all instances of permutation compositions by unfolding
+ − 1388
the definition of the auxiliary constant.
153
+ − 1389
*}
+ − 1390
157
+ − 1391
ML %linenosgray{*val perm_simp_tac =
+ − 1392
let
+ − 1393
val thms1 = [@{thm perm_aux_expand}]
+ − 1394
val thms2 = [@{thm perm_append}, @{thm perm_eq}, @{thm perm_rev},
+ − 1395
@{thm perm_compose_aux}] @ @{thms perm_prod.simps} @
+ − 1396
@{thms perm_list.simps} @ @{thms perm_nat.simps}
+ − 1397
val thms3 = [@{thm perm_aux_def}]
+ − 1398
in
+ − 1399
simp_tac (HOL_basic_ss addsimps thms1)
+ − 1400
THEN' simp_tac (HOL_basic_ss addsimps thms2)
+ − 1401
THEN' simp_tac (HOL_basic_ss addsimps thms3)
+ − 1402
end*}
153
+ − 1403
152
+ − 1404
text {*
209
+ − 1405
For all three phases we have to build simpsets adding specific lemmas. As is sufficient
162
+ − 1406
for our purposes here, we can add these lemma to @{ML HOL_basic_ss} in order to obtain
+ − 1407
the desired results. Now we can solve the following lemma
157
+ − 1408
*}
+ − 1409
+ − 1410
lemma
+ − 1411
fixes c d::"nat" and pi\<^isub>1 pi\<^isub>2::"prm"
+ − 1412
shows "pi\<^isub>1\<bullet>(c, pi\<^isub>2\<bullet>((rev pi\<^isub>1)\<bullet>d)) = (pi\<^isub>1\<bullet>c, (pi\<^isub>1\<bullet>pi\<^isub>2)\<bullet>d)"
+ − 1413
apply(tactic {* perm_simp_tac 1 *})
+ − 1414
done
+ − 1415
152
+ − 1416
157
+ − 1417
text {*
209
+ − 1418
in one step. This tactic can deal with most instances of normalising permutations.
+ − 1419
In order to solve all cases we have to deal with corner-cases such as the
162
+ − 1420
lemma being an exact instance of the permutation composition lemma. This can
+ − 1421
often be done easier by implementing a simproc or a conversion. Both will be
+ − 1422
explained in the next two chapters.
+ − 1423
157
+ − 1424
(FIXME: Is it interesting to say something about @{term "op =simp=>"}?)
+ − 1425
+ − 1426
(FIXME: What are the second components of the congruence rules---something to
+ − 1427
do with weak congruence constants?)
+ − 1428
+ − 1429
(FIXME: Anything interesting to say about @{ML Simplifier.clear_ss}?)
152
+ − 1430
162
+ − 1431
(FIXME: @{ML ObjectLogic.full_atomize_tac},
152
+ − 1432
@{ML ObjectLogic.rulify_tac})
+ − 1433
129
+ − 1434
*}
+ − 1435
+ − 1436
section {* Simprocs *}
+ − 1437
+ − 1438
text {*
+ − 1439
In Isabelle you can also implement custom simplification procedures, called
149
+ − 1440
\emph{simprocs}. Simprocs can be triggered by the simplifier on a specified
+ − 1441
term-pattern and rewrite a term according to a theorem. They are useful in
+ − 1442
cases where a rewriting rule must be produced on ``demand'' or when
+ − 1443
rewriting by simplification is too unpredictable and potentially loops.
129
+ − 1444
+ − 1445
To see how simprocs work, let us first write a simproc that just prints out
132
+ − 1446
the pattern which triggers it and otherwise does nothing. For this
129
+ − 1447
you can use the function:
+ − 1448
*}
+ − 1449
+ − 1450
ML %linenosgray{*fun fail_sp_aux simpset redex =
+ − 1451
let
+ − 1452
val ctxt = Simplifier.the_context simpset
+ − 1453
val _ = warning ("The redex: " ^ (str_of_cterm ctxt redex))
+ − 1454
in
+ − 1455
NONE
+ − 1456
end*}
+ − 1457
+ − 1458
text {*
+ − 1459
This function takes a simpset and a redex (a @{ML_type cterm}) as
132
+ − 1460
arguments. In Lines 3 and~4, we first extract the context from the given
129
+ − 1461
simpset and then print out a message containing the redex. The function
+ − 1462
returns @{ML NONE} (standing for an optional @{ML_type thm}) since at the
+ − 1463
moment we are \emph{not} interested in actually rewriting anything. We want
130
+ − 1464
that the simproc is triggered by the pattern @{term "Suc n"}. This can be
149
+ − 1465
done by adding the simproc to the current simpset as follows
129
+ − 1466
*}
+ − 1467
177
+ − 1468
simproc_setup %gray fail_sp ("Suc n") = {* K fail_sp_aux *}
129
+ − 1469
+ − 1470
text {*
+ − 1471
where the second argument specifies the pattern and the right-hand side
+ − 1472
contains the code of the simproc (we have to use @{ML K} since we ignoring
131
+ − 1473
an argument about morphisms\footnote{FIXME: what does the morphism do?}).
130
+ − 1474
After this, the simplifier is aware of the simproc and you can test whether
131
+ − 1475
it fires on the lemma:
129
+ − 1476
*}
120
+ − 1477
129
+ − 1478
lemma shows "Suc 0 = 1"
178
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1479
apply(simp)
129
+ − 1480
(*<*)oops(*>*)
+ − 1481
+ − 1482
text {*
213
+ − 1483
\begin{isabelle}
+ − 1484
@{text "> The redex: Suc 0"}\\
+ − 1485
@{text "> The redex: Suc 0"}\\
+ − 1486
\end{isabelle}
+ − 1487
129
+ − 1488
This will print out the message twice: once for the left-hand side and
130
+ − 1489
once for the right-hand side. The reason is that during simplification the
+ − 1490
simplifier will at some point reduce the term @{term "1::nat"} to @{term "Suc
129
+ − 1491
0"}, and then the simproc ``fires'' also on that term.
+ − 1492
131
+ − 1493
We can add or delete the simproc from the current simpset by the usual
132
+ − 1494
\isacommand{declare}-statement. For example the simproc will be deleted
+ − 1495
with the declaration
129
+ − 1496
*}
+ − 1497
+ − 1498
declare [[simproc del: fail_sp]]
+ − 1499
+ − 1500
text {*
+ − 1501
If you want to see what happens with just \emph{this} simproc, without any
+ − 1502
interference from other rewrite rules, you can call @{text fail_sp}
+ − 1503
as follows:
+ − 1504
*}
+ − 1505
+ − 1506
lemma shows "Suc 0 = 1"
178
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1507
apply(tactic {* simp_tac (HOL_basic_ss addsimprocs [@{simproc fail_sp}]) 1*})
129
+ − 1508
(*<*)oops(*>*)
+ − 1509
+ − 1510
text {*
131
+ − 1511
Now the message shows up only once since the term @{term "1::nat"} is
+ − 1512
left unchanged.
129
+ − 1513
178
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1514
Setting up a simproc using the command \isacommand{simproc\_setup} will
129
+ − 1515
always add automatically the simproc to the current simpset. If you do not
+ − 1516
want this, then you have to use a slightly different method for setting
+ − 1517
up the simproc. First the function @{ML fail_sp_aux} needs to be modified
+ − 1518
to
+ − 1519
*}
+ − 1520
+ − 1521
ML{*fun fail_sp_aux' simpset redex =
+ − 1522
let
+ − 1523
val ctxt = Simplifier.the_context simpset
+ − 1524
val _ = warning ("The redex: " ^ (Syntax.string_of_term ctxt redex))
+ − 1525
in
+ − 1526
NONE
+ − 1527
end*}
+ − 1528
+ − 1529
text {*
130
+ − 1530
Here the redex is given as a @{ML_type term}, instead of a @{ML_type cterm}
+ − 1531
(therefore we printing it out using the function @{ML string_of_term in Syntax}).
149
+ − 1532
We can turn this function into a proper simproc using the function
+ − 1533
@{ML Simplifier.simproc_i}:
93
+ − 1534
*}
+ − 1535
105
+ − 1536
129
+ − 1537
ML{*val fail_sp' =
146
+ − 1538
let
+ − 1539
val thy = @{theory}
+ − 1540
val pat = [@{term "Suc n"}]
+ − 1541
in
+ − 1542
Simplifier.simproc_i thy "fail_sp'" pat (K fail_sp_aux')
+ − 1543
end*}
129
+ − 1544
+ − 1545
text {*
+ − 1546
Here the pattern is given as @{ML_type term} (instead of @{ML_type cterm}).
130
+ − 1547
The function also takes a list of patterns that can trigger the simproc.
132
+ − 1548
Now the simproc is set up and can be explicitly added using
149
+ − 1549
@{ML addsimprocs} to a simpset whenerver
132
+ − 1550
needed.
+ − 1551
+ − 1552
Simprocs are applied from inside to outside and from left to right. You can
+ − 1553
see this in the proof
129
+ − 1554
*}
+ − 1555
+ − 1556
lemma shows "Suc (Suc 0) = (Suc 1)"
177
+ − 1557
apply(tactic {* simp_tac (HOL_basic_ss addsimprocs [fail_sp']) 1*})
129
+ − 1558
(*<*)oops(*>*)
+ − 1559
+ − 1560
text {*
132
+ − 1561
The simproc @{ML fail_sp'} prints out the sequence
129
+ − 1562
130
+ − 1563
@{text [display]
+ − 1564
"> Suc 0
+ − 1565
> Suc (Suc 0)
+ − 1566
> Suc 1"}
+ − 1567
131
+ − 1568
To see how a simproc applies a theorem, let us implement a simproc that
130
+ − 1569
rewrites terms according to the equation:
129
+ − 1570
*}
+ − 1571
+ − 1572
lemma plus_one:
+ − 1573
shows "Suc n \<equiv> n + 1" by simp
+ − 1574
+ − 1575
text {*
130
+ − 1576
Simprocs expect that the given equation is a meta-equation, however the
131
+ − 1577
equation can contain preconditions (the simproc then will only fire if the
132
+ − 1578
preconditions can be solved). To see that one has relatively precise control over
131
+ − 1579
the rewriting with simprocs, let us further assume we want that the simproc
+ − 1580
only rewrites terms ``greater'' than @{term "Suc 0"}. For this we can write
129
+ − 1581
*}
+ − 1582
131
+ − 1583
130
+ − 1584
ML{*fun plus_one_sp_aux ss redex =
129
+ − 1585
case redex of
+ − 1586
@{term "Suc 0"} => NONE
+ − 1587
| _ => SOME @{thm plus_one}*}
+ − 1588
+ − 1589
text {*
+ − 1590
and set up the simproc as follows.
+ − 1591
*}
+ − 1592
130
+ − 1593
ML{*val plus_one_sp =
146
+ − 1594
let
+ − 1595
val thy = @{theory}
+ − 1596
val pat = [@{term "Suc n"}]
+ − 1597
in
+ − 1598
Simplifier.simproc_i thy "sproc +1" pat (K plus_one_sp_aux)
+ − 1599
end*}
129
+ − 1600
+ − 1601
text {*
132
+ − 1602
Now the simproc is set up so that it is triggered by terms
130
+ − 1603
of the form @{term "Suc n"}, but inside the simproc we only produce
+ − 1604
a theorem if the term is not @{term "Suc 0"}. The result you can see
131
+ − 1605
in the following proof
129
+ − 1606
*}
+ − 1607
+ − 1608
lemma shows "P (Suc (Suc (Suc 0))) (Suc 0)"
177
+ − 1609
apply(tactic {* simp_tac (HOL_basic_ss addsimprocs [plus_one_sp]) 1*})
129
+ − 1610
txt{*
131
+ − 1611
where the simproc produces the goal state
177
+ − 1612
+ − 1613
\begin{minipage}{\textwidth}
129
+ − 1614
@{subgoals[display]}
177
+ − 1615
\end{minipage}
129
+ − 1616
*}
+ − 1617
(*<*)oops(*>*)
+ − 1618
+ − 1619
text {*
133
+ − 1620
As usual with rewriting you have to worry about looping: you already have
132
+ − 1621
a loop with @{ML plus_one_sp}, if you apply it with the default simpset (because
+ − 1622
the default simpset contains a rule which just does the opposite of @{ML plus_one_sp},
+ − 1623
namely rewriting @{text [quotes] "+ 1"} to a successor). So you have to be careful
+ − 1624
in choosing the right simpset to which you add a simproc.
130
+ − 1625
132
+ − 1626
Next let us implement a simproc that replaces terms of the form @{term "Suc n"}
130
+ − 1627
with the number @{text n} increase by one. First we implement a function that
132
+ − 1628
takes a term and produces the corresponding integer value.
129
+ − 1629
*}
+ − 1630
+ − 1631
ML{*fun dest_suc_trm ((Const (@{const_name "Suc"}, _)) $ t) = 1 + dest_suc_trm t
+ − 1632
| dest_suc_trm t = snd (HOLogic.dest_number t)*}
+ − 1633
130
+ − 1634
text {*
+ − 1635
It uses the library function @{ML dest_number in HOLogic} that transforms
+ − 1636
(Isabelle) terms, like @{term "0::nat"}, @{term "1::nat"}, @{term "2::nat"} and so
131
+ − 1637
on, into integer values. This function raises the exception @{ML TERM}, if
130
+ − 1638
the term is not a number. The next function expects a pair consisting of a term
131
+ − 1639
@{text t} (containing @{term Suc}s) and the corresponding integer value @{text n}.
130
+ − 1640
*}
+ − 1641
+ − 1642
ML %linenosgray{*fun get_thm ctxt (t, n) =
+ − 1643
let
+ − 1644
val num = HOLogic.mk_number @{typ "nat"} n
132
+ − 1645
val goal = Logic.mk_equals (t, num)
130
+ − 1646
in
132
+ − 1647
Goal.prove ctxt [] [] goal (K (arith_tac ctxt 1))
130
+ − 1648
end*}
+ − 1649
+ − 1650
text {*
132
+ − 1651
From the integer value it generates the corresponding number term, called
+ − 1652
@{text num} (Line 3), and then generates the meta-equation @{text "t \<equiv> num"}
+ − 1653
(Line 4), which it proves by the arithmetic tactic in Line 6.
+ − 1654
134
+ − 1655
For our purpose at the moment, proving the meta-equation using @{ML arith_tac} is
132
+ − 1656
fine, but there is also an alternative employing the simplifier with a very
+ − 1657
restricted simpset. For the kind of lemmas we want to prove, the simpset
+ − 1658
@{text "num_ss"} in the code will suffice.
+ − 1659
*}
131
+ − 1660
132
+ − 1661
ML{*fun get_thm_alt ctxt (t, n) =
+ − 1662
let
+ − 1663
val num = HOLogic.mk_number @{typ "nat"} n
+ − 1664
val goal = Logic.mk_equals (t, num)
+ − 1665
val num_ss = HOL_ss addsimps [@{thm One_nat_def}, @{thm Let_def}] @
+ − 1666
@{thms nat_number} @ @{thms neg_simps} @ @{thms plus_nat.simps}
+ − 1667
in
+ − 1668
Goal.prove ctxt [] [] goal (K (simp_tac num_ss 1))
+ − 1669
end*}
130
+ − 1670
132
+ − 1671
text {*
+ − 1672
The advantage of @{ML get_thm_alt} is that it leaves very little room for
+ − 1673
something to go wrong; in contrast it is much more difficult to predict
+ − 1674
what happens with @{ML arith_tac}, especially in more complicated
+ − 1675
circumstances. The disatvantage of @{ML get_thm_alt} is to find a simpset
+ − 1676
that is sufficiently powerful to solve every instance of the lemmas
+ − 1677
we like to prove. This requires careful tuning, but is often necessary in
+ − 1678
``production code''.\footnote{It would be of great help if there is another
+ − 1679
way than tracing the simplifier to obtain the lemmas that are successfully
+ − 1680
applied during simplification. Alas, there is none.}
+ − 1681
+ − 1682
Anyway, either version can be used in the function that produces the actual
+ − 1683
theorem for the simproc.
130
+ − 1684
*}
129
+ − 1685
+ − 1686
ML{*fun nat_number_sp_aux ss t =
+ − 1687
let
+ − 1688
val ctxt = Simplifier.the_context ss
+ − 1689
in
130
+ − 1690
SOME (get_thm ctxt (t, dest_suc_trm t))
129
+ − 1691
handle TERM _ => NONE
+ − 1692
end*}
+ − 1693
+ − 1694
text {*
130
+ − 1695
This function uses the fact that @{ML dest_suc_trm} might throw an exception
+ − 1696
@{ML TERM}. In this case there is nothing that can be rewritten and therefore no
131
+ − 1697
theorem is produced (i.e.~the function returns @{ML NONE}). To try out the simproc
+ − 1698
on an example, you can set it up as follows:
129
+ − 1699
*}
+ − 1700
130
+ − 1701
ML{*val nat_number_sp =
132
+ − 1702
let
+ − 1703
val thy = @{theory}
+ − 1704
val pat = [@{term "Suc n"}]
+ − 1705
in
+ − 1706
Simplifier.simproc_i thy "nat_number" pat (K nat_number_sp_aux)
+ − 1707
end*}
130
+ − 1708
+ − 1709
text {*
+ − 1710
Now in the lemma
+ − 1711
*}
129
+ − 1712
+ − 1713
lemma "P (Suc (Suc 2)) (Suc 99) (0::nat) (Suc 4 + Suc 0) (Suc (0 + 0))"
177
+ − 1714
apply(tactic {* simp_tac (HOL_ss addsimprocs [nat_number_sp]) 1*})
129
+ − 1715
txt {*
130
+ − 1716
you obtain the more legible goal state
+ − 1717
177
+ − 1718
\begin{minipage}{\textwidth}
129
+ − 1719
@{subgoals [display]}
177
+ − 1720
\end{minipage}
129
+ − 1721
*}
+ − 1722
(*<*)oops(*>*)
+ − 1723
130
+ − 1724
text {*
132
+ − 1725
where the simproc rewrites all @{term "Suc"}s except in the last argument. There it cannot
130
+ − 1726
rewrite anything, because it does not know how to transform the term @{term "Suc (0 + 0)"}
+ − 1727
into a number. To solve this problem have a look at the next exercise.
+ − 1728
+ − 1729
\begin{exercise}\label{ex:addsimproc}
+ − 1730
Write a simproc that replaces terms of the form @{term "t\<^isub>1 + t\<^isub>2"} by their
+ − 1731
result. You can assume the terms are ``proper'' numbers, that is of the form
+ − 1732
@{term "0::nat"}, @{term "1::nat"}, @{term "2::nat"} and so on.
+ − 1733
\end{exercise}
+ − 1734
+ − 1735
(FIXME: We did not do anything with morphisms. Anything interesting
+ − 1736
one can say about them?)
+ − 1737
*}
129
+ − 1738
137
+ − 1739
section {* Conversions\label{sec:conversion} *}
132
+ − 1740
135
+ − 1741
text {*
145
+ − 1742
147
+ − 1743
Conversions are a thin layer on top of Isabelle's inference kernel, and
169
+ − 1744
can be viewed as a controllable, bare-bone version of Isabelle's simplifier.
147
+ − 1745
One difference between conversions and the simplifier is that the former
+ − 1746
act on @{ML_type cterm}s while the latter acts on @{ML_type thm}s.
+ − 1747
However, we will also show in this section how conversions can be applied
+ − 1748
to theorems via tactics. The type for conversions is
135
+ − 1749
*}
+ − 1750
186
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1751
ML{*type conv = cterm -> thm*}
135
+ − 1752
+ − 1753
text {*
147
+ − 1754
whereby the produced theorem is always a meta-equality. A simple conversion
+ − 1755
is the function @{ML "Conv.all_conv"}, which maps a @{ML_type cterm} to an
+ − 1756
instance of the (meta)reflexivity theorem. For example:
135
+ − 1757
145
+ − 1758
@{ML_response_fake [display,gray]
146
+ − 1759
"Conv.all_conv @{cterm \"Foo \<or> Bar\"}"
+ − 1760
"Foo \<or> Bar \<equiv> Foo \<or> Bar"}
+ − 1761
147
+ − 1762
Another simple conversion is @{ML Conv.no_conv} which always raises the
+ − 1763
exception @{ML CTERM}.
135
+ − 1764
145
+ − 1765
@{ML_response_fake [display,gray]
+ − 1766
"Conv.no_conv @{cterm True}"
+ − 1767
"*** Exception- CTERM (\"no conversion\", []) raised"}
+ − 1768
146
+ − 1769
A more interesting conversion is the function @{ML "Thm.beta_conversion"}: it
160
cc9359bfacf4
redefined the functions warning and tracing in order to properly match more antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1770
produces a meta-equation between a term and its beta-normal form. For example
142
+ − 1771
145
+ − 1772
@{ML_response_fake [display,gray]
146
+ − 1773
"let
+ − 1774
val add = @{cterm \"\<lambda>x y. x + (y::nat)\"}
+ − 1775
val two = @{cterm \"2::nat\"}
+ − 1776
val ten = @{cterm \"10::nat\"}
+ − 1777
in
+ − 1778
Thm.beta_conversion true (Thm.capply (Thm.capply add two) ten)
+ − 1779
end"
+ − 1780
"((\<lambda>x y. x + y) 2) 10 \<equiv> 2 + 10"}
+ − 1781
147
+ − 1782
Note that the actual response in this example is @{term "2 + 10 \<equiv> 2 + (10::nat)"},
190
+ − 1783
since the pretty-printer for @{ML_type cterm}s eta-normalises terms.
174
+ − 1784
But how we constructed the term (using the function
+ − 1785
@{ML Thm.capply}, which is the application @{ML $} for @{ML_type cterm}s)
+ − 1786
ensures that the left-hand side must contain beta-redexes. Indeed
147
+ − 1787
if we obtain the ``raw'' representation of the produced theorem, we
+ − 1788
can see the difference:
+ − 1789
+ − 1790
@{ML_response [display,gray]
+ − 1791
"let
+ − 1792
val add = @{cterm \"\<lambda>x y. x + (y::nat)\"}
+ − 1793
val two = @{cterm \"2::nat\"}
+ − 1794
val ten = @{cterm \"10::nat\"}
160
cc9359bfacf4
redefined the functions warning and tracing in order to properly match more antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1795
val thm = Thm.beta_conversion true (Thm.capply (Thm.capply add two) ten)
147
+ − 1796
in
160
cc9359bfacf4
redefined the functions warning and tracing in order to properly match more antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1797
#prop (rep_thm thm)
147
+ − 1798
end"
+ − 1799
"Const (\"==\",\<dots>) $
+ − 1800
(Abs (\"x\",\<dots>,Abs (\"y\",\<dots>,\<dots>)) $\<dots>$\<dots>) $
+ − 1801
(Const (\"HOL.plus_class.plus\",\<dots>) $ \<dots> $ \<dots>)"}
142
+ − 1802
146
+ − 1803
The argument @{ML true} in @{ML Thm.beta_conversion} indicates that
147
+ − 1804
the right-hand side will be fully beta-normalised. If instead
+ − 1805
@{ML false} is given, then only a single beta-reduction is performed
+ − 1806
on the outer-most level. For example
146
+ − 1807
+ − 1808
@{ML_response_fake [display,gray]
+ − 1809
"let
+ − 1810
val add = @{cterm \"\<lambda>x y. x + (y::nat)\"}
+ − 1811
val two = @{cterm \"2::nat\"}
+ − 1812
in
+ − 1813
Thm.beta_conversion false (Thm.capply add two)
+ − 1814
end"
+ − 1815
"((\<lambda>x y. x + y) 2) \<equiv> \<lambda>y. 2 + y"}
+ − 1816
190
+ − 1817
Again, we actually see as output only the fully eta-normalised term.
146
+ − 1818
147
+ − 1819
The main point of conversions is that they can be used for rewriting
+ − 1820
@{ML_type cterm}s. To do this you can use the function @{ML
160
cc9359bfacf4
redefined the functions warning and tracing in order to properly match more antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1821
"Conv.rewr_conv"}, which expects a meta-equation as an argument. Suppose we
cc9359bfacf4
redefined the functions warning and tracing in order to properly match more antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1822
want to rewrite a @{ML_type cterm} according to the meta-equation:
135
+ − 1823
*}
+ − 1824
139
+ − 1825
lemma true_conj1: "True \<and> P \<equiv> P" by simp
135
+ − 1826
146
+ − 1827
text {*
160
cc9359bfacf4
redefined the functions warning and tracing in order to properly match more antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1828
You can see how this function works in the example rewriting
174
+ − 1829
@{term "True \<and> (Foo \<longrightarrow> Bar)"} to @{term "Foo \<longrightarrow> Bar"}.
139
+ − 1830
145
+ − 1831
@{ML_response_fake [display,gray]
146
+ − 1832
"let
149
+ − 1833
val ctrm = @{cterm \"True \<and> (Foo \<longrightarrow> Bar)\"}
146
+ − 1834
in
+ − 1835
Conv.rewr_conv @{thm true_conj1} ctrm
+ − 1836
end"
+ − 1837
"True \<and> (Foo \<longrightarrow> Bar) \<equiv> Foo \<longrightarrow> Bar"}
139
+ − 1838
147
+ − 1839
Note, however, that the function @{ML Conv.rewr_conv} only rewrites the
160
cc9359bfacf4
redefined the functions warning and tracing in order to properly match more antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1840
outer-most level of the @{ML_type cterm}. If the given @{ML_type cterm} does not match
cc9359bfacf4
redefined the functions warning and tracing in order to properly match more antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1841
exactly the
147
+ − 1842
left-hand side of the theorem, then @{ML Conv.rewr_conv} raises
+ − 1843
the exception @{ML CTERM}.
146
+ − 1844
+ − 1845
This very primitive way of rewriting can be made more powerful by
+ − 1846
combining several conversions into one. For this you can use conversion
+ − 1847
combinators. The simplest conversion combinator is @{ML then_conv},
+ − 1848
which applies one conversion after another. For example
139
+ − 1849
145
+ − 1850
@{ML_response_fake [display,gray]
146
+ − 1851
"let
147
+ − 1852
val conv1 = Thm.beta_conversion false
146
+ − 1853
val conv2 = Conv.rewr_conv @{thm true_conj1}
147
+ − 1854
val ctrm = Thm.capply @{cterm \"\<lambda>x. x \<and> False\"} @{cterm \"True\"}
146
+ − 1855
in
+ − 1856
(conv1 then_conv conv2) ctrm
+ − 1857
end"
145
+ − 1858
"(\<lambda>x. x \<and> False) True \<equiv> False"}
139
+ − 1859
147
+ − 1860
where we first beta-reduce the term and then rewrite according to
149
+ − 1861
@{thm [source] true_conj1}. (Recall the problem with the pretty-printer
+ − 1862
normalising all terms.)
147
+ − 1863
146
+ − 1864
The conversion combinator @{ML else_conv} tries out the
+ − 1865
first one, and if it does not apply, tries the second. For example
+ − 1866
145
+ − 1867
@{ML_response_fake [display,gray]
146
+ − 1868
"let
147
+ − 1869
val conv = Conv.rewr_conv @{thm true_conj1} else_conv Conv.all_conv
146
+ − 1870
val ctrm1 = @{cterm \"True \<and> Q\"}
+ − 1871
val ctrm2 = @{cterm \"P \<or> (True \<and> Q)\"}
+ − 1872
in
+ − 1873
(conv ctrm1, conv ctrm2)
+ − 1874
end"
147
+ − 1875
"(True \<and> Q \<equiv> Q, P \<or> True \<and> Q \<equiv> P \<or> True \<and> Q)"}
146
+ − 1876
+ − 1877
Here the conversion of @{thm [source] true_conj1} only applies
+ − 1878
in the first case, but fails in the second. The whole conversion
151
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1879
does not fail, however, because the combinator @{ML Conv.else_conv} will then
147
+ − 1880
try out @{ML Conv.all_conv}, which always succeeds.
146
+ − 1881
174
+ − 1882
The conversion combinator @{ML Conv.try_conv} constructs a conversion
+ − 1883
which is tried out on a term, but in case of failure just does nothing.
+ − 1884
For example
+ − 1885
+ − 1886
@{ML_response_fake [display,gray]
+ − 1887
"Conv.try_conv (Conv.rewr_conv @{thm true_conj1}) @{cterm \"True \<or> P\"}"
+ − 1888
"True \<or> P \<equiv> True \<or> P"}
+ − 1889
149
+ − 1890
Apart from the function @{ML beta_conversion in Thm}, which is able to fully
+ − 1891
beta-normalise a term, the conversions so far are restricted in that they
147
+ − 1892
only apply to the outer-most level of a @{ML_type cterm}. In what follows we
+ − 1893
will lift this restriction. The combinator @{ML Conv.arg_conv} will apply
149
+ − 1894
the conversion to the first argument of an application, that is the term
147
+ − 1895
must be of the form @{ML "t1 $ t2" for t1 t2} and the conversion is applied
+ − 1896
to @{text t2}. For example
139
+ − 1897
145
+ − 1898
@{ML_response_fake [display,gray]
146
+ − 1899
"let
+ − 1900
val conv = Conv.rewr_conv @{thm true_conj1}
+ − 1901
val ctrm = @{cterm \"P \<or> (True \<and> Q)\"}
+ − 1902
in
+ − 1903
Conv.arg_conv conv ctrm
+ − 1904
end"
+ − 1905
"P \<or> (True \<and> Q) \<equiv> P \<or> Q"}
139
+ − 1906
147
+ − 1907
The reason for this behaviour is that @{text "(op \<or>)"} expects two
160
cc9359bfacf4
redefined the functions warning and tracing in order to properly match more antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1908
arguments. Therefore the term must be of the form @{text "(Const \<dots> $ t1) $ t2"}. The
147
+ − 1909
conversion is then applied to @{text "t2"} which in the example above
150
+ − 1910
stands for @{term "True \<and> Q"}. The function @{ML Conv.fun_conv} applies
+ − 1911
the conversion to the first argument of an application.
147
+ − 1912
+ − 1913
The function @{ML Conv.abs_conv} applies a conversion under an abstractions.
+ − 1914
For example:
139
+ − 1915
147
+ − 1916
@{ML_response_fake [display,gray]
+ − 1917
"let
+ − 1918
val conv = K (Conv.rewr_conv @{thm true_conj1})
+ − 1919
val ctrm = @{cterm \"\<lambda>P. True \<and> P \<and> Foo\"}
+ − 1920
in
+ − 1921
Conv.abs_conv conv @{context} ctrm
+ − 1922
end"
+ − 1923
"\<lambda>P. True \<and> P \<and> Foo \<equiv> \<lambda>P. P \<and> Foo"}
+ − 1924
160
cc9359bfacf4
redefined the functions warning and tracing in order to properly match more antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1925
Note that this conversion needs a context as an argument. The conversion that
cc9359bfacf4
redefined the functions warning and tracing in order to properly match more antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1926
goes under an application is @{ML Conv.combination_conv}. It expects two conversions
cc9359bfacf4
redefined the functions warning and tracing in order to properly match more antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1927
as arguments, each of which is applied to the corresponding ``branch'' of the
cc9359bfacf4
redefined the functions warning and tracing in order to properly match more antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1928
application.
147
+ − 1929
160
cc9359bfacf4
redefined the functions warning and tracing in order to properly match more antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1930
We can now apply all these functions in a conversion that recursively
cc9359bfacf4
redefined the functions warning and tracing in order to properly match more antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1931
descends a term and applies a ``@{thm [source] true_conj1}''-conversion
cc9359bfacf4
redefined the functions warning and tracing in order to properly match more antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1932
in all possible positions.
146
+ − 1933
*}
+ − 1934
147
+ − 1935
ML %linenosgray{*fun all_true1_conv ctxt ctrm =
+ − 1936
case (Thm.term_of ctrm) of
142
+ − 1937
@{term "op \<and>"} $ @{term True} $ _ =>
+ − 1938
(Conv.arg_conv (all_true1_conv ctxt) then_conv
147
+ − 1939
Conv.rewr_conv @{thm true_conj1}) ctrm
+ − 1940
| _ $ _ => Conv.combination_conv
160
cc9359bfacf4
redefined the functions warning and tracing in order to properly match more antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1941
(all_true1_conv ctxt) (all_true1_conv ctxt) ctrm
147
+ − 1942
| Abs _ => Conv.abs_conv (fn (_, ctxt) => all_true1_conv ctxt) ctxt ctrm
+ − 1943
| _ => Conv.all_conv ctrm*}
139
+ − 1944
+ − 1945
text {*
160
cc9359bfacf4
redefined the functions warning and tracing in order to properly match more antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1946
This function ``fires'' if the terms is of the form @{text "True \<and> \<dots>"};
cc9359bfacf4
redefined the functions warning and tracing in order to properly match more antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1947
it descends under applications (Line 6 and 7) and abstractions
cc9359bfacf4
redefined the functions warning and tracing in order to properly match more antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1948
(Line 8); otherwise it leaves the term unchanged (Line 9). In Line 2
149
+ − 1949
we need to transform the @{ML_type cterm} into a @{ML_type term} in order
+ − 1950
to be able to pattern-match the term. To see this
160
cc9359bfacf4
redefined the functions warning and tracing in order to properly match more antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1951
conversion in action, consider the following example:
139
+ − 1952
147
+ − 1953
@{ML_response_fake [display,gray]
+ − 1954
"let
+ − 1955
val ctxt = @{context}
+ − 1956
val ctrm = @{cterm \"distinct [1, x] \<longrightarrow> True \<and> 1 \<noteq> x\"}
+ − 1957
in
+ − 1958
all_true1_conv ctxt ctrm
+ − 1959
end"
145
+ − 1960
"distinct [1, x] \<longrightarrow> True \<and> 1 \<noteq> x \<equiv> distinct [1, x] \<longrightarrow> 1 \<noteq> x"}
139
+ − 1961
149
+ − 1962
To see how much control you have about rewriting by using conversions, let us
147
+ − 1963
make the task a bit more complicated by rewriting according to the rule
149
+ − 1964
@{text true_conj1}, but only in the first arguments of @{term If}s. Then
147
+ − 1965
the conversion should be as follows.
135
+ − 1966
*}
+ − 1967
147
+ − 1968
ML{*fun if_true1_conv ctxt ctrm =
+ − 1969
case Thm.term_of ctrm of
142
+ − 1970
Const (@{const_name If}, _) $ _ =>
147
+ − 1971
Conv.arg_conv (all_true1_conv ctxt) ctrm
+ − 1972
| _ $ _ => Conv.combination_conv
160
cc9359bfacf4
redefined the functions warning and tracing in order to properly match more antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1973
(if_true1_conv ctxt) (if_true1_conv ctxt) ctrm
147
+ − 1974
| Abs _ => Conv.abs_conv (fn (_, ctxt) => if_true1_conv ctxt) ctxt ctrm
+ − 1975
| _ => Conv.all_conv ctrm *}
135
+ − 1976
139
+ − 1977
text {*
149
+ − 1978
Here is an example for this conversion:
139
+ − 1979
145
+ − 1980
@{ML_response_fake [display,gray]
147
+ − 1981
"let
+ − 1982
val ctxt = @{context}
+ − 1983
val ctrm =
160
cc9359bfacf4
redefined the functions warning and tracing in order to properly match more antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1984
@{cterm \"if P (True \<and> 1 \<noteq> 2) then True \<and> True else True \<and> False\"}
147
+ − 1985
in
+ − 1986
if_true1_conv ctxt ctrm
+ − 1987
end"
+ − 1988
"if P (True \<and> 1 \<noteq> 2) then True \<and> True else True \<and> False
+ − 1989
\<equiv> if P (1 \<noteq> 2) then True \<and> True else True \<and> False"}
135
+ − 1990
*}
+ − 1991
+ − 1992
text {*
147
+ − 1993
So far we only applied conversions to @{ML_type cterm}s. Conversions can, however,
+ − 1994
also work on theorems using the function @{ML "Conv.fconv_rule"}. As an example,
149
+ − 1995
consider the conversion @{ML all_true1_conv} and the lemma:
147
+ − 1996
*}
+ − 1997
+ − 1998
lemma foo_test: "P \<or> (True \<and> \<not>P)" by simp
+ − 1999
+ − 2000
text {*
+ − 2001
Using the conversion you can transform this theorem into a new theorem
+ − 2002
as follows
+ − 2003
+ − 2004
@{ML_response_fake [display,gray]
+ − 2005
"Conv.fconv_rule (all_true1_conv @{context}) @{thm foo_test}"
+ − 2006
"?P \<or> \<not> ?P"}
+ − 2007
+ − 2008
Finally, conversions can also be turned into tactics and then applied to
+ − 2009
goal states. This can be done with the help of the function @{ML CONVERSION},
160
cc9359bfacf4
redefined the functions warning and tracing in order to properly match more antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 2010
and also some predefined conversion combinators that traverse a goal
147
+ − 2011
state. The combinators for the goal state are: @{ML Conv.params_conv} for
160
cc9359bfacf4
redefined the functions warning and tracing in order to properly match more antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 2012
converting under parameters (i.e.~where goals are of the form @{text "\<And>x. P \<Longrightarrow>
cc9359bfacf4
redefined the functions warning and tracing in order to properly match more antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 2013
Q"}); the function @{ML Conv.prems_conv} for applying a conversion to all
cc9359bfacf4
redefined the functions warning and tracing in order to properly match more antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 2014
premises of a goal, and @{ML Conv.concl_conv} for applying a conversion to
147
+ − 2015
the conclusion of a goal.
139
+ − 2016
145
+ − 2017
Assume we want to apply @{ML all_true1_conv} only in the conclusion
160
cc9359bfacf4
redefined the functions warning and tracing in order to properly match more antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 2018
of the goal, and @{ML if_true1_conv} should only apply to the premises.
145
+ − 2019
Here is a tactic doing exactly that:
135
+ − 2020
*}
+ − 2021
186
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 2022
ML{*fun true1_tac ctxt = CSUBGOAL (fn (goal, i) =>
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 2023
CONVERSION
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 2024
(Conv.params_conv ~1 (fn ctxt =>
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 2025
(Conv.prems_conv ~1 (if_true1_conv ctxt) then_conv
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 2026
Conv.concl_conv ~1 (all_true1_conv ctxt))) ctxt) i)*}
142
+ − 2027
+ − 2028
text {*
148
+ − 2029
We call the conversions with the argument @{ML "~1"}. This is to
+ − 2030
analyse all parameters, premises and conclusions. If we call them with
147
+ − 2031
a non-negative number, say @{text n}, then these conversions will
+ − 2032
only be called on @{text n} premises (similar for parameters and
+ − 2033
conclusions). To test the tactic, consider the proof
142
+ − 2034
*}
139
+ − 2035
142
+ − 2036
lemma
+ − 2037
"if True \<and> P then P else True \<and> False \<Longrightarrow>
148
+ − 2038
(if True \<and> Q then True \<and> Q else P) \<longrightarrow> True \<and> (True \<and> Q)"
186
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 2039
apply(tactic {* true1_tac @{context} 1 *})
147
+ − 2040
txt {* where the tactic yields the goal state
+ − 2041
177
+ − 2042
\begin{minipage}{\textwidth}
+ − 2043
@{subgoals [display]}
+ − 2044
\end{minipage}*}
142
+ − 2045
(*<*)oops(*>*)
135
+ − 2046
+ − 2047
text {*
148
+ − 2048
As you can see, the premises are rewritten according to @{ML if_true1_conv}, while
+ − 2049
the conclusion according to @{ML all_true1_conv}.
+ − 2050
147
+ − 2051
To sum up this section, conversions are not as powerful as the simplifier
+ − 2052
and simprocs; the advantage of conversions, however, is that you never have
+ − 2053
to worry about non-termination.
146
+ − 2054
151
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 2055
\begin{exercise}\label{ex:addconversion}
152
+ − 2056
Write a tactic that does the same as the simproc in exercise
+ − 2057
\ref{ex:addsimproc}, but is based in conversions. That means replace terms
+ − 2058
of the form @{term "t\<^isub>1 + t\<^isub>2"} by their result. You can make
166
+ − 2059
the same assumptions as in \ref{ex:addsimproc}.
152
+ − 2060
\end{exercise}
+ − 2061
172
+ − 2062
\begin{exercise}\label{ex:compare}
174
+ − 2063
Compare your solutions of Exercises~\ref{ex:addsimproc} and \ref{ex:addconversion},
172
+ − 2064
and try to determine which way of rewriting such terms is faster. For this you might
+ − 2065
have to construct quite large terms. Also see Recipe \ref{rec:timing} for information
+ − 2066
about timing.
151
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 2067
\end{exercise}
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 2068
146
+ − 2069
\begin{readmore}
+ − 2070
See @{ML_file "Pure/conv.ML"} for more information about conversion combinators.
+ − 2071
Further conversions are defined in @{ML_file "Pure/thm.ML"},
+ − 2072
@{ML_file "Pure/drule.ML"} and @{ML_file "Pure/meta_simplifier.ML"}.
+ − 2073
\end{readmore}
151
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 2074
135
+ − 2075
*}
+ − 2076
184
+ − 2077
text {*
+ − 2078
(FIXME: check whether @{ML Pattern.match_rew} and @{ML Pattern.rewrite_term}
+ − 2079
are of any use/efficient)
+ − 2080
*}
135
+ − 2081
151
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 2082
152
+ − 2083
section {* Structured Proofs (TBD) *}
95
+ − 2084
129
+ − 2085
text {* TBD *}
+ − 2086
95
+ − 2087
lemma True
+ − 2088
proof
+ − 2089
+ − 2090
{
+ − 2091
fix A B C
+ − 2092
assume r: "A & B \<Longrightarrow> C"
+ − 2093
assume A B
+ − 2094
then have "A & B" ..
+ − 2095
then have C by (rule r)
+ − 2096
}
+ − 2097
+ − 2098
{
+ − 2099
fix A B C
+ − 2100
assume r: "A & B \<Longrightarrow> C"
+ − 2101
assume A B
+ − 2102
note conjI [OF this]
+ − 2103
note r [OF this]
+ − 2104
}
+ − 2105
oops
+ − 2106
+ − 2107
ML {* fun prop ctxt s =
+ − 2108
Thm.cterm_of (ProofContext.theory_of ctxt) (Syntax.read_prop ctxt s) *}
+ − 2109
+ − 2110
ML {*
+ − 2111
val ctxt0 = @{context};
+ − 2112
val ctxt = ctxt0;
+ − 2113
val (_, ctxt) = Variable.add_fixes ["A", "B", "C"] ctxt;
+ − 2114
val ([r], ctxt) = Assumption.add_assumes [prop ctxt "A & B \<Longrightarrow> C"] ctxt;
+ − 2115
val (this, ctxt) = Assumption.add_assumes [prop ctxt "A", prop ctxt "B"] ctxt;
+ − 2116
val this = [@{thm conjI} OF this];
+ − 2117
val this = r OF this;
+ − 2118
val this = Assumption.export false ctxt ctxt0 this
+ − 2119
val this = Variable.export ctxt ctxt0 [this]
+ − 2120
*}
93
+ − 2121
+ − 2122
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 2123
139
+ − 2124
end