I want to use the locale "preorder" from HOL Main. First I try
to see the locale predicate for "preorder", as described in the
(*** Unknown fact "preorder_def" (line 3 of ...
What is my misunderstanding?
Next, I define a locale:
locale funny =
p1: preorder where
less_eq = p1le and less = p1lt
for p1le::"'a => 'a => bool"
and p1lt::"'a => 'a => bool"
fixes p2le:: "nat => 'a => 'a"
and p2lt:: "nat => 'a => 'a"
assumes p2leAx: "\forall n. preorder p2le p2lt"
Note the use of the (first class) locale predicate in assumption
p2leAx. My intension is that this locale has one carrier ('a), a
preorder on that carrier (p1) and a family of preorders indexed
by naturals (p2le), also on the same carrier. Since I don't know
how to include a family of locales in a locale definition, I use
the first class locale predicate. Is there a better way to
construct this structure?
When isabelle checks this locale "funny" it says:
### Additional type variable(s) in locale specification "funny": 'b
What does that mean? It seems to come from the use of
the "preorder" locale predicate in assumption "p2leAx", but I've
been explicit about the instantiation of "preorder"?
Finally, the context "preorder" contains some definitions and
lemmas outside the original locale definition of "preorder".
(E.g. in the context preorder I define the symmetric closure of
less_eq, and prove that is an equivalence.) Can I access those
definitions and lemmas for the preorder "p2le" in my example?
Thanks for any help,
This archive was generated by a fusion of
Pipermail (Mailman edition) and