Re: [isabelle] Fwd: Subclasses with auxiliary defns

Hi Florian, thanks for putting this on your to-do list. I can work around the issue for now.


On Apr 12, 2007, at 12:43 AM, Florian Haftmann wrote:

Dear John,

the problem is simply that our class concept currently does not
implement a proper concept for derived definitions relative to classes;
so the definition

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

does introduce a theory-level constant size_of with class constraint
C_type, such that

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

fails since inside the locale C_byte and its children 'a always has sort
type, not C_type.

Currently, we cannot even provide a workaround for this, though derived
definitions will be our next step in implementing the class package.

Note that the current implementation allows "class"es to inherit from
"axclass"es, which might provide a (though unsatisfactory) temporary


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