nominal2: comparison Paper/Paper.thy

equal deleted inserted replaced

-:9f55d7927e5b
+:9a894c42e80e
 section {* Alpha-Equivalence and Free Variables\label{sec:alpha} *}
 text {*
 Our choice of syntax for specifications is influenced by the existing
-datatype package of Isabelle/HOL \cite{Berghofer99} and by the syntax of the Ott-tool
+datatype package of Isabelle/HOL \cite{Berghofer99} and by the syntax of the
-\cite{ott-jfp}. For us a specification of a term-calculus is a collection of (possibly mutual
+Ott-tool \cite{ott-jfp}. For us a specification of a term-calculus is a
-recursive) type declarations, say @{text "ty"}$^\alpha_1$, \ldots,
+collection of (possibly mutual recursive) type declarations, say @{text
-@{text ty}$^\alpha_n$, and an associated collection
+"ty\<AL>\<^isub>1, \<dots>, ty\<AL>\<^isub>n"}, and an associated collection of
-of binding functions, say @{text bn}$^\alpha_1$, \ldots, @{text
+binding functions, say @{text "bn\<AL>\<^isub>1, \<dots>, bn\<AL>\<^isub>m"}. The
-bn}$^\alpha_m$. The syntax in Nominal Isabelle for such specifications is
+syntax in Nominal Isabelle for such specifications is roughly as follows:
-roughly as follows:
 %
 \begin{equation}\label{scheme}
 \mbox{\begin{tabular}{@ {\hspace{-5mm}}p{1.8cm}l}
 type \mbox{declaration part} &
 $\begin{cases}
 \mbox{\begin{tabular}{l}
-\isacommand{nominal\_datatype} @{text ty}$^\alpha_1 = \ldots$\\
+\isacommand{nominal\_datatype} @{text "ty\<AL>\<^isub>1 = \<dots>"}\\
-\isacommand{and} @{text ty}$^\alpha_2 = \ldots$\\
+\isacommand{and} @{text "ty\<AL>\<^isub>2 = \<dots>"}\\
 $\ldots$\\
-\isacommand{and} @{text ty}$^\alpha_n = \ldots$\\
+\isacommand{and} @{text "ty\<AL>\<^isub>n = \<dots>"}\\
 \end{tabular}}
 \end{cases}$\\
 binding \mbox{function part} &
 $\begin{cases}
 \mbox{\begin{tabular}{l}
-\isacommand{with} @{text bn}$^\alpha_1$ \isacommand{and} \ldots \isacommand{and} @{text bn}$^\alpha_m$\\
+\isacommand{with} @{text "bn\<AL>\<^isub>1"} \isacommand{and} \ldots \isacommand{and} @{text "bn\<AL>\<^isub>m"}\\
 \isacommand{where}\\
 $\ldots$\\
 \end{tabular}}
 \end{cases}$\\
 \end{tabular}}
 \end{equation}
 \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
+term-constructors, each of which come 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>\<alpha>"} might have
+For example a term-constructor @{text "C\<^sup>\<alpha>"} might be specified with
 \begin{center}
 @{text "C\<^sup>\<alpha> label\<^isub>1::ty"}$'_1$ @{text "\<dots> label\<^isub>l::ty"}$'_l\;\;$  @{text "binding_clauses"}
 \end{center}
 \noindent
 whereby some of the @{text ty}$'_{1..l}$ (or their components) might 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
+In this case we will call the corresponding argument a
-%\emph{recursive argument} of @{text "C\<^sup>\<alpha>"}. The types of such recursive
+\emph{recursive argument} of @{text "C\<^sup>\<alpha>"}.
+%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
 \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). The ``\isacommand{in}-part'' of a binding
-clause will be called the \emph{body}; the
+clause will be called the \emph{body}; the ``\isacommand{bind}-part'' will
-``\isacommand{bind}-part'' will be the \emph{binder}.
+be called the \emph{binder}.
 In addition we distinguish between \emph{shallow} and \emph{deep}
 binders.  Shallow binders are of the form \isacommand{bind}\; {\it label}\;
 \isacommand{in}\; {\it label'} (similar for the other two modes). The
 restriction we impose on shallow binders is that the {\it label} must either
 The first non-trivial step we have to perform is the generation free-variable
 functions from the specifications. Given the raw types @{text "ty\<^isub>1 \<dots> ty\<^isub>n"}
 we need to define free-variable functions
 \begin{center}
-@{text "fv_ty\<^isub>1 :: ty\<^isub>1 \<Rightarrow> atom set    \<dots>    fv_ty\<^isub>n :: ty\<^isub>n \<Rightarrow> atom set"}
+@{text "fv_ty\<^isub>1, \<dots>, fv_ty\<^isub>n"}
 \end{center}
 \noindent
 We define them together with auxiliary free-variable functions for
 the binding functions. Given binding functions
 @{text "bn\<^isub>1 \<dots> bn\<^isub>m"} we need to define
 %
 \begin{center}
-@{text "fv_bn\<^isub>1 :: ty\<^isub>1 \<Rightarrow> atom set  \<dots>  fv_bn\<^isub>m :: ty\<^isub>m \<Rightarrow> atom set"}
+@{text "fv_bn\<^isub>1, \<dots>, fv_bn\<^isub>m"}
 \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 a function
 \begin{center}
 \begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
 $\bullet$ & @{text "fv_bn x\<^isub>i"} provided @{text "rhs"} contains the
 recursive call @{text "bn x\<^isub>i"}\medskip\\
 $\bullet$ & @{term "{}"} provided @{text "rhs"} contains
-@{term "x\<^isub>i"} without a recursive call.
+@{term "x\<^isub>i"} and @{term "x\<^isub>i"} is of atom type.
 \end{tabular}
 \end{center}
 \noindent
 To see how these definitions work in practise, let us reconsider the term-constructors
 context of a @{text Let} or @{text "Let_rec"} will some atoms become bound.
 This is a phenomenon
 that has also been pointed out in \cite{ott-jfp}. We can also see that
 %
 \begin{equation}\label{bnprop}
-@{text "fv_ty x = bn x \<union> fv_bn x"}.
+@{text "fv_ty x  =  bn x \<union> fv_bn x"}.
 \end{equation}
 \noindent
-holds for any @{text "bn"}-function of type @{text "ty"}.
+holds for any @{text "bn"}-function defined for the type @{text "ty"}.
-Next we define alpha-equivalence for the types @{text "ty\<^isub>1, \<dots>, ty\<^isub>n"}. We call them
+Next we define alpha-equivalence relations for the types @{text "ty\<^isub>1, \<dots>, ty\<^isub>n"}. We call them
 @{text "\<approx>ty\<^isub>1, \<dots>, \<approx>ty\<^isub>n"}. Like with the free-variable functions,
 we also need to  define auxiliary alpha-equivalence relations for the binding functions.
 Say we have @{text "bn\<^isub>1, \<dots>, bn\<^isub>m"}, then we also define @{text "\<approx>bn\<^isub>1, \<dots>, \<approx>bn\<^isub>m"}.
 To simplify our definitions we will use the following abbreviations for
 relations and free-variable acting on products.
 \end{center}
 \noindent
 For what follows, let us assume
 @{text C} is of type @{text ty} and its arguments are given by @{text "C ty\<^isub>1 \<dots> ty\<^isub>n"}.
-The task now is to specify what the premises of these clauses are. For this we
+The task is to specify what the premises of these clauses are. For this we
 consider the pairs \mbox{@{text "(x\<^isub>i, y\<^isub>i)"}}, but instead of considering them in turn, it will
 be easier to analyse these pairs according to  ``clusters'' of the binding clauses.
 Therefore we distinguish the following cases:
 *}
 (*<*)
 alpha_trm2 ("\<approx>\<^bsub>assn\<^esub> \<otimes> \<approx>\<^bsub>trm\<^esub>") and
 fv_trm2 ("fv\<^bsub>assn\<^esub> \<oplus> fv\<^bsub>trm\<^esub>")
 (*>*)
 text {*
 \begin{itemize}
-\item The @{text "(x\<^isub>i, y\<^isub>i)"} are bodies of shallow binders with type @{text "ty"}. We assume the
+\item The @{text "(x\<^isub>i, y\<^isub>i)"} is a body of shallow binder 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 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
 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"}
+\item The @{text "(x\<^isub>i, y\<^isub>i)"} is a deep non-recursive binder with type @{text "ty"}
-and @{text bn} being the auxiliary binding function. We assume
+and @{text bn} is corresponding the 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
 %
 \begin{center}
 @{text "x\<^isub>i \<approx>bn y\<^isub>i"}\hfill
 \noindent
 where @{text R} is @{text "\<approx>ty\<^isub>1 \<otimes> ... \<otimes> \<approx>ty\<^isub>m"} and @{text fv} is
 @{text "fv_ty\<^isub>1 \<oplus> ... \<oplus> fv_ty\<^isub>m"}. Similarly for the other binding modes.
-\item The @{text "(x\<^isub>i, y\<^isub>i)"} are deep recursive binders with type @{text "ty"}
+\item The @{text "(x\<^isub>i, y\<^isub>i)"} is a deep recursive binders with type @{text "ty"}
-and with @{text bn} being the auxiliary binding function. We assume
+and  @{text bn} is the corresponding 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 the premise
 %
 \begin{center}
 @{term "\<exists>p. (bn x\<^isub>i, (x\<^isub>i, u\<^isub>1,\<xi>,u\<^isub>m)) \<approx>gen R fv p (bn y\<^isub>i, (y\<^isub>i, v\<^isub>1,\<xi>,v\<^isub>m))"}
 where @{text R} is @{text "\<approx>ty \<otimes> \<approx>ty\<^isub>1 \<otimes> ... \<otimes> \<approx>ty\<^isub>m"} and @{text fv} is
 @{text "fv_ty \<oplus> fv_ty\<^isub>1 \<oplus> ... \<oplus> fv_ty\<^isub>m"}. Similarly for the other modes.
 \end{itemize}
 \noindent
-From these definition it is clear why we can only support one binding mode per binder
+From this 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
+and $\approx_{\textit{res}}$. It is also clear why we have to impose the restriction
 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 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,
-then we generate just @{text "x\<^isub>i = y\<^isub>i"}.
+then we generate the premise @{text "x\<^isub>i = y\<^isub>i"}.
-The definitions of the alpha-equivalence relations @{text "\<approx>bn"} for binding functions
+The alpha-equivalence relations @{text "\<approx>bn\<^isub>j"} for binding functions
 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"}}
 and need to generate appropriate premises. We generate first premises according to the first three
 rules given above. Only the ``left-over'' pairs  @{text "(x\<^isub>i, y\<^isub>i)"} need to be treated
 differently. They depend on whether @{text "x\<^isub>i"}  occurs in @{text "rhs"} of  the
 clause @{text "bn (C x\<^isub>1 \<dots> x\<^isub>n) = rhs"}:
 $\bullet$ & none provided @{text "x\<^isub>i"} occurs in @{text rhs} but it is not
 in a recursive call involving a @{text "bn"}
 \end{tabular}
 \end{center}
-Again lets take a look at an example for these definitions. For \eqref{letrecs}
+Again lets take a look at a concrete 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 @ {}}
 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). 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"},
+to be ``under'' the binder. Such a premise is \emph{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 crucial definitions for raw terms, we can start introducing
+Having made all necessary definitions for raw terms, we can start introducing
-the resoning infrastructure for the types the user specified. For this we first
+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.
 \begin{lemma}
 Given the raw types @{text "ty\<^isub>1, \<dots>, ty\<^isub>n"} and binding functions
 \mbox{@{text "C"}$^\alpha_i$@{text "x\<^isub>1 \<dots> x\<^isub>n"} @{text "\<noteq>"}
 @{text "C"}$^\alpha_j$@{text "y\<^isub>1 \<dots> y\<^isub>m"} holds for @{text "i \<noteq> j"}.}
 \end{equation}
 \noindent
-By definition of alpha-equivalence on raw terms we can show that
+By definition of alpha-equivalence we can show that
 for the raw term-constructors
+%
-\begin{center}
+\begin{equation}\label{distinctraw}
-@{text "C\<^isub>i x\<^isub>1 \<dots> x\<^isub>n"}$\;\not\approx@{text ty}\;$@{text "C\<^isub>j y\<^isub>1 \<dots> y\<^isub>m"} holds for @{text "i \<noteq> j"}.
+@{text "C\<^isub>i x\<^isub>1 \<dots> x\<^isub>n"}\;\not\approx@{text ty}\;@{text "C\<^isub>j y\<^isub>1 \<dots> y\<^isub>m"} holds for @{text "i \<noteq> j"}.
-\end{center}
+\end{equation}
 \noindent
 In order to generate \eqref{distinctalpha} from this fact, the quotient
 package needs to know that the term-constructors @{text "C\<^isub>i"} and @{text "C\<^isub>j"}
 are \emph{respectful} w.r.t.~the alpha-equivalence relations \cite{Homeier05}.
+This means, given @{text "C\<^isub>i"} is of type @{text "ty"} with argument types
-Given a term-constructor @{text C} of type @{text ty} and argument
+@{text "C ty\<^isub>1 \<dots> ty\<^isub>n"}, we have to show that
-types @{text "C ty\<^isub>1 \<dots> ty\<^isub>n"}, respectfullness means that
-%
+\begin{center}
-\begin{center}
+@{text "C x\<^isub>1 \<dots> x\<^isub>n \<approx>ty C y\<^isub>1 \<dots> y\<^isub>n"}
-aa
+\end{center}
-\end{center}
+\noindent
+under the assumption that @{text "x\<^isub>i \<approx>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 "\<approx>ty"}. For this to succed we have to establish an
+auxiliary fact: given a binding function @{text bn} defined for the type @{text ty}
+we have that
+\begin{center}
+@{text "x \<approx>ty y"} implies @{text "x \<approx>bn y"}
+\end{center}
+\noindent
+This can be established by induction on the definition of @{text "\<approx>ty"}.
+Having established respectfullness for every raw term-constructor, the
-\mbox{}\bigskip\bigskip
+quotient package will automaticaly deduce \eqref{distinctalpha} from \eqref{distinctraw}.
-then define the quotient types @{text "ty\<^isub>1\<^isup>\<alpha> \<dots> ty\<^isub>n\<^isup>\<alpha>"}.  To lift
+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
+"ty"}$^\alpha_{1..n}$ fall into this category. So we can also add to our infrastructure
+induction principles that establish
+\begin{center}
+@{text "P\<^bsub>ty\<^isub>1\<^esub> y\<^isub>1 \<dots> P\<^bsub>ty\<^isub>n\<^esub> y\<^isub>n "}
+\end{center}
+\noindent
+for every @{text "y\<^isub>i"} under the assumption we specified the types
+@{text "ty\<^isub>1\<^isup>\<alpha> \<dots> ty\<^isub>n\<^isup>\<alpha>"}. The premises of these induction principles look
+as follows
+\begin{center}
+@{text "\<forall>x\<^isub>1\<dots>x\<^isub>n. P\<^bsub>ty\<^isub>i\<^esub> x\<^isub>i \<and> \<dots> \<and> P\<^bsub>ty\<^isub>j\<^esub> x\<^isub>j \<Rightarrow> P\<^bsub>ty\<^esub> (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>n)"}
+\end{center}
+\noindent
+where the @{text "x\<^isub>i, \<dots>, x\<^isub>j"} are the recursive arguments of @{text "C\<^sup>\<alpha>"}.
+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
 This allows is to strengthen the induction principles. We will explain
 the details with the @{text "Let"} term-constructor from \eqref{letpat}.
 Instead of establishing the implication
 \begin{center}
-a
+@{text "\<forall>p t\<^isub>1 t\<^isub>2. P\<^bsub>pat\<^esub> p \<and> P\<^bsub>trm\<^esub> t\<^isub>1 \<and> P\<^bsub>trm\<^esub> t\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub> (Let p t\<^isub>1 t\<^isub>2)"}
 \end{center}
 \noindent
-from the weak induction principle.
+from the weak induction principle, we will show that it is sufficient
+to establish
+\begin{center}
+\begin{tabular}{l}
+@{text "\<forall>p t\<^isub>1 t\<^isub>2 c."}\\
+\hspace{5mm}@{text "set (bn\<^sup>\<alpha> p) #\<^sup>* c \<and>"}\\
+\hspace{5mm}@{text "(\<forall>d. P\<^bsub>pat\<^esub> d p) \<and> (\<forall>d. P\<^bsub>trm\<^esub> d t\<^isub>1) \<and> (\<forall>d. P\<^bsub>trm\<^esub> d t\<^isub>2)"}\\
+\hspace{15mm}@{text "\<Rightarrow> P\<^bsub>trm\<^esub> c (Let p t\<^isub>1 t\<^isub>2)"}
+\end{tabular}
+\end{center}
 With the help of @{text "\<bullet>bn"} functions defined in the previous section
 we can show that binders can be substituted in term constructors. We show
 this only for the specification from Figure~\ref{nominalcorehas}. The only

changeset 1765	9a894c42e80e
parent 1764	9f55d7927e5b
child 1766	a2d5f9ea17ad