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

  into ML. Suppose 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_ind "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}).\footnote{FIXME: explain prove earlier} 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 tactics @{ML_ind etac}, @{ML_ind rtac} and

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

  rule} and @{text assumption}, respectively. The operator @{ML_ind THEN}

  strings the tactics together.

  \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. Many theorems also have ML-bindings with the same name. Therefore,

  we could also just have written @{ML "etac disjE 1"}, or in case where there

  is no ML-binding obtain the theorem dynamically using the function @{ML

  thm}; for example \mbox{@{ML "etac (thm \"disjE\") 1"}}. Both ways however

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

*}

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'} is used instead of @{ML THEN}. 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 "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. For most operators that combine tactics 

  (@{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 these tactics return the error message:

  \begin{isabelle}

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

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

  \end{isabelle}

  This means they failed.\footnote{To be precise, tactics do not produce this error

  message, it originates from the \isacommand{apply} wrapper.} 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} and @{ML_ind  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 

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

  val _ = tracing (string_of_thm_no_vars ctxt thm)

in 

  Seq.single thm

end*}

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

*}

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. Consider now 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 an @{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. If you use the predefined tactics, which we describe in the next

  section, this will always be the case.

  \begin{readmore}

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

  \end{readmore}

*}

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

text {*

  Let us start with explaining the simple tactic @{ML_ind  print_tac}, 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:\medskip

     \begin{minipage}{\textwidth}\small

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

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

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

     \end{minipage}

   *}

(*<*)oops(*>*)

text {*

  A simple tactic for easy discharge of any proof obligations is 

  the Isabelle command \isacommand{sorry} and is sometimes useful  

  during the development of tactics.

*}

lemma shows "False" and "Goldbach_conjecture"  

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

     @{subgoals [display]}

     \end{minipage}*}

(*<*)oops(*>*)

text {*

  This tactic works however only if the quick-and-dirty mode of Isabelle 

  is switched on.

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

  section, corresponds to the assumption command.

*}

lemma shows "P \<Longrightarrow> P"

apply(tactic {* atac 1 *})

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

     @{subgoals [display]}

     \end{minipage}*}

(*<*)oops(*>*)

text {*

  Similarly, @{ML_ind  rtac}, @{ML_ind  dtac}, @{ML_ind  etac} and 

  @{ML_ind  ftac} 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} is similar to @{ML_ind  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_xmp_tac = 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_xmp_tac 1 *})

apply(tactic {* resolve_xmp_tac 2 *})

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

     @{subgoals [display]} 

     \end{minipage}*}

(*<*)oops(*>*)

text {* 

  Similar versions taking a list of theorems exist for the tactics 

  @{ML dtac} (@{ML_ind  dresolve_tac}), @{ML etac} 

  (@{ML_ind  eresolve_tac}) and so on.

  Another simple tactic is @{ML_ind  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{*produces the goal state\medskip

     \begin{minipage}{\textwidth}

     @{subgoals [display]} 

     \end{minipage}*}

(*<*)oops(*>*)

text {*

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

  procedure might become too fragile, if it just applies inference rules as 

  shown above. The reason is that a number of rules introduce meta-variables 

  into the goal state. Consider for example the proof

*}

lemma shows "\<forall>x \<in> A. P x \<Longrightarrow> Q x"

apply(tactic {* dtac @{thm bspec} 1 *})

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

     @{subgoals [display]} 

     \end{minipage}*}

(*<*)oops(*>*)

text {*

  where the application of rule @{text bspec} generates two subgoals involving the

  meta-variable @{text "?x"}. Now, if you are not careful, tactics 

  applied to the first subgoal might instantiate this meta-variable in such a 

  way that the second subgoal becomes unprovable. If it is clear what the @{text "?x"}

  should be, then this situation can be avoided by introducing a more

  constrained version of the @{text bspec}-rule. Such constraints can be given by

  pre-instantiating theorems with other theorems. One function to do this is

  @{ML_ind "RS"}

  @{ML_response_fake [display,gray]

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