isabelle-cookbook: comparison ProgTutorial/Tactical.thy

equal deleted inserted replaced

-:aec7073d4645
+:daf404920ab9
 apply(assumption)
 apply(rule disjI1)
 apply(assumption)
 done
 text {*
 This proof translates to the following ML-code.
 @{ML_response_fake [display,gray]
 "let
 val ctxt = @{context}
 val goal = @{prop \"P \<or> Q \<Longrightarrow> Q \<or> P\"}
 in
 Goal.prove ctxt [\"P\", \"Q\"] [] goal
-(fn _ =>  etac @{thm disjE} 1
+(fn _ =>  eresolve_tac @{context} [@{thm disjE}] 1
-THEN rtac @{thm disjI2} 1
+THEN resolve_tac @{context} [@{thm disjI2}] 1
-THEN atac 1
+THEN assume_tac @{context} 1
-THEN rtac @{thm disjI1} 1
+THEN resolve_tac @{context} [@{thm disjI1}] 1
-THEN atac 1)
+THEN assume_tac @{context} 1)
 end" "?P \<or> ?Q \<Longrightarrow> ?Q \<or> ?P"}
 To start the proof, the function @{ML_ind prove in Goal} sets up a goal
 state for proving the goal @{prop "P \<or> Q \<Longrightarrow> Q \<or> P"}. We can give this
 function some assumptions in the third argument (there are no assumption in
 the proof at hand). The second argument stands for a list of variables
 (given as strings). This list contains the variables that will be turned
 into schematic variables once the goal is proved (in our case @{text P} and
 @{text Q}). The last argument is the tactic that proves the goal. This
 tactic can make use of the local assumptions (there are none in this
-example). The tactics @{ML_ind etac in Tactic}, @{ML_ind rtac in Tactic} and
+example). The tactics @{ML_ind eresolve_tac in Tactic}, @{ML_ind resolve_tac in Tactic} and
-@{ML_ind atac in Tactic} in the code above correspond roughly to @{text
+@{ML_ind assume_tac in Tactic} in the code above correspond roughly to @{text
 erule}, @{text rule} and @{text assumption}, respectively. The combinator
 @{ML THEN} strings the tactics together.
-TBD: Write something about @{ML_ind prove_multi in Goal}.
+TBD: Write something about @{ML_ind prove_common in Goal}.
 \begin{readmore}
 To learn more about the function @{ML_ind prove in Goal} see
 \isccite{sec:results} and the file @{ML_file "Pure/goal.ML"}.  See @{ML_file
 "Pure/tactic.ML"} and @{ML_file "Pure/tactical.ML"} for the code of basic
 the command \isacommand{apply}@{text "(tactic \<verbopen> \<dots> \<verbclose>)"}.
 Consider the following sequence of tactics
 *}
-ML %grayML{*val foo_tac =
+ML %grayML{*fun foo_tac ctxt =
-(etac @{thm disjE} 1
+(eresolve_tac ctxt [@{thm disjE}] 1
-THEN rtac @{thm disjI2} 1
+THEN resolve_tac  ctxt [@{thm disjI2}] 1
-THEN atac 1
+THEN assume_tac  ctxt 1
-THEN rtac @{thm disjI1} 1
+THEN resolve_tac ctxt [@{thm disjI1}] 1
-THEN atac 1)*}
+THEN assume_tac  ctxt 1)*}
 text {* and the Isabelle proof: *}
 lemma
 shows "P \<or> Q \<Longrightarrow> Q \<or> P"
-apply(tactic {* foo_tac *})
+apply(tactic {* foo_tac @{context} *})
 done
 text {*
 By using @{text "tactic \<verbopen> \<dots> \<verbclose>"} you can call from the
 user-level of Isabelle the tactic @{ML foo_tac} or
 tactic (@{text "1"} stands for the first, or top-most, subgoal). This hard-coding
 of goals is sometimes wanted, but usually it is not. To avoid the explicit numbering,
 you can write
 *}
-ML %grayML{*val foo_tac' =
+ML %grayML{*fun foo_tac' ctxt =
-(etac @{thm disjE}
+(eresolve_tac ctxt [@{thm disjE}]
-THEN' rtac @{thm disjI2}
+THEN' resolve_tac ctxt [@{thm disjI2}]
-THEN' atac
+THEN' assume_tac ctxt
-THEN' rtac @{thm disjI1}
+THEN' resolve_tac ctxt [@{thm disjI1}]
-THEN' atac)*}text_raw{*\label{tac:footacprime}*}
+THEN' assume_tac ctxt)*}text_raw{*\label{tac:footacprime}*}
 text {*
 where @{ML_ind THEN' in Tactical} is used instead of @{ML THEN in
 Tactical}. (For most combinators that combine tactics---@{ML THEN} is only
 one such combinator---a ``primed'' version exists.)  With @{ML foo_tac'} you
 *}
 lemma
 shows "P1 \<or> Q1 \<Longrightarrow> Q1 \<or> P1"
 and   "P2 \<or> Q2 \<Longrightarrow> Q2 \<or> P2"
-apply(tactic {* foo_tac' 2 *})
+apply(tactic {* foo_tac' @{context} 2 *})
-apply(tactic {* foo_tac' 1 *})
+apply(tactic {* foo_tac' @{context} 1 *})
 done
 text {*
 This kind of addressing is more difficult to achieve when the goal is
 hard-coded inside the tactic.
 @{ML foo_tac'}: either using the first assumption or the second.
 *}
 lemma
 shows "\<lbrakk>P \<or> Q; P \<or> Q\<rbrakk> \<Longrightarrow> Q \<or> P"
-apply(tactic {* foo_tac' 1 *})
+apply(tactic {* foo_tac' @{context} 1 *})
 back
 done
 text {*
 definition
 EQ_TRUE
 where
 "EQ_TRUE X \<equiv> (X = True)"
-schematic_lemma test:
+schematic_goal test:
 shows "EQ_TRUE ?X"
 unfolding EQ_TRUE_def
 by (rule refl)
 text {*
 sometimes useful during the development of tactics.
 *}
 lemma
 shows "False" and "Goldbach_conjecture"
-apply(tactic {* Skip_Proof.cheat_tac 1 *})
+apply(tactic {* Skip_Proof.cheat_tac @{context} 1 *})
 txt{*\begin{minipage}{\textwidth}
 @{subgoals [display]}
 \end{minipage}*}
 (*<*)oops(*>*)
 text {*
-Another simple tactic is the function @{ML_ind atac in Tactic}, which, as shown
+Another simple tactic is the function @{ML_ind assume_tac in Tactic}, which, as shown
 earlier, corresponds to the assumption method.
 *}
 lemma
 shows "P \<Longrightarrow> P"
-apply(tactic {* atac 1 *})
+apply(tactic {* assume_tac @{context} 1 *})
 txt{*\begin{minipage}{\textwidth}
 @{subgoals [display]}
 \end{minipage}*}
 (*<*)oops(*>*)
 text {*
-Similarly, @{ML_ind rtac in Tactic}, @{ML_ind dtac in Tactic}, @{ML_ind etac
+Similarly, @{ML_ind resolve_tac in Tactic}, @{ML_ind dresolve_tac in Tactic}, @{ML_ind eresolve_tac
-in Tactic} and @{ML_ind ftac in Tactic} correspond (roughly) to @{text
+in Tactic} and @{ML_ind forward_tac in Tactic} correspond (roughly) to @{text
 rule}, @{text drule}, @{text erule} and @{text frule}, respectively. Each of
 them takes a theorem as argument and attempts to apply it to a goal. Below
 are three self-explanatory examples.
 *}
 lemma
 shows "P \<and> Q"
-apply(tactic {* rtac @{thm conjI} 1 *})
+apply(tactic {* resolve_tac @{context} [@{thm conjI}] 1 *})
 txt{*\begin{minipage}{\textwidth}
 @{subgoals [display]}
 \end{minipage}*}
 (*<*)oops(*>*)
 lemma
 shows "P \<and> Q \<Longrightarrow> False"
-apply(tactic {* etac @{thm conjE} 1 *})
+apply(tactic {* eresolve_tac @{context} [@{thm conjE}] 1 *})
 txt{*\begin{minipage}{\textwidth}
 @{subgoals [display]}
 \end{minipage}*}
 (*<*)oops(*>*)
 lemma
 shows "False \<and> True \<Longrightarrow> False"
-apply(tactic {* dtac @{thm conjunct2} 1 *})
+apply(tactic {* dresolve_tac @{context} [@{thm conjunct2}] 1 *})
 txt{*\begin{minipage}{\textwidth}
 @{subgoals [display]}
 \end{minipage}*}
 (*<*)oops(*>*)
 text {*
-The function @{ML_ind resolve_tac in Tactic} is similar to @{ML rtac}, except that it
+The function @{ML_ind resolve_tac in Tactic}
 expects a list of theorems as argument. From this list it will apply the
 first applicable theorem (later theorems that are also applicable can be
 explored via the lazy sequences mechanism). Given the code
 *}
-ML %grayML{*val resolve_xmp_tac = resolve_tac [@{thm impI}, @{thm conjI}]*}
+ML %grayML{*fun resolve_xmp_tac ctxt = resolve_tac ctxt [@{thm impI}, @{thm conjI}]*}
 text {*
 an example for @{ML resolve_tac} is the following proof where first an outermost
 implication is analysed and then an outermost conjunction.
 *}
 lemma
 shows "C \<longrightarrow> (A \<and> B)"
 and   "(A \<longrightarrow> B) \<and> C"
-apply(tactic {* resolve_xmp_tac 1 *})
+apply(tactic {* resolve_xmp_tac @{context} 1 *})
-apply(tactic {* resolve_xmp_tac 2 *})
+apply(tactic {* resolve_xmp_tac @{context} 2 *})
 txt{*\begin{minipage}{\textwidth}
 @{subgoals [display]}
 \end{minipage}*}
 (*<*)oops(*>*)
 text {*
 Similar versions taking a list of theorems exist for the tactics
-@{ML dtac} (@{ML_ind dresolve_tac in Tactic}), @{ML etac}
+@{ML_ind dresolve_tac in Tactic},
-(@{ML_ind eresolve_tac in Tactic}) and so on.
+@{ML_ind eresolve_tac in Tactic} and so on.
 Another simple tactic is @{ML_ind cut_facts_tac in Tactic}. It inserts a
 list of theorems into the assumptions of the current goal state. Below we
 will insert the definitions for the constants @{term True} and @{term
 False}. So
 \begin{figure}[t]
 \begin{minipage}{\textwidth}
 \begin{isabelle}
 *}
-ML %grayML{*fun foc_tac {prems, params, asms, concl, context, schematics} =
+ML %grayML{*fun foc_tac {context, params, prems, asms, concl, schematics} =
 let
 fun assgn1 f1 f2 xs =
 let
 val out = map (fn (x, y) => Pretty.enum ":=" "" "" [f1 x, f2 y]) xs
 in
 Pretty.list "" "" out
 end
-fun assgn2 f xs = assgn1 f f xs
+fun assgn2 f xs = assgn1 (fn (n,T) => pretty_term context (Var (n,T))) f  xs
 val pps = map (fn (s, pp) => Pretty.block [Pretty.str s, pp])
 [("params: ", assgn1 Pretty.str (pretty_cterm context) params),
 ("assumptions: ", pretty_cterms context asms),
 ("conclusion: ", pretty_cterm context concl),
 in Section~\ref{sec:printing} for extracting strings from @{ML_type cterm}s
 and @{ML_type thm}s.\label{fig:sptac}}
 \end{figure}
 *}
-schematic_lemma
+schematic_goal
 shows "\<And>x y. A x y \<Longrightarrow> B y x \<longrightarrow> C (?z y) x"
 apply(tactic {* Subgoal.FOCUS foc_tac @{context} 1 *})
 txt {*
 The tactic produces the following printout:
 is that the former expects that the goal is solved completely, which the
 latter does not. Another is that @{ML SUBPROOF} cannot instantiate any schematic
 variables.
 Observe that inside @{ML FOCUS in Subgoal} and @{ML SUBPROOF}, we are in a goal
-state where there is only a conclusion. This means the tactics @{ML dtac} and
+state where there is only a conclusion. This means the tactics @{ML dresolve_tac} and
 the like are of no use for manipulating the goal state. The assumptions inside
 @{ML FOCUS in Subgoal} and @{ML SUBPROOF} are given as cterms and theorems in
 the arguments @{text "asms"} and @{text "prems"}, respectively. This
 means we can apply them using the usual assumption tactics. With this you can
-for example easily implement a tactic that behaves almost like @{ML atac}:
+for example easily implement a tactic that behaves almost like @{ML assume_tac}:
 *}
-ML %grayML{*val atac' = Subgoal.FOCUS (fn {prems, ...} => resolve_tac prems 1)*}
+ML %grayML{*val atac' = Subgoal.FOCUS (fn {prems, context, ...} => resolve_tac context prems 1)*}
 text {*
 If you apply @{ML atac'} to the next lemma
 *}
 described next are more appropriate.
 \begin{readmore}
 The functions @{ML FOCUS in Subgoal} and @{ML SUBPROOF} are defined in
-@{ML_file "Pure/subgoal.ML"} and also described in
+@{ML_file "Pure/Isar/subgoal.ML"} and also described in
 \isccite{sec:results}.
 \end{readmore}
 Similar but less powerful functions than @{ML FOCUS in Subgoal},
 respectively @{ML SUBPROOF}, are @{ML_ind SUBGOAL in Tactical} and @{ML_ind
 cterm}). With them you can implement a tactic that applies a rule according
 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.
 *}
-ML %linenosgray{*fun select_tac (t, i) =
+ML %linenosgray{*fun select_tac ctxt (t, i) =
 case t of
-@{term "Trueprop"} $ t' => select_tac (t', i)
+@{term "Trueprop"} $ t' => select_tac ctxt (t', i)
-| @{term "op \<Longrightarrow>"} $ _ $ t' => select_tac (t', i)
+| @{term "(\<Longrightarrow>)"} $ _ $ t' => select_tac ctxt (t', i)
-| @{term "op \<and>"} $ _ $ _ => rtac @{thm conjI} i
+| @{term "(\<and>)"} $ _ $ _ => resolve_tac ctxt [@{thm conjI}] i
-| @{term "op \<longrightarrow>"} $ _ $ _ => rtac @{thm impI} i
+| @{term "(\<longrightarrow>)"} $ _ $ _ => resolve_tac ctxt [@{thm impI}] i
-| @{term "Not"} $ _ => rtac @{thm notI} i
+| @{term "Not"} $ _ => resolve_tac ctxt [@{thm notI}] i
-| Const (@{const_name "All"}, _) $ _ => rtac @{thm allI} i
+| Const (@{const_name "All"}, _) $ _ => resolve_tac ctxt [@{thm allI}] i
 | _ => all_tac*}text_raw{*\label{tac:selecttac}*}
 text {*
 The input of the function is a term representing the subgoal and a number
 specifying the subgoal of interest. In Line 3 you need to descend under the
 *}
 lemma
 shows "A \<and> B" and "A \<longrightarrow> B \<longrightarrow>C" and "\<forall>x. D x" and "E \<Longrightarrow> F"
-apply(tactic {* SUBGOAL select_tac 4 *})
+apply(tactic {* SUBGOAL (select_tac @{context}) 4 *})
-apply(tactic {* SUBGOAL select_tac 3 *})
+apply(tactic {* SUBGOAL (select_tac @{context}) 3 *})
-apply(tactic {* SUBGOAL select_tac 2 *})
+apply(tactic {* SUBGOAL (select_tac @{context}) 2 *})
-apply(tactic {* SUBGOAL select_tac 1 *})
+apply(tactic {* SUBGOAL (select_tac @{context}) 1 *})
 txt{* \begin{minipage}{\textwidth}
 @{subgoals [display]}
 \end{minipage} *}
 (*<*)oops(*>*)
 produced by the rule. If we had applied it in the other order
 *}
 lemma
 shows "A \<and> B" and "A \<longrightarrow> B \<longrightarrow>C" and "\<forall>x. D x" and "E \<Longrightarrow> F"
-apply(tactic {* SUBGOAL select_tac 1 *})
+apply(tactic {* SUBGOAL (select_tac @{context}) 1 *})
-apply(tactic {* SUBGOAL select_tac 3 *})
+apply(tactic {* SUBGOAL (select_tac @{context}) 3 *})
-apply(tactic {* SUBGOAL select_tac 4 *})
+apply(tactic {* SUBGOAL (select_tac @{context}) 4 *})
-apply(tactic {* SUBGOAL select_tac 5 *})
+apply(tactic {* SUBGOAL (select_tac @{context}) 5 *})
 (*<*)oops(*>*)
 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,
 \begin{readmore}
 The functions @{ML SUBGOAL} and @{ML CSUBGOAL} are defined in @{ML_file "Pure/tactical.ML"}.
 \end{readmore}
-Since @{ML_ind rtac in Tactic} and the like use higher-order unification, an
+Since @{ML_ind resolve_tac in Tactic} and the like use higher-order unification, an
 automatic proof procedure based on them might become too fragile, if it just
 applies theorems as shown above. The reason is that a number of theorems
 introduce schematic variables into the goal state. Consider for example the
 proof
 *}
 lemma
 shows "\<forall>x \<in> A. P x \<Longrightarrow> Q x"
-apply(tactic {* dtac @{thm bspec} 1 *})
+apply(tactic {* dresolve_tac @{context} [@{thm bspec}] 1 *})
 txt{*\begin{minipage}{\textwidth}
 @{subgoals [display]}
 \end{minipage}*}
 (*<*)oops(*>*)
 *}
 lemma
 fixes x y u w::"'a"
 shows "t x y = s u w"
-apply(tactic {* Cong_Tac.cong_tac @{thm cong} 1 *})
+apply(tactic {* Cong_Tac.cong_tac @{context} @{thm cong} 1 *})
 txt{*\begin{minipage}{\textwidth}
 @{subgoals [display]}
 \end{minipage}*}
 (*<*)oops(*>*)
 that can be used to instantiate the theorem. The instantiation
 can be done with the function @{ML_ind instantiate_normalize in Drule}. To automate
 this we implement the following function.
 *}
-ML %linenosgray{*fun fo_rtac thm = Subgoal.FOCUS (fn {concl, ...} =>
+ML %linenosgray{*fun fo_rtac thm = Subgoal.FOCUS (fn {context, concl, ...} =>
 let
-val concl_pat = Drule.strip_imp_concl (cprop_of thm)
+val concl_pat = Drule.strip_imp_concl (Thm.cprop_of thm)
 val insts = Thm.first_order_match (concl_pat, concl)
 in
-rtac (Drule.instantiate_normalize insts thm) 1
+resolve_tac context [(Drule.instantiate_normalize insts thm)] 1
 end)*}
 text {*
 Note that we use @{ML FOCUS in Subgoal} because it gives us directly access
 to the conclusion of the goal state, but also because this function
 which just strings together two tactics in a sequence. For example:
 *}
 lemma
 shows "(Foo \<and> Bar) \<and> False"
-apply(tactic {* rtac @{thm conjI} 1 THEN rtac @{thm conjI} 1 *})
+apply(tactic {* resolve_tac @{context} [@{thm conjI}] 1 THEN resolve_tac @{context} [@{thm conjI}] 1 *})
 txt {* \begin{minipage}{\textwidth}
 @{subgoals [display]}
 \end{minipage} *}
 (*<*)oops(*>*)
 For example:
 *}
 lemma
 shows "(Foo \<and> Bar) \<and> False"
-apply(tactic {* (rtac @{thm conjI} THEN' rtac @{thm conjI}) 1 *})
+apply(tactic {* (resolve_tac @{context} [@{thm conjI}] THEN' resolve_tac @{context} [@{thm conjI}]) 1 *})
 txt {* \begin{minipage}{\textwidth}
 @{subgoals [display]}
 \end{minipage} *}
 (*<*)oops(*>*)
 and then apply a tactic to each of the two subgoals.
 *}
 lemma
 shows "A \<Longrightarrow> True \<and> A"
-apply(tactic {* (rtac @{thm conjI}
+apply(tactic {* (resolve_tac @{context} [@{thm conjI}]
-THEN' RANGE [rtac @{thm TrueI}, atac]) 1 *})
+THEN' RANGE [resolve_tac @{context} [@{thm TrueI}], assume_tac @{context}]) 1 *})
 txt {* \begin{minipage}{\textwidth}
 @{subgoals [display]}
 \end{minipage} *}
 (*<*)oops(*>*)
 one specified subgoal, you can use the combinator @{ML_ind EVERY' in
 Tactical}. For example the function @{ML foo_tac'} from
 page~\pageref{tac:footacprime} can also be written as:
 *}
-ML %grayML{*val foo_tac'' = EVERY' [etac @{thm disjE}, rtac @{thm disjI2},
+ML %grayML{*fun foo_tac'' ctxt =
-atac, rtac @{thm disjI1}, atac]*}
+EVERY' [eresolve_tac ctxt [@{thm disjE}], resolve_tac ctxt [@{thm disjI2}],
+assume_tac ctxt, resolve_tac ctxt [@{thm disjI1}], assume_tac ctxt]*}
 text {*
 There is even another way of implementing this tactic: in automatic proof
 procedures (in contrast to tactics that might be called by the user) there
 are often long lists of tactics that are applied to the first
-subgoal. Instead of writing the code above and then calling @{ML "foo_tac'' 1"},
+subgoal. Instead of writing the code above and then calling @{ML "foo_tac'' @{context} 1"},
 you can also just write
 *}
-ML %grayML{*val foo_tac1 = EVERY1 [etac @{thm disjE}, rtac @{thm disjI2},
+ML %grayML{*fun foo_tac1 ctxt =
-atac, rtac @{thm disjI1}, atac]*}
+EVERY1 [eresolve_tac ctxt [@{thm disjE}], resolve_tac ctxt [@{thm disjI2}],
+assume_tac ctxt, resolve_tac ctxt [@{thm disjI1}], assume_tac ctxt]*}
 text {*
 and call @{ML foo_tac1}.
 With the combinators @{ML THEN'}, @{ML EVERY'} and @{ML_ind  EVERY1 in Tactical} it must be
 then you can use the combinator @{ML_ind  ORELSE' in Tactical} for two tactics, and @{ML_ind
 FIRST' in Tactical} (or @{ML_ind  FIRST1 in Tactical}) for a list of tactics. For example, the tactic
 *}
-ML %grayML{*val orelse_xmp_tac = rtac @{thm disjI1} ORELSE' rtac @{thm conjI}*}
+ML %grayML{*fun orelse_xmp_tac ctxt =
+resolve_tac ctxt [@{thm disjI1}] ORELSE' resolve_tac ctxt [@{thm conjI}]*}
 text {*
 will first try out whether theorem @{text disjI} applies and in case of failure
 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 @{context} 2 *})
-apply(tactic {* orelse_xmp_tac 1 *})
+apply(tactic {* orelse_xmp_tac @{context} 1 *})
 txt {* which results in the goal state
 \begin{isabelle}
 @{subgoals [display]}
 \end{isabelle}
 *}
 text {*
 Using @{ML FIRST'} we can simplify our @{ML select_tac} from Page~\pageref{tac:selecttac}
 as follows:
 *}
-ML %grayML{*val select_tac' = FIRST' [rtac @{thm conjI}, rtac @{thm impI},
+ML %grayML{*fun select_tac' ctxt =
-rtac @{thm notI}, rtac @{thm allI}, K all_tac]*}text_raw{*\label{tac:selectprime}*}
+FIRST' [resolve_tac ctxt [@{thm conjI}], resolve_tac ctxt [@{thm impI}],
+resolve_tac ctxt [@{thm notI}], resolve_tac ctxt [@{thm allI}], K all_tac]*}text_raw{*\label{tac:selectprime}*}
 text {*
 Since we like to mimic the behaviour of @{ML select_tac} as closely as possible,
 we must include @{ML all_tac} at the end of the list, otherwise the tactic will
 fail if no theorem applies (we also have to wrap @{ML all_tac} using the
 test the tactic on the same goals:
 *}
 lemma
 shows "A \<and> B" and "A \<longrightarrow> B \<longrightarrow>C" and "\<forall>x. D x" and "E \<Longrightarrow> F"
-apply(tactic {* select_tac' 4 *})
+apply(tactic {* select_tac' @{context} 4 *})
-apply(tactic {* select_tac' 3 *})
+apply(tactic {* select_tac' @{context} 3 *})
-apply(tactic {* select_tac' 2 *})
+apply(tactic {* select_tac' @{context} 2 *})
-apply(tactic {* select_tac' 1 *})
+apply(tactic {* select_tac' @{context} 1 *})
 txt{* \begin{minipage}{\textwidth}
 @{subgoals [display]}
 \end{minipage} *}
 (*<*)oops(*>*)
 @{ML_ind  ALLGOALS in Tactical} that simplifies this. Using this combinator you can simply
 write: *}
 lemma
 shows "A \<and> B" and "A \<longrightarrow> B \<longrightarrow>C" and "\<forall>x. D x" and "E \<Longrightarrow> F"
-apply(tactic {* ALLGOALS select_tac' *})
+apply(tactic {* ALLGOALS (select_tac' @{context}) *})
 txt{* \begin{minipage}{\textwidth}
 @{subgoals [display]}
 \end{minipage} *}
 (*<*)oops(*>*)
 always  succeeds by fact of having @{ML all_tac} at the end of the tactic
 list. The same can be achieved with the tactic combinator @{ML_ind  TRY in Tactical}.
 For example:
 *}
-ML %grayML{*val select_tac'' = TRY o FIRST' [rtac @{thm conjI}, rtac @{thm impI},
+ML %grayML{*fun select_tac'' ctxt =
-rtac @{thm notI}, rtac @{thm allI}]*}
+TRY o FIRST' [resolve_tac ctxt [@{thm conjI}], resolve_tac ctxt [@{thm impI}],
+resolve_tac ctxt [@{thm notI}], resolve_tac ctxt [@{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
 *}
 lemma
 shows "E \<Longrightarrow> F"
-apply(tactic {* select_tac' 1 *})
+apply(tactic {* select_tac' @{context} 1 *})
 txt{* \begin{minipage}{\textwidth}
 @{subgoals [display]}
 \end{minipage} *}
 (*<*)oops(*>*)
 now
 *}
 lemma
 shows "E \<Longrightarrow> F"
-apply(tactic {* CHANGED (select_tac' 1) *})(*<*)?(*>*)
+apply(tactic {* CHANGED (select_tac' @{context} 1) *})(*<*)?(*>*)
 txt{* gives the error message:
 \begin{isabelle}
 @{text "*** empty result sequence -- proof command failed"}\\
 @{text "*** At command \"apply\"."}
 \end{isabelle}
 connective, but also to the ones immediately ``underneath'', i.e.~analyse the goal
 completely. For this you can use the tactic combinator @{ML_ind REPEAT in Tactical}. As an example
 suppose the following tactic
 *}
-ML %grayML{*val repeat_xmp_tac = REPEAT (CHANGED (select_tac' 1)) *}
+ML %grayML{*fun repeat_xmp_tac ctxt = REPEAT (CHANGED (select_tac' ctxt 1)) *}
 text {* which applied to the proof *}
 lemma
 shows "((\<not>A) \<and> (\<forall>x. B x)) \<and> (C \<longrightarrow> D)"
-apply(tactic {* repeat_xmp_tac *})
+apply(tactic {* repeat_xmp_tac @{context} *})
 txt{* produces
 \begin{isabelle}
 @{subgoals [display]}
 \end{isabelle} *}
 (*<*)oops(*>*)
 If you are after the ``primed'' version of @{ML repeat_xmp_tac}, then you
 can implement it as
 *}
-ML %grayML{*val repeat_xmp_tac' = REPEAT o CHANGED o select_tac'*}
+ML %grayML{*fun repeat_xmp_tac' ctxt = REPEAT o CHANGED o select_tac' ctxt*}
 text {*
 since there are no ``primed'' versions of @{ML REPEAT} and @{ML CHANGED}.
 If you look closely at the goal state above, then you see the tactics @{ML repeat_xmp_tac}
 is applied repeatedly only to the first subgoal. To analyse also all
 resulting subgoals, you can use the tactic combinator @{ML_ind  REPEAT_ALL_NEW in Tactical}.
 Supposing the tactic
 *}
-ML %grayML{*val repeat_all_new_xmp_tac = REPEAT_ALL_NEW (CHANGED o select_tac')*}
+ML %grayML{*fun repeat_all_new_xmp_tac ctxt = REPEAT_ALL_NEW (CHANGED o select_tac' ctxt)*}
 text {*
 you can see that the following goal
 *}
 lemma
 shows "((\<not>A) \<and> (\<forall>x. B x)) \<and> (C \<longrightarrow> D)"
-apply(tactic {* repeat_all_new_xmp_tac 1 *})
+apply(tactic {* repeat_all_new_xmp_tac @{context} 1 *})
 txt{* \begin{minipage}{\textwidth}
 @{subgoals [display]}
 \end{minipage} *}
 (*<*)oops(*>*)
 *}
 lemma
 shows "\<lbrakk>P1 \<or> Q1; P2 \<or> Q2\<rbrakk> \<Longrightarrow> R"
-apply(tactic {* etac @{thm disjE} 1 *})
+apply(tactic {* eresolve_tac @{context} [@{thm disjE}] 1 *})
 txt{* applies the rule to the first assumption yielding the goal state:
 \begin{isabelle}
 @{subgoals [display]}
 \end{isabelle}
 *}
 (*<*)
 oops
 lemma
 shows "\<lbrakk>P1 \<or> Q1; P2 \<or> Q2\<rbrakk> \<Longrightarrow> R"
-apply(tactic {* etac @{thm disjE} 1 *})
+apply(tactic {* eresolve_tac @{context} [@{thm disjE}] 1 *})
 (*>*)
 back
 txt{* the rule now applies to the second assumption.
 \begin{isabelle}
 @{subgoals [display]}
 combinator @{ML_ind  DETERM in Tactical}.
 *}
 lemma
 shows "\<lbrakk>P1 \<or> Q1; P2 \<or> Q2\<rbrakk> \<Longrightarrow> R"
-apply(tactic {* DETERM (etac @{thm disjE} 1) *})
+apply(tactic {* DETERM (eresolve_tac @{context} [@{thm disjE}] 1) *})
 txt {*\begin{minipage}{\textwidth}
 @{subgoals [display]}
 \end{minipage} *}
 (*<*)oops(*>*)
 text {*
 fun name_sthm (nm, thm) =
 Pretty.enclose (nm ^ ": ") "" [pretty_thm_no_vars ctxt thm]
 fun name_cthm ((_, nm), thm) =
 Pretty.enclose (nm ^ ": ") "" [pretty_thm_no_vars ctxt thm]
-fun name_ctrm (nm, ctrm) =
+fun name_trm (nm, trm) =
-Pretty.enclose (nm ^ ": ") "" [pretty_cterms ctxt ctrm]
+Pretty.enclose (nm ^ ": ") "" [pretty_terms ctxt trm]
 val pps = [Pretty.big_list "Simplification rules:" (map name_sthm simps),
 Pretty.big_list "Congruences rules:" (map name_cthm congs),
-Pretty.big_list "Simproc patterns:" (map name_ctrm procs)]
+Pretty.big_list "Simproc patterns:" (map name_trm procs)]
 in
 pps |> Pretty.chunks
 |> pwriteln
 end*}
 text_raw {*
 In order to solve all cases we have to deal with corner-cases such as the
 lemma being an exact instance of the permutation composition lemma. This can
 often be done easier by implementing a simproc or a conversion. Both will be
 explained in the next two chapters.
-(FIXME: Is it interesting to say something about @{term "op =simp=>"}?)
+(FIXME: Is it interesting to say something about @{term "(=simp=>)"}?)
 (FIXME: What are the second components of the congruence rules---something to
 do with weak congruence constants?)
 (FIXME: what are @{ML mksimps_pairs}; used in Nominal.thy)
 want this, then you have to use a slightly different method for setting
 up the simproc. First the function @{ML fail_simproc} needs to be modified
 to
 *}
-ML %grayML{*fun fail_simproc' ctxt redex =
+ML %grayML{*fun fail_simproc' _ ctxt redex =
 let
 val _ = pwriteln (Pretty.block
-[Pretty.str "The redex:", pretty_term ctxt redex])
+[Pretty.str "The redex:", pretty_cterm ctxt redex])
 in
 NONE
 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 pretty_term in Pretty}).
 We can turn this function into a proper simproc using the function
-@{ML Simplifier.simproc_global_i}:
+@{ML Simplifier.make_simproc}:
 *}
+ML %grayML{*val fail' =
-ML %grayML{*fun fail' ctxt =
+Simplifier.make_simproc @{context} "fail_simproc'"
-let
+{lhss = [@{term "Suc n"}], proc = fail_simproc'}*}
-val thy = @{theory}
-val pat = [@{term "Suc n"}]
-in
-Simplifier.simproc_global_i thy "fail_simproc'" pat (K fail_simproc' ctxt)
-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.
 Now the simproc is set up and can be explicitly added using
 see this in the proof
 *}
 lemma
 shows "Suc (Suc 0) = (Suc 1)"
-apply(tactic {* simp_tac ((put_simpset HOL_basic_ss @{context}) addsimprocs [fail' @{context}]) 1*})
+apply(tactic {* simp_tac ((put_simpset HOL_basic_ss @{context}) addsimprocs [fail']) 1*})
 (*<*)oops(*>*)
 text {*
 The simproc @{ML fail'} prints out the sequence
 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 %grayML{*fun plus_one_simproc ctxt redex =
+ML %grayML{*fun plus_one_simproc _ ctxt redex =
-case redex of
+case Thm.term_of redex of
 @{term "Suc 0"} => NONE
 | _ => SOME @{thm plus_one}*}
 text {*
 and set up the simproc as follows.
 *}
-ML %grayML{*fun plus_one ctxt =
+ML %grayML{*val plus_one =
-let
+Simplifier.make_simproc @{context} "sproc +1"
-val thy = @{theory}
+{lhss = [@{term "Suc n"}], proc = plus_one_simproc}*}
-val pat = [@{term "Suc n"}]
-in
-Simplifier.simproc_global_i thy "sproc +1" pat (K plus_one_simproc ctxt)
-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 (put_simpset HOL_basic_ss @{context} addsimprocs [plus_one @{context}]) 1*})
+apply(tactic {* simp_tac (put_simpset HOL_basic_ss @{context} addsimprocs [plus_one]) 1*})
 txt{*
 where the simproc produces the goal state
 \begin{isabelle}
 @{subgoals[display]}
 \end{isabelle}
 Anyway, either version can be used in the function that produces the actual
 theorem for the simproc.
 *}
-ML %grayML{*fun nat_number_simproc ctxt t =
+ML %grayML{*fun nat_number_simproc _ ctxt ct =
-SOME (get_thm_alt ctxt (t, dest_suc_trm t))
+SOME (get_thm_alt ctxt (Thm.term_of ct, dest_suc_trm (Thm.term_of ct)))
 handle TERM _ => NONE *}
 text {*
 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 %grayML{*fun nat_number ctxt =
+ML %grayML{*val nat_number =
-let
+Simplifier.make_simproc @{context} "nat_number"
-val thy = @{theory}
+{lhss = [@{term "Suc n"}], proc = nat_number_simproc}*}
-val pat = [@{term "Suc n"}]
-in
-Simplifier.simproc_global_i thy "nat_number" pat (K nat_number_simproc ctxt)
-end*}
 text {*
 Now in the lemma
 *}
 lemma
 shows "P (Suc (Suc 2)) (Suc 99) (0::nat) (Suc 4 + Suc 0) (Suc (0 + 0))"
-apply(tactic {* simp_tac (put_simpset HOL_ss @{context} addsimprocs [nat_number @{context}]) 1*})
+apply(tactic {* simp_tac (put_simpset HOL_ss @{context} addsimprocs [nat_number]) 1*})
 txt {*
 you obtain the more legible goal state
 \begin{isabelle}
 @{subgoals [display]}
 \end{isabelle}*}
 in all possible positions.
 *}
 ML %linenosgray{*fun true_conj1_conv ctxt ctrm =
 case (Thm.term_of ctrm) of
-@{term "op \<and>"} $ @{term True} $ _ =>
+@{term "(\<and>)"} $ @{term True} $ _ =>
 (Conv.arg_conv (true_conj1_conv ctxt) then_conv
 Conv.rewr_conv @{thm true_conj1}) ctrm
 | _ $ _ => Conv.comb_conv (true_conj1_conv ctxt) ctrm
 | Abs _ => Conv.abs_conv (fn (_, ctxt) => true_conj1_conv ctxt) ctxt ctrm
 | _ => Conv.all_conv ctrm*}
 @{ML_type "cterm -> thm"}). The code of the transformation is below.
 *}
 ML %linenosgray{*fun unabs_def ctxt def =
 let
-val (lhs, rhs) = Thm.dest_equals (cprop_of def)
+val (lhs, rhs) = Thm.dest_equals (Thm.cprop_of def)
-val xs = strip_abs_vars (term_of rhs)
+val xs = strip_abs_vars (Thm.term_of rhs)
 val (_, ctxt') = Variable.add_fixes (map fst xs) ctxt
-val thy = Proof_Context.theory_of ctxt'
+val cxs = map (Thm.cterm_of ctxt' o Free) xs
-val cxs = map (cterm_of thy o Free) xs
 val new_lhs = Drule.list_comb (lhs, cxs)
 fun get_conv [] = Conv.rewr_conv def
 | get_conv (_::xs) = Conv.fun_conv (get_conv xs)
 in

changeset 562	daf404920ab9
parent 559	ffa5c4ec9611
child 565	cecd7a941885