Email Gateway (Aug 18 2022 at 10:24): Email Gateway (Aug 18 2022 at 10:24):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
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
florian.haftmann.vcf
signature.asc
Email Gateway (Aug 18 2022 at 10:24):From: John Matthews <matthews@galois.com>
Hi Florian, thanks for putting this on your to-do list. I can work
around the issue for now.
Cheers,
-john
Email Gateway (Aug 18 2022 at 10:25):From: John Matthews <matthews@galois.com>
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
Last updated: May 03 2024 at 12:27 UTC