# [isabelle] using lattice properties.

*To*: isabelle-users <isabelle-users at cl.cam.ac.uk>
*Subject*: [isabelle] using lattice properties.
*From*: Viorel Preoteasa <viorel.preoteasa at abo.fi>
*Date*: Wed, 13 Apr 2011 12:29:11 +0300
*User-agent*: Mozilla/5.0 (Windows; U; Windows NT 5.1; en-US; rv:1.9.2.15) Gecko/20110303 Lightning/1.0b2 Thunderbird/3.1.9

Hello
I have the following lemma.
context some_algebra begin;
lemma lesseq_lesseq_r: "(a <= b) = lesseq_r a b";
proof -;
interpret A: semilattice_inf lesseq_r less_r inf_r;
by unfold_locales;
show "(a <= b) = lesseq_r a b";
apply (subst le_iff_inf);
apply (subst A.le_iff_inf);

`The context some_algebra implies a semilattice_inf structure for <=.
``Also step labeled by A
`proves that we have a semilattice_inf for lesseq_r.

`However the proof step apply (subst A.le_iff_inf) fails with Unknown
``fact "A.le_iff_inf".
`I would be grateful for any help.
Best regards,
Viorel

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