1094   The datatype definition can be obtained by just stripping off the 

  1094   The datatype definition can be obtained by stripping off the 

  1098   For the purpose of the paper we just use superscripts to indicate a

  1098   For the purpose of the paper we just use the superscript @{text "_\<^sup>\<alpha>"} to indicate 

  1099   notion defined over alpha-equivalence classes and leave out the superscript

  1099   that a notion is defined over alpha-equivalence classes and leave it out 

  1100   for the corresponding notion on the ``raw'' level. So for example we have

  1100   for the corresponding notion defined on the ``raw'' level. So for example 

  1101 

  1101   we have

  1102   

  1109   position (see \cite{Berghofer99} for an indepth explanation of the datatype package

  1111   position (see \cite{Berghofer99} for an indepth description of the datatype package

  1111   functions by primitive recursion over the raw datatypes. We can also

  1113   functions, called @{term "bn_ty"}, by primitive recursion over the corresponding 

  1112   easily define a permutation operation by primitive recursion so that for each

  1114   raw datatype @{text ty}. We can also easily define permutation operations by 

  1113   term constructor @{text "C ty\<^isub>1 \<dots> ty\<^isub>n"} we have that

  1115   primitive recursion so that for each term constructor @{text "C ty\<^isub>1 \<dots> ty\<^isub>n"} 

  1114 

  1116   we have that

  1115   \begin{center}

  1117 

  1116   @{text "p \<bullet> (C x\<^isub>1 \<dots> x\<^isub>n) \<equiv> C (p \<bullet> x\<^isub>1) \<dots> (p \<bullet> x\<^isub>n)"}

  1118   \begin{center}

  1119   @{text "p \<bullet> (C x\<^isub>1 \<dots> x\<^isub>n) = C (p \<bullet> x\<^isub>1) \<dots> (p \<bullet> x\<^isub>n)"}

  1134   We define them together with the auxiliary free variable functions for

  1137   We define them together with auxiliary free variable functions for

  1135   binding functions. Given binding functions for raw types

  1138   the binding functions. Given binding functions 

  1137 

  1140   %

  1138   \begin{center}

  1141   \begin{center}

  1139   @{text "fv_bn_ty\<^isub>1 :: ty\<^isub>1 \<Rightarrow> atom set \<dots> fv_bn_ty\<^isub>m :: ty\<^isub>m \<Rightarrow> atom set"}

  1142   @{text "fv_bn_ty\<^isub>1 :: ty\<^isub>1 \<Rightarrow> atom set  \<dots>  fv_bn_ty\<^isub>m :: ty\<^isub>m \<Rightarrow> atom set"}

  1140   \end{center}

  1143   \end{center}

  1141 

  1144 

  1142   \noindent

  1145   \noindent

  1143   The basic idea behind these free-variable functions is to collect all atoms

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

  1144   that are not bound in a term constructor, but because of the rather

  1147   bound. While the idea behind these free variable functions is just to

  1145   complicated binding mechanisms the details are somewhat involved. 

  1148   collect all atoms that are not bound, because of the rather complicated

  1149   binding mechanisms their definitions are somewhat involved.

  1148   @{text "ty\<^isub>1 \<dots> ty\<^isub>n"} and some binding clauses, the function

  1152   \mbox{@{text "ty\<^isub>1 \<dots> ty\<^isub>n"}} and given some binding clauses associated with 

  1153   this constructor, the function

  1150   defined below for each argument. From the binding clause of this term

  1155   calculated below for each argument. 

  1151   constructor, we can determine whether the argument is a shallow or deep

  1156 

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

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

  1153   non-recursive binder. In case the argument, say @{text "x\<^isub>i"} with

  1160   non-recursive binder. 

  1154   type @{text "ty\<^isub>i"}, is a binder, the value is:

  1161 

  1155 

  1162   \begin{center}

  1156   \begin{center}

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

  1157   \begin{tabular}{cp{7cm}}

  1167   In case the argument @{text "x\<^isub>i"} is not a binder, it might be a body of

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

  1168   one or more abstractions. Let @{text "bnds"} be the set of bound atoms calculated

  1174   free variables; in the second clause, we have to look up all

  1169   as follows: If @{text "x\<^isub>i"} is not a body of an abstraction @{term "{}"}.

  1175   the free variables that are left unbound by the binding function @{text "bn_ty\<^isub>i"}---this

  1170   Otherwise there are two cases: either the

  1176   is done with function @{text "fv_bn_ty\<^isub>i"}; in the third clause, since the 

  1171   corresponding binders are all shallow or there is a single deep binder.

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

  1172   In the former case we build the union of all shallow binders; in the

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

  1173   later case we just take the set of atoms specified binding

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

  1174   function returns. With @{text "bnds"} computed as above the value of

  1180 

  1175   for @{text "x\<^isub>i"} is given by:

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

  1176 

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

  1177   \begin{center}

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

  1178   \begin{tabular}{cp{7cm}}

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

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

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

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

  1188 

  1189   \begin{center}

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

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

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

  1183      we are defining with the free variable function @{text "fv_ty\<^isub>i"}\\

  1195      corresponding to the types specified by the user\\

  1191   Next, for each binding function @{text "bn_ty"} we define a

  1203   Like the function @{text atom}, @{text "atoms"} coerces a set of atoms to the generic atom type.

  1192   free variable function @{text "fv_bn_ty"}. The basic idea behind this

  1204   It is defined as @{text "atom as \<equiv> {atom a | a \<in> as}"}.

  1193   function is to compute all the free atoms that are not bound by the binding

  1205 

  1194   function. So given that @{text "bn"} is a binding function for type

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

  1195   @{text "ty\<^isub>i"} it will be the same as @{text "fv_ty\<^isub>i"} with the

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

  1196   omission of the arguments present in @{text "bn"}.

  1208   as above, except that we do not subtract the set @{text bnds}.

  1197 

  1209   

  1198   For a binding function clause @{text "bn (C x\<^isub>1 \<dots> x\<^isub>n) = rhs"},

  1210   Next, we need to define a free variable function @{text "fv_bn_ty\<^isub>i"} for 

  1199   we define @{text "fv_bn"} to be the union of the values calculated

  1211   each binding function @{text "bn_ty\<^isub>i"}. The idea behind this

  1200   for @{text "x\<^isub>j"} as follows:

  1212   function is to compute the set of free atoms that are not bound by 

  1201 

  1213   the binding function. Because of the restrictions we imposed on the 

  1202   \begin{center}

  1214   form of binding functions, this can be done automatically by recursively 

  1203   \begin{tabular}{cp{7cm}}

  1215   building up the the set of free variables from the arguments that are 

  1204   $\bullet$ & @{term "{}"} provided @{term "x\<^isub>j"} occurs in @{text "rhs"} and is an atom,

  1216   not bound. Let us assume one clause of the binding function is 

  1217   @{text "bn_ty\<^isub>i (C x\<^isub>1 \<dots> x\<^isub>n) = rhs"}, then @{text "fv_bn_ty\<^isub>i"} is the 

  1218   union of the values calculated for @{text "x\<^isub>j"} of type @{text "ty\<^isub>j"}

  1219   as follows:

  1220 

  1221   \begin{center}

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

  1223   \multicolumn{2}{l}{@{text "x\<^isub>j"} occurs in @{text "rhs"}:}\\ 

  1224   $\bullet$ & @{term "{}"} provided @{term "x\<^isub>j"} is an atom,

  1206   $\bullet$ & @{text "fv_bn\<^isub>m x\<^isub>j"} provided @{term "x\<^isub>j"} occurs in @{text "rhs"} 

  1226   $\bullet$ & @{text "fv_bn_ty\<^isub>j x\<^isub>j"} in case @{text "rhs"} contains the 

  1207     with the recursive call @{text "bn\<^isub>m x\<^isub>j"}\\

  1227   recursive call @{text "bn_ty\<^isub>j x\<^isub>j"}\\[1mm]

  1208   $\bullet$ & @{text "atoms x\<^isub>j"} provided @{term "x\<^isub>j"} is a set of atoms not in @{text "rhs"}\\

  1228   %

  1209   $\bullet$ & @{term "atoml x\<^isub>j"} provided @{term "x\<^isub>j"} is a list of atoms not in @{text "rhs"}\\

  1229   \multicolumn{2}{l}{@{text "x\<^isub>j"} does not occur in @{text "rhs"}:}\\ 

  1210   $\bullet$ & @{text "fv_ty\<^isub>i x\<^isub>j"} provided @{term "x\<^isub>j"} is not in @{text "rhs"} and is 

  1230   $\bullet$ & @{text "atoms x\<^isub>j"} provided @{term "x\<^isub>j"} is a set of atoms\\

  1211      one of the datatypes

  1231   $\bullet$ & @{term "atoms (set x\<^isub>j)"} provided @{term "x\<^isub>j"} is a list of atoms\\

  1212      we are defining, with the free variable function @{text "fv_ty\<^isub>m"}\\

  1232   $\bullet$ & @{text "fv_ty\<^isub>j x\<^isub>j"} provided @{term "ty\<^isub>j"} is one of the raw

  1233      types corresponding to the types specified by the user\\