# HG changeset patch # User Christian Urban # Date 1316367499 -7200 # Node ID 8de43bd80bc2ec1c711997d37be4ca60cd6e8bb0 # Parent 1b53c9e8719f68f3f33f1c8f106e0d94695c038f polished diff -r 1b53c9e8719f -r 8de43bd80bc2 LMCS-Paper/Paper.thy --- a/LMCS-Paper/Paper.thy Fri Sep 16 11:24:53 2011 +0200 +++ b/LMCS-Paper/Paper.thy Sun Sep 18 19:38:19 2011 +0200 @@ -45,8 +45,8 @@ alpha_abs_lst ("_ \\<^raw:{$\,_{\textit{abs\_list}}$}> _") and alpha_abs_res ("_ \\<^raw:{$\,_{\textit{abs\_set+}}$}> _") and Abs_set ("[_]\<^bsub>set\<^esub>._" [20, 101] 999) and - Abs_lst ("[_]\<^bsub>list\<^esub>._") and - Abs_dist ("[_]\<^bsub>#list\<^esub>._") and + Abs_lst ("[_]\<^bsub>list\<^esub>._" [20, 101] 999) and + Abs_dist ("[_]\<^bsub>#list\<^esub>._" [20, 101] 999) and Abs_res ("[_]\<^bsub>set+\<^esub>._") and Abs_print ("_\<^bsub>set\<^esub>._") and Cons ("_::_" [78,77] 73) and @@ -282,7 +282,7 @@ easier than reasoning with raw terms. The fundamental reason for this is that the HOL-logic underlying Nominal Isabelle allows us to replace ``equals-by-equals''. In contrast, replacing - ``alpha-equals-by-alpha-equals'' in a representation based on raw terms + ``alpha-equals-by-alpha-equals'' in a representation based on ``raw'' terms requires a lot of extra reasoning work. Although in informal settings a reasoning infrastructure for alpha-equated @@ -387,23 +387,25 @@ which includes multiple binders in type-schemes.\medskip \noindent - {\bf Contributions:} We provide three new definitions for when terms + {\bf Contributions:} We provide three new definitions for when terms involving general binders are alpha-equivalent. These definitions are inspired by earlier work of Pitts \cite{Pitts04}. By means of automatic - proofs, we establish a reasoning infrastructure for alpha-equated - terms, including properties about support, freshness and equality - conditions for alpha-equated terms. We are also able to derive strong + proofs, we establish a reasoning infrastructure for alpha-equated terms, + including properties about support, freshness and equality conditions for + alpha-equated terms. We are also able to automatically derive strong induction principles that have the variable convention already built in. - The method behind our specification of general binders is taken - from the Ott-tool, but we introduce crucial restrictions, and also extensions, so - that our specifications make sense for reasoning about alpha-equated terms. - The main improvement over Ott is that we introduce three binding modes - (only one is present in Ott), provide formalised definitions for alpha-equivalence and + For this we simplify the earlier automated proofs by using the proof tools + from the function package~\cite{Krauss09} of Isabelle/HOL. The method + behind our specification of general binders is taken from the Ott-tool, but + we introduce crucial restrictions, and also extensions, so that our + specifications make sense for reasoning about alpha-equated terms. The main + improvement over Ott is that we introduce three binding modes (only one is + present in Ott), provide formalised definitions for alpha-equivalence and for free variables of our terms, and also derive a reasoning infrastructure for our specifications from ``first principles'' inside a theorem prover. - \begin{figure} + \begin{figure}[t] \begin{boxedminipage}{\linewidth} \begin{center} \begin{tabular}{@ {\hspace{8mm}}r@ {\hspace{2mm}}r@ {\hspace{2mm}}l} @@ -638,7 +640,7 @@ Note that @{term "supp x \* \"} is equivalent with @{term "supp \ \* x"}, which means we could also formulate - Propositions \ref{supppermeq} and \ref{avoiding} in the other `direction', however the + Propositions \ref{supppermeq} and \ref{avoiding} in the other `direction'; however the reasoning infrastructure of Nominal Isabelle is set up so that it provides more automation for the formulation given above. @@ -721,8 +723,8 @@ and @{text bs} are lists of atoms). If we do not want to make any difference between the order of binders \emph{and} - also allow vacuous binders, that means according to Pitts \emph{restrict} names - \cite{Pitts04}, then we keep sets of binders, but drop + also allow vacuous binders, that means according to Pitts~\cite{Pitts04} + \emph{restrict} names, then we keep sets of binders, but drop condition {\it (iv)} in Definition~\ref{alphaset}: \begin{defi}[Alpha-Equivalence for Set+-Bindings]\label{alphares}\mbox{}\\ @@ -764,10 +766,10 @@ shown that all three notions of alpha-equivalence coincide, if we only abstract a single atom. - In the rest of this section we are going to show that the alpha-equivalences really - lead to abstractions where some atoms are bound (more precisely removed from the - support). For this we are going to introduce - three abstraction types that are quotients of the relations + In the rest of this section we are going to show that the alpha-equivalences + really lead to abstractions where some atoms are bound (more precisely + removed from the support). For this we will consider three abstraction + types that are quotients of the relations \begin{equation} \begin{array}{r} @@ -841,7 +843,7 @@ \noindent In effect, this theorem states that the atoms @{text "as"} are bound in the - abstraction. As stated earlier, this can be seen as test that our + abstraction. As stated earlier, this can be seen as litmus test that our Definitions \ref{alphaset}, \ref{alphalist} and \ref{alphares} capture the idea of alpha-equivalence relations. Below we will give the proof for the first equation of Theorem \ref{suppabs}. The others follow by similar @@ -874,10 +876,10 @@ \begin{proof} If @{term "a = b"} the lemma is immediate, since @{term "(a \ b) = 0"}. - Also in the other case it is straightforward using \eqref{abseqiff} and - observing that the assumptions give us @{term "(a \ b) \ (supp x - as) = - (supp x - as)"}. We therefore can use as permutation the swapping @{term - "(a \ b)"}. + Also in the other case the lemma is straightforward using \eqref{abseqiff} + and observing that the assumptions give us @{term "(a \ b) \ (supp x - as) = + (supp x - as)"}. We therefore can use the swapping @{term "(a \ b)"}. as + the permutation fpr the proof obligation. \end{proof} \noindent @@ -922,7 +924,7 @@ Finally, taking \eqref{halfone} and \eqref{halftwo} together establishes the first equation of Theorem~\ref{suppabs}. - Recall the definition of support in \eqref{suppdef}, and note the difference between + Recall the definition of support given in \eqref{suppdef}, and note the difference between the support of a ``raw'' pair and an abstraction \[ @@ -933,7 +935,9 @@ \noindent While the permutation operations behave in both cases the same (a permutation is just moved to the arguments), the notion of equality is different for pairs and - abstractions. Therefore we have different supports. + abstractions. Therefore we have different supports. In case of abstractions, + we have established that bound atoms are removed from the support of the + abstractions' bodies. The method of first considering abstractions of the form @{term "Abs_set as x"} etc is motivated by the fact that we can conveniently establish at the @@ -1282,8 +1286,8 @@ for the corresponding notion given on the ``raw'' level. So for example we have @{text "ty\<^sup>\ \ ty"} and @{text "C\<^sup>\ \ C"} where @{term ty} is the type used in the quotient construction for - @{text "ty\<^sup>\"} and @{text "C"} is the term-constructor in the ``raw'' type @{text "ty"}, - respectively @{text "C\<^sup>\"} is the corresponding term-constructor in @{text "ty\<^sup>\"}. + @{text "ty\<^sup>\"} and @{text "C"} is the term-constructor of the ``raw'' type @{text "ty"}, + respectively @{text "C\<^sup>\"} is the corresponding term-constructor of @{text "ty\<^sup>\"}. The resulting datatype definition is legal in Isabelle/HOL provided the datatypes are non-empty and the types in the constructors only occur in positive @@ -1299,7 +1303,7 @@ \end{equation}\smallskip \noindent - We need this operation later when we define the notion of alpha-equivalence. + We will need this operation later when we define the notion of alpha-equivalence. The first non-trivial step we have to perform is the generation of \emph{free-atom functions} from the specifications.\footnote{Admittedly, the @@ -1366,9 +1370,9 @@ \noindent where in case @{text "d\<^isub>i"} refers to one of the raw types @{text "ty"}$_{1..n}$ from the specification, the function @{text "fa_ty\<^isub>i"} is the corresponding free-atom function - we are defining by recursion; otherwise we set \mbox{@{text "fa_ty\<^isub>i d\<^isub>i = supp d\<^isub>i"}}. The reason + we are defining by recursion; otherwise we set \mbox{@{text "fa_ty\<^isub>i \ supp"}}. The reason for the latter is that @{text "ty"}$_i$ is not a type that is part of the specification, and - we assume @{text supp} is the generic notion that characterises the free variables of + we assume @{text supp} is the generic function that characterises the free variables of a type (in fact in the next section we will show that the free-variable functions we define here, are equal to the support once lifted to alpha-equivalence classes). @@ -1595,8 +1599,7 @@ $\approx_{\,\textit{set}}^{\textit{R}, \textit{fa}}$ given in Section~\ref{sec:binders} (similarly $\approx_{\,\textit{set+}}^{\textit{R}, \textit{fa}}$ and $\approx_{\,\textit{list}}^{\textit{R}, \textit{fa}}$ for the other - binding modes). This premise defines alpha-equivalence of two abstractions - involving multiple binders. As above, we first build the tuples @{text "D"} and + binding modes). As above, we first build the tuples @{text "D"} and @{text "D'"} for the bodies @{text "d"}$_{1..q}$, and the corresponding compound alpha-relation @{text "R"} (shown in \eqref{rempty}). For $\approx_{\,\textit{set}}^{\textit{R}, \textit{fa}}$ we also need @@ -1630,7 +1633,7 @@ inside the structure of these binders. An example is @{text "Let"} where we have to make sure the right-hand sides of assignments are alpha-equivalent. For this we use relations @{text "\bn"}$_{1..m}$ (which we - will formally define shortly). Let us assume the non-recursive deep binders + will define shortly). Let us assume the non-recursive deep binders in @{text "bc\<^isub>i"} are \[ @@ -1687,7 +1690,7 @@ for the existentially quantified permutation). Again let us take a look at a concrete example for these definitions. For - the specification given in \eqref{letrecs} + the specification shown in \eqref{letrecs} we have three relations $\approx_{\textit{trm}}$, $\approx_{\textit{assn}}$ and $\approx_{\textit{bn}}$ with the following rules: @@ -1725,7 +1728,7 @@ The underlying reason is that the terms inside an assignment are not meant to be ``under'' the binder. Such a premise is \emph{not} needed in @{text "Let_rec"}, because there all components of an assignment are ``under'' the binder. - Note also that in case of more than one body (that is in the @{text "Let_rec"}-case) + Note also that in case of more than one body (that is in the @{text "Let_rec"}-case above) we need to parametrise the relation $\approx_{\textit{list}}$ with a compound equivalence relation and a compound free-atom function. This is because the corresponding binding clause specifies a binder with two bodies, namely @@ -1885,7 +1888,7 @@ \noindent We call these conditions as \emph{quasi-injectivity}. They correspond to the - premises in our alpha-equiva\-lence relations, with the exception that the + premises in our alpha-equiva\-lence relations, except that the relations @{text "\ty"}$_{1..n}$ are all replaced by equality (and similarly the free-atom and binding functions are replaced by their lifted counterparts). Recall the alpha-equivalence rules for @{text "Let"} and @@ -1936,10 +1939,10 @@ \end{equation}\smallskip \noindent - whereby the @{text P}$_{1..n}$ are the properties established by the induction - and the @{text y}$_{1..n}$ are of type @{text "ty\"}$_{1..n}$. Note that - the induction principle has for the term constructors @{text "C"}$^\alpha_1$ a - hypothesis of the form + whereby the @{text P}$_{1..n}$ are the properties established by the + induction, and the @{text y}$_{1..n}$ are of type @{text + "ty\"}$_{1..n}$. Note that for the term constructors @{text + "C"}$^\alpha_1$ the induction principle has a hypothesis of the form \[ \mbox{@{text "\x\<^isub>1\x\<^isub>k. P\<^isub>i x\<^isub>i \ \ \ P\<^isub>j x\<^isub>j \ P (C\\<^sub>1 x\<^isub>1 \ x\<^isub>k)"}} @@ -1952,7 +1955,7 @@ Recall the lambda-calculus with @{text "Let"}-patterns shown in \eqref{letpat}. The cases lemmas and the induction principle shown in - \eqref{cases} and \eqref{induct} boil down to the following three inference + \eqref{cases} and \eqref{induct} boil down in this example to the following three inference rules (the cases lemmas are on the left-hand side; the induction principle on the right): @@ -2001,7 +2004,7 @@ \noindent This allows us to prove using the induction principle for @{text "ty\"}$_{1..n}$ that every element of type @{text "ty\"}$_{1..n}$ is finitely supported - (using Prop.~\ref{supportsprop}{\it (i)}). + (using Proposition~\ref{supportsprop}{\it (i)}). Similarly, we can establish by induction that the free-atom functions and binding functions are equivariant, namely @@ -2016,10 +2019,11 @@ \noindent Lastly, we can show that the support of elements in @{text - "ty\"}$_{1..n}$ is the same as @{text "fa_ty\"}$_{1..n}$. This fact - is important in the nominal setting where the general theory is formulated - in terms of support and freshness, but also provides evidence that our - notions of free-atoms and alpha-equivalence ``match up''. + "ty\"}$_{1..n}$ is the same as the free atom functions @{text + "fa_ty\"}$_{1..n}$. This fact is important in the nominal setting where + the general theory is formulated in terms of support and freshness, but also + provides evidence that our notions of free-atoms and alpha-equivalence + ``match up'' correctly. \begin{thm}\label{suppfa} For @{text "x"}$_{1..n}$ with type @{text "ty\"}$_{1..n}$, we have @@ -2036,8 +2040,9 @@ \end{proof} \noindent - Consequently we can simplify the quasi-injection lemmas, for example the ones - given in \eqref{alphalift} for @{text "Let\<^sup>\"} and @{text "Let_rec\<^sup>\"} to + Consequently, we can replace the free atom functions by @{text "supp"} in + our quasi-injection lemmas. In the examples shown in \eqref{alphalift}, for instance, + we obtain for @{text "Let\<^sup>\"} and @{text "Let_rec\<^sup>\"} \[\mbox{ \begin{tabular}{@ {}c @ {}} @@ -2051,11 +2056,10 @@ \]\smallskip \noindent - Taking the fact into account that the compound equivalence relation @{term + Taking into account that the compound equivalence relation @{term "equ2"} and the compound free-atom function @{term "supp2"} are by definition equal to @{term "equal"} and @{term "supp"}, respectively, the - above rules simplify even further to - + above rules simplify further to \[\mbox{ \begin{tabular}{@ {}c @ {}} @@ -2085,8 +2089,7 @@ \noindent using the support of abstractions derived in Theorem~\ref{suppabs}. - - To sum up this section, we can establish a reasoning infrastructure for the + To sum up this section, we have established a reasoning infrastructure for the types @{text "ty\"}$_{1..n}$ by first lifting definitions from the ``raw'' level to the quotient level and then by proving facts about these lifted definitions. All necessary proofs are generated automatically @@ -2099,30 +2102,29 @@ text {* In the previous section we derived induction principles for alpha-equated terms (see \eqref{induct} for the general form and \eqref{inductex} for an - instance). This was done by lifting the corresponding inductions principles + example). This was done by lifting the corresponding inductions principles for ``raw'' terms. We already employed these induction principles for - deriving several facts for alpha-equated terms, including the property that + deriving several facts about alpha-equated terms, including the property that the free-variable functions and the notion of support coincide. Still, we call these induction principles \emph{weak}, because for a term-constructor, say \mbox{@{text "C\<^sup>\ x\<^isub>1\x\<^isub>r"}}, the induction hypothesis requires us to establish (under some assumptions) a property @{text "P (C\<^sup>\ x\<^isub>1\x\<^isub>r)"} for \emph{all} @{text - "x"}$_{1..r}$. The problem is that in the presence of binders we cannot make + "x"}$_{1..r}$. The problem with this is that in the presence of binders we cannot make any assumptions about the atoms that are bound. One obvious way around this problem is to rename them. Unfortunately, this leads to very clunky proofs - and makes formalisations grievous experiences (especially in the case for + and makes formalisations grievous experiences (especially in the context of multiple bound atoms). - - For the older versions of Nominal Isabelle we described in - \cite{Urban08} a method for automatically strengthening weak induction - principles. These stronger induction principles allow the user to make - additional assumptions about bound atoms. The advantage of these assumptions - is that they make in most cases any renaming of bound atoms unnecessary. To - explain how the strengthening works in the presence of multiple binders, we - use as running example the lambda-calculus with @{text "Let"}-patterns shown - in \eqref{letpat}. Its weak induction principle is given in - \eqref{inductex}. The stronger induction principle is as follows: + For the older versions of Nominal Isabelle we described in \cite{Urban08} a + method for automatically strengthening weak induction principles. These + stronger induction principles allow the user to make additional assumptions + about bound atoms. The advantage of these assumptions is that they make in + most cases any renaming of bound atoms unnecessary. To explain how the + strengthening works, we use as running example the lambda-calculus with + @{text "Let"}-patterns shown in \eqref{letpat}. Its weak induction principle + is given in \eqref{inductex}. The stronger induction principle is as + follows: \begin{equation}\label{stronginduct} \mbox{ @@ -2143,25 +2145,27 @@ \noindent - Instead of establishing the two properties @{text " P\<^bsub>trm\<^esub> - y\<^isub>1 \ P\<^bsub>pat\<^esub> y\<^isub>2"}, as the weak one does, the - stronger induction principle establishes the properties @{text " - P\<^bsub>trm\<^esub> c y\<^isub>1 \ P\<^bsub>pat\<^esub> c y\<^isub>2"} in - which the additional parameter @{text c} is assumed to be of finite - support. The purpose of @{text "c"} is to ``control'' which freshness - assumptions the binders should satisfy in the @{text "Lam\<^sup>\"} and - @{text "Let_pat\<^sup>\"} cases: for @{text "Lam\<^sup>\"} we can assume the - bound atom @{text "x\<^isub>1"} is fresh for @{text "c"}; for @{text - "Let_pat\<^sup>\"} we can assume all bound atoms from an assignment are fresh - for @{text "c"}. If @{text "c"} is instantiated appropriately, the user can - mimic the ``pencil-and-paper'' reasoning employing the usual variable - convention \cite{Urban08}. + Notice that instead of establishing two properties of the form @{text " + P\<^bsub>trm\<^esub> y\<^isub>1 \ P\<^bsub>pat\<^esub> y\<^isub>2"}, as the + weak one does, the stronger induction principle establishes the properties + of the form @{text " P\<^bsub>trm\<^esub> c y\<^isub>1 \ + P\<^bsub>pat\<^esub> c y\<^isub>2"} in which the additional parameter @{text + c} is assumed to be of finite support. The purpose of @{text "c"} is to + ``control'' which freshness assumptions the binders should satisfy in the + @{text "Lam\<^sup>\"} and @{text "Let_pat\<^sup>\"} cases: for @{text + "Lam\<^sup>\"} we can assume the bound atom @{text "x\<^isub>1"} is fresh + for @{text "c"} (third line); for @{text "Let_pat\<^sup>\"} we can assume + all bound atoms from an assignment are fresh for @{text "c"} (fourth + line). If @{text "c"} is instantiated appropriately in the strong induction + principle, the user can mimic the usual ``pencil-and-paper'' reasoning + employing the variable convention about bound and free variables being + distinct \cite{Urban08}. - In what follows we will show that the induction principle in - \eqref{inductex} implies \eqref{stronginduct}. This fact was established for + In what follows we will show that the weak induction principle in + \eqref{inductex} implies the strong one \eqref{stronginduct}. This fact was established for single binders in \cite{Urban08} by some quite involved, nevertheless automated, induction proof. In this paper we simplify the proof by - leveraging the automated proof methods from the function package of + leveraging the automated proving methods from the function package of Isabelle/HOL \cite{Krauss09}. The reasoning principle behind these methods is well-founded induction. To use them in our setting, we have to discharge two proof obligations: one is that we have well-founded measures (one for @@ -2169,9 +2173,8 @@ step and the other is that we have covered all cases in the induction principle. Once these two proof obligations are discharged, the reasoning infrastructure in the function package will automatically derive the - stronger induction principle. This considerably simplifies the work we have - to do here. - + stronger induction principle. This way of establishing the stronger induction + principle is considerably simpler than the work presented \cite{Urban08}. As measures we can use the size functions @{text "size_ty"}$^\alpha_{1..n}$, which we lifted in the previous section and which are all well-founded. It @@ -2200,25 +2203,25 @@ \]\smallskip \noindent - They are stronger in the sense that they allow us to assume that the bound - atoms avoid a context @{text "c"} (which is assumed to be finitely - supported). This is similar with the stronger induction principles. + They are stronger in the sense that they allow us to assume in the @{text + "Lam\<^sup>\"} and @{text "Let_pat\<^sup>\"} cases that the bound atoms + avoid a context @{text "c"} (which is assumed to be finitely supported). These stronger cases lemmas need to be derived from the `weak' cases lemmas given in \eqref{inductex}. This is trivial in case of patterns (the one on the right-hand side) since the weak and strong cases lemma coincide (there is no binding in patterns). Interesting are only the cases for @{text "Lam\<^sup>\"} and @{text "Let_pat\<^sup>\"}, where we have some binders and - therefore have an addition assumption. Let us show first establish the case - for @{text "Lam\<^sup>\"}. By the weak cases lemma \eqref{inductex} we can - assume that + therefore have an addition assumption about avoiding @{text "c"}. Let us + first establish the case for @{text "Lam\<^sup>\"}. By the weak cases lemma + \eqref{inductex} we can assume that \begin{equation}\label{assm} @{text "y = Lam\<^sup>\ x\<^isub>1 x\<^isub>2"} \end{equation}\smallskip \noindent - holds and need to establish @{text "P\<^bsub>trm\<^esub>"}. The stronger cases lemma has the + holds, and need to establish @{text "P\<^bsub>trm\<^esub>"}. The stronger cases lemma has the corresponding implication \begin{equation}\label{imp} @@ -2226,19 +2229,25 @@ \end{equation}\smallskip \noindent - which we can use to infer @{text "P\<^bsub>trm\<^esub>"}. Clearly, we cannot + which we must use to infer @{text "P\<^bsub>trm\<^esub>"}. Clearly, we cannot use this implication directly, because we have no information whether @{text "x\<^isub>1"} is fresh for @{text "c"}. However, we can use Properties - \ref{supppermeq} and \ref{avoiding} to rename @{text "x\<^isub>1"}: We know + \ref{supppermeq} and \ref{avoiding} to rename @{text "x\<^isub>1"}: we know by Theorem~\ref{suppfa} that @{text "{atom x\<^isub>1} #\<^sup>* Lam\<^sup>\ x\<^isub>1 x\<^isub>2"} (since its support is @{text "supp x\<^isub>2 - - {atom x\<^isub>1}"}). Property \ref{avoiding} provides us therefore with a + {atom x\<^isub>1}"}). Property \ref{avoiding} provides us then with a permutation @{text "\"}, such that @{text "{atom (\ \ x\<^isub>1)} #\<^sup>* c"} and \mbox{@{text "supp (Lam\<^sup>\ x\<^isub>1 x\<^isub>2) #\<^sup>* \"}} hold. - By using Property \ref{supppermeq}, we can infer from the latter that @{text - "Lam\<^sup>\ (\ \ x\<^isub>1) (\ \ x\<^isub>2) = Lam\<^sup>\ x\<^isub>1 x\<^isub>2"} holds. We can use this equation in - the assumption \eqref{assm} and then use \eqref{imp} with the renamed @{text "\ \ x\<^isub>1"} - and @{text "\ \ x\<^isub>2"} in order to conclude this case. + By using Property \ref{supppermeq}, we can infer from the latter that + + \[ + @{text "Lam\<^sup>\ (\ \ x\<^isub>1) (\ \ x\<^isub>2) = Lam\<^sup>\ x\<^isub>1 x\<^isub>2"} + \]\smallskip + + \noindent + holds. We can use this equation in the assumption \eqref{assm}, and hence + use the implication \eqref{imp} with the renamed @{text "\ \ x\<^isub>1"} + and @{text "\ \ x\<^isub>2"} for concluding this case. The @{text "Let_pat\<^sup>\"}-case involving a deep binder is slightly more complicated. We have the assumption @@ -2248,11 +2257,11 @@ \end{equation}\smallskip \noindent - and the implication + and the implication from the stronger cases lemma - \[ + \begin{equation}\label{impletpat} @{text "\x\<^isub>1 x\<^isub>2 x\<^isub>3. set (bn\<^sup>\ x\<^isub>1) #\<^sup>* c \ y = Let_pat\<^sup>\ x\<^isub>1 x\<^isub>2 x\<^isub>3 \ P\<^bsub>trm\<^esub>"} - \]\smallskip + \end{equation}\smallskip \noindent The reason that this case is more complicated is that we cannot apply directly Property @@ -2265,13 +2274,14 @@ \]\smallskip \noindent - Although @{text x} and @{text y} are bound in this term, they are also free - in the assignment. We can, however, obtain obtain such a renaming - permutation, say @{text "\"}, for the abstraction @{term "Abs_lst (bn_al - x\<^isub>1) x\<^isub>3"}. So we have \mbox{@{term "set (bn_al (\ \ - x\<^isub>1)) \* c"}} and @{term "Abs_lst (bn_al (\ \ x\<^isub>1)) (\ \ - x\<^isub>3) = Abs_lst (bn_al x\<^isub>1) x\<^isub>3"} (remember @{text "set"} and @{text "bn\<^sup>\"} are equivariant). - Now the quasi-injective property for @{text "Let_pat\<^sup>\"} states + where @{text x} and @{text y} are bound in the term, but they are also free + in the assignment. We can, however, obtain such a renaming permutation, say + @{text "\"}, for the abstraction @{term "Abs_lst (bn_al x\<^isub>1) + x\<^isub>3"}. As a result we have \mbox{@{term "set (bn_al (\ \ x\<^isub>1)) + \* c"}} and @{term "Abs_lst (bn_al (\ \ x\<^isub>1)) (\ \ x\<^isub>3) = + Abs_lst (bn_al x\<^isub>1) x\<^isub>3"} (remember @{text "set"} and @{text + "bn\<^sup>\"} are equivariant). Now the quasi-injective property for @{text + "Let_pat\<^sup>\"} states that \[ \infer{@{text "Let_pat\<^sup>\ p t\<^isub>1 t\<^isub>2 = Let_pat\<^sup>\ p\ t\\<^isub>1 t\\<^isub>2"}} @@ -2280,31 +2290,30 @@ \]\smallskip \noindent - Since all atoms in a pattern are bound by @{text "Let_pat\<^sup>\"} - (hence @{text "(\ \ x\<^isub>1) \\\<^bsub>bn\<^esub> x\<^isub>1"} holds for every @{text "\"}), we can infer the - equation + Since all atoms in a pattern are bound by @{text "Let_pat\<^sup>\"}, we can infer + @{text "(\ \ x\<^isub>1) \\\<^bsub>bn\<^esub> x\<^isub>1"} holds for every @{text "\"}. Therefore we have that \[ @{text "Let_pat\<^sup>\ (\ \ x\<^isub>1) x\<^isub>2 (\ \ x\<^isub>3) = Let_pat\<^sup>\ x\<^isub>1 x\<^isub>2 x\<^isub>3"} \]\smallskip \noindent - Taking the left-hand side as our assumption in \eqref{assmtwo}, we can use - the implication from the stronger cases lemma to infer @{text "P\<^bsub>trm\<^esub>"}, as needed. + Taking the left-hand side in the assumption from \eqref{assmtwo}, we can use + the implication \eqref{impletpat} from the stronger cases lemma to infer @{text "P\<^bsub>trm\<^esub>"}, as needed. The remaining difficulty is when a deep binder contains atoms that are - bound, but also atoms that are free. An example is @{text "Let\<^sup>\"} in \eqref{}. - Then @{text "(\ \ x\<^isub>1) - \\\<^bsub>bn\<^esub> x\<^isub>1"} does not hold in general. In such - cases, however, we only want to rename binders that will become bound, which - does not affect @{text "\\\<^bsub>bn\<^esub>"}. The problem is that the - permutation operation @{text "\"} permutes all of them. The remedy is to - introduce an auxiliary permutation operation, written @{text "_ - \\<^bsub>bn\<^esub> _"}, for deep binders that only permute bound atoms and - leaves the other atoms unchanged. Like the @{text - "fa_bn"}$_{1..m}$-functions, we can define this operation over raw terms - analysing how the @{text "bn"}$_{1..m}$-functions are defined and then lift - them to alpha-equivalent terms. Assuming the user specified a clause + bound, but also some that are free. An example is @{text "Let\<^sup>\"} in + the example \eqref{letrecs}. In such cases @{text "(\ \ x\<^isub>1) + \\\<^bsub>bn\<^esub> x\<^isub>1"} does not hold in general. The idea is + that we only want to rename binders that will become bound. This does not + affect @{text "\\\<^bsub>bn\<^esub>"}. However, the problem is that the + permutation operation @{text "_ \ _"} applies to all of them. To avoid this + we introduce an auxiliary permutation operations, written @{text "_ + \\<^bsub>bn\<^esub> _"}, for deep binders that only permutes bound atoms (or + more precisely the atoms specified by the @{text "bn"}-functions) and leaves + the other atoms unchanged. Like the @{text "fa_bn"}$_{1..m}$-functions, we + can define these operations over raw terms analysing how the @{text + "bn"}$_{1..m}$-functions are defined. Assuming the user specified a clause \[ @{text "bn (C x\<^isub>1 \ x\<^isub>r) = rhs"} @@ -2326,25 +2335,26 @@ alpha-equated terms. Moreover we can prove the following two properties \begin{lem}\label{permutebn} - Given a binding function @{text "bn\<^sup>\"} then for all @{text "\"}\\ + Given a binding function @{text "bn\<^sup>\"} then for all @{text "\"}\smallskip\\ {\it (i)} @{text "\ \ (bn\<^sup>\ x) = bn\<^sup>\ (\ \\\<^bsub>bn\<^esub> x)"} and\\ {\it (ii)} @{text "(\ \\\<^bsub>bn\<^esub> x) \\\<^bsub>bn\<^esub> x"}. \end{lem} \begin{proof} - By induction on @{text x}. The properties follow by simple unfolding - of the definitions. + By induction on @{text x}. The properties follow by unfolding of the + definitions. \end{proof} \noindent - The first property states that a permutation applied to a binding function is - equivalent to first permuting the binders and then calculating the bound - atoms. The main point of the auxiliary permutation - functions is that it allows us to rename just the binders in a term, - without changing anything else. + The first property states that a permutation applied to a binding function + is equivalent to first permuting the binders and then calculating the bound + atoms. The second states that @{text "_ \\<^bsub>bn\<^esub> _"} preserves + @{text "\\\<^bsub>bn\<^esub>"}. The main point of the auxiliary + permutation functions is that they allow us to rename just the binders in a + term, without changing anything else. Having the auxiliary permutation function in place, we can now solve all remaining cases. - For @{text "Let\<^sup>\"} term-constructor, for example, we can by Property \ref{avoiding} + For the @{text "Let\<^sup>\"} term-constructor, for example, we can by Property \ref{avoiding} obtain a @{text "\"} such that \[ @@ -2356,7 +2366,7 @@ hold. Using Lemma \ref{permutebn}{\it (i)} we can simplify this to @{text "set (bn\<^sup>\ (\ \\\<^bsub>bn\<^esub> x\<^isub>1)) #\<^sup>* c"} and @{text "[bn\<^sup>\ (\ \\\<^bsub>bn\<^esub> x\<^isub>1)]\<^bsub>list\<^esub>. (\ \ x\<^isub>2) = [bn\<^sup>\ x\<^isub>1]\<^bsub>list\<^esub>. x\<^isub>2"}. Since - @{text "(\ \\\<^bsub>bn\<^esub> x\<^isub>1) \\\<^bsub>bn\<^esub> x\<^isub>1"} holds by Lemma \ref{permutebn}{\it (ii)} + @{text "(\ \\\<^bsub>bn\<^esub> x\<^isub>1) \\\<^bsub>bn\<^esub> x\<^isub>1"} holds by Lemma \ref{permutebn}{\it (ii)}, we can infer that \[ @@ -2364,16 +2374,12 @@ \]\smallskip \noindent - are alpha-equivalent. This allows us to use the implication from the strong cases - lemma and we can discharge all proof-obligations to do with having covered all - cases. + holds. This allows us to use the implication from the strong cases + lemma. - This completes the proof showing that the weak induction principles imply - the strong induction principles. We have automated the reasoning for all - term-calculi the user might specify. The feature of the function package - by Krauss \cite{Krauss09} that allows us to establish an induction principle - by just finding decreasing measures and showing that the induction principle - covers all cases, tremendously helped us in implementing the automation. + Conseqently, we can discharge all proof-obligations to do with having covered all + cases. This completes the proof showing that the weak induction principles imply + the strong induction principles. *} @@ -2503,7 +2509,7 @@ cover many interesting term-calculi from programming language research, for example Core-Haskell (see Figure~\ref{nominalcorehas}). - \begin{figure}[p!] + \begin{figure}[t] \begin{boxedminipage}{\linewidth} \small \begin{tabular}{l} @@ -2555,7 +2561,7 @@ lists @{text "co_lst"}, @{text "assoc_lst"} and so on. Apart from that, the declaration follows closely the original in Figure~\ref{corehas}. The point of our work is that having made such a declaration in Nominal Isabelle, - one obtains automatically a reasoning infrastructure for Core-Haskell. + one obtains automatically a reasoning infrastructure for Core-Haskell.\bigskip\bigskip \label{nominalcorehas}} \end{figure}