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