1542 consts alpha_ty ::'a |
1542 consts alpha_ty ::'a |
1543 consts alpha_trm ::'a |
1543 consts alpha_trm ::'a |
1544 consts fa_trm :: 'a |
1544 consts fa_trm :: 'a |
1545 consts alpha_trm2 ::'a |
1545 consts alpha_trm2 ::'a |
1546 consts fa_trm2 :: 'a |
1546 consts fa_trm2 :: 'a |
1547 (*consts ast :: 'a |
1547 consts ast :: 'a |
1548 consts ast' :: 'a*) |
1548 consts ast' :: 'a |
1549 (* |
|
1550 notation (latex output) |
1549 notation (latex output) |
1551 alpha_ty ("\<approx>ty") and |
1550 alpha_ty ("\<approx>ty") and |
1552 alpha_trm ("\<approx>\<^bsub>trm\<^esub>") and |
1551 alpha_trm ("\<approx>\<^bsub>trm\<^esub>") and |
1553 fa_trm ("fa\<^bsub>trm\<^esub>") and |
1552 fa_trm ("fa\<^bsub>trm\<^esub>") and |
1554 alpha_trm2 ("\<approx>\<^bsub>assn\<^esub>\<approx>\<^bsub>trm\<^esub>") and |
1553 alpha_trm2 ("'(\<approx>\<^bsub>assn\<^esub>, \<approx>\<^bsub>trm\<^esub>')") and |
1555 fa_trm2 ("fa\<^bsub>assn\<^esub>fa\<^bsub>trm\<^esub>") and |
1554 fa_trm2 ("'(fa\<^bsub>assn\<^esub>, fa\<^bsub>trm\<^esub>')") and |
1556 ast ("'(as, t')") and |
1555 ast ("'(as, t')") and |
1557 ast' ("'(as', t\<PRIME> ')") |
1556 ast' ("'(as', t\<PRIME> ')") |
1558 *) |
|
1559 (*>*) |
1557 (*>*) |
1560 text {* |
1558 text {* |
1561 Again lets take a look at a concrete example for these definitions. For \eqref{letrecs} |
1559 Again lets take a look at a concrete example for these definitions. For \eqref{letrecs} |
1562 we have three relations $\approx_{\textit{trm}}$, $\approx_{\textit{assn}}$ and |
1560 we have three relations $\approx_{\textit{trm}}$, $\approx_{\textit{assn}}$ and |
1563 $\approx_{\textit{bn}}$ with the following clauses: |
1561 $\approx_{\textit{bn}}$ with the following clauses: |
1564 |
1562 |
1565 \begin{center} |
1563 \begin{center} |
1566 \begin{tabular}{@ {}c @ {}} |
1564 \begin{tabular}{@ {}c @ {}} |
1567 % \infer{@{text "Let as t \<approx>\<^bsub>trm\<^esub> Let as' t'"}} |
1565 \infer{@{text "Let as t \<approx>\<^bsub>trm\<^esub> Let as' t'"}} |
1568 % {@{term "\<exists>p. (bn as, t) \<approx>lst alpha_trm fa_trm p (bn as', t')"} & @{text "as \<approx>\<^bsub>bn\<^esub> as'"}}\smallskip\\ |
1566 {@{term "\<exists>p. (bn as, t) \<approx>lst alpha_trm fa_trm p (bn as', t')"} & @{text "as \<approx>\<^bsub>bn\<^esub> as'"}}\smallskip\\ |
1569 % \infer{@{text "Let_rec as t \<approx>\<^bsub>trm\<^esub> Let_rec as' t'"}} |
1567 \infer{@{text "Let_rec as t \<approx>\<^bsub>trm\<^esub> Let_rec as' t'"}} |
1570 % {@{term "\<exists>p. (bn as, ast) \<approx>lst alpha_trm2 fa_trm2 p (bn as', ast')"}} |
1568 {@{term "\<exists>p. (bn as, ast) \<approx>lst alpha_trm2 fa_trm2 p (bn as', ast')"}} |
1571 \end{tabular} |
1569 \end{tabular} |
1572 \end{center} |
1570 \end{center} |
1573 |
1571 |
1574 \begin{center} |
1572 \begin{center} |
1575 \begin{tabular}{@ {}c @ {}} |
1573 \begin{tabular}{@ {}c @ {}} |