# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1269981075 -7200
# Node ID 1801cc460fc92734ac50a7b6b24cae7d09d48fd2
# Parent  8c788ad717524eed9d7c6eb43752134cde140f84
polished and added an example for fvars

diff -r 8c788ad71752 -r 1801cc460fc9 Paper/Paper.thy
--- a/Paper/Paper.thy	Tue Mar 30 21:15:13 2010 +0200
+++ b/Paper/Paper.thy	Tue Mar 30 22:31:15 2010 +0200
@@ -1054,24 +1054,25 @@
   Note that in the last example we wrote {\it\isacommand{bind}\;bn(p)\;\isacommand{in}\;p}.
   Whenever such a binding clause is present, we will call the binder \emph{recursive}.
   To see the purpose for this, compare ``plain'' Lets and Let\_recs:
-
-  \begin{center}
+  %
+  \begin{equation}\label{letrecs}
+  \mbox{%
   \begin{tabular}{@ {}l@ {}}
-  \isacommand{nominal\_datatype} {\it trm} =\\
+  \isacommand{nominal\_datatype}~@{text "trm ="}\\
   \hspace{5mm}\phantom{$\mid$}\ldots\\
-  \hspace{5mm}$\mid$ Let\;{\it a::assn}\; {\it t::trm} 
-     \;\;\isacommand{bind} {\it bn(a)} \isacommand{in} {\it t}\\
-  \hspace{5mm}$\mid$ Let\_rec\;{\it a::assn}\; {\it t::trm} 
-     \;\;\isacommand{bind} {\it bn(a)} \isacommand{in} {\it t},
-         \isacommand{bind} {\it bn(a)} \isacommand{in} {\it a}\\
+  \hspace{5mm}$\mid$~@{text "Let as::assn t::trm"} 
+     \;\;\isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text t}\\
+  \hspace{5mm}$\mid$~@{text "Let_rec as::assn t::trm"} 
+     \;\;\isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text t},
+         \isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text as}\\
   \isacommand{and} {\it assn} =\\
-  \hspace{5mm}\phantom{$\mid$} ANil\\
-  \hspace{5mm}$\mid$ ACons\;{\it name}\;{\it trm}\;{\it assn}\\
-  \isacommand{with} {\it bn::assn $\Rightarrow$ atom list}\\
-  \isacommand{where} $bn(\textrm{ANil}) = []$\\
-  \hspace{5mm}$\mid$ $bn(\textrm{ACons}\;x\;t\;a) = [atom\; x]\; @\; bn(a)$\\
-  \end{tabular}
-  \end{center}
+  \hspace{5mm}\phantom{$\mid$}~@{text "ANil"}\\
+  \hspace{5mm}$\mid$~@{text "ACons name trm assn"}\\
+  \isacommand{with} @{text "bn::assn \<Rightarrow> atom list"}\\
+  \isacommand{where}~@{text "bn(ANil) = []"}\\
+  \hspace{5mm}$\mid$~@{text "bn(ACons a t as) = [atom a] @ bn(as)"}\\
+  \end{tabular}}
+  \end{equation}
 
   \noindent
   The difference is that with Let we only want to bind the atoms @{text
@@ -1237,6 +1238,45 @@
   \end{tabular}
   \end{center}
 
+  \noindent
+  To see how these definitions work, let us consider the term-constructors 
+  for @{text "Let"} and @{text "Let_rec"} from example shown in \eqref{letrecs}. 
+  For this specification we need to define three functions, namely
+  @{text "fv\<^bsub>trm\<^esub>"}, @{text "fv\<^bsub>assn\<^esub>"} and @{text "fv\<^bsub>bn\<^esub>"}. 
+  %
+  \begin{center}
+  \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
+  @{text "fv\<^bsub>trm\<^esub> (Let as t)"} & @{text "="} & @{text "fv\<^bsub>bn\<^esub> as \<union> (fv\<^bsub>trm\<^esub> t - set (bn as))"}\\
+  @{text "fv\<^bsub>trm\<^esub> (Let_rec as t)"} & @{text "="} &\\
+  \multicolumn{3}{r}{@{text "(fv\<^bsub>assn\<^esub> as - set (bn as)) \<union> (fv\<^bsub>trm\<^esub> t - set (bn as))"}}\\[1mm]
+
+  @{text "fv\<^bsub>assn\<^esub> (ANil)"} & @{text "="} & @{text "[]"}\\
+  @{text "fv\<^bsub>assn\<^esub> (ACons a t as)"} & @{text "="} & @{text "{atom a} \<union> (fv\<^bsub>trm\<^esub> t) \<union> (fv\<^bsub>assn\<^esub> as)"}\\[1mm]
+
+  @{text "fv\<^bsub>bn\<^esub> (ANil)"} & @{text "="} & @{text "[]"}\\
+  @{text "fv\<^bsub>bn\<^esub> (ACons a t as)"} & @{text "="} & @{text "(fv\<^bsub>trm\<^esub> t) \<union> (fv\<^bsub>bn\<^esub> as)"}
+  \end{tabular}
+  \end{center}
+
+  \noindent
+  Since there are no binding clauses for the term-constructors @{text ANil}
+  and @{text "ACons"}, the corresponding free-variable function @{text
+  "fv\<^bsub>assn\<^esub>"} returns all atoms occuring in an assignment. The
+  binding happens in @{text Let} and @{text "Let_rec"}. In the first clause we
+  want to bind all atoms given by @{text "set (bn as)"} in @{text
+  t}. Therefore we have to subtract @{text "set (bn as)"} from @{text
+  "fv\<^bsub>trm\<^esub> t"}. However, we also need to add all atoms that are
+  free in @{text "as"}. This is what the purpose of the function @{text
+  "fv\<^bsub>bn\<^esub>"} is.  In contrast, in @{text "Let_rec"} we have a
+  recursive binder where we want to also bind all occurences of atoms inside
+  @{text "as"}. Therefore we have to subtract @{text "set (bn as)"} from
+  @{text "fv\<^bsub>assn\<^esub> as"}. Similarly for @{text
+  "fv\<^bsub>trm\<^esub> t - bn as"}. An interesting point in this example is
+  that an assignment ``alone'' does not have any bound variables. Only in the
+  context of a @{text Let} pr @{text "Let_rec"} will some atoms occuring in an
+  assignment become bound. This is a phenomenon that has also been pointed out
+  in \cite{ott-jfp}.
+
   We then define the alpha equivalence relations. For the types @{text "ty\<^isub>1, \<dots>, ty\<^isub>n"}
   we need to define