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