
diff -r be28f7b4b97b -r 468c3c1adcba Paper/Paper.thy
--- 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.  
 *}
 
 




