src/HOL/MicroJava/J/Decl.thy

improved document (added headers etc)

(*  Title:      HOL/MicroJava/J/Decl.thy
    ID:         $Id$
    Author:     David von Oheimb
    Copyright   1997 Technische Universitaet Muenchen
*)

header "Class Declarations and whole Programs"

theory Decl = Type:

types	fdecl		(* field declaration, cf. 8.3 (, 9.3) *)
	= "vname \<times> ty"


types	sig		(* signature of a method, cf. 8.4.2 *)
	= "mname \<times> ty list"

	'c mdecl		(* method declaration in a class *)
	= "sig \<times> ty \<times> 'c"

types	'c class		(* class *)
	= "cname \<times> fdecl list \<times> 'c mdecl list"
	(* superclass, fields, methods*)

	'c cdecl		(* class declaration, cf. 8.1 *)
	= "cname \<times> 'c class"

consts

  Object  :: cname	(* name of root class *)
  ObjectC :: "'c cdecl"	(* decl of root class *)

defs 

 ObjectC_def: "ObjectC == (Object, (arbitrary, [], []))"


types 'c prog = "'c cdecl list"


translations
  "fdecl"   <= (type) "vname \<times> ty"
  "sig"     <= (type) "mname \<times> ty list"
  "mdecl c" <= (type) "sig \<times> ty \<times> c"
  "class c" <= (type) "cname \<times> fdecl list \<times> (c mdecl) list"
  "cdecl c" <= (type) "cname \<times> (c class)"
  "prog  c" <= (type) "(c cdecl) list"

constdefs

  class		:: "'c prog => (cname \<leadsto> 'c class)"
  "class        \<equiv> map_of"
  is_class	:: "'c prog => cname => bool"
 "is_class G C  \<equiv> class G C \<noteq> None"

lemma finite_is_class: "finite {C. is_class G C}"
apply (unfold is_class_def class_def)
apply (fold dom_def)
apply (rule finite_dom_map_of)
done

consts

  is_type	:: "'c prog => ty    => bool"

primrec
"is_type G (PrimT pt) = True"
"is_type G (RefT t) = (case t of NullT => True | ClassT C => is_class G C)"

end