--- 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 =