*To*: Peter Lammich <peter.lammich at uni-muenster.de>*Subject*: Re: [isabelle] Question about functions with equal names defined in different theories*From*: Andreas Lochbihler <andreas.lochbihler at kit.edu>*Date*: Wed, 22 Sep 2010 12:59:34 +0200*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <4C99CB28.8090100@uni-muenster.de>*References*: <4C99CB28.8090100@uni-muenster.de>*User-agent*: Thunderbird 2.0.0.17 (X11/20080925)

Hi Peter,

However, some theories based on A are now to be used a bigger context,where the details of A (including foldl, etc.) are no longer important.Nevertheless, the constants remain defined and overwrite the standardconstants from List.thy and Set.thy, which is embarrassing.

Alternatively, I thought of defining a locale: locale A_loc begin definition foldl, foldr, insert, ... end interpretation A: A_loc . And proving extensions to A inside the locale. The interpretation is required for code generation, as the code generator seems not to generate code for "A_loc.foldl", etc.

Am I on the right track? Is there a simpler solution?

theory Foo imports Plain begin definition foldl :: "nat" where "foldl = 0" end theory Bar imports Main Foo begin -- "foldl now refers to Foo.foldl" end theory Bar2 imports Foo Main begin -- "foldl now refers to List.foldl" end Another option is to abuse notation, which also allows to unhide the constant again: theory Foo imports Main begin definition foldl :: "nat" where "foldl = 0" notation List.foldl ("foldl") term "foldl" -- "List.foldl" no_notation List.fold ("foldl") term "foldl" -- "Foo.foldl" end Best, Andreas -- Karlsruher Institut für Technologie IPD Snelting Andreas Lochbihler wissenschaftlicher Mitarbeiter Adenauerring 20a, Gebäude 50.41, Raum 023 76131 Karlsruhe Telefon: +49 721 608-8352 Fax: +49 721 608-8457 E-Mail: andreas.lochbihler at kit.edu http://pp.info.uni-karlsruhe.de

**Follow-Ups**:

**References**:

- Previous by Date: [isabelle] Question about functions with equal names defined in different theories
- Next by Date: Re: [isabelle] Question about functions with equal names defined in different theories
- Previous by Thread: [isabelle] Question about functions with equal names defined in different theories
- Next by Thread: Re: [isabelle] Question about functions with equal names defined in different theories
- Cl-isabelle-users September 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list