author | haftmann |
Mon, 01 Mar 2010 13:40:23 +0100 | |
changeset 35416 | d8d7d1b785af |
parent 32960 | 69916a850301 |
child 35417 | 47ee18b6ae32 |
permissions | -rw-r--r-- |
11376 | 1 |
(* Title: HOL/NanoJava/State.thy |
2 |
Author: David von Oheimb |
|
3 |
Copyright 2001 Technische Universitaet Muenchen |
|
4 |
*) |
|
5 |
||
6 |
header "Program State" |
|
7 |
||
16417 | 8 |
theory State imports TypeRel begin |
11376 | 9 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32960
diff
changeset
|
10 |
definition body :: "cname \<times> mname => stmt" where |
11497
0e66e0114d9a
corrected initialization of locals, streamlined Impl
oheimb
parents:
11376
diff
changeset
|
11 |
"body \<equiv> \<lambda>(C,m). bdy (the (method C m))" |
11376 | 12 |
|
11565 | 13 |
text {* Locations, i.e.\ abstract references to objects *} |
11376 | 14 |
typedecl loc |
15 |
||
16 |
datatype val |
|
11558
6539627881e8
simplified vnam/vname, introduced fname, improved comments
oheimb
parents:
11507
diff
changeset
|
17 |
= Null --{* null reference *} |
6539627881e8
simplified vnam/vname, introduced fname, improved comments
oheimb
parents:
11507
diff
changeset
|
18 |
| Addr loc --{* address, i.e. location of object *} |
11376 | 19 |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
20 |
types fields |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
21 |
= "(fname \<rightharpoonup> val)" |
11376 | 22 |
|
23 |
obj = "cname \<times> fields" |
|
24 |
||
25 |
translations |
|
26 |
||
11558
6539627881e8
simplified vnam/vname, introduced fname, improved comments
oheimb
parents:
11507
diff
changeset
|
27 |
"fields" \<leftharpoondown> (type)"fname => val option" |
11376 | 28 |
"obj" \<leftharpoondown> (type)"cname \<times> fields" |
29 |
||
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32960
diff
changeset
|
30 |
definition init_vars :: "('a \<rightharpoonup> 'b) => ('a \<rightharpoonup> val)" where |
30235
58d147683393
Made Option a separate theory and renamed option_map to Option.map
nipkow
parents:
16417
diff
changeset
|
31 |
"init_vars m == Option.map (\<lambda>T. Null) o m" |
11376 | 32 |
|
11565 | 33 |
text {* private: *} |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
34 |
types heap = "loc \<rightharpoonup> obj" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
35 |
locals = "vname \<rightharpoonup> val" |
11376 | 36 |
|
11565 | 37 |
text {* private: *} |
11376 | 38 |
record state |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
30235
diff
changeset
|
39 |
= heap :: heap |
11376 | 40 |
locals :: locals |
41 |
||
42 |
translations |
|
43 |
||
44 |
"heap" \<leftharpoondown> (type)"loc => obj option" |
|
45 |
"locals" \<leftharpoondown> (type)"vname => val option" |
|
46 |
"state" \<leftharpoondown> (type)"(|heap :: heap, locals :: locals|)" |
|
47 |
||
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32960
diff
changeset
|
48 |
definition del_locs :: "state => state" where |
11772 | 49 |
"del_locs s \<equiv> s (| locals := empty |)" |
11497
0e66e0114d9a
corrected initialization of locals, streamlined Impl
oheimb
parents:
11376
diff
changeset
|
50 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32960
diff
changeset
|
51 |
definition init_locs :: "cname => mname => state => state" where |
11565 | 52 |
"init_locs C m s \<equiv> s (| locals := locals s ++ |
53 |
init_vars (map_of (lcl (the (method C m)))) |)" |
|
11376 | 54 |
|
55 |
text {* The first parameter of @{term set_locs} is of type @{typ state} |
|
56 |
rather than @{typ locals} in order to keep @{typ locals} private.*} |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32960
diff
changeset
|
57 |
definition set_locs :: "state => state => state" where |
11376 | 58 |
"set_locs s s' \<equiv> s' (| locals := locals s |)" |
59 |
||
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32960
diff
changeset
|
60 |
definition get_local :: "state => vname => val" ("_<_>" [99,0] 99) where |
11376 | 61 |
"get_local s x \<equiv> the (locals s x)" |
62 |
||
11558
6539627881e8
simplified vnam/vname, introduced fname, improved comments
oheimb
parents:
11507
diff
changeset
|
63 |
--{* local function: *} |
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32960
diff
changeset
|
64 |
definition get_obj :: "state => loc => obj" where |
11376 | 65 |
"get_obj s a \<equiv> the (heap s a)" |
66 |
||
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32960
diff
changeset
|
67 |
definition obj_class :: "state => loc => cname" where |
11376 | 68 |
"obj_class s a \<equiv> fst (get_obj s a)" |
69 |
||
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32960
diff
changeset
|
70 |
definition get_field :: "state => loc => fname => val" where |
11376 | 71 |
"get_field s a f \<equiv> the (snd (get_obj s a) f)" |
72 |
||
11558
6539627881e8
simplified vnam/vname, introduced fname, improved comments
oheimb
parents:
11507
diff
changeset
|
73 |
--{* local function: *} |
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32960
diff
changeset
|
74 |
definition hupd :: "loc => obj => state => state" ("hupd'(_|->_')" [10,10] 1000) where |
11558
6539627881e8
simplified vnam/vname, introduced fname, improved comments
oheimb
parents:
11507
diff
changeset
|
75 |
"hupd a obj s \<equiv> s (| heap := ((heap s)(a\<mapsto>obj))|)" |
6539627881e8
simplified vnam/vname, introduced fname, improved comments
oheimb
parents:
11507
diff
changeset
|
76 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32960
diff
changeset
|
77 |
definition lupd :: "vname => val => state => state" ("lupd'(_|->_')" [10,10] 1000) where |
11558
6539627881e8
simplified vnam/vname, introduced fname, improved comments
oheimb
parents:
11507
diff
changeset
|
78 |
"lupd x v s \<equiv> s (| locals := ((locals s)(x\<mapsto>v ))|)" |
6539627881e8
simplified vnam/vname, introduced fname, improved comments
oheimb
parents:
11507
diff
changeset
|
79 |
|
6539627881e8
simplified vnam/vname, introduced fname, improved comments
oheimb
parents:
11507
diff
changeset
|
80 |
syntax (xsymbols) |
6539627881e8
simplified vnam/vname, introduced fname, improved comments
oheimb
parents:
11507
diff
changeset
|
81 |
hupd :: "loc => obj => state => state" ("hupd'(_\<mapsto>_')" [10,10] 1000) |
6539627881e8
simplified vnam/vname, introduced fname, improved comments
oheimb
parents:
11507
diff
changeset
|
82 |
lupd :: "vname => val => state => state" ("lupd'(_\<mapsto>_')" [10,10] 1000) |
6539627881e8
simplified vnam/vname, introduced fname, improved comments
oheimb
parents:
11507
diff
changeset
|
83 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32960
diff
changeset
|
84 |
definition new_obj :: "loc => cname => state => state" where |
11376 | 85 |
"new_obj a C \<equiv> hupd(a\<mapsto>(C,init_vars (field C)))" |
86 |
||
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32960
diff
changeset
|
87 |
definition upd_obj :: "loc => fname => val => state => state" where |
11376 | 88 |
"upd_obj a f v s \<equiv> let (C,fs) = the (heap s a) in hupd(a\<mapsto>(C,fs(f\<mapsto>v))) s" |
89 |
||
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32960
diff
changeset
|
90 |
definition new_Addr :: "state => val" where |
11376 | 91 |
"new_Addr s == SOME v. (\<exists>a. v = Addr a \<and> (heap s) a = None) | v = Null" |
92 |
||
11565 | 93 |
|
94 |
subsection "Properties not used in the meta theory" |
|
95 |
||
96 |
lemma locals_upd_id [simp]: "s\<lparr>locals := locals s\<rparr> = s" |
|
97 |
by simp |
|
98 |
||
99 |
lemma lupd_get_local_same [simp]: "lupd(x\<mapsto>v) s<x> = v" |
|
100 |
by (simp add: lupd_def get_local_def) |
|
101 |
||
102 |
lemma lupd_get_local_other [simp]: "x \<noteq> y \<Longrightarrow> lupd(x\<mapsto>v) s<y> = s<y>" |
|
103 |
apply (drule not_sym) |
|
104 |
by (simp add: lupd_def get_local_def) |
|
105 |
||
106 |
lemma get_field_lupd [simp]: |
|
107 |
"get_field (lupd(x\<mapsto>y) s) a f = get_field s a f" |
|
108 |
by (simp add: lupd_def get_field_def get_obj_def) |
|
109 |
||
110 |
lemma get_field_set_locs [simp]: |
|
111 |
"get_field (set_locs l s) a f = get_field s a f" |
|
112 |
by (simp add: lupd_def get_field_def set_locs_def get_obj_def) |
|
113 |
||
13524 | 114 |
lemma get_field_del_locs [simp]: |
11772 | 115 |
"get_field (del_locs s) a f = get_field s a f" |
116 |
by (simp add: lupd_def get_field_def del_locs_def get_obj_def) |
|
11565 | 117 |
|
118 |
lemma new_obj_get_local [simp]: "new_obj a C s <x> = s<x>" |
|
119 |
by (simp add: new_obj_def hupd_def get_local_def) |
|
120 |
||
121 |
lemma heap_lupd [simp]: "heap (lupd(x\<mapsto>y) s) = heap s" |
|
122 |
by (simp add: lupd_def) |
|
123 |
||
124 |
lemma heap_hupd_same [simp]: "heap (hupd(a\<mapsto>obj) s) a = Some obj" |
|
125 |
by (simp add: hupd_def) |
|
126 |
||
127 |
lemma heap_hupd_other [simp]: "aa \<noteq> a \<Longrightarrow> heap (hupd(aa\<mapsto>obj) s) a = heap s a" |
|
128 |
apply (drule not_sym) |
|
129 |
by (simp add: hupd_def) |
|
130 |
||
131 |
lemma hupd_hupd [simp]: "hupd(a\<mapsto>obj) (hupd(a\<mapsto>obj') s) = hupd(a\<mapsto>obj) s" |
|
132 |
by (simp add: hupd_def) |
|
133 |
||
11772 | 134 |
lemma heap_del_locs [simp]: "heap (del_locs s) = heap s" |
135 |
by (simp add: del_locs_def) |
|
11565 | 136 |
|
137 |
lemma heap_set_locs [simp]: "heap (set_locs l s) = heap s" |
|
138 |
by (simp add: set_locs_def) |
|
139 |
||
140 |
lemma hupd_lupd [simp]: |
|
141 |
"hupd(a\<mapsto>obj) (lupd(x\<mapsto>y) s) = lupd(x\<mapsto>y) (hupd(a\<mapsto>obj) s)" |
|
142 |
by (simp add: hupd_def lupd_def) |
|
143 |
||
11772 | 144 |
lemma hupd_del_locs [simp]: |
145 |
"hupd(a\<mapsto>obj) (del_locs s) = del_locs (hupd(a\<mapsto>obj) s)" |
|
146 |
by (simp add: hupd_def del_locs_def) |
|
11565 | 147 |
|
148 |
lemma new_obj_lupd [simp]: |
|
149 |
"new_obj a C (lupd(x\<mapsto>y) s) = lupd(x\<mapsto>y) (new_obj a C s)" |
|
150 |
by (simp add: new_obj_def) |
|
151 |
||
11772 | 152 |
lemma new_obj_del_locs [simp]: |
153 |
"new_obj a C (del_locs s) = del_locs (new_obj a C s)" |
|
11565 | 154 |
by (simp add: new_obj_def) |
155 |
||
156 |
lemma upd_obj_lupd [simp]: |
|
157 |
"upd_obj a f v (lupd(x\<mapsto>y) s) = lupd(x\<mapsto>y) (upd_obj a f v s)" |
|
158 |
by (simp add: upd_obj_def Let_def split_beta) |
|
159 |
||
11772 | 160 |
lemma upd_obj_del_locs [simp]: |
161 |
"upd_obj a f v (del_locs s) = del_locs (upd_obj a f v s)" |
|
11565 | 162 |
by (simp add: upd_obj_def Let_def split_beta) |
163 |
||
164 |
lemma get_field_hupd_same [simp]: |
|
165 |
"get_field (hupd(a\<mapsto>(C, fs)) s) a = the \<circ> fs" |
|
166 |
apply (rule ext) |
|
167 |
by (simp add: get_field_def get_obj_def) |
|
168 |
||
169 |
lemma get_field_hupd_other [simp]: |
|
170 |
"aa \<noteq> a \<Longrightarrow> get_field (hupd(aa\<mapsto>obj) s) a = get_field s a" |
|
171 |
apply (rule ext) |
|
172 |
by (simp add: get_field_def get_obj_def) |
|
173 |
||
11376 | 174 |
lemma new_AddrD: |
175 |
"new_Addr s = v \<Longrightarrow> (\<exists>a. v = Addr a \<and> heap s a = None) | v = Null" |
|
176 |
apply (unfold new_Addr_def) |
|
177 |
apply (erule subst) |
|
178 |
apply (rule someI) |
|
179 |
apply (rule disjI2) |
|
180 |
apply (rule HOL.refl) |
|
181 |
done |
|
182 |
||
183 |
end |