ProgTutorial/Tactical.thy
changeset 256 1fb8d62c88a0
parent 255 ef1da1abee46
child 288 d6e9fb662d68
equal deleted inserted replaced
255:ef1da1abee46 256:1fb8d62c88a0
    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 tactics @{ML etac}, @{ML rtac} and @{ML atac} in the code above correspond 
    59   The tactics @{ML [index] etac}, @{ML [index] rtac} and @{ML [index] atac} in the code above correspond 
    60   roughly to @{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 [index] 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 [index] prove in Goal} 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
    66   "Pure/tactic.ML"} and @{ML_file "Pure/tctical.ML"} for the code of basic
    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
    67   tactics and tactic combinators; see also Chapters 3 and 4 in the old
    68   Isabelle Reference Manual, and Chapter 3 in the Isabelle/Isar Implementation Manual. 
    68   Isabelle Reference Manual, and Chapter 3 in the Isabelle/Isar Implementation Manual. 
    69   \end{readmore}
    69   \end{readmore}
   117        THEN' atac 
   117        THEN' atac 
   118        THEN' rtac @{thm disjI1} 
   118        THEN' rtac @{thm disjI1} 
   119        THEN' atac)*}text_raw{*\label{tac:footacprime}*}
   119        THEN' atac)*}text_raw{*\label{tac:footacprime}*}
   120 
   120 
   121 text {* 
   121 text {* 
   122   where @{ML THEN'} is used instead of @{ML THEN}. With @{ML foo_tac'} you can give 
   122   where @{ML [index] THEN'} is used instead of @{ML THEN}. With @{ML foo_tac'} you can give 
   123   the number for the subgoal explicitly when the tactic is
   123   the number for the subgoal explicitly when the tactic is
   124   called. So in the next proof you can first discharge the second subgoal, and
   124   called. So in the next proof you can first discharge the second subgoal, and
   125   subsequently the first.
   125   subsequently the first.
   126 *}
   126 *}
   127 
   127 
   158   By convention, if a tactic fails, then it should return the empty sequence. 
   158   By convention, if a tactic fails, then it should return the empty sequence. 
   159   Therefore, if you write your own tactics, they  should not raise exceptions 
   159   Therefore, if you write your own tactics, they  should not raise exceptions 
   160   willy-nilly; only in very grave failure situations should a tactic raise the 
   160   willy-nilly; only in very grave failure situations should a tactic raise the 
   161   exception @{text THM}.
   161   exception @{text THM}.
   162 
   162 
   163   The simplest tactics are @{ML no_tac} and @{ML all_tac}. The first returns
   163   The simplest tactics are @{ML [index] no_tac} and @{ML [index] all_tac}. The first returns
   164   the empty sequence and is defined as
   164   the empty sequence and is defined as
   165 *}
   165 *}
   166 
   166 
   167 ML{*fun no_tac thm = Seq.empty*}
   167 ML{*fun no_tac thm = Seq.empty*}
   168 
   168 
   331 *}
   331 *}
   332 
   332 
   333 section {* Simple Tactics\label{sec:simpletacs} *}
   333 section {* Simple Tactics\label{sec:simpletacs} *}
   334 
   334 
   335 text {*
   335 text {*
   336   Let us start with explaining the simple tactic @{ML print_tac}, which is quite useful 
   336   Let us start with explaining the simple tactic @{ML [index] print_tac}, which is quite useful 
   337   for low-level debugging of tactics. It just prints out a message and the current 
   337   for low-level debugging of tactics. It just prints out a message and the current 
   338   goal state. Unlike @{ML my_print_tac} shown earlier, it prints the goal state 
   338   goal state. Unlike @{ML my_print_tac} shown earlier, it prints the goal state 
   339   as the user would see it.  For example, processing the proof
   339   as the user would see it.  For example, processing the proof
   340 *}
   340 *}
   341  
   341  
   351    *}
   351    *}
   352 (*<*)oops(*>*)
   352 (*<*)oops(*>*)
   353 
   353 
   354 text {*
   354 text {*
   355   A simple tactic for easy discharge of any proof obligations is 
   355   A simple tactic for easy discharge of any proof obligations is 
   356   @{ML SkipProof.cheat_tac}. This tactic corresponds to
   356   @{ML [index] cheat_tac in SkipProof}. This tactic corresponds to
   357   the Isabelle command \isacommand{sorry} and is sometimes useful  
   357   the Isabelle command \isacommand{sorry} and is sometimes useful  
   358   during the development of tactics.
   358   during the development of tactics.
   359 *}
   359 *}
   360 
   360 
   361 lemma shows "False" and "Goldbach_conjecture"  
   361 lemma shows "False" and "Goldbach_conjecture"  
   367 
   367 
   368 text {*
   368 text {*
   369   This tactic works however only if the quick-and-dirty mode of Isabelle 
   369   This tactic works however only if the quick-and-dirty mode of Isabelle 
   370   is switched on.
   370   is switched on.
   371 
   371 
   372   Another simple tactic is the function @{ML atac}, which, as shown in the previous
   372   Another simple tactic is the function @{ML [index] atac}, which, as shown in the previous
   373   section, corresponds to the assumption command.
   373   section, corresponds to the assumption command.
   374 *}
   374 *}
   375 
   375 
   376 lemma shows "P \<Longrightarrow> P"
   376 lemma shows "P \<Longrightarrow> P"
   377 apply(tactic {* atac 1 *})
   377 apply(tactic {* atac 1 *})
   379      @{subgoals [display]}
   379      @{subgoals [display]}
   380      \end{minipage}*}
   380      \end{minipage}*}
   381 (*<*)oops(*>*)
   381 (*<*)oops(*>*)
   382 
   382 
   383 text {*
   383 text {*
   384   Similarly, @{ML rtac}, @{ML dtac}, @{ML etac} and @{ML ftac} correspond (roughly)
   384   Similarly, @{ML [index] rtac}, @{ML [index] dtac}, @{ML [index] etac} and 
       
   385   @{ML [index] ftac} correspond (roughly)
   385   to @{text rule}, @{text drule}, @{text erule} and @{text frule}, 
   386   to @{text rule}, @{text drule}, @{text erule} and @{text frule}, 
   386   respectively. Each of them take a theorem as argument and attempt to 
   387   respectively. Each of them take a theorem as argument and attempt to 
   387   apply it to a goal. Below are three self-explanatory examples.
   388   apply it to a goal. Below are three self-explanatory examples.
   388 *}
   389 *}
   389 
   390 
   407      @{subgoals [display]}
   408      @{subgoals [display]}
   408      \end{minipage}*}
   409      \end{minipage}*}
   409 (*<*)oops(*>*)
   410 (*<*)oops(*>*)
   410 
   411 
   411 text {*
   412 text {*
   412   The function @{ML resolve_tac} is similar to @{ML rtac}, except that it
   413   The function @{ML [index] resolve_tac} is similar to @{ML [index] rtac}, except that it
   413   expects a list of theorems as arguments. From this list it will apply the
   414   expects a list of theorems as arguments. From this list it will apply the
   414   first applicable theorem (later theorems that are also applicable can be
   415   first applicable theorem (later theorems that are also applicable can be
   415   explored via the lazy sequences mechanism). Given the code
   416   explored via the lazy sequences mechanism). Given the code
   416 *}
   417 *}
   417 
   418 
   430      \end{minipage}*}
   431      \end{minipage}*}
   431 (*<*)oops(*>*)
   432 (*<*)oops(*>*)
   432 
   433 
   433 text {* 
   434 text {* 
   434   Similar versions taking a list of theorems exist for the tactics 
   435   Similar versions taking a list of theorems exist for the tactics 
   435   @{ML dtac} (@{ML dresolve_tac}), @{ML etac} (@{ML eresolve_tac}) and so on.
   436   @{ML dtac} (@{ML [index] dresolve_tac}), @{ML etac} 
   436 
   437   (@{ML [index] eresolve_tac}) and so on.
   437 
   438 
   438   Another simple tactic is @{ML cut_facts_tac}. It inserts a list of theorems
   439 
       
   440   Another simple tactic is @{ML [index] cut_facts_tac}. It inserts a list of theorems
   439   into the assumptions of the current goal state. For example
   441   into the assumptions of the current goal state. For example
   440 *}
   442 *}
   441 
   443 
   442 lemma shows "True \<noteq> False"
   444 lemma shows "True \<noteq> False"
   443 apply(tactic {* cut_facts_tac [@{thm True_def}, @{thm False_def}] 1 *})
   445 apply(tactic {* cut_facts_tac [@{thm True_def}, @{thm False_def}] 1 *})
   468   applied to the first subgoal might instantiate this meta-variable in such a 
   470   applied to the first subgoal might instantiate this meta-variable in such a 
   469   way that the second subgoal becomes unprovable. If it is clear what the @{text "?x"}
   471   way that the second subgoal becomes unprovable. If it is clear what the @{text "?x"}
   470   should be, then this situation can be avoided by introducing a more
   472   should be, then this situation can be avoided by introducing a more
   471   constrained version of the @{text bspec}-rule. Such constraints can be given by
   473   constrained version of the @{text bspec}-rule. Such constraints can be given by
   472   pre-instantiating theorems with other theorems. One function to do this is
   474   pre-instantiating theorems with other theorems. One function to do this is
   473   @{ML RS}
   475   @{ML [index] RS}
   474   
   476   
   475   @{ML_response_fake [display,gray]
   477   @{ML_response_fake [display,gray]
   476   "@{thm disjI1} RS @{thm conjI}" "\<lbrakk>?P1; ?Q\<rbrakk> \<Longrightarrow> (?P1 \<or> ?Q1) \<and> ?Q"}
   478   "@{thm disjI1} RS @{thm conjI}" "\<lbrakk>?P1; ?Q\<rbrakk> \<Longrightarrow> (?P1 \<or> ?Q1) \<and> ?Q"}
   477 
   479 
   478   which in the example instantiates the first premise of the @{text conjI}-rule 
   480   which in the example instantiates the first premise of the @{text conjI}-rule 
   482   @{ML_response_fake_both [display,gray]
   484   @{ML_response_fake_both [display,gray]
   483   "@{thm conjI} RS @{thm mp}" 
   485   "@{thm conjI} RS @{thm mp}" 
   484 "*** Exception- THM (\"RSN: no unifiers\", 1, 
   486 "*** Exception- THM (\"RSN: no unifiers\", 1, 
   485 [\"\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q\", \"\<lbrakk>?P \<longrightarrow> ?Q; ?P\<rbrakk> \<Longrightarrow> ?Q\"]) raised"}
   487 [\"\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q\", \"\<lbrakk>?P \<longrightarrow> ?Q; ?P\<rbrakk> \<Longrightarrow> ?Q\"]) raised"}
   486 
   488 
   487   then the function raises an exception. The function @{ML RSN} is similar to @{ML RS}, but 
   489   then the function raises an exception. The function @{ML [index] RSN} is similar to @{ML RS}, but 
   488   takes an additional number as argument that makes explicit which premise 
   490   takes an additional number as argument that makes explicit which premise 
   489   should be instantiated. 
   491   should be instantiated. 
   490 
   492 
   491   To improve readability of the theorems we shall produce below, we will use the
   493   To improve readability of the theorems we shall produce below, we will use the
   492   function @{ML no_vars} from Section~\ref{sec:printing}, which transforms
   494   function @{ML no_vars} from Section~\ref{sec:printing}, which transforms
   495 
   497 
   496   @{ML_response_fake [display,gray]
   498   @{ML_response_fake [display,gray]
   497   "no_vars @{context} (@{thm disjI1} RS @{thm conjI})" "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> (P \<or> Qa) \<and> Q"}
   499   "no_vars @{context} (@{thm disjI1} RS @{thm conjI})" "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> (P \<or> Qa) \<and> Q"}
   498 
   500 
   499   If you want to instantiate more than one premise of a theorem, you can use 
   501   If you want to instantiate more than one premise of a theorem, you can use 
   500   the function @{ML MRS}:
   502   the function @{ML [index] MRS}:
   501 
   503 
   502   @{ML_response_fake [display,gray]
   504   @{ML_response_fake [display,gray]
   503   "no_vars @{context} ([@{thm disjI1}, @{thm disjI2}] MRS @{thm conjI})" 
   505   "no_vars @{context} ([@{thm disjI1}, @{thm disjI2}] MRS @{thm conjI})" 
   504   "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> (P \<or> Qa) \<and> (Pa \<or> Q)"}
   506   "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> (P \<or> Qa) \<and> (Pa \<or> Q)"}
   505 
   507 
   506   If you need to instantiate lists of theorems, you can use the
   508   If you need to instantiate lists of theorems, you can use the
   507   functions @{ML RL} and @{ML MRL}. For example in the code below,
   509   functions @{ML RL} and @{ML [index] MRL}. For example in the code below,
   508   every theorem in the second list is instantiated with every 
   510   every theorem in the second list is instantiated with every 
   509   theorem in the first.
   511   theorem in the first.
   510 
   512 
   511   @{ML_response_fake [display,gray]
   513   @{ML_response_fake [display,gray]
   512 "map (no_vars @{context}) 
   514 "map (no_vars @{context}) 
   521   \end{readmore}
   523   \end{readmore}
   522 
   524 
   523   Often proofs on the ML-level involve elaborate operations on assumptions and 
   525   Often proofs on the ML-level involve elaborate operations on assumptions and 
   524   @{text "\<And>"}-quantified variables. To do such operations using the basic tactics 
   526   @{text "\<And>"}-quantified variables. To do such operations using the basic tactics 
   525   shown so far is very unwieldy and brittle. Some convenience and
   527   shown so far is very unwieldy and brittle. Some convenience and
   526   safety is provided by @{ML SUBPROOF}. This tactic fixes the parameters 
   528   safety is provided by @{ML [index] SUBPROOF}. This tactic fixes the parameters 
   527   and binds the various components of a goal state to a record. 
   529   and binds the various components of a goal state to a record. 
   528   To see what happens, assume the function defined in Figure~\ref{fig:sptac}, which
   530   To see what happens, assume the function defined in Figure~\ref{fig:sptac}, which
   529   takes a record and just prints out the content of this record (using the 
   531   takes a record and just prints out the content of this record (using the 
   530   string transformation functions from in Section~\ref{sec:printing}). Consider
   532   string transformation functions from in Section~\ref{sec:printing}). Consider
   531   now the proof:
   533   now the proof:
   584   Similarly the schematic variable @{term z}. The assumption, or premise, 
   586   Similarly the schematic variable @{term z}. The assumption, or premise, 
   585   @{prop "A x y"} is bound as @{ML_type cterm} to the record-variable 
   587   @{prop "A x y"} is bound as @{ML_type cterm} to the record-variable 
   586   @{text asms}, but also as @{ML_type thm} to @{text prems}.
   588   @{text asms}, but also as @{ML_type thm} to @{text prems}.
   587 
   589 
   588   Notice also that we had to append @{text [quotes] "?"} to the
   590   Notice also that we had to append @{text [quotes] "?"} to the
   589   \isacommand{apply}-command. The reason is that @{ML SUBPROOF} normally
   591   \isacommand{apply}-command. The reason is that @{ML [index] SUBPROOF} normally
   590   expects that the subgoal is solved completely.  Since in the function @{ML
   592   expects that the subgoal is solved completely.  Since in the function @{ML
   591   sp_tac} we returned the tactic @{ML no_tac}, the subproof obviously
   593   sp_tac} we returned the tactic @{ML no_tac}, the subproof obviously
   592   fails. The question-mark allows us to recover from this failure in a
   594   fails. The question-mark allows us to recover from this failure in a
   593   graceful manner so that the output messages are not overwritten by an 
   595   graceful manner so that the output messages are not overwritten by an 
   594   ``empty sequence'' error message.
   596   ``empty sequence'' error message.
   661   \begin{readmore}
   663   \begin{readmore}
   662   The function @{ML SUBPROOF} is defined in @{ML_file "Pure/subgoal.ML"} and
   664   The function @{ML SUBPROOF} is defined in @{ML_file "Pure/subgoal.ML"} and
   663   also described in \isccite{sec:results}. 
   665   also described in \isccite{sec:results}. 
   664   \end{readmore}
   666   \end{readmore}
   665 
   667 
   666   Similar but less powerful functions than @{ML SUBPROOF} are @{ML SUBGOAL}
   668   Similar but less powerful functions than @{ML SUBPROOF} are @{ML [index] SUBGOAL}
   667   and @{ML CSUBGOAL}. They allow you to inspect a given subgoal (the former
   669   and @{ML [index] CSUBGOAL}. They allow you to inspect a given subgoal (the former
   668   presents the subgoal as a @{ML_type term}, while the latter as a @{ML_type
   670   presents the subgoal as a @{ML_type term}, while the latter as a @{ML_type
   669   cterm}). With this you can implement a tactic that applies a rule according
   671   cterm}). With this you can implement a tactic that applies a rule according
   670   to the topmost logic connective in the subgoal (to illustrate this we only
   672   to the topmost logic connective in the subgoal (to illustrate this we only
   671   analyse a few connectives). The code of the tactic is as
   673   analyse a few connectives). The code of the tactic is as
   672   follows.
   674   follows.
   773   it is consistently applied to the component tactics.
   775   it is consistently applied to the component tactics.
   774   For most tactic combinators such a ``primed'' version exists and
   776   For most tactic combinators such a ``primed'' version exists and
   775   in what follows we will usually prefer it over the ``unprimed'' one. 
   777   in what follows we will usually prefer it over the ``unprimed'' one. 
   776 
   778 
   777   If there is a list of tactics that should all be tried out in 
   779   If there is a list of tactics that should all be tried out in 
   778   sequence, you can use the combinator @{ML EVERY'}. For example
   780   sequence, you can use the combinator @{ML [index] EVERY'}. For example
   779   the function @{ML foo_tac'} from page~\pageref{tac:footacprime} can also 
   781   the function @{ML foo_tac'} from page~\pageref{tac:footacprime} can also 
   780   be written as:
   782   be written as:
   781 *}
   783 *}
   782 
   784 
   783 ML{*val foo_tac'' = EVERY' [etac @{thm disjE}, rtac @{thm disjI2}, 
   785 ML{*val foo_tac'' = EVERY' [etac @{thm disjE}, rtac @{thm disjI2}, 
   795                        atac, rtac @{thm disjI1}, atac]*}
   797                        atac, rtac @{thm disjI1}, atac]*}
   796 
   798 
   797 text {*
   799 text {*
   798   and call @{ML foo_tac1}.  
   800   and call @{ML foo_tac1}.  
   799 
   801 
   800   With the combinators @{ML THEN'}, @{ML EVERY'} and @{ML EVERY1} it must be
   802   With the combinators @{ML THEN'}, @{ML EVERY'} and @{ML [index] EVERY1} it must be
   801   guaranteed that all component tactics successfully apply; otherwise the
   803   guaranteed that all component tactics successfully apply; otherwise the
   802   whole tactic will fail. If you rather want to try out a number of tactics,
   804   whole tactic will fail. If you rather want to try out a number of tactics,
   803   then you can use the combinator @{ML ORELSE'} for two tactics, and @{ML
   805   then you can use the combinator @{ML [index] ORELSE'} for two tactics, and @{ML
   804   FIRST'} (or @{ML FIRST1}) for a list of tactics. For example, the tactic
   806   [index] FIRST'} (or @{ML [index] FIRST1}) for a list of tactics. For example, the tactic
   805 
   807 
   806 *}
   808 *}
   807 
   809 
   808 ML{*val orelse_xmp_tac = rtac @{thm disjI1} ORELSE' rtac @{thm conjI}*}
   810 ML{*val orelse_xmp_tac = rtac @{thm disjI1} ORELSE' rtac @{thm conjI}*}
   809 
   811 
   851 (*<*)oops(*>*)
   853 (*<*)oops(*>*)
   852 
   854 
   853 text {* 
   855 text {* 
   854   Since such repeated applications of a tactic to the reverse order of 
   856   Since such repeated applications of a tactic to the reverse order of 
   855   \emph{all} subgoals is quite common, there is the tactic combinator 
   857   \emph{all} subgoals is quite common, there is the tactic combinator 
   856   @{ML ALLGOALS} that simplifies this. Using this combinator you can simply 
   858   @{ML [index] ALLGOALS} that simplifies this. Using this combinator you can simply 
   857   write: *}
   859   write: *}
   858 
   860 
   859 lemma shows "A \<and> B" and "A \<longrightarrow> B \<longrightarrow>C" and "\<forall>x. D x" and "E \<Longrightarrow> F"
   861 lemma shows "A \<and> B" and "A \<longrightarrow> B \<longrightarrow>C" and "\<forall>x. D x" and "E \<Longrightarrow> F"
   860 apply(tactic {* ALLGOALS select_tac' *})
   862 apply(tactic {* ALLGOALS select_tac' *})
   861 txt{* \begin{minipage}{\textwidth}
   863 txt{* \begin{minipage}{\textwidth}
   864 (*<*)oops(*>*)
   866 (*<*)oops(*>*)
   865 
   867 
   866 text {*
   868 text {*
   867   Remember that we chose to implement @{ML select_tac'} so that it 
   869   Remember that we chose to implement @{ML select_tac'} so that it 
   868   always  succeeds by adding @{ML all_tac} at the end of the tactic
   870   always  succeeds by adding @{ML all_tac} at the end of the tactic
   869   list. The same can be achieved with the tactic combinator @{ML TRY}.
   871   list. The same can be achieved with the tactic combinator @{ML [index] TRY}.
   870   For example:
   872   For example:
   871 *}
   873 *}
   872 
   874 
   873 ML{*val select_tac'' = TRY o FIRST' [rtac @{thm conjI}, rtac @{thm impI}, 
   875 ML{*val select_tac'' = TRY o FIRST' [rtac @{thm conjI}, rtac @{thm impI}, 
   874                           rtac @{thm notI}, rtac @{thm allI}]*}
   876                           rtac @{thm notI}, rtac @{thm allI}]*}
   897   
   899   
   898   To comply with this convention, we could simply delete the @{ML "K all_tac"}
   900   To comply with this convention, we could simply delete the @{ML "K all_tac"}
   899   from the end of the theorem list. As a result @{ML select_tac'} would only
   901   from the end of the theorem list. As a result @{ML select_tac'} would only
   900   succeed on goals where it can make progress. But for the sake of argument,
   902   succeed on goals where it can make progress. But for the sake of argument,
   901   let us suppose that this deletion is \emph{not} an option. In such cases, you can
   903   let us suppose that this deletion is \emph{not} an option. In such cases, you can
   902   use the combinator @{ML CHANGED} to make sure the subgoal has been changed
   904   use the combinator @{ML [index] CHANGED} to make sure the subgoal has been changed
   903   by the tactic. Because now
   905   by the tactic. Because now
   904 
   906 
   905 *}
   907 *}
   906 
   908 
   907 lemma shows "E \<Longrightarrow> F"
   909 lemma shows "E \<Longrightarrow> F"
   915 
   917 
   916 
   918 
   917 text {*
   919 text {*
   918   We can further extend @{ML select_tac'} so that it not just applies to the topmost
   920   We can further extend @{ML select_tac'} so that it not just applies to the topmost
   919   connective, but also to the ones immediately ``underneath'', i.e.~analyse the goal 
   921   connective, but also to the ones immediately ``underneath'', i.e.~analyse the goal 
   920   completely. For this you can use the tactic combinator @{ML REPEAT}. As an example 
   922   completely. For this you can use the tactic combinator @{ML [index] REPEAT}. As an example 
   921   suppose the following tactic
   923   suppose the following tactic
   922 *}
   924 *}
   923 
   925 
   924 ML{*val repeat_xmp_tac = REPEAT (CHANGED (select_tac' 1)) *}
   926 ML{*val repeat_xmp_tac = REPEAT (CHANGED (select_tac' 1)) *}
   925 
   927 
   936 
   938 
   937 text {*
   939 text {*
   938   Here it is crucial that @{ML select_tac'} is prefixed with @{ML CHANGED}, 
   940   Here it is crucial that @{ML select_tac'} is prefixed with @{ML CHANGED}, 
   939   because otherwise @{ML REPEAT} runs into an infinite loop (it applies the
   941   because otherwise @{ML REPEAT} runs into an infinite loop (it applies the
   940   tactic as long as it succeeds). The function
   942   tactic as long as it succeeds). The function
   941   @{ML REPEAT1} is similar, but runs the tactic at least once (failing if 
   943   @{ML [index] REPEAT1} is similar, but runs the tactic at least once (failing if 
   942   this is not possible).
   944   this is not possible).
   943 
   945 
   944   If you are after the ``primed'' version of @{ML repeat_xmp_tac}, then you 
   946   If you are after the ``primed'' version of @{ML repeat_xmp_tac}, then you 
   945   can implement it as
   947   can implement it as
   946 *}
   948 *}
   952 
   954 
   953   If you look closely at the goal state above, then you see the tactics @{ML repeat_xmp_tac}
   955   If you look closely at the goal state above, then you see the tactics @{ML repeat_xmp_tac}
   954   and @{ML repeat_xmp_tac'} are not yet quite what we are after: the problem is
   956   and @{ML repeat_xmp_tac'} are not yet quite what we are after: the problem is
   955   that goals 2 and 3 are not analysed. This is because the tactic
   957   that goals 2 and 3 are not analysed. This is because the tactic
   956   is applied repeatedly only to the first subgoal. To analyse also all
   958   is applied repeatedly only to the first subgoal. To analyse also all
   957   resulting subgoals, you can use the tactic combinator @{ML REPEAT_ALL_NEW}. 
   959   resulting subgoals, you can use the tactic combinator @{ML [index] REPEAT_ALL_NEW}. 
   958   Suppose the tactic
   960   Suppose the tactic
   959 *}
   961 *}
   960 
   962 
   961 ML{*val repeat_all_new_xmp_tac = REPEAT_ALL_NEW (CHANGED o select_tac')*}
   963 ML{*val repeat_all_new_xmp_tac = REPEAT_ALL_NEW (CHANGED o select_tac')*}
   962 
   964 
  1005 
  1007 
  1006 text {*
  1008 text {*
  1007   Sometimes this leads to confusing behaviour of tactics and also has
  1009   Sometimes this leads to confusing behaviour of tactics and also has
  1008   the potential to explode the search space for tactics.
  1010   the potential to explode the search space for tactics.
  1009   These problems can be avoided by prefixing the tactic with the tactic 
  1011   These problems can be avoided by prefixing the tactic with the tactic 
  1010   combinator @{ML DETERM}.
  1012   combinator @{ML [index] DETERM}.
  1011 *}
  1013 *}
  1012 
  1014 
  1013 lemma "\<lbrakk>P1 \<or> Q1; P2 \<or> Q2\<rbrakk> \<Longrightarrow> R"
  1015 lemma "\<lbrakk>P1 \<or> Q1; P2 \<or> Q2\<rbrakk> \<Longrightarrow> R"
  1014 apply(tactic {* DETERM (etac @{thm disjE} 1) *})
  1016 apply(tactic {* DETERM (etac @{thm disjE} 1) *})
  1015 txt {*\begin{minipage}{\textwidth}
  1017 txt {*\begin{minipage}{\textwidth}
  1042 ML{*val select_tac''' = TRY o select_tac''*}
  1044 ML{*val select_tac''' = TRY o select_tac''*}
  1043 
  1045 
  1044 text {*
  1046 text {*
  1045   then the tactic @{ML select_tac''} will be tried out and any failure is harnessed. 
  1047   then the tactic @{ML select_tac''} will be tried out and any failure is harnessed. 
  1046   We again have to use the construction with \mbox{@{text "TRY o ..."}} since there is 
  1048   We again have to use the construction with \mbox{@{text "TRY o ..."}} since there is 
  1047   no primed version of @{ML TRY}. The tactic combinator @{ML TRYALL} will try out
  1049   no primed version of @{ML [index] TRY}. The tactic combinator @{ML [index] TRYALL} will try out
  1048   a tactic on all subgoals. For example the tactic 
  1050   a tactic on all subgoals. For example the tactic 
  1049 *}
  1051 *}
  1050 
  1052 
  1051 ML{*val triv_tac = TRYALL (rtac @{thm TrueI} ORELSE' etac @{thm FalseE})*}
  1053 ML{*val triv_tac = TRYALL (rtac @{thm TrueI} ORELSE' etac @{thm FalseE})*}
  1052 
  1054 
  1053 text {*
  1055 text {*
  1054   will solve all trivial subgoals involving @{term True} or @{term "False"}.
  1056   will solve all trivial subgoals involving @{term True} or @{term "False"}.
  1055 
  1057 
  1056   (FIXME: say something about @{ML COND} and COND')
  1058   (FIXME: say something about @{ML [index] COND} and COND')
  1057   
  1059   
  1058   \begin{readmore}
  1060   \begin{readmore}
  1059   Most tactic combinators described in this section are defined in @{ML_file "Pure/tctical.ML"}.
  1061   Most tactic combinators described in this section are defined in @{ML_file "Pure/tctical.ML"}.
  1060   Some combinators for the purpose of proof search are implemented in @{ML_file "Pure/search.ML"}.
  1062   Some combinators for the purpose of proof search are implemented in @{ML_file "Pure/search.ML"}.
  1061   \end{readmore}
  1063   \end{readmore}
  1077   the simplifier (in parentheses is their user-level counterpart):
  1079   the simplifier (in parentheses is their user-level counterpart):
  1078 
  1080 
  1079   \begin{isabelle}
  1081   \begin{isabelle}
  1080   \begin{center}
  1082   \begin{center}
  1081   \begin{tabular}{l@ {\hspace{2cm}}l}
  1083   \begin{tabular}{l@ {\hspace{2cm}}l}
  1082    @{ML simp_tac}            & @{text "(simp (no_asm))"} \\
  1084    @{ML [index] simp_tac}            & @{text "(simp (no_asm))"} \\
  1083    @{ML asm_simp_tac}        & @{text "(simp (no_asm_simp))"} \\
  1085    @{ML [index] asm_simp_tac}        & @{text "(simp (no_asm_simp))"} \\
  1084    @{ML full_simp_tac}       & @{text "(simp (no_asm_use))"} \\
  1086    @{ML [index] full_simp_tac}       & @{text "(simp (no_asm_use))"} \\
  1085    @{ML asm_lr_simp_tac}     & @{text "(simp (asm_lr))"} \\
  1087    @{ML [index] asm_lr_simp_tac}     & @{text "(simp (asm_lr))"} \\
  1086    @{ML asm_full_simp_tac}   & @{text "(simp)"}
  1088    @{ML [index] asm_full_simp_tac}   & @{text "(simp)"}
  1087   \end{tabular}
  1089   \end{tabular}
  1088   \end{center}
  1090   \end{center}
  1089   \end{isabelle}
  1091   \end{isabelle}
  1090 
  1092 
  1091   All of the tactics take a simpset and an integer as argument (the latter as usual 
  1093   All of the tactics take a simpset and an integer as argument (the latter as usual 
  1162 
  1164 
  1163   The most common combinators to modify simpsets are:
  1165   The most common combinators to modify simpsets are:
  1164 
  1166 
  1165   \begin{isabelle}
  1167   \begin{isabelle}
  1166   \begin{tabular}{ll}
  1168   \begin{tabular}{ll}
  1167   @{ML addsimps}   & @{ML delsimps}\\
  1169   @{ML [index] addsimps}    & @{ML [index] delsimps}\\
  1168   @{ML addcongs}   & @{ML delcongs}\\
  1170   @{ML [index] addcongs}    & @{ML [index] delcongs}\\
  1169   @{ML addsimprocs} & @{ML delsimprocs}\\
  1171   @{ML [index] addsimprocs} & @{ML [index] delsimprocs}\\
  1170   \end{tabular}
  1172   \end{tabular}
  1171   \end{isabelle}
  1173   \end{isabelle}
  1172 
  1174 
  1173   (FIXME: What about splitters? @{ML addsplits}, @{ML delsplits})
  1175   (FIXME: What about splitters? @{ML addsplits}, @{ML delsplits})
  1174 *}
  1176 *}
  1194     |> writeln
  1196     |> writeln
  1195 end*}
  1197 end*}
  1196 text_raw {* 
  1198 text_raw {* 
  1197 \end{isabelle}
  1199 \end{isabelle}
  1198 \end{minipage}
  1200 \end{minipage}
  1199 \caption{The function @{ML Simplifier.dest_ss} returns a record containing
  1201 \caption{The function @{ML [index] dest_ss in Simplifier} returns a record containing
  1200   all printable information stored in a simpset. We are here only interested in the 
  1202   all printable information stored in a simpset. We are here only interested in the 
  1201   simplification rules, congruence rules and simprocs.\label{fig:printss}}
  1203   simplification rules, congruence rules and simprocs.\label{fig:printss}}
  1202 \end{figure} *}
  1204 \end{figure} *}
  1203 
  1205 
  1204 text {* 
  1206 text {* 
  1205   To see how they work, consider the function in Figure~\ref{fig:printss}, which
  1207   To see how they work, consider the function in Figure~\ref{fig:printss}, which
  1206   prints out some parts of a simpset. If you use it to print out the components of the
  1208   prints out some parts of a simpset. If you use it to print out the components of the
  1207   empty simpset, i.e., @{ML empty_ss}
  1209   empty simpset, i.e., @{ML [index] empty_ss}
  1208   
  1210   
  1209   @{ML_response_fake [display,gray]
  1211   @{ML_response_fake [display,gray]
  1210   "print_ss @{context} empty_ss"
  1212   "print_ss @{context} empty_ss"
  1211 "Simplification rules:
  1213 "Simplification rules:
  1212 Congruences rules:
  1214 Congruences rules:
  1249 
  1251 
  1250   Notice that we had to add these lemmas as meta-equations. The @{ML empty_ss} 
  1252   Notice that we had to add these lemmas as meta-equations. The @{ML empty_ss} 
  1251   expects this form of the simplification and congruence rules. However, even 
  1253   expects this form of the simplification and congruence rules. However, even 
  1252   when adding these lemmas to @{ML empty_ss} we do not end up with anything useful yet.
  1254   when adding these lemmas to @{ML empty_ss} we do not end up with anything useful yet.
  1253 
  1255 
  1254   In the context of HOL, the first really useful simpset is @{ML HOL_basic_ss}. While
  1256   In the context of HOL, the first really useful simpset is @{ML [index] HOL_basic_ss}. While
  1255   printing out the components of this simpset
  1257   printing out the components of this simpset
  1256 
  1258 
  1257   @{ML_response_fake [display,gray]
  1259   @{ML_response_fake [display,gray]
  1258   "print_ss @{context} HOL_basic_ss"
  1260   "print_ss @{context} HOL_basic_ss"
  1259 "Simplification rules:
  1261 "Simplification rules:
  1276 apply(tactic {* ALLGOALS (simp_tac HOL_basic_ss) *})
  1278 apply(tactic {* ALLGOALS (simp_tac HOL_basic_ss) *})
  1277 done
  1279 done
  1278 
  1280 
  1279 text {*
  1281 text {*
  1280   This behaviour is not because of simplification rules, but how the subgoaler, solver 
  1282   This behaviour is not because of simplification rules, but how the subgoaler, solver 
  1281   and looper are set up in @{ML HOL_basic_ss}.
  1283   and looper are set up in @{ML [index] HOL_basic_ss}.
  1282 
  1284 
  1283   The simpset @{ML HOL_ss} is an extension of @{ML HOL_basic_ss} containing 
  1285   The simpset @{ML [index] HOL_ss} is an extension of @{ML HOL_basic_ss} containing 
  1284   already many useful simplification and congruence rules for the logical 
  1286   already many useful simplification and congruence rules for the logical 
  1285   connectives in HOL. 
  1287   connectives in HOL. 
  1286 
  1288 
  1287   @{ML_response_fake [display,gray]
  1289   @{ML_response_fake [display,gray]
  1288   "print_ss @{context} HOL_ss"
  1290   "print_ss @{context} HOL_ss"
  1298 Simproc patterns:
  1300 Simproc patterns:
  1299   \<dots>"}
  1301   \<dots>"}
  1300 
  1302 
  1301   
  1303   
  1302   The simplifier is often used to unfold definitions in a proof. For this the
  1304   The simplifier is often used to unfold definitions in a proof. For this the
  1303   simplifier implements the tactic @{ML rewrite_goals_tac}.\footnote{FIXME: 
  1305   simplifier implements the tactic @{ML [index] rewrite_goals_tac}.\footnote{FIXME: 
  1304   see LocalDefs infrastructure.} Suppose for example the
  1306   see LocalDefs infrastructure.} Suppose for example the
  1305   definition
  1307   definition
  1306 *}
  1308 *}
  1307 
  1309 
  1308 definition "MyTrue \<equiv> True"
  1310 definition "MyTrue \<equiv> True"
  1612 
  1614 
  1613 text {*
  1615 text {*
  1614   Here the pattern is given as @{ML_type term} (instead of @{ML_type cterm}).
  1616   Here the pattern is given as @{ML_type term} (instead of @{ML_type cterm}).
  1615   The function also takes a list of patterns that can trigger the simproc.
  1617   The function also takes a list of patterns that can trigger the simproc.
  1616   Now the simproc is set up and can be explicitly added using
  1618   Now the simproc is set up and can be explicitly added using
  1617   @{ML addsimprocs} to a simpset whenever
  1619   @{ML [index] addsimprocs} to a simpset whenever
  1618   needed. 
  1620   needed. 
  1619 
  1621 
  1620   Simprocs are applied from inside to outside and from left to right. You can
  1622   Simprocs are applied from inside to outside and from left to right. You can
  1621   see this in the proof
  1623   see this in the proof
  1622 *}
  1624 *}
  1698 
  1700 
  1699 ML{*fun dest_suc_trm ((Const (@{const_name "Suc"}, _)) $ t) = 1 + dest_suc_trm t
  1701 ML{*fun dest_suc_trm ((Const (@{const_name "Suc"}, _)) $ t) = 1 + dest_suc_trm t
  1700   | dest_suc_trm t = snd (HOLogic.dest_number t)*}
  1702   | dest_suc_trm t = snd (HOLogic.dest_number t)*}
  1701 
  1703 
  1702 text {* 
  1704 text {* 
  1703   It uses the library function @{ML dest_number in HOLogic} that transforms
  1705   It uses the library function @{ML [index] dest_number in HOLogic} that transforms
  1704   (Isabelle) terms, like @{term "0::nat"}, @{term "1::nat"}, @{term "2::nat"} and so
  1706   (Isabelle) terms, like @{term "0::nat"}, @{term "1::nat"}, @{term "2::nat"} and so
  1705   on, into integer values. This function raises the exception @{ML TERM}, if
  1707   on, into integer values. This function raises the exception @{ML TERM}, if
  1706   the term is not a number. The next function expects a pair consisting of a term
  1708   the term is not a number. The next function expects a pair consisting of a term
  1707   @{text t} (containing @{term Suc}s) and the corresponding integer value @{text n}. 
  1709   @{text t} (containing @{term Suc}s) and the corresponding integer value @{text n}. 
  1708 *}
  1710 *}
  1818 
  1820 
  1819 ML{*type conv = cterm -> thm*}
  1821 ML{*type conv = cterm -> thm*}
  1820 
  1822 
  1821 text {*
  1823 text {*
  1822   whereby the produced theorem is always a meta-equality. A simple conversion
  1824   whereby the produced theorem is always a meta-equality. A simple conversion
  1823   is the function @{ML "Conv.all_conv"}, which maps a @{ML_type cterm} to an
  1825   is the function @{ML [index] all_conv in Conv}, which maps a @{ML_type cterm} to an
  1824   instance of the (meta)reflexivity theorem. For example:
  1826   instance of the (meta)reflexivity theorem. For example:
  1825 
  1827 
  1826   @{ML_response_fake [display,gray]
  1828   @{ML_response_fake [display,gray]
  1827   "Conv.all_conv @{cterm \"Foo \<or> Bar\"}"
  1829   "Conv.all_conv @{cterm \"Foo \<or> Bar\"}"
  1828   "Foo \<or> Bar \<equiv> Foo \<or> Bar"}
  1830   "Foo \<or> Bar \<equiv> Foo \<or> Bar"}
  1829 
  1831 
  1830   Another simple conversion is @{ML Conv.no_conv} which always raises the 
  1832   Another simple conversion is @{ML [index] no_conv in Conv} which always raises the 
  1831   exception @{ML CTERM}.
  1833   exception @{ML CTERM}.
  1832 
  1834 
  1833   @{ML_response_fake [display,gray]
  1835   @{ML_response_fake [display,gray]
  1834   "Conv.no_conv @{cterm True}" 
  1836   "Conv.no_conv @{cterm True}" 
  1835   "*** Exception- CTERM (\"no conversion\", []) raised"}
  1837   "*** Exception- CTERM (\"no conversion\", []) raised"}
  1836 
  1838 
  1837   A more interesting conversion is the function @{ML "Thm.beta_conversion"}: it 
  1839   A more interesting conversion is the function @{ML [index] beta_conversion in Thm}: it 
  1838   produces a meta-equation between a term and its beta-normal form. For example
  1840   produces a meta-equation between a term and its beta-normal form. For example
  1839 
  1841 
  1840   @{ML_response_fake [display,gray]
  1842   @{ML_response_fake [display,gray]
  1841   "let
  1843   "let
  1842   val add = @{cterm \"\<lambda>x y. x + (y::nat)\"}
  1844   val add = @{cterm \"\<lambda>x y. x + (y::nat)\"}
  1848   "((\<lambda>x y. x + y) 2) 10 \<equiv> 2 + 10"}
  1850   "((\<lambda>x y. x + y) 2) 10 \<equiv> 2 + 10"}
  1849 
  1851 
  1850   Note that the actual response in this example is @{term "2 + 10 \<equiv> 2 + (10::nat)"}, 
  1852   Note that the actual response in this example is @{term "2 + 10 \<equiv> 2 + (10::nat)"}, 
  1851   since the pretty-printer for @{ML_type cterm}s eta-normalises terms.
  1853   since the pretty-printer for @{ML_type cterm}s eta-normalises terms.
  1852   But how we constructed the term (using the function 
  1854   But how we constructed the term (using the function 
  1853   @{ML Thm.capply}, which is the application @{ML $} for @{ML_type cterm}s)
  1855   @{ML [index] capply in Thm}, which is the application @{ML $} for @{ML_type cterm}s)
  1854   ensures that the left-hand side must contain beta-redexes. Indeed
  1856   ensures that the left-hand side must contain beta-redexes. Indeed
  1855   if we obtain the ``raw'' representation of the produced theorem, we
  1857   if we obtain the ``raw'' representation of the produced theorem, we
  1856   can see the difference:
  1858   can see the difference:
  1857 
  1859 
  1858   @{ML_response [display,gray]
  1860   @{ML_response [display,gray]
  1902 in
  1904 in
  1903   Conv.rewr_conv @{thm true_conj1} ctrm
  1905   Conv.rewr_conv @{thm true_conj1} ctrm
  1904 end"
  1906 end"
  1905   "True \<and> (Foo \<longrightarrow> Bar) \<equiv> Foo \<longrightarrow> Bar"}
  1907   "True \<and> (Foo \<longrightarrow> Bar) \<equiv> Foo \<longrightarrow> Bar"}
  1906 
  1908 
  1907   Note, however, that the function @{ML Conv.rewr_conv} only rewrites the 
  1909   Note, however, that the function @{ML [index] rewr_conv in Conv} only rewrites the 
  1908   outer-most level of the @{ML_type cterm}. If the given @{ML_type cterm} does not match 
  1910   outer-most level of the @{ML_type cterm}. If the given @{ML_type cterm} does not match 
  1909   exactly the 
  1911   exactly the 
  1910   left-hand side of the theorem, then  @{ML Conv.rewr_conv} fails by raising 
  1912   left-hand side of the theorem, then  @{ML [index] rewr_conv in Conv} fails by raising 
  1911   the exception @{ML CTERM}.
  1913   the exception @{ML CTERM}.
  1912 
  1914 
  1913   This very primitive way of rewriting can be made more powerful by
  1915   This very primitive way of rewriting can be made more powerful by
  1914   combining several conversions into one. For this you can use conversion
  1916   combining several conversions into one. For this you can use conversion
  1915   combinators. The simplest conversion combinator is @{ML then_conv}, 
  1917   combinators. The simplest conversion combinator is @{ML [index] then_conv}, 
  1916   which applies one conversion after another. For example
  1918   which applies one conversion after another. For example
  1917 
  1919 
  1918   @{ML_response_fake [display,gray]
  1920   @{ML_response_fake [display,gray]
  1919 "let
  1921 "let
  1920   val conv1 = Thm.beta_conversion false
  1922   val conv1 = Thm.beta_conversion false
  1927 
  1929 
  1928   where we first beta-reduce the term and then rewrite according to
  1930   where we first beta-reduce the term and then rewrite according to
  1929   @{thm [source] true_conj1}. (Recall the problem with the pretty-printer
  1931   @{thm [source] true_conj1}. (Recall the problem with the pretty-printer
  1930   normalising all terms.)
  1932   normalising all terms.)
  1931 
  1933 
  1932   The conversion combinator @{ML else_conv} tries out the 
  1934   The conversion combinator @{ML [index] else_conv} tries out the 
  1933   first one, and if it does not apply, tries the second. For example 
  1935   first one, and if it does not apply, tries the second. For example 
  1934 
  1936 
  1935   @{ML_response_fake [display,gray]
  1937   @{ML_response_fake [display,gray]
  1936 "let
  1938 "let
  1937   val conv = Conv.rewr_conv @{thm true_conj1} else_conv Conv.all_conv
  1939   val conv = Conv.rewr_conv @{thm true_conj1} else_conv Conv.all_conv
  1942 end"
  1944 end"
  1943 "(True \<and> Q \<equiv> Q, P \<or> True \<and> Q \<equiv> P \<or> True \<and> Q)"}
  1945 "(True \<and> Q \<equiv> Q, P \<or> True \<and> Q \<equiv> P \<or> True \<and> Q)"}
  1944 
  1946 
  1945   Here the conversion of @{thm [source] true_conj1} only applies
  1947   Here the conversion of @{thm [source] true_conj1} only applies
  1946   in the first case, but fails in the second. The whole conversion
  1948   in the first case, but fails in the second. The whole conversion
  1947   does not fail, however, because the combinator @{ML Conv.else_conv} will then 
  1949   does not fail, however, because the combinator @{ML else_conv in Conv} will then 
  1948   try out @{ML Conv.all_conv}, which always succeeds.
  1950   try out @{ML all_conv in Conv}, which always succeeds.
  1949 
  1951 
  1950   The conversion combinator @{ML Conv.try_conv} constructs a conversion 
  1952   The conversion combinator @{ML [index] try_conv in Conv} constructs a conversion 
  1951   which is tried out on a term, but in case of failure just does nothing.
  1953   which is tried out on a term, but in case of failure just does nothing.
  1952   For example
  1954   For example
  1953   
  1955   
  1954   @{ML_response_fake [display,gray]
  1956   @{ML_response_fake [display,gray]
  1955   "Conv.try_conv (Conv.rewr_conv @{thm true_conj1}) @{cterm \"True \<or> P\"}"
  1957   "Conv.try_conv (Conv.rewr_conv @{thm true_conj1}) @{cterm \"True \<or> P\"}"
  1956   "True \<or> P \<equiv> True \<or> P"}
  1958   "True \<or> P \<equiv> True \<or> P"}
  1957 
  1959 
  1958   Apart from the function @{ML beta_conversion in Thm}, which is able to fully
  1960   Apart from the function @{ML beta_conversion in Thm}, which is able to fully
  1959   beta-normalise a term, the conversions so far are restricted in that they
  1961   beta-normalise a term, the conversions so far are restricted in that they
  1960   only apply to the outer-most level of a @{ML_type cterm}. In what follows we
  1962   only apply to the outer-most level of a @{ML_type cterm}. In what follows we
  1961   will lift this restriction. The combinator @{ML Conv.arg_conv} will apply
  1963   will lift this restriction. The combinator @{ML [index] arg_conv in Conv} will apply
  1962   the conversion to the first argument of an application, that is the term
  1964   the conversion to the first argument of an application, that is the term
  1963   must be of the form @{ML "t1 $ t2" for t1 t2} and the conversion is applied
  1965   must be of the form @{ML "t1 $ t2" for t1 t2} and the conversion is applied
  1964   to @{text t2}.  For example
  1966   to @{text t2}.  For example
  1965 
  1967 
  1966   @{ML_response_fake [display,gray]
  1968   @{ML_response_fake [display,gray]
  1973 "P \<or> (True \<and> Q) \<equiv> P \<or> Q"}
  1975 "P \<or> (True \<and> Q) \<equiv> P \<or> Q"}
  1974 
  1976 
  1975   The reason for this behaviour is that @{text "(op \<or>)"} expects two
  1977   The reason for this behaviour is that @{text "(op \<or>)"} expects two
  1976   arguments.  Therefore the term must be of the form @{text "(Const \<dots> $ t1) $ t2"}. The
  1978   arguments.  Therefore the term must be of the form @{text "(Const \<dots> $ t1) $ t2"}. The
  1977   conversion is then applied to @{text "t2"} which in the example above
  1979   conversion is then applied to @{text "t2"} which in the example above
  1978   stands for @{term "True \<and> Q"}. The function @{ML Conv.fun_conv} applies
  1980   stands for @{term "True \<and> Q"}. The function @{ML [index] fun_conv in Conv} applies
  1979   the conversion to the first argument of an application.
  1981   the conversion to the first argument of an application.
  1980 
  1982 
  1981   The function @{ML Conv.abs_conv} applies a conversion under an abstraction.
  1983   The function @{ML [index] abs_conv in Conv} applies a conversion under an abstraction.
  1982   For example:
  1984   For example:
  1983 
  1985 
  1984   @{ML_response_fake [display,gray]
  1986   @{ML_response_fake [display,gray]
  1985 "let 
  1987 "let 
  1986   val conv = Conv.rewr_conv @{thm true_conj1} 
  1988   val conv = Conv.rewr_conv @{thm true_conj1} 
  1989   Conv.abs_conv (K conv) @{context} ctrm
  1991   Conv.abs_conv (K conv) @{context} ctrm
  1990 end"
  1992 end"
  1991   "\<lambda>P. True \<and> P \<and> Foo \<equiv> \<lambda>P. P \<and> Foo"}
  1993   "\<lambda>P. True \<and> P \<and> Foo \<equiv> \<lambda>P. P \<and> Foo"}
  1992   
  1994   
  1993   Note that this conversion needs a context as an argument. The conversion that 
  1995   Note that this conversion needs a context as an argument. The conversion that 
  1994   goes under an application is @{ML Conv.combination_conv}. It expects two conversions 
  1996   goes under an application is @{ML [index] combination_conv in Conv}. It expects two conversions 
  1995   as arguments, each of which is applied to the corresponding ``branch'' of the
  1997   as arguments, each of which is applied to the corresponding ``branch'' of the
  1996   application. 
  1998   application. 
  1997 
  1999 
  1998   We can now apply all these functions in a conversion that recursively
  2000   We can now apply all these functions in a conversion that recursively
  1999   descends a term and applies a ``@{thm [source] true_conj1}''-conversion 
  2001   descends a term and applies a ``@{thm [source] true_conj1}''-conversion 
  2057 \<equiv> if P (1 \<noteq> 2) then True \<and> True else True \<and> False"}
  2059 \<equiv> if P (1 \<noteq> 2) then True \<and> True else True \<and> False"}
  2058 *}
  2060 *}
  2059 
  2061 
  2060 text {*
  2062 text {*
  2061   So far we only applied conversions to @{ML_type cterm}s. Conversions can, however, 
  2063   So far we only applied conversions to @{ML_type cterm}s. Conversions can, however, 
  2062   also work on theorems using the function @{ML "Conv.fconv_rule"}. As an example, 
  2064   also work on theorems using the function @{ML [index] fconv_rule in Conv}. As an example, 
  2063   consider the conversion @{ML all_true1_conv} and the lemma:
  2065   consider the conversion @{ML all_true1_conv} and the lemma:
  2064 *}
  2066 *}
  2065 
  2067 
  2066 lemma foo_test: "P \<or> (True \<and> \<not>P)" by simp
  2068 lemma foo_test: "P \<or> (True \<and> \<not>P)" by simp
  2067 
  2069 
  2072   @{ML_response_fake [display,gray]
  2074   @{ML_response_fake [display,gray]
  2073   "Conv.fconv_rule (all_true1_conv @{context}) @{thm foo_test}" 
  2075   "Conv.fconv_rule (all_true1_conv @{context}) @{thm foo_test}" 
  2074   "?P \<or> \<not> ?P"}
  2076   "?P \<or> \<not> ?P"}
  2075 
  2077 
  2076   Finally, conversions can also be turned into tactics and then applied to
  2078   Finally, conversions can also be turned into tactics and then applied to
  2077   goal states. This can be done with the help of the function @{ML CONVERSION},
  2079   goal states. This can be done with the help of the function @{ML [index] CONVERSION},
  2078   and also some predefined conversion combinators that traverse a goal
  2080   and also some predefined conversion combinators that traverse a goal
  2079   state. The combinators for the goal state are: @{ML Conv.params_conv} for
  2081   state. The combinators for the goal state are: @{ML [index] params_conv in Conv} for
  2080   converting under parameters (i.e.~where goals are of the form @{text "\<And>x. P \<Longrightarrow>
  2082   converting under parameters (i.e.~where goals are of the form @{text "\<And>x. P \<Longrightarrow>
  2081   Q"}); the function @{ML Conv.prems_conv} for applying a conversion to all
  2083   Q"}); the function @{ML [index] prems_conv in Conv} for applying a conversion to all
  2082   premises of a goal, and @{ML Conv.concl_conv} for applying a conversion to
  2084   premises of a goal, and @{ML [index] concl_conv in Conv} for applying a conversion to
  2083   the conclusion of a goal.
  2085   the conclusion of a goal.
  2084 
  2086 
  2085   Assume we want to apply @{ML all_true1_conv} only in the conclusion
  2087   Assume we want to apply @{ML all_true1_conv} only in the conclusion
  2086   of the goal, and @{ML if_true1_conv} should only apply to the premises.
  2088   of the goal, and @{ML if_true1_conv} should only apply to the premises.
  2087   Here is a tactic doing exactly that:
  2089   Here is a tactic doing exactly that: