Let's say I have a propertydefinition 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: Oct 13 2024 at 01:36 UTC