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_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} *}

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)*}

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(*>*)

subsection {* Tests start here *}

lemma cheat: "P" sorry

ML{*fun timing_wrapper tac st =
let 
  val t_start = start_timing ();
  val res = tac st;
  val t_end = end_timing t_start;
in
  (warning (#message t_end); res)
end*}

ML{* 
fun create_term1 0 = @{term "0::nat"}
  | create_term1 n = 
       Const (@{const_name "plus"}, @{typ "nat\<Rightarrow>nat\<Rightarrow>nat"}) 
         $ (HOLogic.mk_number @{typ "nat"} n) $ (create_term1 (n-1))
*}

ML{* 
fun create_term2 0 = @{term "0::nat"}
  | create_term2 n = 
       Const (@{const_name "plus"}, @{typ "nat\<Rightarrow>nat\<Rightarrow>nat"}) 
         $ (create_term2 (n-1)) $ (HOLogic.mk_number @{typ nat} n)
*}

ML{*
fun create_term n = 
  HOLogic.mk_Trueprop
  (@{term "P::nat\<Rightarrow> bool"} $ 
   (Const (@{const_name "plus"}, @{typ "nat\<Rightarrow>nat\<Rightarrow>nat"}) 
    $ (create_term1 n) $ (create_term2 n)))
*}

ML {*
warning (Syntax.string_of_term @{context} (create_term 4))
*}

ML {* 
val _ = Goal.prove @{context} [] [] (create_term 100) 
   (fn _ => timing_wrapper (EVERY1 [add_tac, rtac @{thm cheat}]))
*}

ML {* 
val _ = Goal.prove @{context} [] [] (create_term 100) 
   (fn _ => timing_wrapper (EVERY1 [simp_tac (HOL_basic_ss addsimprocs [@{simproc add_sp}]), rtac @{thm cheat}]))
*}

ML {* 
val _ = Goal.prove @{context} [] [] (create_term 400) 
  (fn _ => timing_wrapper (EVERY1 [add_tac, rtac @{thm cheat}]))
*}

ML {* 
val _ = Goal.prove @{context} [] [] (create_term 400) 
   (fn _ => timing_wrapper (EVERY1 [simp_tac (HOL_basic_ss addsimprocs [@{simproc add_sp}]), rtac @{thm cheat}]))
*}

end