theory Tactical

imports Base FirstSteps

begin

(*<*)

setup{*

open_file_with_prelude 

  "Tactical_Code.thy"

  ["theory Tactical", "imports Base FirstSteps", "begin"]

*}

(*>*)

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

text {*

  One of the main reason for descending to the ML-level of Isabelle is to be

  able to implement automatic proof procedures. Such proof procedures can

  considerably lessen the burden of manual reasoning. They are centred around

  the idea of 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 discharged.

  In this chapter we will explain simple tactics and how to combine them using

  tactic combinators. We also describe the simplifier, simprocs and conversions.

*}

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: 

  shows "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_ind prove in Goal} sets up a goal

  state for proving the goal @{prop "P \<or> Q \<Longrightarrow> Q \<or> P"}. We can give this

  function some assumptions in the third argument (there are no assumption in

  the proof at hand). The second argument stands for a list of variables

  (given as strings). This list contains the variables that will be turned

  into schematic variables once the goal is proved (in our case @{text P} and

  @{text Q}). The last argument is the tactic that proves the goal. This

  tactic can make use of the local assumptions (there are none in this

  example). The tactics @{ML_ind etac in Tactic}, @{ML_ind rtac in Tactic} and

  @{ML_ind atac in Tactic} in the code above correspond roughly to @{text

  erule}, @{text rule} and @{text assumption}, respectively. The combinator

  @{ML THEN} strings the tactics together.

  TBD: Write something about @{ML_ind prove_multi in Goal}.

  \begin{readmore}

  To learn more about the function @{ML_ind prove in Goal} see

  \isccite{sec:results} and the file @{ML_file "Pure/goal.ML"}.  See @{ML_file

  "Pure/tactic.ML"} and @{ML_file "Pure/tactical.ML"} for the code of basic

  tactics and tactic combinators; see also Chapters 3 and 4 in the old

  Isabelle Reference Manual, and Chapter 3 in the Isabelle/Isar Implementation

  Manual.

  \end{readmore}

  Note that in the code above we use antiquotations for referencing the

  theorems. We  could also just have written @{ML "etac disjE 1"} because 

  many of the basic theorems have a corresponding ML-binding:

  @{ML_response_fake [gray,display]

  "disjE"

  "\<lbrakk>?P \<or> ?Q; ?P \<Longrightarrow> ?R; ?Q \<Longrightarrow> ?R\<rbrakk> \<Longrightarrow> ?R"}

  In case where no ML-binding exists, theorems can also be looked up dynamically 

  using the function @{ML thm} and the (string) name of the theorem. For example: 

  @{ML_response_fake [gray,display]

  "thm \"disjE\""

  "\<lbrakk>?P \<or> ?Q; ?P \<Longrightarrow> ?R; ?Q \<Longrightarrow> ?R\<rbrakk> \<Longrightarrow> ?R"}

  Both ways however are considered \emph{bad} style! The reason is that the binding

  for @{ML disjE} can be re-assigned and thus one does not have

  complete control over which theorem is actually applied. Similarly with the

  lookup of @{text [quotes] "disjE"}. Although theorems must have a unique name

  in the theorem database, the string can stand for a dynamically updatable

  theorem list. Also in this case we cannot be sure which theorem is applied.

  These problems can be nicely prevented by using antiquotations

  @{ML_response_fake [gray,display]

  "@{thm \"disjE\"}"

  "\<lbrakk>?P \<or> ?Q; ?P \<Longrightarrow> ?R; ?Q \<Longrightarrow> ?R\<rbrakk> \<Longrightarrow> ?R"}

  because then the theorems are fixed statically at compile-time.

  \index{tactic@ {\tt\slshape{}tactic}}

  \index{raw\_tactic@ {\tt\slshape{}raw\_tactic}}

  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 

  shows "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. There are some goal transformation

  that are performed by @{text "tactic"}. They can be avoided by using 

  @{text "raw_tactic"} instead.

  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_raw{*\label{tac:footacprime}*}

text {* 

  where @{ML_ind THEN' in Tactical} is used instead of @{ML THEN in

  Tactical}. (For most combinators that combine tactics---@{ML THEN} is only

  one such combinator---a ``primed'' version exists.)  With @{ML foo_tac'} you

  can 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 

  shows "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. 

  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 these tactics return the error message:\footnote{To be

  precise, tactics do not produce this error message; the message originates from the

  \isacommand{apply} wrapper that calls the tactic.}

  \begin{isabelle}

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

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

  \end{isabelle}

  This means they 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_ind no_tac in Tactical} and 

  @{ML_ind all_tac in Tactical}. 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 

  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 

  shows "\<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

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}. With this

  tactic we are in the position to inspect every goal state in a proof. For

  this consider 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 (the wrapper is the outermost constant

  @{text "Const (\"prop\", bool \<Rightarrow> bool)"}; in the figure we make it visible

  as a @{text #}). This wrapper 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. This instantiations of schematic variables can be observed 

  on the user level. Have a look at the following definition and proof.

*}

text_raw {*

  \begin{figure}[p]

  \begin{boxedminipage}{\textwidth}

  \begin{isabelle}

*}

notation (output) "prop"  ("#_" [1000] 1000)

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

      @{raw_goal_state}

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

      @{raw_goal_state}

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

      @{raw_goal_state}

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

      @{raw_goal_state}

      \end{tabular}}

      \end{minipage}\medskip   

   *}

(*<*)oops(*>*)

text_raw {*  

  \end{isabelle}

  \end{boxedminipage}

  \caption{The figure shows an Isabelle snippet of 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 tactic shows that every goal state in Isabelle is

  represented by a theorem: when you 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

  you finish the proof the theorem is @{text "#(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and>

  B)"}.\label{fig:goalstates}}

  \end{figure}

*}

definition 

  EQ_TRUE 

where

  "EQ_TRUE X \<equiv> (X = True)"

schematic_lemma test: 

  shows "EQ_TRUE ?X"

unfolding EQ_TRUE_def

by (rule refl)

text {*

  By using \isacommand{schematic\_lemma} it is possible to prove lemmas including

  meta-variables on the user level. However, the proved theorem is not @{text "EQ_TRUE ?X"}, 

  as one might expect, but @{thm test}. We can test this with:

  \begin{isabelle}

  \isacommand{thm}~@{thm [source] test}\\

  @{text ">"}~@{thm test}

  \end{isabelle}

  The reason for this result is that the schematic variable @{text "?X"} 

  is instantiated inside the proof to be @{term True} and then the 

  instantiation propagated to the ``outside''.

  \begin{readmore}

  For more information about the internals of goals see \isccite{sec:tactical-goals}.

  \end{readmore}

*}

section {* Simple Tactics\label{sec:simpletacs} *}

text {*

  In this section we will introduce more of the simple tactics in Isabelle. The 

  first one is @{ML_ind print_tac in Tactical}, which is quite useful 

  for low-level debugging of tactics. It just prints out a message and the current 

  goal state. Unlike @{ML my_print_tac} shown earlier, it prints the goal state 

  as the user would see it.  For example, processing the proof

*}

lemma 

  shows "False \<Longrightarrow> True"

apply(tactic {* print_tac "foo message" *})

txt{*gives:

     \begin{isabelle}

     @{text "foo message"}\\[3mm] 

     @{prop "False \<Longrightarrow> True"}\\

     @{text " 1. False \<Longrightarrow> True"}\\

     \end{isabelle}

   *}

(*<*)oops(*>*)

text {*

  A simple tactic for easy discharge of any proof obligations, even difficult ones, is 

  @{ML_ind cheat_tac in Skip_Proof} in the structure @{ML_struct Skip_Proof}. 

  This tactic corresponds to the Isabelle command \isacommand{sorry} and is 

  sometimes useful during the development of tactics.

*}

lemma 

  shows "False" and "Goldbach_conjecture"  

apply(tactic {* Skip_Proof.cheat_tac @{theory} *})

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

     @{subgoals [display]}

     \end{minipage}*}

(*<*)oops(*>*)

text {*

  Another simple tactic is the function @{ML_ind atac in Tactic}, which, as shown 

  earlier, corresponds to the assumption method.

*}

lemma 

  shows "P \<Longrightarrow> P"

apply(tactic {* atac 1 *})

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

     @{subgoals [display]}

     \end{minipage}*}

(*<*)oops(*>*)

text {*

  Similarly, @{ML_ind rtac in Tactic}, @{ML_ind dtac in Tactic}, @{ML_ind etac

  in Tactic} and @{ML_ind ftac in Tactic} correspond (roughly) 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 {*

  The function @{ML_ind resolve_tac in Tactic} is similar to @{ML rtac}, except that it

  expects a list of theorems as argument. 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_xmp_tac = resolve_tac [@{thm impI}, @{thm conjI}]*}