# HG changeset patch # User Christian Urban # Date 1236903355 -3600 # Node ID a29b81d4fa8882f7a0ad2cb457444e38ba423b7f # Parent d820cb5873ea996052027c50252d7adc92fbf51f some minor polishing diff -r d820cb5873ea -r a29b81d4fa88 CookBook/Solutions.thy --- a/CookBook/Solutions.thy Thu Mar 12 18:39:10 2009 +0000 +++ b/CookBook/Solutions.thy Fri Mar 13 01:15:55 2009 +0100 @@ -144,21 +144,21 @@ text {* \solution{ex:addconversion} *} text {* - To measure the difference, we will create mechanically some terms involving - additions and then set up a goal to be simplified. To prove the remaining - goal we use the ``lemma'': + 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 set up an + unprovable goal which, after simplification, we are going to ``prove'' with + the help of the lemma: *} lemma cheat: "A" sorry text {* - The reason is that it allows us to set up an unprovable goal where we can - eliminate all interferences from other parts of the simplifier and - then prove the goal using @{thm [source] cheat}. We also assume - the timing function @{ML timing_wrapper} from Recipe~\ref{rec:timing}. - - First we define a function that returns a complete binary tree whose - leaves are numbers and the nodes are additions. + 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 = @@ -175,14 +175,14 @@ end*} text {* - For example + 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 generates a goal of the form @{text "P \"} with a term - filled in. + 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))*} @@ -190,7 +190,7 @@ 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 tactics first apply the conversion (respectively simproc) and + respectively. The idea is to first apply the conversion (respectively simproc) and then prove the remaining goal using the lemma @{thm [source] cheat}. *} @@ -198,26 +198,25 @@ fun mk_tac tac = timing_wrapper (EVERY1 [tac, rtac @{thm cheat}]) in val c_tac = mk_tac add_tac -val s_tac = mk_tac - (simp_tac (HOL_basic_ss addsimprocs [@{simproc add_sp}])) +val s_tac = mk_tac (simp_tac (HOL_basic_ss addsimprocs [@{simproc add_sp}])) end*} text {* - This is all we need to let them run against each other. + This is all we need to let the conversion run against the simproc. *} -ML{*val _ = Goal.prove @{context} [] [] (goal 8) (K c_tac); +ML{*val _ = Goal.prove @{context} [] [] (goal 8) (K c_tac) val _ = Goal.prove @{context} [] [] (goal 8) (K s_tac)*} text {* - As you can see, both versions perform relatively the same with perhaps some - advantages for the simproc. That means the simplifier, while much more - complicated than conversions, is quite good for tasks it is designed for. It - usually does not make sense to implement general-purpose rewriting using + If you do the exercise, you can see that both ways of simplifying additions + perform relatively the same 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; another situation is when rewriting rules are prone to - non-termination. + rewriting, or when rewriting rules are lead to non-termination. *} end \ No newline at end of file diff -r d820cb5873ea -r a29b81d4fa88 CookBook/Tactical.thy --- a/CookBook/Tactical.thy Thu Mar 12 18:39:10 2009 +0000 +++ b/CookBook/Tactical.thy Fri Mar 13 01:15:55 2009 +0100 @@ -1762,9 +1762,9 @@ Note that the actual response in this example is @{term "2 + 10 \ 2 + (10::nat)"}, since the pretty-printer for @{ML_type cterm}s already beta-normalises terms. - But by the way how we constructed the term (using the function - @{ML Thm.capply}, which is the application @{ML $} for @{ML_type cterm}s), - we can be sure the left-hand side must contain beta-redexes. Indeed + But how we constructed the term (using the function + @{ML Thm.capply}, which is the application @{ML $} for @{ML_type cterm}s) + ensures that the left-hand side must contain beta-redexes. Indeed if we obtain the ``raw'' representation of the produced theorem, we can see the difference: @@ -1808,7 +1808,7 @@ text {* You can see how this function works in the example rewriting - the @{ML_type cterm} @{term "True \ (Foo \ Bar)"} to @{term "Foo \ Bar"}. + @{term "True \ (Foo \ Bar)"} to @{term "Foo \ Bar"}. @{ML_response_fake [display,gray] "let @@ -1861,6 +1861,14 @@ does not fail, however, because the combinator @{ML Conv.else_conv} will then try out @{ML Conv.all_conv}, which always succeeds. + The conversion combinator @{ML Conv.try_conv} constructs a conversion + which is tried out on a term, but in case of failure just does nothing. + For example + + @{ML_response_fake [display,gray] + "Conv.try_conv (Conv.rewr_conv @{thm true_conj1}) @{cterm \"True \ P\"}" + "True \ P \ True \ P"} + Apart from the function @{ML beta_conversion in Thm}, which is able to fully beta-normalise a term, the conversions so far are restricted in that they only apply to the outer-most level of a @{ML_type cterm}. In what follows we @@ -2028,8 +2036,6 @@ and simprocs; the advantage of conversions, however, is that you never have to worry about non-termination. - (FIXME: explain @{ML Conv.try_conv}) - \begin{exercise}\label{ex:addconversion} Write a tactic that does the same as the simproc in exercise \ref{ex:addsimproc}, but is based in conversions. That means replace terms @@ -2038,7 +2044,7 @@ \end{exercise} \begin{exercise}\label{ex:compare} - Compare your solutions of Exercises~\ref{addsimproc} and \ref{ex:addconversion}, + Compare your solutions of Exercises~\ref{ex:addsimproc} and \ref{ex:addconversion}, and try to determine which way of rewriting such terms is faster. For this you might have to construct quite large terms. Also see Recipe \ref{rec:timing} for information about timing. diff -r d820cb5873ea -r a29b81d4fa88 cookbook.pdf Binary file cookbook.pdf has changed