# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1269948192 -7200
# Node ID 40f13b52b107d459e5927c3f2b76e52fe8507260
# Parent  55cb244b020cd985d74d6d8e28f4f255334f614d# Parent  88b33de74e61f273c23ea5b13cb4162bac49f426
merged

diff -r 55cb244b020c -r 40f13b52b107 Paper/Paper.thy
--- a/Paper/Paper.thy	Tue Mar 30 13:22:54 2010 +0200
+++ b/Paper/Paper.thy	Tue Mar 30 13:23:12 2010 +0200
@@ -1158,26 +1158,27 @@
   \noindent
   In case the argument @{text "x\<^isub>i"} is not a binder, it might be a body of
   one or more abstractions. Let @{text "bnds"} be the bound atoms computed
-  as follows: If @{text "x\<^isub>i"} is not a body of an abstraction @{text "{}"}.
+  as follows: If @{text "x\<^isub>i"} is not a body of an abstraction @{term "{}"}.
   Otherwise there are two cases: either the
   corresponding binders are all shallow or there is a single deep binder.
   In the former case we build the union of all shallow binders; in the
   later case we just take set or list of atoms the specified binding
   function returns. With @{text "bnds"} computed as above the value of
-  for @{text "x\<^isub>i"} is given by:  
- 
+  for @{text "x\<^isub>i"} is given by:
+
   \begin{center}
   \begin{tabular}{cp{7cm}}
   $\bullet$ & @{text "{atom x\<^isub>i} - bnds"} provided @{term "x\<^isub>i"} is an atom\\
   $\bullet$ & @{text "(atoms x\<^isub>i) - bnds"} provided @{term "x\<^isub>i"} is a set of atoms\\
   $\bullet$ & @{text "(atoms (set x\<^isub>i)) - bnds"} provided @{term "x\<^isub>i"} is a list of atoms\\
-  $\bullet$ & @{text "(fv_ty\<^isub>i x\<^isub>i) - bnds"} provided @{term "ty\<^isub>i"} is a nominal datatype\\
-  $\bullet$ & @{term "{}"} otherwise 
+  $\bullet$ & @{text "(fv_ty\<^isub>m x\<^isub>i) - bnds"} provided @{term "x\<^isub>i"} is one of the datatypes
+     we are defining, with the free variable function @{text "fv_ty\<^isub>m"}\\
+  $\bullet$ & @{text "(fv\<^isup>\<alpha> x\<^isub>i) - bnds"} provided @{term "x\<^isub>i"} is a defined nominal datatype
+     with a free variable function @{text "fv\<^isup>\<alpha>"}\\\\
+  $\bullet$ & @{term "{}"} otherwise
   \end{tabular}
   \end{center}
 
-\marginpar{\small We really have @{text "bn_raw"}, @{text "fv_bn_raw"}. Should we mention this?}
-
   \noindent Next, for each binding function @{text "bn"} we define a
   free variable function @{text "fv_bn"}. The basic idea behind this
   function is to compute all the free atoms under this binding
@@ -1189,18 +1190,19 @@
   we define @{text "fv_bn"} to be the union of the values calculated
   for @{text "x\<^isub>j"} as follows:
 
- \marginpar{raw for being defined}
-
   \begin{center}
   \begin{tabular}{cp{7cm}}
-  $\bullet$ & @{term "{}"} provided @{term "x\<^isub>j"} occurs in @{text "rhs"} and is an atom\\
+  $\bullet$ & @{term "{}"} provided @{term "x\<^isub>j"} occurs in @{text "rhs"} and is an atom,
+     atom list or atom set\\
   $\bullet$ & @{text "fv_bn\<^isub>m x\<^isub>j"} provided @{term "x\<^isub>j"} occurs in @{text "rhs"} 
     with the recursive call @{text "bn\<^isub>m x\<^isub>j"}\\
-  $\bullet$ & @{text "(atoms x\<^isub>j) - bnds"} provided @{term "x\<^isub>j"} is a set of atoms\\
-  $\bullet$ & @{text "(atoml x\<^isub>j) - bnds"} provided @{term "x\<^isub>j"} is a list of atoms\\
-  $\bullet$ & @{text "(fv_ty x\<^isub>j) - bnds"} provided @{term "x\<^isub>j"} is a nominal datatype
-    with a free variable function @{text "fv_ty"}. This includes the types being
-    defined, where we use an appropriate @{term "fv_ty\<^isub>i"} function.\\
+  $\bullet$ & @{text "atoms x\<^isub>j"} provided @{term "x\<^isub>j"} is a set of atoms not in @{text "rhs"}\\
+  $\bullet$ & @{term "atoml x\<^isub>j"} provided @{term "x\<^isub>j"} is a list of atoms not in @{text "rhs"}\\
+  $\bullet$ & @{text "fv_ty\<^isub>i x\<^isub>j"} provided @{term "x\<^isub>j"} is not in @{text "rhs"} and is 
+     one of the datatypes
+     we are defining, with the free variable function @{text "fv_ty\<^isub>m"}\\
+  $\bullet$ & @{text "fv_ty\<^isup>\<alpha> x\<^isub>j - bnds"} provided @{term "x\<^isub>j"}  is not in @{text "rhs"}
+     and is an existing nominal datatype with the free variable function @{text "fv\<^isup>\<alpha>"}\\
   $\bullet$ & @{term "{}"} otherwise
   \end{tabular}
   \end{center}
@@ -1219,10 +1221,10 @@
   @{text "\<approx>bn\<^isub>1 :: ty\<^isub>i\<^isub>1 \<Rightarrow> ty\<^isub>i\<^isub>1 \<Rightarrow> bool \<dots> \<approx>bn\<^isub>n :: ty\<^isub>i\<^isub>m \<Rightarrow> ty\<^isub>i\<^isub>m \<Rightarrow> bool"}
   \end{center}
 
-  Given a term-constructor @{text "C ty\<^isub>1 \<dots> ty\<^isub>n"}, of a type @{text ty}, two instances
-  of this constructor are alpha-equivalent @{text "C x\<^isub>1 \<dots> x\<^isub>n \<approx> C y\<^isub>1 \<dots> y\<^isub>n"} if there
+  Given a term-constructor @{text "C_raw ty\<^isub>1 \<dots> ty\<^isub>n"}, of a type @{text ty}, two instances
+  of this constructor are alpha-equivalent @{text "C_raw x\<^isub>1 \<dots> x\<^isub>n \<approx> C_raw y\<^isub>1 \<dots> y\<^isub>n"} if there
   exist permutations @{text "\<pi>\<^isub>1 \<dots> \<pi>\<^isub>p"} (one for each bound argument) such that
-  the conjunction of equivalences for each argument pair @{text "x\<^isub>j"}, @{text "y\<^isub>j"} holds.
+  the conjunction of equivalences defined below for each argument pair @{text "x\<^isub>j"}, @{text "y\<^isub>j"} holds.
   For an argument pair @{text "x\<^isub>j"}, @{text "y\<^isub>j"} this holds if:
 
   \begin{center}
@@ -1234,14 +1236,14 @@
      provided @{term "x\<^isub>j"} is a deep recursive binder with the auxiliary binding
      function @{text "bn\<^isub>m"} and permutation @{text "\<pi>"}, @{term "fvs"} is a compound
      free variable function returning the union of appropriate @{term "fv_ty\<^isub>x"} and
-     @{term "R"} is the composition of equivalence relations @{text "\<approx>"} and @{text "\<approx>n"}\\
+     @{term "R"} is the composition of equivalence relations @{text "\<approx>"} and @{text "\<approx>\<^isub>n"}\\
   $\bullet$ & @{text "x\<^isub>j"} has a deep recursive binding\\
-  $\bullet$ & @{term "(x\<^isub>n, x\<^isub>j) \<approx>gen R fv_ty \<pi> (y\<^isub>n, y\<^isub>j)"} provided @{text "x\<^isub>n"}
-     is bound in @{text "x\<^isub>j"} with permutation @{text "\<pi>"}, @{term "R"} is the
+  $\bullet$ & @{term "({x\<^isub>n, x\<^isub>j) \<approx>gen R fv_ty \<pi> (y\<^isub>n, y\<^isub>j)"} provided @{text "x\<^isub>j"} has
+     a shallow binder @{text "x\<^isub>n"} with permutation @{text "\<pi>"}, @{term "R"} is the
      alpha-equivalence for @{term "x\<^isub>j"}
      and @{term "fv_ty"} is the free variable function for @{term "x\<^isub>j"}\\
-  $\bullet$ & @{term "(bn\<^isub>m x\<^isub>n, x\<^isub>j) \<approx>gen R fv_ty \<pi> (bn\<^isub>m y\<^isub>n, y\<^isub>j)"} provided  @{text "bn\<^isub>m x\<^isub>n"}
-    is bound non-recursively in @{text "x\<^isub>j"} with permutation @{text "\<pi>"}, @{term "R"} is the
+  $\bullet$ & @{term "(bn\<^isub>m x\<^isub>n, x\<^isub>j) \<approx>gen R fv_ty \<pi> (bn\<^isub>m y\<^isub>n, y\<^isub>j)"} provided @{text "x\<^isub>j"}
+     has a deep non-recursive binder @{text "bn\<^isub>m x\<^isub>n"} with permutation @{text "\<pi>"}, @{term "R"} is the
      alpha-equivalence for @{term "x\<^isub>j"}
      and @{term "fv_ty"} is the free variable function for @{term "x\<^isub>j"}\\
   $\bullet$ & @{text "x\<^isub>j \<approx>\<^isub>j y\<^isub>j"} for a nominal datatype with no bindings (this includes
@@ -1254,8 +1256,8 @@
   for their respective types, the difference is that they ommit checking the arguments that
   are bound. We assumed that there are no bindings in the type on which the binding function
   is defined so, there are no permutations involved. For a binding function clause 
-  @{text "bn (C x\<^isub>1 \<dots> x\<^isub>n) = rhs"}, two instances of the constructor are equivalent
-  @{text "C x\<^isub>1 \<dots> x\<^isub>n \<approx> C y\<^isub>1 \<dots> y\<^isub>n"} if:
+  @{text "bn (C_raw x\<^isub>1 \<dots> x\<^isub>n) = rhs"}, two instances of the constructor are equivalent
+  @{text "C_raw x\<^isub>1 \<dots> x\<^isub>n \<approx> C_raw y\<^isub>1 \<dots> y\<^isub>n"} if:
   \begin{center}
   \begin{tabular}{cp{7cm}}
   $\bullet$ & @{text "x\<^isub>j"} is not a nominal datatype and occurs in @{text "rhs"}\\