[isabelle] Problems using subclasses



Dear all,

I stumbled upon the following problem: it seems, that it is not possible
to access generic lemmas with sort-constraints for proving a subclass
relation:

theory Test
imports Main
begin

consts P :: "'a => 'a => bool"
consts Q :: "'a => 'a => bool"
  
class A =
  fixes foo :: "'a => 'a"

class B = A +
  fixes bar :: "'a => 'a"
  assumes P: "P (x :: 'a) (foo x)"
begin
lemma PQ: "P (x :: 'a) y ==> Q x y" sorry
end

lemma Q: "Q (x :: 'a :: B) (foo x)"
  using P[of x] PQ by auto

class C = A +
  assumes QQ: "? y. Q (x :: 'a) y"

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 *)
  
  note P[of x] PQ[of x] 
  (* one can access lemmas from B like P and PQ which have been
     defined within the context *)

  show "? y. Q x y" using Q[of x] ..
  (* delivers "Type unification failed: Variable 'a::type not of sort B" *)
  (* but not lemmas like Q, which are defined outside the class via
     sort constraints *)
qed
end

 

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.

Best regards,
René

PS: I used Isabelle2013-1-RC3



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