15
9da9ba2b095b
added a solution section and some other minor additions
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1 |
theory Solutions
|
25
|
2 |
imports Base
|
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 |
|
9da9ba2b095b
added a solution section and some other minor additions
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
5 |
chapter {* Solutions to Most Exercises *}
|
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 |
|
69
|
9 |
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
|
10 |
let
|
130
|
11 |
fun dest_sum (Const (@{const_name plus}, _) $ u $ u') = u' :: dest_sum u
|
|
12 |
| dest_sum u = [u]
|
|
13 |
in
|
47
4daf913fdbe1
hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
14 |
foldl1 (HOLogic.mk_binop @{const_name plus}) (dest_sum t)
|
130
|
15 |
end *}
|
15
9da9ba2b095b
added a solution section and some other minor additions
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
16 |
|
9da9ba2b095b
added a solution section and some other minor additions
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
17 |
text {* \solution{fun:makesum} *}
|
9da9ba2b095b
added a solution section and some other minor additions
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
18 |
|
69
|
19 |
ML{*fun make_sum t1 t2 =
|
130
|
20 |
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
|
21 |
|
56
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
22 |
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
|
23 |
|
130
|
24 |
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
|
25 |
|
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
26 |
val scan_cmt =
|
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
27 |
let
|
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
28 |
val begin_cmt = Scan.this_string "(*"
|
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
29 |
val end_cmt = Scan.this_string "*)"
|
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
30 |
in
|
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
31 |
begin_cmt |-- Scan.repeat (Scan.unless end_cmt any) --| end_cmt
|
58
|
32 |
>> (enclose "(**" "**)" o implode)
|
56
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
33 |
end
|
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
34 |
|
130
|
35 |
val parser = Scan.repeat (scan_cmt || any)
|
|
36 |
|
56
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
37 |
val scan_all =
|
130
|
38 |
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
|
39 |
|
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
40 |
text {*
|
58
|
41 |
By using @{text "#> fst"} in the last line, the function
|
|
42 |
@{ML scan_all} retruns a string, instead of the pair a parser would
|
|
43 |
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
|
44 |
|
80
|
45 |
@{ML_response [display,gray]
|
|
46 |
"let
|
130
|
47 |
val input1 = (explode \"foo bar\")
|
|
48 |
val input2 = (explode \"foo (*test*) bar (*test*)\")
|
|
49 |
in
|
|
50 |
(scan_all input1, scan_all input2)
|
|
51 |
end"
|
|
52 |
"(\"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
|
53 |
*}
|
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
54 |
|
130
|
55 |
text {* \solution{ex:addsimproc} *}
|
|
56 |
|
|
57 |
ML{*fun dest_sum term =
|
|
58 |
case term of
|
|
59 |
(@{term "(op +):: nat \<Rightarrow> nat \<Rightarrow> nat"} $ t1 $ t2) =>
|
|
60 |
(snd (HOLogic.dest_number t1), snd (HOLogic.dest_number t2))
|
|
61 |
| _ => raise TERM ("dest_sum", [term])
|
|
62 |
|
|
63 |
fun get_sum_thm ctxt t (n1, n2) =
|
|
64 |
let
|
|
65 |
val sum = HOLogic.mk_number @{typ "nat"} (n1 + n2)
|
132
|
66 |
val goal = Logic.mk_equals (t, sum)
|
130
|
67 |
in
|
132
|
68 |
Goal.prove ctxt [] [] goal (K (arith_tac ctxt 1))
|
130
|
69 |
end
|
|
70 |
|
|
71 |
fun add_sp_aux ss t =
|
|
72 |
let
|
|
73 |
val ctxt = Simplifier.the_context ss
|
|
74 |
val t' = term_of t
|
|
75 |
in
|
|
76 |
SOME (get_sum_thm ctxt t' (dest_sum t'))
|
|
77 |
handle TERM _ => NONE
|
|
78 |
end*}
|
|
79 |
|
|
80 |
text {* The setup for the simproc is *}
|
|
81 |
|
|
82 |
simproc_setup add_sp ("t1 + t2") = {* K add_sp_aux *}
|
|
83 |
|
|
84 |
text {* and a test case is the lemma *}
|
|
85 |
|
|
86 |
lemma "P (Suc (99 + 1)) ((0 + 0)::nat) (Suc (3 + 3 + 3)) (4 + 1)"
|
|
87 |
apply(tactic {* simp_tac (HOL_ss addsimprocs [@{simproc add_sp}]) 1 *})
|
|
88 |
txt {*
|
|
89 |
where the simproc produces the goal state
|
|
90 |
|
|
91 |
\begin{minipage}{\textwidth}
|
|
92 |
@{subgoals [display]}
|
|
93 |
\end{minipage}
|
|
94 |
*}(*<*)oops(*>*)
|
|
95 |
|
|
96 |
|
|
97 |
|
15
9da9ba2b095b
added a solution section and some other minor additions
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
98 |
end |