43 Higher-Order Logic (HOL) is based on a small logic kernel, whose only |
43 Higher-Order Logic (HOL) is based on a small logic kernel, whose only |
44 mechanism for extension is the introduction of safe definitions and of |
44 mechanism for extension is the introduction of safe definitions and of |
45 non-empty types. Both extensions are often performed in quotient |
45 non-empty types. Both extensions are often performed in quotient |
46 constructions. To ease the work involved with such quotient constructions, we |
46 constructions. To ease the work involved with such quotient constructions, we |
47 re-implemented in Isabelle/HOL the quotient package by Homeier. In doing so we |
47 re-implemented in Isabelle/HOL the quotient package by Homeier. In doing so we |
48 extended his work in order to deal with compositions of quotients. We also |
48 extended his work in order to deal with compositions of quotients. Like his |
49 designed our quotient package so that every step in a quotient construction |
49 package, we designed our quotient package so that every step in a quotient construction |
50 can be performed separately and as a result we are able to specify completely |
50 can be performed separately and as a result we are able to specify completely |
51 the procedure of lifting theorems from the raw level to the quotient level. |
51 the procedure of lifting theorems from the raw level to the quotient level. |
52 The importance for programming language research is that many properties of |
52 The importance for programming language research is that many properties of |
53 programming language calculi are easier to verify over $\alpha$-equated, or |
53 programming language calculi are easier to verify over $\alpha$-equated, or |
54 $\alpha$-quotient, terms, than over raw terms. |
54 $\alpha$-quotient, terms, than over raw terms. |