15
9da9ba2b095b
added a solution section and some other minor additions
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 1
theory Solutions
172
+ − 2
imports Base "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
156
+ − 5
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
+ − 6
9da9ba2b095b
added a solution section and some other minor additions
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 7
text {* \solution{fun:revsum} *}
9da9ba2b095b
added a solution section and some other minor additions
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 8
271
+ − 9
ML{*fun rev_sum((p as Const(@{const_name plus},_)) $ t $ u) = p $ u $ rev_sum t
+ − 10
| rev_sum t = t *}
+ − 11
+ − 12
text {* \solution{fun:revsum typed} *}
+ − 13
69
+ − 14
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
+ − 15
let
130
+ − 16
fun dest_sum (Const (@{const_name plus}, _) $ u $ u') = u' :: dest_sum u
+ − 17
| dest_sum u = [u]
+ − 18
in
47
4daf913fdbe1
hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 19
foldl1 (HOLogic.mk_binop @{const_name plus}) (dest_sum t)
130
+ − 20
end *}
15
9da9ba2b095b
added a solution section and some other minor additions
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 21
271
+ − 22
270
+ − 23
15
9da9ba2b095b
added a solution section and some other minor additions
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 24
text {* \solution{fun:makesum} *}
9da9ba2b095b
added a solution section and some other minor additions
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 25
69
+ − 26
ML{*fun make_sum t1 t2 =
130
+ − 27
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
+ − 28
56
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 29
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
+ − 30
130
+ − 31
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
+ − 32
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 33
val scan_cmt =
168
+ − 34
let
+ − 35
val begin_cmt = Scan.this_string "(*"
+ − 36
val end_cmt = Scan.this_string "*)"
+ − 37
in
+ − 38
begin_cmt |-- Scan.repeat (Scan.unless end_cmt any) --| end_cmt
+ − 39
>> (enclose "(**" "**)" o implode)
+ − 40
end
56
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 41
130
+ − 42
val parser = Scan.repeat (scan_cmt || any)
+ − 43
56
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 44
val scan_all =
168
+ − 45
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
+ − 46
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 47
text {*
58
+ − 48
By using @{text "#> fst"} in the last line, the function
+ − 49
@{ML scan_all} retruns a string, instead of the pair a parser would
+ − 50
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
+ − 51
80
+ − 52
@{ML_response [display,gray]
+ − 53
"let
130
+ − 54
val input1 = (explode \"foo bar\")
+ − 55
val input2 = (explode \"foo (*test*) bar (*test*)\")
+ − 56
in
+ − 57
(scan_all input1, scan_all input2)
+ − 58
end"
+ − 59
"(\"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
+ − 60
*}
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 61
130
+ − 62
text {* \solution{ex:addsimproc} *}
+ − 63
+ − 64
ML{*fun dest_sum term =
+ − 65
case term of
+ − 66
(@{term "(op +):: nat \<Rightarrow> nat \<Rightarrow> nat"} $ t1 $ t2) =>
+ − 67
(snd (HOLogic.dest_number t1), snd (HOLogic.dest_number t2))
+ − 68
| _ => raise TERM ("dest_sum", [term])
+ − 69
+ − 70
fun get_sum_thm ctxt t (n1, n2) =
+ − 71
let
+ − 72
val sum = HOLogic.mk_number @{typ "nat"} (n1 + n2)
132
+ − 73
val goal = Logic.mk_equals (t, sum)
130
+ − 74
in
214
+ − 75
Goal.prove ctxt [] [] goal (K (Arith_Data.arith_tac ctxt 1))
130
+ − 76
end
+ − 77
+ − 78
fun add_sp_aux ss t =
+ − 79
let
+ − 80
val ctxt = Simplifier.the_context ss
+ − 81
val t' = term_of t
+ − 82
in
+ − 83
SOME (get_sum_thm ctxt t' (dest_sum t'))
+ − 84
handle TERM _ => NONE
+ − 85
end*}
+ − 86
+ − 87
text {* The setup for the simproc is *}
+ − 88
177
+ − 89
simproc_setup %gray add_sp ("t1 + t2") = {* K add_sp_aux *}
130
+ − 90
+ − 91
text {* and a test case is the lemma *}
+ − 92
+ − 93
lemma "P (Suc (99 + 1)) ((0 + 0)::nat) (Suc (3 + 3 + 3)) (4 + 1)"
167
3e30ea95c7aa
added temporarily some timing test about conversions and simprocs
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 94
apply(tactic {* simp_tac (HOL_basic_ss addsimprocs [@{simproc add_sp}]) 1 *})
130
+ − 95
txt {*
+ − 96
where the simproc produces the goal state
+ − 97
+ − 98
\begin{minipage}{\textwidth}
+ − 99
@{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
+ − 100
\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
+ − 101
*}(*<*)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
+ − 102
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
+ − 103
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
+ − 104
168
+ − 105
text {*
+ − 106
The following code assumes the function @{ML dest_sum} from the previous
+ − 107
exercise.
+ − 108
*}
+ − 109
166
+ − 110
ML{*fun add_simple_conv ctxt ctrm =
+ − 111
let
+ − 112
val trm = Thm.term_of ctrm
+ − 113
in
+ − 114
get_sum_thm ctxt trm (dest_sum trm)
+ − 115
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
+ − 116
166
+ − 117
fun add_conv ctxt ctrm =
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
+ − 118
(case Thm.term_of ctrm of
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
+ − 119
@{term "(op +)::nat \<Rightarrow> nat \<Rightarrow> nat"} $ _ $ _ =>
166
+ − 120
(Conv.binop_conv (add_conv ctxt)
+ − 121
then_conv (Conv.try_conv (add_simple_conv ctxt))) ctrm
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
+ − 122
| _ $ _ => Conv.combination_conv
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
+ − 123
(add_conv ctxt) (add_conv ctxt) ctrm
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
+ − 124
| Abs _ => Conv.abs_conv (fn (_, ctxt) => add_conv ctxt) ctxt ctrm
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
+ − 125
| _ => Conv.all_conv ctrm)
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
+ − 126
186
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 127
fun add_tac ctxt = CSUBGOAL (fn (goal, i) =>
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 128
CONVERSION
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 129
(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
+ − 130
(Conv.prems_conv ~1 (add_conv ctxt) then_conv
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 131
Conv.concl_conv ~1 (add_conv ctxt))) ctxt) i)*}
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
+ − 132
168
+ − 133
text {*
175
+ − 134
A test case for this conversion is as follows
168
+ − 135
*}
+ − 136
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
+ − 137
lemma "P (Suc (99 + 1)) ((0 + 0)::nat) (Suc (3 + 3 + 3)) (4 + 1)"
186
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 138
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
+ − 139
txt {*
175
+ − 140
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
+ − 141
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
+ − 142
\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
+ − 143
@{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
+ − 144
\end{minipage}\bigskip
130
+ − 145
*}(*<*)oops(*>*)
+ − 146
172
+ − 147
text {* \solution{ex:addconversion} *}
167
3e30ea95c7aa
added temporarily some timing test about conversions and simprocs
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 148
172
+ − 149
text {*
174
+ − 150
We use the timing function @{ML timing_wrapper} from Recipe~\ref{rec:timing}.
+ − 151
To measure any difference between the simproc and conversion, we will create
+ − 152
mechanically terms involving additions and then set up a goal to be
+ − 153
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
+ − 154
other parts of the simplifier do not interfere. For this we construct an
174
+ − 155
unprovable goal which, after simplification, we are going to ``prove'' with
192
+ − 156
the help of ``\isacommand{sorry}'', that is the method @{ML SkipProof.cheat_tac}
167
3e30ea95c7aa
added temporarily some timing test about conversions and simprocs
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 157
174
+ − 158
For constructing test cases, we first define a function that returns a
+ − 159
complete binary tree whose leaves are numbers and the nodes are
+ − 160
additions.
167
3e30ea95c7aa
added temporarily some timing test about conversions and simprocs
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 161
*}
3e30ea95c7aa
added temporarily some timing test about conversions and simprocs
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 162
172
+ − 163
ML{*fun term_tree n =
+ − 164
let
+ − 165
val count = ref 0;
167
3e30ea95c7aa
added temporarily some timing test about conversions and simprocs
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 166
172
+ − 167
fun term_tree_aux n =
+ − 168
case n of
+ − 169
0 => (count := !count + 1; HOLogic.mk_number @{typ nat} (!count))
+ − 170
| _ => Const (@{const_name "plus"}, @{typ "nat\<Rightarrow>nat\<Rightarrow>nat"})
+ − 171
$ (term_tree_aux (n - 1)) $ (term_tree_aux (n - 1))
+ − 172
in
+ − 173
term_tree_aux n
+ − 174
end*}
+ − 175
+ − 176
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
+ − 177
This function generates for example:
172
+ − 178
+ − 179
@{ML_response_fake [display,gray]
239
+ − 180
"writeln (Syntax.string_of_term @{context} (term_tree 2))"
172
+ − 181
"(1 + 2) + (3 + 4)"}
+ − 182
174
+ − 183
The next function constructs a goal of the form @{text "P \<dots>"} with a term
+ − 184
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
+ − 185
*}
3e30ea95c7aa
added temporarily some timing test about conversions and simprocs
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 186
172
+ − 187
ML{*fun goal n = HOLogic.mk_Trueprop (@{term "P::nat\<Rightarrow> bool"} $ (term_tree n))*}
+ − 188
+ − 189
text {*
+ − 190
Note that the goal needs to be wrapped in a @{term "Trueprop"}. Next we define
+ − 191
two tactics, @{text "c_tac"} and @{text "s_tac"}, for the conversion and simproc,
174
+ − 192
respectively. The idea is to first apply the conversion (respectively simproc) and
192
+ − 193
then prove the remaining goal using @{ML "cheat_tac" in SkipProof}.
167
3e30ea95c7aa
added temporarily some timing test about conversions and simprocs
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 194
*}
3e30ea95c7aa
added temporarily some timing test about conversions and simprocs
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 195
172
+ − 196
ML{*local
225
+ − 197
fun mk_tac tac =
+ − 198
timing_wrapper (EVERY1 [tac, K (SkipProof.cheat_tac @{theory})])
172
+ − 199
in
186
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 200
val c_tac = mk_tac (add_tac @{context})
174
+ − 201
val s_tac = mk_tac (simp_tac (HOL_basic_ss addsimprocs [@{simproc add_sp}]))
172
+ − 202
end*}
+ − 203
+ − 204
text {*
175
+ − 205
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
+ − 206
*}
3e30ea95c7aa
added temporarily some timing test about conversions and simprocs
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 207
174
+ − 208
ML{*val _ = Goal.prove @{context} [] [] (goal 8) (K c_tac)
172
+ − 209
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
+ − 210
172
+ − 211
text {*
174
+ − 212
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
+ − 213
perform relatively similar with perhaps some advantages for the
174
+ − 214
simproc. That means the simplifier, even if much more complicated than
+ − 215
conversions, is quite efficient for tasks it is designed for. It usually does not
+ − 216
make sense to implement general-purpose rewriting using
172
+ − 217
conversions. Conversions only have clear advantages in special situations:
+ − 218
for example if you need to have control over innermost or outermost
174
+ − 219
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
+ − 220
*}
130
+ − 221
270
+ − 222
end