imports Base FirstSteps

  all of them are solved. However, there are also more structured operations

  that help with handling of variables and assumptions.

  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

  The operator @{ML THEN} strings the tactics together.

  To learn more about the function @{ML Goal.prove} see \isccite{sec:results}

  and the file @{ML_file "Pure/goal.ML"}. For more information about the

  internals of goals see \isccite{sec:tactical-goals}.  See @{ML_file

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

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

  Isabelle Reference Manual.

  By using @{text "tactic \<verbopen> \<dots> \<verbclose>"} in the apply-step,

  you can call @{ML foo_tac} or any function that returns a tactic from the

  user level of Isabelle.

  called. For every operator that combines tactics, such a primed version 

  exists. So in the next proof we can first discharge the second subgoal,

  (FIXME: maybe add something about how each goal state is interpreted

  as a theorem)

  The tactic @{ML foo_tac} (and @{ML foo_tac'}) are very specific for

  analysing goals only of the form @{prop "P \<or> Q \<Longrightarrow> Q \<or> P"}. If the goal is not

  of this form, then @{ML foo_tac} throws the error message:

  \begin{isabelle}

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

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

  \end{isabelle}

  Meaning the tactic failed. The reason for this error message is that tactics 

  are functions that map a goal state to a (lazy) sequence of successor states, 

  hence the type of a tactic is

  It is custom that if a tactic fails, it should return the empty sequence: 

  tactics should not raise exceptions willy-nilly.

  The lazy list of possible successor states shows through to 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'}.

  By using \isacommand{back}, we construct the proof that uses the

  second assumption to complete the proof. In more interesting 

  situations, different possibilities can lead to different proofs.

  instead.

text {*

  As seen above, the function @{ML atac} corresponds to the assumption tactic.

*}

lemma shows "P \<Longrightarrow> P"

text {*

  Similarly, @{ML rtac}, @{ML dtac}, @{ML etac} and @{ML ftac} correspond

  to @{ML_text rule}, @{ML_text drule}, @{ML_text erule} and @{ML_text frule}, 

  respectively. Below are three examples with the resulting goal state. How

  they work should therefore be self-explanatory.  

*}

lemma shows "P \<and> Q"

txt{*@{subgoals [display]}*}

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

txt{*@{subgoals [display]}*}

txt{*@{subgoals [display]}*}

  As mentioned above, most basic tactics take a number as argument, which

  addresses to subgoal they are analysing.

*}

lemma shows "Foo" and "P \<and> Q"

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

txt {*@{subgoals [display]}*}

(*<*)oops(*>*)

text {* 

  Corresponding to @{ML rtac}, there is also the tactic @{ML resolve_tac}, which

  however expects a list of theorems as arguments. From this list it will apply with 

  the first applicable theorem (later theorems that are also applicable can be

  explored via the lazy sequences mechanism). Given the abbreviation

ML{*val resolve_tac_xmp = 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_tac_xmp 1 *})

apply(tactic {* resolve_tac_xmp 2 *})

txt{* @{subgoals [display]} *}

(*<*)oops(*>*)

text {* 

  Similarly versions exists for @{ML atac} (@{ML assume_tac}), @{ML etac} 

  (@{ML eresolve_tac}) and so on.

  The tactic @{ML print_tac} is useful for low-level debugging of tactics: it

  prints out a message and the current goal state.

*}

lemma shows "False \<Longrightarrow> True"

text {*

  Also for useful for debugging, but not exclusively, are the tactics @{ML all_tac} and

  @{ML no_tac}. The former always succeeds (but does not change the goal state), and

  the latter always fails.

  (FIXME explain RS MRS)

  Often proofs involve elaborate operations on assumptions and variables

  @{text "\<And>"}-quantified in the goal state. To do such operations on the ML-level 

  using the basic tactics, is very unwieldy and brittle. Some convenience and

  safety is provided by the tactic @{ML SUBPROOF}. This tactic fixes the parameters 

  and binds the various components of a proof state into a record. 

text_raw{*

\begin{figure}

\begin{isabelle}

*}

text_raw{*

\end{isabelle}

\caption{A function that prints out the various parameters provided by the tactic

 @{ML SUBPROOF}. It uses the functions extracting strings from @{ML_type cterm}s 

  and @{ML_type thm}s, which are defined in Section~\ref{sec:printing}.\label{fig:sptac}}

\end{figure}

*}

  To see what happens, assume the function defined in Figure~\ref{fig:sptac}, which

  takes a record as argument and just prints out the content of this record (using the 

  string transformation functions defined in Section~\ref{sec:printing}). Consider

  now the proof

lemma shows "\<And>x y. A x y \<Longrightarrow> B y x \<longrightarrow> C (?z y) x"

  which yields the printout:

  \begin{quote}\small

  \end{quote}

  Note in the actual output the brown colour of the variables @{term x} and 

  @{term y}. Although parameters in the original goal, they are fixed inside

  the subproof. Similarly the schematic variable @{term z}. The assumption 

  is bound once as @{ML_type cterm} to the record-variable @{text asms} and 

  another time as @{ML_type thm} to @{text prems}.

  Notice also that we had to append @{text "?"} to \isacommand{apply}. The 

  reason is that @{ML SUBPROOF} normally expects that the subgoal is solved completely.

  Since in the function @{ML sp_tac} we returned the tactic @{ML no_tac}, the subproof

  obviously fails. The question-mark allows us to recover from this failure

  in a graceful manner so that the warning messages are not overwritten

  by the error message.

  If we continue the proof script by applying the @{text impI}-rule

  then @{ML SUBPROOF} prints out 

  \begin{quote}\small

  \end{quote}

text {*

  where we now also have @{term "B y x"} as assumption.

  One convenience of @{ML SUBPROOF} is that we can apply assumption

  using the usual tactics, because the parameter @{text prems} 

  contains the assumptions as theorems. With this we can easily 

  implement a tactic that almost behaves like @{ML atac}:

*}

lemma shows "\<And>x y. \<lbrakk>B x y; A x y; C x y\<rbrakk> \<Longrightarrow> A x y"

apply(tactic 

       {* SUBPROOF (fn {prems, ...} => resolve_tac prems 1) @{context} 1 *})

txt{* yields

      @{subgoals [display]} *}

(*<*)oops(*>*)

  The restriction in this tactic is that it cannot instantiate any

  schematic variables. This might be seen as a defect, but is actually

  an advantage in the situations for which @{ML SUBPROOF} was designed: 

  the reason is that instantiation of schematic variables can potentially 

  has affect several goals and can render them unprovable.  

  A similar but less powerful function is @{ML SUBGOAL}. It allows you to 

  inspect a subgoal specified by a number. 

ML %linenumbers{*fun select_tac (t,i) =

  case t of

     @{term "Trueprop"} $ t' => select_tac (t',i)

   | @{term "op \<and>"} $ _ $ _ => rtac @{thm conjI} i

   | @{term "op \<longrightarrow>"} $ _ $ _ => rtac @{thm impI} i

   | @{term "Not"} $ _ => rtac @{thm notI} i

   | Const (@{const_name "All"}, _) $ _ => rtac @{thm allI} i

   | _ => no_tac*}

lemma shows "A \<and> B" "A \<longrightarrow> B" "\<forall>x. C x"

apply(tactic {* SUBGOAL select_tac 1 *})

apply(tactic {* SUBGOAL select_tac 3 *})

apply(tactic {* SUBGOAL select_tac 4 *})

txt{* @{subgoals [display]} *}

(*<*)oops(*>*)

text {*

  However, this example is contrived, as there are much simpler ways

  to implement a proof procedure like the one above. They will be explained

  in the next section.

  A variant of @{ML SUBGOAL} is @{ML CSUBGOAL} which allows access to the goal

  as @{ML_type cterm} instead of a @{ML_type term}.

text {* @{ML THEN} *}

lemma shows "(Foo \<and> Bar) \<and> False"

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

                 THEN (rtac @{thm conjI} 1) *})

ML{*val orelse_xmp = (rtac @{thm disjI1} ORELSE' rtac @{thm conjI})*}

lemma shows "True \<and> False" and "Foo \<or> Bar"

apply(tactic {* orelse_xmp 1 *})

apply(tactic {* orelse_xmp 3 *})

  @{ML EVERY} @{ML REPEAT} @{ML DETERM}