header "Types, class Declarations, and whole programs"
theory Decl imports Term begin
datatype ty
= NT --{* null type *}
| Class cname --{* class type *}
text{* Field declaration *}
type_synonym fdecl
= "fname × ty"
record methd
= par :: ty
res :: ty
lcl ::"(vname × ty) list"
bdy :: stmt
text{* Method declaration *}
type_synonym mdecl
= "mname × methd"
record "class"
= super :: cname
flds ::"fdecl list"
methods ::"mdecl list"
text{* Class declaration *}
type_synonym cdecl
= "cname × class"
type_synonym prog
= "cdecl list"
translations
(type) "fdecl" \<leftharpoondown> (type) "fname × ty"
(type) "mdecl" \<leftharpoondown> (type) "mname × ty × ty × stmt"
(type) "class" \<leftharpoondown> (type) "cname × fdecl list × mdecl list"
(type) "cdecl" \<leftharpoondown> (type) "cname × class"
(type) "prog " \<leftharpoondown> (type) "cdecl list"
axiomatization
Prog :: prog --{* program as a global value *}
and
Object :: cname --{* name of root class *}
definition "class" :: "cname \<rightharpoonup> class" where
"class ≡ map_of Prog"
definition is_class :: "cname => bool" where
"is_class C ≡ class C ≠ None"
lemma finite_is_class: "finite {C. is_class C}"
apply (unfold is_class_def class_def)
apply (fold dom_def)
apply (rule finite_dom_map_of)
done
end