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
"class.lattice (op \<ge>) (op >) sup inf"
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
definition "inf_dual x y = dual (sup (undual x) (undual y))"
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.
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.
>> definition "leq = policyOrder"
>> 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
> Hope this helps,
This archive was generated by a fusion of
Pipermail (Mailman edition) and