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 

*}

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}

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

  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 function @{ML thm}; for example 

  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

  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 

  (@{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. 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 

  as a single member sequence; @{ML all_tac} is defined as

*}

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

text {*

  which means it 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 

  @{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. In more interesting situations, only by exploring 

  different possibilities one might be able to find a proof.

  \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

  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{minipage}[t]{0.3\textwidth}

      @{subgoals [display]} 

      \end{minipage} &

*}

apply(rule conjI)

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

txt{* \small 

      \begin{minipage}[t]{0.26\textwidth}

      @{subgoals [display]} 

      \end{minipage} &

*}

apply(assumption)

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

txt{* \small 

      \begin{minipage}[t]{0.3\textwidth}

      @{subgoals [display]} 

      \end{minipage} &

*}

apply(assumption)

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

txt{* \small 

      \begin{minipage}[t]{0.3\textwidth}

      @{subgoals [display]} 

      \end{minipage} &

*}

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

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

*}

section {* Simple Tactics *}

text {*

  A simple tactic is @{ML print_tac}, which is quite 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" *})

txt{*\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 *})

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 analyse 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. 

  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{*\begin{minipage}{\textwidth}

     @{subgoals [display]} 

     \end{minipage}*}

(*<*)oops(*>*)

text {*

  Since rules are applied using higher-order unification, an automatic proof

  @{ML_response_fake [display,gray]

  "@{thm disjI1} RS @{thm conjI}" "\<lbrakk>?P1; ?Q\<rbrakk> \<Longrightarrow> (?P1 \<or> ?Q1) \<and> ?Q"}

  @{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"}

  the function raises an exception. The function @{ML RSN} is similar, but 

  takes a number as argument and thus you can make 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. 

  This means for the first @{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 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 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}