[isabelle] Exhaustiveness of Pure.type
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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and