header {* \isaheader{Class Declarations and Programs} *}
theory Decl imports Type begin
types
fdecl = "vname × ty" -- "field declaration"
'm mdecl = "mname × ty list × ty × 'm" -- "method = name, arg. types, return type, body"
'm "class" = "cname × fdecl list × 'm mdecl list" -- "class = superclass, fields, methods"
'm cdecl = "cname × 'm class" -- "class declaration"
'm prog = "'m cdecl list" -- "program"
translations
"fdecl" <= (type) "String.literal × ty"
"mdecl c" <= (type) "String.literal × ty list × ty × c"
"class c" <= (type) "String.literal × fdecl list × (c mdecl) list"
"cdecl c" <= (type) "String.literal × (c class)"
"prog c" <= (type) "(c cdecl) list"
constdefs
"class" :: "'m prog => cname \<rightharpoonup> 'm class"
"class ≡ map_of"
is_class :: "'m prog => cname => bool"
"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
consts
is_type :: "'m prog => ty => bool"
primrec
is_type_void: "is_type P Void = True"
is_type_bool: "is_type P Boolean = True"
is_type_int: "is_type P Integer = True"
is_type_nt: "is_type P NT = True"
is_type_class: "is_type P (Class C) = is_class P C"
is_type_array: "is_type P (A⌊⌉) = is_type P A"
lemma NT_Array_is_type: "is_NT_Array A ==> is_type P A"
by(induct A, auto)
end