[isabelle] Question about Contexts and Sorts



Hi,

Could someone who understands Isabelle's contexts, classes and sorts
better than I do perhaps enlighten me why the second proof in the
example theory below fails?  (I guess it fails because b_def is
expecting sort HOL.type, while the actual sort is {Scratch.B,Scratch.C}.
However, I don't quite understand the reason for this.  Is it a bug?  Is
there a workaround?)

Many thanks in advance!

Kind regards,
Tjark

========== 8< ==========

theory Scratch imports Main
begin

class A =
  fixes a :: 'a

class B = A
begin
  definition "b = a"
end

class C = A
begin
  definition "c = a"
end

lemma bc: "b = c" by (simp only: b_def c_def)

lemma (in B) "b = c" by (simp only: b_def c_def)
  -- {* fails because b_def is expecting sort HOL.type *}

end







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