1405 the type of @{text "x\<^isub>i"} and @{text "y\<^isub>i"} is @{text ty} and the arguments are |
1405 the type of @{text "x\<^isub>i"} and @{text "y\<^isub>i"} is @{text ty} and the arguments are |
1406 recursive arguments of the term-constructor. If they are non-recursive arguments, |
1406 recursive arguments of the term-constructor. If they are non-recursive arguments, |
1407 then we generate just @{text "x\<^isub>i = y\<^isub>i"}. |
1407 then we generate just @{text "x\<^isub>i = y\<^isub>i"}. |
1408 |
1408 |
1409 |
1409 |
1410 The definition of the alpha-equivalence relations @{text "\<approx>bn"} for binding functions |
1410 The definitions of the alpha-equivalence relations @{text "\<approx>bn"} for binding functions |
1411 are similar. We again have conclusions of the form \mbox{@{text "C x\<^isub>1 \<dots> x\<^isub>n \<approx>bn C y\<^isub>1 \<dots> y\<^isub>n"}}. We |
1411 are similar. We again have conclusions of the form \mbox{@{text "C x\<^isub>1 \<dots> x\<^isub>n \<approx>bn C y\<^isub>1 \<dots> y\<^isub>n"}} |
1412 need to generate premises for each pair @{text "(x\<^isub>i, y\<^isub>i)"} depending on whether @{text "x\<^isub>i"} |
1412 and need to generate appropriate premises. We generate first premises according to the first three |
1413 occurs in @{text "rhs"} of the clause @{text "bn (C x\<^isub>1 \<dots> x\<^isub>n) = rhs"}: |
1413 rules given above. Only the ``left-over'' pairs @{text "(x\<^isub>i, y\<^isub>i)"} need to be treated |
|
1414 differently. They depend on whether @{text "x\<^isub>i"} occurs in @{text "rhs"} of the |
|
1415 clause @{text "bn (C x\<^isub>1 \<dots> x\<^isub>n) = rhs"}: |
1414 |
1416 |
1415 \begin{center} |
1417 \begin{center} |
1416 \begin{tabular}{c@ {\hspace{2mm}}p{7cm}} |
1418 \begin{tabular}{c@ {\hspace{2mm}}p{7cm}} |
1417 $\bullet$ & @{text "x\<^isub>i \<approx>ty y\<^isub>i"} provided @{text "x\<^isub>i"} does not occur in @{text rhs} |
1419 $\bullet$ & @{text "x\<^isub>i \<approx>ty y\<^isub>i"} provided @{text "x\<^isub>i"} does not occur in @{text rhs} |
1418 and the type of @{text "x\<^isub>i"} is @{text "ty"}\\ |
1420 and the type of @{text "x\<^isub>i"} is @{text ty} and @{text "x\<^isub>i"} is a recursive argument |
|
1421 in the term-constructor\\ |
|
1422 $\bullet$ & @{text "x\<^isub>i = y\<^isub>i"} provided @{text "x\<^isub>i"} does not occur in @{text rhs} |
|
1423 and @{text "x\<^isub>i"} is not a recursive argument in the term-constructor\\ |
1419 $\bullet$ & @{text "x\<^isub>i \<approx>bn y\<^isub>i"} provided @{text "x\<^isub>i"} occurs in @{text rhs} |
1424 $\bullet$ & @{text "x\<^isub>i \<approx>bn y\<^isub>i"} provided @{text "x\<^isub>i"} occurs in @{text rhs} |
1420 with the recursive call @{text "bn x\<^isub>i"}\\ |
1425 with the recursive call @{text "bn x\<^isub>i"}\\ |
1421 $\bullet$ & none provided @{text "x\<^isub>i"} occurs in @{text rhs} but it is not |
1426 $\bullet$ & none provided @{text "x\<^isub>i"} occurs in @{text rhs} but it is not |
1422 in a recursive call involving a @{text "bn"} |
1427 in a recursive call involving a @{text "bn"} |
1423 \end{tabular} |
1428 \end{tabular} |
1424 \end{center} |
1429 \end{center} |
1425 |
1430 |
1426 Again lets take a look at an example for these definitions. For \eqref{letrecs} |
1431 Again lets take a look at an example for these definitions. For \eqref{letrecs} |
1427 we have three relations, namely $\approx_{\textit{trm}}$, $\approx_{\textit{assn}}$ and |
1432 we have three relations, namely $\approx_{\textit{trm}}$, $\approx_{\textit{assn}}$ and |
1428 $\approx_{\textit{bn}}$, with the clauses as follows: |
1433 $\approx_{\textit{bn}}$, with the clauses as follows: |
1429 |
1434 |
1430 \begin{center} |
1435 \begin{center} |
1431 \begin{tabular}{@ {}c @ {}} |
1436 \begin{tabular}{@ {}c @ {}} |