*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] question on type classes and subclasses*From*: Manuel Eberl <eberlm at in.tum.de>*Date*: Mon, 6 Feb 2017 17:05:16 +0100*In-reply-to*: <o7a696$oe5$1@blaine.gmane.org>*References*: <o7a696$oe5$1@blaine.gmane.org>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.6.0

class C = A + assumes HC: "g x = x" begin lemma lemmaC: "g x = x" â end or context C begin lemma lemmaC: "g x = x" â end or lemma (in C) lemmaC: "g x = x" â Cheers, Manuel On 2017-02-06 16:55, Esseger wrote:

Dear all,When trying to prove that a class C is a subclass of a class B, say, Iam having trouble using lemmas that I have proved in C. The followingstupid example illustrates it well:class A = fixes f g::"'a â 'a" assumes HA: "f x = g x" class B = A + assumes HB: "f x = x" class C = A + assumes HC: "g x = x" lemma lemmaC: "g x = (x::'a::C)" using HC by auto subclass (in C) B proof (*fix x::'a show "f x = x" using HA[of x] HC[of x] by auto*) fix x::'a show "f x = x" using HA[of x] lemmaC[of x] by auto qedThe proof fails, complaining that lemmaC[of x] makes no sense as thetype 'a of x is not of class C (while it is...). On the other hand,the commented line succeeds. I do not understand what is going onhere, as to me HC and lemmaC are the same statement.In my real use case, I want to use serious lemmas that I have provedin C, should I use another syntax for this?Esseger

**Follow-Ups**:**Re: [isabelle] question on type classes and subclasses***From:*Andreas Lochbihler

**References**:**[isabelle] question on type classes and subclasses***From:*Esseger

- Previous by Date: [isabelle] question on type classes and subclasses
- Next by Date: Re: [isabelle] question on type classes and subclasses
- Previous by Thread: [isabelle] question on type classes and subclasses
- Next by Thread: Re: [isabelle] question on type classes and subclasses
- Cl-isabelle-users February 2017 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