theory Solutions
imports Base "Recipes/Timing"
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(*>*)

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

text {* 
  To measure the difference, we will create mechanically some terms involving 
  additions and then set up a goal to be simplified. To prove the remaining 
  goal we use the ``lemma'':
*}

lemma cheat: "A" sorry

text {*
  The reason is that it allows us to set up an unprovable goal where we can
  eliminate all interferences from other parts of the simplifier and
  then prove the goal using @{thm [source] cheat}. We also assume
  the timing function @{ML timing_wrapper} from Recipe~\ref{rec:timing}.

  First we define a function that returns a complete binary tree whose 
  leaves are numbers and the nodes are additions.
*}

ML{*fun term_tree n =
let
  val count = ref 0; 

  fun term_tree_aux n =
    case n of
      0 => (count := !count + 1; HOLogic.mk_number @{typ nat} (!count))
    | _ => Const (@{const_name "plus"}, @{typ "nat\<Rightarrow>nat\<Rightarrow>nat"}) 
             $ (term_tree_aux (n - 1)) $ (term_tree_aux (n - 1))
in
  term_tree_aux n
end*}

text {*
  For example

  @{ML_response_fake [display,gray] 
  "warning (Syntax.string_of_term @{context} (term_tree 2))" 
  "(1 + 2) + (3 + 4)"} 

  The next function generates a goal of the form @{text "P \<dots>"} with a term 
  filled in.
*}

ML{*fun goal n = HOLogic.mk_Trueprop (@{term "P::nat\<Rightarrow> bool"} $ (term_tree n))*}

text {*
  Note that the goal needs to be wrapped in a @{term "Trueprop"}. Next we define
  two tactics, @{text "c_tac"} and @{text "s_tac"}, for the conversion and simproc,
  respectively. The tactics first apply the conversion (respectively simproc) and 
  then prove the remaining goal using the lemma @{thm [source] cheat}.
*}

ML{*local
  fun mk_tac tac = timing_wrapper (EVERY1 [tac, rtac @{thm cheat}])
in
val c_tac = mk_tac add_tac
val s_tac = mk_tac 
             (simp_tac (HOL_basic_ss addsimprocs [@{simproc add_sp}]))
end*}

text {*
  This is all we need to let them run against each other.
*}

ML{*val _ = Goal.prove @{context} [] [] (goal 8) (K c_tac);
val _ = Goal.prove @{context} [] [] (goal 8) (K s_tac)*}

text {*
  As you can see, both versions perform relatively the same with perhaps some
  advantages for the simproc. That means the simplifier, while much more
  complicated than conversions, is quite good for tasks it is designed for. It
  usually does not make sense to implement general-purpose rewriting using
  conversions. Conversions only have clear advantages in special situations:
  for example if you need to have control over innermost or outermost
  rewriting; another situation is when rewriting rules are prone to
  non-termination.
*}

end