(*  Title:      HOL/NanoJava/Decl.thy
    Author:     David von Oheimb
    Copyright   2001 Technische Universitaet Muenchen
*)

section "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" ↽ (type) "fname × ty"
  (type) "mdecl" ↽ (type) "mname × ty × ty × stmt"
  (type) "class" ↽ (type) "cname × fdecl list × mdecl list"
  (type) "cdecl" ↽ (type) "cname × class"
  (type) "prog " ↽ (type) "cdecl list"

axiomatization
  Prog    :: prog       ― ‹program as a global value›
and
  Object  :: cname      ― ‹name of root class›


definition "class" :: "cname ⇀ 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