--- a/Paper/Paper.thy Tue Jul 13 23:39:39 2010 +0100
+++ b/Paper/Paper.thy Wed Jul 14 21:30:52 2010 +0100
@@ -37,6 +37,21 @@
Cons ("_::_" [78,77] 73) and
supp_gen ("aux _" [1000] 10) and
alpha_bn ("_ \<approx>bn _")
+
+consts alpha_trm ::'a
+consts fa_trm :: 'a
+consts alpha_trm2 ::'a
+consts fa_trm2 :: 'a
+consts ast :: 'a
+consts ast' :: 'a
+notation (latex output)
+ alpha_trm ("\<approx>\<^bsub>trm\<^esub>") and
+ fa_trm ("fa\<^bsub>trm\<^esub>") and
+ alpha_trm2 ("'(\<approx>\<^bsub>assn\<^esub>, \<approx>\<^bsub>trm\<^esub>')") and
+ fa_trm2 ("'(fa\<^bsub>assn\<^esub>, fa\<^bsub>trm\<^esub>')") and
+ ast ("'(as, t')") and
+ ast' ("'(as', t\<PRIME> ')")
+
(*>*)
@@ -923,7 +938,7 @@
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 ``\isacommand{in}-part'' of a binding
+ 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
@@ -1088,8 +1103,8 @@
\noindent
Otherwise it is possible that @{text "bn\<^isub>1"} and @{text "bn\<^isub>2"} pick
out different atoms to become bound, respectively be free, in @{text "p"}.
- (Since the Ott-tool does not derive a reasoning for $\alpha$-equated terms, it can permit
- such specifications.)
+ (Since the Ott-tool does not derive a reasoning infrastructure for
+ $\alpha$-equated terms, it can permit such specifications.)
We also need to restrict the form of the binding functions in order
to ensure the @{text "bn"}-functions can be defined for $\alpha$-equated
@@ -1100,7 +1115,7 @@
In contrast, in case of \eqref{letrecs} the term-constructor @{text ACons}
may have a binding clause involving the argument @{text t} (the only one that
is \emph{not} used in the definition of the binding function). This restriction
- is sufficient for defining the binding function over $\alpha$-equated terms.
+ is sufficient for having the binding function over $\alpha$-equated terms.
In the version of
Nominal Isabelle described here, we also adopted the restriction from the
@@ -1453,7 +1468,8 @@
involving multiple binders. As above, we first build the tuples @{text "D"} and
@{text "D'"} for the bodies @{text "d"}$_{1..q}$, and the corresponding
compound $\alpha$-relation @{text "R"} (shown in \eqref{rempty}).
- For $\approx_{\,\textit{set}}$ we also need
+ For $\approx_{\,\textit{set}}$ (respectively $\approx_{\,\textit{list}}$ and
+ $\approx_{\,\textit{res}}$) we also need
a compound free-atom function for the bodies defined as
%
\begin{center}
@@ -1479,12 +1495,12 @@
\noindent
This premise accounts for $\alpha$-equivalence of the bodies of the binding
- clause. Similarly for the other binding modes.
+ clause.
However, in case the binders have non-recursive deep binders, this premise
is not enough:
we also have to ``propagate'' $\alpha$-equivalence inside the structure of
these binders. An example is @{text "Let"} where we have to make sure the
- right-hand sides of assignments are $\alpha$-equivalent. For this we use the
+ right-hand sides of assignments are $\alpha$-equivalent. For this we use
relations @{text "\<approx>bn"}$_{1..m}$ (which we will formally define shortly).
Let us assume the non-recursive deep binders in @{text "bc\<^isub>i"} are
%
@@ -1493,15 +1509,17 @@
\end{center}
\noindent
+ The tuple @{text L} is then @{text "(l\<^isub>1,\<dots>,l\<^isub>r)"} (similarly @{text "L'"})
+ and the compound equivalence relation @{text "R'"} is @{text "(\<approx>bn\<^isub>1,\<dots>,\<approx>bn\<^isub>r)"}.
All premises for @{text "bc\<^isub>i"} are then given by
%
\begin{center}
- @{text "prems(bc\<^isub>i) \<equiv> P \<and> l\<^isub>1 \<approx>bn\<^isub>1 l\<PRIME>\<^isub>1 \<and> ... \<and> l\<^isub>r \<approx>bn\<^isub>r l\<PRIME>\<^isub>r"}
+ @{text "prems(bc\<^isub>i) \<equiv> P \<and> L R' L'"}
\end{center}
\noindent
- where the auxiliary $\alpha$-equivalence relations @{text "\<approx>bn"}$_{1..m}$
- are defined as follows: assuming a @{text bn}-clause is of the form
+ The auxiliary $\alpha$-equivalence relations @{text "\<approx>bn"}$_{1..m}$
+ in @{text "R'"} are defined as follows: assuming a @{text bn}-clause is of the form
%
\begin{center}
@{text "bn (C z\<^isub>1 \<dots> z\<^isub>s) = rhs"}
@@ -1509,7 +1527,7 @@
\noindent
where the @{text "z"}$_{1..s}$ are of types @{text "ty"}$_{1..s}$,
- then the $\alpha$-equivalence clause for @{text "\<approx>bn"} has the form
+ then the corresponding $\alpha$-equivalence clause for @{text "\<approx>bn"} has the form
%
\begin{center}
\mbox{\infer{@{text "C z\<^isub>1 \<dots> z\<^isub>s \<approx>bn C z\<PRIME>\<^isub>1 \<dots> z\<PRIME>\<^isub>s"}}
@@ -1537,26 +1555,8 @@
that the premises of empty binding clauses are a special case of the clauses for
non-empty ones (we just have to unfold the definition of $\approx_{\,\textit{set}}$ and take @{text "0"}
for the existentially quantified permutation).
-*}
-(*<*)
-consts alpha_ty ::'a
-consts alpha_trm ::'a
-consts fa_trm :: 'a
-consts alpha_trm2 ::'a
-consts fa_trm2 :: 'a
-consts ast :: 'a
-consts ast' :: 'a
-notation (latex output)
- alpha_ty ("\<approx>ty") and
- alpha_trm ("\<approx>\<^bsub>trm\<^esub>") and
- fa_trm ("fa\<^bsub>trm\<^esub>") and
- alpha_trm2 ("'(\<approx>\<^bsub>assn\<^esub>, \<approx>\<^bsub>trm\<^esub>')") and
- fa_trm2 ("'(fa\<^bsub>assn\<^esub>, fa\<^bsub>trm\<^esub>')") and
- ast ("'(as, t')") and
- ast' ("'(as', t\<PRIME> ')")
-(*>*)
-text {*
- Again lets take a look at a concrete example for these definitions. For \eqref{letrecs}
+
+ Again let us take a look at a concrete example for these definitions. For \eqref{letrecs}
we have three relations $\approx_{\textit{trm}}$, $\approx_{\textit{assn}}$ and
$\approx_{\textit{bn}}$ with the following clauses:
@@ -1564,14 +1564,14 @@
\begin{tabular}{@ {}c @ {}}
\infer{@{text "Let as t \<approx>\<^bsub>trm\<^esub> Let as' t'"}}
{@{term "\<exists>p. (bn as, t) \<approx>lst alpha_trm fa_trm p (bn as', t')"} & @{text "as \<approx>\<^bsub>bn\<^esub> as'"}}\smallskip\\
- \infer{@{text "Let_rec as t \<approx>\<^bsub>trm\<^esub> Let_rec as' t'"}}
- {@{term "\<exists>p. (bn as, ast) \<approx>lst alpha_trm2 fa_trm2 p (bn as', ast')"}}
+ \makebox[0mm]{\infer{@{text "Let_rec as t \<approx>\<^bsub>trm\<^esub> Let_rec as' t'"}}
+ {@{term "\<exists>p. (bn as, ast) \<approx>lst alpha_trm2 fa_trm2 p (bn as', ast')"}}}
\end{tabular}
\end{center}
\begin{center}
\begin{tabular}{@ {}c @ {}}
- \infer{@{text "ANil \<approx>\<^bsub>assn\<^esub> ANil"}}{}\\
+ \infer{@{text "ANil \<approx>\<^bsub>assn\<^esub> ANil"}}{}\smallskip\\
\infer{@{text "ACons a t as \<approx>\<^bsub>assn\<^esub> ACons a' t' as"}}
{@{text "a = a'"} & @{text "t \<approx>\<^bsub>trm\<^esub> t'"} & @{text "as \<approx>\<^bsub>assn\<^esub> as'"}}
\end{tabular}
@@ -1579,7 +1579,7 @@
\begin{center}
\begin{tabular}{@ {}c @ {}}
- \infer{@{text "ANil \<approx>\<^bsub>bn\<^esub> ANil"}}{}\\
+ \infer{@{text "ANil \<approx>\<^bsub>bn\<^esub> ANil"}}{}\smallskip\\
\infer{@{text "ACons a t as \<approx>\<^bsub>bn\<^esub> ACons a' t' as"}}
{@{text "t \<approx>\<^bsub>trm\<^esub> t'"} & @{text "as \<approx>\<^bsub>bn\<^esub> as'"}}
\end{tabular}
@@ -1588,8 +1588,8 @@
\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
+ the components in an assignment that are \emph{not} bound. This is needed in the
+ in the clause for @{text "Let"} (which is has
a non-recursive binder). The underlying reason is that the terms inside an assignment are not meant
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.
@@ -1602,7 +1602,7 @@
introducing the reasoning infrastructure for the $\alpha$-equated types the
user originally specified. We sketch in this section the facts we need for establishing
this reasoning infrastructure. First we have to show that the
- $\alpha$-equivalence relations defined in the previous section are indeed
+ $\alpha$-equivalence relations defined in the previous section are
equivalence relations.
\begin{lemma}\label{equiv}
@@ -1620,8 +1620,8 @@
\noindent
We can feed this lemma into our quotient package and obtain new types @{text
- "ty\<AL>\<^bsub>1..n\<^esub>"} representing $\alpha$-equated terms of types @{text "ty\<^bsub>1..n\<^esub>"}. We also obtain
- definitions for the term-constructors @{text
+ "ty"}$^\alpha_{1..n}$ representing $\alpha$-equated terms of types @{text "ty"}$_{1..n}$.
+ We also obtain definitions for the term-constructors @{text
"C"}$^\alpha_{1..m}$ from the raw term-constructors @{text
"C"}$_{1..m}$, and similar definitions for the free-atom functions @{text
"fa_ty"}$^\alpha_{1..n}$ and the binding functions @{text
@@ -1652,7 +1652,7 @@
are \emph{respectful} w.r.t.~the $\alpha$-equivalence relations (see \cite{Homeier05}).
Assuming @{text "C\<^isub>i"} is of type @{text "ty"} with argument types
@{text "ty\<^isub>1, \<dots>, ty\<^isub>n"}, then respectfulness amounts to showing that
-
+ %
\begin{center}
@{text "C\<^isub>i x\<^isub>1 \<dots> x\<^isub>n \<approx>ty C\<^isub>i y\<^isub>1 \<dots> y\<^isub>n"}
\end{center}
@@ -1676,7 +1676,7 @@
In fact we can from now on lift facts from the raw level to the $\alpha$-equated level
as long as they contain raw term-constructors only. The
induction principles derived by the datatype package in Isabelle/HOL for the types @{text
- "ty\<^bsub>1..n\<^esub>"} fall into this category. So we can also add to our infrastructure
+ "ty"}$_{1..n}$ fall into this category. So we can also add to our infrastructure
induction principles that establish
\begin{center}