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

*}

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 

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

  \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

  @{ML_response_fake [gray,display]

  "disjE"

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

  @{ML_response_fake [gray,display]

  "thm \"disjE\""

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

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

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

  These problems can be 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 

  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.

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

*}

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

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

*}

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

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

lemma test: 

  shows "EQ_TRUE ?X"

text {*

  Although Isabelle issues a warning message when stating goals involving 

  meta-variables, it is possible to prove this theorem. The reason for the warning 

  message is that 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"} 

  \begin{readmore}

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

  \end{readmore}

*}

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

text {*

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

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

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

  is switched on. This is done automatically in the ``interactive

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

*}

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

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