Re: [isabelle] locale import

Hi Christian,

> locale poset = ord +
>   fixes A :: "'a set"
>   assumes lt_le_not_le: "[|x : A; y : A|] ==> x < y <-> x <= y & ~ (y <=
> x)"
>     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.




PGP available:

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.