equal
deleted
inserted
replaced
1558 |
1558 |
1559 \noindent |
1559 \noindent |
1560 In this binding clause no atom is bound and we only have to `alpha-relate' |
1560 In this binding clause no atom is bound and we only have to `alpha-relate' |
1561 the bodies. For this we build first the tuples @{text "D \<equiv> (d\<^isub>1,\<dots>, |
1561 the bodies. For this we build first the tuples @{text "D \<equiv> (d\<^isub>1,\<dots>, |
1562 d\<^isub>q)"} and @{text "D' \<equiv> (d\<PRIME>\<^isub>1,\<dots>, d\<PRIME>\<^isub>q)"} |
1562 d\<^isub>q)"} and @{text "D' \<equiv> (d\<PRIME>\<^isub>1,\<dots>, d\<PRIME>\<^isub>q)"} |
1563 whereby the labels @{text "d"}$_{1..q}$ refer to the arguments @{text |
1563 whereby the labels @{text "d"}$_{1..q}$ refer to some of the arguments @{text |
1564 "z"}$_{1..n}$ and respectively @{text "d\<PRIME>"}$_{1..q}$ to @{text |
1564 "z"}$_{1..n}$ and respectively @{text "d\<PRIME>"}$_{1..q}$ to some of @{text |
1565 "z\<PRIME>"}$_{1..n}$ of the term-constructor. In order to relate two such |
1565 "z\<PRIME>"}$_{1..n}$ of the term-constructor. In order to relate two such |
1566 tuples we define the compound alpha-equivalence relation @{text "R"} as |
1566 tuples we define the compound alpha-equivalence relation @{text "R"} as |
1567 follows |
1567 follows |
1568 |
1568 |
1569 \begin{equation}\label{rempty} |
1569 \begin{equation}\label{rempty} |
1571 \end{equation}\smallskip |
1571 \end{equation}\smallskip |
1572 |
1572 |
1573 \noindent |
1573 \noindent |
1574 with @{text "R\<^isub>i"} being @{text "\<approx>ty\<^isub>i"} if the corresponding |
1574 with @{text "R\<^isub>i"} being @{text "\<approx>ty\<^isub>i"} if the corresponding |
1575 labels @{text "d\<^isub>i"} and @{text "d\<PRIME>\<^isub>i"} refer to a |
1575 labels @{text "d\<^isub>i"} and @{text "d\<PRIME>\<^isub>i"} refer to a |
1576 recursive argument of @{text C} with type @{text "ty\<^isub>i"}; otherwise |
1576 recursive argument of @{text C} and have type @{text "ty\<^isub>i"}; otherwise |
1577 we take @{text "R\<^isub>i"} to be the equality @{text "="}. Again the |
1577 we take @{text "R\<^isub>i"} to be the equality @{text "="}. Again the |
1578 latter is because @{text "ty\<^isub>i"} is not part of the specified types |
1578 latter is because @{text "ty\<^isub>i"} is not part of the specified types |
1579 and alpha-equivalence of any previously defined type is supposed to coincide |
1579 and alpha-equivalence of any previously defined type is supposed to coincide |
1580 with equality. This lets us now define the premise for an empty binding |
1580 with equality. This lets us now define the premise for an empty binding |
1581 clause succinctly as @{text "prems(bc\<^isub>i) \<equiv> D R D'"}, which can be |
1581 clause succinctly as @{text "prems(bc\<^isub>i) \<equiv> D R D'"}, which can be |