Re: [isabelle] find_theorems and locales



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.

Cheers,
	Florian

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

-- 

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.