Re: [isabelle] Problems using subclasses

Dear Andreas,

thanks for the clarifying answer and the link to the Isar-Ref manual.


Am 23.10.2013 um 16:27 schrieb Andreas Lochbihler <andreas.lochbihler at>:

> Hi René,
>> subclass (in B) C
>> proof
>>   fix x :: 'a
>>   have "bar x = bar x" by simp
>>   (* since the term "bar x" is accepted, definitely, x
>>      has sort B *)
> No, 'a has sort type, not B, as can be seen by showing the sorts with [[show_sorts]]. Inside a class context, occurrences of class parameters are mapped to the locally fixed class parameter whenever type inference says that this is possible.
>>   note P[of x] PQ[of x]
>>   (* one can access lemmas from B like P and PQ which have been
>>      defined within the context *)
> Fact names from class contexts are localised similarly. You can refer to the global version of these facts with Test.P and Test.PQ. Then, type unification will fail.
>> Is this is known limitation, or did I make some mistake?
>> In my concrete application, I would have liked to use
>> ex_le_of_nat in src/HOL/Archimedean_Field to prove a subclass
>> relation, but could not. Instead I currently use ex_le_of_int
>> and copied the proof for ex_le_of_nat to finish the subclass proof,
>> which works, but is a bit unsatisfactory.
> This is a known problem. And for this reason, as many theorems as possible should be proven inside the class context. However, many theories have yet not been "optimised" in this respect.
> Alternatively, you can do an instance declaration instead of a subclass declaration:
> instance B \<subseteq> C
> Then, the type variable 'a has sort B in the proof, and you can use all you need. The difference to subclass is that you do not get the sublocale declaration B < C, that subclass implicitly issues, i.e., inside the context of B, you cannot refer to theorems from C.
> Best,
> Andreas
> PS: All this is explained in the Isar-Ref manual, section 5.7.

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