1722 added to the simplifier, because now the right-hand side is not anymore an instance |
1722 added to the simplifier, because now the right-hand side is not anymore an instance |
1723 of the left-hand side. In a sense it freezes all redexes of permutation compositions |
1723 of the left-hand side. In a sense it freezes all redexes of permutation compositions |
1724 after one step. In this way, we can split simplification of permutations |
1724 after one step. In this way, we can split simplification of permutations |
1725 into three phases without the user noticing anything about the auxiliary |
1725 into three phases without the user noticing anything about the auxiliary |
1726 constant. We first freeze any instance of permutation compositions in the term using |
1726 constant. We first freeze any instance of permutation compositions in the term using |
1727 lemma @{thm [source] "perm_aux_expand"} (Line 9); |
1727 lemma @{thm [source] "perm_aux_expand"} (Line 10); |
1728 then simplify all other permutations including pushing permutations over |
1728 then simplify all other permutations including pushing permutations over |
1729 other permutations by rule @{thm [source] perm_compose_aux} (Line 10); and |
1729 other permutations by rule @{thm [source] perm_compose_aux} (Line 11); and |
1730 finally ``unfreeze'' all instances of permutation compositions by unfolding |
1730 finally ``unfreeze'' all instances of permutation compositions by unfolding |
1731 the definition of the auxiliary constant. |
1731 the definition of the auxiliary constant. |
1732 \<close> |
1732 \<close> |
1733 |
1733 |
1734 ML %linenosgray\<open>fun perm_simp_tac ctxt = |
1734 ML %linenosgray\<open>fun perm_simp_tac ctxt = |
1798 NONE |
1798 NONE |
1799 end\<close> |
1799 end\<close> |
1800 |
1800 |
1801 text \<open> |
1801 text \<open> |
1802 This function takes a simpset and a redex (a @{ML_type cterm}) as |
1802 This function takes a simpset and a redex (a @{ML_type cterm}) as |
1803 arguments. In Lines 3 and~4, we first extract the context from the given |
1803 arguments and prints out a message containing the redex. The function |
1804 simpset and then print out a message containing the redex. The function |
|
1805 returns @{ML NONE} (standing for an optional @{ML_type thm}) since at the |
1804 returns @{ML NONE} (standing for an optional @{ML_type thm}) since at the |
1806 moment we are \emph{not} interested in actually rewriting anything. We want |
1805 moment we are \emph{not} interested in actually rewriting anything. We want |
1807 that the simproc is triggered by the pattern @{term "Suc n"}. This can be |
1806 that the simproc is triggered by the pattern @{term "Suc n"}. This can be |
1808 done by adding the simproc to the current simpset as follows |
1807 done by adding the simproc to the current simpset as follows |
1809 \<close> |
1808 \<close> |
2516 assumption in @{ML unabs_def} is that the right-hand side is an |
2515 assumption in @{ML unabs_def} is that the right-hand side is an |
2517 abstraction. We compute the possibly empty list of abstracted variables in |
2516 abstraction. We compute the possibly empty list of abstracted variables in |
2518 Line 4 using the function @{ML_ind strip_abs_vars in Term}. For this we have to |
2517 Line 4 using the function @{ML_ind strip_abs_vars in Term}. For this we have to |
2519 first transform the @{ML_type cterm} into a @{ML_type term}. In Line 5 we |
2518 first transform the @{ML_type cterm} into a @{ML_type term}. In Line 5 we |
2520 import these variables into the context \<open>ctxt'\<close>, in order to |
2519 import these variables into the context \<open>ctxt'\<close>, in order to |
2521 export them again in Line 15. In Line 8 we certify the list of variables, |
2520 export them again in Line 14. In Line 7 we certify the list of variables, |
2522 which in turn we apply to the @{ML_text lhs} of the definition using the |
2521 which in turn we apply to the @{ML_text lhs} of the definition using the |
2523 function @{ML_ind list_comb in Drule}. In Line 11 and 12 we generate the |
2522 function @{ML_ind list_comb in Drule}. In Line 10 and 11 we generate the |
2524 conversion according to the length of the list of (abstracted) variables. If |
2523 conversion according to the length of the list of (abstracted) variables. If |
2525 there are none, then we just return the conversion corresponding to the |
2524 there are none, then we just return the conversion corresponding to the |
2526 original definition. If there are variables, then we have to prefix this |
2525 original definition. If there are variables, then we have to prefix this |
2527 conversion with @{ML_ind fun_conv in Conv}. Now in Line 14 we only have to |
2526 conversion with @{ML_ind fun_conv in Conv}. Now in Line 13 we only have to |
2528 apply the new left-hand side to the generated conversion and obtain the the |
2527 apply the new left-hand side to the generated conversion and obtain the the |
2529 theorem we want to construct. As mentioned above, in Line 15 we only have to |
2528 theorem we want to construct. As mentioned above, in Line 14 we only have to |
2530 export the context \<open>ctxt'\<close> back to \<open>ctxt\<close> in order to |
2529 export the context \<open>ctxt'\<close> back to \<open>ctxt\<close> in order to |
2531 produce meta-variables for the theorem. An example is as follows. |
2530 produce meta-variables for the theorem. An example is as follows. |
2532 |
2531 |
2533 @{ML_response [display, gray] |
2532 @{ML_response [display, gray] |
2534 \<open>unabs_def @{context} @{thm id2_def}\<close> |
2533 \<open>unabs_def @{context} @{thm id2_def}\<close> |