nominal2: comparison Paper/Paper.thy

equal deleted inserted replaced

-:24cc3dbd3c4a
+:9e09253c80cf
 @{thm[mode=IfThen] swap_fresh_fresh[no_vars]}
 \end{property}
 While often the support of an object can be relatively easily
 described, for example for atoms, products, lists, function applications,
-booleans and permutations\\[-6mm]
+booleans and permutations as follows\\[-6mm]
 %
 \begin{eqnarray}
 @{term "supp a"} & = & @{term "{a}"}\\
 @{term "supp (x, y)"} & = & @{term "supp x \<union> supp y"}\\
 @{term "supp []"} & = & @{term "{}"}\\
 @{text "p \<bullet> (f x) = f (p \<bullet> x)"}
 \end{equation}
 \noindent
 From property \eqref{equivariancedef} and the definition of @{text supp}, we
-can be easily deduce that an equivariant function has empty support.
+can be easily deduce that equivariant functions have empty support.
 Finally, the nominal logic work provides us with convenient means to rename
 binders. While in the older version of Nominal Isabelle, we used extensively
 Property~\ref{swapfreshfresh} for renaming single binders, this property
-proved unwieldy for dealing with multiple binders. For such pinders the
+proved unwieldy for dealing with multiple binders. For such binders the
 following generalisations turned out to be easier to use.
 \begin{property}\label{supppermeq}
 @{thm[mode=IfThen] supp_perm_eq[no_vars]}
 \end{property}
 \end{array}
 \end{equation}
 \noindent
 where @{term set} is a function that coerces a list of atoms into a set of atoms.
-Now the last clause ensures that the order of the binders matters.
+Now the last clause ensures that the order of the binders matters (since @{text as}
+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, then we keep sets of binders, but drop the fourth
 condition in \eqref{alphaset}:
 %
 \end{center}
 \noindent
 indicating that a set (or list) @{text as} is abstracted in @{text x}. We will
 call the types \emph{abstraction types} and their elements
-\emph{abstractions}. The important property we need to derive the support of
+\emph{abstractions}. The important property we need to derive is the support of
 abstractions, namely:
 \begin{thm}[Support of Abstractions]\label{suppabs}
 Assuming @{text x} has finite support, then\\[-6mm]
 \begin{center}
 @{thm abs_supports(1)[no_vars]}
 \end{equation}
 \noindent
 which by Property~\ref{supportsprop} gives us ``one half'' of
-Thm~\ref{suppabs}. The ``other half'' is a bit more involved. To establish
+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:
 %
 \begin{center}
 @{thm supp_gen.simps[THEN eq_reflection, no_vars]}
 The method of first considering abstractions of the
 form @{term "Abs as x"} etc is motivated by the fact that properties about them
 can be conveninetly established at the Isabelle/HOL level.  It would be
 difficult 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 section.
+the definitions for alpha-equivalence will help us in definitions in the next section.
 *}
 section {* Alpha-Equivalence and Free Variables\label{sec:alpha} *}
 text {*
 \end{tabular}
 \end{center}
 \noindent
 In this specification the function @{text "bn"} determines which atoms of @{text  p} are
-bound in the argument @{text "t"}. Note that in the second last clause the function @{text "atom"}
+bound in the argument @{text "t"}. Note that in the second-last clause the function @{text "atom"}
 coerces a name into the generic atom type of Nominal Isabelle \cite{HuffmanUrban10}. This allows
 us to treat binders of different atom type uniformly.
 As will shortly become clear, we cannot return an atom in a binding function
 that is also bound in the corresponding term-constructor. That means in the
 \noindent
 since there is no overlap of binders.
 Note that in the last example we wrote {\it\isacommand{bind}\;bn(p)\;\isacommand{in}\;p}.
-Whenever such a binding clause is present, we will call the binder \emph{recursive}.
+Whenever such a binding clause is present, we will call the corresponding binder \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{%
 Pottier and Cheney pointed out, we cannot in general re-arrange arguments of
 term-constructors so that binders and their bodies are next to each other, and
 then use the type constructors @{text "abs_set"}, @{text "abs_res"} and
 @{text "abs_list"} from Section \ref{sec:binders}. Therefore we will first
 extract datatype definitions from the specification and then define
-independently an alpha-equivalence relation over them.
+expicitly an alpha-equivalence relation over them.
 The datatype definition can be obtained by stripping off the
 binding clauses and the labels on the types. We also have to invent
 new names for the types @{text "ty\<^sup>\<alpha>"} and term-constructors @{text "C\<^sup>\<alpha>"}
 @{text "fv_bn\<^isub>1 :: ty\<^isub>1 \<Rightarrow> atom set  \<dots>  fv_bn\<^isub>m :: ty\<^isub>m \<Rightarrow> atom set"}
 \end{center}
 \noindent
 The reason for this setup is that in a deep binder not all atoms have to be
-bound, as we shall see in an example below. We need therefore the function
+bound, as we shall see in an example below. We need therefore a function
 that calculates those unbound atoms.
 While the idea behind these
 free-variable functions is clear (they just collect all atoms that are not bound),
-because of the rather complicated binding mechanisms their definitions are
+because of our rather complicated binding mechanisms their definitions are
 somewhat involved.
 Given a term-constructor @{text "C"} of type @{text ty} with argument types
 \mbox{@{text "ty\<^isub>1 \<dots> ty\<^isub>n"}}, the function
 @{text "fv_ty (C x\<^isub>1 \<dots> x\<^isub>n)"} will be the union of the values
 calculated below for each argument.
 $\bullet$ & @{term "{}"} otherwise
 \end{tabular}}
 \end{equation}
 \noindent
-Like the coercion function @{text atom} used earlier, @{text "atoms as"} coerces
+Like the coercion function @{text atom} used earlier, @{text "atoms"} coerces
-the set @{text as} to the generic atom type.
+the set of atoms to a set of the generic atom type.
 It is defined as @{text "atoms as \<equiv> {atom a | a \<in> as}"}.
 The last case we need to consider is when @{text "x\<^isub>i"} is neither
 a binder nor a body of an abstraction. In this case it is defined
 as in \eqref{deepbody}, except that we do not need to subtract the
 functions is to compute the set of free atoms that are not bound by
 @{text "bn\<^isub>j"}. Because of the restrictions we imposed on the
 form of binding functions, this can be done automatically by recursively
 building up the the set of free variables from the arguments that are
 not bound. Let us assume one clause of a binding function is
-@{text "bn\<^isub>j (C x\<^isub>1 \<dots> x\<^isub>n) = rhs"}, then @{text "fv_bn\<^isub>j"} is the
+@{text "bn\<^isub>j (C x\<^isub>1 \<dots> x\<^isub>n) = rhs"}, then @{text "fv_bn\<^isub>j (C x\<^isub>1 \<dots> x\<^isub>n)"} is the
-union of the values calculated for @{text "x\<^isub>i"} of type @{text "ty\<^isub>i"}
+union of the values calculated for @{text "x\<^isub>i"} as follows:
-as follows:
 \begin{center}
 \begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
 \multicolumn{2}{l}{@{text "x\<^isub>i"} occurs in @{text "rhs"}:}\\
 $\bullet$ & @{term "{}"} provided @{term "x\<^isub>i"} is a single atom,
 \begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
 \multicolumn{2}{l}{@{text "x\<^isub>i"} does not occur in @{text "rhs"}:}\\
 $\bullet$ & @{text "atom x\<^isub>i"} provided @{term "x\<^isub>i"} is an atom\\
 $\bullet$ & @{text "atoms x\<^isub>i"} provided @{term "x\<^isub>i"} is a set of atoms\\
 $\bullet$ & @{term "atoms (set x\<^isub>i)"} provided @{term "x\<^isub>i"} is a list of atoms\\
-$\bullet$ & @{text "fv_ty\<^isub>i x\<^isub>i"} provided @{term "ty\<^isub>i"} is one of the raw
+$\bullet$ & @{text "fv_ty\<^isub>i x\<^isub>i"} provided @{term "ty\<^isub>i"} is the type of @{text "x\<^isub>i"} and one of the raw
 types corresponding to the types specified by the user\\
 %  $\bullet$ & @{text "fv_ty\<^isup>\<alpha> x\<^isub>i - bnds"} provided @{term "x\<^isub>i"}  is not in @{text "rhs"}
 %     and is an existing nominal datatype with the free-variable function @{text "fv\<^isup>\<alpha>"}\\
 $\bullet$ & @{term "{}"} otherwise
 \end{tabular}
 @{text t}. Therefore we have to subtract @{text "set (bn as)"} from @{text
 "fv\<^bsub>trm\<^esub> t"}. However, we also need to add all atoms that are
 free in @{text "as"}. This is what the purpose of the function @{text
 "fv\<^bsub>bn\<^esub>"} is.  In contrast, in @{text "Let_rec"} we have a
 recursive binder where we want to also bind all occurrences of the atoms
-@{text "bn as"} inside @{text "as"}. Therefore we have to subtract @{text
+in @{text "set (bn as)"} inside @{text "as"}. Therefore we have to subtract @{text
 "set (bn as)"} from @{text "fv\<^bsub>assn\<^esub> as"}, as well as from
 @{text "fv\<^bsub>trm\<^esub> t"}. An interesting point in this example is
 that an assignment ``alone'' does not have any bound variables. Only in the
 context of a @{text Let} or @{text "Let_rec"} will some atoms become bound.
 This is a phenomenon
 \begin{itemize}
 \item The @{text "(x\<^isub>i, y\<^isub>i)"} are bodies of shallow binders with type @{text "ty"}. We assume the
 \mbox{@{text "(u\<^isub>1, v\<^isub>1),\<dots>,(u\<^isub>m, v\<^isub>m)"}} are the corresponding binders. For the binding mode
 \isacommand{bind\_set} we generate the premise
 \begin{center}
-@{term "\<exists>p. (u\<^isub>1 \<union> \<xi> \<union> u\<^isub>m, x\<^isub>i) \<approx>gen alpha_ty fv_ty\<^isub>i p (v\<^isub>1 \<union> \<xi> \<union> v\<^isub>m, y\<^isub>i)"}
+@{term "\<exists>p. (u\<^isub>1 \<union> \<xi> \<union> u\<^isub>m, x\<^isub>i) \<approx>gen alpha_ty fv_ty p (v\<^isub>1 \<union> \<xi> \<union> v\<^isub>m, y\<^isub>i)"}
 \end{center}
-For the binding mode \isacommand{bind} we use $\approx_{\textit{list}}$, and for
+For the binding mode \isacommand{bind}, we use $\approx_{\textit{list}}$, and for
-binding mode \isacommand{bind\_res} we use $\approx_{\textit{res}}$.
+binding mode \isacommand{bind\_res} we use $\approx_{\textit{res}}$ instead.
 \item The @{text "(x\<^isub>i, y\<^isub>i)"} are deep non-recursive binders with type @{text "ty"}
 and @{text bn} being the auxiliary binding function. We assume
 @{text "(u\<^isub>1, v\<^isub>1),\<dots>,(u\<^isub>m, v\<^isub>m)"} are the corresponding bodies with types @{text "ty\<^isub>1,\<dots>, ty\<^isub>m"}.
 For the binding mode \isacommand{bind\_set} we generate two premises
 \noindent
 From these definition it is clear why we can only support one binding mode per binder
 and body, as we cannot mix the relations $\approx_{\textit{set}}$, $\approx_{\textit{list}}$
 and $\approx_{\textit{res}}$. It is also clear why we had to impose the restriction
-of excluding overlapping binders, as these would need to be translated to separate
+of excluding overlapping binders, as these would need to be translated into separate
 abstractions.
 The only cases that are not covered by the rules above are the cases where @{text "(x\<^isub>i, y\<^isub>i)"} is
-neither a binder nor a body. Then we just generate @{text "x\<^isub>i \<approx>ty y\<^isub>i"}  provided
+neither a binder nor a body in a binding clause. Then we just generate @{text "x\<^isub>i \<approx>ty y\<^isub>i"}  provided
 the type of @{text "x\<^isub>i"} and @{text "y\<^isub>i"} is @{text ty} and the arguments are
-recursive arguments of the term-constructor. If they are non-recursive arguments
+recursive arguments of the term-constructor. If they are non-recursive arguments,
 then we generate just @{text "x\<^isub>i = y\<^isub>i"}.
-{\bf TODO (I do not understand the definition below yet).}
+The definition of the alpha-equivalence relations @{text "\<approx>bn"} for binding functions
-The alpha-equivalence relations for binding functions are similar to the alpha-equivalences
+are similar. We again have conclusions of the form \mbox{@{text "C x\<^isub>1 \<dots> x\<^isub>n \<approx>bn C y\<^isub>1 \<dots> y\<^isub>n"}}. We
-for their respective types, the difference is that they omit checking the arguments that
+need to generate premises for each pair @{text "(x\<^isub>i, y\<^isub>i)"} depending on whether @{text "x\<^isub>i"}
-are bound. We assumed that there are no bindings in the type on which the binding function
+occurs in @{text "rhs"} of  the clause @{text "bn (C x\<^isub>1 \<dots> x\<^isub>n) = rhs"}:
-is defined so, there are no permutations involved. For a binding function clause
-@{text "bn (C x\<^isub>1 \<dots> x\<^isub>n) = rhs"}, two instances of the constructor are equivalent
+\begin{center}
-@{text "C x\<^isub>1 \<dots> x\<^isub>n \<approx> C y\<^isub>1 \<dots> y\<^isub>n"} if:
+\begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
-\begin{center}
+$\bullet$ & @{text "x\<^isub>i \<approx>ty y\<^isub>i"} provided @{text "x\<^isub>i"} does not occur in @{text rhs}
-\begin{tabular}{cp{7cm}}
+and the type of @{text "x\<^isub>i"} is @{text "ty"}\\
-$\bullet$ & @{text "x\<^isub>j"} is not of a type being defined and occurs in @{text "rhs"}\\
+$\bullet$ & @{text "x\<^isub>i \<approx>bn y\<^isub>i"} provided @{text "x\<^isub>i"} occurs in @{text rhs}
-$\bullet$ & @{text "x\<^isub>j = y\<^isub>j"} provided @{text "x\<^isub>j"} is not of a type being defined
+with the recursive call @{text "bn x\<^isub>i"}\\
-and does not occur in @{text "rhs"}\\
+$\bullet$ & none provided @{text "x\<^isub>i"} occurs in @{text rhs} but it is not
-$\bullet$ & @{text "x\<^isub>j \<approx>bn\<^isub>m y\<^isub>j"} provided @{text "x\<^isub>j"} is of a type being defined
+in a recursive call involving a @{text "bn"}
-occuring in @{text "rhs"} under the binding function @{text "bn\<^isub>m"}\\
+\end{tabular}
-$\bullet$ & @{text "x\<^isub>j \<approx> y\<^isub>j"} otherwise\\
+\end{center}
-\end{tabular}
-\end{center}
+Again lets take a look at an example for these definitions. For \eqref{letrecs}
-Again lets take a look at an example for these definitions. For \eqref{letrecs}
 we have three relations, namely $\approx_{\textit{trm}}$, $\approx_{\textit{assn}}$ and
 $\approx_{\textit{bn}}$, with the clauses as follows:
 \begin{center}
 \begin{tabular}{@ {}c @ {}}
 \noindent
 Note the difference between  $\approx_{\textit{assn}}$ and
 $\approx_{\textit{bn}}$: the latter only ``tracks'' alpha-equivalence of
 the components in an assignment that are \emph{not} bound. Therefore we have
 a $\approx_{\textit{bn}}$-premise in the clause for @{text "Let"} (which is
-a non-recursive binder), since the terms inside an assignment are not meant
+a non-recursive binder). The reason is that the terms inside an assignment are not meant
 to be under the binder. Such a premise is not needed in @{text "Let_rec"},
 because there everything from the assignment is under the binder.
 *}
 section {* Establishing the Reasoning Infrastructure *}
 text {*
-Having made all these definition for raw terms, we can start to introduce
+Having made all crucial definitions for raw terms, we can start introducing
-the resoning infrastructure for the specified types. For this we first
+the resoning infrastructure for the types the user specified. For this we first
 have to show that the alpha-equivalence relation defined in the previous
 sections are indeed equivalence relations.
 \begin{lemma}
 Given the raw types @{text "ty\<^isub>1, \<dots>, ty\<^isub>n"} and binding functions
 @{text "bn\<^isub>1, \<dots>, bn\<^isub>m"}, the relations @{text "\<approx>ty\<^isub>1, \<dots>, \<approx>ty\<^isub>n"} and
 @{text "\<approx>bn\<^isub>1 \<dots> \<approx>bn\<^isub>m"} are equivalence relations and equivariant.
 \end{lemma}
 \begin{proof}
-The proof is by induction over the definitions. The non-trivial
+The proof is by mutual induction over the definitions. The non-trivial
-cases involves premises build up by $\approx_{\textit{set}}$,
+cases involve premises build up by $\approx_{\textit{set}}$,
 $\approx_{\textit{res}}$ and $\approx_{\textit{list}}$. They
-can be dealt with like in Lemma~\ref{alphaeq}.
+can be dealt with as in Lemma~\ref{alphaeq}.
 \end{proof}
 \noindent
 We can feed this lemma into our quotient package and obtain new types @{text
 "ty"}$^\alpha_{1..n}$ representing alpha-equated terms of types @{text

changeset 1752	9e09253c80cf
parent 1749	24cc3dbd3c4a
child 1753	7440bfcdf849