*To*: Manuel Eberl <eberlm at in.tum.de>, <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] question on type classes and subclasses*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Mon, 6 Feb 2017 17:39:56 +0100*In-reply-to*: <ecb3b38d-d045-d4ec-9d26-8a804f3af4d7@in.tum.de>*References*: <o7a696$oe5$1@blaine.gmane.org> <ecb3b38d-d045-d4ec-9d26-8a804f3af4d7@in.tum.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.7.0

Dear Esseger and Manuel,

setup âSign.add_const_constraint (@{const_name "g"}, SOME @{typ "'a â 'a"})â setup âSign.add_const_constraint (@{const_name "f"}, SOME @{typ "'a â 'a"})â lemmas lemmaC' = lemmaC[internalize_sort "'a :: C", unoverload "g :: 'a â 'a", unoverload "f :: 'a â 'a"] lemma (in C) lemmaC'': "g x = x" by(rule lemmaC') unfold_locales All this is still very experimental, but it works if you absolutely need it. Best, Andreas On 06/02/17 17:05, Manuel Eberl wrote:

The problem is that lemmaC is /not/ proved in the class C; it is proved without any surrounding context, but with a sort constraint C on the type 'a. This is, unfortunately, something different insofar as you cannot use such facts from within the context of the class. It is therefore advisable to prove facts like this within the class context whenever possible, e.g.: 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, I am having trouble using lemmas that I have proved in C. The following stupid 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 qed The proof fails, complaining that lemmaC[of x] makes no sense as the type '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 on here, as to me HC and lemmaC are the same statement. In my real use case, I want to use serious lemmas that I have proved in C, should I use another syntax for this? Esseger

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

**Re: [isabelle] question on type classes and subclasses***From:*Manuel Eberl

- Previous by Date: Re: [isabelle] question on type classes and subclasses
- Next by Date: [isabelle] WiL 2017: Women in Logic Workshop Second Call for Papers (new dates)
- Previous by Thread: Re: [isabelle] question on type classes and subclasses
- Next by Thread: [isabelle] WiL 2017: Women in Logic Workshop Second Call for Papers (new dates)
- 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