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

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

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

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

  1511 %%% of bindings in term constructors...

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

  1512 

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

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

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

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

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

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

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

  1516 % a constructors the bindings can be renamed.

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

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

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

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

  1520   that applies a permutation under a binding function.

  1521 

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

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

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

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

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

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

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

  1529   \begin{center}

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

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

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

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

  1534   \end{tabular}

  1535   \end{center}

  1536 

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

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

  1539 

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

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

  1542   \begin{center}

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

  1544   \end{center}

  1545   \end{lemma}

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

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

  1548   \end{proof}

  1549 

  1550