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 @{text apply}-style reasoning at
  the user level, where goals are modified in a sequence of proof steps until
  all of them are solved. However, there are also more structured operations
  that help with handling of variables and assumptions.
*}

section {* Tactical Reasoning *}

text {*
  To see how tactics work, let us first transcribe a simple @{text 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. We could also
  just have written @{ML "etac disjE 1"} and so on, but this is 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, it will often be 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>"} in the apply-step,
  you can call @{ML foo_tac} or any function that returns a tactic from the
  user level of Isabelle.

  As can be seen, each tactic in @{ML foo_tac} has a hard-coded number that
  stands for the subgoal analysed by the tactic. In our case, we only focus on the first
  subgoal. This is sometimes wanted, but usually not. To avoid the explicit numbering in the 
  tactic, 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. For every operator that combines tactics, such a primed version 
  exists. So in the next proof we can first discharge the second subgoal,
  and after that the first.
*}

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 {*
  (FIXME: maybe add something about how each goal state is interpreted
  as a theorem)

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

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

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

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

  The lazy list of possible successor states shows through to the user-level 
  of Isabelle when using the command \isacommand{back}. For instance in the 
  following proof, there are two possibilities for how to apply 
  @{ML foo_tac'}.
*}

lemma "\<lbrakk>P \<or> Q; P \<or> Q\<rbrakk> \<Longrightarrow> Q \<or> P"
apply(tactic {* foo_tac' 1 *})
back
done

text {*
  By using \isacommand{back}, we construct the proof that uses the
  second assumption to complete the proof. In more interesting 
  situations, different possibilities can lead to different proofs.
  
  \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}

*}

section {* Basic Tactics *}

text {*
  As seen above, the function @{ML atac} corresponds to the assumption tactic.
*}

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

text {*
  Similarly, @{ML rtac}, @{ML dtac}, @{ML etac} and @{ML ftac} correspond
  to @{ML_text rule}, @{ML_text drule}, @{ML_text erule} and @{ML_text frule}, 
  respectively. Below are three examples with the resulting goal state. How
  they work should therefore be self-explanatory.  
*}

lemma shows "P \<and> Q"
apply(tactic {* rtac @{thm conjI} 1 *})
txt{*@{subgoals [display]}*}
(*<*)oops(*>*)

lemma shows "P \<and> Q \<Longrightarrow> False"
apply(tactic {* etac @{thm conjE} 1 *})
txt{*@{subgoals [display]}*}
(*<*)oops(*>*)

lemma shows "False \<and> True \<Longrightarrow> False"
apply(tactic {* dtac @{thm conjunct2} 1 *})
txt{*@{subgoals [display]}*}
(*<*)oops(*>*)

text {*
  As mentioned above, most basic tactics take a number as argument, which
  addresses to subgoal they are analysing.
*}

lemma shows "Foo" and "P \<and> Q"
apply(tactic {* rtac @{thm conjI} 2 *})
txt {*@{subgoals [display]}*}
(*<*)oops(*>*)

text {* 
  Corresponding to @{ML rtac}, there is also the tactic @{ML resolve_tac}, which
  however expects a list of theorems as arguments. From this list it will apply with 
  the first applicable theorem (later theorems that are also applicable can be
  explored via the lazy sequences mechanism). Given the abbreviation
*}

ML{*val resolve_tac_xmp = resolve_tac [@{thm impI}, @{thm conjI}]*}

text {*
  an example for @{ML resolve_tac} is the following proof where first an outermost 
  implication is analysed and then an outermost conjunction.
*}

lemma shows "C \<longrightarrow> (A \<and> B)" and "(A \<longrightarrow> B) \<and> C"
apply(tactic {* resolve_tac_xmp 1 *})
apply(tactic {* resolve_tac_xmp 2 *})
txt{* @{subgoals [display]} *}
(*<*)oops(*>*)

text {* 
  Similarly versions exists for @{ML atac} (@{ML assume_tac}), @{ML etac} 
  (@{ML eresolve_tac}) and so on.

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

text {*
  Also for useful for debugging, but not exclusively, are the tactics @{ML all_tac} and
  @{ML no_tac}. The former always succeeds (but does not change the goal state), and
  the latter always fails.

  (FIXME explain RS MRS)

  Often proofs involve elaborate operations on assumptions and variables
  @{text "\<And>"}-quantified in the goal state. To do such operations on the ML-level 
  using the basic tactics, is very unwieldy and brittle. Some convenience and
  safety is provided by the tactic @{ML SUBPROOF}. This tactic fixes the parameters 
  and binds the various components of a proof state into a record. 
*}

text_raw{*
\begin{figure}
\begin{isabelle}
*}
ML{*fun sp_tac {prems, params, asms, concl, context, schematics} = 
  let 
    val str_of_params = str_of_cterms context params
    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 ("asms: " ^ str_of_asms);
             warning ("concl: " ^ str_of_concl);
             warning ("prems: " ^ 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 extracting strings from @{ML_type cterm}s 
  and @{ML_type thm}s, which are defined in Section~\ref{sec:printing}.\label{fig:sptac}}
\end{figure}
*}

text {*
  To see what happens, assume the function defined in Figure~\ref{fig:sptac}, which
  takes a record as argument and just prints out the content of this record (using the 
  string transformation functions defined in Section~\ref{sec:printing}). Consider
  now the proof
*}

lemma shows "\<And>x y. A x y \<Longrightarrow> B y x \<longrightarrow> C (?z y) x"
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}\\
  asms:       & @{term "A x y"}\\
  concl:      & @{term "B y x \<longrightarrow> C (z y) x"}\\
  prems:      & @{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 parameters in the original goal, they are fixed inside
  the subproof. Similarly the schematic variable @{term z}. The assumption 
  is bound once as @{ML_type cterm} to the record-variable @{text asms} and 
  another time as @{ML_type thm} to @{text prems}.

  Notice also that we had to append @{text "?"} to \isacommand{apply}. The 
  reason is that @{ML SUBPROOF} normally expects that the subgoal is solved completely.
  Since in the function @{ML sp_tac} we returned the tactic @{ML no_tac}, the subproof
  obviously fails. The question-mark allows us to recover from this failure
  in a graceful manner so that the warning messages are not overwritten
  by the error message.

  If we continue the proof script by applying the @{text impI}-rule
*}

apply(rule impI)
apply(tactic {* SUBPROOF sp_tac @{context} 1 *})?

txt {*
  then @{ML SUBPROOF} prints out 

  \begin{quote}\small
  \begin{tabular}{ll}
  params:     & @{term x}, @{term y}\\
  schematics: & @{term z}\\
  asms:       & @{term "A x y"}, @{term "B y x"}\\
  concl:      & @{term "C (z y) x"}\\
  prems:      & @{term "A x y"}, @{term "B y x"}
  \end{tabular}
  \end{quote}
*}
(*<*)oops(*>*)

text {*
  where we now also have @{term "B y x"} as assumption.

  One convenience of @{ML SUBPROOF} is that we can apply assumption
  using the usual tactics, because the parameter @{text prems} 
  contains the assumptions as theorems. With this we can easily 
  implement a tactic that almost behaves like @{ML atac}:
*}

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


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

  A similar but less powerful function is @{ML SUBGOAL}. It allows you to 
  inspect a subgoal specified by a number. 
*}

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

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

text {*
  However, this example is contrived, as there are much simpler ways
  to implement a proof procedure like the one above. They will be explained
  in the next section.

  A variant of @{ML SUBGOAL} is @{ML CSUBGOAL} which allows access to the goal
  as @{ML_type cterm} instead of a @{ML_type term}.
*}


section {* Operations on Tactics *}

text {* @{ML THEN} *}

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

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

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


text {*
  @{ML EVERY} @{ML REPEAT} @{ML DETERM}

  @{ML rewrite_goals_tac}
  @{ML cut_facts_tac}
  @{ML ObjectLogic.full_atomize_tac}
  @{ML ObjectLogic.rulify_tac}
  @{ML resolve_tac}
*}



text {*


  A goal (or goal state) is a special @{ML_type thm}, which by
  convention is an implication of the form:

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

  where @{term C} is the goal to be proved and the @{term "A\<^isub>i"} are the open 
  subgoals. 
  Since the goal @{term C} can potentially be an implication, there is a
  @{text "#"} wrapped around it, which prevents that premises are 
  misinterpreted as open subgoals. The wrapper @{text "# :: prop \<Rightarrow>
  prop"} is just the identity function and used as a syntactic marker. 
  
 

 

  While tactics can operate on the subgoals (the @{text "A\<^isub>i"} above), they 
  are expected to leave the conclusion @{term C} intact, with the 
  exception of possibly instantiating schematic variables. 
 


*}

section {* Structured Proofs *}

lemma True
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