1805 \begin{proof} |
1805 \begin{proof} |
1806 By induction on @{text x}. The equation follow by simple unfolding |
1806 By induction on @{text x}. The equation follow by simple unfolding |
1807 of the definitions. |
1807 of the definitions. |
1808 \end{proof} |
1808 \end{proof} |
1809 |
1809 |
|
1810 \noindent |
1810 The first property states that a permutation applied to a binding function is |
1811 The first property states that a permutation applied to a binding function is |
1811 equivalent to first permuting the binders and then calculating the bound |
1812 equivalent to first permuting the binders and then calculating the bound |
1812 variables. The second amounts to the fact that permuting the binders has no |
1813 variables. The second amounts to the fact that permuting the binders has no |
1813 effect on the free-variable function. |
1814 effect on the free-variable function. The main point of this permutation |
1814 |
1815 function, however, is that if we have a permutation that is fresh |
1815 This notion allows is to strengthen the induction principles. We will explain |
1816 for the support of an object @{text x}, then we can use this permutation |
1816 the details with the @{text "Let"} term-constructor from the example shown |
1817 to rename the binders, without ``changing'' the term. In case of the |
1817 in \eqref{letpat}. |
1818 @{text "Let"} term-constructor from the example shown |
1818 Instead of establishing the implication |
1819 in \eqref{letpat} this means: |
|
1820 |
|
1821 \begin{center} |
|
1822 if @{term "supp (Abs_lst (bn p) t) \<sharp>* q"} then @{text "Let p t = Let (q \<bullet>\<^bsub>bn\<^bsub>pat\<^esub>\<^esub> p) (q \<bullet> t)"} |
|
1823 \end{center} |
|
1824 |
|
1825 \noindent |
|
1826 This fact will be used when establishing the strong induction principles. |
|
1827 They state that instead of establishing the implication |
1819 |
1828 |
1820 \begin{center} |
1829 \begin{center} |
1821 @{text "\<forall>p t\<^isub>1 t\<^isub>2. P\<^bsub>pat\<^esub> p \<and> P\<^bsub>trm\<^esub> t\<^isub>1 \<and> P\<^bsub>trm\<^esub> t\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub> (Let p t\<^isub>1 t\<^isub>2)"} |
1830 @{text "\<forall>p t\<^isub>1 t\<^isub>2. P\<^bsub>pat\<^esub> p \<and> P\<^bsub>trm\<^esub> t\<^isub>1 \<and> P\<^bsub>trm\<^esub> t\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub> (Let p t\<^isub>1 t\<^isub>2)"} |
1822 \end{center} |
1831 \end{center} |
1823 |
1832 |
1824 \noindent |
1833 \noindent |
1825 for the weak induction principle, we will show that it is sufficient |
1834 it is sufficient to establish the following implication |
1826 to establish |
|
1827 |
1835 |
1828 \begin{center} |
1836 \begin{center} |
1829 \begin{tabular}{l} |
1837 \begin{tabular}{l} |
1830 @{text "\<forall>p t\<^isub>1 t\<^isub>2 c."}\\ |
1838 @{text "\<forall>p t\<^isub>1 t\<^isub>2 c."}\\ |
1831 \hspace{5mm}@{text "set (bn\<^sup>\<alpha> p) #\<^sup>* c \<and>"}\\ |
1839 \hspace{5mm}@{text "set (bn\<^sup>\<alpha> p) #\<^sup>* c \<and>"}\\ |
1833 \hspace{15mm}@{text "\<Rightarrow> P\<^bsub>trm\<^esub> c (Let p t\<^isub>1 t\<^isub>2)"} |
1841 \hspace{15mm}@{text "\<Rightarrow> P\<^bsub>trm\<^esub> c (Let p t\<^isub>1 t\<^isub>2)"} |
1834 \end{tabular} |
1842 \end{tabular} |
1835 \end{center} |
1843 \end{center} |
1836 |
1844 |
1837 \noindent |
1845 \noindent |
1838 While this implication contains additional arguments (i.e.~@{text c}) and |
1846 While this implication contains an additional argument, @{text c}, and |
1839 additional universal quantifications, it is usually easier to establish. |
1847 also additional universal quantifications, it is usually easier to establish. |
1840 The reason is that in the case of @{text "Let"} we can make the freshness |
1848 The reason is that in the case of @{text "Let"} we can make the freshness |
1841 assumption @{text "set (bn\<^sup>\<alpha> p) #\<^sup>* c"}, wherby @{text c} can be arbitrarily |
1849 assumption @{text "set (bn\<^sup>\<alpha> p) #\<^sup>* c"}, wherby @{text c} can be arbitrarily |
1842 chosen as long as it has finite support. |
1850 chosen by the user as long as it has finite support. |
1843 |
1851 |
1844 With the help of @{text "\<bullet>bn"} functions defined in the previous section |
1852 With the help of @{text "\<bullet>bn"} functions defined in the previous section |
1845 we can show that binders can be substituted in term constructors. We show |
1853 we can show that binders can be substituted in term constructors. We show |
1846 this only for the specification from Figure~\ref{nominalcorehas}. The only |
1854 this only for the specification from Figure~\ref{nominalcorehas}. The only |
1847 constructor with a complicated binding structure is @{text "ACons"}. For this |
1855 constructor with a complicated binding structure is @{text "ACons"}. For this |