Re: [isabelle] find_theorems and locales



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




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.