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