Higher Order Quotients and their Implementation in Isabelle HOL

This paper describes the concept of higher order quotients and an implementation in Isabelle. Higher order quotients are a generalization of quotients. They use partial equivalence relations (PERs) instead of equivalence relations to group together di erent elements. This makes them applicable to arbitrary function spaces. Higher order quotients are conservatively implemented in the Isabelle logic HOL with a type constructor and a type class for PERs. Ordinary quotients are a special case of higher order quotients. An example shows how they can be used in Isabelle.

• Type: Conference
• Year: 1997
• Where: TPHOL
• Authors: Oscar Slotosch
• Keywords: Automated Reasoning, Equivalence Relations, Ordinary Quotients, Partial Equivalence Relations, TPHOL 1997