--- a/Paper/Paper.thy Fri Apr 02 03:23:25 2010 +0200
+++ b/Paper/Paper.thy Fri Apr 02 05:09:47 2010 +0200
@@ -869,29 +869,28 @@
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
- \cite{ott-jfp}. For us a specification of a term-calculus is a collection of (possibly mutual
- recursive) type declarations, say @{text "ty"}$^\alpha_1$, \ldots,
- @{text ty}$^\alpha_n$, and an associated collection
- of binding functions, say @{text bn}$^\alpha_1$, \ldots, @{text
- bn}$^\alpha_m$. The syntax in Nominal Isabelle for such specifications is
- roughly as follows:
+ datatype package of Isabelle/HOL \cite{Berghofer99} and by the syntax of the
+ Ott-tool \cite{ott-jfp}. For us a specification of a term-calculus is a
+ collection of (possibly mutual recursive) type declarations, say @{text
+ "ty\<AL>\<^isub>1, \<dots>, ty\<AL>\<^isub>n"}, and an associated collection of
+ binding functions, say @{text "bn\<AL>\<^isub>1, \<dots>, bn\<AL>\<^isub>m"}. The
+ syntax in Nominal Isabelle for such specifications is 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{and} @{text ty}$^\alpha_2 = \ldots$\\
+ \isacommand{nominal\_datatype} @{text "ty\<AL>\<^isub>1 = \<dots>"}\\
+ \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}}
@@ -901,9 +900,9 @@
\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"}
@@ -913,8 +912,9 @@
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
- %\emph{recursive argument} of @{text "C\<^sup>\<alpha>"}. The types of such recursive
+ In this case we will call the corresponding argument a
+ \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}.
@@ -936,8 +936,8 @@
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
- ``\isacommand{bind}-part'' will be the \emph{binder}.
+ clause will be called the \emph{body}; the ``\isacommand{bind}-part'' will
+ 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}\;
@@ -1154,7 +1154,7 @@
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
@@ -1163,7 +1163,7 @@
@{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
@@ -1252,7 +1252,7 @@
$\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}
@@ -1296,13 +1296,13 @@
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"}.
@@ -1327,7 +1327,7 @@
\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:
@@ -1347,7 +1347,7 @@
(*>*)
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}
@@ -1357,8 +1357,8 @@
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"}
- and @{text bn} being the auxiliary binding function. We assume
+ \item The @{text "(x\<^isub>i, y\<^isub>i)"} is a deep non-recursive binder with type @{text "ty"}
+ 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
%
@@ -1371,8 +1371,8 @@
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"}
- and with @{text bn} being the auxiliary binding function. We assume
+ \item The @{text "(x\<^isub>i, y\<^isub>i)"} is a deep recursive binders with type @{text "ty"}
+ 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
%
@@ -1386,9 +1386,9 @@
\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.
@@ -1397,10 +1397,10 @@
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
@@ -1421,7 +1421,7 @@
\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:
@@ -1456,15 +1456,15 @@
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
- the resoning infrastructure for the types the user specified. For this we first
+ 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.
@@ -1502,28 +1502,64 @@
\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}
- @{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}
+ %
+ \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"}.
+ \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
+ @{text "C ty\<^isub>1 \<dots> ty\<^isub>n"}, we have to show that
- Given a term-constructor @{text C} of type @{text ty} and argument
- types @{text "C ty\<^isub>1 \<dots> ty\<^isub>n"}, respectfullness means that
- %
+ \begin{center}
+ @{text "C x\<^isub>1 \<dots> x\<^isub>n \<approx>ty C y\<^isub>1 \<dots> y\<^isub>n"}
+ \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}
- aa
+ @{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
+ quotient package will automaticaly 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
+ "ty"}$^\alpha_{1..n}$ fall into this category. So we can also add to our infrastructure
+ induction principles that establish
- \mbox{}\bigskip\bigskip
- then define the quotient types @{text "ty\<^isub>1\<^isup>\<alpha> \<dots> ty\<^isub>n\<^isup>\<alpha>"}. To lift
+ \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
@@ -1700,11 +1736,21 @@
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