theory Solutions

begin

chapter {* Solutions to Most Exercises\label{ch:solutions} *}

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_basic_ss addsimprocs [@{simproc add_sp}]) 1 *})

txt {* 

  where the simproc produces the goal state

  \begin{minipage}{\textwidth}

  @{subgoals [display]}

  \end{minipage}\bigskip

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

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

text {*

  The following code assumes the function @{ML dest_sum} from the previous

  exercise.

*}

ML{*fun add_simple_conv ctxt ctrm =

let

  val trm =  Thm.term_of ctrm

in 

  get_sum_thm ctxt trm (dest_sum trm)

end

fun add_conv ctxt ctrm =

  (case Thm.term_of ctrm of

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

         (Conv.binop_conv (add_conv ctxt)

          then_conv (Conv.try_conv (add_simple_conv ctxt))) ctrm         

    | _ $ _ => Conv.combination_conv 

                 (add_conv ctxt) (add_conv ctxt) ctrm

    | Abs _ => Conv.abs_conv (fn (_, ctxt) => add_conv ctxt) ctxt ctrm

    | _ => Conv.all_conv ctrm)

val add_tac = CSUBGOAL (fn (goal, i) =>

  let

    val ctxt = ProofContext.init (Thm.theory_of_cterm goal)

  in

    CONVERSION

      (Conv.params_conv ~1 (fn ctxt =>

        (Conv.prems_conv ~1 (add_conv ctxt) then_conv

          Conv.concl_conv ~1 (add_conv ctxt))) ctxt) i

  end)*}

text {*

  A test case is as follows

*}

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

  apply(tactic {* add_tac 1 *})?

txt {* 

  where the conversion produces the goal state

  \begin{minipage}{\textwidth}

  @{subgoals [display]}

  \end{minipage}\bigskip

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

*}

*}

*}

*}

*}

*}

end