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