1 theory Solutions

     2 imports Main

     3 uses "antiquote_setup.ML"

     4      "antiquote_setup_plus.ML"

     5 begin

     6 

     7 chapter {* Solutions to Most Exercises *}

     8 

     9 text {* \solution{fun:revsum} *}

    10 

    11 ML {* 

    12   fun rev_sum t =

    13   let

    14    fun dest_sum (Const (@{const_name plus}, _) $ u $ u') = 

    15                                                       u' :: dest_sum u

    16      | dest_sum u = [u]

    17    in

    18      foldl1 (HOLogic.mk_binop @{const_name plus}) (dest_sum t)

    19    end;

    20 *}

    21 

    22 text {* \solution{fun:makesum} *}

    23 

    24 ML {*

    25   fun make_sum t1 t2 =

    26       HOLogic.mk_nat (HOLogic.dest_nat t1 + HOLogic.dest_nat t2)

    27 *}

    28 

    29 end