isabelle-cookbook: comparison CookBook/Tactical.thy

equal deleted inserted replaced

-:a21d7b300616
+:8db9195bb3e9
 then you can use the combinator @{ML ORELSE'} for two tactics, and @{ML
 FIRST'} (or @{ML FIRST1}) for a list of tactics. For example, the tactic
 *}
-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
 @{text conjI}. To see this consider the proof
 *}
 simproc_setup fail_sp ("Suc n") = {* K fail_sp_aux *}
 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)
 (*<*)oops(*>*)
 text {*
 This will print out the message twice: once for the left-hand side and
 once for the right-hand side. The reason is that during simplification the
 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.
+We can add or delete the simproc from the current simpset by the usual
-For example the simproc will be deleted if you type:
+\isacommand{declare}-statement. For example the simproc will be deleted
+if you type:
 *}
 declare [[simproc del: fail_sp]]
 text {*
 interference from other rewrite rules, you can call @{text fail_sp}
 as follows:
 *}
 lemma shows "Suc 0 = 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
 want this, then you have to use a slightly different method for setting
 up the simproc. First the function @{ML fail_sp_aux} needs to be modified
 It might be interesting to notice that simprocs are applied from inside
 to outside and from left to right. You can see this in the proof
 *}
 lemma shows "Suc (Suc 0) = (Suc 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:
 *}
 lemma plus_one:
 shows "Suc n \<equiv> n + 1" by simp
 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
+preconditions can be solved). To see one has relatively precise control over
-further assume we want that the simproc only rewrites terms greater than
+the rewriting with simprocs, let us further assume we want that the simproc
-@{term "Suc 0"}. For this we can write
+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
 | _ => SOME @{thm plus_one}*}
 in
 Simplifier.simproc_i thy "sproc +1" pat (K plus_one_sp_aux)
 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*})
 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}).
 Let us next implement a simproc that replaces terms of the form @{term "Suc n"}
 | dest_suc_trm t = snd (HOLogic.dest_number t)*}
 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) =
 let
 val num = HOLogic.mk_number @{typ "nat"} n
 in
 mk_meta_eq (Goal.prove ctxt [] [] goal (K (simp_tac @{simpset} 1)))
 end*}
 text {*
-From the integer value it generates the corresponding Isabelle term, called
+(FIXME: is @{text "@{simpset}"} kosher here? Otherwise the following will loop.)
-@{text num} (Line 3), and then generates the equation @{text "t = num"} (Line 4)
+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.
 *}
 SOME (get_thm ctxt (t, dest_suc_trm t))
 handle TERM _ => NONE
 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
+theorem is produced (i.e.~the function returns @{ML NONE}). To try out the simproc
-follows:
+on an example, you can set it up as follows:
 *}
 ML{*val nat_number_sp =
 let
 val thy = @{theory}

changeset 131	8db9195bb3e9
parent 130	a21d7b300616
child 132	2d9198bcb850