src/HOL/MicroJava/J/Decl.thy
author wenzelm
Wed Mar 03 00:33:02 2010 +0100 (2010-03-03)
changeset 35431 8758fe1fc9f8
parent 35416 d8d7d1b785af
child 42463 f270e3e18be5
permissions -rw-r--r--
cleanup type translations;
     1 (*  Title:      HOL/MicroJava/J/Decl.thy
     2     Author:     David von Oheimb
     3     Copyright   1999 Technische Universitaet Muenchen
     4 *)
     5 
     6 header {* \isaheader{Class Declarations and Programs} *}
     7 
     8 theory Decl imports Type begin
     9 
    10 types 
    11   fdecl    = "vname \<times> ty"        -- "field declaration, cf. 8.3 (, 9.3)"
    12 
    13   sig      = "mname \<times> ty list"   -- "signature of a method, cf. 8.4.2"
    14 
    15   'c mdecl = "sig \<times> ty \<times> 'c"     -- "method declaration in a class"
    16 
    17   'c "class" = "cname \<times> fdecl list \<times> 'c mdecl list" 
    18   -- "class = superclass, fields, methods"
    19 
    20   'c cdecl = "cname \<times> 'c class"  -- "class declaration, cf. 8.1"
    21 
    22   'c prog  = "'c cdecl list"     -- "program"
    23 
    24 
    25 translations
    26   (type) "fdecl" <= (type) "vname \<times> ty"
    27   (type) "sig" <= (type) "mname \<times> ty list"
    28   (type) "'c mdecl" <= (type) "sig \<times> ty \<times> 'c"
    29   (type) "'c class" <= (type) "cname \<times> fdecl list \<times> ('c mdecl) list"
    30   (type) "'c cdecl" <= (type) "cname \<times> ('c class)"
    31   (type) "'c prog" <= (type) "('c cdecl) list"
    32 
    33 
    34 definition "class" :: "'c prog => (cname \<rightharpoonup> 'c class)" where
    35   "class \<equiv> map_of"
    36 
    37 definition is_class :: "'c prog => cname => bool" where
    38   "is_class G C \<equiv> class G C \<noteq> None"
    39 
    40 
    41 lemma finite_is_class: "finite {C. is_class G C}"
    42 apply (unfold is_class_def class_def)
    43 apply (fold dom_def)
    44 apply (rule finite_dom_map_of)
    45 done
    46 
    47 primrec is_type :: "'c prog => ty => bool" where
    48   "is_type G (PrimT pt) = True"
    49 | "is_type G (RefT t) = (case t of NullT => True | ClassT C => is_class G C)"
    50 
    51 end