1247   recursive call @{text "bn x\<^isub>i"}\\[1mm]

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

  1248   %

  1248   %

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

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

  1250   $\bullet$ & @{text "atom x\<^isub>i"} provided @{term "x\<^isub>i"} is an atom\\

  1313   @{text "(x\<^isub>1, y\<^isub>1) R\<^isub>1 \<otimes> R\<^isub>2 (x\<^isub>2, y\<^isub>2)"} & @{text "\<equiv>"} & @{text "x\<^isub>1 R\<^isub>1 y\<^isub>1 \<and> x\<^isub>2 R\<^isub>2 y\<^isub>2"}\\

  1314   @{text "(x\<^isub>1, y\<^isub>1) (R\<^isub>1 \<otimes> R\<^isub>2) (x\<^isub>2, y\<^isub>2)"} & @{text "\<equiv>"} & @{text "x\<^isub>1 R\<^isub>1 y\<^isub>1 \<and> x\<^isub>2 R\<^isub>2 y\<^isub>2"}\\

  1314   @{text "fv\<^isub>1 \<oplus> fv\<^isub>2 (x, y)"} & @{text "\<equiv>"} & @{text "fv\<^isub>1 x \<union> fv\<^isub>2 y"}\\

  1315   @{text "(fv\<^isub>1 \<oplus> fv\<^isub>2) (x, y)"} & @{text "\<equiv>"} & @{text "fv\<^isub>1 x \<union> fv\<^isub>2 y"}\\

  1315   \end{tabular}

  1316   \end{tabular}

  1316   \end{center}

  1317   \end{center}

  1317 

  1318 

  1318 

  1319 

  1319   The relations are inductively defined predicates, whose clauses have

  1320   The relations for alpha-equivalence are inductively defined predicates, whose clauses have

  1321   @{text C} is of type @{text ty} and its arguments are specified as @{text "C ty\<^isub>1 \<dots> ty\<^isub>n"}).

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

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

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

  1323   consider the pairs @{text "(x\<^isub>i, y\<^isub>i)"} which necesarily must have the same type, say

  1324   consider the pairs @{text "(x\<^isub>i, y\<^isub>i)"}. We will analyse these pairs according to 

  1324   @{text "ty\<^isub>i"}. For each of these pairs we calculate a premise as follows. 

  1325   ``clusters'' of the binding clauses. There are the following cases:

  1325 

  1326 *}

  1326   \begin{center}

  1327 (*<*)

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

  1328 consts alpha_ty ::'a

  1328   \multicolumn{2}{l}{@{text "x\<^isub>i"} is a binder:}\\

  1329 notation alpha_ty ("\<approx>ty")

  1329   $\bullet$ & none provided @{text "x\<^isub>i"} is a shallow binder\\

  1330 (*>*)

  1330   $\bullet$ & @{text "x\<^isub>i \<approx>bn y\<^isub>i"} provided @{text "x\<^isub>i"} is a deep 

  1331 text {*

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

  1332   \begin{itemize}

  1332   $\bullet$ & @{text "True"} provided @{text "x\<^isub>i"} is a deep 

  1333   \item The @{text "(x\<^isub>i, y\<^isub>i)"} are bodies of shallow binders with type @{text "ty"}. We assume the 

  1333      recursive binder\\

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

  1334   \end{tabular}

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

  1335   \end{center}

  1336   \begin{center}

  1336 

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

  1337   TODO BELOW

  1338   \end{center}

  1338 

  1339 

  1339   \begin{center}

  1340   Similarly for the other modes.

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

  1341 

  1341   \multicolumn{2}{l}{@{text "x\<^isub>i"} is a body where the binding clause has mode \isacommand{bind}:}\\

  1342   \item The @{text "(x\<^isub>i, y\<^isub>i)"} are deep non-recursive binders with type @{text "ty"}

  1342   $\bullet$ & @{text "\<exists>p. (bnds_x\<^isub>i, x\<^isub>i) \<approx>lst (\<approx>ty\<^isub>i) fv_ty\<^isub>i p (bnds_y\<^isub>i, y\<^isub>j)"} 

  1343   and with @{text bn} being the auxiliary binding function. We assume 

  1343      provided @{text "x\<^isub>i"} has only shallow binders; in this case @{text "bnds_x\<^isub>i"} is the

  1344   @{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"}. 

  1344      union of all these shallow binders (similarly for @{text "bnds_y\<^isub>i"}\\

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

  1345   $\bullet$ & @{text "\<exists>p. (bn_ty\<^isub>j x\<^isub>j, x\<^isub>i) \<approx>lst (\<approx>ty\<^isub>i) fv_ty\<^isub>i p (bn_ty y\<^isub>j, y\<^isub>i)"} 

  1346 

  1346      provided @{text "x\<^isub>i"} is a body with a deep non-recursive binder @{text x\<^isub>j}

  1347   \begin{center}

  1347      (similarly @{text "y\<^isub>j"} is the deep non-recursive binder for @{text "y\<^isub>i"})\\ 

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

  1348   $\bullet$ & @{text "\<exists>p (bn_ty\<^isub>i x\<^isub>i, (x\<^isub>j, x\<^isub>n)) \<approx>lst R fvs \<pi> (bn\<^isub>m y\<^isub>j, (y\<^isub>j, y\<^isub>n))"}

  1349    @{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))"}

  1349      provided @{text "x\<^isub>j"} is a deep recursive binder with the auxiliary binding

  1350   \end{center}

  1350      function @{text "bn\<^isub>m"} and permutation @{text "\<pi>"}, @{term "fvs"} is a compound

  1351 

  1351      free variable function returning the union of appropriate @{term "fv_ty\<^isub>x"} and

  1352   \noindent

  1352      @{term "R"} is the composition of equivalence relations @{text "\<approx>"} and @{text "\<approx>\<^isub>n"}\\

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

  1353   $\bullet$ & @{text "x\<^isub>j"} has a deep recursive binding\\

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

  1354   $\bullet$ & @{text "({x\<^isub>n}, x\<^isub>j) \<approx>gen R fv_ty \<pi> ({y\<^isub>n}, y\<^isub>j)"} provided @{text "x\<^isub>j"} has

  1355 

  1355      a shallow binder @{text "x\<^isub>n"} with permutation @{text "\<pi>"}, @{term "R"} is the

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

  1356      alpha-equivalence for @{term "x\<^isub>j"}

  1357   and with @{text bn} being the auxiliary binding function. We assume 

  1357      and @{term "fv_ty"} is the free-variable function for @{term "x\<^isub>j"}\\

  1358   @{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"}. 

  1358   $\bullet$ & @{text "(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"}

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

  1359      has a deep non-recursive binder @{text "bn\<^isub>m x\<^isub>n"} with permutation @{text "\<pi>"}, @{term "R"} is the

  1360 

  1360      alpha-equivalence for @{term "x\<^isub>j"}

  1361   \begin{center}

  1361      and @{term "fv_ty"} is the free-variable function for @{term "x\<^isub>j"}\\

  1362   @{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))"}

  1362   $\bullet$ & @{text "x\<^isub>j \<approx>\<^isub>j y\<^isub>j"} provided @{term "x\<^isub>j"} is one of the types being

  1363   \end{center}

  1363      defined\\

  1364 

  1364   $\bullet$ & @{text "x\<^isub>j = y\<^isub>j"} otherwise\\

  1365   \noindent

  1365   \end{tabular}

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

  1366   \end{center}

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

  1367 

  1368   \end{itemize}

  1368   , of a type @{text ty}, two instances

  1369 

  1369   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

  1370   \noindent

  1370   exist permutations @{text "\<pi>\<^isub>1 \<dots> \<pi>\<^isub>p"} (one for each bound argument) such that

  1371   The only cases that are not covered by these rules is if @{text "(x\<^isub>i, y\<^isub>i)"} is

  1371   the conjunction of equivalences defined below for each argument pair @{text "x\<^isub>j"}, @{text "y\<^isub>j"} holds.

  1372   neither a binder nor a body. Then we just generate @{text "x\<^isub>i \<approx>ty y\<^isub>i"}  provided

  1372   For an argument pair @{text "x\<^isub>j"}, @{text "y\<^isub>j"} this holds if:

  1373   the type of @{text "x\<^isub>i"} and @{text "y\<^isub>i"} is @{text ty} and the arguments are 

  1373 

  1374   recursive arguments of the term constructor. If they are non-recursive arguments

  1374   

  1375   then we generate @{text "x\<^isub>i = y\<^isub>i"}.

  1376 

  1377   TODO