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

*}

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.

*}

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

  \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

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

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

*}

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 

  \begin{isabelle}

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

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

  \end{isabelle}

*}

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.

*}

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)

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}

  \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

  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

*}

definition 

  EQ_TRUE 

where

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

lemma test: 

  shows "EQ_TRUE ?X"

  unfolding EQ_TRUE_def

  by (rule refl)

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 

  \begin{isabelle}

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

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

  \end{isabelle}

  \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

*}

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 

*}

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 

*}

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.

*}

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

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

     @{subgoals [display]}

     \end{minipage}*}

(*<*)oops(*>*)

apply(tactic {* etac @{thm conjE} 1 *})

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

     @{subgoals [display]}

     \end{minipage}*}

(*<*)oops(*>*)

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.

*}