isabelle-cookbook: comparison ProgTutorial/Tactical.thy

equal deleted inserted replaced

-:14d5f0cf91dc
+:6e0f56764ff8
 the first goal. To do this can result in quite messy code. In contrast,
 the ``reverse application'' is easy to implement.
 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
+implementing a tactic analysing a goal according to its topmost
 connective. These simpler methods use tactic combinators, which we will
 explain in the next section.
 *}
 *}
 ML{*val orelse_xmp_tac = rtac @{thm disjI1} ORELSE' rtac @{thm conjI}*}
 text {*
-will first try out whether rule @{text disjI} applies and after that
+will first try out whether rule @{text disjI} applies and in case of failure
-@{text conjI}. To see this consider the proof
+will try @{text conjI}. To see this consider the proof
 *}
 lemma shows "True \<and> False" and "Foo \<or> Bar"
 apply(tactic {* orelse_xmp_tac 2 *})
 apply(tactic {* orelse_xmp_tac 1 *})
 \end{minipage} *}
 (*<*)oops(*>*)
 text {*
 Remember that we chose to implement @{ML select_tac'} so that it
-always  succeeds. This can be potentially very confusing for the user,
+always  succeeds by adding @{ML all_tac} at the end of the tactic
-for example,  in cases where the goal is the form
+list. The same can be achieved with the tactic combinator @{ML TRY}.
+For example:
+*}
+ML{*val select_tac'' = TRY o FIRST' [rtac @{thm conjI}, rtac @{thm impI},
+rtac @{thm notI}, rtac @{thm allI}]*}
+text_raw{*\label{tac:selectprimeprime}*}
+text {*
+This tactic behaves in the same way as @{ML select_tac'}: it tries out
+one of the given tactics and if none applies leaves the goal state
+unchanged. This, however, can be potentially very confusing when visible to
+the user, for example,  in cases where the goal is the form
 *}
 lemma shows "E \<Longrightarrow> F"
 apply(tactic {* select_tac' 1 *})
 txt{* \begin{minipage}{\textwidth}
 @{subgoals [display]}
 \end{minipage} *}
 (*<*)oops(*>*)
 text {*
-In this case no rule applies. The problem for the user is that there is little
+In this case no rule applies, but because of @{ML TRY} or the inclusion of @{ML all_tac}
+the tactics do not fail. The problem with this is that for the user there is little
 chance to see whether or not progress in the proof has been made. By convention
 therefore, tactics visible to the user should either change something or fail.
 To comply with this convention, we could simply delete the @{ML "K all_tac"}
 from the end of the theorem list. As a result @{ML select_tac'} would only
 tactic as long as it succeeds). The function
 @{ML REPEAT1} is similar, but runs the tactic at least once (failing if
 this is not possible).
 If you are after the ``primed'' version of @{ML repeat_xmp_tac}, then you
-need to implement it as
+can implement it as
 *}
 ML{*val repeat_xmp_tac' = REPEAT o CHANGED o select_tac'*}
 text {*
 since there are no ``primed'' versions of @{ML REPEAT} and @{ML CHANGED}.
-If you look closely at the goal state above, the tactics @{ML repeat_xmp_tac}
+If you look closely at the goal state above, then you see the tactics @{ML repeat_xmp_tac}
 and @{ML repeat_xmp_tac'} are not yet quite what we are after: the problem is
 that goals 2 and 3 are not analysed. This is because the tactic
 is applied repeatedly only to the first subgoal. To analyse also all
 resulting subgoals, you can use the tactic combinator @{ML REPEAT_ALL_NEW}.
 Suppose the tactic
 \mbox{\inferrule{@{text "t\<^isub>1 \<equiv> s\<^isub>1 \<dots> t\<^isub>n \<equiv> s\<^isub>n"}}
 {@{text "constr t\<^isub>1\<dots>t\<^isub>n \<equiv> constr s\<^isub>1\<dots>s\<^isub>n"}}}
 \end{center}
 \end{isabelle}
-with @{text "constr"} being a term-constructor, like @{const "If"} or @{const "Let"}.
+with @{text "constr"} being a constant, like @{const "If"} or @{const "Let"}.
 Every simpset contains only
 one congruence rule for each term-constructor, which however can be
 overwritten. The user can declare lemmas to be congruence rules using the
 attribute @{text "[cong]"}. In HOL, the user usually states these lemmas as
 equations, which are then internally transformed into meta-equations.
 \begin{readmore}
 For more information about the simplifier see @{ML_file "Pure/meta_simplifier.ML"}
 and @{ML_file "Pure/simplifier.ML"}. The simplifier for HOL is set up in
-@{ML_file "HOL/Tools/simpdata.ML"}. Generic splitters are implemented in
+@{ML_file "HOL/Tools/simpdata.ML"}. The generic splitter is implemented in
 @{ML_file  "Provers/splitter.ML"}.
 \end{readmore}
 \begin{readmore}
 FIXME: Find the right place: Discrimination nets are implemented
 \begin{figure}[t]
 \begin{minipage}{\textwidth}
 \begin{isabelle}*}
 ML{*fun print_ss ctxt ss =
 let
-val {simps, congs, procs, ...} = MetaSimplifier.dest_ss ss
+val {simps, congs, procs, ...} = Simplifier.dest_ss ss
 fun name_thm (nm, thm) =
 "  " ^ nm ^ ": " ^ (str_of_thm_no_vars ctxt thm)
 fun name_ctrm (nm, ctrm) =
 "  " ^ nm ^ ": " ^ (str_of_cterms ctxt ctrm)
-val s = ["Simplification rules:"] @ (map name_thm simps) @
+val s = ["Simplification rules:"] @ map name_thm simps @
-["Congruences rules:"] @ (map name_thm congs) @
+["Congruences rules:"] @ map name_thm congs @
-["Simproc patterns:"] @ (map name_ctrm procs)
+["Simproc patterns:"] @ map name_ctrm procs
 in
-s |> separate "\n"
+s |> cat_lines
-|> implode
 |> writeln
 end*}
 text_raw {*
 \end{isabelle}
 \end{minipage}
-\caption{The function @{ML MetaSimplifier.dest_ss} returns a record containing
+\caption{The function @{ML Simplifier.dest_ss} returns a record containing
 all printable information stored in a simpset. We are here only interested in the
 simplification rules, congruence rules and simprocs.\label{fig:printss}}
 \end{figure} *}
 text {*
 Simproc patterns:
 \<dots>"}
 The simplifier is often used to unfold definitions in a proof. For this the
-simplifier contains the @{ML rewrite_goals_tac}. Suppose for example the
+simplifier implements the tactic @{ML rewrite_goals_tac}.\footnote{FIXME:
+see LocalDefs infrastructure.} Suppose for example the
 definition
 *}
 definition "MyTrue \<equiv> True"
 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:
 *}
-ML %linenosgray{*fun fail_sp_aux simpset redex =
+ML %linenosgray{*fun fail_simproc simpset redex =
 let
 val ctxt = Simplifier.the_context simpset
 val _ = writeln ("The redex: " ^ (str_of_cterm ctxt redex))
 in
 NONE
 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 simpset as follows
 *}
-simproc_setup %gray fail_sp ("Suc n") = {* K fail_sp_aux *}
+simproc_setup %gray fail ("Suc n") = {* K fail_simproc *}
 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 are ignoring
 an argument about morphisms.
 We can add or delete the simproc from the current simpset by the usual
 \isacommand{declare}-statement. For example the simproc will be deleted
 with the declaration
 *}
-declare [[simproc del: fail_sp]]
+declare [[simproc del: fail]]
 text {*
 If you want to see what happens with just \emph{this} simproc, without any
-interference from other rewrite rules, you can call @{text fail_sp}
+interference from other rewrite rules, you can call @{text fail}
 as follows:
 *}
 lemma shows "Suc 0 = 1"
-apply(tactic {* simp_tac (HOL_basic_ss addsimprocs [@{simproc fail_sp}]) 1*})
+apply(tactic {* simp_tac (HOL_basic_ss addsimprocs [@{simproc fail}]) 1*})
 (*<*)oops(*>*)
 text {*
 Now the message shows up only once since the term @{term "1::nat"} is
 left unchanged.
 Setting up a simproc using the command \isacommand{simproc\_setup} 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
+up the simproc. First the function @{ML fail_simproc} needs to be modified
 to
 *}
-ML{*fun fail_sp_aux' simpset redex =
+ML{*fun fail_simproc' simpset redex =
 let
 val ctxt = Simplifier.the_context simpset
 val _ = writeln ("The redex: " ^ (Syntax.string_of_term ctxt redex))
 in
 NONE
 We can turn this function into a proper simproc using the function
 @{ML Simplifier.simproc_i}:
 *}
-ML{*val fail_sp' =
+ML{*val fail' =
 let
 val thy = @{theory}
 val pat = [@{term "Suc n"}]
 in
-Simplifier.simproc_i thy "fail_sp'" pat (K fail_sp_aux')
+Simplifier.simproc_i thy "fail_simproc'" pat (K fail_simproc')
 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.
 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_basic_ss addsimprocs [fail_sp']) 1*})
+apply(tactic {* simp_tac (HOL_basic_ss addsimprocs [fail']) 1*})
 (*<*)oops(*>*)
 text {*
-The simproc @{ML fail_sp'} prints out the sequence
+The simproc @{ML fail'} prints out the sequence
 @{text [display]
 "> Suc 0
 > Suc (Suc 0)
 > Suc 1"}
 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 =
+ML{*fun plus_one_simproc ss redex =
 case redex of
 @{term "Suc 0"} => NONE
 | _ => SOME @{thm plus_one}*}
 text {*
 and set up the simproc as follows.
 *}
-ML{*val plus_one_sp =
+ML{*val plus_one =
 let
 val thy = @{theory}
 val pat = [@{term "Suc n"}]
 in
-Simplifier.simproc_i thy "sproc +1" pat (K plus_one_sp_aux)
+Simplifier.simproc_i thy "sproc +1" pat (K plus_one_simproc)
 end*}
 text {*
 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
 *}
 lemma shows "P (Suc (Suc (Suc 0))) (Suc 0)"
-apply(tactic {* simp_tac (HOL_basic_ss addsimprocs [plus_one_sp]) 1*})
+apply(tactic {* simp_tac (HOL_basic_ss addsimprocs [plus_one]) 1*})
 txt{*
 where the simproc produces the goal state
 \begin{minipage}{\textwidth}
 @{subgoals[display]}
 *}
 (*<*)oops(*>*)
 text {*
 As usual with rewriting you have to worry about looping: you already have
-a loop with @{ML plus_one_sp}, if you apply it with the default simpset (because
+a loop with @{ML plus_one}, if you apply it with the default simpset (because
-the default simpset contains a rule which just does the opposite of @{ML plus_one_sp},
+the default simpset contains a rule which just does the opposite of @{ML plus_one},
 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.
 Next let us implement a simproc that replaces terms of the form @{term "Suc n"}
 with the number @{text n} increased by one. First we implement a function that
 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 =
+ML{*fun nat_number_simproc ss t =
 let
 val ctxt = Simplifier.the_context ss
 in
 SOME (get_thm ctxt (t, dest_suc_trm t))
 handle TERM _ => NONE
 end*}
 text {*
-This function uses the fact that @{ML dest_suc_trm} might throw an exception
+This function uses the fact that @{ML dest_suc_trm} might raise an exception
 @{ML TERM}. In this case there is nothing that can be rewritten and therefore no
 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 =
+ML{*val nat_number =
 let
 val thy = @{theory}
 val pat = [@{term "Suc n"}]
 in
-Simplifier.simproc_i thy "nat_number" pat (K nat_number_sp_aux)
+Simplifier.simproc_i thy "nat_number" pat (K nat_number_simproc)
 end*}
 text {*
 Now in the lemma
 *}
 lemma "P (Suc (Suc 2)) (Suc 99) (0::nat) (Suc 4 + Suc 0) (Suc (0 + 0))"
-apply(tactic {* simp_tac (HOL_ss addsimprocs [nat_number_sp]) 1*})
+apply(tactic {* simp_tac (HOL_ss addsimprocs [nat_number]) 1*})
 txt {*
 you obtain the more legible goal state
 \begin{minipage}{\textwidth}
 @{subgoals [display]}
 val add = @{cterm \"\<lambda>x y. x + (y::nat)\"}
 val two = @{cterm \"2::nat\"}
 val ten = @{cterm \"10::nat\"}
 val thm = Thm.beta_conversion true (Thm.capply (Thm.capply add two) ten)
 in
-#prop (rep_thm thm)
+Thm.prop_of thm
 end"
 "Const (\"==\",\<dots>) $
 (Abs (\"x\",\<dots>,Abs (\"y\",\<dots>,\<dots>)) $\<dots>$\<dots>) $
 (Const (\"HOL.plus_class.plus\",\<dots>) $ \<dots> $ \<dots>)"}
 The argument @{ML true} in @{ML Thm.beta_conversion} indicates that
-the right-hand side will be fully beta-normalised. If instead
+the right-hand side should be fully beta-normalised. If instead
 @{ML false} is given, then only a single beta-reduction is performed
 on the outer-most level. For example
 @{ML_response_fake [display,gray]
 "let
 "True \<and> (Foo \<longrightarrow> Bar) \<equiv> Foo \<longrightarrow> Bar"}
 Note, however, that the function @{ML Conv.rewr_conv} only rewrites the
 outer-most level of the @{ML_type cterm}. If the given @{ML_type cterm} does not match
 exactly the
-left-hand side of the theorem, then  @{ML Conv.rewr_conv} raises
+left-hand side of the theorem, then  @{ML Conv.rewr_conv} fails by raising
 the exception @{ML CTERM}.
 This very primitive way of rewriting can be made more powerful by
 combining several conversions into one. For this you can use conversion
 combinators. The simplest conversion combinator is @{ML then_conv},
 arguments.  Therefore 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.fun_conv} applies
 the conversion to the first argument of an application.
-The function @{ML Conv.abs_conv} applies a conversion under an abstractions.
+The function @{ML Conv.abs_conv} applies a conversion under an abstraction.
 For example:
 @{ML_response_fake [display,gray]
 "let
-val conv = K (Conv.rewr_conv @{thm true_conj1})
+val conv = Conv.rewr_conv @{thm true_conj1}
 val ctrm = @{cterm \"\<lambda>P. True \<and> P \<and> Foo\"}
 in
-Conv.abs_conv conv @{context} ctrm
+Conv.abs_conv (K conv) @{context} ctrm
 end"
 "\<lambda>P. True \<and> P \<and> Foo \<equiv> \<lambda>P. P \<and> Foo"}
 Note that this conversion needs a context as an argument. The conversion that
 goes under an application is @{ML Conv.combination_conv}. It expects two conversions
 Assume we want to apply @{ML all_true1_conv} only in the conclusion
 of the goal, and @{ML if_true1_conv} should only apply to the premises.
 Here is a tactic doing exactly that:
 *}
-ML{*fun true1_tac ctxt = CSUBGOAL (fn (goal, i) =>
+ML{*fun true1_tac ctxt =
 CONVERSION
 (Conv.params_conv ~1 (fn ctxt =>
 (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)*}
 text {*
 We call the conversions with the argument @{ML "~1"}. This is to
 analyse all parameters, premises and conclusions. If we call them with
 a non-negative number, say @{text n}, then these conversions will
 text {*
 As you can see, the premises are rewritten according to @{ML if_true1_conv}, while
 the conclusion according to @{ML all_true1_conv}.
-To sum up this section, conversions are not as powerful as the simplifier
+To sum up this section, conversions are more general than the simplifier
-and simprocs; the advantage of conversions, however, is that you never have
+or simprocs, but you have to do more work yourself. Also conversions are
-to worry about non-termination.
+often much less efficient than the simplifier. The advantage of conversions,
+however, that they provide much less room for non-termination.
 \begin{exercise}\label{ex:addconversion}
 Write a tactic that does the same as the simproc in exercise
 \ref{ex:addsimproc}, but is based in conversions. That means replace terms
 of the form @{term "t\<^isub>1 + t\<^isub>2"} by their result. You can make
 about timing.
 \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"},
+Some basic conversions are defined in  @{ML_file "Pure/thm.ML"},
 @{ML_file "Pure/drule.ML"} and @{ML_file "Pure/meta_simplifier.ML"}.
 \end{readmore}
 *}

changeset 243	6e0f56764ff8
parent 241	29d4701c5ee1
child 250	ab9e09076462