Re: [isabelle] find_theorems and locales
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.
> 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
>> 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.
> PGP available:
This archive was generated by a fusion of
Pipermail (Mailman edition) and