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 |
9 ML{*fun rev_sum ((p as Const (@{const_name plus}, _)) $ t $ u) = |
|
10 p $ u $ rev_sum t |
10 | rev_sum t = t *} |
11 | rev_sum t = t *} |
11 |
12 |
12 text {* \solution{fun:revsum typed} *} |
13 text {* |
|
14 An alternative solution using the function @{ML [index] mk_binop in HOLogic} is: |
|
15 *} |
13 |
16 |
14 ML{*fun rev_sum t = |
17 ML{*fun rev_sum t = |
15 let |
18 let |
16 fun dest_sum (Const (@{const_name plus}, _) $ u $ u') = u' :: dest_sum u |
19 fun dest_sum (Const (@{const_name plus}, _) $ u $ u') = u' :: dest_sum u |
17 | dest_sum u = [u] |
20 | dest_sum u = [u] |
18 in |
21 in |
19 foldl1 (HOLogic.mk_binop @{const_name plus}) (dest_sum t) |
22 foldl1 (HOLogic.mk_binop @{const_name plus}) (dest_sum t) |
20 end *} |
23 end *} |
21 |
|
22 |
|
23 |
24 |
24 text {* \solution{fun:makesum} *} |
25 text {* \solution{fun:makesum} *} |
25 |
26 |
26 ML{*fun make_sum t1 t2 = |
27 ML{*fun make_sum t1 t2 = |
27 HOLogic.mk_nat (HOLogic.dest_nat t1 + HOLogic.dest_nat t2) *} |
28 HOLogic.mk_nat (HOLogic.dest_nat t1 + HOLogic.dest_nat t2) *} |