Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] locale default structure

Email Gateway (Aug 18 2022 at 09:30):

From: Peter Lammich <Views@gmx.de>
I have some odd(?) behaviour when combining locales:

Given:
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.

I think this behaviour is somewhat odd, because \<squnion> refers to \<squnion>\<^bsub>L\<^esub>, but join_assoc refers to FL.join_assoc.

(How) Can I change this behaviour and make both, the default index and the default scope of the lemmas refer to L ?

Thanks in advance for any help

--
Peter Lammich

--

Der GMX SmartSurfer hilft bis zu 70% Ihrer Onlinekosten zu sparen!
Ideal für Modem und ISDN: http://www.gmx.net/de/go/smartsurfer

Email Gateway (Aug 18 2022 at 09:30):

From: Peter Lammich <peter.lammich@uni-muenster.de>

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

Given:
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 now retired to the following locale, where both, the default indexing
of operators and the default qualifiyng of theorem names are L.
locale test = struct L + complete_lattice FL + complete_lattice L

although I have no idea, why this works.

-- Peter Lammich

Email Gateway (Aug 18 2022 at 09:30):

From: Clemens Ballarin <ballarin@in.tum.de>
Dear Peter,

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

Given:
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.

Clemens

Last updated: May 03 2024 at 12:27 UTC