*To*: Eddy Westbrook <westbrook at kestrel.edu>*Subject*: Re: [isabelle] Changing axiom names in a locale*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Tue, 12 Aug 2014 07:24:46 +0200*Cc*: USR Isabelle Mailinglist <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <51542662-1B7B-4456-9162-9BFA3937CA91@kestrel.edu>*References*: <A0DE04C1-2CB5-416A-BDB5-F95B20CDFA78@kestrel.edu> <53E5DB67.10707@inf.ethz.ch> <51542662-1B7B-4456-9162-9BFA3937CA91@kestrel.edu>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.0

How about using abbreviations? locale l begin definition foo ... end locale l2 = l begin abbreviation bar where "bar == foo" end Best, Andreas On 11/08/14 20:52, Eddy Westbrook wrote:

Btw, is there a similar command for declaring alias names for definitions in the imported locale as well? Thanks, -Eddy On Aug 9, 2014, at 1:27 AM, Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch> wrote:Hi Eddy, AFAIK the names of the assumption only show up as theorem names that can be used in the locale. Therefore, instead of renaming the assumptions, you can declare alias names with lemmas. For example: locale monoid_times = monoid one times for one times begin lemmas left_one = left_zero lemmas right_one = right_zero end Unfortunately, there is no way to specify the names of type variables other than mentioning them in the type of one of the fixed parameters. Best, Andreas On 08/08/14 21:57, Eddy Westbrook wrote:Hi, I was wondering, is there any way to import a locale in a way that changes the names it uses for the axioms, without having to write the whole locale over again? As an example of what I mean, consider the following locale for monoids: locale monoid = fixes zero :: "'a" fixes plus :: "'a \<times> 'a => 'a" assumes left_zero: "plus (zero, x) = x" assumes right_zero: "plus (x, zero) = x" assumes plus_assoc: "plus (plus (x,y),z) = plus (x,plus (y,z))” Is there a way to change this to use the names “one”, “times”, “left_one”, “right_one”, and “times_assoc” without writing the whole locale over again? I was thinking something like the following, which already does what I want (if the last three lines are dropped) for changing “zero” to “one” and “plus” to “times”: locale monoid_times = monoid where zero = one and plus = times and left_zero = left_one and right_zero = right_one and plus_assoc = times_assoc for one times left_one right_one times_assoc I know that, in this particular case, what I wrote above is actually just as long as if I had re-defined monoid_times from scratch, but the context is that we often only want to change a few names, rather than all of them, so some sort of notation like this would be helpful. Similarly, is there a way to change the type variable used, e.g., from ‘a to in monoid to ‘b in monoid_times? I know that in this case I could annotate “one” with the type variable ‘b, but in general a locale might only have elements with more complex types involving ‘a, so it might be annoying to have to write out the whole type just to change one type variable. Thanks, -Eddy

**References**:**[isabelle] Changing axiom names in a locale***From:*Eddy Westbrook

**Re: [isabelle] Changing axiom names in a locale***From:*Andreas Lochbihler

**Re: [isabelle] Changing axiom names in a locale***From:*Eddy Westbrook

- Previous by Date: [isabelle] Simplifier divergence in Isabelle 2014 release candidates.
- Next by Date: Re: [isabelle] Simplifier divergence in Isabelle 2014 release candidates.
- Previous by Thread: Re: [isabelle] Changing axiom names in a locale
- Next by Thread: [isabelle] Discussing RC issues in separate threads
- Cl-isabelle-users August 2014 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