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.
  \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 they return the error message:

  \begin{isabelle}
  @{text "*** empty result sequence -- proof command failed"}\\
  @{text "*** At command \"apply\"."}
  \end{isabelle}

  This means the tactics 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 
  up 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{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}
  \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
  illustrates that every goal state in Isabelle is represented by a theorem:
  when we 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 we 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 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 the 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. 
  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 an argument; it addresses the subgoal they 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 {* 
  Similarly 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 following function
*}

ML{*fun no_vars ctxt thm =
let 
  val ((_, [thm']), _) = Variable.import_thms true [thm] ctxt
in
  thm'
end*}

text {*
  that transform the schematic variables of a theorem into free variables.
  Using this function for the first @{ML RS}-expression above would produce
  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}
\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}
\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}

  Note 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}

  A similar but less powerful function than @{ML SUBPROOF} is @{ML SUBGOAL}. 
  It allows you to inspect a given  subgoal. 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}. For the
  final 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 {* Rewriting and Simplifier Tactics *}

text {*
  @{ML rewrite_goals_tac}
  
  @{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 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 simproc as follows
*}

simproc_setup 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{setup\_simproc} 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
*}


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_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_ss addsimprocs [plus_one_sp]) 1*})
txt{*
  where the simproc produces the goal state

  @{subgoals[display]}
*}  
(*<*)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
  
  @{subgoals [display]}
  *}
(*<*)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: core of the simplifier

see: Pure/conv.ML
*}

ML {* type conv = Thm.cterm -> Thm.thm *}

text {*
simple example:
*}

lemma true_conj_1: "True \<and> P \<equiv> P" by simp

ML {*
val true1_conv = Conv.rewr_conv @{thm true_conj_1}
*}

ML {*
true1_conv @{cterm "True \<and> False"}
*}

text {*
@{ML_response_fake "true1_conv @{cterm \"True \<and> False\"}"
  "True \<and> False \<equiv> False"}
*}

text {*
how to extend rewriting to more complex cases? e.g.:
*}

ML {*
val complex = @{cterm "distinct [1, x] \<longrightarrow> True \<and> 1 \<noteq> (x::int)"}
*}

text {* conversionals: basically a count-down version of MetaSimplifier.rewrite *}

ML {*
fun all_true1_conv ctxt ct =
  (case Thm.term_of ct of
    @{term "op \<and>"} $ @{term True} $ _ => true1_conv ct
  | _ $ _ => Conv.combination_conv (all_true1_conv ctxt) (all_true1_conv ctxt) ct
  | Abs _ => Conv.abs_conv (fn (_, cx) => all_true1_conv cx) ctxt ct)
*}

text {*
@{ML_response_fake "all_true1_conv @{context} complex"
  "distinct [1, x] \<longrightarrow> True \<and> 1 \<noteq> x \<equiv> distinct [1, x] \<longrightarrow> 1 \<noteq> x"}
*}


text {*
transforming theorems: @{ML "Conv.fconv_rule"} (give type)

example:
*}

lemma foo: "True \<and> (P \<or> \<not>P)" by simp

text {*
@{ML_response_fake "Conv.fconv_rule (Conv.arg_conv (all_true1_conv @{context})) @{thm foo}" "P \<or> \<not>P"}
*}

text {* now, replace "True and P" with "P" if it occurs inside an If *}

ML {*
fun if_true1_conv ctxt ct =
  (case Thm.term_of ct of
    Const (@{const_name If}, _) $ _ => Conv.arg_conv (all_true1_conv ctxt) ct
  | _ $ _ => Conv.combination_conv (if_true1_conv ctxt) (if_true1_conv ctxt) ct
  | Abs _ => Conv.abs_conv (fn (_, cx) => if_true1_conv cx) ctxt ct)
*}

text {* show example *}

text {*
conversions inside a tactic: replace "true" in conclusion, "if true" in assumptions
*}

ML {*
local open Conv 
in
fun true1_tac ctxt =
  CONVERSION (
    Conv.params_conv ~1 (fn cx =>
      (Conv.prems_conv ~1 (if_true1_conv cx)) then_conv
        (Conv.concl_conv ~1 (all_true1_conv cx))) ctxt)
end
*}

text {* give example, show that the conditional rewriting works *}





section {* Structured Proofs *}

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