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