Re: [isabelle] find_theorems and locales



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

Attachment: signature.asc
Description: OpenPGP digital signature



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