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.

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
> 





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