# HG changeset patch # User Christian Urban # Date 1315483399 -3600 # Node ID c6af56de923debfc7d497d5a81b06f50604c5438 # Parent 02d98590454da6a39f08d0bb053ad8c641c26f22 more on paper diff -r 02d98590454d -r c6af56de923d LMCS-Paper/Paper.thy --- a/LMCS-Paper/Paper.thy Thu Sep 08 11:21:03 2011 +0100 +++ b/LMCS-Paper/Paper.thy Thu Sep 08 13:03:19 2011 +0100 @@ -202,7 +202,7 @@ \mbox{\begin{tabular}{r@ {\hspace{2mm}}r@ {\hspace{2mm}}ll} @{text trm} & @{text "::="} & @{text "\"} \\ & @{text "|"} & @{text "\ as::assn s::trm"}\hspace{2mm} - \isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text "s"}\\[1mm] + \isacommand{binds} @{text "bn(as)"} \isacommand{in} @{text "s"}\\[1mm] @{text assn} & @{text "::="} & @{text "\"}\\ & @{text "|"} & @{text "\ name trm assn"} \end{tabular}} @@ -222,7 +222,7 @@ \noindent The scope of the binding is indicated by labels given to the types, for example @{text "s::trm"}, and a binding clause, in this case - \isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text "s"}. This binding + \isacommand{binds} @{text "bn(as)"} \isacommand{in} @{text "s"}. This binding clause states that all the names the function @{text "bn(as)"} returns should be bound in @{text s}. This style of specifying terms and bindings is heavily inspired by the syntax of the Ott-tool \cite{ott-jfp}. Our work @@ -517,7 +517,7 @@ described, for example for atoms, products, lists, function applications, booleans and permutations as follows - \[\mbox{ + \begin{equation}\label{supps}\mbox{ \begin{tabular}{c@ {\hspace{10mm}}c} \begin{tabular}{rcl} @{term "supp a"} & $=$ & @{term "{a}"}\\ @@ -532,7 +532,7 @@ @{term "supp \"} & $=$ & @{term "{a. \ \ a \ a}"} \end{tabular} \end{tabular}} - \]\smallskip + \end{equation}\smallskip \noindent in some cases it can be difficult to characterise the support precisely, and @@ -613,8 +613,10 @@ in the support of @{text x} (that is @{term "supp x \* \"}). The last fact and Property~\ref{supppermeq} allow us to ``rename'' just the binders @{text as} in @{text x}, because @{term "\ \ x = x"}. Note that @{term "supp x \* \"} - is equivalent with @{term "supp \ \* x"}, which means we could also use the other - `direction' in Propositions \ref{supppermeq} and \ref{avoiding}. + is equivalent with @{term "supp \ \* x"}, which means we could also formulate + 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 original formulation. Most properties given in this section are described in detail in \cite{HuffmanUrban10} and all are formalised in Isabelle/HOL. In the next sections we will make @@ -753,9 +755,6 @@ \begin{lem}\label{alphaeq} The relations $\approx_{\,\textit{abs\_set}}$, $\approx_{\,\textit{abs\_list}}$ and $\approx_{\,\textit{abs\_set+}}$ are equivalence relations and equivariant. - %, and if - %@{term "abs_set (as, x) (bs, y)"} then also - %@{term "abs_set (p \ as, p \ x) (p \ bs, p \ y)"} (similarly for the other two relations). \end{lem} \begin{proof} @@ -763,9 +762,11 @@ a permutation @{text "\"} and for the proof obligation take @{term "- \"}. In case of transitivity, we have two permutations @{text "\\<^isub>1"} and @{text "\\<^isub>2"}, and for the proof obligation use @{text "\\<^isub>1 + \\<^isub>2"}. Equivariance means - @{term "abs_set (p \ as, p \ x) (p \ bs, p \ y)"} holds provided - @{term "abs_set (as, x) (bs, y)"}. - + @{term "abs_set (\ \ as, \ \ x) (\ \ bs, \ \ y)"} holds provided + @{term "abs_set (as, x) (bs, y)"}. To show this, we need to unfold the + definitions and `pull out' the permutations, which is possible since all + operators, such as @{text "#\<^sup>*, -, set"} and @{text "supp"}, are equivariant + (see \cite{HuffmanUrban10}). \end{proof} \noindent @@ -802,13 +803,14 @@ \end{thm} \noindent - This theorem states that the bound names do not appear in the support. - Below we will show the first equation. The others follow by similar + In effect, this theorem states that the bound names do not appear in the support + of abstractions. This can be seen as test that our Definitions \ref{alphaset}, \ref{alphalist} + and \ref{alphares} capture the idea of alpha-equivalence relations. + Below we will show the first equation of Theorem \ref{suppabs}. The others follow by similar arguments. By definition of the abstraction type @{text "abs\<^bsub>set\<^esub>"} we have - \begin{equation}\label{abseqiff} - @{thm (lhs) Abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]} \;\;\text{if and only if}\;\; + @{thm (lhs) Abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]} \;\;\;\text{if and only if}\;\;\; @{term "\\. alpha_set (as, x) equal supp \ (bs, y)"} \end{equation}\smallskip @@ -826,13 +828,14 @@ the following lemma about swapping two atoms in an abstraction. \begin{lem} - @{thm[mode=IfThen] Abs_swap1(1)[where bs="as", no_vars]} + If @{thm (prem 1) Abs_swap1(1)[where bs="as", no_vars]} and + @{thm (prem 2) Abs_swap1(1)[where bs="as", no_vars]} then + @{thm (concl) Abs_swap1(1)[where bs="as", no_vars]} \end{lem} \begin{proof} This lemma is straightforward using \eqref{abseqiff} and observing that the assumptions give us @{term "(a \ b) \ (supp x - as) = (supp x - as)"}. - Moreover @{text supp} and set difference are equivariant (see \cite{HuffmanUrban10}). \end{proof} \noindent @@ -841,45 +844,48 @@ \begin{equation}\label{halfone} @{thm Abs_supports(1)[no_vars]} - \end{equation} + \end{equation}\smallskip \noindent which by Property~\ref{supportsprop} gives us ``one half'' of Theorem~\ref{suppabs}. The ``other half'' is a bit more involved. To establish it, we use a trick from \cite{Pitts04} and first define an auxiliary - function @{text aux}, taking an abstraction as argument: - @{thm supp_set.simps[THEN eq_reflection, no_vars]}. - + function @{text aux}, taking an abstraction as argument + + \[ + @{thm supp_set.simps[THEN eq_reflection, no_vars]} + \]\smallskip + + \noindent Using the second equation in \eqref{equivariance}, we can show that - @{text "aux"} is equivariant (since @{term "p \ (supp x - as) = (supp (p \ x)) - (p \ as)"}) + @{text "aux"} is equivariant (since @{term "\ \ (supp x - as) = (supp (\ \ x)) - (\ \ as)"}) and therefore has empty support. This in turn means - \begin{center} - @{term "supp (supp_gen (Abs_set as x)) \ supp (Abs_set as x)"} - \end{center} + \[ + @{term "supp (supp_set (Abs_set as x)) \ supp (Abs_set as x)"} + \]\smallskip \noindent - using \eqref{suppfun}. Assuming @{term "supp x - as"} is a finite set, - we further obtain + using fact about function applications in \eqref{supps}. Assuming + @{term "supp x - as"} is a finite set, we further obtain \begin{equation}\label{halftwo} @{thm (concl) Abs_supp_subset1(1)[no_vars]} - \end{equation} + \end{equation}\smallskip \noindent - since for finite sets of atoms, @{text "bs"}, we have + since for every finite sets of atoms, say @{text "bs"}, we have @{thm (concl) supp_finite_atom_set[where S="bs", no_vars]}. Finally, taking \eqref{halfone} and \eqref{halftwo} together establishes Theorem~\ref{suppabs}. - 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 Isabelle/HOL level - properties about them. It would be - laborious to write custom ML-code that derives automatically such properties - for every term-constructor that binds some atoms. Also the generality of - the definitions for alpha-equivalence will help us in the next sections. + 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 + Isabelle/HOL level properties about them. It would be extremely laborious + to write custom ML-code that derives automatically such properties for every + term-constructor that binds some atoms. Also the generality of the + definitions for alpha-equivalence will help us in the next sections. *} section {* Specifying General Bindings\label{sec:spec} *} @@ -914,129 +920,124 @@ \end{tabular}} \end{cases}$\\ \end{tabular}} - \end{equation} + \end{equation}\smallskip \noindent - Every type declaration @{text ty}$^\alpha_{1..n}$ consists of a collection of - term-constructors, each of which comes with a list of labelled - types that stand for the types of the arguments of the term-constructor. - For example a term-constructor @{text "C\<^sup>\"} might be specified with + Every type declaration @{text ty}$^\alpha_{1..n}$ consists of a collection + of term-constructors, each of which comes with a list of labelled types that + stand for the types of the arguments of the term-constructor. For example a + term-constructor @{text "C\<^sup>\"} might be specified with - \begin{center} - @{text "C\<^sup>\ label\<^isub>1::ty"}$'_1$ @{text "\ label\<^isub>l::ty"}$'_l\;\;$ @{text "binding_clauses"} - \end{center} + \[ + @{text "C\<^sup>\ label\<^isub>1::ty"}\mbox{$'_1$} @{text "\ label\<^isub>l::ty"}\mbox{$'_l\;\;$} @{text "binding_clauses"} + \]\smallskip + + \noindent + whereby some of the @{text ty}$'_{1..l}$ (or their components) can be + contained in the collection of @{text ty}$^\alpha_{1..n}$ declared in + \eqref{scheme}. In this case we will call the corresponding argument a + \emph{recursive argument} of @{text "C\<^sup>\"}. The types of such + recursive arguments need to satisfy a ``positivity'' restriction, which + ensures that the type has a set-theoretic semantics (see + \cite{Berghofer99}). The labels annotated on the types are optional. Their + purpose is to be used in the (possibly empty) list of \emph{binding + clauses}, which indicate the binders and their scope in a term-constructor. + They come in three \emph{modes}: + + + \[\mbox{ + \begin{tabular}{@ {}l@ {}} + \isacommand{binds} {\it binders} \isacommand{in} {\it bodies}\\ + \isacommand{binds (set)} {\it binders} \isacommand{in} {\it bodies}\\ + \isacommand{binds (set+)} {\it binders} \isacommand{in} {\it bodies} + \end{tabular}} + \]\smallskip \noindent - whereby some of the @{text ty}$'_{1..l}$ (or their components) - can be contained - in the collection of @{text ty}$^\alpha_{1..n}$ declared in - \eqref{scheme}. - In this case we will call the corresponding argument a - \emph{recursive argument} of @{text "C\<^sup>\"}. - The types of such recursive - arguments need to satisfy a ``positivity'' - restriction, which ensures that the type has a set-theoretic semantics - \cite{Berghofer99}. - The labels - annotated on the types are optional. Their purpose is to be used in the - (possibly empty) list of \emph{binding clauses}, which indicate the binders - and their scope in a term-constructor. They come in three \emph{modes}: - % - \begin{center} - \begin{tabular}{@ {}l@ {}} - \isacommand{bind} {\it binders} \isacommand{in} {\it bodies}\;\;\;\, - \isacommand{bind (set)} {\it binders} \isacommand{in} {\it bodies}\;\;\;\, - \isacommand{bind (set+)} {\it binders} \isacommand{in} {\it bodies} - \end{tabular} - \end{center} - % - \noindent - The first mode is for binding lists of atoms (the order of binders matters); - the second is for sets of binders (the order does not matter, but the - cardinality does) and the last is for sets of binders (with vacuous binders - preserving alpha-equivalence). As indicated, the labels in the ``\isacommand{in}-part'' of a binding - clause will be called \emph{bodies}; the - ``\isacommand{bind}-part'' will be called \emph{binders}. In contrast to - Ott, we allow multiple labels in binders and bodies. - - For example we allow + The first mode is for binding lists of atoms (the order of bound atoms + matters); the second is for sets of binders (the order does not matter, but + the cardinality does) and the last is for sets of binders (with vacuous + binders preserving alpha-equivalence). As indicated, the labels in the + ``\isacommand{in}-part'' of a binding clause will be called \emph{bodies}; + the ``\isacommand{binds}-part'' will be called \emph{binders}. In contrast to + Ott, we allow multiple labels in binders and bodies. For example we allow binding clauses of the form: - - \begin{center} + + \[\mbox{ \begin{tabular}{@ {}ll@ {}} @{text "Foo\<^isub>1 x::name y::name t::trm s::trm"} & - \isacommand{bind} @{text "x y"} \isacommand{in} @{text "t s"}\\ + \isacommand{binds} @{text "x y"} \isacommand{in} @{text "t s"}\\ @{text "Foo\<^isub>2 x::name y::name t::trm s::trm"} & - \isacommand{bind} @{text "x y"} \isacommand{in} @{text "t"}, - \isacommand{bind} @{text "x y"} \isacommand{in} @{text "s"}\\ - \end{tabular} - \end{center} + \isacommand{binds} @{text "x y"} \isacommand{in} @{text "t"}, + \isacommand{binds} @{text "x y"} \isacommand{in} @{text "s"}\\ + \end{tabular}} + \]\smallskip \noindent - Similarly for the other binding modes. - Interestingly, in case of \isacommand{bind (set)} - and \isacommand{bind (set+)} the binding clauses above will make a difference to the semantics - of the specifications (the corresponding alpha-equivalence will differ). We will - show this later with an example. + Similarly for the other binding modes. Interestingly, in case of + \isacommand{binds (set)} and \isacommand{binds (set+)} the binding clauses + above will make a difference to the semantics of the specifications (the + corresponding alpha-equivalence will differ). We will show this later with + an example. + - There are also some restrictions we need to impose on our binding clauses in comparison to - the ones of Ott. The - main idea behind these restrictions is that we obtain a sensible notion of - alpha-equivalence where it is ensured that within a given scope an - atom occurrence cannot be both bound and free at the same time. The first - restriction is that a body can only occur in + There are also some restrictions we need to impose on our binding clauses in + comparison to the ones of Ott. The main idea behind these restrictions is + that we obtain a sensible notion of alpha-equivalence where it is ensured + that within a given scope an atom occurrence cannot be both bound and free + at the same time. The first restriction is that a body can only occur in \emph{one} binding clause of a term constructor (this ensures that the bound - atoms of a body cannot be free at the same time by specifying an - alternative binder for the same body). + atoms of a body cannot be free at the same time by specifying an alternative + binder for the same body). - For binders we distinguish between - \emph{shallow} and \emph{deep} binders. Shallow binders are just - labels. The restriction we need to impose on them is that in case of - \isacommand{bind (set)} and \isacommand{bind (set+)} the labels must either - refer to atom types or to sets of atom types; in case of \isacommand{bind} - the labels must refer to atom types or lists of atom types. Two examples for - the use of shallow binders are the specification of lambda-terms, where a - single name is bound, and type-schemes, where a finite set of names is - bound: + For binders we distinguish between \emph{shallow} and \emph{deep} binders. + Shallow binders are just labels. The restriction we need to impose on them + is that in case of \isacommand{binds (set)} and \isacommand{binds (set+)} the + labels must either refer to atom types or to sets of atom types; in case of + \isacommand{binds} the labels must refer to atom types or lists of atom + types. Two examples for the use of shallow binders are the specification of + lambda-terms, where a single name is bound, and type-schemes, where a finite + set of names is bound: - \begin{center} - \begin{tabular}{@ {}c@ {\hspace{7mm}}c@ {}} + \[\mbox{ + \begin{tabular}{@ {}c@ {\hspace{5mm}}c@ {}} \begin{tabular}{@ {}l} \isacommand{nominal\_datatype} @{text lam} $=$\\ \hspace{2mm}\phantom{$\mid$}~@{text "Var name"}\\ \hspace{2mm}$\mid$~@{text "App lam lam"}\\ - \hspace{2mm}$\mid$~@{text "Lam x::name t::lam"}~~\isacommand{bind} @{text x} \isacommand{in} @{text t}\\ + \hspace{2mm}$\mid$~@{text "Lam x::name t::lam"}\hspace{3mm}% + \isacommand{binds} @{text x} \isacommand{in} @{text t}\\ \end{tabular} & \begin{tabular}{@ {}l@ {}} \isacommand{nominal\_datatype}~@{text ty} $=$\\ \hspace{5mm}\phantom{$\mid$}~@{text "TVar name"}\\ \hspace{5mm}$\mid$~@{text "TFun ty ty"}\\ - \isacommand{and}~@{text "tsc = All xs::(name fset) T::ty"}~~% - \isacommand{bind (set+)} @{text xs} \isacommand{in} @{text T}\\ + \isacommand{and}~@{text "tsc = All xs::(name fset) T::ty"}\hspace{3mm}% + \isacommand{binds (set+)} @{text xs} \isacommand{in} @{text T}\\ \end{tabular} - \end{tabular} - \end{center} + \end{tabular}} + \]\smallskip + \noindent In these specifications @{text "name"} refers to an atom type, and @{text - "fset"} to the type of finite sets. - Note that for @{text lam} it does not matter which binding mode we use. The - reason is that we bind only a single @{text name}. However, having - \isacommand{bind (set)} or \isacommand{bind} in the second case makes a - difference to the semantics of the specification (which we will define in the next section). - + "fset"} to the type of finite sets. Note that for @{text lam} it does not + matter which binding mode we use. The reason is that we bind only a single + @{text name}. However, having \isacommand{binds (set)} or \isacommand{binds} + in the second case makes a difference to the semantics of the specification + (which we will define in the next section). A \emph{deep} binder uses an auxiliary binding function that ``picks'' out the atoms in one argument of the term-constructor, which can be bound in other arguments and also in the same argument (we will call such binders \emph{recursive}, see below). The binding functions are - expected to return either a set of atoms (for \isacommand{bind (set)} and - \isacommand{bind (set+)}) or a list of atoms (for \isacommand{bind}). They can - be defined by recursion over the corresponding type; the equations + expected to return either a set of atoms (for \isacommand{binds (set)} and + \isacommand{binds (set+)}) or a list of atoms (for \isacommand{binds}). They need + to be defined by recursion over the corresponding type; the equations must be given in the binding function part of the scheme shown in \eqref{scheme}. For example a term-calculus containing @{text "Let"}s with tuple patterns might be specified as: - % + \begin{equation}\label{letpat} \mbox{% \begin{tabular}{l} @@ -1044,20 +1045,20 @@ \hspace{5mm}\phantom{$\mid$}~@{term "Var name"}\\ \hspace{5mm}$\mid$~@{term "App trm trm"}\\ \hspace{5mm}$\mid$~@{text "Lam x::name t::trm"} - \;\;\isacommand{bind} @{text x} \isacommand{in} @{text t}\\ + \;\;\isacommand{binds} @{text x} \isacommand{in} @{text t}\\ \hspace{5mm}$\mid$~@{text "Let p::pat trm t::trm"} - \;\;\isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text t}\\ - \isacommand{and} @{text pat} $=$ - @{text PNil} - $\mid$~@{text "PVar name"} - $\mid$~@{text "PTup pat pat"}\\ + \;\;\isacommand{binds} @{text "bn(p)"} \isacommand{in} @{text t}\\ + \isacommand{and} @{text pat} $=$\\ + \hspace{5mm}\phantom{$\mid$}~@{text PNil}\\ + \hspace{5mm}$\mid$~@{text "PVar name"}\\ + \hspace{5mm}$\mid$~@{text "PTup pat pat"}\\ \isacommand{binder}~@{text "bn::pat \ atom list"}\\ \isacommand{where}~@{text "bn(PNil) = []"}\\ \hspace{5mm}$\mid$~@{text "bn(PVar x) = [atom x]"}\\ \hspace{5mm}$\mid$~@{text "bn(PTup p\<^isub>1 p\<^isub>2) = bn(p\<^isub>1) @ bn(p\<^isub>2)"}\smallskip\\ \end{tabular}} - \end{equation} - % + \end{equation}\smallskip + \noindent In this specification the function @{text "bn"} determines which atoms of the pattern @{text p} are bound in the argument @{text "t"}. Note that in the @@ -1067,36 +1068,37 @@ As said above, for deep binders we allow binding clauses such as - \begin{center} + \[\mbox{ \begin{tabular}{ll} @{text "Bar p::pat t::trm"} & - \isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text "p t"} \\ - \end{tabular} - \end{center} + \isacommand{binds} @{text "bn(p)"} \isacommand{in} @{text "p t"} \\ + \end{tabular}} + \]\smallskip + \noindent where the argument of the deep binder also occurs in the body. We call such binders \emph{recursive}. To see the purpose of such recursive binders, compare ``plain'' @{text "Let"}s and @{text "Let_rec"}s in the following specification: - % + \begin{equation}\label{letrecs} \mbox{% \begin{tabular}{@ {}l@ {}} \isacommand{nominal\_datatype}~@{text "trm ="}~\ldots\\ \hspace{5mm}$\mid$~@{text "Let as::assn t::trm"} - \;\;\isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text t}\\ + \;\;\isacommand{binds} @{text "bn(as)"} \isacommand{in} @{text t}\\ \hspace{5mm}$\mid$~@{text "Let_rec as::assn t::trm"} - \;\;\isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text "as t"}\\ - \isacommand{and} @{text "assn"} $=$ - @{text "ANil"} - $\mid$~@{text "ACons name trm assn"}\\ + \;\;\isacommand{binds} @{text "bn(as)"} \isacommand{in} @{text "as t"}\\ + \isacommand{and} @{text "assn"} $=$\\ + \hspace{5mm}\phantom{$\mid$}~@{text "ANil"}\\ + \hspace{5mm}$\mid$~@{text "ACons name trm assn"}\\ \isacommand{binder} @{text "bn::assn \ atom list"}\\ \isacommand{where}~@{text "bn(ANil) = []"}\\ \hspace{5mm}$\mid$~@{text "bn(ACons a t as) = [atom a] @ bn(as)"}\\ \end{tabular}} - \end{equation} - % + \end{equation}\smallskip + \noindent The difference is that with @{text Let} we only want to bind the atoms @{text "bn(as)"} in the term @{text t}, but with @{text "Let_rec"} we also want to bind the atoms @@ -1110,10 +1112,10 @@ \begin{center} \begin{tabular}{@ {}l@ {\hspace{2mm}}l@ {}} @{text "Baz\<^isub>1 p::pat t::trm"} & - \isacommand{bind} @{text "bn\<^isub>1(p) bn\<^isub>2(p)"} \isacommand{in} @{text t}\\ + \isacommand{binds} @{text "bn\<^isub>1(p) bn\<^isub>2(p)"} \isacommand{in} @{text t}\\ @{text "Baz\<^isub>2 p::pat t\<^isub>1::trm t\<^isub>2::trm"} & - \isacommand{bind} @{text "bn\<^isub>1(p)"} \isacommand{in} @{text "t\<^isub>1"}, - \isacommand{bind} @{text "bn\<^isub>2(p)"} \isacommand{in} @{text "t\<^isub>2"}\\ + \isacommand{binds} @{text "bn\<^isub>1(p)"} \isacommand{in} @{text "t\<^isub>1"}, + \isacommand{binds} @{text "bn\<^isub>2(p)"} \isacommand{in} @{text "t\<^isub>2"}\\ \end{tabular} \end{center} @@ -1147,18 +1149,18 @@ of term-calculi are implicitly \emph{completed}. By this we mean that for every argument of a term-constructor that is \emph{not} already part of a binding clause given by the user, we add implicitly a special \emph{empty} binding - clause, written \isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "labels"}. In case + clause, written \isacommand{binds}~@{term "{}"}~\isacommand{in}~@{text "labels"}. In case of the lambda-terms, the completion produces \begin{center} \begin{tabular}{@ {}l@ {\hspace{-1mm}}} \isacommand{nominal\_datatype} @{text lam} =\\ \hspace{5mm}\phantom{$\mid$}~@{text "Var x::name"} - \;\;\isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "x"}\\ + \;\;\isacommand{binds}~@{term "{}"}~\isacommand{in}~@{text "x"}\\ \hspace{5mm}$\mid$~@{text "App t\<^isub>1::lam t\<^isub>2::lam"} - \;\;\isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "t\<^isub>1 t\<^isub>2"}\\ + \;\;\isacommand{binds}~@{term "{}"}~\isacommand{in}~@{text "t\<^isub>1 t\<^isub>2"}\\ \hspace{5mm}$\mid$~@{text "Lam x::name t::lam"} - \;\;\isacommand{bind}~@{text x} \isacommand{in} @{text t}\\ + \;\;\isacommand{binds}~@{text x} \isacommand{in} @{text t}\\ \end{tabular} \end{center} @@ -1236,11 +1238,11 @@ binding clauses @{text "bc\<^isub>1\bc\<^isub>k"}, the result of @{text "fa_ty (C z\<^isub>1 \ z\<^isub>n)"} will be the union @{text "fa(bc\<^isub>1) \ \ \ fa(bc\<^isub>k)"} where we will define below what @{text "fa"} for a binding - clause means. We only show the details for the mode \isacommand{bind (set)} (the other modes are similar). + clause means. We only show the details for the mode \isacommand{binds (set)} (the other modes are similar). Suppose the binding clause @{text bc\<^isub>i} is of the form \begin{center} - \mbox{\isacommand{bind (set)} @{text "b\<^isub>1\b\<^isub>p"} \isacommand{in} @{text "d\<^isub>1\d\<^isub>q"}} + \mbox{\isacommand{binds (set)} @{text "b\<^isub>1\b\<^isub>p"} \isacommand{in} @{text "d\<^isub>1\d\<^isub>q"}} \end{center} \noindent @@ -1443,7 +1445,7 @@ empty binding clause of the form \begin{center} - \mbox{\isacommand{bind (set)} @{term "{}"} \isacommand{in} @{text "d\<^isub>1\d\<^isub>q"}.} + \mbox{\isacommand{binds (set)} @{term "{}"} \isacommand{in} @{text "d\<^isub>1\d\<^isub>q"}.} \end{center} \noindent @@ -1475,7 +1477,7 @@ Now suppose the binding clause @{text "bc\<^isub>i"} is of the general form \begin{equation}\label{nonempty} - \mbox{\isacommand{bind (set)} @{text "b\<^isub>1\b\<^isub>p"} \isacommand{in} @{text "d\<^isub>1\d\<^isub>q"}.} + \mbox{\isacommand{binds (set)} @{text "b\<^isub>1\b\<^isub>p"} \isacommand{in} @{text "d\<^isub>1\d\<^isub>q"}.} \end{equation} \noindent @@ -1842,14 +1844,14 @@ %\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 "TAll tv::tvar tkind ty::ty"} \isacommand{binds}~@{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 "CAll cv::cvar ckind cty::cty"} \isacommand{binds}~@{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"}\\ @@ -1857,15 +1859,15 @@ %\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 "LAM_ty tv::tvar tkind t::trm"} \isacommand{binds}~@{text "tv"}~\isacommand{in}~@{text t}\\ + %$|$~@{text "LAM_cty cv::cvar ckind t::trm"} \isacommand{binds}~@{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 "Lam v::var ty t::trm"} \isacommand{binds}~@{text "v"}~\isacommand{in}~@{text t}\\ + %$|$~@{text "Let x::var ty trm t::trm"} \isacommand{binds}~@{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}\\ + %$|$~@{text "ACons p::pat t::trm assoc_lst"} \isacommand{binds}~@{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 ="}\\ @@ -2250,18 +2252,18 @@ meaning in a HOL-based theorem prover. We also had to generalise slightly Ott's binding clauses. In Ott you specify binding clauses with a single body; we allow more than one. We have to do this, because this makes a difference - for our notion of alpha-equivalence in case of \isacommand{bind (set)} and - \isacommand{bind (set+)}. + for our notion of alpha-equivalence in case of \isacommand{binds (set)} and + \isacommand{binds (set+)}. Consider the examples \begin{center} \begin{tabular}{@ {}l@ {\hspace{2mm}}l@ {}} @{text "Foo\<^isub>1 xs::name fset t::trm s::trm"} & - \isacommand{bind (set)} @{text "xs"} \isacommand{in} @{text "t s"}\\ + \isacommand{binds (set)} @{text "xs"} \isacommand{in} @{text "t s"}\\ @{text "Foo\<^isub>2 xs::name fset t::trm s::trm"} & - \isacommand{bind (set)} @{text "xs"} \isacommand{in} @{text "t"}, - \isacommand{bind (set)} @{text "xs"} \isacommand{in} @{text "s"}\\ + \isacommand{binds (set)} @{text "xs"} \isacommand{in} @{text "t"}, + \isacommand{binds (set)} @{text "xs"} \isacommand{in} @{text "s"}\\ \end{tabular} \end{center} @@ -2296,7 +2298,7 @@ can be specified using special markers, written @{text "inner"} and @{text "outer"}. It seems our and his specifications can be inter-translated as long as ours use the binding mode - \isacommand{bind} only. + \isacommand{binds} only. However, we have not proved this. Pottier gives a definition for alpha-equivalence, which also uses a permutation operation (like ours). Still, this definition is rather different from ours and he only proves that @@ -2306,7 +2308,7 @@ In a slightly different domain (programming with dependent types), the paper \cite{Altenkirch10} presents a calculus with a notion of - alpha-equivalence related to our binding mode \isacommand{bind (set+)}. + alpha-equivalence related to our binding mode \isacommand{binds (set+)}. The definition in \cite{Altenkirch10} is similar to the one by Pottier, except that it has a more operational flavour and calculates a partial (renaming) map. In this way, the definition can deal with vacuous binders. However, to our diff -r 02d98590454d -r c6af56de923d Nominal/Nominal2_Abs.thy --- a/Nominal/Nominal2_Abs.thy Thu Sep 08 11:21:03 2011 +0100 +++ b/Nominal/Nominal2_Abs.thy Thu Sep 08 13:03:19 2011 +0100 @@ -64,7 +64,9 @@ unfolding set_eqvt[symmetric] unfolding permute_fun_app_eq[symmetric] unfolding Diff_eqvt[symmetric] - by (auto simp add: permute_bool_def fresh_star_permute_iff) + unfolding eq_eqvt[symmetric] + unfolding fresh_star_eqvt[symmetric] + by (auto simp add: permute_bool_def) section {* Equivalence *}