*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] find_theorems and locales*From*: Johannes Hölzl <hoelzl at in.tum.de>*Date*: Thu, 25 Jun 2015 17:02:45 +0200*In-reply-to*: <558C1544.7000906@informatik.tu-muenchen.de>*Organization*: TU München*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> <8D86E6AF-FE1E-4191-B78C-E8CF9FB65821@cam.ac.uk> <558C1544.7000906@informatik.tu-muenchen.de>

Am Donnerstag, den 25.06.2015, 16:50 +0200 schrieb Florian Haftmann: > There is nothing wrong with type classes here: > > class involutory = > fixes f :: "'a â 'a" > assumes involutory: "f (f x) = x" > begin > > lemma involutory3: > "f (f (f x)) = f x" > by (fact involutory) > > end > > find_theorems "f" > > It seems to be a constraint issue: > > find_theorems "_ = norm (_ - _)" > ~> 'a::real_normed_vector is inferred > find_theorems "_ = norm ((_::'a::dist_norm) - _)" > ~> typing error > > Maybe some naughty tweaking of sort constraints or an unforseen > behaviour of coercions, but these are mere guesses. I do not understand > these parts of the type class hierarchy. Yes, in Real_Vector_Spaces are a couple of "add_const_constraint"s for dist, open, and norm. These give a nicer user experience when only working with the semantic typeclasses. Obviously, if one needs to instantiate syntactic typelcasses it is more complicated. - Johannes > Am 19.06.2015 um 17:22 schrieb Larry Paulson: > > 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 > >> > > > > >

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

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

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

- Previous by Date: Re: [isabelle] find_theorems and locales
- 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