src/HOL/NanoJava/Decl.thy
author wenzelm
Fri Mar 28 19:43:54 2008 +0100 (2008-03-28)
changeset 26462 dac4e2bce00d
parent 18551 be0705186ff5
child 32960 69916a850301
permissions -rw-r--r--
avoid rebinding of existing facts;
oheimb@11376
     1
(*  Title:      HOL/NanoJava/Decl.thy
oheimb@11376
     2
    ID:         $Id$
oheimb@11376
     3
    Author:     David von Oheimb
oheimb@11376
     4
    Copyright   2001 Technische Universitaet Muenchen
oheimb@11376
     5
*)
oheimb@11376
     6
oheimb@11376
     7
header "Types, class Declarations, and whole programs"
oheimb@11376
     8
haftmann@16417
     9
theory Decl imports Term begin
oheimb@11376
    10
oheimb@11376
    11
datatype ty
oheimb@11558
    12
  = NT           --{* null type  *}
oheimb@11558
    13
  | Class cname  --{* class type *}
oheimb@11376
    14
oheimb@11565
    15
text{* Field declaration *}
oheimb@11558
    16
types	fdecl		
oheimb@11558
    17
	= "fname \<times> ty"
oheimb@11376
    18
oheimb@11558
    19
record  methd		
oheimb@11376
    20
	= par :: ty 
oheimb@11376
    21
          res :: ty 
oheimb@11376
    22
          lcl ::"(vname \<times> ty) list"
oheimb@11376
    23
          bdy :: stmt
oheimb@11376
    24
oheimb@11565
    25
text{* Method declaration *}
oheimb@11558
    26
types	mdecl
oheimb@11376
    27
        = "mname \<times> methd"
oheimb@11376
    28
haftmann@18551
    29
record	"class"
oheimb@11376
    30
	= super   :: cname
wenzelm@12264
    31
          flds    ::"fdecl list"
oheimb@11376
    32
          methods ::"mdecl list"
oheimb@11376
    33
oheimb@11565
    34
text{* Class declaration *}
oheimb@11558
    35
types	cdecl
oheimb@11376
    36
	= "cname \<times> class"
oheimb@11376
    37
oheimb@11376
    38
types   prog
oheimb@11376
    39
        = "cdecl list"
oheimb@11376
    40
oheimb@11376
    41
translations
oheimb@11558
    42
  "fdecl" \<leftharpoondown> (type)"fname \<times> ty"
oheimb@11376
    43
  "mdecl" \<leftharpoondown> (type)"mname \<times> ty \<times> ty \<times> stmt"
oheimb@11376
    44
  "class" \<leftharpoondown> (type)"cname \<times> fdecl list \<times> mdecl list"
oheimb@11376
    45
  "cdecl" \<leftharpoondown> (type)"cname \<times> class"
oheimb@11376
    46
  "prog " \<leftharpoondown> (type)"cdecl list"
oheimb@11376
    47
oheimb@11376
    48
consts
oheimb@11376
    49
oheimb@11558
    50
  Prog    :: prog	--{* program as a global value *}
oheimb@11558
    51
  Object  :: cname	--{* name of root class *}
oheimb@11376
    52
oheimb@11376
    53
oheimb@11376
    54
constdefs
haftmann@18551
    55
  "class"	     :: "cname \<rightharpoonup> class"
oheimb@11376
    56
 "class      \<equiv> map_of Prog"
oheimb@11376
    57
oheimb@11376
    58
  is_class   :: "cname => bool"
oheimb@11376
    59
 "is_class C \<equiv> class C \<noteq> None"
oheimb@11376
    60
oheimb@11376
    61
lemma finite_is_class: "finite {C. is_class C}"
oheimb@11376
    62
apply (unfold is_class_def class_def)
oheimb@11376
    63
apply (fold dom_def)
oheimb@11376
    64
apply (rule finite_dom_map_of)
oheimb@11376
    65
done
oheimb@11376
    66
oheimb@11376
    67
end