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 =

val parser = Scan.repeat (scan_cmt || any)

val scan_all =

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 {* 

  \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