equal
deleted
inserted
replaced
1110 |
1110 |
1111 |
1111 |
1112 The datatype definition can be obtained by stripping off the |
1112 The datatype definition can be obtained by stripping off the |
1113 binding clauses and the labels on the types. We also have to invent |
1113 binding clauses and the labels on the types. We also have to invent |
1114 new names for the types @{text "ty\<^sup>\<alpha>"} and term-constructors @{text "C\<^sup>\<alpha>"} |
1114 new names for the types @{text "ty\<^sup>\<alpha>"} and term-constructors @{text "C\<^sup>\<alpha>"} |
1115 given by user. In our implementation we just use the affix ``@{text "_raw"}''. |
1115 given by the user. In our implementation we just use the affix ``@{text "_raw"}''. |
1116 But for the purpose of this paper, we just use the superscript @{text "_\<^sup>\<alpha>"} to indicate |
1116 But for the purpose of this paper, we just use the superscript @{text "_\<^sup>\<alpha>"} to indicate |
1117 that a notion is defined over alpha-equivalence classes and leave it out |
1117 that a notion is defined over alpha-equivalence classes and leave it out |
1118 for the corresponding notion defined on the ``raw'' level. So for example |
1118 for the corresponding notion defined on the ``raw'' level. So for example |
1119 we have |
1119 we have |
1120 |
1120 |
1310 \end{equation} |
1310 \end{equation} |
1311 |
1311 |
1312 Next we define alpha-equivalence for the types @{text "ty\<^isub>1, \<dots>, ty\<^isub>n"}. We call them |
1312 Next we define alpha-equivalence for the types @{text "ty\<^isub>1, \<dots>, ty\<^isub>n"}. We call them |
1313 @{text "\<approx>ty\<^isub>1, \<dots>, \<approx>ty\<^isub>n"}. Like with the free-variable functions, |
1313 @{text "\<approx>ty\<^isub>1, \<dots>, \<approx>ty\<^isub>n"}. Like with the free-variable functions, |
1314 we also need to define auxiliary alpha-equivalence relations for the binding functions. |
1314 we also need to define auxiliary alpha-equivalence relations for the binding functions. |
1315 Say we have @{text "bn\<^isub>1, \<dots>, bn\<^isub>m"}, then we also define @{text "\<approx>bn\<^isub>1, \<dots>, \<approx>b\<^isub>m"}. |
1315 Say we have @{text "bn\<^isub>1, \<dots>, bn\<^isub>m"}, then we also define @{text "\<approx>bn\<^isub>1, \<dots>, \<approx>bn\<^isub>m"}. |
1316 To simplify our definitions we will use the following abbreviations for |
1316 To simplify our definitions we will use the following abbreviations for |
1317 relations and free-variable acting on products. |
1317 relations and free-variable acting on products. |
1318 % |
1318 % |
1319 \begin{center} |
1319 \begin{center} |
1320 \begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l} |
1320 \begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l} |
1331 @{text "C x\<^isub>1 \<dots> x\<^isub>n \<approx>ty C y\<^isub>1 \<dots> y\<^isub>n"} |
1331 @{text "C x\<^isub>1 \<dots> x\<^isub>n \<approx>ty C y\<^isub>1 \<dots> y\<^isub>n"} |
1332 \end{center} |
1332 \end{center} |
1333 |
1333 |
1334 \noindent |
1334 \noindent |
1335 For what follows, let us assume |
1335 For what follows, let us assume |
1336 @{text C} is of type @{text ty} and its arguments are given by @{text "C ty\<^isub>1 \<dots> ty\<^isub>n"}). |
1336 @{text C} is of type @{text ty} and its arguments are given by @{text "C ty\<^isub>1 \<dots> ty\<^isub>n"}. |
1337 The task now is to specify what the premises of these clauses are. For this we |
1337 The task now is to specify what the premises of these clauses are. For this we |
1338 consider the pairs \mbox{@{text "(x\<^isub>i, y\<^isub>i)"}}, but instead of considering them in turn, it will |
1338 consider the pairs \mbox{@{text "(x\<^isub>i, y\<^isub>i)"}}, but instead of considering them in turn, it will |
1339 be easier to analyse these pairs according to ``clusters'' of the binding clauses. |
1339 be easier to analyse these pairs according to ``clusters'' of the binding clauses. |
1340 Therefore we distinguish the following cases: |
1340 Therefore we distinguish the following cases: |
1341 *} |
1341 *} |
1682 |
1682 |
1683 |
1683 |
1684 \noindent In comparison, the cases for the same constructors in the derived strong |
1684 \noindent In comparison, the cases for the same constructors in the derived strong |
1685 induction principle are: |
1685 induction principle are: |
1686 |
1686 |
1687 %% TODO get rid of the ugly hspaces. |
|
1688 \begin{equation}\nonumber |
1687 \begin{equation}\nonumber |
1689 \infer |
1688 \infer |
1690 { |
1689 { |
1691 \begin{tabular}{cp{7cm}} |
1690 \begin{tabular}{cp{7cm}} |
1692 \textrm{The properties }@{text "P1, P2, \<dots>, P12"}\textrm{ hold for all }@{text "tkind, ckind, \<dots>"}\\ |
1691 \textrm{The properties }@{text "P1, P2, \<dots>, P12"}\textrm{ hold for all }@{text "tkind, ckind, \<dots>"}\\ |