equal
deleted
inserted
replaced
186 @{text "\<LET> (y, x) = (3, 2) \<IN> x - y \<END>"} |
186 @{text "\<LET> (y, x) = (3, 2) \<IN> x - y \<END>"} |
187 \]\smallskip |
187 \]\smallskip |
188 |
188 |
189 \noindent |
189 \noindent |
190 As a result, we provide three general binding mechanisms each of which binds |
190 As a result, we provide three general binding mechanisms each of which binds |
191 multiple variables at once, and let the user chose which one is intended |
191 multiple variables at once, and let the user choose which one is intended |
192 when formalising a term-calculus. |
192 when formalising a term-calculus. |
193 |
193 |
194 By providing these general binding mechanisms, however, we have to work |
194 By providing these general binding mechanisms, however, we have to work |
195 around a problem that has been pointed out by Pottier \cite{Pottier06} and |
195 around a problem that has been pointed out by Pottier \cite{Pottier06} and |
196 Cheney \cite{Cheney05}: in @{text "\<LET>"}-constructs of the form |
196 Cheney \cite{Cheney05}: in @{text "\<LET>"}-constructs of the form |
447 *} |
447 *} |
448 |
448 |
449 section {* A Short Review of the Nominal Logic Work *} |
449 section {* A Short Review of the Nominal Logic Work *} |
450 |
450 |
451 text {* |
451 text {* |
452 At its core, Nominal Isabelle is an adaption of the nominal logic work by |
452 At its core, Nominal Isabelle is an adaptation of the nominal logic work by |
453 Pitts \cite{Pitts03}. This adaptation for Isabelle/HOL is described in |
453 Pitts \cite{Pitts03}. This adaptation for Isabelle/HOL is described in |
454 \cite{HuffmanUrban10} (including proofs). We shall briefly review this work |
454 \cite{HuffmanUrban10} (including proofs). We shall briefly review this work |
455 to aid the description of what follows. |
455 to aid the description of what follows. |
456 |
456 |
457 Two central notions in the nominal logic work are sorted atoms and |
457 Two central notions in the nominal logic work are sorted atoms and |
781 @{term "alpha_lst_ex (as, x) equal supp (bs, y)"}\\ |
781 @{term "alpha_lst_ex (as, x) equal supp (bs, y)"}\\ |
782 \end{array} |
782 \end{array} |
783 \end{equation}\smallskip |
783 \end{equation}\smallskip |
784 |
784 |
785 \noindent |
785 \noindent |
786 Note that in these relation we replaced the free-atom function @{text "fa"} |
786 Note that in these relations we replaced the free-atom function @{text "fa"} |
787 with @{term "supp"} and the relation @{text R} with equality. We can show |
787 with @{term "supp"} and the relation @{text R} with equality. We can show |
788 the following two properties: |
788 the following two properties: |
789 |
789 |
790 \begin{lem}\label{alphaeq} |
790 \begin{lem}\label{alphaeq} |
791 The relations $\approx_{\,\textit{set}}^{=, \textit{supp}}$, |
791 The relations $\approx_{\,\textit{set}}^{=, \textit{supp}}$, |
956 text {* |
956 text {* |
957 Our choice of syntax for specifications is influenced by the existing |
957 Our choice of syntax for specifications is influenced by the existing |
958 datatype package of Isabelle/HOL \cite{Berghofer99} |
958 datatype package of Isabelle/HOL \cite{Berghofer99} |
959 and by the syntax of the |
959 and by the syntax of the |
960 Ott-tool \cite{ott-jfp}. For us a specification of a term-calculus is a |
960 Ott-tool \cite{ott-jfp}. For us a specification of a term-calculus is a |
961 collection of (possibly mutual recursive) type declarations, say @{text |
961 collection of (possibly mutually recursive) type declarations, say @{text |
962 "ty\<AL>\<^isub>1, \<dots>, ty\<AL>\<^isub>n"}, and an associated collection of |
962 "ty\<AL>\<^isub>1, \<dots>, ty\<AL>\<^isub>n"}, and an associated collection of |
963 binding functions, say @{text "bn\<AL>\<^isub>1, \<dots>, bn\<AL>\<^isub>m"}. The |
963 binding functions, say @{text "bn\<AL>\<^isub>1, \<dots>, bn\<AL>\<^isub>m"}. The |
964 syntax in Nominal Isabelle for such specifications is schematically as follows: |
964 syntax in Nominal Isabelle for such specifications is schematically as follows: |
965 |
965 |
966 \begin{equation}\label{scheme} |
966 \begin{equation}\label{scheme} |
1887 \[ |
1887 \[ |
1888 @{text "C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r = C\<^sup>\<alpha> x\<PRIME>\<^isub>1 \<dots> x\<PRIME>\<^isub>r"}. |
1888 @{text "C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r = C\<^sup>\<alpha> x\<PRIME>\<^isub>1 \<dots> x\<PRIME>\<^isub>r"}. |
1889 \]\smallskip |
1889 \]\smallskip |
1890 |
1890 |
1891 \noindent |
1891 \noindent |
1892 We call these conditions as \emph{quasi-injectivity}. They correspond to the |
1892 We call these conditions \emph{quasi-injectivity}. They correspond to the |
1893 premises in our alpha-equiva\-lence relations, except that the |
1893 premises in our alpha-equiva\-lence relations, except that the |
1894 relations @{text "\<approx>ty"}$_{1..n}$ are all replaced by equality (and similarly |
1894 relations @{text "\<approx>ty"}$_{1..n}$ are all replaced by equality (and similarly |
1895 the free-atom and binding functions are replaced by their lifted |
1895 the free-atom and binding functions are replaced by their lifted |
1896 counterparts). Recall the alpha-equivalence rules for @{text "Let"} and |
1896 counterparts). Recall the alpha-equivalence rules for @{text "Let"} and |
1897 @{text "Let_rec"} shown in \eqref{rawalpha}. For @{text "Let\<^sup>\<alpha>"} and |
1897 @{text "Let_rec"} shown in \eqref{rawalpha}. For @{text "Let\<^sup>\<alpha>"} and |
1941 \end{equation}\smallskip |
1941 \end{equation}\smallskip |
1942 |
1942 |
1943 \noindent |
1943 \noindent |
1944 whereby the @{text P}$_{1..n}$ are the properties established by the |
1944 whereby the @{text P}$_{1..n}$ are the properties established by the |
1945 induction, and the @{text y}$_{1..n}$ are of type @{text |
1945 induction, and the @{text y}$_{1..n}$ are of type @{text |
1946 "ty\<AL>"}$_{1..n}$. Note that for the term constructors @{text |
1946 "ty\<AL>"}$_{1..n}$. Note that for the term constructor @{text |
1947 "C"}$^\alpha_1$ the induction principle has a hypothesis of the form |
1947 "C"}$^\alpha_1$ the induction principle has a hypothesis of the form |
1948 |
1948 |
1949 \[ |
1949 \[ |
1950 \mbox{@{text "\<forall>x\<^isub>1\<dots>x\<^isub>k. P\<^isub>i x\<^isub>i \<and> \<dots> \<and> P\<^isub>j x\<^isub>j \<Rightarrow> P (C\<AL>\<^sub>1 x\<^isub>1 \<dots> x\<^isub>k)"}} |
1950 \mbox{@{text "\<forall>x\<^isub>1\<dots>x\<^isub>k. P\<^isub>i x\<^isub>i \<and> \<dots> \<and> P\<^isub>j x\<^isub>j \<Rightarrow> P (C\<AL>\<^sub>1 x\<^isub>1 \<dots> x\<^isub>k)"}} |
1951 \]\smallskip |
1951 \]\smallskip |
2205 \]\smallskip |
2205 \]\smallskip |
2206 |
2206 |
2207 \noindent |
2207 \noindent |
2208 They are stronger in the sense that they allow us to assume in the @{text |
2208 They are stronger in the sense that they allow us to assume in the @{text |
2209 "Lam\<^sup>\<alpha>"} and @{text "Let_pat\<^sup>\<alpha>"} cases that the bound atoms |
2209 "Lam\<^sup>\<alpha>"} and @{text "Let_pat\<^sup>\<alpha>"} cases that the bound atoms |
2210 avoid, or being fresh for, a context @{text "c"} (which is assumed to be finitely supported). |
2210 avoid, or are fresh for, a context @{text "c"} (which is assumed to be finitely supported). |
2211 |
2211 |
2212 These stronger cases lemmas can be derived from the `weak' cases lemmas |
2212 These stronger cases lemmas can be derived from the `weak' cases lemmas |
2213 given in \eqref{inductex}. This is trivial in case of patterns (the one on |
2213 given in \eqref{inductex}. This is trivial in case of patterns (the one on |
2214 the right-hand side) since the weak and strong cases lemma coincide (there |
2214 the right-hand side) since the weak and strong cases lemma coincide (there |
2215 is no binding in patterns). Interesting are only the cases for @{text |
2215 is no binding in patterns). Interesting are only the cases for @{text |