# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1270134052 -7200
# Node ID 731d39fb26b7583f012db0169dcbddd1aa360641
# Parent  d803c0adfcf8cae8d0e3454940635ae90b1d6d31
Update fv_bn definition for bindings allowed in types for which bn is present.

diff -r d803c0adfcf8 -r 731d39fb26b7 Paper/Paper.thy
--- a/Paper/Paper.thy	Thu Apr 01 16:55:34 2010 +0200
+++ b/Paper/Paper.thy	Thu Apr 01 17:00:52 2010 +0200
@@ -1179,16 +1179,17 @@
   we can determine whether the argument is a shallow or deep
   binder, and in the latter case also whether it is a recursive or
   non-recursive binder. 
-
-  \begin{center}
+  %
+  \begin{equation}\label{deepbinder}
+  \mbox{%
   \begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
   $\bullet$ & @{term "{}"} provided @{text "x\<^isub>i"} is a shallow binder\\
   $\bullet$ & @{text "fv_bn x\<^isub>i"} provided @{text "x\<^isub>i"} is a deep
       non-recursive binder with the auxiliary binding function @{text "bn"}\\
   $\bullet$ & @{text "fv_ty\<^isub>i x\<^isub>i - bn x\<^isub>i"} provided @{text "x\<^isub>i"} is
       a deep recursive binder with the auxiliary binding function @{text "bn"}
-  \end{tabular}
-  \end{center}
+  \end{tabular}}
+  \end{equation}
 
   \noindent
   The first clause states that shallow binders do not contribute to the
@@ -1230,38 +1231,24 @@
   a binder nor a body of an abstraction. In this case it is defined 
   as in \eqref{deepbody}, except that we do not need to subtract the 
   set @{text bnds}.
-  
-  Next, we need to define a free-variable function @{text "fv_bn\<^isub>j"} for 
-  each binding function @{text "bn\<^isub>j"}. The idea behind these
-  functions is to compute the set of free atoms that are not bound by 
-  @{text "bn\<^isub>j"}. Because of the restrictions we imposed on the 
-  form of binding functions, this can be done automatically by recursively 
-  building up the the set of free variables from the arguments that are 
-  not bound. Let us assume one clause of a binding function is 
-  @{text "bn\<^isub>j (C x\<^isub>1 \<dots> x\<^isub>n) = rhs"}, then @{text "fv_bn\<^isub>j (C x\<^isub>1 \<dots> x\<^isub>n)"} is the 
-  union of the values calculated for @{text "x\<^isub>i"} as follows:
+
+  The definitions of the free-variable functions for binding
+  functions are similar. For each binding function
+  @{text "bn\<^isub>j"} we need to define a free-variable function
+  @{text "fv_bn\<^isub>j"}. Given a term-constructor @{term "C"}, the
+  function @{text "fv_bn\<^isub>j(C x\<^isub>1 \<dots> x\<^isub>n)"} is the union of the
+  values calculated for the arguments. For each argument @{term "x\<^isub>i"}
+  we know whether it appears in the @{term "rhs"} of the binding
+  function equation @{text "bn\<^isub>j (C x\<^isub>1 \<dots> x\<^isub>n) = rhs"}. If it does not
+  appear in @{text "rhs"} we generate the premise according to the
+  rules for @{text "fv_ty"} described above in (\ref{deepbinder}--\ref{deepbody}). Otherwise:
 
   \begin{center}
   \begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
-  \multicolumn{2}{l}{@{text "x\<^isub>i"} occurs in @{text "rhs"}:}\\ 
-  $\bullet$ & @{term "{}"} provided @{term "x\<^isub>i"} is a single atom,
-     atom list or atom set\\
-  $\bullet$ & @{text "fv_bn x\<^isub>i"} in case @{text "rhs"} contains the 
-  recursive call @{text "bn x\<^isub>i"}\medskip\\
-  \end{tabular}
-  \end{center}
-
-  \begin{center}
-  \begin{tabular}{c@ {\hspace{2mm}}p{7cm}}
-  \multicolumn{2}{l}{@{text "x\<^isub>i"} does not occur in @{text "rhs"}:}\\
-  $\bullet$ & @{text "atom x\<^isub>i"} provided @{term "x\<^isub>i"} is an atom\\
-  $\bullet$ & @{text "atoms x\<^isub>i"} provided @{term "x\<^isub>i"} is a set of atoms\\
-  $\bullet$ & @{term "atoms (set x\<^isub>i)"} provided @{term "x\<^isub>i"} is a list of atoms\\
-  $\bullet$ & @{text "fv_ty\<^isub>i x\<^isub>i"} provided @{term "ty\<^isub>i"} is the type of @{text "x\<^isub>i"} and one of the raw
-     types corresponding to the types specified by the user\\
-%  $\bullet$ & @{text "fv_ty\<^isup>\<alpha> x\<^isub>i - bnds"} provided @{term "x\<^isub>i"}  is not in @{text "rhs"}
-%     and is an existing nominal datatype with the free-variable function @{text "fv\<^isup>\<alpha>"}\\
-  $\bullet$ & @{term "{}"} otherwise
+   $\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.
   \end{tabular}
   \end{center}