2 imports Base

     2 imports Base FirstSteps

    15   all of them are solved.

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

    16 

    16   that help with handling of variables and assumptions.

    17 

    53   tac"} sets up a goal state for proving the goal @{text C} under the

    52   tac"} sets up a goal state for proving the goal @{text C} 

    54   assumptions @{text As} (empty in the proof at hand) with the variables

    53   (that is @{prop "P \<or> Q \<Longrightarrow> Q \<or> P"} in the proof at hand) under the

    54   assumptions @{text As} (happens to be empty) with the variables

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

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

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

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

    64   the file @{ML_file "Pure/goal.ML"}. For more information about the internals of goals see 

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

    65   \isccite{sec:tactical-goals}. 

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

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

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

    68   Isabelle Reference Manual.

    95   The apply-step applies the @{ML foo_tac} and therefore solves the goal completely.  

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

    96   Inside @{text "tactic \<verbopen> \<dots> \<verbclose>"} 

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

    97   we can call any function that returns a tactic.

   100   user level of Isabelle.

   114   called. So in the next proof we discharge first the second subgoal,

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

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

   125   The tactic @{ML foo_tac} is very specific for analysing goals of the form

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

   126   @{prop "P \<or> Q \<Longrightarrow> Q \<or> P"}. If the goal is not of this form, then @{ML foo_tac}

   130   as a theorem)

   127   throws the error message about an empty result sequence---meaning the tactic

   131 

   128   failed. The reason for this message is that tactics are functions that map 

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

   129   a goal state to a (lazy) sequence of successor states, hence the type of a 

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

   130   tactic is

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

   135 

   136   \begin{isabelle}

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

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

   139   \end{isabelle}

   140 

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

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

   143   hence the type of a tactic is

   134   Consequently, if a tactic fails, then it returns the empty sequence. This

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

   135   is by the way the default behaviour for a failing tactic; tactics should 

   148   tactics should not raise exceptions willy-nilly.

   136   not raise exceptions.

   149 

   137 

   150   The lazy list of possible successor states shows through to the user-level 

   138   In the following example there are two possibilities for how to apply the tactic.

   151   of Isabelle when using the command \isacommand{back}. For instance in the 

   152   following proof, there are two possibilities for how to apply 

   153   @{ML foo_tac'}.

   147   The application of the tactic results in a sequence of two possible

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

   148   proofs. The Isabelle command \isacommand{back} allows us to explore both 

   163   second assumption to complete the proof. In more interesting 

   149   possibilities.

   164   situations, different possibilities can lead to different proofs.

   150 

   165   

   155   instead. See @{ML_file "Pure/tactic.ML"} and 

   170   instead.

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

   157   combinators; see also Chapters 3 and 4 in 

   158   the old Isabelle Reference Manual.

   166 lemma shows "False \<Longrightarrow> False"

   177 text {*

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

   179 *}

   180 

   181 lemma shows "P \<Longrightarrow> P"

   170 lemma shows "True \<and> True"

   185 text {*

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

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

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

   189   they work should therefore be self-explanatory.  

   190 *}

   191 

   192 lemma shows "P \<and> Q"

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

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

   173 (*<*)oops(*>*)

   195 (*<*)oops(*>*)

   174 

   196 

   175 lemma 

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

   176   shows "Foo"

   177   and "True \<and> True"

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

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

   180 (*<*)oops(*>*)

   181 

   182 lemma shows "False \<and> False \<Longrightarrow> False"

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

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

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

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

   190 (*<*)oops(*>*)

   205 (*<*)oops(*>*)

   191 

   206 

   192 text {*

   207 text {*

   193   similarly @{ML ftac}

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

   194 *}

   209   addresses to subgoal they are analysing.

   195 

   210 *}

   196 text {* diagnostics *} 

   211 

   197 lemma shows "True \<Longrightarrow> False"

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

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

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

   215 (*<*)oops(*>*)

   216 

   217 text {* 

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

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

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

   221   explored via the lazy sequences mechanism). Given the abbreviation

   222 *}

   223 

   224 ML{*val resolve_tac_xmp = resolve_tac [@{thm impI}, @{thm conjI}]*}

   225 

   226 text {*

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

   228   implication is analysed and then an outermost conjunction.

   229 *}

   230 

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

   232 apply(tactic {* resolve_tac_xmp 1 *})

   233 apply(tactic {* resolve_tac_xmp 2 *})

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

   235 (*<*)oops(*>*)

   236 

   237 text {* 

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

   239   (@{ML eresolve_tac}) and so on.

   240 

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

   242   prints out a message and the current goal state.

   243 *}

   244  

   245 lemma shows "False \<Longrightarrow> True"

   201 text {* Let us assume the following four string conversion functions: *}

   249 text {*

   202 

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

   203 ML{*fun str_of_cterm ctxt t =  

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

   204    Syntax.string_of_term ctxt (term_of t)

   252   the latter always fails.

   205 

   253 

   206 fun str_of_cterms ctxt ts =  

   254   (FIXME explain RS MRS)

   207   commas (map (str_of_cterm ctxt) ts)

   255 

   208 

   256   Often proofs involve elaborate operations on assumptions and variables

   209 fun str_of_thm ctxt thm =

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

   210   let

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

   211     val {prop, ...} = crep_thm thm

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

   212   in 

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

   213     str_of_cterm ctxt prop

   261 *}

   214   end

   262 

   215 

   263 text_raw{*

   216 fun str_of_thms ctxt thms =  

   264 \begin{figure}

   217   commas (map (str_of_thm ctxt) thms)*}

   265 \begin{isabelle}

   218 

   266 *}

   219 text {*

   220   and the following function

   221 *}

   222 

   239 

   283 text_raw{*

   240 text {*

   284 \end{isabelle}

   241   then the tactic @{ML SUBPROOF} fixes the parameters and binds the various components

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

   242   of a proof state into a record. For example 

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

   243 *}

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

   244 

   288 \end{figure}

   245 lemma 

   289 *}

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

   290 

   291 text {*

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

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

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

   295   now the proof

   296 *}

   297 

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

   250   prints out 

   302   which yields the printout:

   251 

   303 

   252   \begin{center}

   304   \begin{quote}\small

   260   \end{center}

   312   \end{quote}

   261 

   313 

   262   Continuing the proof script with

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

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

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

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

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

   319 

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

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

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

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

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

   325   by the error message.

   326 

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

   269   prints out 

   334   then @{ML SUBPROOF} prints out 

   270 

   335 

   271   \begin{center}

   336   \begin{quote}\small

   279   \end{center}

   344   \end{quote}

   280 *}

   345 *}

   281 (*<*)oops(*>*)

   346 (*<*)oops(*>*)

   282 

   347 

   283 

   348 text {*

   284 text {*

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

   285   @{ML PRIMITIVE}? @{ML SUBGOAL} see page 32 in ref

   350 

   286 *}

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

   287 

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

   288 text {* 

   353   contains the assumptions as theorems. With this we can easily 

   289   @{ML all_tac} @{ML no_tac}

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

   290 *}

   355 *}

   356 

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

   358 apply(tactic 

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

   360 txt{* yields

   361       @{subgoals [display]} *}

   362 (*<*)oops(*>*)

   363 

   364 

   365 text {*

   366   The restriction in this tactic is that it cannot instantiate any

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

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

   369   the reason is that instantiation of schematic variables can potentially 

   370   has affect several goals and can render them unprovable.  

   371 

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

   373   inspect a subgoal specified by a number. 

   374 *}

   375 

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

   377   case t of

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

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

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

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

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

   383    | _ => no_tac*}

   384 

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

   386 apply(tactic {* SUBGOAL select_tac 1 *})

   387 apply(tactic {* SUBGOAL select_tac 3 *})

   388 apply(tactic {* SUBGOAL select_tac 4 *})

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

   390 (*<*)oops(*>*)

   391 

   392 text {*

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

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

   395   in the next section.

   396 

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

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

   399 *}

   400 

   294 text {* THEN *}

   404 text {* @{ML THEN} *}

   295 

   405 

   296 lemma shows "(True \<and> True) \<and> False"

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

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

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

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

   301 lemma shows "True \<and> False"

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

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

   413 

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

   415 apply(tactic {* orelse_xmp 1 *})

   416 apply(tactic {* orelse_xmp 3 *})

   308   @{ML EVERY} @{ML REPEAT} 

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