1465 section {* Establishing the Reasoning Infrastructure *} |
1465 section {* Establishing the Reasoning Infrastructure *} |
1466 |
1466 |
1467 text {* |
1467 text {* |
1468 Having made all crucial definitions for raw terms, we can start introducing |
1468 Having made all crucial definitions for raw terms, we can start introducing |
1469 the resoning infrastructure for the types the user specified. For this we first |
1469 the resoning infrastructure for the types the user specified. For this we first |
1470 have to show that the alpha-equivalence relation defined in the previous |
1470 have to show that the alpha-equivalence relations defined in the previous |
1471 sections are indeed equivalence relations. |
1471 section are indeed equivalence relations. |
1472 |
1472 |
1473 \begin{lemma} |
1473 \begin{lemma} |
1474 Given the raw types @{text "ty\<^isub>1, \<dots>, ty\<^isub>n"} and binding functions |
1474 Given the raw types @{text "ty\<^isub>1, \<dots>, ty\<^isub>n"} and binding functions |
1475 @{text "bn\<^isub>1, \<dots>, bn\<^isub>m"}, the relations @{text "\<approx>ty\<^isub>1, \<dots>, \<approx>ty\<^isub>n"} and |
1475 @{text "bn\<^isub>1, \<dots>, bn\<^isub>m"}, the relations @{text "\<approx>ty\<^isub>1, \<dots>, \<approx>ty\<^isub>n"} and |
1476 @{text "\<approx>bn\<^isub>1 \<dots> \<approx>bn\<^isub>m"} are equivalence relations and equivariant. |
1476 @{text "\<approx>bn\<^isub>1 \<dots> \<approx>bn\<^isub>m"} are equivalence relations and equivariant. |
1489 "ty"}$_{1..n}$. We also obtain definitions for the term-constructors @{text |
1489 "ty"}$_{1..n}$. We also obtain definitions for the term-constructors @{text |
1490 "C"}$^\alpha_{1..m}$ from the raw term-constructors @{text |
1490 "C"}$^\alpha_{1..m}$ from the raw term-constructors @{text |
1491 "C"}$_{1..m}$. Similarly for the free-variable functions @{text |
1491 "C"}$_{1..m}$. Similarly for the free-variable functions @{text |
1492 "fv_ty"}$^\alpha_{1..n}$ and the binding functions @{text |
1492 "fv_ty"}$^\alpha_{1..n}$ and the binding functions @{text |
1493 "bn"}$^\alpha_{1..k}$. However, these definitions are of not much use for the |
1493 "bn"}$^\alpha_{1..k}$. However, these definitions are of not much use for the |
1494 user, since the are formulated in terms of the isomorphism we obtained by |
1494 user, since the are formulated in terms of the isomorphisms we obtained by |
1495 creating a new type in Isabelle/HOL (remember the picture shown in the |
1495 creating new types in Isabelle/HOL (recall the picture shown in the |
1496 Introduction). |
1496 Introduction). |
1497 |
1497 |
1498 {\bf TODO below.} |
1498 The first usefull property about term-constructors @{text |
|
1499 "C"}$^\alpha_{1..m}$ is to know that they are distinct, that is |
|
1500 @{text "C"}$^\alpha_i$@{text "x\<^isub>1 \<dots> x\<^isub>n"} @{text "\<noteq>"} |
|
1501 @{text "C"}$^\alpha_j$@{text "y\<^isub>1 \<dots> y\<^isub>m"} holds for @{text "i \<noteq> j"}. |
1499 |
1502 |
1500 then define the quotient types @{text "ty\<^isub>1\<^isup>\<alpha> \<dots> ty\<^isub>n\<^isup>\<alpha>"}. To lift |
1503 then define the quotient types @{text "ty\<^isub>1\<^isup>\<alpha> \<dots> ty\<^isub>n\<^isup>\<alpha>"}. To lift |
1501 the raw definitions to the quotient type, we need to prove that they |
1504 the raw definitions to the quotient type, we need to prove that they |
1502 \emph{respect} the relation. We follow the definition of respectfullness given |
1505 \emph{respect} the relation. We follow the definition of respectfullness given |
1503 by Homeier~\cite{Homeier05}. The intuition behind a respectfullness condition |
1506 by Homeier~\cite{Homeier05}. The intuition behind a respectfullness condition |