*To*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Subject*: Re: [isabelle] Problems using subclasses*From*: René Thiemann <rene.thiemann at uibk.ac.at>*Date*: Thu, 24 Oct 2013 14:32:17 +0200*Cc*: "isabelle-users at cl.cam.ac.uk Mailinglist" <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <5267DCDB.7020100@inf.ethz.ch>*References*: <C642ED9D-66A7-4A6D-9F27-36AA01FEAA0C@uibk.ac.at> <5267DCDB.7020100@inf.ethz.ch>

Dear Andreas, thanks for the clarifying answer and the link to the Isar-Ref manual. Best, René Am 23.10.2013 um 16:27 schrieb Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>: > 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. >

**References**:**[isabelle] Problems using subclasses***From:*René Thiemann

**Re: [isabelle] Problems using subclasses***From:*Andreas Lochbihler

- Previous by Date: [isabelle] Autocompletion in 2013-1
- Next by Date: Re: [isabelle] efficient code for ('a, 'b) map (as opposed to ('a, 'b) mapping
- Previous by Thread: Re: [isabelle] Problems using subclasses
- Next by Thread: [isabelle] Problem with Session-Creation
- Cl-isabelle-users October 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list