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