theory Solutions
imports Base
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_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 {*
  (FIXME This solution works but is awkward.)
*}

ML{*fun add_conv ctxt ctrm =
  (case Thm.term_of ctrm of
     @{term "(op +)::nat \<Rightarrow> nat \<Rightarrow> nat"} $ _ $ _ => 
         (let
            val eq1 = Conv.binop_conv (add_conv ctxt) ctrm;
            val ctrm' = Thm.rhs_of eq1;
            val trm' = Thm.term_of ctrm';
            val eq2 = Conv.rewr_conv (get_sum_thm ctxt trm' (dest_sum trm')) ctrm'
          in
             Thm.transitive eq1 eq2
          end)       
    | _ $ _ => 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)*}

lemma "P (Suc (99 + 1)) ((0 + 0)::nat) (Suc (3 + 3 + 3)) (4 + 1)"
  apply(tactic {* add_tac 1 *})?
txt {* 
  where the simproc produces the goal state
  
  \begin{minipage}{\textwidth}
  @{subgoals [display]}
  \end{minipage}\bigskip
*}(*<*)oops(*>*)


end