Let's say I have a property
definition prop :: "'a => bool" where "property a ≡ (∀A. ...)". Then I have a lemma (I hope I roughly minimized it right, my code is a bit convoluted):
lemma (in linorder) "prop x" proof (unfold my_property_def, intro allI) fix A :: "('a :: linorder) set" (* <-- problem here*) ...
Isabelle complains that "Sort constraint linorder inconsistent with default type for type variable 'a" at the
fix. I only need to prove the lemma for
'a which satisfy linorder, I do not care about other cases. The issue seems to be that the
shows statement is too general and/or
(in linorder) seems to somehow not apply to the implicit
'a in the shows statement? Can I make it explicit somehow?
I think in the context of linorder the type
'a isn't of sort
linorder (the typeclass
linorder does not exist in the context of
linorder, only outside of the context). You either have to state the lemma in the global context and annotate the sort
linorder or just drop the sort annotation. I could be wrong though.
Last updated: Dec 07 2023 at 20:16 UTC