ProgTutorial/Tactical.thy
changeset 241 29d4701c5ee1
parent 240 d111f5988e49
child 243 6e0f56764ff8
equal deleted inserted replaced
240:d111f5988e49 241:29d4701c5ee1
    54   (that is @{prop "P \<or> Q \<Longrightarrow> Q \<or> P"} in the proof at hand) under the
    54   (that is @{prop "P \<or> Q \<Longrightarrow> Q \<or> P"} in the proof at hand) under the
    55   assumptions @{text As} (happens to be empty) with the variables
    55   assumptions @{text As} (happens to be empty) with the variables
    56   @{text xs} that will be generalised once the goal is proved (in our case
    56   @{text xs} that will be generalised once the goal is proved (in our case
    57   @{text P} and @{text Q}). The @{text "tac"} is the tactic that proves the goal;
    57   @{text P} and @{text Q}). The @{text "tac"} is the tactic that proves the goal;
    58   it can make use of the local assumptions (there are none in this example). 
    58   it can make use of the local assumptions (there are none in this example). 
    59   The functions @{ML etac}, @{ML rtac} and @{ML atac} in the code above correspond to 
    59   The tactics @{ML etac}, @{ML rtac} and @{ML atac} in the code above correspond 
    60   @{text erule}, @{text rule} and @{text assumption}, respectively. 
    60   roughly to @{text erule}, @{text rule} and @{text assumption}, respectively. 
    61   The operator @{ML THEN} strings the tactics together. 
    61   The operator @{ML THEN} strings the tactics together. 
    62 
    62 
    63   \begin{readmore}
    63   \begin{readmore}
    64   To learn more about the function @{ML Goal.prove} see \isccite{sec:results}
    64   To learn more about the function @{ML Goal.prove} see \isccite{sec:results}
    65   and the file @{ML_file "Pure/goal.ML"}.  See @{ML_file
    65   and the file @{ML_file "Pure/goal.ML"}.  See @{ML_file
   143   \begin{isabelle}
   143   \begin{isabelle}
   144   @{text "*** empty result sequence -- proof command failed"}\\
   144   @{text "*** empty result sequence -- proof command failed"}\\
   145   @{text "*** At command \"apply\"."}
   145   @{text "*** At command \"apply\"."}
   146   \end{isabelle}
   146   \end{isabelle}
   147 
   147 
   148   This means they failed. The reason for this error message is that tactics 
   148   This means they failed.\footnote{To be precise tactics do not produce this error
       
   149   message, the it originates from the \isacommand{apply} wrapper.} The reason for this 
       
   150   error message is that tactics 
   149   are functions mapping a goal state to a (lazy) sequence of successor states. 
   151   are functions mapping a goal state to a (lazy) sequence of successor states. 
   150   Hence the type of a tactic is:
   152   Hence the type of a tactic is:
   151 *}
   153 *}
   152   
   154   
   153 ML{*type tactic = thm -> thm Seq.seq*}
   155 ML{*type tactic = thm -> thm Seq.seq*}
   308   @{text[display] "A\<^isub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^isub>n \<Longrightarrow> (C)"}
   310   @{text[display] "A\<^isub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^isub>n \<Longrightarrow> (C)"}
   309 
   311 
   310   where @{term C} is the goal to be proved and the @{term "A\<^isub>i"} are
   312   where @{term C} is the goal to be proved and the @{term "A\<^isub>i"} are
   311   the subgoals. So after setting up the lemma, the goal state is always of the
   313   the subgoals. So after setting up the lemma, the goal state is always of the
   312   form @{text "C \<Longrightarrow> (C)"}; when the proof is finished we are left with @{text
   314   form @{text "C \<Longrightarrow> (C)"}; when the proof is finished we are left with @{text
   313   "(C)"}. Since the goal @{term C} can potentially be an implication, there is
   315   "(C)"}.\footnote{This only applies to single statements. If the lemma
   314   a ``protector'' wrapped around it (the wrapper is the outermost constant @{text
   316   contains more than one statement, then one has more such implications.} 
   315   "Const (\"prop\", bool \<Rightarrow> bool)"}; however this constant
   317   Since the goal @{term C} can potentially be an implication, there is a
   316   is invisible in the figure). This wrapper prevents that premises of @{text C} are
   318   ``protector'' wrapped around it (the wrapper is the outermost constant
       
   319   @{text "Const (\"prop\", bool \<Rightarrow> bool)"}; however this constant is invisible
       
   320   in the figure). This wrapper prevents that premises of @{text C} are
   317   misinterpreted as open subgoals. While tactics can operate on the subgoals
   321   misinterpreted as open subgoals. While tactics can operate on the subgoals
   318   (the @{text "A\<^isub>i"} above), they are expected to leave the conclusion
   322   (the @{text "A\<^isub>i"} above), they are expected to leave the conclusion
   319   @{term C} intact, with the exception of possibly instantiating schematic
   323   @{term C} intact, with the exception of possibly instantiating schematic
   320   variables. If you use the predefined tactics, which we describe in the next
   324   variables. If you use the predefined tactics, which we describe in the next
   321   section, this will always be the case.
   325   section, this will always be the case.
   360      @{subgoals [display]}
   364      @{subgoals [display]}
   361      \end{minipage}*}
   365      \end{minipage}*}
   362 (*<*)oops(*>*)
   366 (*<*)oops(*>*)
   363 
   367 
   364 text {*
   368 text {*
       
   369   This tactic works however only if the quick-and-dirty mode of Isabelle 
       
   370   is switched on.
       
   371 
   365   Another simple tactic is the function @{ML atac}, which, as shown in the previous
   372   Another simple tactic is the function @{ML atac}, which, as shown in the previous
   366   section, corresponds to the assumption command.
   373   section, corresponds to the assumption command.
   367 *}
   374 *}
   368 
   375 
   369 lemma shows "P \<Longrightarrow> P"
   376 lemma shows "P \<Longrightarrow> P"
   372      @{subgoals [display]}
   379      @{subgoals [display]}
   373      \end{minipage}*}
   380      \end{minipage}*}
   374 (*<*)oops(*>*)
   381 (*<*)oops(*>*)
   375 
   382 
   376 text {*
   383 text {*
   377   Similarly, @{ML rtac}, @{ML dtac}, @{ML etac} and @{ML ftac} correspond
   384   Similarly, @{ML rtac}, @{ML dtac}, @{ML etac} and @{ML ftac} correspond (roughly)
   378   to @{text rule}, @{text drule}, @{text erule} and @{text frule}, 
   385   to @{text rule}, @{text drule}, @{text erule} and @{text frule}, 
   379   respectively. Each of them take a theorem as argument and attempt to 
   386   respectively. Each of them take a theorem as argument and attempt to 
   380   apply it to a goal. Below are three self-explanatory examples.
   387   apply it to a goal. Below are three self-explanatory examples.
   381 *}
   388 *}
   382 
   389 
   459   where the application of rule @{text bspec} generates two subgoals involving the
   466   where the application of rule @{text bspec} generates two subgoals involving the
   460   meta-variable @{text "?x"}. Now, if you are not careful, tactics 
   467   meta-variable @{text "?x"}. Now, if you are not careful, tactics 
   461   applied to the first subgoal might instantiate this meta-variable in such a 
   468   applied to the first subgoal might instantiate this meta-variable in such a 
   462   way that the second subgoal becomes unprovable. If it is clear what the @{text "?x"}
   469   way that the second subgoal becomes unprovable. If it is clear what the @{text "?x"}
   463   should be, then this situation can be avoided by introducing a more
   470   should be, then this situation can be avoided by introducing a more
   464   constraint version of the @{text bspec}-rule. Such constraints can be given by
   471   constrained version of the @{text bspec}-rule. Such constraints can be given by
   465   pre-instantiating theorems with other theorems. One function to do this is
   472   pre-instantiating theorems with other theorems. One function to do this is
   466   @{ML RS}
   473   @{ML RS}
   467   
   474   
   468   @{ML_response_fake [display,gray]
   475   @{ML_response_fake [display,gray]
   469   "@{thm disjI1} RS @{thm conjI}" "\<lbrakk>?P1; ?Q\<rbrakk> \<Longrightarrow> (?P1 \<or> ?Q1) \<and> ?Q"}
   476   "@{thm disjI1} RS @{thm conjI}" "\<lbrakk>?P1; ?Q\<rbrakk> \<Longrightarrow> (?P1 \<or> ?Q1) \<and> ?Q"}
   514   \end{readmore}
   521   \end{readmore}
   515 
   522 
   516   Often proofs on the ML-level involve elaborate operations on assumptions and 
   523   Often proofs on the ML-level involve elaborate operations on assumptions and 
   517   @{text "\<And>"}-quantified variables. To do such operations using the basic tactics 
   524   @{text "\<And>"}-quantified variables. To do such operations using the basic tactics 
   518   shown so far is very unwieldy and brittle. Some convenience and
   525   shown so far is very unwieldy and brittle. Some convenience and
   519   safety is provided by the tactic @{ML SUBPROOF}. This tactic fixes the parameters 
   526   safety is provided by @{ML SUBPROOF}. This tactic fixes the parameters 
   520   and binds the various components of a goal state to a record. 
   527   and binds the various components of a goal state to a record. 
   521   To see what happens, assume the function defined in Figure~\ref{fig:sptac}, which
   528   To see what happens, assume the function defined in Figure~\ref{fig:sptac}, which
   522   takes a record and just prints out the content of this record (using the 
   529   takes a record and just prints out the content of this record (using the 
   523   string transformation functions from in Section~\ref{sec:printing}). Consider
   530   string transformation functions from in Section~\ref{sec:printing}). Consider
   524   now the proof:
   531   now the proof:
   627 txt{* it will produce
   634 txt{* it will produce
   628       @{subgoals [display]} *}
   635       @{subgoals [display]} *}
   629 (*<*)oops(*>*)
   636 (*<*)oops(*>*)
   630 
   637 
   631 text {*
   638 text {*
   632   The restriction in this tactic which is not present in @{ML atac} is 
   639   The restriction in this tactic which is not present in @{ML atac} is that it
   633   that it cannot instantiate any
   640   cannot instantiate any schematic variables. This might be seen as a defect,
   634   schematic variable. This might be seen as a defect, but it is actually
   641   but it is actually an advantage in the situations for which @{ML SUBPROOF}
   635   an advantage in the situations for which @{ML SUBPROOF} was designed: 
   642   was designed: the reason is that, as mentioned before, instantiation of
   636   the reason is that, as mentioned before, instantiation of schematic variables can affect 
   643   schematic variables can affect several goals and can render them
   637   several goals and can render them unprovable. @{ML SUBPROOF} is meant 
   644   unprovable. @{ML SUBPROOF} is meant to avoid this.
   638   to avoid this.
   645 
   639 
   646   Notice that @{ML atac'} inside @{ML SUBPROOF} calls @{ML resolve_tac} with
   640   Notice that @{ML atac'} inside @{ML SUBPROOF} calls @{ML resolve_tac} with 
   647   the subgoal number @{text "1"} and also the outer call to @{ML SUBPROOF} in
   641   the subgoal number @{text "1"} and also the outer call to @{ML SUBPROOF} in 
   648   the \isacommand{apply}-step uses @{text "1"}. This is another advantage of
   642   the \isacommand{apply}-step uses @{text "1"}. This is another advantage 
   649   @{ML SUBPROOF}: the addressing inside it is completely local to the tactic
   643   of @{ML SUBPROOF}: the addressing  inside it is completely 
   650   inside the subproof. It is therefore possible to also apply @{ML atac'} to
   644   local to the tactic inside the subproof. It is therefore possible to also apply 
   651   the second goal by just writing:
   645   @{ML atac'} to the second goal by just writing:
       
   646 *}
   652 *}
   647 
   653 
   648 lemma shows "True" and "\<lbrakk>B x y; A x y; C x y\<rbrakk> \<Longrightarrow> A x y"
   654 lemma shows "True" and "\<lbrakk>B x y; A x y; C x y\<rbrakk> \<Longrightarrow> A x y"
   649 apply(tactic {* atac' @{context} 2 *})
   655 apply(tactic {* atac' @{context} 2 *})
   650 apply(rule TrueI)
   656 apply(rule TrueI)