equal
deleted
inserted
replaced
4 |
4 |
5 chapter {* Solutions to Most Exercises\label{ch:solutions} *} |
5 chapter {* Solutions to Most Exercises\label{ch:solutions} *} |
6 |
6 |
7 text {* \solution{fun:revsum} *} |
7 text {* \solution{fun:revsum} *} |
8 |
8 |
|
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 |
9 ML{*fun rev_sum t = |
14 ML{*fun rev_sum t = |
10 let |
15 let |
11 fun dest_sum (Const (@{const_name plus}, _) $ u $ u') = u' :: dest_sum u |
16 fun dest_sum (Const (@{const_name plus}, _) $ u $ u') = u' :: dest_sum u |
12 | dest_sum u = [u] |
17 | dest_sum u = [u] |
13 in |
18 in |
14 foldl1 (HOLogic.mk_binop @{const_name plus}) (dest_sum t) |
19 foldl1 (HOLogic.mk_binop @{const_name plus}) (dest_sum t) |
15 end *} |
20 end *} |
|
21 |
|
22 |
16 |
23 |
17 text {* \solution{fun:makesum} *} |
24 text {* \solution{fun:makesum} *} |
18 |
25 |
19 ML{*fun make_sum t1 t2 = |
26 ML{*fun make_sum t1 t2 = |
20 HOLogic.mk_nat (HOLogic.dest_nat t1 + HOLogic.dest_nat t2) *} |
27 HOLogic.mk_nat (HOLogic.dest_nat t1 + HOLogic.dest_nat t2) *} |