changeset 2514 | 69780ae147f5 |
parent 2513 | ae860c95bf9f |
child 2515 | 06a8f782b2c1 |
2513:ae860c95bf9f | 2514:69780ae147f5 |
---|---|
122 % |
122 % |
123 \noindent |
123 \noindent |
124 where @{text z} does not occur freely in the type. In this paper we will |
124 where @{text z} does not occur freely in the type. In this paper we will |
125 give a general binding mechanism and associated notion of $\alpha$-equivalence |
125 give a general binding mechanism and associated notion of $\alpha$-equivalence |
126 that can be used to faithfully represent this kind of binding in Nominal |
126 that can be used to faithfully represent this kind of binding in Nominal |
127 Isabelle. The difficulty of finding the right notion for $\alpha$-equivalence |
127 Isabelle. |
128 can be appreciated in this case by considering that the definition given by |
128 %The difficulty of finding the right notion for $\alpha$-equivalence |
129 Leroy in \cite{Leroy92} is incorrect (it omits a side-condition). |
129 %can be appreciated in this case by considering that the definition given by |
130 %Leroy in \cite{Leroy92} is incorrect (it omits a side-condition). |
|
130 |
131 |
131 However, the notion of $\alpha$-equivalence that is preserved by vacuous |
132 However, the notion of $\alpha$-equivalence that is preserved by vacuous |
132 binders is not always wanted. For example in terms like |
133 binders is not always wanted. For example in terms like |
133 % |
134 % |
134 \begin{equation}\label{one} |
135 \begin{equation}\label{one} |
238 allowed by Ott. One reason is that Ott lets the user specify ``empty'' |
239 allowed by Ott. One reason is that Ott lets the user specify ``empty'' |
239 types like @{text "t ::= t t | \<lambda>x. t"} |
240 types like @{text "t ::= t t | \<lambda>x. t"} |
240 where no clause for variables is given. Arguably, such specifications make |
241 where no clause for variables is given. Arguably, such specifications make |
241 some sense in the context of Coq's type theory (which Ott supports), but not |
242 some sense in the context of Coq's type theory (which Ott supports), but not |
242 at all in a HOL-based environment where every datatype must have a non-empty |
243 at all in a HOL-based environment where every datatype must have a non-empty |
243 set-theoretic model \cite{Berghofer99}. |
244 set-theoretic model. % \cite{Berghofer99}. |
244 |
245 |
245 Another reason is that we establish the reasoning infrastructure |
246 Another reason is that we establish the reasoning infrastructure |
246 for $\alpha$-\emph{equated} terms. In contrast, Ott produces a reasoning |
247 for $\alpha$-\emph{equated} terms. In contrast, Ott produces a reasoning |
247 infrastructure in Isabelle/HOL for |
248 infrastructure in Isabelle/HOL for |
248 \emph{non}-$\alpha$-equated, or ``raw'', terms. While our $\alpha$-equated terms |
249 \emph{non}-$\alpha$-equated, or ``raw'', terms. While our $\alpha$-equated terms |
259 only support specifications that make sense on the level of $\alpha$-equated |
260 only support specifications that make sense on the level of $\alpha$-equated |
260 terms (offending specifications, which for example bind a variable according |
261 terms (offending specifications, which for example bind a variable according |
261 to a variable bound somewhere else, are not excluded by Ott, but we have |
262 to a variable bound somewhere else, are not excluded by Ott, but we have |
262 to). |
263 to). |
263 |
264 |
264 Our insistence on reasoning with $\alpha$-equated terms comes from the |
265 %Our insistence on reasoning with $\alpha$-equated terms comes from the |
265 wealth of experience we gained with the older version of Nominal Isabelle: |
266 %wealth of experience we gained with the older version of Nominal Isabelle: |
266 for non-trivial properties, reasoning with $\alpha$-equated terms is much |
267 %for non-trivial properties, reasoning with $\alpha$-equated terms is much |
267 easier than reasoning with raw terms. The fundamental reason for this is |
268 %easier than reasoning with raw terms. The fundamental reason for this is |
268 that the HOL-logic underlying Nominal Isabelle allows us to replace |
269 %that the HOL-logic underlying Nominal Isabelle allows us to replace |
269 ``equals-by-equals''. In contrast, replacing |
270 %``equals-by-equals''. In contrast, replacing |
270 ``$\alpha$-equals-by-$\alpha$-equals'' in a representation based on raw terms |
271 %``$\alpha$-equals-by-$\alpha$-equals'' in a representation based on raw terms |
271 requires a lot of extra reasoning work. |
272 %requires a lot of extra reasoning work. |
272 |
273 |
273 Although in informal settings a reasoning infrastructure for $\alpha$-equated |
274 Although in informal settings a reasoning infrastructure for $\alpha$-equated |
274 terms is nearly always taken for granted, establishing it automatically in |
275 terms is nearly always taken for granted, establishing it automatically in |
275 the Isabelle/HOL is a rather non-trivial task. For every |
276 the Isabelle/HOL is a rather non-trivial task. For every |
276 specification we will need to construct a type containing as elements the |
277 specification we will need to construct a type containing as elements the |
347 \noindent |
348 \noindent |
348 (Note that this means also the term-constructors for variables, applications |
349 (Note that this means also the term-constructors for variables, applications |
349 and lambda are lifted to the quotient level.) This construction, of course, |
350 and lambda are lifted to the quotient level.) This construction, of course, |
350 only works if $\alpha$-equivalence is indeed an equivalence relation, and the |
351 only works if $\alpha$-equivalence is indeed an equivalence relation, and the |
351 ``raw'' definitions and theorems are respectful w.r.t.~$\alpha$-equivalence. |
352 ``raw'' definitions and theorems are respectful w.r.t.~$\alpha$-equivalence. |
352 For example, we will not be able to lift a bound-variable function. Although |
353 %For example, we will not be able to lift a bound-variable function. Although |
353 this function can be defined for raw terms, it does not respect |
354 %this function can be defined for raw terms, it does not respect |
354 $\alpha$-equivalence and therefore cannot be lifted. To sum up, every lifting |
355 %$\alpha$-equivalence and therefore cannot be lifted. |
356 To sum up, every lifting |
|
355 of theorems to the quotient level needs proofs of some respectfulness |
357 of theorems to the quotient level needs proofs of some respectfulness |
356 properties (see \cite{Homeier05}). In the paper we show that we are able to |
358 properties (see \cite{Homeier05}). In the paper we show that we are able to |
357 automate these proofs and as a result can automatically establish a reasoning |
359 automate these proofs and as a result can automatically establish a reasoning |
358 infrastructure for $\alpha$-equated terms.\smallskip |
360 infrastructure for $\alpha$-equated terms.\smallskip |
359 |
361 |
377 from the Ott-tool, but we introduce crucial restrictions, and also extensions, so |
379 from the Ott-tool, but we introduce crucial restrictions, and also extensions, so |
378 that our specifications make sense for reasoning about $\alpha$-equated terms. |
380 that our specifications make sense for reasoning about $\alpha$-equated terms. |
379 The main improvement over Ott is that we introduce three binding modes |
381 The main improvement over Ott is that we introduce three binding modes |
380 (only one is present in Ott), provide definitions for $\alpha$-equivalence and |
382 (only one is present in Ott), provide definitions for $\alpha$-equivalence and |
381 for free variables of our terms, and also derive a reasoning infrastructure |
383 for free variables of our terms, and also derive a reasoning infrastructure |
382 about our specifications inside Isabelle/HOL. |
384 for our specifications inside Isabelle/HOL. |
383 |
385 |
384 |
386 |
385 %\begin{figure} |
387 %\begin{figure} |
386 %\begin{boxedminipage}{\linewidth} |
388 %\begin{boxedminipage}{\linewidth} |
387 %%\begin{center} |
389 %%\begin{center} |
446 |
448 |
447 Permutations are bijective functions from atoms to atoms that are |
449 Permutations are bijective functions from atoms to atoms that are |
448 the identity everywhere except on a finite number of atoms. There is a |
450 the identity everywhere except on a finite number of atoms. There is a |
449 two-place permutation operation written |
451 two-place permutation operation written |
450 @{text "_ \<bullet> _ :: perm \<Rightarrow> \<beta> \<Rightarrow> \<beta>"} |
452 @{text "_ \<bullet> _ :: perm \<Rightarrow> \<beta> \<Rightarrow> \<beta>"} |
451 where the generic type @{text "\<beta>"} stands for the type of the object |
453 where the generic type @{text "\<beta>"} is the type of the object |
452 over which the permutation |
454 over which the permutation |
453 acts. In Nominal Isabelle, the identity permutation is written as @{term "0::perm"}, |
455 acts. In Nominal Isabelle, the identity permutation is written as @{term "0::perm"}, |
454 the composition of two permutations @{term p} and @{term q} as \mbox{@{term "p + q"}}, |
456 the composition of two permutations @{term p} and @{term q} as \mbox{@{term "p + q"}}, |
455 and the inverse permutation of @{term p} as @{text "- p"}. The permutation |
457 and the inverse permutation of @{term p} as @{text "- p"}. The permutation |
456 operation is defined over the type-hierarchy \cite{HuffmanUrban10}; |
458 operation is defined over the type-hierarchy \cite{HuffmanUrban10}; |
502 A striking consequence of these definitions is that we can prove |
504 A striking consequence of these definitions is that we can prove |
503 without knowing anything about the structure of @{term x} that |
505 without knowing anything about the structure of @{term x} that |
504 swapping two fresh atoms, say @{text a} and @{text b}, leaves |
506 swapping two fresh atoms, say @{text a} and @{text b}, leaves |
505 @{text x} unchanged: |
507 @{text x} unchanged: |
506 |
508 |
507 \begin{property}\label{swapfreshfresh} |
509 \begin{myproperty}\label{swapfreshfresh} |
508 @{thm[mode=IfThen] swap_fresh_fresh[no_vars]} |
510 @{thm[mode=IfThen] swap_fresh_fresh[no_vars]} |
509 \end{property} |
511 \end{myproperty} |
510 |
512 |
511 %While often the support of an object can be relatively easily |
513 %While often the support of an object can be relatively easily |
512 %described, for example for atoms, products, lists, function applications, |
514 %described, for example for atoms, products, lists, function applications, |
513 %booleans and permutations as follows |
515 %booleans and permutations as follows |
514 %% |
516 %% |
544 % |
546 % |
545 %\noindent |
547 %\noindent |
546 %The main point of @{text supports} is that we can establish the following |
548 %The main point of @{text supports} is that we can establish the following |
547 %two properties. |
549 %two properties. |
548 % |
550 % |
549 %\begin{property}\label{supportsprop} |
551 %\begin{myproperty}\label{supportsprop} |
550 %Given a set @{text "as"} of atoms. |
552 %Given a set @{text "as"} of atoms. |
551 %{\it (i)} @{thm[mode=IfThen] supp_is_subset[where S="as", no_vars]} |
553 %{\it (i)} @{thm[mode=IfThen] supp_is_subset[where S="as", no_vars]} |
552 %{\it (ii)} @{thm supp_supports[no_vars]}. |
554 %{\it (ii)} @{thm supp_supports[no_vars]}. |
553 %\end{property} |
555 %\end{myproperty} |
554 % |
556 % |
555 %Another important notion in the nominal logic work is \emph{equivariance}. |
557 %Another important notion in the nominal logic work is \emph{equivariance}. |
556 %For a function @{text f}, say of type @{text "\<alpha> \<Rightarrow> \<beta>"}, to be equivariant |
558 %For a function @{text f}, say of type @{text "\<alpha> \<Rightarrow> \<beta>"}, to be equivariant |
557 %it is required that every permutation leaves @{text f} unchanged, that is |
559 %it is required that every permutation leaves @{text f} unchanged, that is |
558 %% |
560 %% |
587 %Property~\ref{swapfreshfresh} |
589 %Property~\ref{swapfreshfresh} |
588 this property to rename single binders, it %%this property |
590 this property to rename single binders, it %%this property |
589 proved too unwieldy for dealing with multiple binders. For such binders the |
591 proved too unwieldy for dealing with multiple binders. For such binders the |
590 following generalisations turned out to be easier to use. |
592 following generalisations turned out to be easier to use. |
591 |
593 |
592 \begin{property}\label{supppermeq} |
594 \begin{myproperty}\label{supppermeq} |
593 @{thm[mode=IfThen] supp_perm_eq[no_vars]} |
595 @{thm[mode=IfThen] supp_perm_eq[no_vars]} |
594 \end{property} |
596 \end{myproperty} |
595 |
597 |
596 \begin{property}\label{avoiding} |
598 \begin{myproperty}\label{avoiding} |
597 For a finite set @{text as} and a finitely supported @{text x} with |
599 For a finite set @{text as} and a finitely supported @{text x} with |
598 @{term "as \<sharp>* x"} and also a finitely supported @{text c}, there |
600 @{term "as \<sharp>* x"} and also a finitely supported @{text c}, there |
599 exists a permutation @{text p} such that @{term "(p \<bullet> as) \<sharp>* c"} and |
601 exists a permutation @{text p} such that @{term "(p \<bullet> as) \<sharp>* c"} and |
600 @{term "supp x \<sharp>* p"}. |
602 @{term "supp x \<sharp>* p"}. |
601 \end{property} |
603 \end{myproperty} |
602 |
604 |
603 \noindent |
605 \noindent |
604 The idea behind the second property is that given a finite set @{text as} |
606 The idea behind the second property is that given a finite set @{text as} |
605 of binders (being bound, or fresh, in @{text x} is ensured by the |
607 of binders (being bound, or fresh, in @{text x} is ensured by the |
606 assumption @{term "as \<sharp>* x"}), then there exists a permutation @{text p} such that |
608 assumption @{term "as \<sharp>* x"}), then there exists a permutation @{text p} such that |
758 This lemma allows us to use our quotient package for introducing |
760 This lemma allows us to use our quotient package for introducing |
759 new types @{text "\<beta> abs_set"}, @{text "\<beta> abs_res"} and @{text "\<beta> abs_list"} |
761 new types @{text "\<beta> abs_set"}, @{text "\<beta> abs_res"} and @{text "\<beta> abs_list"} |
760 representing $\alpha$-equivalence classes of pairs of type |
762 representing $\alpha$-equivalence classes of pairs of type |
761 @{text "(atom set) \<times> \<beta>"} (in the first two cases) and of type @{text "(atom list) \<times> \<beta>"} |
763 @{text "(atom set) \<times> \<beta>"} (in the first two cases) and of type @{text "(atom list) \<times> \<beta>"} |
762 (in the third case). |
764 (in the third case). |
763 The elements in these types will be, respectively, written as: |
765 The elements in these types will be, respectively, written as |
764 |
766 % |
765 \begin{center} |
767 %\begin{center} |
766 @{term "Abs_set as x"} \hspace{5mm} |
768 @{term "Abs_set as x"}, %\hspace{5mm} |
767 @{term "Abs_res as x"} \hspace{5mm} |
769 @{term "Abs_res as x"} and %\hspace{5mm} |
768 @{term "Abs_lst as x"} |
770 @{term "Abs_lst as x"}, |
769 \end{center} |
771 %\end{center} |
770 |
772 % |
771 \noindent |
773 %\noindent |
772 indicating that a set (or list) of atoms @{text as} is abstracted in @{text x}. We will |
774 indicating that a set (or list) of atoms @{text as} is abstracted in @{text x}. We will |
773 call the types \emph{abstraction types} and their elements |
775 call the types \emph{abstraction types} and their elements |
774 \emph{abstractions}. The important property we need to derive is the support of |
776 \emph{abstractions}. The important property we need to derive is the support of |
775 abstractions, namely: |
777 abstractions, namely: |
776 |
778 |
873 |
875 |
874 section {* Specifying General Bindings\label{sec:spec} *} |
876 section {* Specifying General Bindings\label{sec:spec} *} |
875 |
877 |
876 text {* |
878 text {* |
877 Our choice of syntax for specifications is influenced by the existing |
879 Our choice of syntax for specifications is influenced by the existing |
878 datatype package of Isabelle/HOL \cite{Berghofer99} and by the syntax of the |
880 datatype package of Isabelle/HOL %\cite{Berghofer99} |
881 and by the syntax of the |
|
879 Ott-tool \cite{ott-jfp}. For us a specification of a term-calculus is a |
882 Ott-tool \cite{ott-jfp}. For us a specification of a term-calculus is a |
880 collection of (possibly mutual recursive) type declarations, say @{text |
883 collection of (possibly mutual recursive) type declarations, say @{text |
881 "ty\<AL>\<^isub>1, \<dots>, ty\<AL>\<^isub>n"}, and an associated collection of |
884 "ty\<AL>\<^isub>1, \<dots>, ty\<AL>\<^isub>n"}, and an associated collection of |
882 binding functions, say @{text "bn\<AL>\<^isub>1, \<dots>, bn\<AL>\<^isub>m"}. The |
885 binding functions, say @{text "bn\<AL>\<^isub>1, \<dots>, bn\<AL>\<^isub>m"}. The |
883 syntax in Nominal Isabelle for such specifications is roughly as follows: |
886 syntax in Nominal Isabelle for such specifications is roughly as follows: |
973 $\alpha$-equivalence where it is ensured that within a given scope an |
976 $\alpha$-equivalence where it is ensured that within a given scope an |
974 atom occurrence cannot be both bound and free at the same time. The first |
977 atom occurrence cannot be both bound and free at the same time. The first |
975 restriction is that a body can only occur in |
978 restriction is that a body can only occur in |
976 \emph{one} binding clause of a term constructor (this ensures that the bound |
979 \emph{one} binding clause of a term constructor (this ensures that the bound |
977 atoms of a body cannot be free at the same time by specifying an |
980 atoms of a body cannot be free at the same time by specifying an |
978 alternative binder for the same body). For binders we distinguish between |
981 alternative binder for the same body). |
982 |
|
983 For binders we distinguish between |
|
979 \emph{shallow} and \emph{deep} binders. Shallow binders are just |
984 \emph{shallow} and \emph{deep} binders. Shallow binders are just |
980 labels. The restriction we need to impose on them is that in case of |
985 labels. The restriction we need to impose on them is that in case of |
981 \isacommand{bind (set)} and \isacommand{bind (res)} the labels must either |
986 \isacommand{bind (set)} and \isacommand{bind (res)} the labels must either |
982 refer to atom types or to sets of atom types; in case of \isacommand{bind} |
987 refer to atom types or to sets of atom types; in case of \isacommand{bind} |
983 the labels must refer to atom types or lists of atom types. Two examples for |
988 the labels must refer to atom types or lists of atom types. Two examples for |
1106 |
1111 |
1107 \noindent |
1112 \noindent |
1108 Otherwise it is possible that @{text "bn\<^isub>1"} and @{text "bn\<^isub>2"} pick |
1113 Otherwise it is possible that @{text "bn\<^isub>1"} and @{text "bn\<^isub>2"} pick |
1109 out different atoms to become bound, respectively be free, in @{text "p"}. |
1114 out different atoms to become bound, respectively be free, in @{text "p"}. |
1110 (Since the Ott-tool does not derive a reasoning infrastructure for |
1115 (Since the Ott-tool does not derive a reasoning infrastructure for |
1111 $\alpha$-equated terms, it can permit such specifications.) |
1116 $\alpha$-equated terms with deep binders, it can permit such specifications.) |
1112 |
1117 |
1113 We also need to restrict the form of the binding functions in order |
1118 We also need to restrict the form of the binding functions in order |
1114 to ensure the @{text "bn"}-functions can be defined for $\alpha$-equated |
1119 to ensure the @{text "bn"}-functions can be defined for $\alpha$-equated |
1115 terms. The main restriction is that we cannot return an atom in a binding function that is also |
1120 terms. The main restriction is that we cannot return an atom in a binding function that is also |
1116 bound in the corresponding term-constructor. That means in \eqref{letpat} |
1121 bound in the corresponding term-constructor. That means in \eqref{letpat} |
1179 for the corresponding notion given on the ``raw'' level. So for example |
1184 for the corresponding notion given on the ``raw'' level. So for example |
1180 we have @{text "ty\<^sup>\<alpha> \<mapsto> ty"} and @{text "C\<^sup>\<alpha> \<mapsto> C"} |
1185 we have @{text "ty\<^sup>\<alpha> \<mapsto> ty"} and @{text "C\<^sup>\<alpha> \<mapsto> C"} |
1181 where @{term ty} is the type used in the quotient construction for |
1186 where @{term ty} is the type used in the quotient construction for |
1182 @{text "ty\<^sup>\<alpha>"} and @{text "C"} is the term-constructor on the ``raw'' type @{text "ty"}. |
1187 @{text "ty\<^sup>\<alpha>"} and @{text "C"} is the term-constructor on the ``raw'' type @{text "ty"}. |
1183 |
1188 |
1184 The resulting datatype definition is legal in Isabelle/HOL provided the datatypes are |
1189 %The resulting datatype definition is legal in Isabelle/HOL provided the datatypes are |
1185 non-empty and the types in the constructors only occur in positive |
1190 %non-empty and the types in the constructors only occur in positive |
1186 position (see \cite{Berghofer99} for an in-depth description of the datatype package |
1191 %position (see \cite{Berghofer99} for an in-depth description of the datatype package |
1187 in Isabelle/HOL). We subsequently define each of the user-specified binding |
1192 %in Isabelle/HOL). |
1193 We subsequently define each of the user-specified binding |
|
1188 functions @{term "bn"}$_{1..m}$ by recursion over the corresponding |
1194 functions @{term "bn"}$_{1..m}$ by recursion over the corresponding |
1189 raw datatype. We can also easily define permutation operations by |
1195 raw datatype. We can also easily define permutation operations by |
1190 recursion so that for each term constructor @{text "C"} we have that |
1196 recursion so that for each term constructor @{text "C"} we have that |
1191 % |
1197 % |
1192 \begin{equation}\label{ceqvt} |
1198 \begin{equation}\label{ceqvt} |
1672 holds under the assumptions that we have \mbox{@{text |
1678 holds under the assumptions that we have \mbox{@{text |
1673 "x\<^isub>i \<approx>ty\<^isub>i x\<PRIME>\<^isub>i"}} whenever @{text "x\<^isub>i"} |
1679 "x\<^isub>i \<approx>ty\<^isub>i x\<PRIME>\<^isub>i"}} whenever @{text "x\<^isub>i"} |
1674 and @{text "x\<PRIME>\<^isub>i"} are recursive arguments of @{text C} and |
1680 and @{text "x\<PRIME>\<^isub>i"} are recursive arguments of @{text C} and |
1675 @{text "x\<^isub>i = x\<PRIME>\<^isub>i"} whenever they are non-recursive arguments. We can prove this |
1681 @{text "x\<^isub>i = x\<PRIME>\<^isub>i"} whenever they are non-recursive arguments. We can prove this |
1676 implication by applying the corresponding rule in our $\alpha$-equivalence |
1682 implication by applying the corresponding rule in our $\alpha$-equivalence |
1677 definition and by establishing the following auxiliary facts |
1683 definition and by establishing the following auxiliary implications %facts |
1678 % |
1684 % |
1679 \begin{equation}\label{fnresp} |
1685 \begin{equation}\label{fnresp} |
1680 \mbox{% |
1686 \mbox{% |
1681 \begin{tabular}{l} |
1687 \begin{tabular}{ll@ {\hspace{7mm}}ll} |
1682 @{text "x \<approx>ty\<^isub>i x\<PRIME>"}~~implies~@{text "fa_ty\<^isub>i x = fa_ty\<^isub>i x\<PRIME>"}\\ |
1688 \mbox{\it (i)} & @{text "x \<approx>ty\<^isub>i x\<PRIME>"}~~@{text "\<Rightarrow>"}~~@{text "fa_ty\<^isub>i x = fa_ty\<^isub>i x\<PRIME>"} & |
1683 @{text "x \<approx>ty\<^isub>j x\<PRIME>"}~~implies~@{text "fa_bn\<^isub>j x = fa_bn\<^isub>j x\<PRIME>"}\\ |
1689 \mbox{\it (iii)} & @{text "x \<approx>ty\<^isub>j x\<PRIME>"}~~@{text "\<Rightarrow>"}~~@{text "bn\<^isub>j x = bn\<^isub>j x\<PRIME>"}\\ |
1684 @{text "x \<approx>ty\<^isub>j x\<PRIME>"}~~implies~@{text "bn\<^isub>j x = bn\<^isub>j x\<PRIME>"}\\ |
1690 |
1685 @{text "x \<approx>ty\<^isub>j x\<PRIME>"}~~implies~@{text "x \<approx>bn\<^isub>j x\<PRIME>"}\\ |
1691 \mbox{\it (ii)} & @{text "x \<approx>ty\<^isub>j x\<PRIME>"}~~@{text "\<Rightarrow>"}~~@{text "fa_bn\<^isub>j x = fa_bn\<^isub>j x\<PRIME>"} & |
1692 \mbox{\it (iv)} & @{text "x \<approx>ty\<^isub>j x\<PRIME>"}~~@{text "\<Rightarrow>"}~~@{text "x \<approx>bn\<^isub>j x\<PRIME>"}\\ |
|
1686 \end{tabular}} |
1693 \end{tabular}} |
1687 \end{equation} |
1694 \end{equation} |
1688 |
1695 |
1689 \noindent |
1696 \noindent |
1690 They can be established by induction on @{text "\<approx>ty"}$_{1..n}$. Whereas the first, |
1697 They can be established by induction on @{text "\<approx>ty"}$_{1..n}$. Whereas the first, |
1708 |
1715 |
1709 \noindent |
1716 \noindent |
1710 are $\alpha$-equivalent. This gives us conditions when the corresponding |
1717 are $\alpha$-equivalent. This gives us conditions when the corresponding |
1711 $\alpha$-equated terms are \emph{equal}, namely |
1718 $\alpha$-equated terms are \emph{equal}, namely |
1712 % |
1719 % |
1713 \begin{center} |
1720 %\begin{center} |
1714 @{text "C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r = C\<^sup>\<alpha> x\<PRIME>\<^isub>1 \<dots> x\<PRIME>\<^isub>r"} |
1721 @{text "C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r = C\<^sup>\<alpha> x\<PRIME>\<^isub>1 \<dots> x\<PRIME>\<^isub>r"}. |
1715 \end{center} |
1722 %\end{center} |
1716 |
1723 % |
1717 \noindent |
1724 %\noindent |
1718 We call these conditions as \emph{quasi-injectivity}. They correspond to |
1725 We call these conditions as \emph{quasi-injectivity}. They correspond to |
1719 the premises in our $\alpha$-equivalence relations. |
1726 the premises in our $\alpha$-equivalence relations. |
1720 |
1727 |
1721 Next we can lift the permutation |
1728 Next we can lift the permutation |
1722 operations defined in \eqref{ceqvt}. In order to make this |
1729 operations defined in \eqref{ceqvt}. In order to make this |
1742 Finally we can add to our infrastructure a cases lemma (explained in the next section) |
1749 Finally we can add to our infrastructure a cases lemma (explained in the next section) |
1743 and a structural induction principle |
1750 and a structural induction principle |
1744 for the types @{text "ty\<AL>"}$_{i..n}$. The conclusion of the induction principle is |
1751 for the types @{text "ty\<AL>"}$_{i..n}$. The conclusion of the induction principle is |
1745 of the form |
1752 of the form |
1746 % |
1753 % |
1747 \begin{equation}\label{weakinduct} |
1754 %\begin{equation}\label{weakinduct} |
1748 \mbox{@{text "P\<^isub>1 x\<^isub>1 \<and> \<dots> \<and> P\<^isub>n x\<^isub>n "}} |
1755 \mbox{@{text "P\<^isub>1 x\<^isub>1 \<and> \<dots> \<and> P\<^isub>n x\<^isub>n "}} |
1749 \end{equation} |
1756 %\end{equation} |
1750 |
1757 % |
1751 \noindent |
1758 %\noindent |
1752 whereby the @{text P}$_{1..n}$ are predicates and the @{text x}$_{1..n}$ |
1759 whereby the @{text P}$_{1..n}$ are predicates and the @{text x}$_{1..n}$ |
1753 have types @{text "ty\<AL>"}$_{1..n}$. This induction principle has for each |
1760 have types @{text "ty\<AL>"}$_{1..n}$. This induction principle has for each |
1754 term constructor @{text "C"}$^\alpha$ a premise of the form |
1761 term constructor @{text "C"}$^\alpha$ a premise of the form |
1755 % |
1762 % |
1756 \begin{equation}\label{weakprem} |
1763 \begin{equation}\label{weakprem} |
1764 By working now completely on the $\alpha$-equated level, we |
1771 By working now completely on the $\alpha$-equated level, we |
1765 can first show that the free-atom functions and binding functions are |
1772 can first show that the free-atom functions and binding functions are |
1766 equivariant, namely |
1773 equivariant, namely |
1767 % |
1774 % |
1768 \begin{center} |
1775 \begin{center} |
1769 \begin{tabular}{rcl} |
1776 \begin{tabular}{rcl@ {\hspace{10mm}}rcl} |
1770 @{text "p \<bullet> (fa_ty\<AL>\<^isub>i x)"} & $=$ & @{text "fa_ty\<AL>\<^isub>i (p \<bullet> x)"}\\ |
1777 @{text "p \<bullet> (fa_ty\<AL>\<^isub>i x)"} & $=$ & @{text "fa_ty\<AL>\<^isub>i (p \<bullet> x)"} & |
1778 @{text "p \<bullet> (bn\<AL>\<^isub>j x)"} & $=$ & @{text "bn\<AL>\<^isub>j (p \<bullet> x)"}\\ |
|
1771 @{text "p \<bullet> (fa_bn\<AL>\<^isub>j x)"} & $=$ & @{text "fa_bn\<AL>\<^isub>j (p \<bullet> x)"}\\ |
1779 @{text "p \<bullet> (fa_bn\<AL>\<^isub>j x)"} & $=$ & @{text "fa_bn\<AL>\<^isub>j (p \<bullet> x)"}\\ |
1772 @{text "p \<bullet> (bn\<AL>\<^isub>j x)"} & $=$ & @{text "bn\<AL>\<^isub>j (p \<bullet> x)"} |
|
1773 \end{tabular} |
1780 \end{tabular} |
1774 \end{center} |
1781 \end{center} |
1775 |
1782 % |
1776 \noindent |
1783 \noindent |
1777 These properties can be established using the induction principle |
1784 These properties can be established using the induction principle. |
1778 in \eqref{weakinduct}. |
1785 %%in \eqref{weakinduct}. |
1779 Having these equivariant properties established, we can |
1786 Having these equivariant properties established, we can |
1780 show for every term-constructor @{text "C\<^sup>\<alpha>"} that |
1787 show that the support of term-constructors @{text "C\<^sup>\<alpha>"} is included in |
1781 |
1788 the support of its arguments, that means |
1782 \begin{center} |
1789 |
1783 @{text "(supp x\<^isub>1 \<union> \<dots> \<union> supp x\<^isub>r) supports (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r)"} |
1790 \begin{center} |
1791 @{text "supp (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r) \<subseteq> (supp x\<^isub>1 \<union> \<dots> \<union> supp x\<^isub>r)"} |
|
1784 \end{center} |
1792 \end{center} |
1785 |
1793 |
1786 \noindent |
1794 \noindent |
1787 holds. This together with Property~\ref{supportsprop} allows us to prove |
1795 holds. This allows us to prove by induction that |
1788 that every @{text x} of type @{text "ty\<AL>"}$_{1..n}$ is finitely supported, |
1796 every @{text x} of type @{text "ty\<AL>"}$_{1..n}$ is finitely supported. |
1789 namely @{text "finite (supp x)"}. This can be again shown by induction |
1797 %This can be again shown by induction |
1790 over @{text "ty\<AL>"}$_{1..n}$. Lastly, we can show that the support of |
1798 %over @{text "ty\<AL>"}$_{1..n}$. |
1799 Lastly, we can show that the support of |
|
1791 elements in @{text "ty\<AL>"}$_{1..n}$ is the same as @{text "fa_ty\<AL>"}$_{1..n}$. |
1800 elements in @{text "ty\<AL>"}$_{1..n}$ is the same as @{text "fa_ty\<AL>"}$_{1..n}$. |
1792 This fact is important in a nominal setting, but also provides evidence |
1801 This fact is important in a nominal setting, but also provides evidence |
1793 that our notions of free-atoms and $\alpha$-equivalence are correct. |
1802 that our notions of free-atoms and $\alpha$-equivalence are correct. |
1794 |
1803 |
1795 \begin{lemma} |
1804 \begin{theorem} |
1796 For every @{text "x"} of type @{text "ty\<AL>"}$_{1..n}$, we have |
1805 For @{text "x"}$_{1..n}$ with type @{text "ty\<AL>"}$_{1..n}$, we have |
1797 @{text "supp x = fa_ty\<AL>\<^isub>i x"}. |
1806 @{text "supp x\<^isub>i = fa_ty\<AL>\<^isub>i x\<^isub>i"}. |
1798 \end{lemma} |
1807 \end{theorem} |
1799 |
1808 |
1800 \begin{proof} |
1809 \begin{proof} |
1801 The proof is by induction. In each case |
1810 The proof is by induction. In each case |
1802 we unfold the definition of @{text "supp"}, move the swapping inside the |
1811 we unfold the definition of @{text "supp"}, move the swapping inside the |
1803 term-constructors and then use the quasi-injectivity lemmas in order to complete the |
1812 term-constructors and then use the quasi-injectivity lemmas in order to complete the |
1886 |
1895 |
1887 |
1896 |
1888 section {* Strong Induction Principles *} |
1897 section {* Strong Induction Principles *} |
1889 |
1898 |
1890 text {* |
1899 text {* |
1891 In the previous section we were able to provide induction principles that |
1900 In the previous section we derived induction principles for $\alpha$-equated terms. |
1892 allow us to perform structural inductions over $\alpha$-equated terms. |
1901 We call such induction principles \emph{weak}, because for a |
1893 We call such induction principles \emph{weak}, because in case of the |
1902 term-constructor \mbox{@{text "C\<^sup>\<alpha> x\<^isub>1\<dots>x\<^isub>r"}} |
1894 term-constructor @{text "C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r"}, |
|
1895 the induction hypothesis requires us to establish the implications \eqref{weakprem}. |
1903 the induction hypothesis requires us to establish the implications \eqref{weakprem}. |
1896 The problem with these implications is that in general they are difficult to establish. |
1904 The problem with these implications is that in general they are difficult to establish. |
1897 The reason is that we cannot make any assumption about the binders that might be in @{text "C\<^sup>\<alpha>"} |
1905 The reason is that we cannot make any assumption about the binders that might be in @{text "C\<^sup>\<alpha>"}. |
1898 (for example we cannot assume the variable convention for them). |
1906 %%(for example we cannot assume the variable convention for them). |
1899 |
1907 |
1900 In \cite{UrbanTasson05} we introduced a method for automatically |
1908 In \cite{UrbanTasson05} we introduced a method for automatically |
1901 strengthening weak induction principles for terms containing single |
1909 strengthening weak induction principles for terms containing single |
1902 binders. These stronger induction principles allow the user to make additional |
1910 binders. These stronger induction principles allow the user to make additional |
1903 assumptions about binders. |
1911 assumptions about binders. |
1904 These additional assumptions amount to a formal |
1912 %These additional assumptions amount to a formal |
1905 version of the informal variable convention for binders. A natural question is |
1913 %version of the informal variable convention for binders. |
1906 whether we can also strengthen the weak induction principles involving |
1914 To sketch how this strengthening extends to the case of multiple binders, we use as |
1907 the general binders presented here. We will indeed be able to so, but for this we need an |
1915 running example the term-constructors @{text "Lam"} and @{text "Let"} |
1908 additional notion for permuting deep binders. |
1916 from example \eqref{letpat}. Instead of establishing @{text " P\<^bsub>trm\<^esub> t \<and> P\<^bsub>pat\<^esub> p"}, |
1909 |
1917 the stronger induction principles establish properties @{text " P\<^bsub>trm\<^esub> c t \<and> P\<^bsub>pat\<^esub> c p"} |
1910 Given a binding function @{text "bn"} we define an auxiliary permutation |
1918 where the additional parameter @{text c} controls |
1911 operation @{text "_ \<bullet>\<^bsub>bn\<^esub> _"} which permutes only bound arguments in a deep binder. |
1919 which freshness assumptions the binders should satisfy. For the two term constructors |
1912 Assuming a clause of @{text bn} is given as |
1920 this means that the user has to establish in inductions the implications |
1913 % |
1921 % |
1914 \begin{center} |
1922 \begin{center} |
1915 @{text "bn (C x\<^isub>1 \<dots> x\<^isub>r) = rhs"}, |
1923 \begin{tabular}{l} |
1916 \end{center} |
1924 @{text "\<forall>a t c. {atom a} \<FRESH>\<^sup>* c \<and> (\<forall>d. P\<^bsub>trm\<^esub> d t) \<Rightarrow> P\<^bsub>trm\<^esub> c (Lam a t)"}\\ |
1917 |
1925 @{text "\<forall>p t c. (set (bn p)) \<FRESH>\<^sup>* c \<and> (\<forall>d. P\<^bsub>pat\<^esub> d p) \<and> (\<forall>d. P\<^bsub>trm\<^esub> d t) \<and> \<Rightarrow> P\<^bsub>trm\<^esub> c (Let p t)"} |
1918 \noindent |
1926 \end{tabular} |
1919 then we define |
1927 \end{center} |
1928 |
|
1929 In \cite{UrbanTasson05} we showed how the weaker induction principles imply |
|
1930 the stronger ones. This was done by some quite complicated, nevertheless automated, |
|
1931 induction proofs. In this paper we simplify this work by leveraging the automated proof |
|
1932 methods from the function package of Isabelle/HOL generates. |
|
1933 |
|
1934 The reasoning principle we employ here is well-founded induction. For this we have to discharge |
|
1935 two proof obligations: one is that we have |
|
1936 well-founded measures (for each type @{text "ty"}$^\alpha_{1..n}$) that decrease in |
|
1937 every induction step and the other is that we have covered all cases. |
|
1938 As measures we use are the size functions |
|
1939 @{text "size_ty"}$^\alpha_{1..n}$, which we lifted in the previous section and which are |
|
1940 all well-founded. It is straightforward to establish that these measures decrease |
|
1941 in every induction step. |
|
1942 |
|
1943 What is left to show is that we covered all cases. To do so, we use |
|
1944 a cases lemma derived for each type, which for the terms in \eqref{letpat} |
|
1945 is of the form |
|
1946 % |
|
1947 \begin{equation}\label{weakcases} |
|
1948 \infer{@{text "P\<^bsub>trm\<^esub>"}} |
|
1949 {\begin{array}{l@ {\hspace{9mm}}l} |
|
1950 @{text "\<forall>x. t = Var x \<Rightarrow> P\<^bsub>trm\<^esub>"} & @{text "\<forall>a t'. t = Lam a t' \<Rightarrow> P\<^bsub>trm\<^esub>"}\\ |
|
1951 @{text "\<forall>t\<^isub>1 t\<^isub>2. t = App t\<^isub>1 t\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub>"} & @{text "\<forall>p t'. t = Let p t' \<Rightarrow> P\<^bsub>trm\<^esub>"}\\ |
|
1952 \end{array}} |
|
1953 \end{equation} |
|
1954 % |
|
1955 These cases lemmas have a premise for auch term-constructor. |
|
1956 The idea behind them is that we can conclude with a property @{text "P\<^bsub>trm\<^esub>"}, |
|
1957 provided we can show that this property holds if we substitute for @{text "t"} all |
|
1958 possible term-constructors. |
|
1959 |
|
1960 The only remaining difficulty is that in order to derive the stronger induction |
|
1961 principles conveniently, the cases lemma in \eqref{weakcases} is too weak. For this note that |
|
1962 in order to apply this lemma, we have to establish @{text "P\<^bsub>trm\<^esub>"} for \emph{all} @{text Lam}- and |
|
1963 \emph{all} @{text Let}-terms. |
|
1964 What we need instead is a cases rule where we only have to consider terms that have |
|
1965 binders being fresh w.r.t.~a context @{text "c"}, namely |
|
1966 % |
|
1967 \begin{center} |
|
1968 \begin{tabular}{l} |
|
1969 @{text "\<forall>a t'. t = Lam a t' \<and> {atom a} \<FRESH>\<^sup>* c \<Rightarrow> P\<^bsub>trm\<^esub>"}\\ |
|
1970 @{text "\<forall>p t'. t = Let p t' \<and> (set (bn p)) \<FRESH>\<^sup>* c \<Rightarrow> P\<^bsub>trm\<^esub>"} |
|
1971 \end{tabular} |
|
1972 \end{center} |
|
1973 % |
|
1974 However, this can be relatively easily be derived from the implications in \eqref{weakcases} |
|
1975 by a renaming using Properties \ref{supppermeq} and \ref{avoiding}. In the first case we know |
|
1976 that @{text "{atom a} \<FRESH>\<^sup>* Lam a t"}. Property \eqref{avoiding} provides us therefore with |
|
1977 a permutation @{text q}, such that @{text "{atom (q \<bullet> a)} \<FRESH>\<^sup>* c"} and |
|
1978 @{text "supp (Lam a t) \<FRESH>\<^sup>* q"} hold. |
|
1979 By using Property \ref{supppermeq}, we can infer that @{text "Lam (q \<bullet> a) (q \<bullet> t) = Lam a t"} |
|
1980 and we are done with this case. |
|
1981 |
|
1982 The @{text Let}-case involving a (non-recursive) deep binder is a bit more complicated. |
|
1983 The reason is that the we cannot apply Property \ref{avoiding} to the whole term @{text "Let p t"}, |
|
1984 because @{text p} might contain names that are bound (by @{text bn}) and that are |
|
1985 free. To solve this problem we have to introduce a permutation functions that only |
|
1986 permutes names bound by @{text bn} and leaves the other names unchanged. We do this again |
|
1987 by lifting. Assuming a |
|
1988 clause @{text "bn (C x\<^isub>1 \<dots> x\<^isub>r) = rhs"}, we define |
|
1920 % |
1989 % |
1921 \begin{center} |
1990 \begin{center} |
1922 @{text "p \<bullet>\<^bsub>bn\<^esub> (C x\<^isub>1 \<dots> x\<^isub>r) \<equiv> C y\<^isub>1 \<dots> y\<^isub>r"} |
1991 @{text "p \<bullet>\<^bsub>bn\<^esub> (C x\<^isub>1 \<dots> x\<^isub>r) \<equiv> C y\<^isub>1 \<dots> y\<^isub>r"} |
1923 \end{center} |
1992 \end{center} |
1924 |
1993 % |
1925 \noindent |
1994 \noindent |
1926 with @{text "y\<^isub>i"} determined as follows: |
1995 with @{text "y\<^isub>i"} determined as follows: |
1927 % |
1996 % |
1928 \begin{center} |
1997 \begin{center} |
1929 \begin{tabular}{c@ {\hspace{2mm}}p{7cm}} |
1998 \begin{tabular}{c@ {\hspace{2mm}}p{0.9\textwidth}} |
1930 $\bullet$ & @{text "y\<^isub>i \<equiv> x\<^isub>i"} provided @{text "x\<^isub>i"} does not occur in @{text "rhs"}\\ |
1999 $\bullet$ & @{text "y\<^isub>i \<equiv> x\<^isub>i"} provided @{text "x\<^isub>i"} does not occur in @{text "rhs"}\\ |
1931 $\bullet$ & @{text "y\<^isub>i \<equiv> p \<bullet>\<^bsub>bn'\<^esub> x\<^isub>i"} provided @{text "bn' x\<^isub>i"} is in @{text "rhs"}\\ |
2000 $\bullet$ & @{text "y\<^isub>i \<equiv> p \<bullet>\<^bsub>bn'\<^esub> x\<^isub>i"} provided @{text "bn' x\<^isub>i"} is in @{text "rhs"}\\ |
1932 $\bullet$ & @{text "y\<^isub>i \<equiv> p \<bullet> x\<^isub>i"} otherwise |
2001 $\bullet$ & @{text "y\<^isub>i \<equiv> p \<bullet> x\<^isub>i"} otherwise |
1933 \end{tabular} |
2002 \end{tabular} |
1934 \end{center} |
2003 \end{center} |
2004 % |
|
2005 Now Properties \ref{supppermeq} and \ref{avoiding} give us a permutation @{text q} such that |
|
2006 @{text "(set (bn (q \<bullet>\<^bsub>bn\<^esub> p)) \<FRESH>\<^sup>* c"} holds and such that @{text "[q \<bullet>\<^bsub>bn\<^esub> p]\<^bsub>list\<^esub>.(q \<bullet> t)"} |
|
2007 is equal to @{text "[p]\<^bsub>list\<^esub>. t"}. We can also show that @{text "(q \<bullet>\<^bsub>bn\<^esub> p) \<approx>\<^bsub>bn\<^esub> p"}. But |
|
2008 these facts establish that @{text "Let (q \<bullet>\<^bsub>bn\<^esub> p) (p \<bullet> t) = Let p t"}, as we need. This |
|
2009 completes the interesting cases in \eqref{letpat} for stregthening the induction |
|
2010 principles. |
|
1935 |
2011 |
1936 \noindent |
2012 |
1937 Using again the quotient package we can lift the @{text "_ \<bullet>\<^bsub>bn\<^esub> _"} function to |
2013 |
1938 $\alpha$-equated terms. We can then prove the following two facts |
2014 %A natural question is |
1939 |
2015 %whether we can also strengthen the weak induction principles involving |
1940 \begin{lemma}\label{permutebn} |
2016 %the general binders presented here. We will indeed be able to so, but for this we need an |
1941 Given a binding function @{text "bn\<^sup>\<alpha>"} then for all @{text p} |
2017 %additional notion for permuting deep binders. |
1942 {\it (i)} @{text "p \<bullet> (bn\<^sup>\<alpha> x) = bn\<^sup>\<alpha> (p \<bullet>\<AL>\<^bsub>bn\<^esub> x)"} and {\it (ii)} |
2018 |
1943 @{text "fa_bn\<^isup>\<alpha> x = fa_bn\<^isup>\<alpha> (p \<bullet>\<AL>\<^bsub>bn\<^esub> x)"}. |
2019 %Given a binding function @{text "bn"} we define an auxiliary permutation |
1944 \end{lemma} |
2020 %operation @{text "_ \<bullet>\<^bsub>bn\<^esub> _"} which permutes only bound arguments in a deep binder. |
1945 |
2021 %Assuming a clause of @{text bn} is given as |
1946 \begin{proof} |
2022 % |
1947 By induction on @{text x}. The equations follow by simple unfolding |
2023 %\begin{center} |
1948 of the definitions. |
2024 %@{text "bn (C x\<^isub>1 \<dots> x\<^isub>r) = rhs"}, |
1949 \end{proof} |
2025 %\end{center} |
1950 |
2026 |
1951 \noindent |
2027 %\noindent |
1952 The first property states that a permutation applied to a binding function is |
2028 %then we define |
1953 equivalent to first permuting the binders and then calculating the bound |
2029 % |
1954 atoms. The second amounts to the fact that permuting the binders has no |
2030 %\begin{center} |
1955 effect on the free-atom function. The main point of this permutation |
2031 %@{text "p \<bullet>\<^bsub>bn\<^esub> (C x\<^isub>1 \<dots> x\<^isub>r) \<equiv> C y\<^isub>1 \<dots> y\<^isub>r"} |
1956 function, however, is that if we have a permutation that is fresh |
2032 %\end{center} |
1957 for the support of an object @{text x}, then we can use this permutation |
2033 |
1958 to rename the binders in @{text x}, without ``changing'' @{text x}. In case of the |
2034 %\noindent |
1959 @{text "Let"} term-constructor from the example shown |
2035 %with @{text "y\<^isub>i"} determined as follows: |
1960 in \eqref{letpat} this means for a permutation @{text "r"} |
2036 % |
1961 % |
2037 %\begin{center} |
1962 \begin{equation}\label{renaming} |
2038 %\begin{tabular}{c@ {\hspace{2mm}}p{7cm}} |
1963 \begin{array}{l} |
2039 %$\bullet$ & @{text "y\<^isub>i \<equiv> x\<^isub>i"} provided @{text "x\<^isub>i"} does not occur in @{text "rhs"}\\ |
1964 \mbox{if @{term "supp (Abs_lst (bn p) t\<^isub>2) \<sharp>* r"}}\\ |
2040 %$\bullet$ & @{text "y\<^isub>i \<equiv> p \<bullet>\<^bsub>bn'\<^esub> x\<^isub>i"} provided @{text "bn' x\<^isub>i"} is in @{text "rhs"}\\ |
1965 \qquad\mbox{then @{text "Let p t\<^isub>1 t\<^isub>2 = Let (r \<bullet>\<AL>\<^bsub>bn_pat\<^esub> p) t\<^isub>1 (r \<bullet> t\<^isub>2)"}} |
2041 %$\bullet$ & @{text "y\<^isub>i \<equiv> p \<bullet> x\<^isub>i"} otherwise |
1966 \end{array} |
2042 %\end{tabular} |
1967 \end{equation} |
2043 %\end{center} |
1968 |
2044 |
1969 \noindent |
2045 %\noindent |
1970 This fact will be crucial when establishing the strong induction principles below. |
2046 %Using again the quotient package we can lift the @{text "_ \<bullet>\<^bsub>bn\<^esub> _"} function to |
2047 %$\alpha$-equated terms. We can then prove the following two facts |
|
2048 |
|
2049 %\begin{lemma}\label{permutebn} |
|
2050 %Given a binding function @{text "bn\<^sup>\<alpha>"} then for all @{text p} |
|
2051 %{\it (i)} @{text "p \<bullet> (bn\<^sup>\<alpha> x) = bn\<^sup>\<alpha> (p \<bullet>\<AL>\<^bsub>bn\<^esub> x)"} and {\it (ii)} |
|
2052 % @{text "fa_bn\<^isup>\<alpha> x = fa_bn\<^isup>\<alpha> (p \<bullet>\<AL>\<^bsub>bn\<^esub> x)"}. |
|
2053 %\end{lemma} |
|
2054 |
|
2055 %\begin{proof} |
|
2056 %By induction on @{text x}. The equations follow by simple unfolding |
|
2057 %of the definitions. |
|
2058 %\end{proof} |
|
2059 |
|
2060 %\noindent |
|
2061 %The first property states that a permutation applied to a binding function is |
|
2062 %equivalent to first permuting the binders and then calculating the bound |
|
2063 %atoms. The second amounts to the fact that permuting the binders has no |
|
2064 %effect on the free-atom function. The main point of this permutation |
|
2065 %function, however, is that if we have a permutation that is fresh |
|
2066 %for the support of an object @{text x}, then we can use this permutation |
|
2067 %to rename the binders in @{text x}, without ``changing'' @{text x}. In case of the |
|
2068 %@{text "Let"} term-constructor from the example shown |
|
2069 %in \eqref{letpat} this means for a permutation @{text "r"} |
|
2070 %% |
|
2071 %\begin{equation}\label{renaming} |
|
2072 %\begin{array}{l} |
|
2073 %\mbox{if @{term "supp (Abs_lst (bn p) t\<^isub>2) \<sharp>* r"}}\\ |
|
2074 %\qquad\mbox{then @{text "Let p t\<^isub>1 t\<^isub>2 = Let (r \<bullet>\<AL>\<^bsub>bn_pat\<^esub> p) t\<^isub>1 (r \<bullet> t\<^isub>2)"}} |
|
2075 %\end{array} |
|
2076 %\end{equation} |
|
2077 |
|
2078 %\noindent |
|
2079 %This fact will be crucial when establishing the strong induction principles below. |
|
1971 |
2080 |
1972 |
2081 |
1973 In our running example about @{text "Let"}, the strong induction |
2082 %In our running example about @{text "Let"}, the strong induction |
1974 principle means that instead |
2083 %principle means that instead |
1975 of establishing the implication |
2084 %of establishing the implication |
1976 % |
2085 % |
1977 \begin{center} |
2086 %\begin{center} |
1978 @{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)"} |
2087 %@{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)"} |
1979 \end{center} |
2088 %\end{center} |
1980 |
2089 % |
1981 \noindent |
2090 %\noindent |
1982 it is sufficient to establish the following implication |
2091 %it is sufficient to establish the following implication |
1983 % |
2092 % |
1984 \begin{equation}\label{strong} |
2093 %\begin{equation}\label{strong} |
1985 \mbox{\begin{tabular}{l} |
2094 %\mbox{\begin{tabular}{l} |
1986 @{text "\<forall>p t\<^isub>1 t\<^isub>2 c."}\\ |
2095 %@{text "\<forall>p t\<^isub>1 t\<^isub>2 c."}\\ |
1987 \hspace{5mm}@{text "set (bn p) #\<^sup>* c \<and>"}\\ |
2096 %\hspace{5mm}@{text "set (bn p) #\<^sup>* c \<and>"}\\ |
1988 \hspace{5mm}@{text "(\<forall>d. P\<^bsub>pat\<^esub> d p) \<and> (\<forall>d. P\<^bsub>trm\<^esub> d t\<^isub>1) \<and> (\<forall>d. P\<^bsub>trm\<^esub> d t\<^isub>2)"}\\ |
2097 %\hspace{5mm}@{text "(\<forall>d. P\<^bsub>pat\<^esub> d p) \<and> (\<forall>d. P\<^bsub>trm\<^esub> d t\<^isub>1) \<and> (\<forall>d. P\<^bsub>trm\<^esub> d t\<^isub>2)"}\\ |
1989 \hspace{15mm}@{text "\<Rightarrow> P\<^bsub>trm\<^esub> c (Let p t\<^isub>1 t\<^isub>2)"} |
2098 %\hspace{15mm}@{text "\<Rightarrow> P\<^bsub>trm\<^esub> c (Let p t\<^isub>1 t\<^isub>2)"} |
1990 \end{tabular}} |
2099 %\end{tabular}} |
1991 \end{equation} |
2100 %\end{equation} |
1992 |
2101 % |
1993 \noindent |
2102 %\noindent |
1994 While this implication contains an additional argument, namely @{text c}, and |
2103 %While this implication contains an additional argument, namely @{text c}, and |
1995 also additional universal quantifications, it is usually easier to establish. |
2104 %also additional universal quantifications, it is usually easier to establish. |
1996 The reason is that we have the freshness |
2105 %The reason is that we have the freshness |
1997 assumption @{text "set (bn\<^sup>\<alpha> p) #\<^sup>* c"}, whereby @{text c} can be arbitrarily |
2106 %assumption @{text "set (bn\<^sup>\<alpha> p) #\<^sup>* c"}, whereby @{text c} can be arbitrarily |
1998 chosen by the user as long as it has finite support. |
2107 %chosen by the user as long as it has finite support. |
1999 |
2108 % |
2000 Let us now show how we derive the strong induction principles from the |
2109 %Let us now show how we derive the strong induction principles from the |
2001 weak ones. In case of the @{text "Let"}-example we derive by the weak |
2110 %weak ones. In case of the @{text "Let"}-example we derive by the weak |
2002 induction the following two properties |
2111 %induction the following two properties |
2003 % |
2112 % |
2004 \begin{equation}\label{hyps} |
2113 %\begin{equation}\label{hyps} |
2005 @{text "\<forall>q c. P\<^bsub>trm\<^esub> c (q \<bullet> t)"} \hspace{4mm} |
2114 %@{text "\<forall>q c. P\<^bsub>trm\<^esub> c (q \<bullet> t)"} \hspace{4mm} |
2006 @{text "\<forall>q\<^isub>1 q\<^isub>2 c. P\<^bsub>pat\<^esub> (q\<^isub>1 \<bullet>\<AL>\<^bsub>bn\<^esub> (q\<^isub>2 \<bullet> p))"} |
2115 %@{text "\<forall>q\<^isub>1 q\<^isub>2 c. P\<^bsub>pat\<^esub> (q\<^isub>1 \<bullet>\<AL>\<^bsub>bn\<^esub> (q\<^isub>2 \<bullet> p))"} |
2007 \end{equation} |
2116 %\end{equation} |
2008 |
2117 % |
2009 \noindent |
2118 %\noindent |
2010 For the @{text Let} term-constructor we therefore have to establish @{text "P\<^bsub>trm\<^esub> c (q \<bullet> Let p t\<^isub>1 t\<^isub>2)"} |
2119 %For the @{text Let} term-constructor we therefore have to establish @{text "P\<^bsub>trm\<^esub> c (q \<bullet> Let p t\<^isub>1 t\<^isub>2)"} |
2011 assuming \eqref{hyps} as induction hypotheses (the first for @{text t\<^isub>1} and @{text t\<^isub>2}). |
2120 %assuming \eqref{hyps} as induction hypotheses (the first for @{text t\<^isub>1} and @{text t\<^isub>2}). |
2012 By Property~\ref{avoiding} we |
2121 %By Property~\ref{avoiding} we |
2013 obtain a permutation @{text "r"} such that |
2122 %obtain a permutation @{text "r"} such that |
2014 % |
2123 % |
2015 \begin{equation}\label{rprops} |
2124 %\begin{equation}\label{rprops} |
2016 @{term "(r \<bullet> set (bn (q \<bullet> p))) \<sharp>* c "}\hspace{4mm} |
2125 %@{term "(r \<bullet> set (bn (q \<bullet> p))) \<sharp>* c "}\hspace{4mm} |
2017 @{term "supp (Abs_lst (bn (q \<bullet> p)) (q \<bullet> t\<^isub>2)) \<sharp>* r"} |
2126 %@{term "supp (Abs_lst (bn (q \<bullet> p)) (q \<bullet> t\<^isub>2)) \<sharp>* r"} |
2018 \end{equation} |
2127 %\end{equation} |
2019 |
2128 % |
2020 \noindent |
2129 %\noindent |
2021 hold. The latter fact and \eqref{renaming} give us |
2130 %hold. The latter fact and \eqref{renaming} give us |
2022 % |
2131 %% |
2023 \begin{center} |
2132 %\begin{center} |
2024 \begin{tabular}{l} |
2133 %\begin{tabular}{l} |
2025 @{text "Let (q \<bullet> p) (q \<bullet> t\<^isub>1) (q \<bullet> t\<^isub>2) ="} \\ |
2134 %@{text "Let (q \<bullet> p) (q \<bullet> t\<^isub>1) (q \<bullet> t\<^isub>2) ="} \\ |
2026 \hspace{15mm}@{text "Let (r \<bullet>\<AL>\<^bsub>bn\<^esub> (q \<bullet> p)) (q \<bullet> t\<^isub>1) (r \<bullet> (q \<bullet> t\<^isub>2))"} |
2135 %\hspace{15mm}@{text "Let (r \<bullet>\<AL>\<^bsub>bn\<^esub> (q \<bullet> p)) (q \<bullet> t\<^isub>1) (r \<bullet> (q \<bullet> t\<^isub>2))"} |
2027 \end{tabular} |
2136 %\end{tabular} |
2028 \end{center} |
2137 %\end{center} |
2029 |
2138 % |
2030 \noindent |
2139 %\noindent |
2031 So instead of proving @{text "P\<^bsub>trm\<^esub> c (q \<bullet> Let p t\<^isub>1 t\<^isub>2)"}, we can equally |
2140 %So instead of proving @{text "P\<^bsub>trm\<^esub> c (q \<bullet> Let p t\<^isub>1 t\<^isub>2)"}, we can equally |
2032 establish @{text "P\<^bsub>trm\<^esub> c (Let (r \<bullet>\<AL>\<^bsub>bn\<^esub> (q \<bullet> p)) (q \<bullet> t\<^isub>1) (r \<bullet> (q \<bullet> t\<^isub>2)))"}. |
2141 %establish @{text "P\<^bsub>trm\<^esub> c (Let (r \<bullet>\<AL>\<^bsub>bn\<^esub> (q \<bullet> p)) (q \<bullet> t\<^isub>1) (r \<bullet> (q \<bullet> t\<^isub>2)))"}. |
2033 To do so, we will use the implication \eqref{strong} of the strong induction |
2142 %To do so, we will use the implication \eqref{strong} of the strong induction |
2034 principle, which requires us to discharge |
2143 %principle, which requires us to discharge |
2035 the following four proof obligations: |
2144 %the following four proof obligations: |
2036 % |
2145 %% |
2037 \begin{center} |
2146 %\begin{center} |
2038 \begin{tabular}{rl} |
2147 %\begin{tabular}{rl} |
2039 {\it (i)} & @{text "set (bn (r \<bullet>\<AL>\<^bsub>bn\<^esub> (q \<bullet> p))) #\<^sup>* c"}\\ |
2148 %{\it (i)} & @{text "set (bn (r \<bullet>\<AL>\<^bsub>bn\<^esub> (q \<bullet> p))) #\<^sup>* c"}\\ |
2040 {\it (ii)} & @{text "\<forall>d. P\<^bsub>pat\<^esub> d (r \<bullet>\<AL>\<^bsub>bn\<^esub> (q \<bullet> p))"}\\ |
2149 %{\it (ii)} & @{text "\<forall>d. P\<^bsub>pat\<^esub> d (r \<bullet>\<AL>\<^bsub>bn\<^esub> (q \<bullet> p))"}\\ |
2041 {\it (iii)} & @{text "\<forall>d. P\<^bsub>trm\<^esub> d (q \<bullet> t\<^isub>1)"}\\ |
2150 %{\it (iii)} & @{text "\<forall>d. P\<^bsub>trm\<^esub> d (q \<bullet> t\<^isub>1)"}\\ |
2042 {\it (iv)} & @{text "\<forall>d. P\<^bsub>trm\<^esub> d (r \<bullet> (q \<bullet> t\<^isub>2))"}\\ |
2151 %{\it (iv)} & @{text "\<forall>d. P\<^bsub>trm\<^esub> d (r \<bullet> (q \<bullet> t\<^isub>2))"}\\ |
2043 \end{tabular} |
2152 %\end{tabular} |
2044 \end{center} |
2153 %\end{center} |
2045 |
2154 % |
2046 \noindent |
2155 %\noindent |
2047 The first follows from \eqref{rprops} and Lemma~\ref{permutebn}.{\it (i)}; the |
2156 %The first follows from \eqref{rprops} and Lemma~\ref{permutebn}.{\it (i)}; the |
2048 others from the induction hypotheses in \eqref{hyps} (in the fourth case |
2157 %others from the induction hypotheses in \eqref{hyps} (in the fourth case |
2049 we have to use the fact that @{term "(r \<bullet> (q \<bullet> t\<^isub>2)) = (r + q) \<bullet> t\<^isub>2"}). |
2158 %we have to use the fact that @{term "(r \<bullet> (q \<bullet> t\<^isub>2)) = (r + q) \<bullet> t\<^isub>2"}). |
2050 |
2159 % |
2051 Taking now the identity permutation @{text 0} for the permutations in \eqref{hyps}, |
2160 %Taking now the identity permutation @{text 0} for the permutations in \eqref{hyps}, |
2052 we can establish our original goals, namely @{text "P\<^bsub>trm\<^esub> c t"} and \mbox{@{text "P\<^bsub>pat\<^esub> c p"}}. |
2161 %we can establish our original goals, namely @{text "P\<^bsub>trm\<^esub> c t"} and \mbox{@{text "P\<^bsub>pat\<^esub> c p"}}. |
2053 This completes the proof showing that the weak induction principles imply |
2162 %This completes the proof showing that the weak induction principles imply |
2054 the strong induction principles. |
2163 %the strong induction principles. |
2055 *} |
2164 *} |
2056 |
2165 |
2057 |
2166 |
2058 section {* Related Work *} |
2167 section {* Related Work *} |
2059 |
2168 |
2071 representations of bindings comes for free in theorem provers like Isabelle/HOL or |
2180 representations of bindings comes for free in theorem provers like Isabelle/HOL or |
2072 Coq, since the corresponding term-calculi can be implemented as ``normal'' |
2181 Coq, since the corresponding term-calculi can be implemented as ``normal'' |
2073 datatypes. However, in both approaches it seems difficult to achieve our |
2182 datatypes. However, in both approaches it seems difficult to achieve our |
2074 fine-grained control over the ``semantics'' of bindings (i.e.~whether the |
2183 fine-grained control over the ``semantics'' of bindings (i.e.~whether the |
2075 order of binders should matter, or vacuous binders should be taken into |
2184 order of binders should matter, or vacuous binders should be taken into |
2076 account). To do so, one would require additional predicates that filter out |
2185 account). %To do so, one would require additional predicates that filter out |
2077 unwanted terms. Our guess is that such predicates result in rather |
2186 %unwanted terms. Our guess is that such predicates result in rather |
2078 intricate formal reasoning. |
2187 %intricate formal reasoning. |
2079 |
2188 |
2080 Another representation technique for binding is higher-order abstract syntax |
2189 Another representation technique for binding is higher-order abstract syntax |
2081 (HOAS), which for example is implemented in the Twelf system. This representation |
2190 (HOAS), which for example is implemented in the Twelf system. This representation |
2082 technique supports very elegantly many aspects of \emph{single} binding, and |
2191 technique supports very elegantly many aspects of \emph{single} binding, and |
2083 impressive work has been done that uses HOAS for mechanising the metatheory |
2192 impressive work has been done that uses HOAS for mechanising the metatheory |
2156 % |
2265 % |
2157 %\noindent |
2266 %\noindent |
2158 %and therefore need the extra generality to be able to distinguish between |
2267 %and therefore need the extra generality to be able to distinguish between |
2159 %both specifications. |
2268 %both specifications. |
2160 Because of how we set up our definitions, we also had to impose some restrictions |
2269 Because of how we set up our definitions, we also had to impose some restrictions |
2161 (like a single binding function for a deep binder) that are not present in Ott. Our |
2270 (like a single binding function for a deep binder) that are not present in Ott. |
2162 expectation is that we can still cover many interesting term-calculi from |
2271 %Our |
2163 programming language research, for example Core-Haskell. |
2272 %expectation is that we can still cover many interesting term-calculi from |
2273 %programming language research, for example Core-Haskell. |
|
2164 |
2274 |
2165 Pottier presents in \cite{Pottier06} a language, called C$\alpha$ml, for |
2275 Pottier presents in \cite{Pottier06} a language, called C$\alpha$ml, for |
2166 representing terms with general binders inside OCaml. This language is |
2276 representing terms with general binders inside OCaml. This language is |
2167 implemented as a front-end that can be translated to OCaml with the help of |
2277 implemented as a front-end that can be translated to OCaml with the help of |
2168 a library. He presents a type-system in which the scope of general binders |
2278 a library. He presents a type-system in which the scope of general binders |
2173 However, we have not proved this. Pottier gives a definition for |
2283 However, we have not proved this. Pottier gives a definition for |
2174 $\alpha$-equivalence, which also uses a permutation operation (like ours). |
2284 $\alpha$-equivalence, which also uses a permutation operation (like ours). |
2175 Still, this definition is rather different from ours and he only proves that |
2285 Still, this definition is rather different from ours and he only proves that |
2176 it defines an equivalence relation. A complete |
2286 it defines an equivalence relation. A complete |
2177 reasoning infrastructure is well beyond the purposes of his language. |
2287 reasoning infrastructure is well beyond the purposes of his language. |
2288 Similar work for Haskell with similar results was reported by Cheney \cite{Cheney05a}. |
|
2178 |
2289 |
2179 In a slightly different domain (programming with dependent types), the |
2290 In a slightly different domain (programming with dependent types), the |
2180 paper \cite{Altenkirch10} presents a calculus with a notion of |
2291 paper \cite{Altenkirch10} presents a calculus with a notion of |
2181 $\alpha$-equivalence related to our binding mode \isacommand{bind (res)}. |
2292 $\alpha$-equivalence related to our binding mode \isacommand{bind (res)}. |
2182 The definition in \cite{Altenkirch10} is similar to the one by Pottier, except that it |
2293 The definition in \cite{Altenkirch10} is similar to the one by Pottier, except that it |