src/HOL/NanoJava/Decl.thy
author wenzelm
Sun Sep 18 20:33:48 2016 +0200 (2016-09-18)
changeset 63915 bab633745c7f
parent 63167 0909deb8059b
child 67443 3abf6a722518
permissions -rw-r--r--
tuned proofs;
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
wenzelm@58889
     6
section "Types, class Declarations, and whole programs"
oheimb@11376
     7
haftmann@16417
     8
theory Decl imports Term begin
oheimb@11376
     9
blanchet@58310
    10
datatype ty
wenzelm@63167
    11
  = NT           \<comment>\<open>null type\<close>
wenzelm@63167
    12
  | Class cname  \<comment>\<open>class type\<close>
oheimb@11376
    13
wenzelm@63167
    14
text\<open>Field declaration\<close>
wenzelm@42463
    15
type_synonym 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
wenzelm@63167
    24
text\<open>Method declaration\<close>
wenzelm@42463
    25
type_synonym 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
wenzelm@63167
    33
text\<open>Class declaration\<close>
wenzelm@42463
    34
type_synonym cdecl
wenzelm@32960
    35
        = "cname \<times> class"
oheimb@11376
    36
wenzelm@42463
    37
type_synonym 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
krauss@44375
    47
axiomatization
wenzelm@63167
    48
  Prog    :: prog       \<comment>\<open>program as a global value\<close>
krauss@44375
    49
and
wenzelm@63167
    50
  Object  :: cname      \<comment>\<open>name of root class\<close>
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