diff -r 8939b8fd8603 -r 069d525f8f1d ProgTutorial/Tactical.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ProgTutorial/Tactical.thy	Thu Mar 19 13:28:16 2009 +0100
@@ -0,0 +1,2121 @@
+theory Tactical
+imports Base FirstSteps
+begin
+
+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 \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.
+
+*}
+
+section {* Basics of Reasoning with Tactics*}
+
+text {*
+  To see how tactics work, let us first transcribe a simple \isacommand{apply}-style proof 
+  into ML. Suppose the following proof.
+*}
+
+lemma disj_swap: "P \<or> Q \<Longrightarrow> Q \<or> P"
+apply(erule disjE)
+apply(rule disjI2)
+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
+      THEN rtac @{thm disjI2} 1
+      THEN atac 1
+      THEN rtac @{thm disjI1} 1
+      THEN atac 1)
+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} 
+  (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} in the code above correspond to 
+  @{text erule}, @{text rule} and @{text assumption}, respectively. 
+  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"}.  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, and Chapter 3 in the Isabelle/Isar Implementation Manual. 
+  \end{readmore}
+
+  Note that in the code above we use 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 where there are no ML-binding obtain
+  the theorem dynamically using the function @{ML thm}; for example 
+  \mbox{@{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 
+  done with the command \isacommand{apply}@{text "(tactic \<verbopen> \<dots> \<verbclose>)"}. 
+  Consider the following sequence of tactics
+*}
+
+ML{*val foo_tac = 
+      (etac @{thm disjE} 1
+       THEN rtac @{thm disjI2} 1
+       THEN atac 1
+       THEN rtac @{thm disjI1} 1
+       THEN atac 1)*}
+
+text {* and the Isabelle proof: *}
+
+lemma "P \<or> Q \<Longrightarrow> Q \<or> P"
+apply(tactic {* foo_tac *})
+done
+
+text {*
+  By using @{text "tactic \<verbopen> \<dots> \<verbclose>"} you can call from the 
+  user-level of Isabelle the tactic @{ML foo_tac} or 
+  any other function that returns a tactic.
+
+  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 hard-coding
+  of goals is sometimes wanted, but usually it is not. To avoid the explicit numbering, 
+  you can write\label{tac:footacprime}
+*}
+
+ML{*val foo_tac' = 
+      (etac @{thm disjE} 
+       THEN' rtac @{thm disjI2} 
+       THEN' atac 
+       THEN' rtac @{thm disjI1} 
+       THEN' atac)*}
+
+text {* 
+  and then give the number for the subgoal explicitly when the tactic is
+  called. So in the next proof you can first discharge the second subgoal, and
+  subsequently the first.
+*}
+
+lemma "P1 \<or> Q1 \<Longrightarrow> Q1 \<or> P1"
+   and "P2 \<or> Q2 \<Longrightarrow> Q2 \<or> P2"
+apply(tactic {* foo_tac' 2 *})
+apply(tactic {* foo_tac' 1 *})
+done
+
+text {*
+  This kind of addressing is more difficult to achieve when the goal is 
+  hard-coded inside the tactic. For most operators that combine 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 these tactics return the error message:
+
+  \begin{isabelle}
+  @{text "*** empty result sequence -- proof command failed"}\\
+  @{text "*** At command \"apply\"."}
+  \end{isabelle}
+
+  This means they failed. The reason for this error message is that tactics 
+  are functions mapping a goal state to a (lazy) sequence of successor states. 
+  Hence the type of a tactic is:
+*}
+  
+ML{*type tactic = thm -> thm Seq.seq*}
+
+text {*
+  By convention, if a tactic fails, then it should return the empty sequence. 
+  Therefore, if you write your own tactics, they  should not raise exceptions 
+  willy-nilly; only in very grave failure situations should a tactic raise the 
+  exception @{text THM}.
+
+  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 
+  in 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 goal 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'}: either using the first assumption or the second.
+*}
+
+lemma "\<lbrakk>P \<or> Q; P \<or> Q\<rbrakk> \<Longrightarrow> Q \<or> P"
+apply(tactic {* foo_tac' 1 *})
+back
+done
+
+
+text {*
+  By using \isacommand{back}, we construct the proof that uses the
+  second assumption. While in the proof above, it does not really matter which 
+  assumption is used, in more interesting cases provability might depend
+  on exploring different possibilities.
+  
+  \begin{readmore}
+  See @{ML_file "Pure/General/seq.ML"} for the implementation of lazy
+  sequences. In day-to-day Isabelle programming, however, one rarely 
+  constructs sequences explicitly, but uses the predefined tactics and 
+  tactic combinators instead.
+  \end{readmore}
+
+  It might be surprising that tactics, which transform
+  one goal state to the next, are functions from theorems to theorem 
+  (sequences). The surprise resolves by knowing that every 
+  goal 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_raw {*
+  \begin{figure}[p]
+  \begin{boxedminipage}{\textwidth}
+  \begin{isabelle}
+*}
+lemma shows "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B" 
+apply(tactic {* my_print_tac @{context} *})
+
+txt{* \begin{minipage}{\textwidth}
+      @{subgoals [display]} 
+      \end{minipage}\medskip      
+
+      \begin{minipage}{\textwidth}
+      \small\colorbox{gray!20}{
+      \begin{tabular}{@ {}l@ {}}
+      internal goal state:\\
+      @{text "(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B)"}
+      \end{tabular}}
+      \end{minipage}\medskip
+*}
+
+apply(rule conjI)
+apply(tactic {* my_print_tac @{context} *})
+
+txt{* \begin{minipage}{\textwidth}
+      @{subgoals [display]} 
+      \end{minipage}\medskip
+
+      \begin{minipage}{\textwidth}
+      \small\colorbox{gray!20}{
+      \begin{tabular}{@ {}l@ {}}
+      internal goal state:\\
+      @{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}}
+      \end{minipage}\medskip
+*}
+
+apply(assumption)
+apply(tactic {* my_print_tac @{context} *})
+
+txt{* \begin{minipage}{\textwidth}
+      @{subgoals [display]} 
+      \end{minipage}\medskip
+
+      \begin{minipage}{\textwidth}
+      \small\colorbox{gray!20}{
+      \begin{tabular}{@ {}l@ {}}
+      internal goal state:\\
+      @{text "(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> B) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B)"}
+      \end{tabular}}
+      \end{minipage}\medskip
+*}
+
+apply(assumption)
+apply(tactic {* my_print_tac @{context} *})
+
+txt{* \begin{minipage}{\textwidth}
+      @{subgoals [display]} 
+      \end{minipage}\medskip 
+  
+      \begin{minipage}{\textwidth}
+      \small\colorbox{gray!20}{
+      \begin{tabular}{@ {}l@ {}}
+      internal goal state:\\
+      @{text "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B"}
+      \end{tabular}}
+      \end{minipage}\medskip   
+   *}
+done
+text_raw {*  
+  \end{isabelle}
+  \end{boxedminipage}
+  \caption{The figure shows a proof where each intermediate goal state is
+  printed by the Isabelle system and by @{ML my_print_tac}. The latter shows
+  the goal state as represented internally (highlighted boxes). This
+  tactic shows that every goal state in Isabelle is represented by a theorem:
+  when you start the proof of \mbox{@{text "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B"}} the theorem is
+  @{text "(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B)"}; when you finish the proof the
+  theorem is @{text "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B"}.\label{fig:goalstates}}
+  \end{figure}
+*}
+
+
+text {*
+  which prints out the given theorem (using the string-function defined in
+  Section~\ref{sec:printing}) and then behaves like @{ML all_tac}. With this
+  tactic we are in the position to inspect every goal state in a
+  proof. Consider now the proof in Figure~\ref{fig:goalstates}: 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. So after setting up the lemma, the goal state is always of the
+  form @{text "C \<Longrightarrow> (C)"}; when the proof is finished we are left with @{text
+  "(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)"}; however this constant
+  is invisible in the figure). This wrapper prevents that premises of @{text C} are
+  mis-interpreted 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. If you use the predefined tactics, which we describe in the next
+  section, this will always be the case.
+ 
+  \begin{readmore}
+  For more information about the internals of goals see \isccite{sec:tactical-goals}.
+  \end{readmore}
+
+*}
+
+section {* Simple Tactics *}
+
+text {*
+  Let us start with explaining the simple tactic @{ML print_tac}, which is quite useful 
+  for low-level debugging of tactics. It just prints out a message and the current 
+  goal state. Unlike @{ML my_print_tac} shown earlier, it prints the goal state 
+  as the user would see it.  For example, processing the proof
+*}
+ 
+lemma shows "False \<Longrightarrow> True"
+apply(tactic {* print_tac "foo message" *})
+txt{*gives:\medskip
+
+     \begin{minipage}{\textwidth}\small
+     @{text "foo message"}\\[3mm] 
+     @{prop "False \<Longrightarrow> True"}\\
+     @{text " 1. False \<Longrightarrow> True"}\\
+     \end{minipage}
+   *}
+(*<*)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"
+apply(tactic {* atac 1 *})
+txt{*\begin{minipage}{\textwidth}
+     @{subgoals [display]}
+     \end{minipage}*}
+(*<*)oops(*>*)
+
+text {*
+  Similarly, @{ML rtac}, @{ML dtac}, @{ML etac} and @{ML ftac} correspond
+  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 *})
+txt{*\begin{minipage}{\textwidth}
+     @{subgoals [display]}
+     \end{minipage}*}
+(*<*)oops(*>*)
+
+lemma shows "P \<and> Q \<Longrightarrow> False"
+apply(tactic {* etac @{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 *})
+txt{*\begin{minipage}{\textwidth}
+     @{subgoals [display]}
+     \end{minipage}*}
+(*<*)oops(*>*)
+
+text {*
+  Note the number in each tactic call. Also as mentioned in the previous section, most 
+  basic tactics take such a number as argument: this argument addresses the subgoal 
+  the tacics are analysing. In the proof below, we first split up the conjunction in  
+  the second subgoal by focusing on this subgoal first.
+*}
+
+lemma shows "Foo" and "P \<and> Q"
+apply(tactic {* rtac @{thm conjI} 2 *})
+txt {*\begin{minipage}{\textwidth}
+      @{subgoals [display]}
+      \end{minipage}*}
+(*<*)oops(*>*)
+
+text {*
+  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}]*}
+
+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{*\begin{minipage}{\textwidth}
+     @{subgoals [display]} 
+     \end{minipage}*}
+(*<*)oops(*>*)
+
+text {* 
+  Similar versions taking a list of theorems exist for the tactics 
+  @{ML dtac} (@{ML dresolve_tac}), @{ML etac} (@{ML eresolve_tac}) and so on.
+
+
+  Another simple tactic is @{ML cut_facts_tac}. It inserts a list of theorems
+  into the assumptions of the current goal state. For example
+*}
+
+lemma shows "True \<noteq> False"
+apply(tactic {* cut_facts_tac [@{thm True_def}, @{thm False_def}] 1 *})
+txt{*produces the goal state\medskip
+
+     \begin{minipage}{\textwidth}
+     @{subgoals [display]} 
+     \end{minipage}*}
+(*<*)oops(*>*)
+
+text {*
+  Since rules are applied using higher-order unification, an automatic proof
+  procedure might become too fragile, if it just applies inference rules as 
+  shown above. The reason is that a number of rules introduce meta-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 *})
+txt{*\begin{minipage}{\textwidth}
+     @{subgoals [display]} 
+     \end{minipage}*}
+(*<*)oops(*>*)
+
+text {*
+  where the application of rule @{text bspec} generates two subgoals involving the
+  meta-variable @{text "?x"}. Now, if you are not careful, tactics 
+  applied to the first subgoal might instantiate this meta-variable in such a 
+  way that the second subgoal becomes unprovable. If it is clear what the @{text "?x"}
+  should be, then this situation can be avoided by introducing a more
+  constraint version of the @{text bspec}-rule. Such constraints can be given by
+  pre-instantiating theorems with other theorems. One function to do this is
+  @{ML RS}
+  
+  @{ML_response_fake [display,gray]
+  "@{thm disjI1} RS @{thm conjI}" "\<lbrakk>?P1; ?Q\<rbrakk> \<Longrightarrow> (?P1 \<or> ?Q1) \<and> ?Q"}
+
+  which in the example instantiates the first premise of the @{text conjI}-rule 
+  with the rule @{text disjI1}. If the instantiation is impossible, as in the 
+  case of
+
+  @{ML_response_fake_both [display,gray]
+  "@{thm conjI} RS @{thm mp}" 
+"*** Exception- THM (\"RSN: no unifiers\", 1, 
+[\"\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q\", \"\<lbrakk>?P \<longrightarrow> ?Q; ?P\<rbrakk> \<Longrightarrow> ?Q\"]) raised"}
+
+  then the function raises an exception. The function @{ML RSN} is similar to @{ML RS}, but 
+  takes an additional number as argument that makes explicit which premise 
+  should be instantiated. 
+
+  To improve readability of the theorems we produce below, we shall use the
+  function @{ML no_vars} from Section~\ref{sec:printing}, which transforms
+  schematic variables into free ones.  Using this function for the first @{ML
+  RS}-expression above produces the more readable result:
+
+  @{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 of a theorem, 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 in the code below,
+  every theorem in the second list is instantiated with every 
+  theorem in the first.
+
+  @{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 on the ML-level involve elaborate operations on assumptions and 
+  @{text "\<And>"}-quantified variables. To do such operations using the basic tactics 
+  shown so far 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 goal state to a record. 
+  To see what happens, assume the function defined in Figure~\ref{fig:sptac}, which
+  takes a record and just prints out the content of this record (using the 
+  string transformation functions from in Section~\ref{sec:printing}). Consider
+  now the proof:
+*}
+
+text_raw{*
+\begin{figure}[t]
+\begin{minipage}{\textwidth}
+\begin{isabelle}
+*}
+ML{*fun sp_tac {prems, params, asms, concl, context, schematics} = 
+let 
+  val str_of_params = str_of_cterms context params
+  val str_of_asms = str_of_cterms context asms
+  val str_of_concl = str_of_cterm context concl
+  val str_of_prems = str_of_thms context prems   
+  val str_of_schms = str_of_cterms context (snd schematics)    
+ 
+  val _ = (warning ("params: " ^ str_of_params);
+           warning ("schematics: " ^ str_of_schms);
+           warning ("assumptions: " ^ str_of_asms);
+           warning ("conclusion: " ^ str_of_concl);
+           warning ("premises: " ^ str_of_prems))
+in
+  no_tac 
+end*}
+text_raw{*
+\end{isabelle}
+\end{minipage}
+\caption{A function that prints out the various parameters provided by the tactic
+ @{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}
+*}
+
+
+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 {*
+  The tactic produces the following printout:
+
+  \begin{quote}\small
+  \begin{tabular}{ll}
+  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}
+
+  Notice in the actual output the brown colour of the variables @{term x} and 
+  @{term y}. Although they are parameters in the original goal, they are fixed inside
+  the subproof. By convention these fixed variables are printed in brown colour.
+  Similarly the schematic variable @{term z}. The assumption, or premise, 
+  @{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 [quotes] "?"} to the
+  \isacommand{apply}-command. 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 an 
+  ``empty sequence'' 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 {*
+  then the tactic prints out: 
+
+  \begin{quote}\small
+  \begin{tabular}{ll}
+  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}
+*}
+(*<*)oops(*>*)
+
+text {*
+  Now also @{term "B y x"} is an assumption bound to @{text asms} and @{text prems}.
+
+  One convenience of @{ML SUBPROOF} is that we can apply the assumptions
+  using the usual tactics, because the parameter @{text prems} 
+  contains them as theorems. With this you can easily 
+  implement a tactic that behaves almost like @{ML atac}:
+*}
+
+ML{*val atac' = SUBPROOF (fn {prems, ...} => resolve_tac prems 1)*}
+
+text {*
+  If you apply @{ML atac'} to the next lemma
+*}
+
+lemma shows "\<lbrakk>B x y; A x y; C x y\<rbrakk> \<Longrightarrow> A x y"
+apply(tactic {* atac' @{context} 1 *})
+txt{* it will produce
+      @{subgoals [display]} *}
+(*<*)oops(*>*)
+
+text {*
+  The restriction in this tactic which is not present in @{ML atac} is 
+  that it cannot instantiate any
+  schematic variable. This might be seen as a defect, but it is actually
+  an advantage in the situations for which @{ML SUBPROOF} was designed: 
+  the reason is that, as mentioned before, instantiation of schematic variables can affect 
+  several goals and can render them unprovable. @{ML SUBPROOF} is meant 
+  to avoid this.
+
+  Notice that @{ML atac'} inside @{ML SUBPROOF} calls @{ML resolve_tac} with 
+  the subgoal number @{text "1"} and also the outer call to @{ML SUBPROOF} in 
+  the \isacommand{apply}-step uses @{text "1"}. This is another advantage 
+  of @{ML SUBPROOF}: the addressing  inside it is completely 
+  local to the tactic inside the subproof. It is therefore possible to also apply 
+  @{ML atac'} to the second goal by just writing:
+*}
+
+lemma shows "True" and "\<lbrakk>B x y; A x y; C x y\<rbrakk> \<Longrightarrow> A x y"
+apply(tactic {* atac' @{context} 2 *})
+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}
+
+  Similar but less powerful functions than @{ML SUBPROOF} are @{ML SUBGOAL}
+  and @{ML CSUBGOAL}. They allow you to inspect a given subgoal (the former
+  presents the subgoal as a @{ML_type term}, while the latter as a @{ML_type
+  cterm}). With this 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.\label{tac:selecttac}
+
+*}
+
+ML %linenosgray{*fun select_tac (t, i) =
+  case t of
+     @{term "Trueprop"} $ t' => select_tac (t', i)
+   | @{term "op \<Longrightarrow>"} $ _ $ 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
+   | _ => all_tac*}
+
+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
+  outermost @{term "Trueprop"} in order to get to the connective you like to
+  analyse. Otherwise goals like @{prop "A \<and> B"} are not properly
+  analysed. Similarly with meta-implications in the next line.  While for the
+  first five patterns we can use the @{text "@term"}-antiquotation to
+  construct the patterns, the pattern in Line 8 cannot be constructed in this
+  way. The reason is that an antiquotation would fix the type of the
+  quantified variable. So you really have to construct the pattern using the
+  basic term-constructors. This is not necessary in other cases, because their
+  type is always fixed to function types involving only the type @{typ
+  bool}. (See Section \ref{sec:terms_types_manually} about constructing terms
+  manually.) For the catch-all pattern, we chose to just return @{ML all_tac}. 
+  Consequently, @{ML select_tac} never fails.
+
+
+  Let us now see how to apply this tactic. Consider the four goals:
+*}
+
+
+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 *})
+apply(tactic {* SUBGOAL select_tac 1 *})
+txt{* \begin{minipage}{\textwidth}
+      @{subgoals [display]}
+      \end{minipage} *}
+(*<*)oops(*>*)
+
+text {*
+  where in all but the last the tactic applied an introduction rule. 
+  Note that we applied the tactic to the goals in ``reverse'' order. 
+  This is a trick in order to be independent from the subgoals that are 
+  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 3 *})
+apply(tactic {* SUBGOAL select_tac 4 *})
+apply(tactic {* SUBGOAL select_tac 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, 
+  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
+  connective. These simpler methods use tactic combinators, which we will
+  explain in the next section.
+
+*}
+
+section {* Tactic Combinators *}
+
+text {* 
+  The purpose of tactic combinators is to build compound tactics out of
+  smaller tactics. In the previous section we already used @{ML THEN}, 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 *})
+txt {* \begin{minipage}{\textwidth}
+       @{subgoals [display]} 
+       \end{minipage} *}
+(*<*)oops(*>*)
+
+text {*
+  If you want to avoid the hard-coded subgoal addressing, then you can use
+  the ``primed'' version of @{ML THEN}. For example:
+*}
+
+lemma shows "(Foo \<and> Bar) \<and> False"
+apply(tactic {* (rtac @{thm conjI} THEN' rtac @{thm conjI}) 1 *})
+txt {* \begin{minipage}{\textwidth}
+       @{subgoals [display]} 
+       \end{minipage} *}
+(*<*)oops(*>*)
+
+text {* 
+  Here you only have to specify the subgoal of interest only once and
+  it is consistently applied to the component tactics.
+  For most tactic combinators such a ``primed'' version exists and
+  in what follows we will usually prefer it over the ``unprimed'' one. 
+
+  If there is a list of tactics that should all be tried out in 
+  sequence, you can use the combinator @{ML EVERY'}. For example
+  the function @{ML foo_tac'} from page~\pageref{tac:footacprime} can also 
+  be written as:
+*}
+
+ML{*val foo_tac'' = EVERY' [etac @{thm disjE}, rtac @{thm disjI2}, 
+                        atac, rtac @{thm disjI1}, atac]*}
+
+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"}, 
+  you can also just write
+*}
+
+ML{*val foo_tac1 = EVERY1 [etac @{thm disjE}, rtac @{thm disjI2}, 
+                       atac, rtac @{thm disjI1}, atac]*}
+
+text {*
+  and call @{ML foo_tac1}.  
+
+  With the combinators @{ML THEN'}, @{ML EVERY'} and @{ML EVERY1} it must be
+  guaranteed that all component tactics successfully apply; otherwise the
+  whole tactic will fail. If you rather want to try out a number of tactics,
+  then you can use the combinator @{ML ORELSE'} for two tactics, and @{ML
+  FIRST'} (or @{ML FIRST1}) for a list of tactics. For example, the tactic
+
+*}
+
+ML{*val orelse_xmp = rtac @{thm disjI1} ORELSE' rtac @{thm conjI}*}
+
+text {*
+  will first try out whether rule @{text disjI} applies and after that 
+  @{text conjI}. To see this consider the proof
+*}
+
+lemma shows "True \<and> False" and "Foo \<or> Bar"
+apply(tactic {* orelse_xmp 2 *})
+apply(tactic {* orelse_xmp 1 *})
+txt {* which results in the goal state
+
+       \begin{minipage}{\textwidth}
+       @{subgoals [display]} 
+       \end{minipage}
+*}
+(*<*)oops(*>*)
+
+
+text {*
+  Using @{ML FIRST'} we can simplify our @{ML select_tac} from Page~\pageref{tac:selecttac} 
+  as follows:
+*}
+
+ML{*val select_tac' = FIRST' [rtac @{thm conjI}, rtac @{thm impI}, 
+                          rtac @{thm notI}, rtac @{thm allI}, K all_tac]*}
+
+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 rule applies (we also have to wrap @{ML all_tac} using the 
+  @{ML K}-combinator, because it does not take a subgoal number as argument). You can 
+  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' 3 *})
+apply(tactic {* select_tac' 2 *})
+apply(tactic {* select_tac' 1 *})
+txt{* \begin{minipage}{\textwidth}
+      @{subgoals [display]}
+      \end{minipage} *}
+(*<*)oops(*>*)
+
+text {* 
+  Since such repeated applications of a tactic to the reverse order of 
+  \emph{all} subgoals is quite common, there is the tactic combinator 
+  @{ML ALLGOALS} 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' *})
+txt{* \begin{minipage}{\textwidth}
+      @{subgoals [display]}
+      \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, 
+  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 
+  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
+  succeed on goals where it can make progress. But for the sake of argument,
+  let us suppose that this deletion is \emph{not} an option. In such cases, you can
+  use the combinator @{ML CHANGED} to make sure the subgoal has been changed
+  by the tactic. Because now
+
+*}
+
+lemma shows "E \<Longrightarrow> F"
+apply(tactic {* CHANGED (select_tac' 1) *})(*<*)?(*>*)
+txt{* gives the error message:
+  \begin{isabelle}
+  @{text "*** empty result sequence -- proof command failed"}\\
+  @{text "*** At command \"apply\"."}
+  \end{isabelle} 
+*}(*<*)oops(*>*)
+
+
+text {*
+  We can further extend @{ML select_tac'} so that it not just applies to the topmost
+  connective, but also to the ones immediately ``underneath'', i.e.~analyse the goal 
+  completely. For this you can use the tactic combinator @{ML REPEAT}. As an example 
+  suppose the following tactic
+*}
+
+ML{*val repeat_xmp = REPEAT (CHANGED (select_tac' 1)) *}
+
+text {* which applied to the proof *}
+
+lemma shows "((\<not>A) \<and> (\<forall>x. B x)) \<and> (C \<longrightarrow> D)"
+apply(tactic {* repeat_xmp *})
+txt{* produces
+
+      \begin{minipage}{\textwidth}
+      @{subgoals [display]}
+      \end{minipage} *}
+(*<*)oops(*>*)
+
+text {*
+  Here it is crucial that @{ML select_tac'} is prefixed with @{ML CHANGED}, 
+  because otherwise @{ML REPEAT} runs into an infinite loop (it applies the
+  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}, then you 
+  need to implement it as
+*}
+
+ML{*val repeat_xmp' = 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}
+  and @{ML repeat_xmp'} 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
+*}
+
+ML{*val repeat_all_new_xmp = REPEAT_ALL_NEW (CHANGED o select_tac')*}
+
+text {* 
+  you see that the following goal
+*}
+
+lemma shows "((\<not>A) \<and> (\<forall>x. B x)) \<and> (C \<longrightarrow> D)"
+apply(tactic {* repeat_all_new_xmp 1 *})
+txt{* \begin{minipage}{\textwidth}
+      @{subgoals [display]}
+      \end{minipage} *}
+(*<*)oops(*>*)
+
+text {*
+  is completely analysed according to the theorems we chose to
+  include in @{ML select_tac'}. 
+
+  Recall that tactics produce a lazy sequence of successor goal states. These
+  states can be explored using the command \isacommand{back}. For example
+
+*}
+
+lemma "\<lbrakk>P1 \<or> Q1; P2 \<or> Q2\<rbrakk> \<Longrightarrow> R"
+apply(tactic {* etac @{thm disjE} 1 *})
+txt{* applies the rule to the first assumption yielding the goal state:\smallskip
+      
+      \begin{minipage}{\textwidth}
+      @{subgoals [display]}
+      \end{minipage}\smallskip 
+
+      After typing
+  *}
+(*<*)
+oops
+lemma "\<lbrakk>P1 \<or> Q1; P2 \<or> Q2\<rbrakk> \<Longrightarrow> R"
+apply(tactic {* etac @{thm disjE} 1 *})
+(*>*)
+back
+txt{* the rule now applies to the second assumption.\smallskip
+
+      \begin{minipage}{\textwidth}
+      @{subgoals [display]}
+      \end{minipage} *}
+(*<*)oops(*>*)
+
+text {*
+  Sometimes this leads to confusing behaviour of tactics and also has
+  the potential to explode the search space for tactics.
+  These problems can be avoided by prefixing the tactic with the tactic 
+  combinator @{ML DETERM}.
+*}
+
+lemma "\<lbrakk>P1 \<or> Q1; P2 \<or> Q2\<rbrakk> \<Longrightarrow> R"
+apply(tactic {* DETERM (etac @{thm disjE} 1) *})
+txt {*\begin{minipage}{\textwidth}
+      @{subgoals [display]}
+      \end{minipage} *}
+(*<*)oops(*>*)
+text {*
+  This combinator will prune the search space to just the first successful application.
+  Attempting to apply \isacommand{back} in this goal states gives the
+  error message:
+
+  \begin{isabelle}
+  @{text "*** back: no alternatives"}\\
+  @{text "*** At command \"back\"."}
+  \end{isabelle}
+
+  \begin{readmore}
+  Most tactic combinators described in this section are defined in @{ML_file "Pure/tctical.ML"}.
+  \end{readmore}
+
+*}
+
+section {* Simplifier Tactics *}
+
+text {*
+  A lot of convenience in the reasoning with Isabelle derives from its
+  powerful simplifier. The power of simplifier is a strength and a weakness at
+  the same time, because you can easily make the simplifier to run into a  loop and its
+  behaviour can be difficult to predict. There is also a multitude
+  of options that you can configurate to control the behaviour of the simplifier. 
+  We describe some of them in this and the next section.
+
+  There are the following five main tactics behind 
+  the simplifier (in parentheses is their user-level counterpart):
+
+  \begin{isabelle}
+  \begin{center}
+  \begin{tabular}{l@ {\hspace{2cm}}l}
+   @{ML simp_tac}            & @{text "(simp (no_asm))"} \\
+   @{ML asm_simp_tac}        & @{text "(simp (no_asm_simp))"} \\
+   @{ML full_simp_tac}       & @{text "(simp (no_asm_use))"} \\
+   @{ML asm_lr_simp_tac}     & @{text "(simp (asm_lr))"} \\
+   @{ML asm_full_simp_tac}   & @{text "(simp)"}
+  \end{tabular}
+  \end{center}
+  \end{isabelle}
+
+  All of the tactics take a simpset and an interger as argument (the latter as usual 
+  to specify  the goal to be analysed). So the proof
+*}
+
+lemma "Suc (1 + 2) < 3 + 2"
+apply(simp)
+done
+
+text {*
+  corresponds on the ML-level to the tactic
+*}
+
+lemma "Suc (1 + 2) < 3 + 2"
+apply(tactic {* asm_full_simp_tac @{simpset} 1 *})
+done
+
+text {*
+  If the simplifier cannot make any progress, then it leaves the goal unchanged,
+  i.e.~does not raise any error message. That means if you use it to unfold a 
+  definition for a constant and this constant is not present in the goal state, 
+  you can still safely apply the simplifier.
+
+  When using the simplifier, the crucial information you have to provide is
+  the simpset. If this information is not handled with care, then the
+  simplifier can easily run into a loop. Therefore a good rule of thumb is to
+  use simpsets that are as minimal as possible. It might be surprising that a
+  simpset is more complex than just a simple collection of theorems used as
+  simplification rules. One reason for the complexity is that the simplifier
+  must be able to rewrite inside terms and should also be able to rewrite
+  according to rules that have precoditions.
+
+
+  The rewriting inside terms requires congruence rules, which
+  are meta-equalities typical of the form
+
+  \begin{isabelle}
+  \begin{center}
+  \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"}. 
+  Every simpset contains only
+  one concruence 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.
+
+
+  The rewriting with rules involving preconditions requires what is in
+  Isabelle called a subgoaler, a solver and a looper. These can be arbitrary
+  tactics that can be installed in a simpset and which are called during
+  various stages during simplification. However, simpsets also include
+  simprocs, which can produce rewrite rules on demand (see next
+  section). Another component are split-rules, which can simplify for example
+  the ``then'' and ``else'' branches of if-statements under the corresponding
+  precoditions.
+
+
+  \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  "Provers/splitter.ML"}.
+  \end{readmore}
+
+  \begin{readmore}
+  FIXME: Find the right place Discrimination nets are implemented
+  in @{ML_file "Pure/net.ML"}.
+  \end{readmore}
+
+  The most common combinators to modify simpsets are
+
+  \begin{isabelle}
+  \begin{tabular}{ll}
+  @{ML addsimps}   & @{ML delsimps}\\
+  @{ML addcongs}   & @{ML delcongs}\\
+  @{ML addsimprocs} & @{ML delsimprocs}\\
+  \end{tabular}
+  \end{isabelle}
+
+  (FIXME: What about splitters? @{ML addsplits}, @{ML delsplits})
+*}
+
+text_raw {*
+\begin{figure}[t]
+\begin{minipage}{\textwidth}
+\begin{isabelle}*}
+ML{*fun print_ss ctxt ss =
+let
+  val {simps, congs, procs, ...} = MetaSimplifier.dest_ss ss
+
+  fun name_thm (nm, thm) =
+      "  " ^ nm ^ ": " ^ (str_of_thm ctxt thm)
+  fun name_ctrm (nm, ctrm) =
+      "  " ^ nm ^ ": " ^ (str_of_cterms ctxt ctrm)
+
+  val s1 = ["Simplification rules:"]
+  val s2 = map name_thm simps
+  val s3 = ["Congruences rules:"]
+  val s4 = map name_thm congs
+  val s5 = ["Simproc patterns:"]
+  val s6 = map name_ctrm procs
+in
+  (s1 @ s2 @ s3 @ s4 @ s5 @ s6) 
+     |> separate "\n"
+     |> implode
+     |> warning
+end*}
+text_raw {* 
+\end{isabelle}
+\end{minipage}
+\caption{The function @{ML MetaSimplifier.dest_ss} returns a record containing
+  all printable information stored in a simpset. We are here only interested in the 
+  simplifcation rules, congruence rules and simprocs.\label{fig:printss}}
+\end{figure} *}
+
+text {* 
+  To see how they work, consider the function in Figure~\ref{fig:printss}, which
+  prints out some parts of a simpset. If you use it to print out the components of the
+  empty simpset, i.e.~ @{ML empty_ss}
+  
+  @{ML_response_fake [display,gray]
+  "print_ss @{context} empty_ss"
+"Simplification rules:
+Congruences rules:
+Simproc patterns:"}
+
+  you can see it contains nothing. This simpset is usually not useful, except as a 
+  building block to build bigger simpsets. For example you can add to @{ML empty_ss} 
+  the simplification rule @{thm [source] Diff_Int} as follows:
+*}
+
+ML{*val ss1 = empty_ss addsimps [@{thm Diff_Int} RS @{thm eq_reflection}] *}
+
+text {*
+  Printing then out the components of the simpset gives:
+
+  @{ML_response_fake [display,gray]
+  "print_ss @{context} ss1"
+"Simplification rules:
+  ??.unknown: A - B \<inter> C \<equiv> A - B \<union> (A - C)
+Congruences rules:
+Simproc patterns:"}
+
+  (FIXME: Why does it print out ??.unknown)
+
+  Adding also the congruence rule @{thm [source] UN_cong} 
+*}
+
+ML{*val ss2 = ss1 addcongs [@{thm UN_cong} RS @{thm eq_reflection}] *}
+
+text {*
+  gives
+
+  @{ML_response_fake [display,gray]
+  "print_ss @{context} ss2"
+"Simplification rules:
+  ??.unknown: A - B \<inter> C \<equiv> A - B \<union> (A - C)
+Congruences rules:
+  UNION: \<lbrakk>A = B; \<And>x. x \<in> B \<Longrightarrow> C x = D x\<rbrakk> \<Longrightarrow> \<Union>x\<in>A. C x \<equiv> \<Union>x\<in>B. D x
+Simproc patterns:"}
+
+  Notice that we had to add these lemmas as meta-equations. The @{ML empty_ss} 
+  expects this form of the simplification and congruence rules. However, even 
+  when adding these lemmas to @{ML empty_ss} we do not end up with anything useful yet.
+
+  In the context of HOL, the first really useful simpset is @{ML HOL_basic_ss}. While
+  printing out the components of this simpset
+
+  @{ML_response_fake [display,gray]
+  "print_ss @{context} HOL_basic_ss"
+"Simplification rules:
+Congruences rules:
+Simproc patterns:"}
+
+  also produces ``nothing'', the printout is misleading. In fact
+  the @{ML HOL_basic_ss} is setup so that it can solve goals of the
+  form  
+
+  \begin{isabelle}
+  @{thm TrueI}, @{thm refl[no_vars]}, @{term "t \<equiv> t"} and @{thm FalseE[no_vars]}; 
+  \end{isabelle}
+
+  and also resolve with assumptions. For example:
+*}
+
+lemma 
+ "True" and "t = t" and "t \<equiv> t" and "False \<Longrightarrow> Foo" and "\<lbrakk>A; B; C\<rbrakk> \<Longrightarrow> A"
+apply(tactic {* ALLGOALS (simp_tac HOL_basic_ss) *})
+done
+
+text {*
+  This behaviour is not because of simplification rules, but how the subgoaler, solver 
+  and looper are set up in @{ML HOL_basic_ss}.
+
+  The simpset @{ML HOL_ss} is an extention of @{ML HOL_basic_ss} containing 
+  already many useful simplification and congruence rules for the logical 
+  connectives in HOL. 
+
+  @{ML_response_fake [display,gray]
+  "print_ss @{context} HOL_ss"
+"Simplification rules:
+  Pure.triv_forall_equality: (\<And>x. PROP V) \<equiv> PROP V
+  HOL.the_eq_trivial: THE x. x = y \<equiv> y
+  HOL.the_sym_eq_trivial: THE ya. y = ya \<equiv> y
+  \<dots>
+Congruences rules:
+  HOL.simp_implies: \<dots>
+    \<Longrightarrow> (PROP P =simp=> PROP Q) \<equiv> (PROP P' =simp=> PROP Q')
+  op -->: \<lbrakk>P \<equiv> P'; P' \<Longrightarrow> Q \<equiv> Q'\<rbrakk> \<Longrightarrow> P \<longrightarrow> Q \<equiv> P' \<longrightarrow> Q'
+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
+  definition
+*}
+
+definition "MyTrue \<equiv> True"
+
+text {*
+  then in the following proof we can unfold this constant
+*}
+
+lemma shows "MyTrue \<Longrightarrow> True \<and> True"
+apply(rule conjI)
+apply(tactic {* rewrite_goals_tac [@{thm MyTrue_def}] *})
+txt{* producing the goal state
+
+      \begin{minipage}{\textwidth}
+      @{subgoals [display]}
+      \end{minipage} *}
+(*<*)oops(*>*)
+
+text {*
+  As you can see, the tactic unfolds the definitions in all subgoals.
+*}
+
+
+text_raw {*
+\begin{figure}[p]
+\begin{boxedminipage}{\textwidth}
+\begin{isabelle} *}
+types  prm = "(nat \<times> nat) list"
+consts perm :: "prm \<Rightarrow> 'a \<Rightarrow> 'a"  ("_ \<bullet> _" [80,80] 80)
+
+primrec (perm_nat)
+ "[]\<bullet>c = c"
+ "(ab#pi)\<bullet>c = (if (pi\<bullet>c)=fst ab then snd ab 
+               else (if (pi\<bullet>c)=snd ab then fst ab else (pi\<bullet>c)))" 
+
+primrec (perm_prod)
+ "pi\<bullet>(x, y) = (pi\<bullet>x, pi\<bullet>y)"
+
+primrec (perm_list)
+ "pi\<bullet>[] = []"
+ "pi\<bullet>(x#xs) = (pi\<bullet>x)#(pi\<bullet>xs)"
+
+lemma perm_append[simp]:
+  fixes c::"nat" and pi\<^isub>1 pi\<^isub>2::"prm"
+  shows "((pi\<^isub>1@pi\<^isub>2)\<bullet>c) = (pi\<^isub>1\<bullet>(pi\<^isub>2\<bullet>c))"
+by (induct pi\<^isub>1) (auto) 
+
+lemma perm_eq[simp]:
+  fixes c::"nat" and pi::"prm"
+  shows "(pi\<bullet>c = pi\<bullet>d) = (c = d)" 
+by (induct pi) (auto)
+
+lemma perm_rev[simp]:
+  fixes c::"nat" and pi::"prm"
+  shows "pi\<bullet>((rev pi)\<bullet>c) = c"
+by (induct pi arbitrary: c) (auto)
+
+lemma perm_compose:
+  fixes c::"nat" and pi\<^isub>1 pi\<^isub>2::"prm"
+  shows "pi\<^isub>1\<bullet>(pi\<^isub>2\<bullet>c) = (pi\<^isub>1\<bullet>pi\<^isub>2)\<bullet>(pi\<^isub>1\<bullet>c)" 
+by (induct pi\<^isub>2) (auto)
+text_raw {*
+\end{isabelle}
+\end{boxedminipage}
+\caption{A simple theory about permutations over @{typ nat}. The point is that the
+  lemma @{thm [source] perm_compose} cannot be directly added to the simplifier, as
+  it would cause the simplifier to loop. It can still be used as a simplification 
+  rule if the permutation is sufficiently protected.\label{fig:perms}
+  (FIXME: Uses old primrec.)}
+\end{figure} *}
+
+
+text {*
+  The simplifier is often used in order to bring terms into a normal form.
+  Unfortunately, often the situation arises that the corresponding
+  simplification rules will cause the simplifier to run into an infinite
+  loop. Consider for example the simple theory about permutations over natural
+  numbers shown in Figure~\ref{fig:perms}. The purpose of the lemmas is to
+  push permutations as far inside as possible, where they might disappear by
+  Lemma @{thm [source] perm_rev}. However, to fully normalise all instances,
+  it would be desirable to add also the lemma @{thm [source] perm_compose} to
+  the simplifier for pushing permutations over other permutations. Unfortunately, 
+  the right-hand side of this lemma is again an instance of the left-hand side 
+  and so causes an infinite loop. The seems to be no easy way to reformulate 
+  this rule and so one ends up with clunky proofs like:
+*}
+
+lemma 
+  fixes c d::"nat" and pi\<^isub>1 pi\<^isub>2::"prm"
+  shows "pi\<^isub>1\<bullet>(c, pi\<^isub>2\<bullet>((rev pi\<^isub>1)\<bullet>d)) = (pi\<^isub>1\<bullet>c, (pi\<^isub>1\<bullet>pi\<^isub>2)\<bullet>d)"
+apply(simp)
+apply(rule trans)
+apply(rule perm_compose)
+apply(simp)
+done 
+
+text {*
+  It is however possible to create a single simplifier tactic that solves
+  such proofs. The trick is to introduce an auxiliary constant for permutations 
+  and split the simplification into two phases (below actually three). Let 
+  assume the auxiliary constant is
+*}
+
+definition
+  perm_aux :: "prm \<Rightarrow> 'a \<Rightarrow> 'a" ("_ \<bullet>aux _" [80,80] 80)
+where
+  "pi \<bullet>aux c \<equiv> pi \<bullet> c"
+
+text {* Now the two lemmas *}
+
+lemma perm_aux_expand:
+  fixes c::"nat" and pi\<^isub>1 pi\<^isub>2::"prm"
+  shows "pi\<^isub>1\<bullet>(pi\<^isub>2\<bullet>c) = pi\<^isub>1 \<bullet>aux (pi\<^isub>2\<bullet>c)" 
+unfolding perm_aux_def by (rule refl)
+
+lemma perm_compose_aux:
+  fixes c::"nat" and pi\<^isub>1 pi\<^isub>2::"prm"
+  shows "pi\<^isub>1\<bullet>(pi\<^isub>2\<bullet>aux c) = (pi\<^isub>1\<bullet>pi\<^isub>2) \<bullet>aux (pi\<^isub>1\<bullet>c)" 
+unfolding perm_aux_def by (rule perm_compose)
+
+text {* 
+  are simple consequence of the definition and @{thm [source] perm_compose}. 
+  More importantly, the lemma @{thm [source] perm_compose_aux} can be safely 
+  added to the simplifier, because now the right-hand side is not anymore an instance 
+  of the left-hand side. In a sense it freezes all redexes of permutation compositions
+  after one step. In this way, we can split simplification of permutations
+  into three phases without the user not noticing anything about the auxiliary 
+  contant. We first freeze any instance of permutation compositions in the term using 
+  lemma @{thm [source] "perm_aux_expand"} (Line 9);
+  then simplifiy all other permutations including pusing permutations over
+  other permutations by rule @{thm [source] perm_compose_aux} (Line 10); and
+  finally ``unfreeze'' all instances of permutation compositions by unfolding 
+  the definition of the auxiliary constant. 
+*}
+
+ML %linenosgray{*val perm_simp_tac =
+let
+  val thms1 = [@{thm perm_aux_expand}]
+  val thms2 = [@{thm perm_append}, @{thm perm_eq}, @{thm perm_rev}, 
+               @{thm perm_compose_aux}] @ @{thms perm_prod.simps} @ 
+               @{thms perm_list.simps} @ @{thms perm_nat.simps}
+  val thms3 = [@{thm perm_aux_def}]
+in
+  simp_tac (HOL_basic_ss addsimps thms1)
+  THEN' simp_tac (HOL_basic_ss addsimps thms2)
+  THEN' simp_tac (HOL_basic_ss addsimps thms3)
+end*}
+
+text {*
+  For all three phases we have to build simpsets addig specific lemmas. As is sufficient
+  for our purposes here, we can add these lemma to @{ML HOL_basic_ss} in order to obtain
+  the desired results. Now we can solve the following lemma
+*}
+
+lemma 
+  fixes c d::"nat" and pi\<^isub>1 pi\<^isub>2::"prm"
+  shows "pi\<^isub>1\<bullet>(c, pi\<^isub>2\<bullet>((rev pi\<^isub>1)\<bullet>d)) = (pi\<^isub>1\<bullet>c, (pi\<^isub>1\<bullet>pi\<^isub>2)\<bullet>d)"
+apply(tactic {* perm_simp_tac 1 *})
+done
+
+
+text {*
+  in one step. This tactic can deal with most instances of normalising permutations;
+  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: What are the second components of the congruence rules---something to
+  do with weak congruence constants?)
+
+  (FIXME: Anything interesting to say about @{ML Simplifier.clear_ss}?)
+
+  (FIXME: @{ML ObjectLogic.full_atomize_tac}, 
+  @{ML ObjectLogic.rulify_tac})
+
+*}
+
+section {* Simprocs *}
+
+text {*
+  In Isabelle you can also implement custom simplification procedures, called
+  \emph{simprocs}. Simprocs can be triggered by the simplifier on a specified
+  term-pattern and rewrite a term according to a theorem. They are useful in
+  cases where a rewriting rule must be produced on ``demand'' or when
+  rewriting by simplification is too unpredictable and potentially loops.
+
+  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 = 
+let
+  val ctxt = Simplifier.the_context simpset
+  val _ = warning ("The redex: " ^ (str_of_cterm ctxt redex))
+in
+  NONE
+end*}
+
+text {*
+  This function takes a simpset and a redex (a @{ML_type cterm}) as
+  arguments. In Lines 3 and~4, we first extract the context from the given
+  simpset and then print out a message containing the redex.  The function
+  returns @{ML NONE} (standing for an optional @{ML_type thm}) since at the
+  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 *}
+
+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 ignoring
+  an argument about morphisms\footnote{FIXME: what does the morphism do?}). 
+  After this, the simplifier is aware of the simproc and you can test whether 
+  it fires on the lemma:
+*}
+
+lemma shows "Suc 0 = 1"
+apply(simp)
+(*<*)oops(*>*)
+
+text {*
+  This will print out the message twice: once for the left-hand side and
+  once for the right-hand side. The reason is that during simplification the
+  simplifier will at some point reduce the term @{term "1::nat"} to @{term "Suc
+  0"}, and then the simproc ``fires'' also on that term. 
+
+  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]]
+
+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} 
+  as follows:
+*}
+
+lemma shows "Suc 0 = 1"
+apply(tactic {* simp_tac (HOL_basic_ss addsimprocs [@{simproc fail_sp}]) 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
+  to
+*}
+
+ML{*fun fail_sp_aux' simpset redex = 
+let
+  val ctxt = Simplifier.the_context simpset
+  val _ = warning ("The redex: " ^ (Syntax.string_of_term 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 string_of_term in Syntax}).
+  We can turn this function into a proper simproc using the function 
+  @{ML Simplifier.simproc_i}:
+*}
+
+
+ML{*val fail_sp' = 
+let 
+  val thy = @{theory}
+  val pat = [@{term "Suc n"}]
+in
+  Simplifier.simproc_i thy "fail_sp'" pat (K fail_sp_aux')
+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
+  @{ML addsimprocs} to a simpset whenerver
+  needed. 
+
+  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*})
+(*<*)oops(*>*)
+
+text {*
+  The simproc @{ML fail_sp'} prints out the sequence 
+
+@{text [display]
+"> Suc 0
+> Suc (Suc 0) 
+> Suc 1"}
+
+  To see how a simproc applies a theorem,  let us implement a simproc that
+  rewrites terms according to the equation:
+*}
+
+lemma plus_one: 
+  shows "Suc n \<equiv> n + 1" by simp
+
+text {*
+  Simprocs expect that the given equation is a meta-equation, however the
+  equation can contain preconditions (the simproc then will only fire if the
+  preconditions can be solved). To see that one has relatively precise control over
+  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 =
+  case redex of
+    @{term "Suc 0"} => NONE
+  | _ => SOME @{thm plus_one}*}
+
+text {*
+  and set up the simproc as follows.
+*}
+
+ML{*val plus_one_sp =
+let
+  val thy = @{theory}
+  val pat = [@{term "Suc n"}] 
+in
+  Simplifier.simproc_i thy "sproc +1" pat (K plus_one_sp_aux)
+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*})
+txt{*
+  where the simproc produces the goal state
+  
+  \begin{minipage}{\textwidth}
+  @{subgoals[display]}
+  \end{minipage}
+*}  
+(*<*)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
+  the default simpset contains a rule which just does the opposite of @{ML plus_one_sp},
+  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} increase by one. First we implement a function that
+  takes a term and produces the corresponding integer value.
+*}
+
+ML{*fun dest_suc_trm ((Const (@{const_name "Suc"}, _)) $ t) = 1 + dest_suc_trm t
+  | dest_suc_trm t = snd (HOLogic.dest_number t)*}
+
+text {* 
+  It uses the library function @{ML dest_number in HOLogic} that transforms
+  (Isabelle) terms, like @{term "0::nat"}, @{term "1::nat"}, @{term "2::nat"} and so
+  on, into integer values. This function raises the exception @{ML TERM}, if
+  the term is not a number. The next function expects a pair consisting of a term
+  @{text t} (containing @{term Suc}s) and the corresponding integer value @{text n}. 
+*}
+
+ML %linenosgray{*fun get_thm ctxt (t, n) =
+let
+  val num = HOLogic.mk_number @{typ "nat"} n
+  val goal = Logic.mk_equals (t, num)
+in
+  Goal.prove ctxt [] [] goal (K (arith_tac ctxt 1))
+end*}
+
+text {*
+  From the integer value it generates the corresponding number term, called 
+  @{text num} (Line 3), and then generates the meta-equation @{text "t \<equiv> num"} 
+  (Line 4), which it proves by the arithmetic tactic in Line 6. 
+
+  For our purpose at the moment, proving the meta-equation using @{ML arith_tac} is
+  fine, but there is also an alternative employing the simplifier with a very
+  restricted simpset. For the kind of lemmas we want to prove, the simpset
+  @{text "num_ss"} in the code will suffice.
+*}
+
+ML{*fun get_thm_alt ctxt (t, n) =
+let
+  val num = HOLogic.mk_number @{typ "nat"} n
+  val goal = Logic.mk_equals (t, num)
+  val num_ss = HOL_ss addsimps [@{thm One_nat_def}, @{thm Let_def}] @ 
+          @{thms nat_number} @ @{thms neg_simps} @ @{thms plus_nat.simps}
+in
+  Goal.prove ctxt [] [] goal (K (simp_tac num_ss 1))
+end*}
+
+text {*
+  The advantage of @{ML get_thm_alt} is that it leaves very little room for 
+  something to go wrong; in contrast it is much more difficult to predict 
+  what happens with @{ML arith_tac}, especially in more complicated 
+  circumstances. The disatvantage of @{ML get_thm_alt} is to find a simpset
+  that is sufficiently powerful to solve every instance of the lemmas
+  we like to prove. This requires careful tuning, but is often necessary in 
+  ``production code''.\footnote{It would be of great help if there is another
+  way than tracing the simplifier to obtain the lemmas that are successfully 
+  applied during simplification. Alas, there is none.} 
+
+  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 =
+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 
+  @{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 =
+let
+  val thy = @{theory}
+  val pat = [@{term "Suc n"}]
+in 
+  Simplifier.simproc_i thy "nat_number" pat (K nat_number_sp_aux) 
+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*})
+txt {* 
+  you obtain the more legible goal state
+  
+  \begin{minipage}{\textwidth}
+  @{subgoals [display]}
+  \end{minipage}
+  *}
+(*<*)oops(*>*)
+
+text {*
+  where the simproc rewrites all @{term "Suc"}s except in the last argument. There it cannot 
+  rewrite anything, because it does not know how to transform the term @{term "Suc (0 + 0)"}
+  into a number. To solve this problem have a look at the next exercise. 
+
+  \begin{exercise}\label{ex:addsimproc}
+  Write a simproc that replaces terms of the form @{term "t\<^isub>1 + t\<^isub>2"} by their 
+  result. You can assume the terms are ``proper'' numbers, that is of the form
+  @{term "0::nat"}, @{term "1::nat"}, @{term "2::nat"} and so on.
+  \end{exercise}
+
+  (FIXME: We did not do anything with morphisms. Anything interesting
+  one can say about them?)
+*}
+
+section {* Conversions\label{sec:conversion} *}
+
+text {*
+
+  Conversions are a thin layer on top of Isabelle's inference kernel, and 
+  can be viewed as a controllable, bare-bone version of Isabelle's simplifier.
+  One difference between conversions and the simplifier is that the former
+  act on @{ML_type cterm}s while the latter acts on @{ML_type thm}s. 
+  However, we will also show in this section how conversions can be applied
+  to theorems via tactics. The type for conversions is
+*}
+
+ML{*type conv = cterm -> thm*}
+
+text {*
+  whereby the produced theorem is always a meta-equality. A simple conversion
+  is the function @{ML "Conv.all_conv"}, which maps a @{ML_type cterm} to an
+  instance of the (meta)reflexivity theorem. For example:
+
+  @{ML_response_fake [display,gray]
+  "Conv.all_conv @{cterm \"Foo \<or> Bar\"}"
+  "Foo \<or> Bar \<equiv> Foo \<or> Bar"}
+
+  Another simple conversion is @{ML Conv.no_conv} which always raises the 
+  exception @{ML CTERM}.
+
+  @{ML_response_fake [display,gray]
+  "Conv.no_conv @{cterm True}" 
+  "*** Exception- CTERM (\"no conversion\", []) raised"}
+
+  A more interesting conversion is the function @{ML "Thm.beta_conversion"}: it 
+  produces a meta-equation between a term and its beta-normal form. For example
+
+  @{ML_response_fake [display,gray]
+  "let
+  val add = @{cterm \"\<lambda>x y. x + (y::nat)\"}
+  val two = @{cterm \"2::nat\"}
+  val ten = @{cterm \"10::nat\"}
+in
+  Thm.beta_conversion true (Thm.capply (Thm.capply add two) ten)
+end"
+  "((\<lambda>x y. x + y) 2) 10 \<equiv> 2 + 10"}
+
+  Note that the actual response in this example is @{term "2 + 10 \<equiv> 2 + (10::nat)"}, 
+  since the pretty-printer for @{ML_type cterm}s already beta-normalises terms.
+  But how we constructed the term (using the function 
+  @{ML Thm.capply}, which is the application @{ML $} for @{ML_type cterm}s)
+  ensures that the left-hand side must contain beta-redexes. Indeed
+  if we obtain the ``raw'' representation of the produced theorem, we
+  can see the difference:
+
+  @{ML_response [display,gray]
+"let
+  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)
+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 
+  @{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
+  val add = @{cterm \"\<lambda>x y. x + (y::nat)\"}
+  val two = @{cterm \"2::nat\"}
+in
+  Thm.beta_conversion false (Thm.capply add two)
+end"
+  "((\<lambda>x y. x + y) 2) \<equiv> \<lambda>y. 2 + y"} 
+
+  Again, we actually see as output only the fully normalised term 
+  @{text "\<lambda>y. 2 + y"}.
+
+  The main point of conversions is that they can be used for rewriting
+  @{ML_type cterm}s. To do this you can use the function @{ML
+  "Conv.rewr_conv"}, which expects a meta-equation as an argument. Suppose we
+  want to rewrite a @{ML_type cterm} according to the meta-equation:
+*}
+
+lemma true_conj1: "True \<and> P \<equiv> P" by simp
+
+text {* 
+  You can see how this function works in the example rewriting 
+  @{term "True \<and> (Foo \<longrightarrow> Bar)"} to @{term "Foo \<longrightarrow> Bar"}.
+
+  @{ML_response_fake [display,gray]
+"let 
+  val ctrm = @{cterm \"True \<and> (Foo \<longrightarrow> Bar)\"}
+in
+  Conv.rewr_conv @{thm true_conj1} ctrm
+end"
+  "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 
+  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}, 
+  which applies one conversion after another. For example
+
+  @{ML_response_fake [display,gray]
+"let
+  val conv1 = Thm.beta_conversion false
+  val conv2 = Conv.rewr_conv @{thm true_conj1}
+  val ctrm = Thm.capply @{cterm \"\<lambda>x. x \<and> False\"} @{cterm \"True\"}
+in
+  (conv1 then_conv conv2) ctrm
+end"
+  "(\<lambda>x. x \<and> False) True \<equiv> False"}
+
+  where we first beta-reduce the term and then rewrite according to
+  @{thm [source] true_conj1}. (Recall the problem with the pretty-printer
+  normalising all terms.)
+
+  The conversion combinator @{ML else_conv} tries out the 
+  first one, and if it does not apply, tries the second. For example 
+
+  @{ML_response_fake [display,gray]
+"let
+  val conv = Conv.rewr_conv @{thm true_conj1} else_conv Conv.all_conv
+  val ctrm1 = @{cterm \"True \<and> Q\"}
+  val ctrm2 = @{cterm \"P \<or> (True \<and> Q)\"}
+in
+  (conv ctrm1, conv ctrm2)
+end"
+"(True \<and> Q \<equiv> Q, P \<or> True \<and> Q \<equiv> P \<or> True \<and> Q)"}
+
+  Here the conversion of @{thm [source] true_conj1} only applies
+  in the first case, but fails in the second. The whole conversion
+  does not fail, however, because the combinator @{ML Conv.else_conv} will then 
+  try out @{ML Conv.all_conv}, which always succeeds.
+
+  The conversion combinator @{ML Conv.try_conv} constructs a conversion 
+  which is tried out on a term, but in case of failure just does nothing.
+  For example
+  
+  @{ML_response_fake [display,gray]
+  "Conv.try_conv (Conv.rewr_conv @{thm true_conj1}) @{cterm \"True \<or> P\"}"
+  "True \<or> P \<equiv> True \<or> P"}
+
+  Apart from the function @{ML beta_conversion in Thm}, which is able to fully
+  beta-normalise a term, the conversions so far are restricted in that they
+  only apply to the outer-most level of a @{ML_type cterm}. In what follows we
+  will lift this restriction. The combinator @{ML Conv.arg_conv} will apply
+  the conversion to the first argument of an application, that is the term
+  must be of the form @{ML "t1 $ t2" for t1 t2} and the conversion is applied
+  to @{text t2}.  For example
+
+  @{ML_response_fake [display,gray]
+"let 
+  val conv = Conv.rewr_conv @{thm true_conj1}
+  val ctrm = @{cterm \"P \<or> (True \<and> Q)\"}
+in
+  Conv.arg_conv conv ctrm
+end"
+"P \<or> (True \<and> Q) \<equiv> P \<or> Q"}
+
+  The reason for this behaviour is that @{text "(op \<or>)"} expects two
+  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.
+  For example:
+
+  @{ML_response_fake [display,gray]
+"let 
+  val conv = K (Conv.rewr_conv @{thm true_conj1}) 
+  val ctrm = @{cterm \"\<lambda>P. True \<and> P \<and> Foo\"}
+in
+  Conv.abs_conv 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 
+  as arguments, each of which is applied to the corresponding ``branch'' of the
+  application. 
+
+  We can now apply all these functions in a conversion that recursively
+  descends a term and applies a ``@{thm [source] true_conj1}''-conversion 
+  in all possible positions.
+*}
+
+ML %linenosgray{*fun all_true1_conv ctxt ctrm =
+  case (Thm.term_of ctrm) of
+    @{term "op \<and>"} $ @{term True} $ _ => 
+      (Conv.arg_conv (all_true1_conv ctxt) then_conv
+         Conv.rewr_conv @{thm true_conj1}) ctrm
+  | _ $ _ => Conv.combination_conv 
+               (all_true1_conv ctxt) (all_true1_conv ctxt) ctrm
+  | Abs _ => Conv.abs_conv (fn (_, ctxt) => all_true1_conv ctxt) ctxt ctrm
+  | _ => Conv.all_conv ctrm*}
+
+text {*
+  This function ``fires'' if the terms is of the form @{text "True \<and> \<dots>"}; 
+  it descends under applications (Line 6 and 7) and abstractions 
+  (Line 8); otherwise it leaves the term unchanged (Line 9). In Line 2
+  we need to transform the @{ML_type cterm} into a @{ML_type term} in order
+  to be able to pattern-match the term. To see this 
+  conversion in action, consider the following example:
+
+@{ML_response_fake [display,gray]
+"let
+  val ctxt = @{context}
+  val ctrm = @{cterm \"distinct [1, x] \<longrightarrow> True \<and> 1 \<noteq> x\"}
+in
+  all_true1_conv ctxt ctrm
+end"
+  "distinct [1, x] \<longrightarrow> True \<and> 1 \<noteq> x \<equiv> distinct [1, x] \<longrightarrow> 1 \<noteq> x"}
+
+  To see how much control you have about rewriting by using conversions, let us 
+  make the task a bit more complicated by rewriting according to the rule
+  @{text true_conj1}, but only in the first arguments of @{term If}s. Then 
+  the conversion should be as follows.
+*}
+
+ML{*fun if_true1_conv ctxt ctrm =
+  case Thm.term_of ctrm of
+    Const (@{const_name If}, _) $ _ =>
+      Conv.arg_conv (all_true1_conv ctxt) ctrm
+  | _ $ _ => Conv.combination_conv 
+                (if_true1_conv ctxt) (if_true1_conv ctxt) ctrm
+  | Abs _ => Conv.abs_conv (fn (_, ctxt) => if_true1_conv ctxt) ctxt ctrm
+  | _ => Conv.all_conv ctrm *}
+
+text {*
+  Here is an example for this conversion:
+
+  @{ML_response_fake [display,gray]
+"let
+  val ctxt = @{context}
+  val ctrm = 
+       @{cterm \"if P (True \<and> 1 \<noteq> 2) then True \<and> True else True \<and> False\"}
+in
+  if_true1_conv ctxt ctrm
+end"
+"if P (True \<and> 1 \<noteq> 2) then True \<and> True else True \<and> False 
+\<equiv> if P (1 \<noteq> 2) then True \<and> True else True \<and> False"}
+*}
+
+text {*
+  So far we only applied conversions to @{ML_type cterm}s. Conversions can, however, 
+  also work on theorems using the function @{ML "Conv.fconv_rule"}. As an example, 
+  consider the conversion @{ML all_true1_conv} and the lemma:
+*}
+
+lemma foo_test: "P \<or> (True \<and> \<not>P)" by simp
+
+text {*
+  Using the conversion you can transform this theorem into a new theorem
+  as follows
+
+  @{ML_response_fake [display,gray]
+  "Conv.fconv_rule (all_true1_conv @{context}) @{thm foo_test}" 
+  "?P \<or> \<not> ?P"}
+
+  Finally, conversions can also be turned into tactics and then applied to
+  goal states. This can be done with the help of the function @{ML CONVERSION},
+  and also some predefined conversion combinators that traverse a goal
+  state. The combinators for the goal state are: @{ML Conv.params_conv} for
+  converting under parameters (i.e.~where goals are of the form @{text "\<And>x. P \<Longrightarrow>
+  Q"}); the function @{ML Conv.prems_conv} for applying a conversion to all
+  premises of a goal, and @{ML Conv.concl_conv} for applying a conversion to
+  the conclusion of a goal.
+
+  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) =>
+  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)*}
+
+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 
+  only be called on @{text n} premises (similar for parameters and
+  conclusions). To test the tactic, consider the proof
+*}
+
+lemma
+  "if True \<and> P then P else True \<and> False \<Longrightarrow>
+  (if True \<and> Q then True \<and> Q else P) \<longrightarrow> True \<and> (True \<and> Q)"
+apply(tactic {* true1_tac @{context} 1 *})
+txt {* where the tactic yields the goal state
+
+  \begin{minipage}{\textwidth}
+  @{subgoals [display]}
+  \end{minipage}*}
+(*<*)oops(*>*)
+
+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
+  and simprocs; the advantage of conversions, however, is that you never have
+  to worry about 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
+  the same assumptions as in \ref{ex:addsimproc}. 
+  \end{exercise}
+
+  \begin{exercise}\label{ex:compare}
+  Compare your solutions of Exercises~\ref{ex:addsimproc} and \ref{ex:addconversion},
+  and try to determine which way of rewriting such terms is faster. For this you might 
+  have to construct quite large terms. Also see Recipe \ref{rec:timing} for information 
+  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"},
+  @{ML_file "Pure/drule.ML"} and @{ML_file "Pure/meta_simplifier.ML"}.
+  \end{readmore}
+
+*}
+
+text {*
+  (FIXME: check whether @{ML Pattern.match_rew} and @{ML Pattern.rewrite_term}
+  are of any use/efficient)
+*}
+
+
+section {* Structured Proofs (TBD) *}
+
+text {* TBD *}
+
+lemma True
+proof
+
+  {
+    fix A B C
+    assume r: "A & B \<Longrightarrow> C"
+    assume A B
+    then have "A & B" ..
+    then have C by (rule r)
+  }
+
+  {
+    fix A B C
+    assume r: "A & B \<Longrightarrow> C"
+    assume A B
+    note conjI [OF this]
+    note r [OF this]
+  }
+oops
+
+ML {* fun prop ctxt s =
+  Thm.cterm_of (ProofContext.theory_of ctxt) (Syntax.read_prop ctxt s) *}
+
+ML {* 
+  val ctxt0 = @{context};
+  val ctxt = ctxt0;
+  val (_, ctxt) = Variable.add_fixes ["A", "B", "C"] ctxt;
+  val ([r], ctxt) = Assumption.add_assumes [prop ctxt "A & B \<Longrightarrow> C"] ctxt;
+  val (this, ctxt) = Assumption.add_assumes [prop ctxt "A", prop ctxt "B"] ctxt;
+  val this = [@{thm conjI} OF this]; 
+  val this = r OF this;
+  val this = Assumption.export false ctxt ctxt0 this 
+  val this = Variable.export ctxt ctxt0 [this] 
+*}
+
+
+
+end