Re: [isabelle] Fwd: Subclasses with auxiliary defns



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

>> 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
solution.

Florian
begin:vcard
fn:Florian Haftmann
n:Haftmann;Florian
org;quoted-printable;quoted-printable:Technische Universit=C3=A4t M=C3=BCnchen ;Institut f=C3=BCr Informatik, Lehrstuhl Software and Systems Engineering
adr;quoted-printable;quoted-printable:;;Boltzmannstra=C3=9Fe 3;M=C3=BCnchen;Bayern;85748;Deutschland
email;internet:florian.haftmann at informatik.tu-muenchen.de
title:M. Sc.
tel;work:(++49 89) 289 - 17300
note;quoted-printable:PGP available: =
	=0D=0A=
	http://www4.informatik.tu-muenchen.de/~haftmann/pgp/florian_haftmann_at_i=
	nformatik_tu_muenchen_de.pgp=0D=0A=
	
x-mozilla-html:FALSE
url:http://isabelle.in.tum.de/~haftmann
version:2.1
end:vcard

Attachment: signature.asc
Description: OpenPGP digital signature



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