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 \ nat \ 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 \ nat \ 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\nat\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 \"} with a term - produced by @{ML term_tree} filled in. -*} - -ML{*fun goal n = HOLogic.mk_Trueprop (@{term "P::nat\ 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