*To*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Subject*: Re: [isabelle] find_theorems and locales*From*: Larry Paulson <lp15 at cam.ac.uk>*Date*: Fri, 19 Jun 2015 16:22:53 +0100*Cc*: Bertram Felgenhauer <bertram.felgenhauer at googlemail.com>, cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <557DBB6B.6010800@informatik.tu-muenchen.de>*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> <557DBB6B.6010800@informatik.tu-muenchen.de>

I've stumbled across a related issue with find_theorems that certainly seems wrong. I was searching for the theorem Real_Vector_Spaces.dist_norm_class.dist_norm, which is introduced as a type class axiom here: class dist_norm = dist + norm + minus + assumes dist_norm: "dist x y = norm (x - y)" Calling find_theorems with suitable patterns, such as dist "norm (_-_)â does not return this theorem among the results, but clearly it should. Larry > On 14 Jun 2015, at 18:35, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de> wrote: > > 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 >

**Follow-Ups**:**Re: [isabelle] find_theorems and locales***From:*Florian Haftmann

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

**Re: [isabelle] find_theorems and locales***From:*Florian Haftmann

- Previous by Date: Re: [isabelle] Sledgehammer: Cannot connect to server.
- Next by Date: Re: [isabelle] Sledgehammer: Cannot connect to server.
- 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