Re: [isabelle] locale import
> locale poset = ord +
> fixes A :: "'a set"
> assumes lt_le_not_le: "[|x : A; y : A|] ==> x < y <-> x <= y & ~ (y <=
> and refl: "x : A ==> x <= x"
> and trans: "[|x : A; y : A; z : A; x <= y; y <= z|] ==> x <= z"
the issue is that the syntax <= < is not defined in the locale ord, but
in the type class ord. Hence <= < in your spec do not refer to 'a but
to a fresh 'b::ord.
A quick solution to your issue is to turn »locale« into »class«. If
this it not suitable for your modelling, I suggest to use syntactic
variants for <= <, e.g. bended ones. Replacing or overloading standard
syntax in HOL-Main is nothing I recommend.
Btw. did you have a look at HOL-Algebra? You will also find order
specifications there which look quite similar to yours.
This archive was generated by a fusion of
Pipermail (Mailman edition) and