366   conditions for alpha-equated terms. We are also able to derive, at the moment 

   366   conditions for alpha-equated terms. We are also able to derive, for the moment 

   493   We also use for sets of atoms the abbreviation 

   493   We use for sets of atoms the abbreviation 

   685   We set @{text R} to be the equality and for @{text "fv(T)"} we define

   685   We set @{text R} to be the usual equality @{text "="} and for @{text "fv(T)"} we define

   767   representing alpha-equivalence classes of pairs. The elements in these types 

   767   representing alpha-equivalence classes of pairs of type 

   768   will be, respectively, written as:

   768   @{text "(atom set) \<times> \<beta>"} (in the first two cases) and of type @{text "(atom list) \<times> \<beta>"}. 

   769   The elements in these types will be, respectively, written as:

   772   @{term "Abs_lst as x"} \hspace{5mm}

   773   @{term "Abs_res as x"} \hspace{5mm}

   773   @{term "Abs_res as x"}

   774   @{term "Abs_lst as x"} 

   787   @{thm (lhs) supp_abs(3)[where bs="as", no_vars]} & $=$ & @{thm (rhs) supp_abs(3)[where bs="as", no_vars]}\\

   788   @{thm (lhs) supp_abs(2)[no_vars]} & $=$ & @{thm (rhs) supp_abs(2)[no_vars]}\\

   788   @{thm (lhs) supp_abs(2)[no_vars]} & $=$ & @{thm (rhs) supp_abs(2)[no_vars]}

   789   @{thm (lhs) supp_abs(3)[where bs="as", no_vars]} & $=$ & @{thm (rhs) supp_abs(3)[where bs="as", no_vars]}

   854   using \eqref{suppfun}. Assuming @{term "supp x - as"} is a finite set

   855   using \eqref{suppfun}. Assuming @{term "supp x - as"} is a finite set,

   900   \isacommand{with} @{text "bn\<AL>\<^isub>1"} \isacommand{and} \ldots \isacommand{and} @{text "bn\<AL>\<^isub>m"}\\

   901   \isacommand{binder} @{text "bn\<AL>\<^isub>1"} \isacommand{and} \ldots \isacommand{and} @{text "bn\<AL>\<^isub>m"}\\

   946   clause will be called \emph{body}; the ``\isacommand{bind}-part'' will

   947   clause will be called \emph{bodies} (there can be more than one); the 

   947   be called \emph{binder}.

   948   ``\isacommand{bind}-part'' will be called \emph{binders}. A body can only occur 

   949   in \emph{one} binding clause. A binder, in contrast, may occur in several binding 

   950   clauses, but cannot occur as a body.

   979   If we have shallow binders that ``share'' a body, for instance $t$ in

   982   Shallow binders may also ``share'' several bodies, for instance @{text t} 

   980   the following term-constructor

   983   and @{text s} in the following term-constructor

   984   @{text "Foo x::name y::name t::lam"} &  

   987   @{text "Foo x::name y::name t::lam s::lam"} &  

   985       \isacommand{bind} @{text x} \isacommand{in} @{text t},\;

   988       \isacommand{bind} @{text "x y"} \isacommand{in} @{text "t s"}  

   986       \isacommand{bind} @{text y} \isacommand{in} @{text t}  

   989   \end{tabular}

   987   \end{tabular}

   990   \end{center}

   988   \end{center}

   989 

   990   \noindent

   991   then we have to make sure the modes of the binders agree. We cannot

   992   have, for instance, in the first binding clause the mode \isacommand{bind} 

   993   and in the second \isacommand{bind\_set}.

  1020   \isacommand{with}~@{text "bn::pat \<Rightarrow> atom list"}\\

  1017   \isacommand{binder}~@{text "bn::pat \<Rightarrow> atom list"}\\

  1049   @{text "Foo p::pat q::pat t::trm"} & 

  1046   @{text "Foo\<^isub>1 p::pat q::pat t::trm"} & 

  1050      \isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text t},\;

  1047      \isacommand{bind} @{text "bn(p) bn(q)"} \isacommand{in} @{text t}\\

  1051      \isacommand{bind} @{text "bn(q)"} \isacommand{in} @{text t}\\

  1048   @{text "Foo\<^isub>2 x::name p::pat t::trm"} & 

  1052   @{text "Foo' x::name p::pat t::trm"} & 

  1049      \isacommand{bind} @{text "x bn(p)"} \isacommand{in} @{text t}\\ 

  1053      \isacommand{bind} @{text x} \isacommand{in} @{text t},\;

  1050   \end{tabular}

  1054      \isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text t} 

  1051   \end{center}

  1055   \end{tabular}

  1052 

  1056   \end{center}

  1053   \noindent

  1057 

  1054   In the first case the intention is to bind all atoms from the pattern @{text p} in @{text t}

  1058   \noindent

  1055   and also all atoms from @{text q} in @{text t}. Unfortunately, we have no way

  1059   In the first case we might bind all atoms from the pattern @{text p} in @{text t}

  1060   and also all atoms from @{text q} in @{text t}. As a result we have no way

  1069   @{text "Bar p::pat t::trm s::trm"} & 

  1064   @{text "Bar\<^isub>1 p::pat t::trm s::trm"} & 

  1070      \isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text t},\;

  1065      \isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text "t s"}\\

  1071      \isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text s}\\

  1066   @{text "Bar\<^isub>2 p::pat t::trm"} &  

  1072   @{text "Bar' p::pat t::trm"} &  

  1067      \isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text "p t"}\\

  1073      \isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text p},\;

  1074      \isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text t}\\

  1081   Note that in the last example we wrote {\it\isacommand{bind}\;bn(p)\;\isacommand{in}\;p}.

  1074   Note that in the last example we wrote \isacommand{bind}~@{text "bn(p)"}~\isacommand{in}~@{text "p.."}.

  1093   \hspace{5mm}$\mid$~@{text "Let_rec as::assn t::trm"}\\ 

  1086   \hspace{5mm}$\mid$~@{text "Let_rec as::assn t::trm"}

  1094   \hspace{20mm}\isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text t},

  1087      \;\;\isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text "as t"}\\

  1095          \isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text as}\\

  1088   \isacommand{and} @{text "ass"} =\\

  1096   \isacommand{and} {\it assn} =\\

  1099   \isacommand{with} @{text "bn::assn \<Rightarrow> atom list"}\\

  1091   \isacommand{binder} @{text "bn::assn \<Rightarrow> atom list"}\\

  1115   Pottier and Cheney pointed out \cite{Pottier06,Cheney5}, we cannot in general 

  1131   Pottier and Cheney pointed out \cite{Pottier06,Cheney05}, by just 

  1116   re-arrange arguments of

  1132   re-arranging the arguments of

  1118   then use the type constructors @{text "abs_set"}, @{text "abs_res"} and

  1134   then use directly the type constructors @{text "abs_set"}, @{text "abs_res"} and

  1119   @{text "abs_list"} from Section \ref{sec:binders}. Therefore we will first

  1135   @{text "abs_list"} from Section \ref{sec:binders}, will result in an inadequate

  1136   representatation. Therefore we will first

  1155   functions from the specifications. Given the raw types @{text "ty\<^isub>1 \<dots> ty\<^isub>n"}

  1172   functions from the specifications. For atomic types we define the auxilary

  1156   we need to define free-variable functions

  1173   free variable functions:

  1157 

  1174 

  1158   \begin{center}

  1175   \begin{center}

  1159   @{text "fv_ty\<^isub>1, \<dots>, fv_ty\<^isub>n"}

  1176   \begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}

  1160   \end{center}

  1177   @{text "fv_atom a"} & @{text "="} & @{text "atom a"}\\

  1161 

  1178   @{text "fv_atom_set as"} & @{text "="} & @{text "atoms as"}\\

  1162   \noindent

  1179   @{text "fv_atom_list as"} & @{text "="} & @{text "atoms (set as)"}\\

  1163   We define them together with auxiliary free-variable functions for

  1180   \end{tabular}

  1164   the binding functions. Given binding functions 

  1181   \end{center}

  1165   @{text "bn\<^isub>1 \<dots> bn\<^isub>m"} we define

  1166   %

  1167   \begin{center}

  1168   @{text "fv_bn\<^isub>1, \<dots>, fv_bn\<^isub>m"}

  1169   \end{center}

  1170 

  1171   \noindent

  1172   The reason for this setup is that in a deep binder not all atoms have to be

  1173   bound, as we saw in the example with ``plain'' @{text Let}s. We need therefore a function

  1174   that calculates those unbound atoms. 

  1175 

  1176   While the idea behind these

  1177   free-variable functions is clear (they just collect all atoms that are not bound),

  1178   because of our rather complicated binding mechanisms their definitions are

  1179   somewhat involved.

  1180   Given a term-constructor @{text "C"} of type @{text ty} with argument types

  1181   \mbox{@{text "ty\<^isub>1 \<dots> ty\<^isub>n"}}, the function

  1182   @{text "fv_ty (C x\<^isub>1 \<dots> x\<^isub>n)"} will be the union of the values, @{text v},

  1183   calculated below for each argument. 

  1184   First we deal with the case that @{text "x\<^isub>i"} is a binder. From the binding clauses, 

  1185   we can determine whether the argument is a shallow or deep

  1186   binder, and in the latter case also whether it is a recursive or

  1187   non-recursive binder. 

  1188   %

  1189   \begin{equation}\label{deepbinder}

  1190   \mbox{%

  1191   \begin{tabular}{c@ {\hspace{2mm}}p{7cm}}

  1192   $\bullet$ & @{term "v = {}"} provided @{text "x\<^isub>i"} is a shallow binder\\

  1193   $\bullet$ & @{text "v = fv_bn x\<^isub>i"} provided @{text "x\<^isub>i"} is a deep

  1194       non-recursive binder with the auxiliary binding function @{text "bn"}\\

  1195   $\bullet$ & @{text "v = fv_ty\<^isub>i x\<^isub>i - bn x\<^isub>i"} provided @{text "x\<^isub>i"} is

  1196       a deep recursive binder with the auxiliary binding function @{text "bn"}

  1197   \end{tabular}}

  1198   \end{equation}

  1199 

  1200   \noindent

  1201   The first clause states that shallow binders do not contribute to the

  1202   free variables; in the second clause, we have to collect all

  1203   variables that are left unbound by the binding function @{text "bn"}---this

  1204   is done with function @{text "fv_bn"}; in the third clause, since the 

  1205   binder is recursive, we need to bind all variables specified by 

  1206   @{text "bn"}---therefore we subtract @{text "bn x\<^isub>i"} from the free

  1207   variables of @{text "x\<^isub>i"}.

  1208 

  1209   In case the argument is \emph{not} a binder, we need to consider 

  1210   whether the @{text "x\<^isub>i"} is the body of one or more binding clauses. 

  1211   In this case we first calculate the set @{text "bnds"} as follows: 

  1212   either the corresponding binders are all shallow or there is a single deep binder.

  1213   In the former case we take @{text bnds} to be the union of all shallow 

  1214   binders; in the latter case, we just take the set of atoms specified by the 

  1215   corresponding binding function. The value for @{text "x\<^isub>i"} is then given by:

  1216   %

  1217   \begin{equation}\label{deepbody}

  1218   \mbox{%

  1219   \begin{tabular}{c@ {\hspace{2mm}}p{7cm}}

  1220   $\bullet$ & @{text "v = {atom x\<^isub>i} - bnds"} provided @{term "x\<^isub>i"} is an atom\\

  1221   $\bullet$ & @{text "v = (atoms x\<^isub>i) - bnds"} provided @{term "x\<^isub>i"} is a set of atoms\\

  1222   $\bullet$ & @{text "v = (atoms (set x\<^isub>i)) - bnds"} provided @{term "x\<^isub>i"} is a list of atoms\\

  1223   $\bullet$ & @{text "v = (fv_ty\<^isub>i x\<^isub>i) - bnds"} provided @{term "ty\<^isub>i"} is one of the raw datatypes

  1224      corresponding to the types specified by the user\\

  1225 %  $\bullet$ & @{text "(fv\<^isup>\<alpha> x\<^isub>i) - bnds"} provided @{term "x\<^isub>i"} is a defined nominal datatype

  1226 %     with a free-variable function @{text "fv\<^isup>\<alpha>"}\\

  1227   $\bullet$ & @{term "v = {}"} otherwise

  1228   \end{tabular}}

  1229   \end{equation}

  1236   The last case we need to consider is when @{text "x\<^isub>i"} is neither

  1188   Given the raw types @{text "ty\<^isub>1 \<dots> ty\<^isub>n"}

  1237   a binder nor a body of an abstraction. In this case it is defined 

  1189   we define now free-variable functions

  1238   as in \eqref{deepbody}, except that we do not need to subtract the 

  1190 

  1239   set @{text bnds}.

  1191   \begin{center}

  1240 

  1192   @{text "fv_ty\<^isub>1, \<dots>, fv_ty\<^isub>n"}

  1241   The definitions of the free-variable functions for binding

  1193   \end{center}

  1242   functions are similar. For each binding function

  1194 

  1243   @{text "bn\<^isub>j"} we need to define a free-variable function

  1195   \noindent

  1244   @{text "fv_bn\<^isub>j"}. Given a term-constructor @{term "C"}, the

  1196   We define them together with auxiliary free-variable functions for

  1245   function @{text "fv_bn\<^isub>j(C x\<^isub>1 \<dots> x\<^isub>n)"} is the union of the

  1197   the binding functions. Given binding functions 

  1246   values calculated for the arguments. For each argument @{term "x\<^isub>i"}

  1198   @{text "bn\<^isub>1 \<dots> bn\<^isub>m"} we define

  1247   we know whether it appears in the @{term "rhs"} of the binding

  1199   %

  1248   function equation @{text "bn\<^isub>j (C x\<^isub>1 \<dots> x\<^isub>n) = rhs"}. If it does not

  1200   \begin{center}

  1249   appear in @{text "rhs"} we generate the premise according to the

  1201   @{text "fv_bn\<^isub>1, \<dots>, fv_bn\<^isub>m"}

  1250   rules for @{text "fv_ty"} described above in (\ref{deepbinder}--\ref{deepbody}). Otherwise:

  1202   \end{center}

  1251 

  1203 

  1252   \begin{center}

  1204   \noindent

  1205   The reason for this setup is that in a deep binder not all atoms have to be

  1206   bound, as we saw in the example with ``plain'' @{text Let}s. We need therefore a function

  1207   that calculates those unbound atoms. 

  1208 

  1209   While the idea behind these free-variable functions is clear (they just

  1210   collect all atoms that are not bound), because of our rather complicated

  1211   binding mechanisms their definitions are somewhat involved.  Given a

  1212   term-constructor @{text "C"} of type @{text ty} and some associated binding

  1213   clauses, the function @{text "fv_ty (C x\<^isub>1 \<dots> x\<^isub>n)"} will be

  1214   the union of the values, @{text v}, calculated below for each binding

  1215   clause. 

  1216 

  1217   \begin{equation}\label{deepbinder}

  1218   \mbox{%

  1254    $\bullet$ & @{text "v = fv_bn x\<^isub>i"} provided @{text "rhs"} contains the

  1220   \multicolumn{2}{@ {}l}{Empty binding clauses of the form 

  1255     recursive call @{text "bn x\<^isub>i"}\medskip\\

  1221   \isacommand{bind\_set}~@{term "{}"}~\isacommand{in}~@{text "y"}:}\\ 

  1256   $\bullet$ & @{term "v = {}"} provided @{text "rhs"} contains

  1222   $\bullet$ & @{term "v = fv_ty y"} provided @{text "y"} is of type @{text "ty"}\smallskip\\

  1257     @{term "x\<^isub>i"} and @{term "x\<^isub>i"} is of atom type.

  1223   \multicolumn{2}{@ {}l}{Shallow binders of the form 

  1258   \end{tabular}

  1224   \isacommand{bind\_set}~@{text "x\<^isub>1\<dots>x\<^isub>n"}~\isacommand{in}~@{text "y\<^isub>1\<dots>y\<^isub>m"}:}\\ 

  1259   \end{center}

  1225   $\bullet$ & @{text "v = (fv_ty\<^isub>1 y\<^isub>1 \<union> fv_ty\<^isub>m y\<^isub>m) - (x\<^isub>1 \<union> \<dots> \<union> x\<^isub>n)"} 

  1260 

  1226      provided the @{text "y\<^isub>i"} are of type @{text "ty\<^isub>i"}\smallskip\\

  1261   \noindent

  1227   \multicolumn{2}{@ {}l}{Deep binders of the form 

  1228   \isacommand{bind\_set}~@{text "bn x"}~\isacommand{in}~@{text "y\<^isub>1\<dots>y\<^isub>m"}:}\\ 

  1229   $\bullet$ & @{text "v = (fv_ty\<^isub>1 y\<^isub>1 \<union> fv_ty\<^isub>m y\<^isub>m) - (bn x) \<union> (fv_bn x)"}\\

  1230   $\bullet$ & @{text "v = (fv_ty\<^isub>1 y\<^isub>1 \<union> fv_ty\<^isub>m y\<^isub>m) - (bn x)"}\\

  1231      & provided the @{text "y\<^isub>i"} are of type @{text "ty\<^isub>i"}; the first 

  1232     clause applies for @{text x} being a non-recursive deep binder, the 

  1233     second for a recursive deep binder

  1234   \end{tabular}}

  1235   \end{equation}

  1236 

  1237   \noindent

  1238   Similarly for the other binding modes. Note that in a non-recursive deep

  1239   binder, we have to add all atoms that are left unbound by the binding

  1240   function @{text "bn"}. For this we use the function @{text "fv_bn"}. Assume

  1241   for the constructor @{text "C"} the binding function equation is of the form @{text

  1242   "bn\<^isub>j (C x\<^isub>1 \<dots> x\<^isub>n) = rhs"}. We again define a value

  1243   @{text v} which is exactly as in \eqref{deepbinder} for shallow and deep

  1244   binders. We only modify the clause for empty binding clauses as follows:

  1245 

  1246 

  1247   \begin{equation}\label{bnemptybinder}

  1248   \mbox{%

  1249   \begin{tabular}{c@ {\hspace{2mm}}p{7cm}}

  1250   \multicolumn{2}{@ {}l}{Empty binding clauses of the form 

  1251   \isacommand{bind\_set}~@{term "{}"}~\isacommand{in}~@{text "y"}:}\\ 

  1252   $\bullet$ & @{term "v = fv_ty\<^isub>i y"} provided @{text "y"} does not occur in @{text "rhs"}

  1253   and the free-variable function for the type of @{text "y"} is @{text "fv_ty\<^isub>i"}\\

  1254   $\bullet$ & @{term "v = fv_bn\<^isub>i y"} provided @{text "y"} occurs in  @{text "rhs"}

  1255   with a recursive call @{text "bn\<^isub>i y"}\\

  1256   $\bullet$ & @{term "v = {}"} provided @{text "y"} occurs in  @{text "rhs"},

  1257   but without a recursive call\\

  1258   \end{tabular}}

  1259   \end{equation}

  1260 

  1261   \noindent

  1262   The reason why we only have to treat the empty binding clauses specially in

  1263   the definition of @{text "fv_bn"} is that binding functions can only use arguments

  1264   that do not occur in binding clauses. Otherwise the @{text "bn"} function cannot

  1265   be lifted to alpha-equated terms.

  1266 

  1267 

  1269   @{text "fv\<^bsub>trm\<^esub> (Let as t)"} & @{text "="} & @{text "fv\<^bsub>bn\<^esub> as \<union> (fv\<^bsub>trm\<^esub> t - set (bn as))"}\\

  1275   @{text "fv\<^bsub>trm\<^esub> (Let as t)"} & @{text "="} & @{text "(fv\<^bsub>trm\<^esub> t - set (bn as)) \<union> fv\<^bsub>bn\<^esub> as"}\\

  1270   @{text "fv\<^bsub>trm\<^esub> (Let_rec as t)"} & @{text "="} &\\

  1276   @{text "fv\<^bsub>trm\<^esub> (Let_rec as t)"} & @{text "="} & @{text "(fv\<^bsub>assn\<^esub> as \<union> fv\<^bsub>trm\<^esub> t) - set (bn as)"}\\[1mm]

  1271   \multicolumn{3}{r}{@{text "(fv\<^bsub>assn\<^esub> as - set (bn as)) \<union> (fv\<^bsub>trm\<^esub> t - set (bn as))"}}\\[1mm]

  1277 

  1272 

  1278   @{text "fv\<^bsub>assn\<^esub> (ANil)"} & @{text "="} & @{term "{}"}\\

  1273   @{text "fv\<^bsub>assn\<^esub> (ANil)"} & @{text "="} & @{text "[]"}\\

  1276   @{text "fv\<^bsub>bn\<^esub> (ANil)"} & @{text "="} & @{text "[]"}\\

  1281   @{text "fv\<^bsub>bn\<^esub> (ANil)"} & @{text "="} & @{term "{}"}\\

  1282   Since there are no binding clauses for the term-constructors @{text ANil}

  1287   Since there are only (implicit) empty binding clauses for the term-constructors @{text ANil}

  1293   "set (bn as)"} from @{text "fv\<^bsub>assn\<^esub> as"}, as well as from

  1298   "set (bn as)"} from @{text "fv\<^bsub>trm\<^esub> t"}, as well as from

  1294   @{text "fv\<^bsub>trm\<^esub> t"}. An interesting point in this example is

  1299   @{text "fv\<^bsub>assn\<^esub> as"}. An interesting point in this example is

  1298   that has also been pointed out in \cite{ott-jfp}. We can also see that

  1303   that has also been pointed out in \cite{ott-jfp}. For us it is crucial, because

  1304   we would not be able to lift a @{text "bn"}-function that is defined over 

  1305   arguments that are either binders or bodies. In that case @{text "bn"} would

  1306   not respect alpha-equivalence. We can also see that

  1310   Say we have @{text "bn\<^isub>1, \<dots>, bn\<^isub>m"}, then we also define @{text "\<approx>bn\<^isub>1, \<dots>, \<approx>bn\<^isub>m"}.

  1318   Say we have binding functions @{text "bn\<^isub>1, \<dots>, bn\<^isub>m"}, then we also define @{text "\<approx>bn\<^isub>1, \<dots>, \<approx>bn\<^isub>m"}.

  1330   For what follows, let us assume 

  1338   For what follows, let us assume @{text C} is of type @{text ty}.  The task

  1331   @{text C} is of type @{text ty} and its arguments are given by @{text "C ty\<^isub>1 \<dots> ty\<^isub>n"}.

  1339   is to specify what the premises of these clauses are. Again for this we

  1332   The task is to specify what the premises of these clauses are. For this we

  1340   analyse the binding clauses and produce a corresponding premise.

  1333   consider the pairs \mbox{@{text "(x\<^isub>i, y\<^isub>i)"}}, but instead of considering them in turn, it will 

  1334   be easier to analyse these pairs according to  ``clusters'' of the binding clauses. 

  1335   Therefore we distinguish the following cases:

  1351   \begin{itemize}

  1356   \begin{equation}\label{alpha}

  1352   \item The @{text "(x\<^isub>i, y\<^isub>i)"} is a body of shallow binder with type @{text "ty"}. We assume the 

  1357   \mbox{%

  1353   \mbox{@{text "(u\<^isub>1, v\<^isub>1),\<dots>,(u\<^isub>m, v\<^isub>m)"}} are the corresponding binders. For the binding mode

  1358   \begin{tabular}{c@ {\hspace{2mm}}p{7cm}}

  1354   \isacommand{bind\_set} we generate the premise

  1359   \multicolumn{2}{@ {}l}{Empty binding clauses of the form 

  1355   \begin{center}

  1360   \isacommand{bind\_set}~@{term "{}"}~\isacommand{in}~@{text "x\<^isub>i"}:}\\ 

  1356    @{term "\<exists>p. (u\<^isub>1 \<union> \<xi> \<union> u\<^isub>m, x\<^isub>i) \<approx>gen alpha_ty fv_ty p (v\<^isub>1 \<union> \<xi> \<union> v\<^isub>m, y\<^isub>i)"}

  1361   $\bullet$ & @{text "x\<^isub>i \<approx>ty y\<^isub>i"} provided @{text "x\<^isub>i"} and @{text "y\<^isub>i"} 

  1357   \end{center}

  1362   are recursive arguments of @{text "C"}\\

  1358 

  1363   $\bullet$ & @{term "x\<^isub>i = y\<^isub>i"} provided @{text "x\<^isub>i"} and @{text "y\<^isub>i"} are 

  1359   For the binding mode \isacommand{bind}, we use $\approx_{\textit{list}}$, and for

  1364   non-recursive arguments\smallskip\\

  1360   binding mode \isacommand{bind\_res} we use $\approx_{\textit{res}}$ instead. 

  1365   \multicolumn{2}{@ {}l}{Shallow binders of the form 

  1361 

  1366   \isacommand{bind\_set}~@{text "x\<^isub>1\<dots>x\<^isub>n"}~\isacommand{in}~@{text "x'\<^isub>1\<dots>x'\<^isub>m"}:}\\ 

  1362   \item The @{text "(x\<^isub>i, y\<^isub>i)"} is a deep non-recursive binder with type @{text "ty"}

  1367   $\bullet$ & Assume the bodies @{text "x'\<^isub>1\<dots>x'\<^isub>m"} are of type @{text "ty\<^isub>1\<dots>ty\<^isub>m"},

  1363   and @{text bn} is corresponding the binding function. We assume 

  1368   @{text "R"} is @{text "\<approx>ty\<^isub>1 \<otimes> ... \<otimes> \<approx>ty\<^isub>m"} and @{text fv} is

  1364   @{text "(u\<^isub>1, v\<^isub>1),\<dots>,(u\<^isub>m, v\<^isub>m)"} are the corresponding bodies with types @{text "ty\<^isub>1,\<dots>, ty\<^isub>m"}. 

  1369   @{text "fv_ty\<^isub>1 \<oplus> ... \<oplus> fv_ty\<^isub>m"}, then

  1365   For the binding mode \isacommand{bind\_set} we generate two premises

  1370   \begin{center}

  1366   %

  1371   @{term "\<exists>p. (x\<^isub>1 \<union> \<xi> \<union> x\<^isub>n, (x'\<^isub>1,\<xi>,x'\<^isub>m)) \<approx>gen R fv p (y\<^isub>1 \<union> \<xi> \<union> y\<^isub>n, (y'\<^isub>1,\<xi>,y'\<^isub>m))"}

  1367   \begin{center}

  1372   \end{center}\\

  1368    @{text "x\<^isub>i \<approx>bn y\<^isub>i"}\hfill

  1373   \multicolumn{2}{@ {}l}{Deep binders of the form 

  1369    @{term "\<exists>p. (bn x\<^isub>i, (u\<^isub>1,\<xi>,u\<^isub>m)) \<approx>gen R fv p (bn y\<^isub>i, (v\<^isub>1,\<xi>,v\<^isub>m))"}

  1374   \isacommand{bind\_set}~@{text "bn x"}~\isacommand{in}~@{text "x'\<^isub>1\<dots>x'\<^isub>m"}:}\\ 

  1370   \end{center}

  1375   $\bullet$ & Assume the bodies @{text "x'\<^isub>1\<dots>x'\<^isub>m"} are of type @{text "ty\<^isub>1\<dots>ty\<^isub>m"},

  1371 

  1376   @{text "R"} is @{text "\<approx>ty\<^isub>1 \<otimes> ... \<otimes> \<approx>ty\<^isub>m"} and @{text fv} is

  1372   \noindent

  1377   @{text "fv_ty\<^isub>1 \<oplus> ... \<oplus> fv_ty\<^isub>m"}, then for recursive deep binders

  1373   where @{text R} is @{text "\<approx>ty\<^isub>1 \<otimes> ... \<otimes> \<approx>ty\<^isub>m"} and @{text fv} is

  1378   \begin{center}

  1374   @{text "fv_ty\<^isub>1 \<oplus> ... \<oplus> fv_ty\<^isub>m"}. Similarly for the other binding modes.

  1379   @{term "\<exists>p. (bn x, (x'\<^isub>1,\<xi>,x'\<^isub>m)) \<approx>gen R fv p (bn y, (y'\<^isub>1,\<xi>,y'\<^isub>m))"}

  1375 

  1380   \end{center}\\

  1376   \item The @{text "(x\<^isub>i, y\<^isub>i)"} is a deep recursive binders with type @{text "ty"}

  1381   $\bullet$ & for non-recursive binders we generate in addition @{text "x \<approx>bn y"}\\

  1377   and  @{text bn} is the corresponding binding function. We assume 

  1382   \end{tabular}}

  1378   @{text "(u\<^isub>1, v\<^isub>1),\<dots>,(u\<^isub>m, v\<^isub>m)"} are the corresponding bodies with types @{text "ty\<^isub>1,\<dots>, ty\<^isub>m"}. 

  1383   \end{equation}

  1379   For the binding mode \isacommand{bind\_set} we generate the premise

  1384 

  1380   %

  1385   \noindent

  1381   \begin{center}

  1386   Similarly for the other binding modes.

  1382   @{term "\<exists>p. (bn x\<^isub>i, (x\<^isub>i, u\<^isub>1,\<xi>,u\<^isub>m)) \<approx>gen R fv p (bn y\<^isub>i, (y\<^isub>i, v\<^isub>1,\<xi>,v\<^isub>m))"}

  1387   From this definition it is clear why we have to impose the restriction

  1383   \end{center}

  1388   of excluding overlapping deep binders, as these would need to be translated into separate

  1384 

  1385   \noindent

  1386   where @{text R} is @{text "\<approx>ty \<otimes> \<approx>ty\<^isub>1 \<otimes> ... \<otimes> \<approx>ty\<^isub>m"} and @{text fv} is

  1387   @{text "fv_ty \<oplus> fv_ty\<^isub>1 \<oplus> ... \<oplus> fv_ty\<^isub>m"}. Similarly for the other modes.

  1388   \end{itemize}

  1389 

  1390   \noindent

  1391   From this definition it is clear why we can only support one binding mode per binder

  1392   and body, as we cannot mix the relations $\approx_{\textit{set}}$, $\approx_{\textit{list}}$

  1393   and $\approx_{\textit{res}}$. It is also clear why we have to impose the restriction

  1394   of excluding overlapping binders, as these would need to be translated into separate