theory Tactical

imports Base FirstSteps

begin

chapter {* Tactical Reasoning\label{chp:tactical} *}

text {*

*}

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. 

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

  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

*}

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

*}

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 

  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

  \begin{isabelle}

  @{text "*** empty result sequence -- proof command failed"}\\

  @{text "*** At command \"apply\"."}

  \end{isabelle}

  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: 

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

  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

*}

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  

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

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

*}

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

*}

lemma shows "Foo" and "P \<and> Q"

apply(tactic {* rtac @{thm conjI} 2 *})

txt {*\begin{minipage}{\textwidth}

      @{subgoals [display]}

      \end{minipage}*}

(*<*)oops(*>*)

text {* 

*}

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} 

*}

text {*

  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. 

*}

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

\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 

  the subproof. Similarly the schematic variable @{term z}. The assumption 

  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