
diff -r 0a5c95f4d70c -r de625e5f6a36 CookBook/Tactical.thy
--- a/CookBook/Tactical.thy	Thu Feb 05 22:40:22 2009 +0000
+++ b/CookBook/Tactical.thy	Thu Feb 05 22:40:46 2009 +0000
@@ -1,5 +1,5 @@
 theory Tactical
-imports Base
+imports Base FirstSteps
 begin
 
 chapter {* Tactical Reasoning\label{chp:tactical} *}
@@ -12,9 +12,8 @@
   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.
-
-
+  all of them are solved. However, there are also more structured operations
+  that help with handling of variables and assumptions.
 *}
 
 section {* Tactical Reasoning *}
@@ -50,19 +49,23 @@
 end" "?P \<or> ?Q \<Longrightarrow> ?Q \<or> ?P"}
   
   To start the proof, the function @{ML "Goal.prove"}~@{text "ctxt xs As C
-  tac"} sets up a goal state for proving the goal @{text C} under the
-  assumptions @{text As} (empty in the proof at hand) with the variables
+  tac"} sets up a goal state for proving the goal @{text C} 
+  (that is @{prop "P \<or> Q \<Longrightarrow> Q \<or> P"} in the proof at hand) under the
+  assumptions @{text As} (happens to be empty) with the variables
   @{text xs} that will be generalised once the goal is proved (in our case
   @{text P} and @{text Q}). The @{text "tac"} is the tactic that proves the goal;
   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 tactics together.
+  The operator @{ML THEN} strings the tactics together.
 
   \begin{readmore}
-  To learn more about the function @{ML Goal.prove} see \isccite{sec:results} and
-  the file @{ML_file "Pure/goal.ML"}. For more information about the internals of goals see 
-  \isccite{sec:tactical-goals}. 
+  To learn more about the function @{ML Goal.prove} see \isccite{sec:results}
+  and the file @{ML_file "Pure/goal.ML"}. For more information about the
+  internals of goals see \isccite{sec:tactical-goals}.  See @{ML_file
+  "Pure/tactic.ML"} and @{ML_file "Pure/tctical.ML"} for the code of basic
+  tactics and tactic combinators; see also Chapters 3 and 4 in the old
+  Isabelle Reference Manual.
   \end{readmore}
 
   Note that we used antiquotations for referencing the theorems. We could also
@@ -92,9 +95,9 @@
 done
 
 text {*
-  The apply-step applies the @{ML foo_tac} and therefore solves the goal completely.  
-  Inside @{text "tactic \<verbopen> \<dots> \<verbclose>"} 
-  we can call any function that returns a tactic.
+  By using @{text "tactic \<verbopen> \<dots> \<verbclose>"} in the apply-step,
+  you can call @{ML foo_tac} or any function that returns a tactic from the
+  user level of Isabelle.
 
   As can be seen, each tactic in @{ML foo_tac} has a hard-coded number that
   stands for the subgoal analysed by the tactic. In our case, we only focus on the first
@@ -111,7 +114,8 @@
 
 text {* 
   and then give the number for the subgoal explicitly when the tactic is
-  called. So in the next proof we discharge first the second subgoal,
+  called. For every operator that combines tactics, such a primed version 
+  exists. So in the next proof we can first discharge the second subgoal,
   and after that the first.
 *}
 
@@ -122,20 +126,31 @@
 done
 
 text {*
-  The tactic @{ML foo_tac} is very specific for analysing goals 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 about an empty result sequence---meaning the tactic
-  failed. The reason for this 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
+  (FIXME: maybe add something about how each goal state is interpreted
+  as a theorem)
+
+  The tactic @{ML foo_tac} (and @{ML foo_tac'}) are very specific for
+  analysing goals 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:
+
+  \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 
+  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"}
 
-  Consequently, if a tactic fails, then it returns the empty sequence. This
-  is by the way the default behaviour for a failing tactic; tactics should 
-  not raise exceptions.
+  It is custom that if a tactic fails, it should return the empty sequence: 
+  tactics should not raise exceptions willy-nilly.
 
-  In the following example there are two possibilities for how to apply the tactic.
+  The lazy list of possible successor states shows through to 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'}.
 *}
 
 lemma "\<lbrakk>P \<or> Q; P \<or> Q\<rbrakk> \<Longrightarrow> Q \<or> P"
@@ -144,82 +159,111 @@
 done
 
 text {*
-  The application of the tactic results in a sequence of two possible
-  proofs. The Isabelle command \isacommand{back} allows us to explore both 
-  possibilities.
-
+  By using \isacommand{back}, we construct the proof that uses the
+  second assumption to complete the proof. In more interesting 
+  situations, different possibilities can lead to different proofs.
+  
   \begin{readmore}
   See @{ML_file "Pure/General/seq.ML"} for the implementation of lazy
   sequences. However in day-to-day Isabelle programming, one rarely 
   constructs sequences explicitly, but uses the predefined functions
-  instead. See @{ML_file "Pure/tactic.ML"} and 
-  @{ML_file "Pure/tctical.ML"} for the code of basic tactics and tactic
-  combinators; see also Chapters 3 and 4 in 
-  the old Isabelle Reference Manual.
+  instead.
   \end{readmore}
 
 *}
 
-
 section {* Basic Tactics *}
 
-lemma shows "False \<Longrightarrow> False"
+text {*
+  As seen above, the function @{ML atac} corresponds to the assumption tactic.
+*}
+
+lemma shows "P \<Longrightarrow> P"
 apply(tactic {* atac 1 *})
 done
 
-lemma shows "True \<and> True"
+text {*
+  Similarly, @{ML rtac}, @{ML dtac}, @{ML etac} and @{ML ftac} correspond
+  to @{ML_text rule}, @{ML_text drule}, @{ML_text erule} and @{ML_text frule}, 
+  respectively. Below are three examples with the resulting goal state. How
+  they work should therefore be self-explanatory.  
+*}
+
+lemma shows "P \<and> Q"
 apply(tactic {* rtac @{thm conjI} 1 *})
-txt {* @{subgoals [display]} *}
+txt{*@{subgoals [display]}*}
 (*<*)oops(*>*)
 
-lemma 
-  shows "Foo"
-  and "True \<and> True"
-apply(tactic {* rtac @{thm conjI} 2 *})
-txt {* @{subgoals [display]} *}
-(*<*)oops(*>*)
-
-lemma shows "False \<and> False \<Longrightarrow> False"
+lemma shows "P \<and> Q \<Longrightarrow> False"
 apply(tactic {* etac @{thm conjE} 1 *})
-txt {* @{subgoals [display]} *}
+txt{*@{subgoals [display]}*}
 (*<*)oops(*>*)
 
 lemma shows "False \<and> True \<Longrightarrow> False"
 apply(tactic {* dtac @{thm conjunct2} 1 *})
-txt {* @{subgoals [display]} *}
+txt{*@{subgoals [display]}*}
 (*<*)oops(*>*)
 
 text {*
-  similarly @{ML ftac}
+  As mentioned above, most basic tactics take a number as argument, which
+  addresses to subgoal they are analysing.
+*}
+
+lemma shows "Foo" and "P \<and> Q"
+apply(tactic {* rtac @{thm conjI} 2 *})
+txt {*@{subgoals [display]}*}
+(*<*)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
 *}
 
-text {* diagnostics *} 
-lemma shows "True \<Longrightarrow> False"
+ML{*val resolve_tac_xmp = resolve_tac [@{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_tac_xmp 1 *})
+apply(tactic {* resolve_tac_xmp 2 *})
+txt{* @{subgoals [display]} *}
+(*<*)oops(*>*)
+
+text {* 
+  Similarly versions exists for @{ML atac} (@{ML assume_tac}), @{ML etac} 
+  (@{ML eresolve_tac}) and so on.
+
+  The tactic @{ML print_tac} is useful for low-level debugging of tactics: it
+  prints out a message and the current goal state.
+*}
+ 
+lemma shows "False \<Longrightarrow> True"
 apply(tactic {* print_tac "foo message" *})
 (*<*)oops(*>*)
 
-text {* Let us assume the following four string conversion functions: *}
-
-ML{*fun str_of_cterm ctxt t =  
-   Syntax.string_of_term ctxt (term_of t)
-
-fun str_of_cterms ctxt ts =  
-  commas (map (str_of_cterm ctxt) ts)
+text {*
+  Also for useful for debugging, but not exclusively, are the tactics @{ML all_tac} and
+  @{ML no_tac}. The former always succeeds (but does not change the goal state), and
+  the latter always fails.
 
-fun str_of_thm ctxt thm =
-  let
-    val {prop, ...} = crep_thm thm
-  in 
-    str_of_cterm ctxt prop
-  end
+  (FIXME explain RS MRS)
 
-fun str_of_thms ctxt thms =  
-  commas (map (str_of_thm ctxt) thms)*}
-
-text {*
-  and the following function
+  Often proofs involve elaborate operations on assumptions and variables
+  @{text "\<And>"}-quantified in the goal state. 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. 
 *}
 
+text_raw{*
+\begin{figure}
+\begin{isabelle}
+*}
 ML{*fun sp_tac {prems, params, asms, concl, context, schematics} = 
   let 
     val str_of_params = str_of_cterms context params
@@ -236,20 +280,28 @@
   in
     no_tac 
   end*}
+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}}
+\end{figure}
+*}
 
 text {*
-  then the tactic @{ML SUBPROOF} fixes the parameters and binds the various components
-  of a proof state into a record. For example 
+  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"
+lemma shows "\<And>x y. A x y \<Longrightarrow> B y x \<longrightarrow> C (?z y) x"
 apply(tactic {* SUBPROOF sp_tac @{context} 1 *})?
 
 txt {*
-  prints out 
+  which yields the printout:
 
-  \begin{center}
+  \begin{quote}\small
   \begin{tabular}{ll}
   params:     & @{term x}, @{term y}\\
   schematics: & @{term z}\\
@@ -257,18 +309,31 @@
   concl:      & @{term "B y x \<longrightarrow> C (z y) x"}\\
   prems:      & @{term "A x y"}
   \end{tabular}
-  \end{center}
+  \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
+  the subproof. Similarly the schematic variable @{term z}. The assumption 
+  is bound once as @{ML_type cterm} to the record-variable @{text asms} and 
+  another time as @{ML_type thm} to @{text prems}.
 
-  Continuing the proof script with
+  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.
+  Since in the function @{ML sp_tac} we returned the tactic @{ML no_tac}, the subproof
+  obviously fails. The question-mark allows us to recover from this failure
+  in a graceful manner so that the warning messages are not overwritten
+  by the error message.
+
+  If we continue the proof script by applying the @{text impI}-rule
 *}
 
 apply(rule impI)
 apply(tactic {* SUBPROOF sp_tac @{context} 1 *})?
 
 txt {*
-  prints out 
+  then @{ML SUBPROOF} prints out 
 
-  \begin{center}
+  \begin{quote}\small
   \begin{tabular}{ll}
   params:     & @{term x}, @{term y}\\
   schematics: & @{term z}\\
@@ -276,36 +341,85 @@
   concl:      & @{term "C (z y) x"}\\
   prems:      & @{term "A x y"}, @{term "B y x"}
   \end{tabular}
-  \end{center}
+  \end{quote}
 *}
 (*<*)oops(*>*)
 
+text {*
+  where we now also have @{term "B y x"} as assumption.
+
+  One convenience of @{ML SUBPROOF} is that we can apply assumption
+  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}:
+*}
+
+lemma shows "\<And>x y. \<lbrakk>B x y; A x y; C x y\<rbrakk> \<Longrightarrow> A x y"
+apply(tactic 
+       {* SUBPROOF (fn {prems, ...} => resolve_tac prems 1) @{context} 1 *})
+txt{* yields
+      @{subgoals [display]} *}
+(*<*)oops(*>*)
+
 
 text {*
-  @{ML PRIMITIVE}? @{ML SUBGOAL} see page 32 in ref
+  The restriction in this tactic is that it cannot instantiate any
+  schematic variables. This might be seen as a defect, but is actually
+  an advantage in the situations for which @{ML SUBPROOF} was designed: 
+  the reason is that instantiation of schematic variables can potentially 
+  has affect several goals and can render them unprovable.  
+
+  A similar but less powerful function is @{ML SUBGOAL}. It allows you to 
+  inspect a subgoal specified by a number. 
 *}
 
-text {* 
-  @{ML all_tac} @{ML no_tac}
+ML %linenumbers{*fun select_tac (t,i) =
+  case t of
+     @{term "Trueprop"} $ 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
+   | _ => no_tac*}
+
+lemma shows "A \<and> B" "A \<longrightarrow> B" "\<forall>x. C x"
+apply(tactic {* SUBGOAL select_tac 1 *})
+apply(tactic {* SUBGOAL select_tac 3 *})
+apply(tactic {* SUBGOAL select_tac 4 *})
+txt{* @{subgoals [display]} *}
+(*<*)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.
+
+  A variant of @{ML SUBGOAL} is @{ML CSUBGOAL} which allows access to the goal
+  as @{ML_type cterm} instead of a @{ML_type term}.
 *}
 
+
 section {* Operations on Tactics *}
 
-text {* THEN *}
+text {* @{ML THEN} *}
 
-lemma shows "(True \<and> True) \<and> False"
-apply(tactic {* (rtac @{thm conjI} 1) THEN (rtac @{thm conjI} 1) *})
+lemma shows "(Foo \<and> Bar) \<and> False"
+apply(tactic {* (rtac @{thm conjI} 1) 
+                 THEN (rtac @{thm conjI} 1) *})
 txt {* @{subgoals [display]} *}
 (*<*)oops(*>*)
 
-lemma shows "True \<and> False"
-apply(tactic {* (rtac @{thm disjI1} 1) ORELSE (rtac @{thm conjI} 1) *})
+ML{*val orelse_xmp = (rtac @{thm disjI1} ORELSE' rtac @{thm conjI})*}
+
+lemma shows "True \<and> False" and "Foo \<or> Bar"
+apply(tactic {* orelse_xmp 1 *})
+apply(tactic {* orelse_xmp 3 *})
 txt {* @{subgoals [display]} *}
 (*<*)oops(*>*)
 
 
 text {*
-  @{ML EVERY} @{ML REPEAT} 
+  @{ML EVERY} @{ML REPEAT} @{ML DETERM}
 
   @{ML rewrite_goals_tac}
   @{ML cut_facts_tac}




