theory Solutions

imports Base

begin

chapter {* Solutions to Most Exercises *}

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

ML{*fun rev_sum t =

let

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

    | dest_sum u = [u]

in

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

end *}

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

ML{*fun make_sum t1 t2 =

      HOLogic.mk_nat (HOLogic.dest_nat t1 + HOLogic.dest_nat t2) *}

text {* \solution{ex:scancmts} *}

ML{*val any = Scan.one (Symbol.not_eof)

val scan_cmt =

  let

    val begin_cmt = Scan.this_string "(*" 

    val end_cmt = Scan.this_string "*)"

  in

   begin_cmt |-- Scan.repeat (Scan.unless end_cmt any) --| end_cmt 

    >> (enclose "(**" "**)" o implode)

  end

val parser = Scan.repeat (scan_cmt || any)

val scan_all =

  Scan.finite Symbol.stopper parser >> implode #> fst *}

text {*

  By using @{text "#> fst"} in the last line, the function 

  @{ML scan_all} retruns a string, instead of the pair a parser would

  normally return. For example:

  @{ML_response [display,gray]

"let

  val input1 = (explode \"foo bar\")

  val input2 = (explode \"foo (*test*) bar (*test*)\")

in

  (scan_all input1, scan_all input2)

end"

"(\"foo bar\", \"foo (**test**) bar (**test**)\")"}

*}

text {* \solution{ex:addsimproc} *}

ML{*fun dest_sum term =

  case term of 

    (@{term "(op +):: nat \<Rightarrow> nat \<Rightarrow> nat"} $ t1 $ t2) =>

        (snd (HOLogic.dest_number t1), snd (HOLogic.dest_number t2))

  | _ => raise TERM ("dest_sum", [term])

fun get_sum_thm ctxt t (n1, n2) =  

let 

  val sum = HOLogic.mk_number @{typ "nat"} (n1 + n2)

  val goal = Logic.mk_equals (t, sum)

in

  Goal.prove ctxt [] [] goal (K (arith_tac ctxt 1))

end

fun add_sp_aux ss t =

let 

  val ctxt = Simplifier.the_context ss

  val t' = term_of t

in

  SOME (get_sum_thm ctxt t' (dest_sum t'))

  handle TERM _ => NONE

end*}

text {* The setup for the simproc is *}

simproc_setup add_sp ("t1 + t2") = {* K add_sp_aux *}

text {* and a test case is the lemma *}

lemma "P (Suc (99 + 1)) ((0 + 0)::nat) (Suc (3 + 3 + 3)) (4 + 1)"

  apply(tactic {* simp_tac (HOL_ss addsimprocs [@{simproc add_sp}]) 1 *})

txt {* 

  where the simproc produces the goal state

  \begin{minipage}{\textwidth}

  @{subgoals [display]}

*}(*<*)oops(*>*)

end