isabelle-cookbook: comparison CookBook/Tactical.thy

equal deleted inserted replaced

-:84d1392186d3
+:253ea99c1441
 the subgoals. So after setting up the lemma, the goal state is always of the
 form @{text "C \<Longrightarrow> (C)"}; when the proof is finished we are left with @{text
 "(C)"}. Since the goal @{term C} can potentially be an implication, there is
 a ``protector'' wrapped around it (in from of an outermost constant @{text
 "Const (\"prop\", bool \<Rightarrow> bool)"}; however this constant
-is invisible in the figure). This prevents that premises of @{text C} are
+is invisible in the figure). This wrapper prevents that premises of @{text C} are
 mis-interpreted as open subgoals. While tactics can operate on the subgoals
 (the @{text "A\<^isub>i"} above), they are expected to leave the conclusion
 @{term C} intact, with the exception of possibly instantiating schematic
 variables. If you use the predefined tactics, which we describe in the next
 section, this will always be the case.
 @{subgoals [display]}
 \end{minipage}*}
 (*<*)oops(*>*)
 text {*
-where the application of Rule @{text bspec} generates two subgoals involving the
+where the application of rule @{text bspec} generates two subgoals involving the
 meta-variable @{text "?x"}. Now, if you are not careful, tactics
 applied to the first subgoal might instantiate this meta-variable in such a
 way that the second subgoal becomes unprovable. If it is clear what the @{text "?x"}
 should be, then this situation can be avoided by introducing a more
 constraint version of the @{text bspec}-rule. Such constraints can be given by
 conclusion:  & @{term "B y x \<longrightarrow> C (z y) x"}\\
 premises:    & @{term "A x y"}
 \end{tabular}
 \end{quote}
-Note in the actual output the brown colour of the variables @{term x} and
+Notice in the actual output the brown colour of the variables @{term x} and
 @{term y}. Although they are parameters in the original goal, they are fixed inside
 the subproof. By convention these fixed variables are printed in brown colour.
 Similarly the schematic variable @{term z}. The assumption, or premise,
 @{prop "A x y"} is bound as @{ML_type cterm} to the record-variable
 @{text asms}, but also as @{ML_type thm} to @{text prems}.
 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.
-(FIXME: mention @{ML "CSUBGOAL"})
+The tactic @{ML "CSUBGOAL"} is similar to @{ML SUBGOAL} except that it takes
+a @{ML_type cterm} instead of a @{ML_type term}.  Of course, this example is
-Of course, this example is contrived: there are much simpler methods available in
+contrived: there are much simpler methods available in Isabelle for
-Isabelle for implementing a proof procedure analysing a goal according to its topmost
+implementing a proof procedure analysing a goal according to its topmost
-connective. These simpler methods use tactic combinators, which we will explain
+connective. These simpler methods use tactic combinators, which we will
-in the next section.
+explain in the next section.
 *}
 section {* Tactic Combinators *}
 text {*
 section {* Simprocs *}
 text {*
 In Isabelle you can also implement custom simplification procedures, called
-\emph{simprocs}. Simprocs can be triggered on a specified term-pattern and
+\emph{simprocs}. Simprocs can be triggered by the simplifier on a specified
-rewrite a term according to a theorem. They are useful in cases where
+term-pattern and rewrite a term according to a theorem. They are useful in
-a rewriting rule must be produced on ``demand'' or when rewriting by
+cases where a rewriting rule must be produced on ``demand'' or when
-simplification is too unpredictable and potentially loops.
+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 which triggers it and otherwise does nothing. For this
 you can use the function:
 *}
 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
+done by adding the simproc to the current simpset as follows
 *}
 simproc_setup fail_sp ("Suc n") = {* K fail_sp_aux *}
 text {*
 end*}
 text {*
 Here the redex is given as a @{ML_type term}, instead of a @{ML_type cterm}
 (therefore we printing it out using the function @{ML string_of_term in Syntax}).
-We can turn this function into a proper simproc using
+We can turn this function into a proper simproc using the function
+@{ML Simplifier.simproc_i}:
 *}
 ML{*val fail_sp' =
 let
 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.
 Now the simproc is set up and can be explicitly added using
-{ML addsimprocs} to a simpset whenerver
+@{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*})
+apply(tactic {* simp_tac (HOL_basic_ss addsimprocs [fail_sp']) 1*})
 (*<*)oops(*>*)
 text {*
 The simproc @{ML fail_sp'} prints out the sequence
 a theorem if the term is not @{term "Suc 0"}. The result you can see
 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_basic_ss addsimprocs [plus_one_sp]) 1*})
 txt{*
 where the simproc produces the goal state
 @{subgoals[display]}
 *}
 in choosing the right simpset to which you add a simproc.
 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.
 *}
 ML{*fun dest_suc_trm ((Const (@{const_name "Suc"}, _)) $ t) = 1 + dest_suc_trm t
 | dest_suc_trm t = snd (HOLogic.dest_number t)*}
 You can see how this function works with the example
 @{term "True \<and> (Foo \<longrightarrow> Bar)"}:
 @{ML_response_fake [display,gray]
 "let
-val ctrm =  @{cterm \"True \<and> (Foo \<longrightarrow> Bar)\"}
+val ctrm = @{cterm \"True \<and> (Foo \<longrightarrow> Bar)\"}
 in
 Conv.rewr_conv @{thm true_conj1} ctrm
 end"
 "True \<and> (Foo \<longrightarrow> Bar) \<equiv> Foo \<longrightarrow> Bar"}
 (conv1 then_conv conv2) ctrm
 end"
 "(\<lambda>x. x \<and> False) True \<equiv> False"}
 where we first beta-reduce the term and then rewrite according to
-@{thm [source] true_conj1}.
+@{thm [source] true_conj1}. (Recall the problem with the pretty-printer
+normalising all terms.)
 The conversion combinator @{ML else_conv} tries out the
 first one, and if it does not apply, tries the second. For example
 @{ML_response_fake [display,gray]
 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
 try out @{ML Conv.all_conv}, which always succeeds.
-Apart from the function @{ML beta_conversion in Thm}, which able to fully
+Apart from the function @{ML beta_conversion in Thm}, which is able to fully
-beta-normalise a term, the restriction of conversions so far is that they
+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
 will lift this restriction. The combinator @{ML Conv.arg_conv} will apply
-the conversion on the first argument of an application, that is the term
+the conversion to the first argument of an application, that is the term
 must be of the form @{ML "t1 $ t2" for t1 t2} and the conversion is applied
 to @{text t2}.  For example
 @{ML_response_fake [display,gray]
 "let
 Conv.arg_conv conv ctrm
 end"
 "P \<or> (True \<and> Q) \<equiv> P \<or> Q"}
 The reason for this behaviour is that @{text "(op \<or>)"} expects two
-arguments.  So the term must be of the form @{text "Const \<dots> $ t1 $ t2"}. The
+arguments.  So the term must be of the form @{text "(Const \<dots> $ t1) $ t2"}. The
 conversion is then applied to @{text "t2"} which in the example above
 stands for @{term "True \<and> Q"}.
 The function @{ML Conv.abs_conv} applies a conversion under an abstractions.
 For example:
 | _ => Conv.all_conv ctrm*}
 text {*
 This functions descends under applications (Line 6 and 7) and abstractions
 (Line 8); and ``fires'' if the outer-most constant is an @{text "True \<and> \<dots>"}
-(Lines 3-5); otherwise it leaves the term unchanged (Line 9). To see this
+(Lines 3-5); otherwise it leaves the term unchanged (Line 9). In Line 2
-conversion in action, consider the following example.
+we need to transform the @{ML_type cterm} into a @{ML_type term} in order
+to be able to pattern-match the term. To see this
+conversion in action, consider the following example
 @{ML_response_fake [display,gray]
 "let
 val ctxt = @{context}
 val ctrm = @{cterm \"distinct [1, x] \<longrightarrow> True \<and> 1 \<noteq> x\"}
 in
 all_true1_conv ctxt ctrm
 end"
 "distinct [1, x] \<longrightarrow> True \<and> 1 \<noteq> x \<equiv> distinct [1, x] \<longrightarrow> 1 \<noteq> x"}
-To see how much control you have about rewriting via conversions, let us
+where the conversion is applied ``deep'' inside the term.
+To see how much control you have about rewriting by using conversions, let us
 make the task a bit more complicated by rewriting according to the rule
-@{text true_conj1}, but only in the first arguments of @{term If}s. The
+@{text true_conj1}, but only in the first arguments of @{term If}s. Then
 the conversion should be as follows.
 *}
 ML{*fun if_true1_conv ctxt ctrm =
 case Thm.term_of ctrm of
 (if_true1_conv ctxt) (if_true1_conv ctxt) ctrm
 | Abs _ => Conv.abs_conv (fn (_, ctxt) => if_true1_conv ctxt) ctxt ctrm
 | _ => Conv.all_conv ctrm *}
 text {*
-Here is an application of this conversion:
+Here is an example for this conversion:
 @{ML_response_fake [display,gray]
 "let
 val ctxt = @{context}
 val ctrm =
 *}
 text {*
 So far we only applied conversions to @{ML_type cterm}s. Conversions can, however,
 also work on theorems using the function @{ML "Conv.fconv_rule"}. As an example,
-consider @{ML all_true1_conv} and the lemma:
+consider the conversion @{ML all_true1_conv} and the lemma:
 *}
 lemma foo_test: "P \<or> (True \<and> \<not>P)" by simp
 text {*
 Q"}); the function @{ML Conv.prems_conv} for applying the conversion to all
 premises of a goal, and @{ML Conv.concl_conv} for applying the conversion to
 the conclusion of a goal.
 Assume we want to apply @{ML all_true1_conv} only in the conclusion
-of the goal, and @{ML if_true1_conv} should only be applied in the premises.
+of the goal, and @{ML if_true1_conv} should only be applied to the premises.
 Here is a tactic doing exactly that:
 *}
 ML{*val true1_tac = CSUBGOAL (fn (goal, i) =>
 let
 "if True \<and> P then P else True \<and> False \<Longrightarrow>
 (if True \<and> Q then True \<and> Q else P) \<longrightarrow> True \<and> (True \<and> Q)"
 apply(tactic {* true1_tac 1 *})
 txt {* where the tactic yields the goal state
-\begin{minipage}{\textwidth}
+@{subgoals [display]}*}
-@{subgoals [display]}
-\end{minipage} *}
 (*<*)oops(*>*)
 text {*
 As you can see, the premises are rewritten according to @{ML if_true1_conv}, while
 the conclusion according to @{ML all_true1_conv}.

changeset 149	253ea99c1441
parent 148	84d1392186d3
child 150	cb39c41548bd
child 169	d3fcc1a0272c