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_ind [index] etac}, @{ML_ind [index] rtac} and @{ML_ind [index] atac} |
59 The tactics @{ML_ind etac}, @{ML_ind rtac} and @{ML_ind atac} |
60 in the code above correspond |
60 in the code above correspond |
61 roughly to @{text erule}, @{text rule} and @{text assumption}, respectively. |
61 roughly to @{text erule}, @{text rule} and @{text assumption}, respectively. |
62 The operator @{ML_ind [index] THEN} strings the tactics together. |
62 The operator @{ML_ind THEN} strings the tactics together. |
63 |
63 |
64 \begin{readmore} |
64 \begin{readmore} |
65 To learn more about the function @{ML_ind [index] prove in Goal} see \isccite{sec:results} |
65 To learn more about the function @{ML_ind prove in Goal} see \isccite{sec:results} |
66 and the file @{ML_file "Pure/goal.ML"}. See @{ML_file |
66 and the file @{ML_file "Pure/goal.ML"}. See @{ML_file |
67 "Pure/tactic.ML"} and @{ML_file "Pure/tactical.ML"} for the code of basic |
67 "Pure/tactic.ML"} and @{ML_file "Pure/tactical.ML"} for the code of basic |
68 tactics and tactic combinators; see also Chapters 3 and 4 in the old |
68 tactics and tactic combinators; see also Chapters 3 and 4 in the old |
69 Isabelle Reference Manual, and Chapter 3 in the Isabelle/Isar Implementation Manual. |
69 Isabelle Reference Manual, and Chapter 3 in the Isabelle/Isar Implementation Manual. |
70 \end{readmore} |
70 \end{readmore} |
118 THEN' atac |
118 THEN' atac |
119 THEN' rtac @{thm disjI1} |
119 THEN' rtac @{thm disjI1} |
120 THEN' atac)*}text_raw{*\label{tac:footacprime}*} |
120 THEN' atac)*}text_raw{*\label{tac:footacprime}*} |
121 |
121 |
122 text {* |
122 text {* |
123 where @{ML_ind [index] THEN'} is used instead of @{ML THEN}. With @{ML foo_tac'} you can give |
123 where @{ML_ind THEN'} is used instead of @{ML THEN}. With @{ML foo_tac'} you can give |
124 the number for the subgoal explicitly when the tactic is |
124 the number for the subgoal explicitly when the tactic is |
125 called. So in the next proof you can first discharge the second subgoal, and |
125 called. So in the next proof you can first discharge the second subgoal, and |
126 subsequently the first. |
126 subsequently the first. |
127 *} |
127 *} |
128 |
128 |
159 By convention, if a tactic fails, then it should return the empty sequence. |
159 By convention, if a tactic fails, then it should return the empty sequence. |
160 Therefore, if you write your own tactics, they should not raise exceptions |
160 Therefore, if you write your own tactics, they should not raise exceptions |
161 willy-nilly; only in very grave failure situations should a tactic raise the |
161 willy-nilly; only in very grave failure situations should a tactic raise the |
162 exception @{text THM}. |
162 exception @{text THM}. |
163 |
163 |
164 The simplest tactics are @{ML_ind [index] no_tac} and @{ML_ind [index] all_tac}. The first returns |
164 The simplest tactics are @{ML_ind no_tac} and @{ML_ind all_tac}. The first returns |
165 the empty sequence and is defined as |
165 the empty sequence and is defined as |
166 *} |
166 *} |
167 |
167 |
168 ML{*fun no_tac thm = Seq.empty*} |
168 ML{*fun no_tac thm = Seq.empty*} |
169 |
169 |
334 *} |
334 *} |
335 |
335 |
336 section {* Simple Tactics\label{sec:simpletacs} *} |
336 section {* Simple Tactics\label{sec:simpletacs} *} |
337 |
337 |
338 text {* |
338 text {* |
339 Let us start with explaining the simple tactic @{ML_ind [index] print_tac}, which is quite useful |
339 Let us start with explaining the simple tactic @{ML_ind print_tac}, which is quite useful |
340 for low-level debugging of tactics. It just prints out a message and the current |
340 for low-level debugging of tactics. It just prints out a message and the current |
341 goal state. Unlike @{ML my_print_tac} shown earlier, it prints the goal state |
341 goal state. Unlike @{ML my_print_tac} shown earlier, it prints the goal state |
342 as the user would see it. For example, processing the proof |
342 as the user would see it. For example, processing the proof |
343 *} |
343 *} |
344 |
344 |
354 *} |
354 *} |
355 (*<*)oops(*>*) |
355 (*<*)oops(*>*) |
356 |
356 |
357 text {* |
357 text {* |
358 A simple tactic for easy discharge of any proof obligations is |
358 A simple tactic for easy discharge of any proof obligations is |
359 @{ML_ind [index] cheat_tac in SkipProof}. This tactic corresponds to |
359 @{ML_ind cheat_tac in SkipProof}. This tactic corresponds to |
360 the Isabelle command \isacommand{sorry} and is sometimes useful |
360 the Isabelle command \isacommand{sorry} and is sometimes useful |
361 during the development of tactics. |
361 during the development of tactics. |
362 *} |
362 *} |
363 |
363 |
364 lemma shows "False" and "Goldbach_conjecture" |
364 lemma shows "False" and "Goldbach_conjecture" |
370 |
370 |
371 text {* |
371 text {* |
372 This tactic works however only if the quick-and-dirty mode of Isabelle |
372 This tactic works however only if the quick-and-dirty mode of Isabelle |
373 is switched on. |
373 is switched on. |
374 |
374 |
375 Another simple tactic is the function @{ML_ind [index] atac}, which, as shown in the previous |
375 Another simple tactic is the function @{ML_ind atac}, which, as shown in the previous |
376 section, corresponds to the assumption command. |
376 section, corresponds to the assumption command. |
377 *} |
377 *} |
378 |
378 |
379 lemma shows "P \<Longrightarrow> P" |
379 lemma shows "P \<Longrightarrow> P" |
380 apply(tactic {* atac 1 *}) |
380 apply(tactic {* atac 1 *}) |
382 @{subgoals [display]} |
382 @{subgoals [display]} |
383 \end{minipage}*} |
383 \end{minipage}*} |
384 (*<*)oops(*>*) |
384 (*<*)oops(*>*) |
385 |
385 |
386 text {* |
386 text {* |
387 Similarly, @{ML_ind [index] rtac}, @{ML_ind [index] dtac}, @{ML_ind [index] etac} and |
387 Similarly, @{ML_ind rtac}, @{ML_ind dtac}, @{ML_ind etac} and |
388 @{ML_ind [index] ftac} correspond (roughly) |
388 @{ML_ind ftac} correspond (roughly) |
389 to @{text rule}, @{text drule}, @{text erule} and @{text frule}, |
389 to @{text rule}, @{text drule}, @{text erule} and @{text frule}, |
390 respectively. Each of them takes a theorem as argument and attempts to |
390 respectively. Each of them takes a theorem as argument and attempts to |
391 apply it to a goal. Below are three self-explanatory examples. |
391 apply it to a goal. Below are three self-explanatory examples. |
392 *} |
392 *} |
393 |
393 |
411 @{subgoals [display]} |
411 @{subgoals [display]} |
412 \end{minipage}*} |
412 \end{minipage}*} |
413 (*<*)oops(*>*) |
413 (*<*)oops(*>*) |
414 |
414 |
415 text {* |
415 text {* |
416 The function @{ML_ind [index] resolve_tac} is similar to @{ML_ind [index] rtac}, except that it |
416 The function @{ML_ind resolve_tac} is similar to @{ML_ind rtac}, except that it |
417 expects a list of theorems as arguments. From this list it will apply the |
417 expects a list of theorems as arguments. From this list it will apply the |
418 first applicable theorem (later theorems that are also applicable can be |
418 first applicable theorem (later theorems that are also applicable can be |
419 explored via the lazy sequences mechanism). Given the code |
419 explored via the lazy sequences mechanism). Given the code |
420 *} |
420 *} |
421 |
421 |
434 \end{minipage}*} |
434 \end{minipage}*} |
435 (*<*)oops(*>*) |
435 (*<*)oops(*>*) |
436 |
436 |
437 text {* |
437 text {* |
438 Similar versions taking a list of theorems exist for the tactics |
438 Similar versions taking a list of theorems exist for the tactics |
439 @{ML dtac} (@{ML_ind [index] dresolve_tac}), @{ML etac} |
439 @{ML dtac} (@{ML_ind dresolve_tac}), @{ML etac} |
440 (@{ML_ind [index] eresolve_tac}) and so on. |
440 (@{ML_ind eresolve_tac}) and so on. |
441 |
441 |
442 |
442 |
443 Another simple tactic is @{ML_ind [index] cut_facts_tac}. It inserts a list of theorems |
443 Another simple tactic is @{ML_ind cut_facts_tac}. It inserts a list of theorems |
444 into the assumptions of the current goal state. For example |
444 into the assumptions of the current goal state. For example |
445 *} |
445 *} |
446 |
446 |
447 lemma shows "True \<noteq> False" |
447 lemma shows "True \<noteq> False" |
448 apply(tactic {* cut_facts_tac [@{thm True_def}, @{thm False_def}] 1 *}) |
448 apply(tactic {* cut_facts_tac [@{thm True_def}, @{thm False_def}] 1 *}) |
473 applied to the first subgoal might instantiate this meta-variable in such a |
473 applied to the first subgoal might instantiate this meta-variable in such a |
474 way that the second subgoal becomes unprovable. If it is clear what the @{text "?x"} |
474 way that the second subgoal becomes unprovable. If it is clear what the @{text "?x"} |
475 should be, then this situation can be avoided by introducing a more |
475 should be, then this situation can be avoided by introducing a more |
476 constrained version of the @{text bspec}-rule. Such constraints can be given by |
476 constrained version of the @{text bspec}-rule. Such constraints can be given by |
477 pre-instantiating theorems with other theorems. One function to do this is |
477 pre-instantiating theorems with other theorems. One function to do this is |
478 @{ML_ind [index] "RS"} |
478 @{ML_ind "RS"} |
479 |
479 |
480 @{ML_response_fake [display,gray] |
480 @{ML_response_fake [display,gray] |
481 "@{thm disjI1} RS @{thm conjI}" "\<lbrakk>?P1; ?Q\<rbrakk> \<Longrightarrow> (?P1 \<or> ?Q1) \<and> ?Q"} |
481 "@{thm disjI1} RS @{thm conjI}" "\<lbrakk>?P1; ?Q\<rbrakk> \<Longrightarrow> (?P1 \<or> ?Q1) \<and> ?Q"} |
482 |
482 |
483 which in the example instantiates the first premise of the @{text conjI}-rule |
483 which in the example instantiates the first premise of the @{text conjI}-rule |
487 @{ML_response_fake_both [display,gray] |
487 @{ML_response_fake_both [display,gray] |
488 "@{thm conjI} RS @{thm mp}" |
488 "@{thm conjI} RS @{thm mp}" |
489 "*** Exception- THM (\"RSN: no unifiers\", 1, |
489 "*** Exception- THM (\"RSN: no unifiers\", 1, |
490 [\"\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q\", \"\<lbrakk>?P \<longrightarrow> ?Q; ?P\<rbrakk> \<Longrightarrow> ?Q\"]) raised"} |
490 [\"\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q\", \"\<lbrakk>?P \<longrightarrow> ?Q; ?P\<rbrakk> \<Longrightarrow> ?Q\"]) raised"} |
491 |
491 |
492 then the function raises an exception. The function @{ML_ind [index] RSN} is similar to @{ML RS}, but |
492 then the function raises an exception. The function @{ML_ind RSN} is similar to @{ML RS}, but |
493 takes an additional number as argument that makes explicit which premise |
493 takes an additional number as argument that makes explicit which premise |
494 should be instantiated. |
494 should be instantiated. |
495 |
495 |
496 To improve readability of the theorems we shall produce below, we will use the |
496 To improve readability of the theorems we shall produce below, we will use the |
497 function @{ML no_vars} from Section~\ref{sec:printing}, which transforms |
497 function @{ML no_vars} from Section~\ref{sec:printing}, which transforms |
500 |
500 |
501 @{ML_response_fake [display,gray] |
501 @{ML_response_fake [display,gray] |
502 "no_vars @{context} (@{thm disjI1} RS @{thm conjI})" "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> (P \<or> Qa) \<and> Q"} |
502 "no_vars @{context} (@{thm disjI1} RS @{thm conjI})" "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> (P \<or> Qa) \<and> Q"} |
503 |
503 |
504 If you want to instantiate more than one premise of a theorem, you can use |
504 If you want to instantiate more than one premise of a theorem, you can use |
505 the function @{ML_ind [index] MRS}: |
505 the function @{ML_ind MRS}: |
506 |
506 |
507 @{ML_response_fake [display,gray] |
507 @{ML_response_fake [display,gray] |
508 "no_vars @{context} ([@{thm disjI1}, @{thm disjI2}] MRS @{thm conjI})" |
508 "no_vars @{context} ([@{thm disjI1}, @{thm disjI2}] MRS @{thm conjI})" |
509 "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> (P \<or> Qa) \<and> (Pa \<or> Q)"} |
509 "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> (P \<or> Qa) \<and> (Pa \<or> Q)"} |
510 |
510 |
511 If you need to instantiate lists of theorems, you can use the |
511 If you need to instantiate lists of theorems, you can use the |
512 functions @{ML RL} and @{ML_ind [index] MRL}. For example in the code below, |
512 functions @{ML RL} and @{ML_ind MRL}. For example in the code below, |
513 every theorem in the second list is instantiated with every |
513 every theorem in the second list is instantiated with every |
514 theorem in the first. |
514 theorem in the first. |
515 |
515 |
516 @{ML_response_fake [display,gray] |
516 @{ML_response_fake [display,gray] |
517 "map (no_vars @{context}) |
517 "map (no_vars @{context}) |
526 \end{readmore} |
526 \end{readmore} |
527 |
527 |
528 Often proofs on the ML-level involve elaborate operations on assumptions and |
528 Often proofs on the ML-level involve elaborate operations on assumptions and |
529 @{text "\<And>"}-quantified variables. To do such operations using the basic tactics |
529 @{text "\<And>"}-quantified variables. To do such operations using the basic tactics |
530 shown so far is very unwieldy and brittle. Some convenience and |
530 shown so far is very unwieldy and brittle. Some convenience and |
531 safety is provided by the functions @{ML_ind [index] FOCUS in Subgoal} and |
531 safety is provided by the functions @{ML_ind FOCUS in Subgoal} and |
532 @{ML_ind [index] SUBPROOF}. These tactics fix the parameters |
532 @{ML_ind SUBPROOF}. These tactics fix the parameters |
533 and bind the various components of a goal state to a record. |
533 and bind the various components of a goal state to a record. |
534 To see what happens, use the function defined in Figure~\ref{fig:sptac}, which |
534 To see what happens, use the function defined in Figure~\ref{fig:sptac}, which |
535 takes a record and just prints out the contents of this record. Consider |
535 takes a record and just prints out the contents of this record. Consider |
536 now the proof: |
536 now the proof: |
537 *} |
537 *} |
666 \isccite{sec:results}. |
666 \isccite{sec:results}. |
667 \end{readmore} |
667 \end{readmore} |
668 |
668 |
669 Similar but less powerful functions than @{ML FOCUS in Subgoal}, respectively |
669 Similar but less powerful functions than @{ML FOCUS in Subgoal}, respectively |
670 @{ML SUBPROOF}, are |
670 @{ML SUBPROOF}, are |
671 @{ML_ind [index] SUBGOAL} and @{ML_ind [index] CSUBGOAL}. They allow you to |
671 @{ML_ind SUBGOAL} and @{ML_ind CSUBGOAL}. They allow you to |
672 inspect a given subgoal (the former |
672 inspect a given subgoal (the former |
673 presents the subgoal as a @{ML_type term}, while the latter as a @{ML_type |
673 presents the subgoal as a @{ML_type term}, while the latter as a @{ML_type |
674 cterm}). With this you can implement a tactic that applies a rule according |
674 cterm}). With this you can implement a tactic that applies a rule according |
675 to the topmost logic connective in the subgoal (to illustrate this we only |
675 to the topmost logic connective in the subgoal (to illustrate this we only |
676 analyse a few connectives). The code of the tactic is as |
676 analyse a few connectives). The code of the tactic is as |
778 it is consistently applied to the component tactics. |
778 it is consistently applied to the component tactics. |
779 For most tactic combinators such a ``primed'' version exists and |
779 For most tactic combinators such a ``primed'' version exists and |
780 in what follows we will usually prefer it over the ``unprimed'' one. |
780 in what follows we will usually prefer it over the ``unprimed'' one. |
781 |
781 |
782 If there is a list of tactics that should all be tried out in |
782 If there is a list of tactics that should all be tried out in |
783 sequence, you can use the combinator @{ML_ind [index] EVERY'}. For example |
783 sequence, you can use the combinator @{ML_ind EVERY'}. For example |
784 the function @{ML foo_tac'} from page~\pageref{tac:footacprime} can also |
784 the function @{ML foo_tac'} from page~\pageref{tac:footacprime} can also |
785 be written as: |
785 be written as: |
786 *} |
786 *} |
787 |
787 |
788 ML{*val foo_tac'' = EVERY' [etac @{thm disjE}, rtac @{thm disjI2}, |
788 ML{*val foo_tac'' = EVERY' [etac @{thm disjE}, rtac @{thm disjI2}, |
800 atac, rtac @{thm disjI1}, atac]*} |
800 atac, rtac @{thm disjI1}, atac]*} |
801 |
801 |
802 text {* |
802 text {* |
803 and call @{ML foo_tac1}. |
803 and call @{ML foo_tac1}. |
804 |
804 |
805 With the combinators @{ML THEN'}, @{ML EVERY'} and @{ML_ind [index] EVERY1} it must be |
805 With the combinators @{ML THEN'}, @{ML EVERY'} and @{ML_ind EVERY1} it must be |
806 guaranteed that all component tactics successfully apply; otherwise the |
806 guaranteed that all component tactics successfully apply; otherwise the |
807 whole tactic will fail. If you rather want to try out a number of tactics, |
807 whole tactic will fail. If you rather want to try out a number of tactics, |
808 then you can use the combinator @{ML_ind [index] ORELSE'} for two tactics, and @{ML_ind |
808 then you can use the combinator @{ML_ind ORELSE'} for two tactics, and @{ML_ind |
809 [index] FIRST'} (or @{ML_ind [index] FIRST1}) for a list of tactics. For example, the tactic |
809 FIRST'} (or @{ML_ind FIRST1}) for a list of tactics. For example, the tactic |
810 |
810 |
811 *} |
811 *} |
812 |
812 |
813 ML{*val orelse_xmp_tac = rtac @{thm disjI1} ORELSE' rtac @{thm conjI}*} |
813 ML{*val orelse_xmp_tac = rtac @{thm disjI1} ORELSE' rtac @{thm conjI}*} |
814 |
814 |
856 (*<*)oops(*>*) |
856 (*<*)oops(*>*) |
857 |
857 |
858 text {* |
858 text {* |
859 Since such repeated applications of a tactic to the reverse order of |
859 Since such repeated applications of a tactic to the reverse order of |
860 \emph{all} subgoals is quite common, there is the tactic combinator |
860 \emph{all} subgoals is quite common, there is the tactic combinator |
861 @{ML_ind [index] ALLGOALS} that simplifies this. Using this combinator you can simply |
861 @{ML_ind ALLGOALS} that simplifies this. Using this combinator you can simply |
862 write: *} |
862 write: *} |
863 |
863 |
864 lemma shows "A \<and> B" and "A \<longrightarrow> B \<longrightarrow>C" and "\<forall>x. D x" and "E \<Longrightarrow> F" |
864 lemma shows "A \<and> B" and "A \<longrightarrow> B \<longrightarrow>C" and "\<forall>x. D x" and "E \<Longrightarrow> F" |
865 apply(tactic {* ALLGOALS select_tac' *}) |
865 apply(tactic {* ALLGOALS select_tac' *}) |
866 txt{* \begin{minipage}{\textwidth} |
866 txt{* \begin{minipage}{\textwidth} |
869 (*<*)oops(*>*) |
869 (*<*)oops(*>*) |
870 |
870 |
871 text {* |
871 text {* |
872 Remember that we chose to implement @{ML select_tac'} so that it |
872 Remember that we chose to implement @{ML select_tac'} so that it |
873 always succeeds by adding @{ML all_tac} at the end of the tactic |
873 always succeeds by adding @{ML all_tac} at the end of the tactic |
874 list. The same can be achieved with the tactic combinator @{ML_ind [index] TRY}. |
874 list. The same can be achieved with the tactic combinator @{ML_ind TRY}. |
875 For example: |
875 For example: |
876 *} |
876 *} |
877 |
877 |
878 ML{*val select_tac'' = TRY o FIRST' [rtac @{thm conjI}, rtac @{thm impI}, |
878 ML{*val select_tac'' = TRY o FIRST' [rtac @{thm conjI}, rtac @{thm impI}, |
879 rtac @{thm notI}, rtac @{thm allI}]*} |
879 rtac @{thm notI}, rtac @{thm allI}]*} |
902 |
902 |
903 To comply with this convention, we could simply delete the @{ML "K all_tac"} |
903 To comply with this convention, we could simply delete the @{ML "K all_tac"} |
904 from the end of the theorem list. As a result @{ML select_tac'} would only |
904 from the end of the theorem list. As a result @{ML select_tac'} would only |
905 succeed on goals where it can make progress. But for the sake of argument, |
905 succeed on goals where it can make progress. But for the sake of argument, |
906 let us suppose that this deletion is \emph{not} an option. In such cases, you can |
906 let us suppose that this deletion is \emph{not} an option. In such cases, you can |
907 use the combinator @{ML_ind [index] CHANGED} to make sure the subgoal has been changed |
907 use the combinator @{ML_ind CHANGED} to make sure the subgoal has been changed |
908 by the tactic. Because now |
908 by the tactic. Because now |
909 |
909 |
910 *} |
910 *} |
911 |
911 |
912 lemma shows "E \<Longrightarrow> F" |
912 lemma shows "E \<Longrightarrow> F" |
920 |
920 |
921 |
921 |
922 text {* |
922 text {* |
923 We can further extend @{ML select_tac'} so that it not just applies to the topmost |
923 We can further extend @{ML select_tac'} so that it not just applies to the topmost |
924 connective, but also to the ones immediately ``underneath'', i.e.~analyse the goal |
924 connective, but also to the ones immediately ``underneath'', i.e.~analyse the goal |
925 completely. For this you can use the tactic combinator @{ML_ind [index] REPEAT}. As an example |
925 completely. For this you can use the tactic combinator @{ML_ind REPEAT}. As an example |
926 suppose the following tactic |
926 suppose the following tactic |
927 *} |
927 *} |
928 |
928 |
929 ML{*val repeat_xmp_tac = REPEAT (CHANGED (select_tac' 1)) *} |
929 ML{*val repeat_xmp_tac = REPEAT (CHANGED (select_tac' 1)) *} |
930 |
930 |
941 |
941 |
942 text {* |
942 text {* |
943 Here it is crucial that @{ML select_tac'} is prefixed with @{ML CHANGED}, |
943 Here it is crucial that @{ML select_tac'} is prefixed with @{ML CHANGED}, |
944 because otherwise @{ML REPEAT} runs into an infinite loop (it applies the |
944 because otherwise @{ML REPEAT} runs into an infinite loop (it applies the |
945 tactic as long as it succeeds). The function |
945 tactic as long as it succeeds). The function |
946 @{ML_ind [index] REPEAT1} is similar, but runs the tactic at least once (failing if |
946 @{ML_ind REPEAT1} is similar, but runs the tactic at least once (failing if |
947 this is not possible). |
947 this is not possible). |
948 |
948 |
949 If you are after the ``primed'' version of @{ML repeat_xmp_tac}, then you |
949 If you are after the ``primed'' version of @{ML repeat_xmp_tac}, then you |
950 can implement it as |
950 can implement it as |
951 *} |
951 *} |
957 |
957 |
958 If you look closely at the goal state above, then you see the tactics @{ML repeat_xmp_tac} |
958 If you look closely at the goal state above, then you see the tactics @{ML repeat_xmp_tac} |
959 and @{ML repeat_xmp_tac'} are not yet quite what we are after: the problem is |
959 and @{ML repeat_xmp_tac'} are not yet quite what we are after: the problem is |
960 that goals 2 and 3 are not analysed. This is because the tactic |
960 that goals 2 and 3 are not analysed. This is because the tactic |
961 is applied repeatedly only to the first subgoal. To analyse also all |
961 is applied repeatedly only to the first subgoal. To analyse also all |
962 resulting subgoals, you can use the tactic combinator @{ML_ind [index] REPEAT_ALL_NEW}. |
962 resulting subgoals, you can use the tactic combinator @{ML_ind REPEAT_ALL_NEW}. |
963 Suppose the tactic |
963 Suppose the tactic |
964 *} |
964 *} |
965 |
965 |
966 ML{*val repeat_all_new_xmp_tac = REPEAT_ALL_NEW (CHANGED o select_tac')*} |
966 ML{*val repeat_all_new_xmp_tac = REPEAT_ALL_NEW (CHANGED o select_tac')*} |
967 |
967 |
1010 |
1010 |
1011 text {* |
1011 text {* |
1012 Sometimes this leads to confusing behaviour of tactics and also has |
1012 Sometimes this leads to confusing behaviour of tactics and also has |
1013 the potential to explode the search space for tactics. |
1013 the potential to explode the search space for tactics. |
1014 These problems can be avoided by prefixing the tactic with the tactic |
1014 These problems can be avoided by prefixing the tactic with the tactic |
1015 combinator @{ML_ind [index] DETERM}. |
1015 combinator @{ML_ind DETERM}. |
1016 *} |
1016 *} |
1017 |
1017 |
1018 lemma "\<lbrakk>P1 \<or> Q1; P2 \<or> Q2\<rbrakk> \<Longrightarrow> R" |
1018 lemma "\<lbrakk>P1 \<or> Q1; P2 \<or> Q2\<rbrakk> \<Longrightarrow> R" |
1019 apply(tactic {* DETERM (etac @{thm disjE} 1) *}) |
1019 apply(tactic {* DETERM (etac @{thm disjE} 1) *}) |
1020 txt {*\begin{minipage}{\textwidth} |
1020 txt {*\begin{minipage}{\textwidth} |
1047 ML{*val select_tac''' = TRY o select_tac''*} |
1047 ML{*val select_tac''' = TRY o select_tac''*} |
1048 |
1048 |
1049 text {* |
1049 text {* |
1050 then the tactic @{ML select_tac''} will be tried out and any failure is harnessed. |
1050 then the tactic @{ML select_tac''} will be tried out and any failure is harnessed. |
1051 We again have to use the construction with \mbox{@{text "TRY o ..."}} since there is |
1051 We again have to use the construction with \mbox{@{text "TRY o ..."}} since there is |
1052 no primed version of @{ML_ind [index] TRY}. The tactic combinator @{ML_ind [index] TRYALL} will try out |
1052 no primed version of @{ML_ind TRY}. The tactic combinator @{ML_ind TRYALL} will try out |
1053 a tactic on all subgoals. For example the tactic |
1053 a tactic on all subgoals. For example the tactic |
1054 *} |
1054 *} |
1055 |
1055 |
1056 ML{*val triv_tac = TRYALL (rtac @{thm TrueI} ORELSE' etac @{thm FalseE})*} |
1056 ML{*val triv_tac = TRYALL (rtac @{thm TrueI} ORELSE' etac @{thm FalseE})*} |
1057 |
1057 |
1058 text {* |
1058 text {* |
1059 will solve all trivial subgoals involving @{term True} or @{term "False"}. |
1059 will solve all trivial subgoals involving @{term True} or @{term "False"}. |
1060 |
1060 |
1061 (FIXME: say something about @{ML_ind [index] COND} and COND') |
1061 (FIXME: say something about @{ML_ind COND} and COND') |
1062 |
1062 |
1063 (FIXME: PARALLEL-CHOICE PARALLEL-GOALS) |
1063 (FIXME: PARALLEL-CHOICE PARALLEL-GOALS) |
1064 |
1064 |
1065 \begin{readmore} |
1065 \begin{readmore} |
1066 Most tactic combinators described in this section are defined in @{ML_file "Pure/tactical.ML"}. |
1066 Most tactic combinators described in this section are defined in @{ML_file "Pure/tactical.ML"}. |
1116 Implement a tactic that explores all possibilites of applying these rules to |
1116 Implement a tactic that explores all possibilites of applying these rules to |
1117 a propositional formula until a goal state is reached in which all subgoals |
1117 a propositional formula until a goal state is reached in which all subgoals |
1118 are discharged. Note that in Isabelle the left-rules need to be implemented |
1118 are discharged. Note that in Isabelle the left-rules need to be implemented |
1119 as elimination rules. You need to prove separate lemmas corresponding to |
1119 as elimination rules. You need to prove separate lemmas corresponding to |
1120 $\longrightarrow_{L_{1..4}}$. In order to explore all possibilities of applying |
1120 $\longrightarrow_{L_{1..4}}$. In order to explore all possibilities of applying |
1121 the rules, use the tactic combinator @{ML_ind [index] DEPTH_SOLVE}, which searches |
1121 the rules, use the tactic combinator @{ML_ind DEPTH_SOLVE}, which searches |
1122 for a state in which all subgoals are solved. Add also rules for equality and |
1122 for a state in which all subgoals are solved. Add also rules for equality and |
1123 run your tactic on the de Bruijn formulae discussed in Exercise~\ref{ex:debruijn}. |
1123 run your tactic on the de Bruijn formulae discussed in Exercise~\ref{ex:debruijn}. |
1124 \end{exercise} |
1124 \end{exercise} |
1125 |
1125 |
1126 *} |
1126 *} |
1140 the simplifier (in parentheses is their user-level counterpart): |
1140 the simplifier (in parentheses is their user-level counterpart): |
1141 |
1141 |
1142 \begin{isabelle} |
1142 \begin{isabelle} |
1143 \begin{center} |
1143 \begin{center} |
1144 \begin{tabular}{l@ {\hspace{2cm}}l} |
1144 \begin{tabular}{l@ {\hspace{2cm}}l} |
1145 @{ML_ind [index] simp_tac} & @{text "(simp (no_asm))"} \\ |
1145 @{ML_ind simp_tac} & @{text "(simp (no_asm))"} \\ |
1146 @{ML_ind [index] asm_simp_tac} & @{text "(simp (no_asm_simp))"} \\ |
1146 @{ML_ind asm_simp_tac} & @{text "(simp (no_asm_simp))"} \\ |
1147 @{ML_ind [index] full_simp_tac} & @{text "(simp (no_asm_use))"} \\ |
1147 @{ML_ind full_simp_tac} & @{text "(simp (no_asm_use))"} \\ |
1148 @{ML_ind [index] asm_lr_simp_tac} & @{text "(simp (asm_lr))"} \\ |
1148 @{ML_ind asm_lr_simp_tac} & @{text "(simp (asm_lr))"} \\ |
1149 @{ML_ind [index] asm_full_simp_tac} & @{text "(simp)"} |
1149 @{ML_ind asm_full_simp_tac} & @{text "(simp)"} |
1150 \end{tabular} |
1150 \end{tabular} |
1151 \end{center} |
1151 \end{center} |
1152 \end{isabelle} |
1152 \end{isabelle} |
1153 |
1153 |
1154 All of the tactics take a simpset and an integer as argument (the latter as usual |
1154 All of the tactics take a simpset and an integer as argument (the latter as usual |
1228 |
1228 |
1229 The most common combinators to modify simpsets are: |
1229 The most common combinators to modify simpsets are: |
1230 |
1230 |
1231 \begin{isabelle} |
1231 \begin{isabelle} |
1232 \begin{tabular}{ll} |
1232 \begin{tabular}{ll} |
1233 @{ML_ind [index] addsimps} & @{ML_ind [index] delsimps}\\ |
1233 @{ML_ind addsimps} & @{ML_ind delsimps}\\ |
1234 @{ML_ind [index] addcongs} & @{ML_ind [index] delcongs}\\ |
1234 @{ML_ind addcongs} & @{ML_ind delcongs}\\ |
1235 @{ML_ind [index] addsimprocs} & @{ML_ind [index] delsimprocs}\\ |
1235 @{ML_ind addsimprocs} & @{ML_ind delsimprocs}\\ |
1236 \end{tabular} |
1236 \end{tabular} |
1237 \end{isabelle} |
1237 \end{isabelle} |
1238 |
1238 |
1239 (FIXME: What about splitters? @{ML addsplits}, @{ML delsplits}) |
1239 (FIXME: What about splitters? @{ML addsplits}, @{ML delsplits}) |
1240 *} |
1240 *} |
1260 |> tracing |
1260 |> tracing |
1261 end*} |
1261 end*} |
1262 text_raw {* |
1262 text_raw {* |
1263 \end{isabelle} |
1263 \end{isabelle} |
1264 \end{minipage} |
1264 \end{minipage} |
1265 \caption{The function @{ML_ind [index] dest_ss in Simplifier} returns a record containing |
1265 \caption{The function @{ML_ind dest_ss in Simplifier} returns a record containing |
1266 all printable information stored in a simpset. We are here only interested in the |
1266 all printable information stored in a simpset. We are here only interested in the |
1267 simplification rules, congruence rules and simprocs.\label{fig:printss}} |
1267 simplification rules, congruence rules and simprocs.\label{fig:printss}} |
1268 \end{figure} *} |
1268 \end{figure} *} |
1269 |
1269 |
1270 text {* |
1270 text {* |
1271 To see how they work, consider the function in Figure~\ref{fig:printss}, which |
1271 To see how they work, consider the function in Figure~\ref{fig:printss}, which |
1272 prints out some parts of a simpset. If you use it to print out the components of the |
1272 prints out some parts of a simpset. If you use it to print out the components of the |
1273 empty simpset, i.e., @{ML_ind [index] empty_ss} |
1273 empty simpset, i.e., @{ML_ind empty_ss} |
1274 |
1274 |
1275 @{ML_response_fake [display,gray] |
1275 @{ML_response_fake [display,gray] |
1276 "print_ss @{context} empty_ss" |
1276 "print_ss @{context} empty_ss" |
1277 "Simplification rules: |
1277 "Simplification rules: |
1278 Congruences rules: |
1278 Congruences rules: |
1315 |
1315 |
1316 Notice that we had to add these lemmas as meta-equations. The @{ML empty_ss} |
1316 Notice that we had to add these lemmas as meta-equations. The @{ML empty_ss} |
1317 expects this form of the simplification and congruence rules. However, even |
1317 expects this form of the simplification and congruence rules. However, even |
1318 when adding these lemmas to @{ML empty_ss} we do not end up with anything useful yet. |
1318 when adding these lemmas to @{ML empty_ss} we do not end up with anything useful yet. |
1319 |
1319 |
1320 In the context of HOL, the first really useful simpset is @{ML_ind [index] HOL_basic_ss}. While |
1320 In the context of HOL, the first really useful simpset is @{ML_ind HOL_basic_ss}. While |
1321 printing out the components of this simpset |
1321 printing out the components of this simpset |
1322 |
1322 |
1323 @{ML_response_fake [display,gray] |
1323 @{ML_response_fake [display,gray] |
1324 "print_ss @{context} HOL_basic_ss" |
1324 "print_ss @{context} HOL_basic_ss" |
1325 "Simplification rules: |
1325 "Simplification rules: |
1342 apply(tactic {* ALLGOALS (simp_tac HOL_basic_ss) *}) |
1342 apply(tactic {* ALLGOALS (simp_tac HOL_basic_ss) *}) |
1343 done |
1343 done |
1344 |
1344 |
1345 text {* |
1345 text {* |
1346 This behaviour is not because of simplification rules, but how the subgoaler, solver |
1346 This behaviour is not because of simplification rules, but how the subgoaler, solver |
1347 and looper are set up in @{ML_ind [index] HOL_basic_ss}. |
1347 and looper are set up in @{ML_ind HOL_basic_ss}. |
1348 |
1348 |
1349 The simpset @{ML_ind [index] HOL_ss} is an extension of @{ML HOL_basic_ss} containing |
1349 The simpset @{ML_ind HOL_ss} is an extension of @{ML HOL_basic_ss} containing |
1350 already many useful simplification and congruence rules for the logical |
1350 already many useful simplification and congruence rules for the logical |
1351 connectives in HOL. |
1351 connectives in HOL. |
1352 |
1352 |
1353 @{ML_response_fake [display,gray] |
1353 @{ML_response_fake [display,gray] |
1354 "print_ss @{context} HOL_ss" |
1354 "print_ss @{context} HOL_ss" |
1678 |
1678 |
1679 text {* |
1679 text {* |
1680 Here the pattern is given as @{ML_type term} (instead of @{ML_type cterm}). |
1680 Here the pattern is given as @{ML_type term} (instead of @{ML_type cterm}). |
1681 The function also takes a list of patterns that can trigger the simproc. |
1681 The function also takes a list of patterns that can trigger the simproc. |
1682 Now the simproc is set up and can be explicitly added using |
1682 Now the simproc is set up and can be explicitly added using |
1683 @{ML_ind [index] addsimprocs} to a simpset whenever |
1683 @{ML_ind addsimprocs} to a simpset whenever |
1684 needed. |
1684 needed. |
1685 |
1685 |
1686 Simprocs are applied from inside to outside and from left to right. You can |
1686 Simprocs are applied from inside to outside and from left to right. You can |
1687 see this in the proof |
1687 see this in the proof |
1688 *} |
1688 *} |
1764 |
1764 |
1765 ML{*fun dest_suc_trm ((Const (@{const_name "Suc"}, _)) $ t) = 1 + dest_suc_trm t |
1765 ML{*fun dest_suc_trm ((Const (@{const_name "Suc"}, _)) $ t) = 1 + dest_suc_trm t |
1766 | dest_suc_trm t = snd (HOLogic.dest_number t)*} |
1766 | dest_suc_trm t = snd (HOLogic.dest_number t)*} |
1767 |
1767 |
1768 text {* |
1768 text {* |
1769 It uses the library function @{ML_ind [index] dest_number in HOLogic} that transforms |
1769 It uses the library function @{ML_ind dest_number in HOLogic} that transforms |
1770 (Isabelle) terms, like @{term "0::nat"}, @{term "1::nat"}, @{term "2::nat"} and so |
1770 (Isabelle) terms, like @{term "0::nat"}, @{term "1::nat"}, @{term "2::nat"} and so |
1771 on, into integer values. This function raises the exception @{ML TERM}, if |
1771 on, into integer values. This function raises the exception @{ML TERM}, if |
1772 the term is not a number. The next function expects a pair consisting of a term |
1772 the term is not a number. The next function expects a pair consisting of a term |
1773 @{text t} (containing @{term Suc}s) and the corresponding integer value @{text n}. |
1773 @{text t} (containing @{term Suc}s) and the corresponding integer value @{text n}. |
1774 *} |
1774 *} |
1884 |
1884 |
1885 ML{*type conv = cterm -> thm*} |
1885 ML{*type conv = cterm -> thm*} |
1886 |
1886 |
1887 text {* |
1887 text {* |
1888 whereby the produced theorem is always a meta-equality. A simple conversion |
1888 whereby the produced theorem is always a meta-equality. A simple conversion |
1889 is the function @{ML_ind [index] all_conv in Conv}, which maps a @{ML_type cterm} to an |
1889 is the function @{ML_ind all_conv in Conv}, which maps a @{ML_type cterm} to an |
1890 instance of the (meta)reflexivity theorem. For example: |
1890 instance of the (meta)reflexivity theorem. For example: |
1891 |
1891 |
1892 @{ML_response_fake [display,gray] |
1892 @{ML_response_fake [display,gray] |
1893 "Conv.all_conv @{cterm \"Foo \<or> Bar\"}" |
1893 "Conv.all_conv @{cterm \"Foo \<or> Bar\"}" |
1894 "Foo \<or> Bar \<equiv> Foo \<or> Bar"} |
1894 "Foo \<or> Bar \<equiv> Foo \<or> Bar"} |
1895 |
1895 |
1896 Another simple conversion is @{ML_ind [index] no_conv in Conv} which always raises the |
1896 Another simple conversion is @{ML_ind no_conv in Conv} which always raises the |
1897 exception @{ML CTERM}. |
1897 exception @{ML CTERM}. |
1898 |
1898 |
1899 @{ML_response_fake [display,gray] |
1899 @{ML_response_fake [display,gray] |
1900 "Conv.no_conv @{cterm True}" |
1900 "Conv.no_conv @{cterm True}" |
1901 "*** Exception- CTERM (\"no conversion\", []) raised"} |
1901 "*** Exception- CTERM (\"no conversion\", []) raised"} |
1902 |
1902 |
1903 A more interesting conversion is the function @{ML_ind [index] beta_conversion in Thm}: it |
1903 A more interesting conversion is the function @{ML_ind beta_conversion in Thm}: it |
1904 produces a meta-equation between a term and its beta-normal form. For example |
1904 produces a meta-equation between a term and its beta-normal form. For example |
1905 |
1905 |
1906 @{ML_response_fake [display,gray] |
1906 @{ML_response_fake [display,gray] |
1907 "let |
1907 "let |
1908 val add = @{cterm \"\<lambda>x y. x + (y::nat)\"} |
1908 val add = @{cterm \"\<lambda>x y. x + (y::nat)\"} |
1940 @{ML false} is given, then only a single beta-reduction is performed |
1940 @{ML false} is given, then only a single beta-reduction is performed |
1941 on the outer-most level. |
1941 on the outer-most level. |
1942 |
1942 |
1943 The main point of conversions is that they can be used for rewriting |
1943 The main point of conversions is that they can be used for rewriting |
1944 @{ML_type cterm}s. One example is the function |
1944 @{ML_type cterm}s. One example is the function |
1945 @{ML_ind [index] rewr_conv in Conv}, which expects a meta-equation as an |
1945 @{ML_ind rewr_conv in Conv}, which expects a meta-equation as an |
1946 argument. Suppose the following meta-equation. |
1946 argument. Suppose the following meta-equation. |
1947 |
1947 |
1948 *} |
1948 *} |
1949 |
1949 |
1950 lemma true_conj1: "True \<and> P \<equiv> P" by simp |
1950 lemma true_conj1: "True \<and> P \<equiv> P" by simp |
1959 in |
1959 in |
1960 Conv.rewr_conv @{thm true_conj1} ctrm |
1960 Conv.rewr_conv @{thm true_conj1} ctrm |
1961 end" |
1961 end" |
1962 "True \<and> (Foo \<longrightarrow> Bar) \<equiv> Foo \<longrightarrow> Bar"} |
1962 "True \<and> (Foo \<longrightarrow> Bar) \<equiv> Foo \<longrightarrow> Bar"} |
1963 |
1963 |
1964 Note, however, that the function @{ML_ind [index] rewr_conv in Conv} only rewrites the |
1964 Note, however, that the function @{ML_ind rewr_conv in Conv} only rewrites the |
1965 outer-most level of the @{ML_type cterm}. If the given @{ML_type cterm} does not match |
1965 outer-most level of the @{ML_type cterm}. If the given @{ML_type cterm} does not match |
1966 exactly the |
1966 exactly the |
1967 left-hand side of the theorem, then @{ML_ind [index] rewr_conv in Conv} fails, raising |
1967 left-hand side of the theorem, then @{ML_ind rewr_conv in Conv} fails, raising |
1968 the exception @{ML CTERM}. |
1968 the exception @{ML CTERM}. |
1969 |
1969 |
1970 This very primitive way of rewriting can be made more powerful by |
1970 This very primitive way of rewriting can be made more powerful by |
1971 combining several conversions into one. For this you can use conversion |
1971 combining several conversions into one. For this you can use conversion |
1972 combinators. The simplest conversion combinator is @{ML_ind [index] then_conv}, |
1972 combinators. The simplest conversion combinator is @{ML_ind then_conv}, |
1973 which applies one conversion after another. For example |
1973 which applies one conversion after another. For example |
1974 |
1974 |
1975 @{ML_response_fake [display,gray] |
1975 @{ML_response_fake [display,gray] |
1976 "let |
1976 "let |
1977 val conv1 = Thm.beta_conversion false |
1977 val conv1 = Thm.beta_conversion false |
1984 |
1984 |
1985 where we first beta-reduce the term and then rewrite according to |
1985 where we first beta-reduce the term and then rewrite according to |
1986 @{thm [source] true_conj1}. (When running this example recall the |
1986 @{thm [source] true_conj1}. (When running this example recall the |
1987 problem with the pretty-printer normalising all terms.) |
1987 problem with the pretty-printer normalising all terms.) |
1988 |
1988 |
1989 The conversion combinator @{ML_ind [index] else_conv} tries out the |
1989 The conversion combinator @{ML_ind else_conv} tries out the |
1990 first one, and if it does not apply, tries the second. For example |
1990 first one, and if it does not apply, tries the second. For example |
1991 |
1991 |
1992 @{ML_response_fake [display,gray] |
1992 @{ML_response_fake [display,gray] |
1993 "let |
1993 "let |
1994 val conv = Conv.rewr_conv @{thm true_conj1} else_conv Conv.all_conv |
1994 val conv = Conv.rewr_conv @{thm true_conj1} else_conv Conv.all_conv |
2002 Here the conversion of @{thm [source] true_conj1} only applies |
2002 Here the conversion of @{thm [source] true_conj1} only applies |
2003 in the first case, but fails in the second. The whole conversion |
2003 in the first case, but fails in the second. The whole conversion |
2004 does not fail, however, because the combinator @{ML else_conv in Conv} will then |
2004 does not fail, however, because the combinator @{ML else_conv in Conv} will then |
2005 try out @{ML all_conv in Conv}, which always succeeds. |
2005 try out @{ML all_conv in Conv}, which always succeeds. |
2006 |
2006 |
2007 The conversion combinator @{ML_ind [index] try_conv in Conv} constructs a conversion |
2007 The conversion combinator @{ML_ind try_conv in Conv} constructs a conversion |
2008 which is tried out on a term, but in case of failure just does nothing. |
2008 which is tried out on a term, but in case of failure just does nothing. |
2009 For example |
2009 For example |
2010 |
2010 |
2011 @{ML_response_fake [display,gray] |
2011 @{ML_response_fake [display,gray] |
2012 "let |
2012 "let |
2018 "True \<or> P \<equiv> True \<or> P"} |
2018 "True \<or> P \<equiv> True \<or> P"} |
2019 |
2019 |
2020 Apart from the function @{ML beta_conversion in Thm}, which is able to fully |
2020 Apart from the function @{ML beta_conversion in Thm}, which is able to fully |
2021 beta-normalise a term, the conversions so far are restricted in that they |
2021 beta-normalise a term, the conversions so far are restricted in that they |
2022 only apply to the outer-most level of a @{ML_type cterm}. In what follows we |
2022 only apply to the outer-most level of a @{ML_type cterm}. In what follows we |
2023 will lift this restriction. The combinators @{ML_ind [index] fun_conv in Conv} |
2023 will lift this restriction. The combinators @{ML_ind fun_conv in Conv} |
2024 and @{ML_ind [index] arg_conv in Conv} will apply |
2024 and @{ML_ind arg_conv in Conv} will apply |
2025 a conversion to the first, respectively second, argument of an application. |
2025 a conversion to the first, respectively second, argument of an application. |
2026 For example |
2026 For example |
2027 |
2027 |
2028 @{ML_response_fake [display,gray] |
2028 @{ML_response_fake [display,gray] |
2029 "let |
2029 "let |
2038 arguments. Therefore the term must be of the form @{text "(Const \<dots> $ t1) $ t2"}. The |
2038 arguments. Therefore the term must be of the form @{text "(Const \<dots> $ t1) $ t2"}. The |
2039 conversion is then applied to @{text "t2"}, which in the example above |
2039 conversion is then applied to @{text "t2"}, which in the example above |
2040 stands for @{term "True \<and> Q"}. The function @{ML fun_conv in Conv} would apply |
2040 stands for @{term "True \<and> Q"}. The function @{ML fun_conv in Conv} would apply |
2041 the conversion to the term @{text "(Const \<dots> $ t1)"}. |
2041 the conversion to the term @{text "(Const \<dots> $ t1)"}. |
2042 |
2042 |
2043 The function @{ML_ind [index] abs_conv in Conv} applies a conversion under an |
2043 The function @{ML_ind abs_conv in Conv} applies a conversion under an |
2044 abstraction. For example: |
2044 abstraction. For example: |
2045 |
2045 |
2046 @{ML_response_fake [display,gray] |
2046 @{ML_response_fake [display,gray] |
2047 "let |
2047 "let |
2048 val conv = Conv.rewr_conv @{thm true_conj1} |
2048 val conv = Conv.rewr_conv @{thm true_conj1} |
2054 |
2054 |
2055 Note that this conversion needs a context as an argument. We also give the |
2055 Note that this conversion needs a context as an argument. We also give the |
2056 conversion as @{text "(K conv)"}, which is a function that ignores its |
2056 conversion as @{text "(K conv)"}, which is a function that ignores its |
2057 argument (the argument being a sufficiently freshened version of the |
2057 argument (the argument being a sufficiently freshened version of the |
2058 variable that is abstracted and a context). The conversion that goes under |
2058 variable that is abstracted and a context). The conversion that goes under |
2059 an application is @{ML_ind [index] combination_conv in Conv}. It expects two |
2059 an application is @{ML_ind combination_conv in Conv}. It expects two |
2060 conversions as arguments, each of which is applied to the corresponding |
2060 conversions as arguments, each of which is applied to the corresponding |
2061 ``branch'' of the application. An abbreviation for this conversion is the |
2061 ``branch'' of the application. An abbreviation for this conversion is the |
2062 function @{ML_ind [index] comb_conv in Conv}, which applies the same conversion |
2062 function @{ML_ind comb_conv in Conv}, which applies the same conversion |
2063 to both branches. |
2063 to both branches. |
2064 |
2064 |
2065 We can now apply all these functions in a conversion that recursively |
2065 We can now apply all these functions in a conversion that recursively |
2066 descends a term and applies a ``@{thm [source] true_conj1}''-conversion |
2066 descends a term and applies a ``@{thm [source] true_conj1}''-conversion |
2067 in all possible positions. |
2067 in all possible positions. |
2122 \<equiv> if P (1 \<noteq> 2) then True \<and> True else True \<and> False"} |
2122 \<equiv> if P (1 \<noteq> 2) then True \<and> True else True \<and> False"} |
2123 *} |
2123 *} |
2124 |
2124 |
2125 text {* |
2125 text {* |
2126 So far we only applied conversions to @{ML_type cterm}s. Conversions can, however, |
2126 So far we only applied conversions to @{ML_type cterm}s. Conversions can, however, |
2127 also work on theorems using the function @{ML_ind [index] fconv_rule in Conv}. As an example, |
2127 also work on theorems using the function @{ML_ind fconv_rule in Conv}. As an example, |
2128 consider the conversion @{ML all_true1_conv} and the lemma: |
2128 consider the conversion @{ML all_true1_conv} and the lemma: |
2129 *} |
2129 *} |
2130 |
2130 |
2131 lemma foo_test: "P \<or> (True \<and> \<not>P)" by simp |
2131 lemma foo_test: "P \<or> (True \<and> \<not>P)" by simp |
2132 |
2132 |
2142 conv thm |
2142 conv thm |
2143 end" |
2143 end" |
2144 "?P \<or> \<not> ?P"} |
2144 "?P \<or> \<not> ?P"} |
2145 |
2145 |
2146 Finally, conversions can also be turned into tactics and then applied to |
2146 Finally, conversions can also be turned into tactics and then applied to |
2147 goal states. This can be done with the help of the function @{ML_ind [index] CONVERSION}, |
2147 goal states. This can be done with the help of the function @{ML_ind CONVERSION}, |
2148 and also some predefined conversion combinators that traverse a goal |
2148 and also some predefined conversion combinators that traverse a goal |
2149 state. The combinators for the goal state are: |
2149 state. The combinators for the goal state are: |
2150 |
2150 |
2151 \begin{itemize} |
2151 \begin{itemize} |
2152 \item @{ML_ind [index] params_conv in Conv} for converting under parameters |
2152 \item @{ML_ind params_conv in Conv} for converting under parameters |
2153 (i.e.~where goals are of the form @{text "\<And>x. P x \<Longrightarrow> Q x"}) |
2153 (i.e.~where goals are of the form @{text "\<And>x. P x \<Longrightarrow> Q x"}) |
2154 |
2154 |
2155 \item @{ML_ind [index] prems_conv in Conv} for applying a conversion to all |
2155 \item @{ML_ind prems_conv in Conv} for applying a conversion to all |
2156 premises of a goal, and |
2156 premises of a goal, and |
2157 |
2157 |
2158 \item @{ML_ind [index] concl_conv in Conv} for applying a conversion to the |
2158 \item @{ML_ind concl_conv in Conv} for applying a conversion to the |
2159 conclusion of a goal. |
2159 conclusion of a goal. |
2160 \end{itemize} |
2160 \end{itemize} |
2161 |
2161 |
2162 Assume we want to apply @{ML all_true1_conv} only in the conclusion |
2162 Assume we want to apply @{ML all_true1_conv} only in the conclusion |
2163 of the goal, and @{ML if_true1_conv} should only apply to the premises. |
2163 of the goal, and @{ML if_true1_conv} should only apply to the premises. |