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+
−