# Theory Decl

```(*  Title:      HOL/MicroJava/J/Decl.thy

Author:     David von Oheimb
*)

section ‹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 ⇀ '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}"

(*<*)
proof -
have "{C. is_class P C} = dom (map_of P)"
by (simp add: is_class_def class_def dom_def)
thus ?thesis by (simp add: finite_dom_map_of)
qed
(*>*)

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"