
diff -r 8939b8fd8603 -r 069d525f8f1d CookBook/Solutions.thy
--- a/CookBook/Solutions.thy	Wed Mar 18 23:52:51 2009 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,218 +0,0 @@
-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 %gray 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)
-
-fun add_tac ctxt = CSUBGOAL (fn (goal, i) =>
-  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)*}
-
-text {*
-  A test case for this conversion is as follows
-*}
-
-lemma "P (Suc (99 + 1)) ((0 + 0)::nat) (Suc (3 + 3 + 3)) (4 + 1)"
-  apply(tactic {* add_tac @{context} 1 *})?
-txt {* 
-  where it produces the goal state
-  
-  \begin{minipage}{\textwidth}
-  @{subgoals [display]}
-  \end{minipage}\bigskip
-*}(*<*)oops(*>*)
-
-text {* \solution{ex:addconversion} *}
-
-text {* 
-  We use the timing function @{ML timing_wrapper} from Recipe~\ref{rec:timing}.
-  To measure any difference between the simproc and conversion, we will create 
-  mechanically terms involving additions and then set up a goal to be 
-  simplified. We have to be careful to set up the goal so that
-  other parts of the simplifier do not interfere. For this we construct an
-  unprovable goal which, after simplification, we are going to ``prove'' with
-  the help of the lemma:
-*}
-
-lemma cheat: "A" sorry
-
-text {*
-  For constructing test cases, we first 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 {*
-  This function generates for example:
-
-  @{ML_response_fake [display,gray] 
-  "warning (Syntax.string_of_term @{context} (term_tree 2))" 
-  "(1 + 2) + (3 + 4)"} 
-
-  The next function constructs a goal of the form @{text "P \<dots>"} with a term 
-  produced by @{ML term_tree} 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 idea is to first apply the conversion (respectively simproc) and 
-  then prove the remaining goal using the @{thm [source] cheat}-lemma.
-*}
-
-ML{*local
-  fun mk_tac tac = timing_wrapper (EVERY1 [tac, rtac @{thm cheat}])
-in
-val c_tac = mk_tac (add_tac @{context}) 
-val s_tac = mk_tac (simp_tac (HOL_basic_ss addsimprocs [@{simproc add_sp}]))
-end*}
-
-text {*
-  This is all we need to let the conversion run against the simproc:
-*}
-
-ML{*val _ = Goal.prove @{context} [] [] (goal 8) (K c_tac)
-val _ = Goal.prove @{context} [] [] (goal 8) (K s_tac)*}
-
-text {*
-  If you do the exercise, you can see that both ways of simplifying additions
-  perform relatively similar with perhaps some advantages for the
-  simproc. That means the simplifier, even if much more complicated than
-  conversions, is quite efficient 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, or when rewriting rules are lead to non-termination.
-*}
-
-end
\ No newline at end of file




