[isabelle] using lattice properties.



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.