isabelle-cookbook: comparison CookBook/Tactical.thy

equal deleted inserted replaced

-:cb39c41548bd
+:7e0bf13bf743
 \begin{readmore}
 The function @{ML SUBPROOF} is defined in @{ML_file "Pure/subgoal.ML"} and
 also described in \isccite{sec:results}.
 \end{readmore}
-A similar but less powerful function than @{ML SUBPROOF} is @{ML SUBGOAL}.
+Similar but less powerful functions than @{ML SUBPROOF} are @{ML SUBGOAL}
-It allows you to inspect a given  subgoal. With this you can implement
+and @{ML CSUBGOAL}. They allow you to inspect a given subgoal (the former
-a tactic that applies a rule according to the topmost logic connective in the
+presents the subgoal as a @{ML_type term}, while the latter as a @{ML_type
-subgoal (to illustrate this we only analyse a few connectives). The code
+cterm}). With this you can implement a tactic that applies a rule according
-of the tactic is as follows.\label{tac:selecttac}
+to the topmost logic connective in the subgoal (to illustrate this we only
-*}
+analyse a few connectives). The code of the tactic is as
+follows.\label{tac:selecttac}
-ML %linenosgray{*fun select_tac (t,i) =
+*}
+ML %linenosgray{*fun select_tac (t, i) =
 case t of
-@{term "Trueprop"} $ t' => select_tac (t',i)
+@{term "Trueprop"} $ t' => select_tac (t', i)
-| @{term "op \<Longrightarrow>"} $ _ $ t' => select_tac (t',i)
+| @{term "op \<Longrightarrow>"} $ _ $ t' => select_tac (t', i)
 | @{term "op \<and>"} $ _ $ _ => rtac @{thm conjI} i
 | @{term "op \<longrightarrow>"} $ _ $ _ => rtac @{thm impI} i
 | @{term "Not"} $ _ => rtac @{thm notI} i
 | Const (@{const_name "All"}, _) $ _ => rtac @{thm allI} i
 | _ => all_tac*}
 text {*
 then we have to be careful to not apply the tactic to the two subgoals produced by
 the first goal. To do this can result in quite messy code. In contrast,
 the ``reverse application'' is easy to implement.
-The tactic @{ML "CSUBGOAL"} is similar to @{ML SUBGOAL} except that it takes
+Of course, this example is
-a @{ML_type cterm} instead of a @{ML_type term}.  Of course, this example is
 contrived: there are much simpler methods available in Isabelle for
 implementing a proof procedure analysing a goal according to its topmost
 connective. These simpler methods use tactic combinators, which we will
 explain in the next section.
 Most tactic combinators described in this section are defined in @{ML_file "Pure/tctical.ML"}.
 \end{readmore}
 *}
-section {* Rewriting and Simplifier Tactics *}
+section {* Simplifier Tactics *}
 text {*
 @{ML rewrite_goals_tac}
 @{ML ObjectLogic.full_atomize_tac}
 end"
 "(True \<and> Q \<equiv> Q, P \<or> True \<and> Q \<equiv> P \<or> True \<and> Q)"}
 Here the conversion of @{thm [source] true_conj1} only applies
 in the first case, but fails in the second. The whole conversion
-does not fail, however, because the combinator @{ML else_conv} will then
+does not fail, however, because the combinator @{ML Conv.else_conv} will then
 try out @{ML Conv.all_conv}, which always succeeds.
 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
 let
 val ctxt = ProofContext.init (Thm.theory_of_cterm goal)
 in
 CONVERSION
 (Conv.params_conv ~1 (fn ctxt =>
-(Conv.prems_conv ~1 (if_true1_conv ctxt)) then_conv
+(Conv.prems_conv ~1 (if_true1_conv ctxt) then_conv
-Conv.concl_conv ~1 (all_true1_conv ctxt)) ctxt) i
+Conv.concl_conv ~1 (all_true1_conv ctxt))) ctxt) i
 end)*}
 text {*
 We call the conversions with the argument @{ML "~1"}. This is to
 analyse all parameters, premises and conclusions. If we call them with
 To sum up this section, conversions are not as powerful as the simplifier
 and simprocs; the advantage of conversions, however, is that you never have
 to worry about non-termination.
+\begin{exercise}\label{ex:addconversion}
+Write a tactic that is based on conversions which does the same as the simproc in
+exercise \ref{ex:addsimproc}, that is replaces terms of the form @{term "t\<^isub>1 + t\<^isub>2"}
+by their result. You can make the same assumptions as in \ref{ex:addsimproc}.
+\end{exercise}
 \begin{readmore}
 See @{ML_file "Pure/conv.ML"} for more information about conversion combinators.
 Further conversions are defined in  @{ML_file "Pure/thm.ML"},
 @{ML_file "Pure/drule.ML"} and @{ML_file "Pure/meta_simplifier.ML"}.
 \end{readmore}
-*}
+*}
 section {* Structured Proofs *}

changeset 151	7e0bf13bf743
parent 150	cb39c41548bd
child 152	8084c353d196