[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:18.104.22.168) Gecko/20110303 Lightning/1.0b2 Thunderbird/3.1.9
I have the following lemma.
context some_algebra begin;
lemma lesseq_lesseq_r: "(a <= b) = lesseq_r a b";
interpret A: semilattice_inf lesseq_r less_r inf_r;
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
I would be grateful for any help.
This archive was generated by a fusion of
Pipermail (Mailman edition) and