| author | Christian Urban <urbanc@in.tum.de> |
| Tue, 16 Dec 2008 08:08:44 +0000 | |
| changeset 56 | 126646f2aa88 |
| parent 47 | 4daf913fdbe1 |
| child 58 | f3794c231898 |
| permissions | -rw-r--r-- |
|
15
9da9ba2b095b
added a solution section and some other minor additions
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1 |
theory Solutions |
|
25
e2f9f94b26d4
Antiquotation setup is now contained in theory Base.
berghofe
parents:
15
diff
changeset
|
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 |
|
|
9da9ba2b095b
added a solution section and some other minor additions
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
9 |
ML {*
|
|
47
4daf913fdbe1
hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
parents:
35
diff
changeset
|
10 |
fun rev_sum t = |
|
4daf913fdbe1
hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
parents:
35
diff
changeset
|
11 |
let |
|
4daf913fdbe1
hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
parents:
35
diff
changeset
|
12 |
fun dest_sum (Const (@{const_name plus}, _) $ u $ u') = u' :: dest_sum u
|
|
4daf913fdbe1
hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
parents:
35
diff
changeset
|
13 |
| dest_sum u = [u] |
|
4daf913fdbe1
hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
parents:
35
diff
changeset
|
14 |
in |
|
4daf913fdbe1
hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
parents:
35
diff
changeset
|
15 |
foldl1 (HOLogic.mk_binop @{const_name plus}) (dest_sum t)
|
|
4daf913fdbe1
hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
parents:
35
diff
changeset
|
16 |
end; |
|
15
9da9ba2b095b
added a solution section and some other minor additions
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
17 |
*} |
|
9da9ba2b095b
added a solution section and some other minor additions
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
18 |
|
|
9da9ba2b095b
added a solution section and some other minor additions
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
19 |
text {* \solution{fun:makesum} *}
|
|
9da9ba2b095b
added a solution section and some other minor additions
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
20 |
|
|
9da9ba2b095b
added a solution section and some other minor additions
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
21 |
ML {*
|
|
47
4daf913fdbe1
hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
parents:
35
diff
changeset
|
22 |
fun make_sum t1 t2 = |
|
4daf913fdbe1
hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
parents:
35
diff
changeset
|
23 |
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
|
24 |
*} |
|
9da9ba2b095b
added a solution section and some other minor additions
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
25 |
|
|
56
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents:
47
diff
changeset
|
26 |
text {* \solution{ex:scancmts} *}
|
|
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents:
47
diff
changeset
|
27 |
|
|
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents:
47
diff
changeset
|
28 |
ML {*
|
|
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents:
47
diff
changeset
|
29 |
val any = Scan.one (Symbol.not_eof); |
|
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents:
47
diff
changeset
|
30 |
|
|
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents:
47
diff
changeset
|
31 |
val scan_cmt = |
|
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents:
47
diff
changeset
|
32 |
let |
|
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents:
47
diff
changeset
|
33 |
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>
parents:
47
diff
changeset
|
34 |
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>
parents:
47
diff
changeset
|
35 |
in |
|
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents:
47
diff
changeset
|
36 |
begin_cmt |-- Scan.repeat (Scan.unless end_cmt any) --| end_cmt |
|
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents:
47
diff
changeset
|
37 |
>> (enclose "(**" "**)" o implode) |
|
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents:
47
diff
changeset
|
38 |
end |
|
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents:
47
diff
changeset
|
39 |
|
|
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents:
47
diff
changeset
|
40 |
val scan_all = |
|
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents:
47
diff
changeset
|
41 |
Scan.finite Symbol.stopper (Scan.repeat (scan_cmt || any)) |
|
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents:
47
diff
changeset
|
42 |
>> implode #> fst |
|
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents:
47
diff
changeset
|
43 |
*} |
|
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents:
47
diff
changeset
|
44 |
|
|
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents:
47
diff
changeset
|
45 |
text {*
|
|
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents:
47
diff
changeset
|
46 |
By using @{ML_text "#> fst"} in the last line, the function
|
|
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents:
47
diff
changeset
|
47 |
@{ML scan_all} retruns a string instead of a pair. For example:
|
|
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents:
47
diff
changeset
|
48 |
|
|
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents:
47
diff
changeset
|
49 |
@{ML_response [display] "scan_all (explode \"foo bar\")" "\"foo bar\""}
|
|
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents:
47
diff
changeset
|
50 |
|
|
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents:
47
diff
changeset
|
51 |
@{ML_response [display] "scan_all (explode \"foo (*test*) bar (*test*)\")"
|
|
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents:
47
diff
changeset
|
52 |
"\"foo (**test**) bar (**test**)\""} |
|
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents:
47
diff
changeset
|
53 |
|
|
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents:
47
diff
changeset
|
54 |
*} |
|
126646f2aa88
added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents:
47
diff
changeset
|
55 |
|
|
15
9da9ba2b095b
added a solution section and some other minor additions
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
56 |
end |