diff -r a21d7b300616 -r 8db9195bb3e9 CookBook/Tactical.thy --- a/CookBook/Tactical.thy Sun Feb 22 13:37:47 2009 +0000 +++ b/CookBook/Tactical.thy Mon Feb 23 00:27:27 2009 +0000 @@ -798,7 +798,7 @@ *} -ML{*val orelse_xmp = (rtac @{thm disjI1} ORELSE' rtac @{thm conjI})*} +ML{*val orelse_xmp = rtac @{thm disjI1} ORELSE' rtac @{thm conjI}*} text {* will first try out whether rule @{text disjI} applies and after that @@ -1059,13 +1059,13 @@ text {* where the second argument specifies the pattern and the right-hand side contains the code of the simproc (we have to use @{ML K} since we ignoring - an argument about a morphism\footnote{FIXME: what does the morphism do?}). + an argument about morphisms\footnote{FIXME: what does the morphism do?}). After this, the simplifier is aware of the simproc and you can test whether - it fires on the lemma + it fires on the lemma: *} lemma shows "Suc 0 = 1" -apply(simp) + apply(simp) (*<*)oops(*>*) text {* @@ -1074,8 +1074,9 @@ simplifier will at some point reduce the term @{term "1::nat"} to @{term "Suc 0"}, and then the simproc ``fires'' also on that term. - We can add or delete the simproc by the usual \isacommand{declare}-statement. - For example the simproc will be deleted if you type: + We can add or delete the simproc from the current simpset by the usual + \isacommand{declare}-statement. For example the simproc will be deleted + if you type: *} declare [[simproc del: fail_sp]] @@ -1087,13 +1088,14 @@ *} lemma shows "Suc 0 = 1" -apply(tactic {* simp_tac (HOL_ss addsimprocs [@{simproc fail_sp}]) 1*}) + apply(tactic {* simp_tac (HOL_ss addsimprocs [@{simproc fail_sp}]) 1*}) (*<*)oops(*>*) text {* (FIXME: should one use HOL-basic-ss or HOL-ss?) - Now the message shows up only once since @{term "1::nat"} is left unchanged. + Now the message shows up only once since the term @{term "1::nat"} is + left unchanged. Setting up a simproc using the command \isacommand{setup\_simproc} will always add automatically the simproc to the current simpset. If you do not @@ -1133,18 +1135,18 @@ *} lemma shows "Suc (Suc 0) = (Suc 1)" -apply(tactic {* simp_tac (HOL_ss addsimprocs [fail_sp']) 1*}) + apply(tactic {* simp_tac (HOL_ss addsimprocs [fail_sp']) 1*}) (*<*)oops(*>*) text {* - since the @{ML fail_sp'}-simproc prints out the sequence + since @{ML fail_sp'} prints out the sequence @{text [display] "> Suc 0 > Suc (Suc 0) > Suc 1"} - To see how a simproc applies a theorem let us implement a simproc that + To see how a simproc applies a theorem, let us implement a simproc that rewrites terms according to the equation: *} @@ -1153,12 +1155,13 @@ text {* Simprocs expect that the given equation is a meta-equation, however the - equation can contain preconditions (the simproc then will only fire if the - preconditions can be solved). To see how rewriting can be tuned precisely, let us - further assume we want that the simproc only rewrites terms greater than - @{term "Suc 0"}. For this we can write + equation can contain preconditions (the simproc then will only fire if the + preconditions can be solved). To see one has relatively precise control over + the rewriting with simprocs, let us further assume we want that the simproc + only rewrites terms ``greater'' than @{term "Suc 0"}. For this we can write *} + ML{*fun plus_one_sp_aux ss redex = case redex of @{term "Suc 0"} => NONE @@ -1177,23 +1180,23 @@ end*} text {* - Now the have set up the simproc so that it is triggered by terms + Now the simproc is set up xso that it is triggered by terms of the form @{term "Suc n"}, but inside the simproc we only produce a theorem if the term is not @{term "Suc 0"}. The result you can see - in the following proof. + in the following proof *} lemma shows "P (Suc (Suc (Suc 0))) (Suc 0)" -apply(tactic {* simp_tac (HOL_ss addsimprocs [plus_one_sp]) 1*}) + apply(tactic {* simp_tac (HOL_ss addsimprocs [plus_one_sp]) 1*}) txt{* - the simproc produces the goal state + where the simproc produces the goal state @{subgoals[display]} *} (*<*)oops(*>*) text {* - As usual with simplification you have to be careful with loops: you already have + As usual with simplification you have to be careful with looping: you already have one @{ML plus_one_sp}, if you apply if with the default simpset (because the default simpset contains a rule which just undoes the rewriting @{ML plus_one_sp}). @@ -1210,9 +1213,9 @@ text {* It uses the library function @{ML dest_number in HOLogic} that transforms (Isabelle) terms, like @{term "0::nat"}, @{term "1::nat"}, @{term "2::nat"} and so - on, into integer values. This function raises the exception @{ML TERM} if + on, into integer values. This function raises the exception @{ML TERM}, if the term is not a number. The next function expects a pair consisting of a term - @{text t} and the corresponding integer value @{text n}. + @{text t} (containing @{term Suc}s) and the corresponding integer value @{text n}. *} ML %linenosgray{*fun get_thm ctxt (t, n) = @@ -1224,10 +1227,12 @@ end*} text {* - From the integer value it generates the corresponding Isabelle term, called - @{text num} (Line 3), and then generates the equation @{text "t = num"} (Line 4) + (FIXME: is @{text "@{simpset}"} kosher here? Otherwise the following will loop.) + + From the integer value it generates the corresponding number term, called + @{text num} (Line 3), and then generates the equation @{text "t = num"} (Line 4), which it proves by simplification in Line 6. The function @{ML mk_meta_eq} - at the outside of the proof just transforms the equality to a meta-equality. + at the outside of the proof just transforms the equality into a meta-equality. Both functions can be stringed together in the function that produces the actual theorem for the simproc. @@ -1242,12 +1247,10 @@ end*} text {* - (FIXME: is @{text "@{simpset}"} kosher here? Otherwise the following will loop.) - This function uses the fact that @{ML dest_suc_trm} might throw an exception @{ML TERM}. In this case there is nothing that can be rewritten and therefore no - theorem is produced. To try out the simproc on an example, you can set it up as - follows: + theorem is produced (i.e.~the function returns @{ML NONE}). To try out the simproc + on an example, you can set it up as follows: *} ML{*val nat_number_sp =