theory Solutions

imports Base

uses "infix_conv.ML"

begin

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