theory Tactical

imports Base First_Steps

begin

chapter \<open>Tactical Reasoning\label{chp:tactical}\<close>

text \<open>

   \begin{flushright}

  {\em

  ``The first thing I would say is that when you write a program, think of\\ 

   it primarily as a work of literature. You're trying to write something\\ 

   that human beings are going to read. Don't think of it primarily as\\  

   something a computer is going to follow. The more effective you are\\ 

   at making your program readable, the more effective it's going to\\  

   be: You'll understand it today, you'll understand it next week, and\\ 

   your successors who are going to maintain and modify it will\\ 

   understand it.''}\\[1ex]

  Donald E.~Knuth, from an interview in Dr.~Dobb's Journal, 1996.

  \end{flushright}

  One of the main reason for descending to the ML-level of Isabelle is 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 explain how to implement simple tactics and how to combine them using

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

\<close>

section \<open>Basics of Reasoning with Tactics\label{sec:basictactics}\<close>

text \<open>

  To see how tactics work, let us first transcribe a simple \isacommand{apply}-style proof 

  into ML. Suppose the following proof.

\<close>

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

  This proof translates to the following ML-code.

@{ML_matchresult_fake [display,gray]

  val ctxt = @{context}

in

   (fn _ =>  eresolve_tac @{context} [@{thm disjE}] 1

             THEN resolve_tac @{context} [@{thm disjI2}] 1

             THEN assume_tac @{context} 1

             THEN resolve_tac @{context} [@{thm disjI1}] 1

             THEN assume_tac @{context} 1)

  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 \<open>P\<close> and

  \<open>Q\<close>). 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 eresolve_tac in Tactic}, @{ML_ind resolve_tac in Tactic} and

  @{ML_ind assume_tac in Tactic} in the code above correspond roughly to \<open>erule\<close>, \<open>rule\<close> and \<open>assumption\<close>, respectively. The combinator

  @{ML THEN} strings the tactics together.

  TBD: Write something about @{ML_ind prove_common 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}

  \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}\<open>(tactic \<verbopen> \<dots> \<verbclose>)\<close>. 

  Consider the following sequence of tactics

\<close>

ML %grayML\<open>fun foo_tac ctxt = 

      (eresolve_tac ctxt [@{thm disjE}] 1

       THEN resolve_tac  ctxt [@{thm disjI2}] 1

       THEN assume_tac  ctxt 1

       THEN resolve_tac ctxt [@{thm disjI1}] 1

       THEN assume_tac  ctxt 1)\<close>

text \<open>and the Isabelle proof:\<close>

lemma 

  shows "P \<or> Q \<Longrightarrow> Q \<or> P"

apply(tactic \<open>foo_tac @{context}\<close>)

done

text \<open>

  By using \<open>tactic \<verbopen> \<dots> \<verbclose>\<close> 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 transformations

  that are performed by \<open>tactic\<close>. They can be avoided by using 

  \<open>raw_tactic\<close> 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 (\<open>1\<close> 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

\<close>

ML %grayML\<open>fun foo_tac' ctxt = 

      (eresolve_tac ctxt [@{thm disjE}] 

       THEN' resolve_tac ctxt [@{thm disjI2}] 

       THEN' assume_tac ctxt 

       THEN' resolve_tac ctxt [@{thm disjI1}] 

       THEN' assume_tac ctxt)\<close>text_raw\<open>\label{tac:footacprime}\<close>

text \<open>

  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

  then the first.

\<close>

lemma 

  shows "P1 \<or> Q1 \<Longrightarrow> Q1 \<or> P1"

  and   "P2 \<or> Q2 \<Longrightarrow> Q2 \<or> P2"

apply(tactic \<open>foo_tac' @{context} 2\<close>)

apply(tactic \<open>foo_tac' @{context} 1\<close>)

done

text \<open>

  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 specific

  to goals 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}

  \<open>*** empty result sequence -- proof command failed\<close>\\

  \<open>*** At command "apply".\<close>

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

\<close>

ML %grayML\<open>type tactic = thm -> thm Seq.seq\<close>

text \<open>

  By convention, if a tactic fails, then 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 \<open>THM\<close>.

  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

\<close>

ML %grayML\<open>fun no_tac thm = Seq.empty\<close>

text \<open>

  which means @{ML no_tac} always fails. The second returns the given theorem wrapped 

  in a single member sequence; it is defined as

\<close>

ML %grayML\<open>fun all_tac thm = Seq.single thm\<close>

text \<open>

  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.

\<close>

lemma 

  shows "\<lbrakk>P \<or> Q; P \<or> Q\<rbrakk> \<Longrightarrow> Q \<or> P"

apply(tactic \<open>foo_tac' @{context} 1\<close>)

back

done

text \<open>

  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

\<close>

ML %grayML\<open>fun my_print_tac ctxt thm =

let

  val _ = tracing (Pretty.string_of (pretty_thm_no_vars ctxt thm))

in 

  Seq.single thm

end\<close>

text \<open>

  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\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^sub>n \<Longrightarrow> #C"}

  where @{term C} is the goal to be proved and the @{term "A\<^sub>i"} are

  the subgoals. So after setting up the lemma, the goal state is always of the

  form \<open>C \<Longrightarrow> #C\<close>; when the proof is finished we are left with \<open>#C\<close>. Since the goal @{term C} can potentially be an implication, there is a

  ``protector'' wrapped around it (the wrapper is the outermost constant

  \<open>Const ("Pure.prop", bool \<Rightarrow> bool)\<close>; in the figure we make it visible

  as a \<open>#\<close>). This wrapper prevents that premises of \<open>C\<close> are

  misinterpreted as open subgoals. While tactics can operate on the subgoals

  (the \<open>A\<^sub>i\<close> 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.

\<close>

text_raw \<open>

  \begin{figure}[p]

  \begin{boxedminipage}{\textwidth}

  \begin{isabelle}

\<close>

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

lemma 

  shows "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B" 

apply(tactic \<open>my_print_tac @{context}\<close>)

txt\<open>\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

\<close>

apply(rule conjI)

apply(tactic \<open>my_print_tac @{context}\<close>)

txt\<open>\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

\<close>

apply(assumption)

apply(tactic \<open>my_print_tac @{context}\<close>)

txt\<open>\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

\<close>

apply(assumption)

apply(tactic \<open>my_print_tac @{context}\<close>)

txt\<open>\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   

\<close>

(*<*)oops(*>*)

text_raw \<open>

  \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{\<open>\<lbrakk>A; B\<rbrakk> \<Longrightarrow>

  A \<and> B\<close>} the theorem is \<open>(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B) \<Longrightarrow> #(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B)\<close>; when

  you finish the proof the theorem is \<open>#(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and>

  B)\<close>.\label{fig:goalstates}}

  \end{figure}

\<close>

definition 

  EQ_TRUE 

where

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

schematic_goal test: 

  shows "EQ_TRUE ?X"

unfolding EQ_TRUE_def

by (rule refl)

text \<open>

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

  meta-variables on the user level. However, the proved theorem is not \<open>EQ_TRUE ?X\<close>, 

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

  \begin{isabelle}

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

  \<open>>\<close>~@{thm test}

  \end{isabelle}

  The reason for this result is that the schematic variable \<open>?X\<close> 

  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}

\<close>

section \<open>Simple Tactics\label{sec:simpletacs}\<close>

text \<open>

  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

\<close>

lemma 

  shows "False \<Longrightarrow> True"

apply(tactic \<open>print_tac @{context} "foo message"\<close>)

txt\<open>gives:

     \begin{isabelle}

     \<open>foo message\<close>\\[3mm] 

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

     \<open> 1. False \<Longrightarrow> True\<close>\\

     \end{isabelle}

\<close>

(*<*)oops(*>*)

text \<open>

  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_structure Skip_Proof}. 

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

  sometimes useful during the development of tactics.

\<close>

lemma 

  shows "False" and "Goldbach_conjecture"  

apply(tactic \<open>Skip_Proof.cheat_tac @{context} 1\<close>)

txt\<open>\begin{minipage}{\textwidth}

     @{subgoals [display]}

     \end{minipage}\<close>

(*<*)oops(*>*)

text \<open>

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

  earlier, corresponds to the assumption method.

\<close>

lemma 

  shows "P \<Longrightarrow> P"

apply(tactic \<open>assume_tac @{context} 1\<close>)

txt\<open>\begin{minipage}{\textwidth}

     @{subgoals [display]}

     \end{minipage}\<close>

(*<*)oops(*>*)

text \<open>

  Similarly, @{ML_ind resolve_tac in Tactic}, @{ML_ind dresolve_tac in Tactic}, @{ML_ind eresolve_tac

  in Tactic} and @{ML_ind forward_tac in Tactic} correspond (roughly) to \<open>rule\<close>, \<open>drule\<close>, \<open>erule\<close> and \<open>frule\<close>, respectively. Each of

  them takes a theorem as argument and attempts to apply it to a goal. Below

  are three self-explanatory examples.

\<close>

lemma 

  shows "P \<and> Q"

apply(tactic \<open>resolve_tac @{context} [@{thm conjI}] 1\<close>)

txt\<open>\begin{minipage}{\textwidth}

     @{subgoals [display]}

     \end{minipage}\<close>

(*<*)oops(*>*)

lemma 

  shows "P \<and> Q \<Longrightarrow> False"

apply(tactic \<open>eresolve_tac @{context} [@{thm conjE}] 1\<close>)

txt\<open>\begin{minipage}{\textwidth}

     @{subgoals [display]}

     \end{minipage}\<close>

(*<*)oops(*>*)

lemma 

  shows "False \<and> True \<Longrightarrow> False"

apply(tactic \<open>dresolve_tac @{context} [@{thm conjunct2}] 1\<close>)

txt\<open>\begin{minipage}{\textwidth}

     @{subgoals [display]}

     \end{minipage}\<close>

(*<*)oops(*>*)

text \<open>

  The function @{ML_ind resolve_tac in Tactic} 

  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

\<close>

ML %grayML\<open>fun resolve_xmp_tac ctxt = resolve_tac ctxt [@{thm impI}, @{thm conjI}]\<close>

text \<open>

  an example for @{ML resolve_tac} is the following proof where first an outermost 

  implication is analysed and then an outermost conjunction.

\<close>

lemma 

  shows "C \<longrightarrow> (A \<and> B)" 

  and   "(A \<longrightarrow> B) \<and> C"

apply(tactic \<open>resolve_xmp_tac @{context} 1\<close>)

apply(tactic \<open>resolve_xmp_tac @{context} 2\<close>)

txt\<open>\begin{minipage}{\textwidth}

     @{subgoals [display]} 

     \end{minipage}\<close>

(*<*)oops(*>*)

text \<open>

  Similar versions taking a list of theorems exist for the tactics