theory Solutions+
−
imports Base+
−
uses "infix_conv.ML"+
−
begin+
−
+
−
chapter {* Solutions to Most Exercises *}+
−
+
−
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+
−