Theory Decl

Up to index of Isabelle/HOL/arrays

(*  Title:      HOL/MicroJava/J/Decl.thy
    ID:         $Id: Decl.html,v 1.1 2002/11/28 16:11:18 kleing Exp $
    Author:     David von Oheimb
    Copyright   1999 Technische Universitaet Muenchen
*)

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

theory Decl = Type:

types 
  fdecl    = "vname × ty"        -- "field declaration, cf. 8.3 (, 9.3)"
  sig      = "mname × ty list"   -- "signature of a method, cf. 8.4.2"
  'c mdecl = "sig × ty × 'c"     -- "method declaration in a class"
  'c class = "cname × fdecl list × 'c mdecl list" 
  -- "class = superclass, fields, methods"

  'c cdecl = "cname × 'c class"  -- "class declaration, cf. 8.1"
  'c prog  = "'c cdecl list"     -- "program"

translations
  "fdecl"   <= (type) "vname × ty"
  "sig"     <= (type) "mname × ty list"
  "mdecl c" <= (type) "sig × 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 :: "'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

lemma class_SomeD:
  "class G C = Some D \<Longrightarrow> (C,D) \<in> set G"
  apply (unfold class_def)
  apply (erule map_of_SomeD)
  done  

consts
  is_type :: "'c prog \<Rightarrow> ty \<Rightarrow> bool"
  isrtype :: "'c prog \<Rightarrow> ref_ty \<Rightarrow> bool"
primrec 
  "is_type G (PrimT T)  = True"
        "is_type G (RefT T)   = isrtype G T"
        "isrtype G (NullT)    = True"
        "isrtype G (ClassT C) = is_class G C"
        "isrtype G (ArrayT T) = is_type  G T"  


consts
  is_RA :: "ty => bool"
recdef is_RA "{}"
  "is_RA (RA pc) = True"
  "is_RA t       = False"

end

lemma finite_is_class:

  finite (Collect (is_class G))

lemma class_SomeD:

  class G C = Some D ==> (C, D) : set G