[isabelle] Exhaustiveness of Pure.type



Hello!

I've recently noticed an unexpected thing about the quite common type proxy ‹Pure.type›. My understanding is that it's convenient to use for defining type-dependent polymorphic constants, including type class members with no normal parameters (say, some abstract number ascribed to a type such as its assumed physical size). The thing is, I can't find any exhaustiveness theorem related to the constant ‹Pure.type› and its type ‹'a itself› e.g. "x ≡ Pure.type" or "(x ≡ Pure.type ⟹ P) ⟹ P". Analogous lemma exists for the unit type in HOL and the type itself looks similar enough to Haskell's Proxy datatype with a single Proxy constructor (which should imply exhaustiveness as with other datatypes). The non-exhaustiveness of ‹'a itself› causes a problem when one accidentally defines some class axiom with an extra term variable ‹t :: 'a itself› in place of the ‹Pure.type› constant, sometimes the axiom then cannot be proved if the corresponding instance definition is specified using the ‹Pure.type› constant, since the definition in the goal can be neither unfolded nor refined using the exhaustiveness rewrite/elimination rule. Is this situation intentional due to some logical limitations I'm not aware of? Of course ‹Pure.type› is part of Pure and not even HOL, so it's not technically related to datatypes, but is such exhaustiveness axiom incompatible with something important?

Regards, Mikhail




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.