Re: [isabelle] question on type classes and subclasses



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






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