Max Nowak (May 29 2021 at 13:37): Max Nowak (May 29 2021 at 13:37):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?
Lukas Stevens (May 30 2021 at 19:42):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: Apr 20 2024 at 04:19 UTC