Theory Decl

(*  Title:      HOL/MicroJava/J/Decl.thy
    ID:         $Id: Decl.html 1910 2004-05-19 04:46:04Z kleing $
    Author:     David von Oheimb
    Copyright   1999 Technische Universitaet Muenchen
*)

header {* \isaheader{Class Declarations and Programs} *}

theory Decl = Type:

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) "vname × ty"
  "mdecl c" <= (type) "mname × ty list × ty × c"
  "class c" <= (type) "cname × fdecl list × (c mdecl) list"
  "cdecl c" <= (type) "cname × (c class)"
  "prog  c" <= (type) "(c cdecl) list"
(*>*)

constdefs
  class :: "'m prog => cname => '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
(*>*)

constdefs
  is_type :: "'m prog => ty => bool"
  "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"
(*<*)by(simp add:is_type_def)(*>*)


translations
  "types P" == "Collect (is_type P)"

end