Re: [isabelle] lattices, typeclasses, notations?



Thanks Alex.  I'm using "order" in HOL/Orderings.thy and "lattice" in
HOL/Lattices.thy as Alex suggested.  My typeclass instantiation works.

Now I want to work with the dual of a given lattice.  In HOL/Lattices.thy I see

lemma dual_lattice:
  "class.lattice (op \<ge>) (op >) sup inf"
  by [...]

What does that mean?  How can I use this lemma?  Please point me to
examples;.  This lemma is not even used to prove lemma
dual_bounded_lattice in the same file.

Looking at the HOL/Lattice session I found the following kind of example

datatype 'a dual = dual 'a
primrec undual :: "'a dual \<Rightarrow> 'a" where
  undual_dual: "undual (dual x) = x"

instantiation dual:: (lattice) lattice
begin
definition "inf_dual x y = dual (sup (undual x) (undual y))"
[...]
instance
proof

Now I get 12 subgoals (which I can probably prove) but I haven't taken advantage
of lemma dual_lattice.

Please explain how this is intended to be done.

Thanks,
Randy
---
On Fri, May 27, 2011 at 4:54 PM, Alexander Krauss <krauss at in.tum.de> wrote:
> 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.