Re: [isabelle] locale default structure

Dear Peter,

I have some odd(?) behaviour when combining locales:

  locale test = complete_lattice L + complete_lattice FL

the default index for operators like \<squnion> is L, but the default structure for referencing a lemma is FL. i.e. the following proof will fail:

lemma (in test) "[|a:carrier L; b:carrier L; c:carrier L|] ==> (a\<squnion>b)\<squnion>c = a\<squnion>(b\<squnion>c)" by (simp only: join_assoc)

if I use the qualified name, L.join_assoc to reference the lemma, the proof works.

The structure default only applies to term syntax. Theorem names are managed through name spaces, and the later declaration wins. This is also the reason why the modified declaration

 locale test = struct L + complete_lattice FL + complete_lattice L

of you later e-mail "works", because the order of theorems is changed.

Dr. Clemens Ballarin
Institut fuer Informatik, TU Muenchen
Boltzmannstr. 3, 85748 Garching, Germany
Phone: +49-89-289-17326, Fax: +49-89-289-17307

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