
diff -r 5dcad9348e4d -r f49dc7e96235 CookBook/Tactical.thy
--- a/CookBook/Tactical.thy	Sun Feb 08 08:45:25 2009 +0000
+++ b/CookBook/Tactical.thy	Mon Feb 09 01:12:00 2009 +0000
@@ -5,16 +5,15 @@
 chapter {* Tactical Reasoning\label{chp:tactical} *}
 
 text {*
-
-  The main reason for descending to the ML-level of Isabelle is to be
-  able to implement automatic proof procedures. Such proof procedures usually
-  lessen considerably the burden of manual reasoning, for example, when
-  introducing new definitions. These proof procedures are centred around
-  refining a goal state using tactics. This is similar to the @{text
-  apply}-style reasoning at the user level, where goals are modified in a
-  sequence of proof steps until all of them are solved. However, there are
-  also more structured operations available on the ML-level that help with 
-  the handling of variables and assumptions.
+  The main reason for descending to the ML-level of Isabelle is to be able to
+  implement automatic proof procedures. Such proof procedures usually lessen
+  considerably the burden of manual reasoning, for example, when introducing
+  new definitions. These proof procedures are centred around refining a goal
+  state using tactics. This is similar to the \isacommand{apply}-style
+  reasoning at the user level, where goals are modified in a sequence of proof
+  steps until all of them are solved. However, there are also more structured
+  operations available on the ML-level that help with the handling of
+  variables and assumptions.
 
 *}
 
@@ -59,10 +58,7 @@
   it can make use of the local assumptions (there are none in this example). 
   The functions @{ML etac}, @{ML rtac} and @{ML atac} correspond to 
   @{text erule}, @{text rule} and @{text assumption}, respectively. 
-  The operator @{ML THEN} strings the tactics together. A difference
-  between the \isacommand{apply}-script and the ML-code is that the
-  former causes the lemma to be stored under the name @{text "disj_swap"}, 
-  whereas the latter does not include any code for this.
+  The operator @{ML THEN} strings the tactics together. 
 
   \begin{readmore}
   To learn more about the function @{ML Goal.prove} see \isccite{sec:results}
@@ -73,12 +69,15 @@
   Isabelle Reference Manual.
   \end{readmore}
 
-  Note that we used antiquotations for referencing the theorems. We could also
-  just have written @{ML "etac disjE 1"} and so on, but this is considered bad
-  style. The reason is that the binding for @{ML disjE} can be re-assigned by 
-  the user and thus one does not have complete control over which theorem is
-  actually applied. This problem is nicely prevented by using antiquotations, 
-  because then the theorems are fixed statically at compile-time.
+  Note that we used 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 there are no ML-binding obtained
+  the theorem dynamically using the theorem @{ML thm}; for example @{ML "etac
+  (thm \"disjE\") 1"}. Both ways however are considered bad style. The reason
+  is that the binding for @{ML disjE} can be re-assigned by the user and thus
+  one does not have complete control over which theorem is actually
+  applied. This problem is nicely prevented by using antiquotations, because
+  then the theorems are fixed statically at compile-time.
 
   During the development of automatic proof procedures, you will often find it 
   necessary to test a tactic on examples. This can be conveniently 
@@ -107,9 +106,9 @@
   The tactic @{ML foo_tac} is just a sequence of simple tactics stringed
   together by @{ML THEN}. As can be seen, each simple tactic in @{ML foo_tac}
   has a hard-coded number that stands for the subgoal analysed by the
-  tactic (@{text "1"} stands for the first, or top-most, subgoal). This is 
-  sometimes wanted, but usually not. To avoid the explicit numbering in 
-  the tactic, you can write
+  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{*val foo_tac' = 
@@ -121,9 +120,8 @@
 
 text {* 
   and then give the number for the subgoal explicitly when the tactic is
-  called. For every operator that combines tactics (@{ML THEN} is only one 
-  such operator), a primed version exists. So in the next proof you 
-  can first discharge the second subgoal, and after that the first.
+  called. So in the next proof you can first discharge the second subgoal, and
+  after that the first.
 *}
 
 lemma "P1 \<or> Q1 \<Longrightarrow> Q1 \<or> P1"
@@ -134,25 +132,26 @@
 
 text {*
   This kind of addressing is more difficult to achieve when the goal is 
-  hard-coded inside the tactic.
+  hard-coded inside the tactic. For every operator that combines tactics 
+  (@{ML THEN} is only one such operator) a ``primed'' version exists.
 
   The tactics @{ML foo_tac} and @{ML foo_tac'} are very specific for
   analysing goals being only of the form @{prop "P \<or> Q \<Longrightarrow> Q \<or> P"}. If the goal is not
-  of this form, then @{ML foo_tac} throws the error message:
+  of this form, then they throw the error message:
 
   \begin{isabelle}
   @{text "*** empty result sequence -- proof command failed"}\\
   @{text "*** At command \"apply\"."}
   \end{isabelle}
 
-  Meaning the tactic failed. The reason for this error message is that tactics 
+  Meaning the tactics failed. The reason for this error message is that tactics 
   are functions that map a goal state to a (lazy) sequence of successor states, 
   hence the type of a tactic is:
   
   @{text [display, gray] "type tactic = thm -> thm Seq.seq"}
 
   It is custom that if a tactic fails, it should return the empty sequence: 
-  your own tactics should not raise exceptions willy-nilly.
+  therefore your own tactics should not raise exceptions willy-nilly.
 
   The simplest tactics are @{ML no_tac} and @{ML all_tac}. The first returns
   the empty sequence and is defined as
@@ -171,7 +170,7 @@
   which means @{ML all_tac} always succeeds (but also does not make any progress 
   with the proof).
 
-  The lazy list of possible successor states shows through to the user-level 
+  The lazy list of possible successor states shows through at the user-level 
   of Isabelle when using the command \isacommand{back}. For instance in the 
   following proof, there are two possibilities for how to apply 
   @{ML foo_tac'}.
@@ -214,12 +213,12 @@
 text {*
   which prints out the given theorem (using the string-function defined 
   in Section~\ref{sec:printing}) and then behaves like @{ML all_tac}. We
-  now can inspect every proof state in the follwing proof. On the left-hand
-  side we show the goal state as shown by the system; on the right-hand
-  side the print out from @{ML my_print_tac}.
+  now can inspect every proof state in a proof. Consider the proof below: on 
+  the left-hand side we show the goal state as shown by Isabelle; on the 
+  right-hand side the print out from @{ML my_print_tac}.
 *}
 
-lemma shows "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B"
+lemma shows "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B" 
 apply(tactic {* my_print_tac @{context} *})
 
 txt{* \small 
@@ -275,12 +274,12 @@
   @{text[display] "A\<^isub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^isub>n \<Longrightarrow> (C)"}
 
   where @{term C} is the goal to be proved and the @{term "A\<^isub>i"} are the  
-  subgoals. So in the first step the goal state is always of the form
+  subgoals. So after setting up the lemma, the goal state is always of the form
   @{text "C \<Longrightarrow> (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)"} applied to each goal;
   however this constant is invisible in the print out above). This 
-  prevents that premises are misinterpreted as open subgoals. 
+  prevents that premises of @{text C} are misinterpreted 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. 
@@ -290,7 +289,17 @@
 section {* Simple Tactics *}
 
 text {*
-  As seen above, the function @{ML atac} corresponds to the assumption tactic.
+  A simple tactic is @{ML print_tac}, which is useful for low-level debugging of tactics.
+  It just prints out a message and the current goal state.
+*}
+ 
+lemma shows "False \<Longrightarrow> True"
+apply(tactic {* print_tac "foo message" *})
+(*<*)oops(*>*)
+
+text {*
+  Another simple tactic is the function @{ML atac}, which, as shown in the previous
+  section, corresponds to the assumption command.
 *}
 
 lemma shows "P \<Longrightarrow> P"
@@ -327,8 +336,9 @@
 (*<*)oops(*>*)
 
 text {*
-  As mentioned above, most basic tactics take a number as argument, which
-  addresses to subgoal they are analysing.
+  As mentioned in the previous section, most basic tactics take a number as 
+  argument, which addresses the subgoal they are analysing. In the proof below,
+  we first break up the second subgoal by focusing on this subgoal first.
 *}
 
 lemma shows "Foo" and "P \<and> Q"
@@ -339,10 +349,10 @@
 (*<*)oops(*>*)
 
 text {* 
-  Corresponding to @{ML rtac}, there is also the tactic @{ML resolve_tac}, which
-  however expects a list of theorems as arguments. From this list it will apply with 
-  the first applicable theorem (later theorems that are also applicable can be
-  explored via the lazy sequences mechanism). Given the abbreviation
+  The function @{ML resolve_tac} is similar to @{ML rtac}, except that it
+  expects a list of theorems as arguments. 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{*val resolve_tac_xmp = resolve_tac [@{thm impI}, @{thm conjI}]*}
@@ -362,25 +372,71 @@
 
 text {* 
   Similarly versions exists for @{ML atac} (@{ML assume_tac}), @{ML etac} 
-  (@{ML eresolve_tac}) and so on.
+  (@{ML eresolve_tac}) and so on. 
+
+  (FIXME: @{ML cut_facts_tac})
 
-  The tactic @{ML print_tac} is useful for low-level debugging of tactics: it
-  prints out a message and the current goal state.
+  Since rules are applied using higher-order unification, an automatic proof
+  procedure might become too fragile, if it just applies inference rules shown
+  in the fashion above.  More constraints can be introduced by
+  pre-instantiating theorems with other theorems. You can do this using the
+  function @{ML RS}. For example
+  
+  @{ML_response_fake [display,gray]
+  "@{thm disjI1} RS @{thm conjI}" "\<lbrakk>?P1; ?Q\<rbrakk> \<Longrightarrow> (?P1 \<or> ?Q1) \<and> ?Q"}
+
+  instantiates the first premise of the @{text conjI}-rule with the
+  rule @{text disjI1}. The function @{ML RSN} is similar, but 
+  takes a number and makes explicit which premise should be instantiated. 
+  To improve readability we are going use the following function
 *}
- 
-lemma shows "False \<Longrightarrow> True"
-apply(tactic {* print_tac "foo message" *})
-(*<*)oops(*>*)
+
+ML{*fun no_vars ctxt thm =
+let 
+  val ((_, [thm']), _) = Variable.import_thms true [thm] ctxt
+in
+  thm'
+end*}
 
 text {*
-  
-  (FIXME explain RS MRS)
+  to transform the schematic variables of a theorem into free variables. 
+  This means for the @{ML RS}-expression above:
+
+  @{ML_response_fake [display,gray]
+  "no_vars @{context} (@{thm disjI1} RS @{thm conjI})" "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> (P \<or> Qa) \<and> Q"}
+
+  If you want to instantiate more than one premise, you can use the function 
+  @{ML MRS}:
+
+  @{ML_response_fake [display,gray]
+  "no_vars @{context} ([@{thm disjI1}, @{thm disjI2}] MRS @{thm conjI})" 
+  "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> (P \<or> Qa) \<and> (Pa \<or> Q)"}
+
+  If you need to instantiate lists of theorems, you can use the
+  functions @{ML RL} and @{ML MRL}. For example below every
+  theorem in the first list is instantiated against every theorem
+  in the second.
+
+  @{ML_response_fake [display,gray]
+   "[@{thm impI}, @{thm disjI2}] RL [@{thm conjI}, @{thm disjI1}]" 
+"[\<lbrakk>P \<Longrightarrow> Q; Qa\<rbrakk> \<Longrightarrow> (P \<longrightarrow> Q) \<and> Qa,
+ \<lbrakk>Q; Qa\<rbrakk> \<Longrightarrow> (P \<or> Q) \<and> Qa,
+ (P \<Longrightarrow> Q) \<Longrightarrow> (P \<longrightarrow> Q) \<or> Qa,
+ Q \<Longrightarrow> (P \<or> Q) \<or> Qa]"}
+
+  \begin{readmore}
+  The combinators for instantiating theorems are defined in @{ML_file "Pure/drule.ML"}.
+  \end{readmore}
 
   Often proofs involve elaborate operations on assumptions and 
   @{text "\<And>"}-quantified variables. To do such operations on the ML-level 
   using the basic tactics is very unwieldy and brittle. Some convenience and
   safety is provided by the tactic @{ML SUBPROOF}. This tactic fixes the parameters 
   and binds the various components of a proof state into a record. 
+  To see what happens, assume the function defined in Figure~\ref{fig:sptac}, which
+  takes a record as argument and just prints out the content of this record (using the 
+  string transformation functions defined in Section~\ref{sec:printing}). Consider
+  now the proof
 *}
 
 text_raw{*
@@ -406,17 +462,11 @@
 text_raw{*
 \end{isabelle}
 \caption{A function that prints out the various parameters provided by the tactic
- @{ML SUBPROOF}. It uses the functions extracting strings from @{ML_type cterm}s 
-  and @{ML_type thm}s, which are defined in Section~\ref{sec:printing}.\label{fig:sptac}}
+ @{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}}
 \end{figure}
 *}
 
-text {*
-  To see what happens, assume the function defined in Figure~\ref{fig:sptac}, which
-  takes a record as argument and just prints out the content of this record (using the 
-  string transformation functions defined in Section~\ref{sec:printing}). Consider
-  now the proof
-*}
 
 lemma shows "\<And>x y. A x y \<Longrightarrow> B y x \<longrightarrow> C (?z y) x"
 apply(tactic {* SUBPROOF sp_tac @{context} 1 *})?
@@ -435,10 +485,10 @@
   \end{quote}
 
   Note in the actual output the brown colour of the variables @{term x} and 
-  @{term y}. Although parameters in the original goal, they are fixed inside
+  @{term y}. Although they are parameters in the original goal, they are fixed inside
   the subproof. Similarly the schematic variable @{term z}. The assumption 
-  @{prop "A x y"} is bound once as @{ML_type cterm} to the record-variable 
-  @{text asms} and another time as @{ML_type thm} to @{text prems}.
+  @{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}.
 
   Notice also that we had to append @{text "?"} to \isacommand{apply}. The 
   reason is that @{ML SUBPROOF} normally expects that the subgoal is solved completely.
@@ -471,10 +521,10 @@
 text {*
   where we now also have @{term "B y x"} as an assumption.
 
-  One convenience of @{ML SUBPROOF} is that we can apply assumption
+  One convenience of @{ML SUBPROOF} is that we can apply the assumptions
   using the usual tactics, because the parameter @{text prems} 
-  contains the assumptions as theorems. With this we can easily 
-  implement a tactic that almost behaves like @{ML atac}:
+  contains them as theorems. With this we can easily 
+  implement a tactic that almost behaves like @{ML atac}, namely:
 *}
 
 ML{*val atac' = SUBPROOF (fn {prems, ...} => resolve_tac prems 1)*}
@@ -496,23 +546,26 @@
   number @{text "1"} and also the ``outer'' call to @{ML SUBPROOF} in 
   the \isacommand{apply}-step uses @{text "1"}. Another advantage 
   of @{ML SUBGOAL} is that the addressing  inside it is completely 
-  local to the proof inside. It is therefore possible to also apply 
+  local to the subproof inside. It is therefore possible to also apply 
   @{ML atac'} to the second goal:
 *}
 
 lemma shows "True" and "\<And>x y. \<lbrakk>B x y; A x y; C x y\<rbrakk> \<Longrightarrow> A x y"
 apply(tactic {* atac' @{context} 2 *})
-txt{* This gives:
-      @{subgoals [display]} *}
-(*<*)oops(*>*)
+apply(rule TrueI)
+done
 
 
 text {*
+  \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}. 
-  It allows you to inspect a subgoal specified by a number. With this we can 
-  implement a little tactic that applies a rule corresponding to its 
-  topmost connective. The tactic should only apply ``safe'' rules (that is
-  which do not render the goal unprovable). For this we can write:
+  It allows you to inspect a specified subgoal. With this you can implement 
+  a tactic that applies a rule according to its topmost connective (we only 
+  analyse a few connectives). The tactic is as follows:
 *}
 
 ML %linenumbers{*fun select_tac (t,i) =
@@ -524,7 +577,21 @@
    | Const (@{const_name "All"}, _) $ _ => rtac @{thm allI} i
    | _ => all_tac*}
 
-lemma shows "A \<and> B" "A \<longrightarrow> B" "\<forall>x. C x" "D \<Longrightarrow> E"
+text {*
+  In line 3 you need to decend under the outermost @{term "Trueprop"} in order
+  to get to the connective you like to analyse. Otherwise goals @{prop "A \<and> B"} 
+  are not bropek up. In line 7, the pattern cannot be constructed using the
+  @{text "@term"}-antiquotation, because that would fix the type of the 
+  quantified variable. In this case you really have to construct the pattern
+  by using the term-constructors. The other cases work, because their type
+  is always bool. In case that the goal does not fall into any of the categorories, 
+  then we chose to just return @{ML all_tac} (i.e., the tactic never fails). 
+
+  Let us now see how to apply this tactic.
+*}
+
+
+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 3 *})
 apply(tactic {* SUBGOAL select_tac 2 *})
@@ -533,29 +600,72 @@
 (*<*)oops(*>*)
 
 text {*
-  However, this example is contrived, as there are much simpler ways
-  to implement a proof procedure like the one above. They will be explained
-  in the next section.
+  Note that we applied it in ``reverse'' order. This is a trick in 
+  order to be independent from what subgoals the rule produced. If we had
+  it applied 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 3 *})
+apply(tactic {* SUBGOAL select_tac 4 *})
+apply(tactic {* SUBGOAL select_tac 5 *})
+(*<*)oops(*>*)
 
-  (Notice that we applied the goals in reverse order)
+text {*
+  then we have to be careful to not apply the tactic to the two subgoals the
+  first goal produced. This can be messy in an automated proof script. The
+  reverse application, on the other hand, is easy to implement.
 
-  A variant of @{ML SUBGOAL} is @{ML CSUBGOAL} which allows access to the goal
-  as @{ML_type cterm} instead of a @{ML_type term}.
+  However, this example is contrived: there are much simpler ways to implement
+  such proof procedure that analyses a goal according to its topmost
+  connective. They will be explained in the next section.
+*}
+
+section {* Tactic Combinators *}
+
+text {* 
+  To be able to implement powerful tactics out of smaller component tactics, 
+  Isabelle provides tactic combinators. In the previous section we already
+  used @{ML THEN} which strings two tactics together in sequence. For example:
 *}
 
+lemma shows "(Foo \<and> Bar) \<and> False"
+apply(tactic {* rtac @{thm conjI} 1 THEN rtac @{thm conjI} 1 *})
+txt {* \begin{minipage}{\textwidth}
+       @{subgoals [display]} 
+       \end{minipage} *}
+(*<*)oops(*>*)
 
-section {* Operations on Tactics *}
-
-text {* @{ML THEN} *}
+text {*
+  If you want to avoid the hard-coded subgoal addressing, then you can use
+  @{ML THEN'}. For example:
+*}
 
 lemma shows "(Foo \<and> Bar) \<and> False"
-apply(tactic {* (rtac @{thm conjI} 1) 
-                 THEN (rtac @{thm conjI} 1) *})
-txt {* @{subgoals [display]} *}
+apply(tactic {* (rtac @{thm conjI} THEN' rtac @{thm conjI}) 1 *})
+txt {* \begin{minipage}{\textwidth}
+       @{subgoals [display]} 
+       \end{minipage} *}
 (*<*)oops(*>*)
 
+text {* 
+  For most tactic combinators such a ``primed'' version exists.
+  In what follows we will, whenever appropriate, prefer the primed version of
+  the tactic combinator and omit to mention the simple one. 
+
+  With @{ML THEN} and @{ML THEN'} it must be guaranteed that both tactics 
+  sucessfully apply; otherwise the whole tactic will fail. If you want to
+  try out either one tactic, then you can use @{ML ORELSE'}. For 
+  example
+*}
+
 ML{*val orelse_xmp = (rtac @{thm disjI1} ORELSE' rtac @{thm conjI})*}
 
+text {*
+  will first try out rule @{text disjI} and after that @{text conjI}.
+*}
+
 lemma shows "True \<and> False" and "Foo \<or> Bar"
 apply(tactic {* orelse_xmp 1 *})
 apply(tactic {* orelse_xmp 3 *})
@@ -564,15 +674,22 @@
 
 
 text {*
-  @{ML EVERY} @{ML REPEAT} @{ML DETERM}
+  applies 
+
+
+  @{ML REPEAT} @{ML DETERM}
 
+*}
+
+section {* Rewriting and Simplifier Tactics *}
+
+text {*
   @{ML rewrite_goals_tac}
-  @{ML cut_facts_tac}
   @{ML ObjectLogic.full_atomize_tac}
   @{ML ObjectLogic.rulify_tac}
-  @{ML resolve_tac}
 *}
 
+
 section {* Structured Proofs *}
 
 lemma True




