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. Consider 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} 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"}. For more information about the
  internals of goals see \isccite{sec:tactical-goals}.  See @{ML_file
  "Pure/tactic.ML"} and @{ML_file "Pure/tctical.ML"} for the code of basic
  tactics and tactic combinators; see also Chapters 3 and 4 in the old
  Isabelle Reference Manual.
  \end{readmore}

  Note that we used antiquotations for referencing the theorems. Many theorems
  also have ML-bindings with the same name. Therefore, we could also just have
  written @{ML "etac disjE 1"}, or in case there are no ML-binding obtained
  the theorem dynamically using the theorem @{ML thm}; for example @{ML "etac
  (thm \"disjE\") 1"}. Both ways however are considered bad style. The reason
  is that the binding for @{ML disjE} can be re-assigned by the user and thus
  one does not have complete control over which theorem is actually
  applied. This problem is nicely prevented by using antiquotations, because
  then the theorems are fixed statically at compile-time.

  During the development of automatic proof procedures, you will often find it 
  necessary to test a tactic on examples. This can be conveniently 
  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
*}

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
  after that 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 every operator that combines tactics 
  (@{ML THEN} is only one such operator) a ``primed'' version exists.

  The tactics @{ML foo_tac} and @{ML foo_tac'} are very specific for
  analysing goals being only of the form @{prop "P \<or> Q \<Longrightarrow> Q \<or> P"}. If the goal is not
  of this form, then they throw the error message:

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

  Meaning the tactics failed. The reason for this error message is that tactics 
  are functions that map a goal state to a (lazy) sequence of successor states, 
  hence the type of a tactic is:
  
  @{text [display, gray] "type tactic = thm -> thm Seq.seq"}

  It is custom that if a tactic fails, it should return the empty sequence: 
  therefore your own tactics should not raise exceptions willy-nilly.

  The simplest tactics are @{ML no_tac} and @{ML all_tac}. The first returns
  the empty sequence and is defined as
*}

ML{*fun no_tac thm = Seq.empty*}

text {*
  which means @{ML no_tac} always fails. The second returns the given theorem wrapped 
  as a single member sequence. It is defined as
*}

ML{*fun all_tac thm = Seq.single thm*}

text {*
  which means @{ML all_tac} always succeeds (but also does not make any progress 
  with the proof).

  The lazy list of possible successor states shows through 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'}.
*}

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. In more interesting situations, different possibilities 
  can lead to different proofs and even often need to be explored when
  a first proof attempt is unsuccessful.
  
  \begin{readmore}
  See @{ML_file "Pure/General/seq.ML"} for the implementation of lazy
  sequences. However in day-to-day Isabelle programming, one rarely 
  constructs sequences explicitly, but uses the predefined functions
  instead.
  \end{readmore}

  It might be surprising that tactics, which transform
  one proof state to the next, are functions from theorems to theorem 
  (sequences). The surprise resolves by knowing that every 
  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 {*
  which prints out the given theorem (using the string-function defined 
  in Section~\ref{sec:printing}) and then behaves like @{ML all_tac}. We
  now can inspect every proof state in a proof. Consider the proof below: on 
  the left-hand side we show the goal state as shown by Isabelle; on the 
  right-hand side the print out from @{ML my_print_tac}.
*}

lemma shows "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B" 
apply(tactic {* my_print_tac @{context} *})

txt{* \small 
      \begin{tabular}{@ {}l@ {}p{0.7\textwidth}@ {}}
      \begin{minipage}[t]{0.3\textwidth}
      @{subgoals [display]} 
      \end{minipage} &
      \hfill@{text "(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B)"}
      \end{tabular}
*}

apply(rule conjI)
apply(tactic {* my_print_tac @{context} *})

txt{* \small 
      \begin{tabular}{@ {}l@ {}p{0.76\textwidth}@ {}}
      \begin{minipage}[t]{0.26\textwidth}
      @{subgoals [display]} 
      \end{minipage} &
      \hfill@{text "(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> B) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B)"}
      \end{tabular}
*}

apply(assumption)
apply(tactic {* my_print_tac @{context} *})

txt{* \small 
      \begin{tabular}{@ {}l@ {}p{0.7\textwidth}@ {}}
      \begin{minipage}[t]{0.3\textwidth}
      @{subgoals [display]} 
      \end{minipage} &
      \hfill@{text "(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> B) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B)"}
      \end{tabular}
*}

apply(assumption)
apply(tactic {* my_print_tac @{context} *})

txt{* \small 
      \begin{tabular}{@ {}l@ {}p{0.7\textwidth}@ {}}
      \begin{minipage}[t]{0.3\textwidth}
      @{subgoals [display]} 
      \end{minipage} &
      \hfill@{text "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B"}
      \end{tabular}
*}

done

text {*
  As can be seen, internally every goal state is an implication of the form

  @{text[display] "A\<^isub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^isub>n \<Longrightarrow> (C)"}

  where @{term C} is the goal to be proved and the @{term "A\<^isub>i"} are the  
  subgoals. So after setting up the lemma, the goal state is always of the form
  @{text "C \<Longrightarrow> (C)"}. Since the goal @{term C} can potentially be an implication, 
  there is a ``protector'' wrapped around it (in from of an outermost constant 
  @{text "Const (\"prop\", bool \<Rightarrow> bool)"} applied to each goal;
  however this constant is invisible in the print out above). This 
  prevents that premises of @{text C} are misinterpreted as open subgoals. 
  While tactics can operate on the subgoals (the @{text "A\<^isub>i"} above), they 
  are expected to leave the conclusion @{term C} intact, with the 
  exception of possibly instantiating schematic variables. 
 
*}

section {* Simple Tactics *}

text {*
  A simple tactic is @{ML print_tac}, which is useful for low-level debugging of tactics.
  It just prints out a message and the current goal state.
*}
 
lemma shows "False \<Longrightarrow> True"
apply(tactic {* print_tac "foo message" *})
(*<*)oops(*>*)

text {*
  Another simple tactic is the function @{ML atac}, which, as shown in the previous
  section, corresponds to the assumption command.
*}

lemma shows "P \<Longrightarrow> P"
apply(tactic {* atac 1 *})
done

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. Below are three 
  examples with the resulting goal state. How
  they work should be self-explanatory.  
*}

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 {*
  As mentioned in the previous section, most basic tactics take a number as 
  argument, which addresses the subgoal they are analysing. In the proof below,
  we first break up the second subgoal by focusing on this subgoal first.
*}

lemma shows "Foo" and "P \<and> Q"
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 exists for @{ML atac} (@{ML assume_tac}), @{ML etac} 
  (@{ML eresolve_tac}) and so on. 

  (FIXME: @{ML cut_facts_tac})

  Since rules are applied using higher-order unification, an automatic proof
  procedure might become too fragile, if it just applies inference rules shown
  in the fashion above.  More constraints can be introduced by
  pre-instantiating theorems with other theorems. You can do this using the
  function @{ML RS}. For example
  
  @{ML_response_fake [display,gray]
  "@{thm disjI1} RS @{thm conjI}" "\<lbrakk>?P1; ?Q\<rbrakk> \<Longrightarrow> (?P1 \<or> ?Q1) \<and> ?Q"}

  instantiates the first premise of the @{text conjI}-rule with the
  rule @{text disjI1}. The function @{ML RSN} is similar, but 
  takes a number and makes explicit which premise should be instantiated. 
  To improve readability we are going use the following function
*}

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

text {*
  to transform the schematic variables of a theorem into free variables. 
  This means for the @{ML RS}-expression above:

  @{ML_response_fake [display,gray]
  "no_vars @{context} (@{thm disjI1} RS @{thm conjI})" "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> (P \<or> Qa) \<and> Q"}

  If you want to instantiate more than one premise, you can use the function 
  @{ML MRS}:

  @{ML_response_fake [display,gray]
  "no_vars @{context} ([@{thm disjI1}, @{thm disjI2}] MRS @{thm conjI})" 
  "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> (P \<or> Qa) \<and> (Pa \<or> Q)"}

  If you need to instantiate lists of theorems, you can use the
  functions @{ML RL} and @{ML MRL}. For example below every
  theorem in the first list is instantiated against every theorem
  in the second.

  @{ML_response_fake [display,gray]
   "[@{thm impI}, @{thm disjI2}] RL [@{thm conjI}, @{thm disjI1}]" 
"[\<lbrakk>P \<Longrightarrow> Q; Qa\<rbrakk> \<Longrightarrow> (P \<longrightarrow> Q) \<and> Qa,
 \<lbrakk>Q; Qa\<rbrakk> \<Longrightarrow> (P \<or> Q) \<and> Qa,
 (P \<Longrightarrow> Q) \<Longrightarrow> (P \<longrightarrow> Q) \<or> Qa,
 Q \<Longrightarrow> (P \<or> Q) \<or> Qa]"}

  \begin{readmore}
  The combinators for instantiating theorems are defined in @{ML_file "Pure/drule.ML"}.
  \end{readmore}

  Often proofs involve elaborate operations on assumptions and 
  @{text "\<And>"}-quantified variables. To do such operations on the ML-level 
  using the basic tactics is very unwieldy and brittle. Some convenience and
  safety is provided by the tactic @{ML SUBPROOF}. This tactic fixes the parameters 
  and binds the various components of a proof state into a record. 
  To see what happens, assume the function defined in Figure~\ref{fig:sptac}, which
  takes a record as argument and just prints out the content of this record (using the 
  string transformation functions defined in Section~\ref{sec:printing}). Consider
  now the proof
*}

text_raw{*
\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 {*
  which yields the 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. Similarly the schematic variable @{term z}. The assumption 
  @{prop "A x y"} is bound as @{ML_type cterm} to the record-variable 
  @{text asms} but also as @{ML_type thm} to @{text prems}.

  Notice also that we had to append @{text "?"} to \isacommand{apply}. The 
  reason is that @{ML SUBPROOF} normally expects that the subgoal is solved completely.
  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 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 @{ML SUBPROOF} 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 {*
  where we now also have @{term "B y x"} as an assumption.

  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 we can easily 
  implement a tactic that almost behaves like @{ML atac}, namely:
*}

ML{*val atac' = SUBPROOF (fn {prems, ...} => resolve_tac prems 1)*}
lemma shows "\<And>x y. \<lbrakk>B x y; A x y; C x y\<rbrakk> \<Longrightarrow> A x y"
apply(tactic {* atac' @{context} 1 *})
txt{* yields
      @{subgoals [display]} *}
(*<*)oops(*>*)

text {*
  The restriction in this tactic is that it cannot instantiate any
  schematic variables. This might be seen as a defect, but is actually
  an advantage in the situations for which @{ML SUBPROOF} was designed: 
  the reason is that instantiation of schematic variables can affect 
  several goals and can render them unprovable. @{ML SUBPROOF} is meant 
  to avoid this.

  Notice that @{ML atac'} 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"}. Another advantage 
  of @{ML SUBGOAL} is that the addressing  inside it is completely 
  local to the subproof inside. It is therefore possible to also apply 
  @{ML atac'} to the second goal:
*}

lemma shows "True" and "\<And>x y. \<lbrakk>B x y; A x y; C x y\<rbrakk> \<Longrightarrow> A x y"
apply(tactic {* atac' @{context} 2 *})
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 specified subgoal. With this you can implement 
  a tactic that applies a rule according to its topmost connective (we only 
  analyse a few connectives). The tactic is as follows:
*}

ML %linenumbers{*fun select_tac (t,i) =
  case t of
     @{term "Trueprop"} $ t' => select_tac (t',i)
   | @{term "op \<and>"} $ _ $ _ => rtac @{thm conjI} i
   | @{term "op \<longrightarrow>"} $ _ $ _ => rtac @{thm impI} i
   | @{term "Not"} $ _ => rtac @{thm notI} i
   | Const (@{const_name "All"}, _) $ _ => rtac @{thm allI} i
   | _ => all_tac*}

text {*
  In line 3 you need to decend under the outermost @{term "Trueprop"} in order
  to get to the connective you like to analyse. Otherwise goals @{prop "A \<and> B"} 
  are not bropek up. In line 7, the pattern cannot be constructed using the
  @{text "@term"}-antiquotation, because that would fix the type of the 
  quantified variable. In this case you really have to construct the pattern
  by using the term-constructors. The other cases work, because their type
  is always bool. In case that the goal does not fall into any of the categorories, 
  then we chose to just return @{ML all_tac} (i.e., the tactic never fails). 

  Let us now see how to apply this tactic.
*}


lemma shows "A \<and> B" and "A \<longrightarrow> B \<longrightarrow>C" and "\<forall>x. D x" and "E \<Longrightarrow> F"
apply(tactic {* SUBGOAL select_tac 4 *})
apply(tactic {* SUBGOAL select_tac 3 *})
apply(tactic {* SUBGOAL select_tac 2 *})
apply(tactic {* SUBGOAL select_tac 1 *})
txt{* @{subgoals [display]} *}
(*<*)oops(*>*)

text {*
  Note that we applied it in ``reverse'' order. This is a trick in 
  order to be independent from what subgoals the rule produced. If we had
  it applied in the other order 
*}

lemma shows "A \<and> B" and "A \<longrightarrow> B \<longrightarrow>C" and "\<forall>x. D x" and "E \<Longrightarrow> F"
apply(tactic {* SUBGOAL select_tac 1 *})
apply(tactic {* SUBGOAL select_tac 3 *})
apply(tactic {* SUBGOAL select_tac 4 *})
apply(tactic {* SUBGOAL select_tac 5 *})
(*<*)oops(*>*)

text {*
  then we have to be careful to not apply the tactic to the two subgoals the
  first goal produced. This can be messy in an automated proof script. The
  reverse application, on the other hand, is easy to implement.

  However, this example is contrived: there are much simpler ways to implement
  such proof procedure that analyses a goal according to its topmost
  connective. They will be explained in the next section.
*}

section {* Tactic Combinators *}

text {* 
  To be able to implement powerful tactics out of smaller component tactics, 
  Isabelle provides tactic combinators. In the previous section we already
  used @{ML THEN} which strings two tactics together in sequence. For example:
*}

lemma shows "(Foo \<and> Bar) \<and> False"
apply(tactic {* rtac @{thm conjI} 1 THEN rtac @{thm conjI} 1 *})
txt {* \begin{minipage}{\textwidth}
       @{subgoals [display]} 
       \end{minipage} *}
(*<*)oops(*>*)

text {*
  If you want to avoid the hard-coded subgoal addressing, then you can use
  @{ML THEN'}. For example:
*}

lemma shows "(Foo \<and> Bar) \<and> False"
apply(tactic {* (rtac @{thm conjI} THEN' rtac @{thm conjI}) 1 *})
txt {* \begin{minipage}{\textwidth}
       @{subgoals [display]} 
       \end{minipage} *}
(*<*)oops(*>*)

text {* 
  For most tactic combinators such a ``primed'' version exists.
  In what follows we will, whenever appropriate, prefer the primed version of
  the tactic combinator and omit to mention the simple one. 

  With @{ML THEN} and @{ML THEN'} it must be guaranteed that both tactics 
  sucessfully apply; otherwise the whole tactic will fail. If you want to
  try out either one tactic, then you can use @{ML ORELSE'}. For 
  example
*}

ML{*val orelse_xmp = (rtac @{thm disjI1} ORELSE' rtac @{thm conjI})*}

text {*
  will first try out rule @{text disjI} and after that @{text conjI}.
*}

lemma shows "True \<and> False" and "Foo \<or> Bar"
apply(tactic {* orelse_xmp 1 *})
apply(tactic {* orelse_xmp 3 *})
txt {* @{subgoals [display]} *}
(*<*)oops(*>*)


text {*
  applies 


  @{ML REPEAT} @{ML DETERM}

*}

section {* Rewriting and Simplifier Tactics *}

text {*
  @{ML rewrite_goals_tac}
  @{ML ObjectLogic.full_atomize_tac}
  @{ML ObjectLogic.rulify_tac}
*}


section {* Structured Proofs *}

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