Re: [isabelle] find_theorems and locales



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






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