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