[isabelle] locale import



Hi all,

I seem to be unable to extract the necessary information from the locale documentation. Could somebody explain what happens in the following declaration?

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"

My goal was to reuse the syntax of ord and define a locale capturing partially ordered sets. However, the above declaration gives me:

print_locale poset

locale elements:
  fixes less_eq :: "'a ⇒ 'a ⇒ bool"
    and less :: "'a ⇒ 'a ⇒ bool"
    and A :: "'b ⇒ bool"
  assumes "poset A"

And I doen't see why the carrier A does not have elements of the same type as less_eq and less? How could I achieve this effect?

cheers

chris






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