*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] find_theorems and locales*From*: Bertram Felgenhauer <bertram.felgenhauer at googlemail.com>*From*: Bertram Felgenhauer via Cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk>*Date*: Fri, 12 Jun 2015 09:40:08 +0200*In-reply-to*: <5579533C.6060304@in.tum.de>*References*: <20150611090559.GA5121@24f89f8c-e6a1-4e75-85ee-bb8a3743bb9f> <5579533C.6060304@in.tum.de>*Reply-to*: Bertram Felgenhauer <bertram.felgenhauer at googlemail.com>*User-agent*: Mutt/1.5.23 (2014-03-12)

Lars Noschinski wrote: > On 11.06.2015 11:05, Bertram Felgenhauer via Cl-isabelle-users wrote: > > Hi, > > > > find_theorems doesn't seem to find locale definitions. Is this behavior > > intentional? For example: > > > > locale xyzzy = assumes "Some () = None" > > The reasoning seems to be that the locale predicate (and hence its > definition) is more or less an implementation detail of locales, so you > shouldn't access it directly. The similarly, the lemmas establishing > locale relationships are hidden from the public view. This also effects > sledgehammer. That means that for now, I should use unfold_locales instead. I have two issues with the current situation, though neither one is very severe. First of all, this is not clear from the documentation: The loc_def name is mentioned in the (nonauthoritative, I guess) locales tutorial. The Isar reference manual says that locales are turned into predicate /definitions/ loc and loc_axioms (not mentioning that the latter is omitted for leaf locales like xyzzy above), and explicitly mentions loc.intro and loc_axioms.intro ... which find_theorems can't find either. Neither source says that these facts are hidden and only used internally. Secondly, I feel that there is a tangible advantage of making these facts available, which to my mind means that they should also be discoverable through find_theorems, though not necessarily by sledgehammer. (Can those two visibilities be separated in Isabelle?) One advantage is that it allows unfolding locale definitions selectively. But perhaps more importantly, by having the definitions as theorems, they become compatible with existing proof tactics (for example, I can add loc_def as a simp rule to auto; I cannot do that with unfold_locales). Cheers, Bertram

**Follow-Ups**:**Re: [isabelle] find_theorems and locales***From:*Larry Paulson

**References**:**[isabelle] find_theorems and locales***From:*Bertram Felgenhauer

**Re: [isabelle] find_theorems and locales***From:*Lars Noschinski

- Previous by Date: Re: [isabelle] find_theorems and locales
- Next by Date: Re: [isabelle] find_theorems and locales
- Previous by Thread: Re: [isabelle] find_theorems and locales
- Next by Thread: Re: [isabelle] find_theorems and locales
- Cl-isabelle-users June 2015 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