[isabelle] Problems using subclasses
I stumbled upon the following problem: it seems, that it is not possible
to access generic lemmas with sort-constraints for proving a subclass
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)"
lemma PQ: "P (x :: 'a) y ==> Q x y" sorry
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
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 *)
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.
PS: I used Isabelle2013-1-RC3
This archive was generated by a fusion of
Pipermail (Mailman edition) and