equal
deleted
inserted
replaced
11 fun dest_sum (Const (@{const_name plus}, _) $ u $ u') = u' :: dest_sum u |
11 fun dest_sum (Const (@{const_name plus}, _) $ u $ u') = u' :: dest_sum u |
12 | dest_sum u = [u] |
12 | dest_sum u = [u] |
13 in |
13 in |
14 foldl1 (HOLogic.mk_binop @{const_name plus}) (dest_sum t) |
14 foldl1 (HOLogic.mk_binop @{const_name plus}) (dest_sum t) |
15 end *} |
15 end *} |
|
16 |
|
17 (* Alternative Solution: |
|
18 fun rev_sum((plus as Const(@{const_name plus},_)) $ t $ u) = plus $ u $ rev_sum t |
|
19 | rev_sum t = t |
|
20 *) |
16 |
21 |
17 text {* \solution{fun:makesum} *} |
22 text {* \solution{fun:makesum} *} |
18 |
23 |
19 ML{*fun make_sum t1 t2 = |
24 ML{*fun make_sum t1 t2 = |
20 HOLogic.mk_nat (HOLogic.dest_nat t1 + HOLogic.dest_nat t2) *} |
25 HOLogic.mk_nat (HOLogic.dest_nat t1 + HOLogic.dest_nat t2) *} |