
diff -r 123401a5c8e9 -r 5e309df58557 CookBook/Tactical.thy
--- a/CookBook/Tactical.thy	Fri Feb 06 06:19:52 2009 +0000
+++ b/CookBook/Tactical.thy	Sat Feb 07 12:05:02 2009 +0000
@@ -6,20 +6,22 @@
 
 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
-  that help with 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 @{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.
+
 *}
 
-section {* Tactical Reasoning *}
+section {* Basics of Reasoning with Tactics*}
 
 text {*
-  To see how tactics work, let us first transcribe a simple @{text apply}-style proof 
+  To see how tactics work, let us first transcribe a simple \isacommand{apply}-style proof 
   into ML. Consider the following proof.
 *}
 
@@ -57,7 +59,10 @@
   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.
+  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.
 
   \begin{readmore}
   To learn more about the function @{ML Goal.prove} see \isccite{sec:results}
@@ -75,8 +80,8 @@
   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, it will often be necessary 
-  to test a tactic on examples. This can be conveniently 
+  During the development of automatic proof procedures, you will often find it 
+  necessary to test a tactic on examples. This can be conveniently 
   done with the command \isacommand{apply}@{text "(tactic \<verbopen> \<dots> \<verbclose>)"}. 
   Consider the following sequence of tactics
 *}
@@ -96,13 +101,15 @@
 
 text {*
   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.
+  you can call from the user level of Isabelle the tactic @{ML foo_tac} or 
+  any other function that returns a tactic.
 
-  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
-  subgoal. This is sometimes wanted, but usually not. To avoid the explicit numbering in the 
-  tactic, you can write
+  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
 *}
 
 ML{*val foo_tac' = 
@@ -114,9 +121,9 @@
 
 text {* 
   and then give the number for the subgoal explicitly when the tactic is
-  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.
+  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.
 *}
 
 lemma "P1 \<or> Q1 \<Longrightarrow> Q1 \<or> P1"
@@ -126,11 +133,11 @@
 done
 
 text {*
-  (FIXME: maybe add something about how each goal state is interpreted
-  as a theorem)
+  This kind of addressing is more difficult to achieve when the goal is 
+  hard-coded inside the tactic.
 
-  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
+  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:
 
   \begin{isabelle}
@@ -140,12 +147,29 @@
 
   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
+  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: 
-  tactics should not raise exceptions willy-nilly.
+  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
+*}
+
+ML{*fun no_tac thm = Seq.empty*}
+
+text {*
+  which means @{ML no_tac} always fails. The second returns the given theorem wrapped 
+  as a single member sequence. It is defined as
+*}
+
+ML{*fun all_tac thm = Seq.single thm*}
+
+text {*
+  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 
   of Isabelle when using the command \isacommand{back}. For instance in the 
@@ -158,10 +182,12 @@
 back
 done
 
+
 text {*
   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.
+  second assumption. In more interesting situations, different possibilities 
+  can lead to different proofs and even often need to be explored when
+  a first proof attempt is unsuccessful.
   
   \begin{readmore}
   See @{ML_file "Pure/General/seq.ML"} for the implementation of lazy
@@ -170,9 +196,95 @@
   instead.
   \end{readmore}
 
+  For a beginner it might be surprising that tactics, which transform
+  one proof state to the next, are functions from theorems to theorem 
+  (sequences). The surprise resolves by knowing that every 
+  proof state is indeed a theorem. To shed more light on this,
+  let us modify the code of @{ML all_tac} to obtain the following
+  tactic
+*}
+
+ML{*fun my_print_tac ctxt thm =
+ let
+   val _ = warning (str_of_thm ctxt thm)
+ in 
+   Seq.single thm
+ end*}
+
+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 our @{ML my_print_tac}.
+*}
+
+lemma shows "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B"
+apply(tactic {* my_print_tac @{context} *})
+
+txt{* \small 
+      \begin{tabular}{@ {}l@ {}p{0.7\textwidth}@ {}}
+      \begin{minipage}[t]{0.3\textwidth}
+      @{subgoals [display]} 
+      \end{minipage} &
+      \hfill@{text "(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B)"}
+      \end{tabular}
 *}
 
-section {* Basic Tactics *}
+apply(rule conjI)
+apply(tactic {* my_print_tac @{context} *})
+
+txt{* \small 
+      \begin{tabular}{@ {}l@ {}p{0.76\textwidth}@ {}}
+      \begin{minipage}[t]{0.26\textwidth}
+      @{subgoals [display]} 
+      \end{minipage} &
+      \hfill@{text "(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> B) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B)"}
+      \end{tabular}
+*}
+
+apply(assumption)
+apply(tactic {* my_print_tac @{context} *})
+
+txt{* \small 
+      \begin{tabular}{@ {}l@ {}p{0.7\textwidth}@ {}}
+      \begin{minipage}[t]{0.3\textwidth}
+      @{subgoals [display]} 
+      \end{minipage} &
+      \hfill@{text "(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> B) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B)"}
+      \end{tabular}
+*}
+
+apply(assumption)
+apply(tactic {* my_print_tac @{context} *})
+
+txt{* \small 
+      \begin{tabular}{@ {}l@ {}p{0.7\textwidth}@ {}}
+      \begin{minipage}[t]{0.3\textwidth}
+      @{subgoals [display]} 
+      \end{minipage} &
+      \hfill@{text "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B"}
+      \end{tabular}
+*}
+
+done
+
+text {*
+  As can be seen, internally every goal state is an implication of the form
+
+  @{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. Since the goal @{term C} can potentially be an implication, 
+  there is a protector (invisible in the print out above) wrapped around 
+  it. This prevents that premises 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. 
+ 
+*}
+
+section {* Simple Tactics *}
 
 text {*
   As seen above, the function @{ML atac} corresponds to the assumption tactic.
@@ -184,7 +296,7 @@
 
 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}, 
+  to @{text rule}, @{text drule}, @{text erule} and @{text frule}, 
   respectively. Below are three examples with the resulting goal state. How
   they work should therefore be self-explanatory.  
 *}
@@ -247,7 +359,7 @@
 (*<*)oops(*>*)
 
 text {*
-  Also for useful for debugging, but not exclusively, are the tactics @{ML all_tac} and
+  Also for useful for debugging purposes 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.
 
@@ -274,9 +386,9 @@
  
     val _ = (warning ("params: " ^ str_of_params);
              warning ("schematics: " ^ str_of_schms);
-             warning ("asms: " ^ str_of_asms);
-             warning ("concl: " ^ str_of_concl);
-             warning ("prems: " ^ str_of_prems))
+             warning ("assumptions: " ^ str_of_asms);
+             warning ("conclusion: " ^ str_of_concl);
+             warning ("premises: " ^ str_of_prems))
   in
     no_tac 
   end*}
@@ -303,11 +415,11 @@
 
   \begin{quote}\small
   \begin{tabular}{ll}
-  params:     & @{term x}, @{term y}\\
-  schematics: & @{term z}\\
-  asms:       & @{term "A x y"}\\
-  concl:      & @{term "B y x \<longrightarrow> C (z y) x"}\\
-  prems:      & @{term "A x y"}
+  params:      & @{term x}, @{term y}\\
+  schematics:  & @{term z}\\
+  assumptions: & @{term "A x y"}\\
+  conclusion:  & @{term "B y x \<longrightarrow> C (z y) x"}\\
+  premises:    & @{term "A x y"}
   \end{tabular}
   \end{quote}
 
@@ -335,11 +447,11 @@
 
   \begin{quote}\small
   \begin{tabular}{ll}
-  params:     & @{term x}, @{term y}\\
-  schematics: & @{term z}\\
-  asms:       & @{term "A x y"}, @{term "B y x"}\\
-  concl:      & @{term "C (z y) x"}\\
-  prems:      & @{term "A x y"}, @{term "B y x"}
+  params:      & @{term x}, @{term y}\\
+  schematics:  & @{term z}\\
+  assumptions: & @{term "A x y"}, @{term "B y x"}\\
+  conclusion:  & @{term "C (z y) x"}\\
+  premises:    & @{term "A x y"}, @{term "B y x"}
   \end{tabular}
   \end{quote}
 *}
@@ -428,35 +540,6 @@
   @{ML resolve_tac}
 *}
 
-
-
-text {*
-
-
-  A goal (or goal state) is a special @{ML_type thm}, which by
-  convention is an implication of the form:
-
-  @{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 open 
-  subgoals. 
-  Since the goal @{term C} can potentially be an implication, there is a
-  @{text "#"} wrapped around it, which prevents that premises are 
-  misinterpreted as open subgoals. The wrapper @{text "# :: prop \<Rightarrow>
-  prop"} is just the identity function and used as a syntactic marker. 
-  
- 
-
- 
-
-  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. 
- 
-
-
-*}
-
 section {* Structured Proofs *}
 
 lemma True
@@ -495,4 +578,5 @@
 *}
 
 
+
 end
\ No newline at end of file




