15
9da9ba2b095b
added a solution section and some other minor additions
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 1
theory Solutions
329
+ − 2
imports FirstSteps "Recipes/Timing"
15
9da9ba2b095b
added a solution section and some other minor additions
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 3
begin
9da9ba2b095b
added a solution section and some other minor additions
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 4
346
+ − 5
(*<*)
+ − 6
setup{*
+ − 7
open_file_with_prelude
+ − 8
"Solutions_Code.thy"
+ − 9
["theory Solutions", "imports FirstSteps", "begin"]
+ − 10
*}
+ − 11
(*>*)
+ − 12
156
+ − 13
chapter {* Solutions to Most Exercises\label{ch:solutions} *}
15
9da9ba2b095b
added a solution section and some other minor additions
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 14
9da9ba2b095b
added a solution section and some other minor additions
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 15
text {* \solution{fun:revsum} *}
9da9ba2b095b
added a solution section and some other minor additions
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 16
293
+ − 17
ML{*fun rev_sum ((p as Const (@{const_name plus}, _)) $ t $ u) =
+ − 18
p $ u $ rev_sum t
271
+ − 19
| rev_sum t = t *}
+ − 20
293
+ − 21
text {*
316
+ − 22
An alternative solution using the function @{ML_ind mk_binop in HOLogic} is:
293
+ − 23
*}
271
+ − 24
69
+ − 25
ML{*fun rev_sum t =
47
4daf913fdbe1
hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 26
let
130
+ − 27
fun dest_sum (Const (@{const_name plus}, _) $ u $ u') = u' :: dest_sum u
+ − 28
| dest_sum u = [u]
+ − 29
in
47
4daf913fdbe1
hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 30
foldl1 (HOLogic.mk_binop @{const_name plus}) (dest_sum t)
130
+ − 31
end *}
15
9da9ba2b095b
added a solution section and some other minor additions
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 32
9da9ba2b095b
added a solution section and some other minor additions
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 33
text {* \solution{fun:makesum} *}
9da9ba2b095b
added a solution section and some other minor additions
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 34
69
+ − 35
ML{*fun make_sum t1 t2 =
130
+ − 36
HOLogic.mk_nat (HOLogic.dest_nat t1 + HOLogic.dest_nat t2) *}
15
9da9ba2b095b
added a solution section and some other minor additions
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 37
313
+ − 38
text {* \solution{ex:debruijn} *}
+ − 39
+ − 40
ML{*fun P n = @{term "P::nat \<Rightarrow> bool"} $ (HOLogic.mk_number @{typ "nat"} n)
+ − 41
+ − 42
fun rhs 1 = P 1
+ − 43
| rhs n = HOLogic.mk_conj (P n, rhs (n - 1))
+ − 44
+ − 45
fun lhs 1 n = HOLogic.mk_imp (HOLogic.mk_eq (P 1, P n), rhs n)
+ − 46
| lhs m n = HOLogic.mk_conj (HOLogic.mk_imp
+ − 47
(HOLogic.mk_eq (P (m - 1), P m), rhs n), lhs (m - 1) n)
+ − 48
+ − 49
fun de_bruijn n =
+ − 50
HOLogic.mk_Trueprop (HOLogic.mk_imp (lhs n n, rhs n))*}
+ − 51
56
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 52
text {* \solution{ex:scancmts} *}
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 53
130
+ − 54
ML{*val any = Scan.one (Symbol.not_eof)
56
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 55
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 56
val scan_cmt =
168
+ − 57
let
+ − 58
val begin_cmt = Scan.this_string "(*"
+ − 59
val end_cmt = Scan.this_string "*)"
+ − 60
in
+ − 61
begin_cmt |-- Scan.repeat (Scan.unless end_cmt any) --| end_cmt
+ − 62
>> (enclose "(**" "**)" o implode)
+ − 63
end
56
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 64
130
+ − 65
val parser = Scan.repeat (scan_cmt || any)
+ − 66
56
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 67
val scan_all =
168
+ − 68
Scan.finite Symbol.stopper parser >> implode #> fst *}
56
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 69
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 70
text {*
58
+ − 71
By using @{text "#> fst"} in the last line, the function
+ − 72
@{ML scan_all} retruns a string, instead of the pair a parser would
+ − 73
normally return. For example:
56
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 74
80
+ − 75
@{ML_response [display,gray]
+ − 76
"let
130
+ − 77
val input1 = (explode \"foo bar\")
+ − 78
val input2 = (explode \"foo (*test*) bar (*test*)\")
+ − 79
in
+ − 80
(scan_all input1, scan_all input2)
+ − 81
end"
+ − 82
"(\"foo bar\", \"foo (**test**) bar (**test**)\")"}
56
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 83
*}
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 84
391
+ − 85
text {* \solution{ex:contextfree} *}
+ − 86
+ − 87
ML{*datatype expr =
+ − 88
Number of int
+ − 89
| Mult of expr * expr
+ − 90
| Add of expr * expr
314
+ − 91
391
+ − 92
fun parse_basic xs =
+ − 93
(OuterParse.nat >> Number
+ − 94
|| OuterParse.$$$ "(" |-- parse_expr --| OuterParse.$$$ ")") xs
+ − 95
and parse_factor xs =
+ − 96
(parse_basic --| OuterParse.$$$ "*" -- parse_factor >> Mult
+ − 97
|| parse_basic) xs
+ − 98
and parse_expr xs =
+ − 99
(parse_factor --| OuterParse.$$$ "+" -- parse_expr >> Add
+ − 100
|| parse_factor) xs*}
+ − 101
+ − 102
407
+ − 103
text {* \solution{ex:dyckhoff} *}
+ − 104
+ − 105
text {*
314
+ − 106
The axiom rule can be implemented with the function @{ML atac}. The other
+ − 107
rules correspond to the theorems:
+ − 108
+ − 109
\begin{center}
+ − 110
\begin{tabular}{cc}
+ − 111
\begin{tabular}{rl}
+ − 112
$\wedge_R$ & @{thm [source] conjI}\\
+ − 113
$\vee_{R_1}$ & @{thm [source] disjI1}\\
+ − 114
$\vee_{R_2}$ & @{thm [source] disjI2}\\
+ − 115
$\longrightarrow_R$ & @{thm [source] impI}\\
+ − 116
$=_R$ & @{thm [source] iffI}\\
+ − 117
\end{tabular}
+ − 118
&
+ − 119
\begin{tabular}{rl}
+ − 120
$False$ & @{thm [source] FalseE}\\
+ − 121
$\wedge_L$ & @{thm [source] conjE}\\
+ − 122
$\vee_L$ & @{thm [source] disjE}\\
+ − 123
$=_L$ & @{thm [source] iffE}
+ − 124
\end{tabular}
+ − 125
\end{tabular}
+ − 126
\end{center}
+ − 127
+ − 128
For the other rules we need to prove the following lemmas.
+ − 129
*}
+ − 130
+ − 131
lemma impE1:
+ − 132
shows "\<lbrakk>A \<longrightarrow> B; A; B \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
+ − 133
by iprover
+ − 134
+ − 135
lemma impE2:
+ − 136
shows "\<lbrakk>(C \<and> D) \<longrightarrow> B; C \<longrightarrow> (D \<longrightarrow>B) \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
+ − 137
by iprover
+ − 138
+ − 139
lemma impE3:
+ − 140
shows "\<lbrakk>(C \<or> D) \<longrightarrow> B; \<lbrakk>C \<longrightarrow> B; D \<longrightarrow> B\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
+ − 141
by iprover
+ − 142
+ − 143
lemma impE4:
+ − 144
shows "\<lbrakk>(C \<longrightarrow> D) \<longrightarrow> B; D \<longrightarrow> B \<Longrightarrow> C \<longrightarrow> D; B \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
+ − 145
by iprover
+ − 146
+ − 147
lemma impE5:
+ − 148
shows "\<lbrakk>(C = D) \<longrightarrow> B; (C \<longrightarrow> D) \<longrightarrow> ((D \<longrightarrow> C) \<longrightarrow> B) \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
+ − 149
by iprover
+ − 150
+ − 151
text {*
+ − 152
Now the tactic which applies a single rule can be implemented
+ − 153
as follows.
+ − 154
*}
+ − 155
+ − 156
ML %linenosgray{*val apply_tac =
+ − 157
let
+ − 158
val intros = [@{thm conjI}, @{thm disjI1}, @{thm disjI2},
+ − 159
@{thm impI}, @{thm iffI}]
+ − 160
val elims = [@{thm FalseE}, @{thm conjE}, @{thm disjE}, @{thm iffE},
+ − 161
@{thm impE2}, @{thm impE3}, @{thm impE4}, @{thm impE5}]
+ − 162
in
+ − 163
atac
+ − 164
ORELSE' resolve_tac intros
+ − 165
ORELSE' eresolve_tac elims
+ − 166
ORELSE' (etac @{thm impE1} THEN' atac)
+ − 167
end*}
+ − 168
+ − 169
text {*
+ − 170
In Line 11 we apply the rule @{thm [source] impE1} in concjunction
+ − 171
with @{ML atac} in order to reduce the number of possibilities that
+ − 172
need to be explored. You can use the tactic as follows.
+ − 173
*}
+ − 174
+ − 175
lemma
+ − 176
shows "((((P \<longrightarrow> Q) \<longrightarrow> P) \<longrightarrow> P) \<longrightarrow> Q) \<longrightarrow> Q"
+ − 177
apply(tactic {* (DEPTH_SOLVE o apply_tac) 1 *})
+ − 178
done
+ − 179
+ − 180
text {*
+ − 181
We can use the tactic to prove or disprove automatically the
+ − 182
de Bruijn formulae from Exercise \ref{ex:debruijn}.
+ − 183
*}
+ − 184
+ − 185
ML{*fun de_bruijn_prove ctxt n =
+ − 186
let
+ − 187
val goal = HOLogic.mk_Trueprop (HOLogic.mk_imp (lhs n n, rhs n))
+ − 188
in
+ − 189
Goal.prove ctxt ["P"] [] goal
+ − 190
(fn _ => (DEPTH_SOLVE o apply_tac) 1)
+ − 191
end*}
+ − 192
+ − 193
text {*
+ − 194
You can use this function to prove de Bruijn formulae.
+ − 195
*}
+ − 196
+ − 197
ML{*de_bruijn_prove @{context} 3 *}
+ − 198
130
+ − 199
text {* \solution{ex:addsimproc} *}
+ − 200
+ − 201
ML{*fun dest_sum term =
+ − 202
case term of
+ − 203
(@{term "(op +):: nat \<Rightarrow> nat \<Rightarrow> nat"} $ t1 $ t2) =>
+ − 204
(snd (HOLogic.dest_number t1), snd (HOLogic.dest_number t2))
+ − 205
| _ => raise TERM ("dest_sum", [term])
+ − 206
+ − 207
fun get_sum_thm ctxt t (n1, n2) =
+ − 208
let
+ − 209
val sum = HOLogic.mk_number @{typ "nat"} (n1 + n2)
132
+ − 210
val goal = Logic.mk_equals (t, sum)
130
+ − 211
in
214
+ − 212
Goal.prove ctxt [] [] goal (K (Arith_Data.arith_tac ctxt 1))
130
+ − 213
end
+ − 214
+ − 215
fun add_sp_aux ss t =
+ − 216
let
+ − 217
val ctxt = Simplifier.the_context ss
+ − 218
val t' = term_of t
+ − 219
in
+ − 220
SOME (get_sum_thm ctxt t' (dest_sum t'))
+ − 221
handle TERM _ => NONE
+ − 222
end*}
+ − 223
+ − 224
text {* The setup for the simproc is *}
+ − 225
177
+ − 226
simproc_setup %gray add_sp ("t1 + t2") = {* K add_sp_aux *}
130
+ − 227
+ − 228
text {* and a test case is the lemma *}
+ − 229
405
+ − 230
lemma "P (Suc (99 + 1)) ((0 + 0)::nat) (Suc (3 + 3 + 3)) ((4 + 1)::nat)"
167
3e30ea95c7aa
added temporarily some timing test about conversions and simprocs
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 231
apply(tactic {* simp_tac (HOL_basic_ss addsimprocs [@{simproc add_sp}]) 1 *})
130
+ − 232
txt {*
+ − 233
where the simproc produces the goal state
+ − 234
+ − 235
\begin{minipage}{\textwidth}
+ − 236
@{subgoals [display]}
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
+ − 237
\end{minipage}\bigskip
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
+ − 238
*}(*<*)oops(*>*)
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
+ − 239
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
+ − 240
text {* \solution{ex:addconversion} *}
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
+ − 241
168
+ − 242
text {*
+ − 243
The following code assumes the function @{ML dest_sum} from the previous
+ − 244
exercise.
+ − 245
*}
+ − 246
407
+ − 247
ML{*fun add_simple_conv ctxt ctrm =
166
+ − 248
let
405
+ − 249
val trm = Thm.term_of ctrm
+ − 250
in
+ − 251
case trm of
+ − 252
@{term "(op +)::nat \<Rightarrow> nat \<Rightarrow> nat"} $ _ $ _ =>
+ − 253
get_sum_thm ctxt trm (dest_sum trm)
+ − 254
| _ => Conv.all_conv ctrm
166
+ − 255
end
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
+ − 256
405
+ − 257
val add_conv = More_Conv.bottom_conv add_simple_conv
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
+ − 258
410
+ − 259
fun add_tac ctxt = CONVERSION (add_conv ctxt)*}
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
+ − 260
168
+ − 261
text {*
175
+ − 262
A test case for this conversion is as follows
168
+ − 263
*}
+ − 264
405
+ − 265
lemma "P (Suc (99 + 1)) ((0 + 0)::nat) (Suc (3 + 3 + 3)) ((4 + 1)::nat)"
186
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 266
apply(tactic {* add_tac @{context} 1 *})?
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
+ − 267
txt {*
175
+ − 268
where it produces the goal state
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
+ − 269
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
+ − 270
\begin{minipage}{\textwidth}
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
+ − 271
@{subgoals [display]}
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
+ − 272
\end{minipage}\bigskip
130
+ − 273
*}(*<*)oops(*>*)
+ − 274
407
+ − 275
text {* \solution{ex:compare} *}
167
3e30ea95c7aa
added temporarily some timing test about conversions and simprocs
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 276
172
+ − 277
text {*
174
+ − 278
We use the timing function @{ML timing_wrapper} from Recipe~\ref{rec:timing}.
+ − 279
To measure any difference between the simproc and conversion, we will create
+ − 280
mechanically terms involving additions and then set up a goal to be
+ − 281
simplified. We have to be careful to set up the goal so that
178
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 282
other parts of the simplifier do not interfere. For this we construct an
174
+ − 283
unprovable goal which, after simplification, we are going to ``prove'' with
351
+ − 284
the help of ``\isacommand{sorry}'', that is the method @{ML Skip_Proof.cheat_tac}
167
3e30ea95c7aa
added temporarily some timing test about conversions and simprocs
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 285
174
+ − 286
For constructing test cases, we first define a function that returns a
+ − 287
complete binary tree whose leaves are numbers and the nodes are
+ − 288
additions.
167
3e30ea95c7aa
added temporarily some timing test about conversions and simprocs
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 289
*}
3e30ea95c7aa
added temporarily some timing test about conversions and simprocs
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 290
172
+ − 291
ML{*fun term_tree n =
+ − 292
let
328
+ − 293
val count = Unsynchronized.ref 0;
167
3e30ea95c7aa
added temporarily some timing test about conversions and simprocs
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 294
172
+ − 295
fun term_tree_aux n =
+ − 296
case n of
+ − 297
0 => (count := !count + 1; HOLogic.mk_number @{typ nat} (!count))
+ − 298
| _ => Const (@{const_name "plus"}, @{typ "nat\<Rightarrow>nat\<Rightarrow>nat"})
+ − 299
$ (term_tree_aux (n - 1)) $ (term_tree_aux (n - 1))
+ − 300
in
+ − 301
term_tree_aux n
+ − 302
end*}
+ − 303
+ − 304
text {*
178
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 305
This function generates for example:
172
+ − 306
+ − 307
@{ML_response_fake [display,gray]
329
+ − 308
"writeln (string_of_term @{context} (term_tree 2))"
172
+ − 309
"(1 + 2) + (3 + 4)"}
+ − 310
174
+ − 311
The next function constructs a goal of the form @{text "P \<dots>"} with a term
+ − 312
produced by @{ML term_tree} filled in.
167
3e30ea95c7aa
added temporarily some timing test about conversions and simprocs
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 313
*}
3e30ea95c7aa
added temporarily some timing test about conversions and simprocs
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 314
172
+ − 315
ML{*fun goal n = HOLogic.mk_Trueprop (@{term "P::nat\<Rightarrow> bool"} $ (term_tree n))*}
+ − 316
+ − 317
text {*
+ − 318
Note that the goal needs to be wrapped in a @{term "Trueprop"}. Next we define
+ − 319
two tactics, @{text "c_tac"} and @{text "s_tac"}, for the conversion and simproc,
174
+ − 320
respectively. The idea is to first apply the conversion (respectively simproc) and
351
+ − 321
then prove the remaining goal using @{ML "cheat_tac" in Skip_Proof}.
167
3e30ea95c7aa
added temporarily some timing test about conversions and simprocs
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 322
*}
3e30ea95c7aa
added temporarily some timing test about conversions and simprocs
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 323
172
+ − 324
ML{*local
225
+ − 325
fun mk_tac tac =
351
+ − 326
timing_wrapper (EVERY1 [tac, K (Skip_Proof.cheat_tac @{theory})])
172
+ − 327
in
352
+ − 328
val c_tac = mk_tac (add_tac @{context})
407
+ − 329
val s_tac = mk_tac (simp_tac
+ − 330
(HOL_basic_ss addsimprocs [@{simproc add_sp}]))
172
+ − 331
end*}
+ − 332
+ − 333
text {*
175
+ − 334
This is all we need to let the conversion run against the simproc:
167
3e30ea95c7aa
added temporarily some timing test about conversions and simprocs
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 335
*}
3e30ea95c7aa
added temporarily some timing test about conversions and simprocs
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 336
174
+ − 337
ML{*val _ = Goal.prove @{context} [] [] (goal 8) (K c_tac)
172
+ − 338
val _ = Goal.prove @{context} [] [] (goal 8) (K s_tac)*}
167
3e30ea95c7aa
added temporarily some timing test about conversions and simprocs
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 339
172
+ − 340
text {*
174
+ − 341
If you do the exercise, you can see that both ways of simplifying additions
178
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 342
perform relatively similar with perhaps some advantages for the
174
+ − 343
simproc. That means the simplifier, even if much more complicated than
+ − 344
conversions, is quite efficient for tasks it is designed for. It usually does not
+ − 345
make sense to implement general-purpose rewriting using
172
+ − 346
conversions. Conversions only have clear advantages in special situations:
+ − 347
for example if you need to have control over innermost or outermost
174
+ − 348
rewriting, or when rewriting rules are lead to non-termination.
167
3e30ea95c7aa
added temporarily some timing test about conversions and simprocs
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 349
*}
130
+ − 350
270
+ − 351
end