Theory Decl

theory Decl
imports Term
(*  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"

  (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"

  Prog    :: prog       ‹program as a global value›
  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)