Re: [isabelle] question on type classes and subclasses



Dear Esseger and Manuel,

In real-world cases, proving theorems within the class context may be require more work than outside. For example, all theorems about the Isabelle constant mono live in the global context, because mono's type is too polymorphic (two type variables) for a class context. This means that you cannot use any theorem about mono in a subclass proof, even if the concrete instance just contains one type variable. :-(

Fortunately, Types_To_Sets from Isabelle2016-1 can help in such cases. Import "~~/src/HOL/Types_To_Sets/Types_To_Sets" and put the following lines outside of any context. Then, you get a version lemmaC'' in the class context.

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







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