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