| author | Christian Urban <urbanc@in.tum.de> |
| Mon, 06 Oct 2008 10:11:08 -0400 | |
| changeset 20 | 5ae6a1bb91c9 |
| parent 15 | 9da9ba2b095b |
| child 25 | e2f9f94b26d4 |
| 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 |
|
9da9ba2b095b
added a solution section and some other minor additions
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
2 |
imports Main |
|
9da9ba2b095b
added a solution section and some other minor additions
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
3 |
uses "antiquote_setup.ML" |
|
9da9ba2b095b
added a solution section and some other minor additions
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
4 |
"antiquote_setup_plus.ML" |
|
9da9ba2b095b
added a solution section and some other minor additions
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
5 |
begin |
|
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 |
chapter {* Solutions to Most Exercises *}
|
|
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 |
text {* \solution{fun:revsum} *}
|
|
9da9ba2b095b
added a solution section and some other minor additions
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
10 |
|
|
9da9ba2b095b
added a solution section and some other minor additions
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
11 |
ML {*
|
|
9da9ba2b095b
added a solution section and some other minor additions
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
12 |
fun rev_sum t = |
|
9da9ba2b095b
added a solution section and some other minor additions
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
13 |
let |
|
9da9ba2b095b
added a solution section and some other minor additions
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
14 |
fun dest_sum (Const (@{const_name plus}, _) $ u $ u') =
|
|
9da9ba2b095b
added a solution section and some other minor additions
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
15 |
u' :: dest_sum u |
|
9da9ba2b095b
added a solution section and some other minor additions
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
16 |
| dest_sum u = [u] |
|
9da9ba2b095b
added a solution section and some other minor additions
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
17 |
in |
|
9da9ba2b095b
added a solution section and some other minor additions
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
18 |
foldl1 (HOLogic.mk_binop @{const_name plus}) (dest_sum t)
|
|
9da9ba2b095b
added a solution section and some other minor additions
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
19 |
end; |
|
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 |
|
|
9da9ba2b095b
added a solution section and some other minor additions
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
22 |
text {* \solution{fun:makesum} *}
|
|
9da9ba2b095b
added a solution section and some other minor additions
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
23 |
|
|
9da9ba2b095b
added a solution section and some other minor additions
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
24 |
ML {*
|
|
9da9ba2b095b
added a solution section and some other minor additions
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
25 |
fun make_sum t1 t2 = |
|
9da9ba2b095b
added a solution section and some other minor additions
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
26 |
HOLogic.mk_nat (HOLogic.dest_nat t1 + HOLogic.dest_nat t2) |
|
9da9ba2b095b
added a solution section and some other minor additions
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
27 |
*} |
|
9da9ba2b095b
added a solution section and some other minor additions
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
28 |
|
|
9da9ba2b095b
added a solution section and some other minor additions
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
29 |
end |