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