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