[isabelle] Subclasses with auxiliary defns



I am trying to use Isabelle's new "class" declaration form rather than the old "axclass" form. However, I'm having trouble admitting subclasses whose axioms contain auxiliary definitions. Below is an example theory. I'm using Isabelle developer snapshot Isabelle_29- Jan-2007.

Thanks,
-john

theory "C_byte_type"
imports Main
begin

datatype byte = Byte int

class C_type =
  fixes to_bytes   :: "'a \<Rightarrow> byte list"
  assumes C_type_size_uniform:
            "length (to_bytes (x::'a)) = length (to_bytes (y::'a))"

definition
  size_of :: "'a::C_type itself \<Rightarrow> nat" where
  "size_of (t::'a::C_type itself) = length (to_bytes (arbitrary::'a))"


text {* This class definition is accepted: *}

class C_byte_type = C_type +
assumes one_byte_long: "length (to_bytes (arbitrary::'a::C_type)) = 1"


text {* But the next class definition causes this error:

  *** exception THM raised: Type not of sort C_type
  *** At command "class".

*}
class C_byte_type2 = C_type +
  assumes one_byte_long: "size_of TYPE('a::C_type) = 1"

end





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