ProgTutorial/Solutions.thy
changeset 270 bfcabed9079e
parent 225 7859fc59249a
child 271 949957531f63
equal deleted inserted replaced
269:3e084d62885c 270:bfcabed9079e
    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) *}