header {* \isaheader{Class Declarations and Programs} *}
theory Decl imports Type begin
type_synonym
fdecl = "vname × ty" -- "field declaration"
type_synonym
'm mdecl = "mname × ty list × ty × 'm" -- {* method = name, arg.\ types, return type, body *}
type_synonym
'm "class" = "cname × fdecl list × 'm mdecl list" -- "class = superclass, fields, methods"
type_synonym
'm cdecl = "cname × 'm class" -- "class declaration"
type_synonym
'm prog = "'m cdecl list" -- "program"
translations
(type) "fdecl" <= (type) "vname × ty"
(type) "'c mdecl" <= (type) "mname × ty list × ty × 'c"
(type) "'c class" <= (type) "cname × fdecl list × ('c mdecl) list"
(type) "'c cdecl" <= (type) "cname × ('c class)"
(type) "'c prog" <= (type) "('c cdecl) list"
definition "class" :: "'m prog => cname \<rightharpoonup> 'm class"
where
"class ≡ map_of"
definition is_class :: "'m prog => cname => bool"
where
"is_class P C ≡ class P C ≠ None"
lemma finite_is_class: "finite {C. is_class P C}"
apply (unfold is_class_def class_def)
apply (fold dom_def)
apply (rule finite_dom_map_of)
done
definition is_type :: "'m prog => ty => bool"
where
"is_type P T ≡
(case T of Void => True | Boolean => True | Integer => True | NT => True
| Class C => is_class P C)"
lemma is_type_simps [simp]:
"is_type P Void ∧ is_type P Boolean ∧ is_type P Integer ∧
is_type P NT ∧ is_type P (Class C) = is_class P C"
by(simp add:is_type_def)
abbreviation
"types P == Collect (is_type P)"
end