--- a/Paper/Paper.thy Thu Apr 01 01:05:05 2010 +0200
+++ b/Paper/Paper.thy Thu Apr 01 03:28:28 2010 +0200
@@ -18,9 +18,9 @@
supp ("supp _" [78] 73) and
uminus ("-_" [78] 73) and
If ("if _ then _ else _" 10) and
- alpha_gen ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{set}}$}}>\<^bsup>_,_,_\<^esup> _") and
- alpha_lst ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{list}}$}}>\<^bsup>_,_,_\<^esup> _") and
- alpha_res ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{res}}$}}>\<^bsup>_,_,_\<^esup> _") and
+ alpha_gen ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{set}}$}}>\<^bsup>_, _, _\<^esup> _") and
+ alpha_lst ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{list}}$}}>\<^bsup>_, _, _\<^esup> _") and
+ alpha_res ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{res}}$}}>\<^bsup>_, _, _\<^esup> _") and
abs_set ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and
fv ("fv'(_')" [100] 100) and
equal ("=") and
@@ -31,13 +31,14 @@
Cons ("_::_" [78,77] 73) and
supp_gen ("aux _" [1000] 10) and
alpha_bn ("_ \<approx>bn _")
-
(*>*)
section {* Introduction *}
text {*
+ @{text "(1, (2, 3))"}
+
So far, Nominal Isabelle provides a mechanism for constructing
alpha-equated terms, for example
@@ -733,14 +734,11 @@
and $\approx_{\textit{abs\_res}}$). We can show that these relations are equivalence
relations and equivariant.
- \begin{lemma}\label{alphaeq} The relations
- $\approx_{\textit{abs\_set}}$,
- $\approx_{\textit{abs\_list}}$
- and $\approx_{\textit{abs\_res}}$
- are equivalence
- relations, and if @{term "abs_set (as, x) (bs, y)"} then also
- @{term "abs_set (p \<bullet> as, p \<bullet> x) (p \<bullet> bs, p \<bullet> y)"} (similarly for
- the other two relations).
+ \begin{lemma}\label{alphaeq}
+ The relations $\approx_{\textit{abs\_set}}$, $\approx_{\textit{abs\_list}}$
+ and $\approx_{\textit{abs\_res}}$ are equivalence relations, and if @{term
+ "abs_set (as, x) (bs, y)"} then also @{term "abs_set (p \<bullet> as, p \<bullet> x) (p \<bullet>
+ bs, p \<bullet> y)"} (similarly for the other two relations).
\end{lemma}
\begin{proof}
@@ -1343,7 +1341,16 @@
*}
(*<*)
consts alpha_ty ::'a
-notation alpha_ty ("\<approx>ty")
+consts alpha_trm ::'a
+consts fv_trm :: 'a
+consts alpha_trm2 ::'a
+consts fv_trm2 :: 'a
+notation (latex output)
+ alpha_ty ("\<approx>ty") and
+ alpha_trm ("\<approx>\<^bsub>trm\<^esub>") and
+ fv_trm ("fv\<^bsub>trm\<^esub>") and
+ 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}
@@ -1399,7 +1406,7 @@
recursive arguments of the term-constructor. If they are non-recursive arguments
then we generate just @{text "x\<^isub>i = y\<^isub>i"}.
- TODO
+ {\bf TODO (I do not understand the definition below yet).}
The alpha-equivalence relations for binding functions are similar to the alpha-equivalences
for their respective types, the difference is that they ommit checking the arguments that
@@ -1418,23 +1425,81 @@
\end{tabular}
\end{center}
+ 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 @ {}}
+ \infer{@{text "Let as t \<approx>\<^bsub>trm\<^esub> Let as' t'"}}
+ {@{text "as \<approx>\<^bsub>bn\<^esub> as'"} & @{term "\<exists>p. (bn as, t) \<approx>lst alpha_trm fv_trm p (bn as', t')"}}\smallskip\\
+ \infer{@{text "Let_rec as t \<approx>\<^bsub>trm\<^esub> Let_rec as' t'"}}
+ {@{term "\<exists>p. (bn as, (as, t)) \<approx>lst alpha_trm2 fv_trm2 p (bn as', (as', t'))"}}
+ \end{tabular}
+ \end{center}
+
+ \begin{center}
+ \begin{tabular}{@ {}c @ {}}
+ \infer{@{text "ANil \<approx>\<^bsub>assn\<^esub> ANil"}}{}\\
+ \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'"}}\medskip\\
+ \end{tabular}
+ \end{center}
+
+ \begin{center}
+ \begin{tabular}{@ {}c @ {}}
+ \infer{@{text "ANil \<approx>\<^bsub>bn\<^esub> ANil"}}{}\\
+ \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'"}}\medskip\\
+ \end{tabular}
+ \end{center}
+
+ \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
+ 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 {* The Lifting of Definitions and Properties *}
+section {* Establishing the Reasoning Infrastructure *}
text {*
- To define the quotient types we first need to show that the defined
- relations are equivalence relations.
+ Having made all these definition for raw terms, we can start to introduce
+ the resoning infrastructure for the specified types. For this we first
+ have to show that the alpha-equivalence relation defined in the previous
+ sections are indeed equivalence relations.
- \begin{lemma} The relations @{text "\<approx>\<^isub>1 \<dots> \<approx>\<^isub>1"} and @{text "\<approx>bn\<^isub>1 \<dots> \<approx>bn\<^isub>m"}
- defined as above are equivalence relations and are equivariant.
+ \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} Reflexivity by induction on the raw datatype. Symmetry,
- transitivity and equivariance by induction on the alpha equivalence
- relation. Using lemma \ref{alphaeq}, the conditions follow by simple
- calculations. \end{proof}
+
+ \begin{proof}
+ The proof is by induction over the definitions. The non-trivial
+ cases involves premises build up by $\approx_{\textit{set}}$,
+ $\approx_{\textit{res}}$ and $\approx_{\textit{list}}$. They
+ can be dealt with like in Lemma~\ref{alphaeq}.
+ \end{proof}
- \noindent We then define the quotient types @{text "ty\<^isub>1\<^isup>\<alpha> \<dots> ty\<^isub>n\<^isup>\<alpha>"}. To lift
+ \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
+ "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}$. Similarly for the free-variable functions @{text
+ "fv_ty"}$^\alpha_{1..n}$ and the binding functions @{text
+ "bn"}$^\alpha_{1..k}$. However, these definitions are of not much use for the
+ user, since the are formulated in terms of the isomorphism we obtained by
+ cerating a new type in Isabelle/HOL (remember the picture shown in the
+ Introduction).
+
+ {\bf TODO below.}
+
+ then define the quotient types @{text "ty\<^isub>1\<^isup>\<alpha> \<dots> ty\<^isub>n\<^isup>\<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
@@ -1572,28 +1637,8 @@
permutations on the lifted type and the lifted defining eqautions of @{text "\<bullet>bn"}.
\end{proof}
-
-
*}
-(* @{thm "ACons_subst[no_vars]"}*)
-
-text {*
-%%% FIXME: The restricions should have already been described in previous sections?
- Restrictions
-
- \begin{itemize}
- \item non-emptiness
- \item positive datatype definitions
- \item finitely supported abstractions
- \item respectfulness of the bn-functions\bigskip
- \item binders can only have a ``single scope''
- \item all bindings must have the same mode
- \end{itemize}
-*}
-
-section {* Examples *}
-
text {*
\begin{figure}
@@ -1629,7 +1674,7 @@
$|$~@{text "LAM_cty cv::cvar ckind t::trm"} \isacommand{bind}~@{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 "Let x::var ty trm t::trm"} \isacommand{bind}~@{text x}~\isacommand{in}~@{text t}\\
$|$~@{text "Case trm assoc_lst"}~$|$~@{text "Cast trm co"}\\
\isacommand{and}~@{text "assoc_lst ="}\\
\phantom{$|$}~@{text ANil}~%
@@ -1657,14 +1702,20 @@
$|$~@{text "bv3 (TVCKCons c cty tl) = (atom c)::(bv3 tl)"}\\
\end{tabular}
\end{boxedminipage}
- \caption{\label{nominalcorehas}}
+ \caption{The nominal datatype declaration for Core-Haskell. At the moment we
+ do not support nested types; therefore we explicitly have to unfold the
+ lists @{text "co_lst"}, @{text "assoc_lst"} and so on. This will be improved
+ in a future version of Nominal Isabelle. Apart from that, the
+ declaration follows closely the original in Figure~\ref{corehas}. The
+ point of our work is that having made such a declaration one obtains
+ automatically a reasoning infrastructure for Core-Haskell.\label{nominalcorehas}}
\end{figure}
*}
-
+(* @{thm "ACons_subst[no_vars]"}*)
-section {* Adequacy *}
+section {* Strong Induction Principles *}
section {* Related Work *}
@@ -1698,8 +1749,22 @@
The reasoning there turned out to be quite complex.
Ott is better with list dot specifications; subgrammars, is untyped;
+*}
+
+text {*
+%%% FIXME: The restricions should have already been described in previous sections?
+ Restrictions
+
+ \begin{itemize}
+ \item non-emptiness
+ \item positive datatype definitions
+ \item finitely supported abstractions
+ \item respectfulness of the bn-functions\bigskip
+ \item binders can only have a ``single scope''
+ \item all bindings must have the same mode
+ \end{itemize}
+*}
-*}
section {* Conclusion *}
@@ -1718,9 +1783,7 @@
the Mercurial repository linked at
\href{http://isabelle.in.tum.de/nominal/download}
{http://isabelle.in.tum.de/nominal/download}.\medskip
-*}
-text {*
\noindent
{\bf Acknowledgements:} We are very grateful to Andrew Pitts for
many discussions about Nominal Isabelle. We thank Peter Sewell for
@@ -1728,11 +1791,7 @@
also for patiently explaining some of the finer points about the abstract
definitions and about the implementation of the Ott-tool. We
also thank Stephanie Weirich for suggesting to separate the subgrammars
- of kinds and types in our Core-Haskell example.
-
-
-
-
+ of kinds and types in our Core-Haskell example.
*}