isabelle-cookbook: comparison CookBook/Tactical.thy

equal deleted inserted replaced

-:8db9195bb3e9
+:2d9198bcb850
 "Pure/tactic.ML"} and @{ML_file "Pure/tctical.ML"} for the code of basic
 tactics and tactic combinators; see also Chapters 3 and 4 in the old
 Isabelle Reference Manual.
 \end{readmore}
-(FIXME:  what is @{ML Goal.prove_global}?)
 Note that in the code above we use antiquotations for referencing the theorems. Many theorems
 also have ML-bindings with the same name. Therefore, we could also just have
 written @{ML "etac disjE 1"}, or in case where there are no ML-binding obtain
 the theorem dynamically using the function @{ML thm}; for example
 \mbox{@{ML  "etac (thm \"disjE\") 1"}}. Both ways however are considered bad style!
 let us modify the code of @{ML all_tac} to obtain the following
 tactic
 *}
 ML{*fun my_print_tac ctxt thm =
 let
 val _ = warning (str_of_thm ctxt thm)
 in
 Seq.single thm
 end*}
 text_raw {*
 \begin{figure}[p]
 \begin{isabelle}
 *}
 text_raw{*
 \begin{figure}
 \begin{isabelle}
 *}
 ML{*fun sp_tac {prems, params, asms, concl, context, schematics} =
 let
 val str_of_params = str_of_cterms context params
 val str_of_asms = str_of_cterms context asms
 val str_of_concl = str_of_cterm context concl
 val str_of_prems = str_of_thms context prems
 val str_of_schms = str_of_cterms context (snd schematics)
 val _ = (warning ("params: " ^ str_of_params);
 warning ("schematics: " ^ str_of_schms);
 warning ("assumptions: " ^ str_of_asms);
 warning ("conclusion: " ^ str_of_concl);
 warning ("premises: " ^ str_of_prems))
 in
 no_tac
 end*}
 text_raw{*
 \end{isabelle}
 \caption{A function that prints out the various parameters provided by the tactic
 @{ML SUBPROOF}. It uses the functions defined in Section~\ref{sec:printing} for
 extracting strings from @{ML_type cterm}s and @{ML_type thm}s.\label{fig:sptac}}
 rewrite a term according to theorem. They are useful in cases where
 a rewriting rule must be produced on ``demand'' or when rewriting by
 simplification is too unpredictable and potentially loops.
 To see how simprocs work, let us first write a simproc that just prints out
-the pattern that triggers it and otherwise does nothing. For this
+the pattern which triggers it and otherwise does nothing. For this
 you can use the function:
 *}
 ML %linenosgray{*fun fail_sp_aux simpset redex =
 let
 NONE
 end*}
 text {*
 This function takes a simpset and a redex (a @{ML_type cterm}) as
-argument. In Lines 3 and~4, we first extract the context from the given
+arguments. In Lines 3 and~4, we first extract the context from the given
 simpset and then print out a message containing the redex.  The function
 returns @{ML NONE} (standing for an optional @{ML_type thm}) since at the
 moment we are \emph{not} interested in actually rewriting anything. We want
 that the simproc is triggered by the pattern @{term "Suc n"}. This can be
 done by adding the simproc to the current simproc as follows
 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 from the current simpset by the usual
 \isacommand{declare}-statement. For example the simproc will be deleted
-if you type:
+with the declaration
 *}
 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*})
+apply(tactic {* simp_tac (HOL_basic_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 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
 end*}
 text {*
 Here the pattern is given as @{ML_type term} (instead of @{ML_type cterm}).
 The function also takes a list of patterns that can trigger the simproc.
-It might be interesting to notice that simprocs are applied from inside
+Now the simproc is set up and can be explicitly added using
-to outside and from left to right. You can see this in the proof
+{ML addsimprocs} to a simpset whenerver
+needed.
+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 @{ML fail_sp'} prints out the sequence
+The simproc @{ML fail_sp'} prints out the sequence
 @{text [display]
 "> Suc 0
 > Suc (Suc 0)
 > Suc 1"}
 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 one has relatively precise control over
+preconditions can be solved). To see that 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
 *}
 in
 Simplifier.simproc_i thy "sproc +1" pat (K plus_one_sp_aux)
 end*}
 text {*
-Now the simproc is set up xso that it is triggered by terms
+Now the simproc is set up so 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
 *}
 @{subgoals[display]}
 *}
 (*<*)oops(*>*)
 text {*
-As usual with simplification you have to be careful with looping: you already have
+As usual with simplification you have to worry about looping: you already have
-one @{ML plus_one_sp}, if you apply if with the default simpset (because
+a loop with @{ML plus_one_sp}, if you apply it with the default simpset (because
-the default simpset contains a rule which just undoes the rewriting
+the default simpset contains a rule which just does the opposite of @{ML plus_one_sp},
-@{ML plus_one_sp}).
+namely rewriting @{text [quotes] "+ 1"} to a successor). So you have to be careful
+in choosing the right simpset to which you add a simproc.
-Let us next implement a simproc that replaces terms of the form @{term "Suc n"}
+Next let us implement a simproc that replaces terms of the form @{term "Suc n"}
 with the number @{text n} increase by one. First we implement a function that
-takes a term and produces the corresponding integer value, if it can.
+takes a term and produces the corresponding integer value.
 *}
 ML{*fun dest_suc_trm ((Const (@{const_name "Suc"}, _)) $ t) = 1 + dest_suc_trm t
 | dest_suc_trm t = snd (HOLogic.dest_number t)*}
 *}
 ML %linenosgray{*fun get_thm ctxt (t, n) =
 let
 val num = HOLogic.mk_number @{typ "nat"} n
-val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (t,num))
+val goal = Logic.mk_equals (t, num)
 in
-mk_meta_eq (Goal.prove ctxt [] [] goal (K (simp_tac @{simpset} 1)))
+Goal.prove ctxt [] [] goal (K (arith_tac ctxt 1))
 end*}
 text {*
-(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),
+@{text num} (Line 3), and then generates the meta-equation @{text "t \<equiv> num"}
-which it proves by simplification in Line 6. The function @{ML mk_meta_eq}
+(Line 4), which it proves by the arithmetic tactic in Line 6.
-at the outside of the proof just transforms the equality into a meta-equality.
+For our purpose at the moment, using in the code above @{ML arith_tac} is
-Both functions can be stringed together in the function that produces the
+fine, but there is also an alternative employing the simplifier with a very
-actual theorem for the simproc.
+restricted simpset. For the kind of lemmas we want to prove, the simpset
+@{text "num_ss"} in the code will suffice.
+*}
+ML{*fun get_thm_alt ctxt (t, n) =
+let
+val num = HOLogic.mk_number @{typ "nat"} n
+val goal = Logic.mk_equals (t, num)
+val num_ss = HOL_ss addsimps [@{thm One_nat_def}, @{thm Let_def}] @
+@{thms nat_number} @ @{thms neg_simps} @ @{thms plus_nat.simps}
+in
+Goal.prove ctxt [] [] goal (K (simp_tac num_ss 1))
+end*}
+text {*
+The advantage of @{ML get_thm_alt} is that it leaves very little room for
+something to go wrong; in contrast it is much more difficult to predict
+what happens with @{ML arith_tac}, especially in more complicated
+circumstances. The disatvantage of @{ML get_thm_alt} is to find a simpset
+that is sufficiently powerful to solve every instance of the lemmas
+we like to prove. This requires careful tuning, but is often necessary in
+``production code''.\footnote{It would be of great help if there is another
+way than tracing the simplifier to obtain the lemmas that are successfully
+applied during simplification. Alas, there is none.}
+Anyway, either version can be used in the function that produces the actual
+theorem for the simproc.
 *}
 ML{*fun nat_number_sp_aux ss t =
 let
 val ctxt = Simplifier.the_context ss
 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 =
 let
 val thy = @{theory}
 val pat = [@{term "Suc n"}]
 in
 Simplifier.simproc_i thy "nat_number" pat (K nat_number_sp_aux)
 end*}
 text {*
 Now in the lemma
 *}
 @{subgoals [display]}
 *}
 (*<*)oops(*>*)
 text {*
-where the simproc rewrites all @{term "Suc"}s except in the last arguments. There it cannot
+where the simproc rewrites all @{term "Suc"}s except in the last argument. There it cannot
 rewrite anything, because it does not know how to transform the term @{term "Suc (0 + 0)"}
 into a number. To solve this problem have a look at the next exercise.
 \begin{exercise}\label{ex:addsimproc}
 Write a simproc that replaces terms of the form @{term "t\<^isub>1 + t\<^isub>2"} by their
 \end{exercise}
 (FIXME: We did not do anything with morphisms. Anything interesting
 one can say about them?)
 *}
+section {* Conversions *}
 section {* Structured Proofs *}
 text {* TBD *}

changeset 132	2d9198bcb850
parent 131	8db9195bb3e9
child 133	3e94ccc0f31e