Re: [isabelle] locale import



On 11/30/2011 04:34 PM, Florian Haftmann wrote:
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.
I was not aware of HOL-Algebra. That looks great, thank you! Until now I did always skip (or simply not understand) parts of the documentation that mentioned (structure) and indices, but this looks really useful. Is there some paper/tutorial/documentation that describes structures for dummies? ;)

cheers

chris





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