*To*: Bertram Felgenhauer <bertram.felgenhauer at googlemail.com>*Subject*: Re: [isabelle] find_theorems and locales*From*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Date*: Sun, 14 Jun 2015 19:35:39 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <7E55C52F-00F6-495C-A391-8B262891251C@cam.ac.uk>*Organization*: TU Munich*References*: <20150611090559.GA5121@24f89f8c-e6a1-4e75-85ee-bb8a3743bb9f> <5579533C.6060304@in.tum.de> <20150612074008.GA11432@24f89f8c-e6a1-4e75-85ee-bb8a3743bb9f> <7E55C52F-00F6-495C-A391-8B262891251C@cam.ac.uk>*User-agent*: Mozilla/5.0 (X11; Linux i686; rv:31.0) Gecko/20100101 Thunderbird/31.7.0

Hi Bertram et al, > 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). first, some terminology to make issues more clear: * The facts (or, the locale predicate with corresponding facts) is not ÂhiddenÂ, otherwise it would not be accessible through the name space, which is not the case. * Instead, it is ÂconcealedÂ, which is no more than an internal flag which some parts of the system (including find_theorems and probabliby sledgehammer) are free to interpret in a certain fashion. For the case of find_theorems, it just skips these on search. Hence, the definition and rules for locale predicates *are* accessible, and this is used throughout the distribution for some low-level constructions. Their naming convention is firmly established since 2007 (?) and with some familiarity it should not be difficult to use them in advanced satisfiability proofs for locale expressions etc. pp. It is indeed arguable why locale predicates must be concealed et all, but I guess this has something to do with sledgehammer!? > 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. I tend to put it this way: Isabelle has a module system (locales) which is founded in its the logical calculus itself, hence you are free to intermix them in formally sound ways. But then you are loosing a certain discipline which normally is imposed by the way the module system is implemented, so you have to establish your own discipline in order not to screw up the practical (re)usability of the system. Cheers, Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

**Attachment:
signature.asc**

**Follow-Ups**:**Re: [isabelle] find_theorems and locales***From:*Jasmin Blanchette

**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

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

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

- Previous by Date: Re: [isabelle] Splicing runtime ML values into Isar
- Next by Date: Re: [isabelle] The type class for integer division
- 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