1457   Notice that until now we have not said anything about the support of the

  1457   Until now we have not said anything about the support of the

  1507 %%% Without defining permute_bn, we cannot even write the substitution

  1507   With the above equations we can substitute free variables for support in

  1508 %%% of bindings in term constructors...

  1508   the lifted free variable equations, which gives us the support equations

  1509 

  1509   for the term constructors. With this we can show that for each binding in

  1510 % With the above equations we can substitute free variables for support in

  1510   a constructors the bindings can be renamed. To rename a shallow binder

  1511 % the lifted free variable equations, which gives us the support equations

  1511   or a deep recursive binder a permutation is sufficient. This is not the

  1512 % for the term constructors. With this we can show that for each binding in

  1512   case for a deep non-recursive bindings. Take the term

  1513 % a constructors the bindings can be renamed.

  1513   @{text "Let (ACons x (Vr x) ANil) (Vr x)"}, representing the language construct

  1514   @{text "let x = x in x"}. To rename the binder the permutation cannot

  1515   be applied to the whole assignment since it would rename the free @{term "x"}

  1516   as well. To avoid this we introduce a new construction operation

  1517   that applies a permutation under a binding function.

  1518 

  1519   For each binding function @{text "bn\<^isub>j :: ty\<^isub>i \<Rightarrow> \<dots>"} we define a permutation operation

  1520   @{text "\<bullet>bn\<^isub>j\<^isub> :: perm \<Rightarrow> ty\<^isub>i \<Rightarrow> ty\<^isub>i"}. This operation permutes only the arguments

  1521   that are bound by the binding function while also descending in the recursive subcalls.

  1522   For each term constructor @{text "C x\<^isub>1 \<dots> x\<^isub>n"} the @{text "\<bullet>bn\<^isub>j"} operation applied

  1523   to a permutation @{text "\<pi>"} and to this constructor equals the constructor applied

  1524   to the values for each argument. Provided @{text "bn\<^isub>j (C x\<^isub>1 \<dots> x\<^isub>n) = rhs"}, the value

  1525   for an argument @{text "x\<^isub>j"} is:

  1526   \begin{center}

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

  1528   $\bullet$ & @{text "x\<^isub>i"} provided @{text "x\<^isub>i"} is not in @{text "rhs"}\\

  1529   $\bullet$ & @{text "\<pi> \<bullet> x\<^isub>i"} provided @{text "x\<^isub>i"} is in @{text "rhs"} without a binding function\\

  1530   $\bullet$ & @{text "\<pi> \<bullet>bn\<^isub>k x\<^isub>i"} provided @{text "bn\<^isub>k x\<^isub>i"} is @{text "rhs"}\\

  1531   \end{tabular}

  1532   \end{center}

  1533 

  1534   The definition of @{text "\<bullet>bn"} is respectful (simple induction) so we can lift it

  1535   and obtain @{text "\<bullet>bn\<^isup>\<alpha>"}. A property that shows that this defnition is correct is:

  1536 

  1537 %% We could get this from ExLet/perm_bn lemma.

  1538   \begin{lemma} For every bn function  @{text "bn\<^isup>\<alpha>\<^isub>i"},

  1539   \begin{center}

  1540   @{text "\<pi> \<bullet> bn\<^isup>\<alpha>\<^isub>i l = bn\<^isup>\<alpha>\<^isub>i(p \<bullet>bn\<^isup>\<alpha>\<^isub>i l)"}

  1541   \end{center}

  1542   \end{lemma}

  1543   \begin{proof} By induction on the lifted type it follows from the definitions of

  1544     permutations on the lifted type and the lifted defining eqautions of @{text "\<bullet>bn"}.

  1545   \end{proof}

  1546 

  1547