diff -r 9a894c42e80e -r a2d5f9ea17ad Paper/Paper.thy --- a/Paper/Paper.thy Fri Apr 02 05:09:47 2010 +0200 +++ b/Paper/Paper.thy Fri Apr 02 06:45:50 2010 +0200 @@ -1138,10 +1138,10 @@ raw datatype. We can also easily define permutation operations by primitive recursion so that for each term constructor @{text "C ty\<^isub>1 \ ty\<^isub>n"} we have that - - \begin{center} + % + \begin{equation}\label{ceqvt} @{text "p \ (C x\<^isub>1 \ x\<^isub>n) = C (p \ x\<^isub>1) \ (p \ x\<^isub>n)"} - \end{center} + \end{equation} % TODO: we did not define permutation types %\noindent @@ -1463,12 +1463,14 @@ section {* Establishing the Reasoning Infrastructure *} text {* - Having made all necessary definitions for raw terms, we can start introducing - the reasoning infrastructure for the types the user specified. For this we first - have to show that the alpha-equivalence relations defined in the previous - section are indeed equivalence relations. + Having made all necessary definitions for raw terms, we can start + introducing the reasoning infrastructure for the alpha-equated types the + user specified. We sketch in this section the facts we need for establishing + this reasoning infrastructure. We first have to show that the + alpha-equivalence relations defined in the previous section are indeed + equivalence relations. - \begin{lemma} + \begin{lemma}\label{equiv} Given the raw types @{text "ty\<^isub>1, \, ty\<^isub>n"} and binding functions @{text "bn\<^isub>1, \, bn\<^isub>m"}, the relations @{text "\ty\<^isub>1, \, \ty\<^isub>n"} and @{text "\bn\<^isub>1 \ \bn\<^isub>m"} are equivalence relations and equivariant. @@ -1523,7 +1525,7 @@ \noindent under the assumption that @{text "x\<^isub>i \ty\<^isub>i y\<^isub>i"} holds for all recursive arguments and @{text "x\<^isub>i = y\<^isub>i"} for all non-recursive arguments. We can prove this by - analysing the definition of @{text "\ty"}. For this to succed we have to establish an + analysing the definition of @{text "\ty"}. For this to succeed we have to establish an auxiliary fact: given a binding function @{text bn} defined for the type @{text ty} we have that @@ -1534,8 +1536,8 @@ \noindent This can be established by induction on the definition of @{text "\ty"}. - Having established respectfullness for every raw term-constructor, the - quotient package will automaticaly deduce \eqref{distinctalpha} from \eqref{distinctraw}. + Having established respectfulness for every raw term-constructor, the + quotient package will automatically deduce \eqref{distinctalpha} from \eqref{distinctraw}. In fact we can lift any fact from the raw level to the alpha-equated level that apart from variables only contains the raw term-constructors @{text "C\<^isub>i"}. The induction principles derived by the datatype package of Isabelle/HOL for @{text @@ -1557,119 +1559,185 @@ \noindent where the @{text "x\<^isub>i, \, x\<^isub>j"} are the recursive arguments of @{text "C\<^sup>\"}. - - -To lift - the raw definitions to the quotient type, we need to prove that they - \emph{respect} the relation. We follow the definition of respectfullness given - by Homeier~\cite{Homeier05}. The intuition behind a respectfullness condition - is that when a function (or constructor) is given arguments that are - alpha-equivalent the results are also alpha equivalent. For arguments that are - not of any of the relations taken into account, equivalence is replaced by - equality. In particular the respectfullness condition for a @{text "bn"} - function means that for alpha equivalent raw terms it returns the same bound - names. Thanks to the restrictions on the binding functions introduced in - Section~\ref{sec:alpha} we can show that are respectful. + Next we lift the permutation operations defined in \eqref{ceqvt} for + the raw term-constructors @{text "C"}. These facts contain, in addition + to the term-constructors, also permutations operations. Therefore + we have to know that permutation operations are respectful + w.r.t.~alpha-equivalence, which amounts to knowing that the + alpha-equivalence relations are equivariant, which we established + in Lemma~\ref{equiv}. As a result we can add the equations + + \begin{equation}\label{ceqvt} + @{text "p \ (C\<^sup>\ x\<^isub>1 \ x\<^isub>n) = C\<^sup>\ (p \ x\<^isub>1) \ (p \ x\<^isub>n)"} + \end{equation} - \begin{lemma} The functions @{text "bn\<^isub>1 \ bn\<^isub>m"}, @{text "fv_ty\<^isub>1 \ fv_ty\<^isub>n"}, - the raw constructors, the raw permutations and @{text "\bn\<^isub>1 \ \bn\<^isub>m"} are - respectful w.r.t. the relations @{text "\\<^isub>1 \ \\<^isub>n"}. - \end{lemma} - \begin{proof} Respectfullness of permutations is a direct consequence of - equivariance. All other properties by induction on the alpha-equivalence - relation. For @{text "bn"} the thesis follows by simple calculations thanks - to the restrictions on the binding functions. For @{text "fv"} functions it - follows using respectfullness of @{text "bn"}. For type constructors it is a - simple calculation thanks to the way alpha-equivalence was defined. For @{text - "alpha_bn"} after a second induction on the second relation by simple - calculations. \end{proof} + \noindent + to our infrastructure. In a similar fashion we can lift the equations + characterising our free-variable functions and the binding functions. + The necessary respectfulness lemmas are + % + \begin{equation}\label{fnresp} + \mbox{% + \begin{tabular}{l} + @{text "x \ty y"} implies @{text "fv_ty x = fv_ty y"}\\ + @{text "x \ty y"} implies @{text "bn x = bn y"} + \end{tabular}} + \end{equation} - With these respectfullness properties we can use the quotient package - to define the above constants on the quotient level. We can then automatically - lift the theorems that talk about the raw constants to theorems on the quotient - level. The following lifted properties are proved: + \noindent + which can be established by induction on @{text "\ty"}. While the first + kind of lemma is always ensured by way of how we defined the free variable + functions, the second does not hold in general. It only if the @{text bn}-functions + do not return any atom that is also bound. Hence our restriction imposed + on the binding functions that excludes this possibility. + + Having the facts \eqref{fnresp} at our disposal, we can finally lift the + definitions that characterise when two terms of the form \begin{center} - \begin{tabular}{cp{7cm}} -%skipped permute_zero and permute_add, since we do not have a permutation -%definition - $\bullet$ & permutation defining equations \\ - $\bullet$ & @{term "bn"} defining equations \\ - $\bullet$ & @{term "fv_ty"} and @{term "fv_bn"} defining equations \\ - $\bullet$ & induction. The induction principle that we obtain by lifting - is the weak induction principle, just on the term structure \\ - $\bullet$ & quasi-injectivity. This means the equations that specify - when two constructors are equal and comes from lifting the alpha - equivalence defining relations\\ - $\bullet$ & distinctness\\ -%may be skipped - $\bullet$ & equivariance of @{term "fv"} and @{term "bn"} functions\\ + @{text "C x\<^isub>1 \ x\<^isub>n \ty C y\<^isub>1 \ y\<^isub>n"} + \end{center} + + \noindent + are alpha-equivalent. This gives us conditions when the corresponding + alpha-equated terms are equal, namely + + \begin{center} + @{text "C\<^sup>\ x\<^isub>1 \ x\<^isub>n = C\<^sup>\ y\<^isub>1 \ y\<^isub>n"} + \end{center} + + \noindent + We call these conditions as \emph{quasi-injectivity}. Except for one definition we have + to lift in the next section, this completes + the lifting part of establishing the reasoning infrastructure. From + now on we can ``forget'' about the raw types @{text "ty\<^bsub>1..n\<^esub>"} and only + reason with @{text "ty\\<^bsub>1..n\<^esub>"} + + We can first show that the free-variable function and binding functions + are equivariant, namely + + \begin{center} + \begin{tabular}{rcl} + @{text "p \ (fv_ty\<^sup>\ x)"} & $=$ & @{text "fv_ty\<^sup>\ (p \ x)"}\\ + @{text "p \ (bn\<^sup>\ x)"} & $=$ & @{text "bn\<^sup>\ (p \ x)"} \end{tabular} \end{center} - Until now we have not said anything about the support of the - defined type. This is because we could not use the general definition of - support in lifted theorems, since it does not preserve the relation. - Indeed, take the term @{text "\x. x"}. The support of the term is empty @{term "{}"}, - since the @{term "x"} is bound. On the raw level, before the binding is - introduced the term has the support equal to @{text "{x}"}. + \noindent + These facts can be established by structural induction over the @{text x}. + + Until now we have not yet derived any fact about the support of the + alpha-equated terms. Using the equivariance properties in \eqref{ceqvt} we can + show for every term-constructor @{text "C\<^sup>\"} that + + \begin{center} + @{text "supp x\<^isub>1 \ \ supp x\<^isub>n supports (C\<^sup>\ x\<^isub>1 \ x\<^isub>n)"} + \end{center} + + \noindent + holds. This together with Property~\ref{supportsprobs} allows us to show + - To show the support equations for the lifted types we want to use the - Theorem \ref{suppabs}, so we start with showing that they have a finite - support. + \begin{center} + @{text "finite (supp x\<^isub>i)"} + \end{center} - \begin{lemma} The types @{text "ty\<^isup>\\<^isub>1 \ ty\<^isup>\\<^isub>n"} have finite support. + \noindent + by mutual structural induction over @{text "x\<^isub>1, \, x\<^isub>n"} (whereby @{text "x\<^isub>i"} ranges over the types + @{text "ty\\<^isub>1 \ ty\\<^isub>n"}). Lastly, we can show that the support of elements in + @{text "ty\\<^bsub>1..n\<^esub>"} coincides with @{text "fv_ty\\<^bsub>1..n\<^esub>"}. + + \begin{lemma} For every @{text "x\<^isub>i"} of type @{text "ty\\<^bsub>1..n\<^esub>"}, we have that + @{text "supp x\<^isub>i = fv_ty\\<^isub>i x\<^isub>i"} holds. \end{lemma} + \begin{proof} - By induction on the lifted types. For each constructor its support is - supported by the union of the supports of all arguments. By induction - hypothesis we know that each of the recursive arguments has finite - support. We also know that atoms and finite atom sets and lists that - occur in the constructors have finite support. A union of finite - sets is finite thus the support of the constructor is finite. + The proof proceeds by structural induction over the @{text "x\<^isub>i"}. In each case + we unfold the definition of @{text "supp"}, move the swapping inside the + term-constructors and the use the quasi-injectivity lemmas in order to complete the + proof. \end{proof} -% Very vague... - \begin{lemma} For each lifted type @{text "ty\<^isup>\\<^isub>i"}, for every @{text "x"} - of this type: - \begin{equation} - @{term "supp x = fv_ty\<^isup>\\<^isub>i x"}. - \end{equation} - \end{lemma} - \begin{proof} - We will show this by induction together with equations that characterize - @{term "fv_bn\<^isup>\\<^isub>"} in terms of @{term "alpha_bn\<^isup>\"}. For each of @{text "fv_bn\<^isup>\"} - functions this equation is: - \begin{center} - @{term "{a. infinite {b. \ alpha_bn\<^isup>\ ((a \ b) \ x) x}} = fv_bn\<^isup>\ x"} - \end{center} + \noindent + To sum up this section, we established a reasoning infrastructure + for the types @{text "ty\\<^isub>1 \ ty\\<^isub>n"} + by first lifting definitions from the raw level to the quotient level and + then establish facts about these lifted definitions. All necessary proofs + are generated automatically by custom ML-code. This code can deal with + specifications as shown in Figure~\ref{nominalcorehas} for Core-Haskell. - In the induction we need to show these equations together with the goal - for the appropriate constructors. We first transform the right hand sides. - The free variable functions are applied to theirs respective constructors - so we can apply the lifted free variable defining equations to obtain - free variable functions applied to subterms minus binders. Using the - induction hypothesis we can replace free variable functions applied to - subterms by support. Using Theorem \ref{suppabs} we replace the differences - by supports of appropriate abstractions. - - Unfolding the definition of supports on both sides of the equations we - obtain by simple calculations the equalities. - \end{proof} + \begin{figure}[t!] + \begin{boxedminipage}{\linewidth} + \small + \begin{tabular}{l} + \isacommand{atom\_decl}~@{text "var"}\\ + \isacommand{atom\_decl}~@{text "cvar"}\\ + \isacommand{atom\_decl}~@{text "tvar"}\\[1mm] + \isacommand{nominal\_datatype}~@{text "tkind ="}\\ + \phantom{$|$}~@{text "KStar"}~$|$~@{text "KFun tkind tkind"}\\ + \isacommand{and}~@{text "ckind ="}\\ + \phantom{$|$}~@{text "CKSim ty ty"}\\ + \isacommand{and}~@{text "ty ="}\\ + \phantom{$|$}~@{text "TVar tvar"}~$|$~@{text "T string"}~$|$~@{text "TApp ty ty"}\\ + $|$~@{text "TFun string ty_list"}~% + $|$~@{text "TAll tv::tvar tkind ty::ty"} \isacommand{bind}~@{text "tv"}~\isacommand{in}~@{text ty}\\ + $|$~@{text "TArr ckind ty"}\\ + \isacommand{and}~@{text "ty_lst ="}\\ + \phantom{$|$}~@{text "TNil"}~$|$~@{text "TCons ty ty_lst"}\\ + \isacommand{and}~@{text "cty ="}\\ + \phantom{$|$}~@{text "CVar cvar"}~% + $|$~@{text "C string"}~$|$~@{text "CApp cty cty"}~$|$~@{text "CFun string co_lst"}\\ + $|$~@{text "CAll cv::cvar ckind cty::cty"} \isacommand{bind}~@{text "cv"}~\isacommand{in}~@{text cty}\\ + $|$~@{text "CArr ckind cty"}~$|$~@{text "CRefl ty"}~$|$~@{text "CSym cty"}~$|$~@{text "CCirc cty cty"}\\ + $|$~@{text "CAt cty ty"}~$|$~@{text "CLeft cty"}~$|$~@{text "CRight cty"}~$|$~@{text "CSim cty cty"}\\ + $|$~@{text "CRightc cty"}~$|$~@{text "CLeftc cty"}~$|$~@{text "Coerce cty cty"}\\ + \isacommand{and}~@{text "co_lst ="}\\ + \phantom{$|$}@{text "CNil"}~$|$~@{text "CCons cty co_lst"}\\ + \isacommand{and}~@{text "trm ="}\\ + \phantom{$|$}~@{text "Var var"}~$|$~@{text "K string"}\\ + $|$~@{text "LAM_ty tv::tvar tkind t::trm"} \isacommand{bind}~@{text "tv"}~\isacommand{in}~@{text t}\\ + $|$~@{text "LAM_cty cv::cvar ckind t::trm"} \isacommand{bind}~@{text "cv"}~\isacommand{in}~@{text t}\\ + $|$~@{text "App_ty trm ty"}~$|$~@{text "App_cty trm cty"}~$|$~@{text "App trm trm"}\\ + $|$~@{text "Lam v::var ty t::trm"} \isacommand{bind}~@{text "v"}~\isacommand{in}~@{text t}\\ + $|$~@{text "Let x::var ty trm t::trm"} \isacommand{bind}~@{text x}~\isacommand{in}~@{text t}\\ + $|$~@{text "Case trm assoc_lst"}~$|$~@{text "Cast trm co"}\\ + \isacommand{and}~@{text "assoc_lst ="}\\ + \phantom{$|$}~@{text ANil}~% + $|$~@{text "ACons p::pat t::trm assoc_lst"} \isacommand{bind}~@{text "bv p"}~\isacommand{in}~@{text t}\\ + \isacommand{and}~@{text "pat ="}\\ + \phantom{$|$}~@{text "Kpat string tvtk_lst tvck_lst vt_lst"}\\ + \isacommand{and}~@{text "vt_lst ="}\\ + \phantom{$|$}~@{text VTNil}~$|$~@{text "VTCons var ty vt_lst"}\\ + \isacommand{and}~@{text "tvtk_lst ="}\\ + \phantom{$|$}~@{text TVTKNil}~$|$~@{text "TVTKCons tvar tkind tvtk_lst"}\\ + \isacommand{and}~@{text "tvck_lst ="}\\ + \phantom{$|$}~@{text TVCKNil}~$|$ @{text "TVCKCons cvar ckind tvck_lst"}\\ + \isacommand{binder}\\ + @{text "bv :: pat \ atom list"}~\isacommand{and}~% + @{text "bv1 :: vt_lst \ atom list"}~\isacommand{and}\\ + @{text "bv2 :: tvtk_lst \ atom list"}~\isacommand{and}~% + @{text "bv3 :: tvck_lst \ atom list"}\\ + \isacommand{where}\\ + \phantom{$|$}~@{text "bv (K s tvts tvcs vs) = (bv3 tvts) @ (bv2 tvcs) @ (bv1 vs)"}\\ + $|$~@{text "bv1 VTNil = []"}\\ + $|$~@{text "bv1 (VTCons x ty tl) = (atom x)::(bv1 tl)"}\\ + $|$~@{text "bv2 TVTKNil = []"}\\ + $|$~@{text "bv2 (TVTKCons a ty tl) = (atom a)::(bv2 tl)"}\\ + $|$~@{text "bv3 TVCKNil = []"}\\ + $|$~@{text "bv3 (TVCKCons c cty tl) = (atom c)::(bv3 tl)"}\\ + \end{tabular} + \end{boxedminipage} + \caption{The nominal datatype declaration for Core-Haskell. At the moment we + do not support nested types; therefore we explicitly have to unfold the + lists @{text "co_lst"}, @{text "assoc_lst"} and so on. This will be improved + in a future version of Nominal Isabelle. 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. + \label{nominalcorehas}} + \end{figure} +*} - With the above equations we can substitute free variables for support in - the lifted free variable equations, which gives us the support equations - for the term constructors. With this we can show that for each binding in - a constructors the bindings can be renamed. To rename a shallow binder - or a deep recursive binder a permutation is sufficient. This is not the - case for a deep non-recursive bindings. Take the term - @{text "Let (ACons x (Vr x) ANil) (Vr x)"}, representing the language construct - @{text "let x = x in x"}. To rename the binder the permutation cannot - be applied to the whole assignment since it would rename the free @{term "x"} - as well. To avoid this we introduce a new construction operation - that applies a permutation under a binding function. - -*} section {* Strong Induction Principles *} @@ -1808,83 +1876,8 @@ } \end{equation} - - *} -text {* - - \begin{figure}[t!] - \begin{boxedminipage}{\linewidth} - \small - \begin{tabular}{l} - \isacommand{atom\_decl}~@{text "var"}\\ - \isacommand{atom\_decl}~@{text "cvar"}\\ - \isacommand{atom\_decl}~@{text "tvar"}\\[1mm] - \isacommand{nominal\_datatype}~@{text "tkind ="}\\ - \phantom{$|$}~@{text "KStar"}~$|$~@{text "KFun tkind tkind"}\\ - \isacommand{and}~@{text "ckind ="}\\ - \phantom{$|$}~@{text "CKSim ty ty"}\\ - \isacommand{and}~@{text "ty ="}\\ - \phantom{$|$}~@{text "TVar tvar"}~$|$~@{text "T string"}~$|$~@{text "TApp ty ty"}\\ - $|$~@{text "TFun string ty_list"}~% - $|$~@{text "TAll tv::tvar tkind ty::ty"} \isacommand{bind}~@{text "tv"}~\isacommand{in}~@{text ty}\\ - $|$~@{text "TArr ckind ty"}\\ - \isacommand{and}~@{text "ty_lst ="}\\ - \phantom{$|$}~@{text "TNil"}~$|$~@{text "TCons ty ty_lst"}\\ - \isacommand{and}~@{text "cty ="}\\ - \phantom{$|$}~@{text "CVar cvar"}~% - $|$~@{text "C string"}~$|$~@{text "CApp cty cty"}~$|$~@{text "CFun string co_lst"}\\ - $|$~@{text "CAll cv::cvar ckind cty::cty"} \isacommand{bind}~@{text "cv"}~\isacommand{in}~@{text cty}\\ - $|$~@{text "CArr ckind cty"}~$|$~@{text "CRefl ty"}~$|$~@{text "CSym cty"}~$|$~@{text "CCirc cty cty"}\\ - $|$~@{text "CAt cty ty"}~$|$~@{text "CLeft cty"}~$|$~@{text "CRight cty"}~$|$~@{text "CSim cty cty"}\\ - $|$~@{text "CRightc cty"}~$|$~@{text "CLeftc cty"}~$|$~@{text "Coerce cty cty"}\\ - \isacommand{and}~@{text "co_lst ="}\\ - \phantom{$|$}@{text "CNil"}~$|$~@{text "CCons cty co_lst"}\\ - \isacommand{and}~@{text "trm ="}\\ - \phantom{$|$}~@{text "Var var"}~$|$~@{text "K string"}\\ - $|$~@{text "LAM_ty tv::tvar tkind t::trm"} \isacommand{bind}~@{text "tv"}~\isacommand{in}~@{text t}\\ - $|$~@{text "LAM_cty cv::cvar ckind t::trm"} \isacommand{bind}~@{text "cv"}~\isacommand{in}~@{text t}\\ - $|$~@{text "App_ty trm ty"}~$|$~@{text "App_cty trm cty"}~$|$~@{text "App trm trm"}\\ - $|$~@{text "Lam v::var ty t::trm"} \isacommand{bind}~@{text "v"}~\isacommand{in}~@{text t}\\ - $|$~@{text "Let x::var ty trm t::trm"} \isacommand{bind}~@{text x}~\isacommand{in}~@{text t}\\ - $|$~@{text "Case trm assoc_lst"}~$|$~@{text "Cast trm co"}\\ - \isacommand{and}~@{text "assoc_lst ="}\\ - \phantom{$|$}~@{text ANil}~% - $|$~@{text "ACons p::pat t::trm assoc_lst"} \isacommand{bind}~@{text "bv p"}~\isacommand{in}~@{text t}\\ - \isacommand{and}~@{text "pat ="}\\ - \phantom{$|$}~@{text "Kpat string tvtk_lst tvck_lst vt_lst"}\\ - \isacommand{and}~@{text "vt_lst ="}\\ - \phantom{$|$}~@{text VTNil}~$|$~@{text "VTCons var ty vt_lst"}\\ - \isacommand{and}~@{text "tvtk_lst ="}\\ - \phantom{$|$}~@{text TVTKNil}~$|$~@{text "TVTKCons tvar tkind tvtk_lst"}\\ - \isacommand{and}~@{text "tvck_lst ="}\\ - \phantom{$|$}~@{text TVCKNil}~$|$ @{text "TVCKCons cvar ckind tvck_lst"}\\ - \isacommand{binder}\\ - @{text "bv :: pat \ atom list"}~\isacommand{and}~% - @{text "bv1 :: vt_lst \ atom list"}~\isacommand{and}\\ - @{text "bv2 :: tvtk_lst \ atom list"}~\isacommand{and}~% - @{text "bv3 :: tvck_lst \ atom list"}\\ - \isacommand{where}\\ - \phantom{$|$}~@{text "bv (K s tvts tvcs vs) = (bv3 tvts) @ (bv2 tvcs) @ (bv1 vs)"}\\ - $|$~@{text "bv1 VTNil = []"}\\ - $|$~@{text "bv1 (VTCons x ty tl) = (atom x)::(bv1 tl)"}\\ - $|$~@{text "bv2 TVTKNil = []"}\\ - $|$~@{text "bv2 (TVTKCons a ty tl) = (atom a)::(bv2 tl)"}\\ - $|$~@{text "bv3 TVCKNil = []"}\\ - $|$~@{text "bv3 (TVCKCons c cty tl) = (atom c)::(bv3 tl)"}\\ - \end{tabular} - \end{boxedminipage} - \caption{The nominal datatype declaration for Core-Haskell. At the moment we - do not support nested types; therefore we explicitly have to unfold the - lists @{text "co_lst"}, @{text "assoc_lst"} and so on. This will be improved - in a future version of Nominal Isabelle. 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. - \label{nominalcorehas}} - \end{figure} -*} section {* Related Work *}