Re: [isabelle] lattices, typeclasses, notations?
However as a typeclass instantiation I get stuck:
First of all, you seem to be using the partial_order class from
HOL/Lattice session. There is nothing wrong with this, but note that
there is also a similar class "order" in HOL/Orderings.thy and "lattice"
in HOL/Lattices.thy. These are already part of the HOL image, and I
think they are better integrated in terms of reasoning infrastructure,
but I am not sure. These classes use the symbol \<le> rather than
\<sqsubseteq> and also include a strict variant.
definition "leq = policyOrder"
The first goal is
\<And>x. x \<sqsubseteq> x
So I try
fix x::policy show "x \<sqsubseteq> x"
Already this is not accepted. Perhaps there is an ambiguity between
the \<sqsubseteq> of policyOrder and the \<sqsubseteq> of the
partial_order class (in spite of the explicit annotation (x::policy").
So I try
fix x::policy show "leq x x" using policyOrderRfl .
Here the "show" is accepted, but the last step "." still fails.
What is my problem? Thanks for any info.
You are confusing the two constants, "leq" and "policyOrder". They are
defined to be equal, but the definition must be used explicitly. Since
you have ambiguous notation, \<sqsubseteq> refers to policyOrder, which
is why the first attempt fails. In the second attempt, your goal is OK,
but the proof is not, because policyOrderRfl uses a different constant.
You should unfold the definition (I think in this context it will be
called something like leq_policy_def) explicitly.
It may also be a good idea to get rid of the syntax for policyOrder. It
makes your grammar ambiguous (which produces tons of warnings), and once
you have the instance, you can use it anyway, since it is defined for
the type class.
Hope this helps,
This archive was generated by a fusion of
Pipermail (Mailman edition) and