Re: [isabelle] lattices, typeclasses, notations?



Hi Randy,

[...]
However as a typeclass instantiation I get stuck:

instantiation policy::partial_order

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.

begin
definition "leq = policyOrder"
instance
proof (intro_classes)

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,
Alex





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