author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 42463  f270e3e18be5 
child 55466  786edc984c98 
permissions  rwrr 
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 

42463  20 
type_synonym fields 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

21 
= "(fname \<rightharpoonup> val)" 
11376  22 

42463  23 
type_synonym 
11376  24 
obj = "cname \<times> fields" 
25 

26 
translations 

35431  27 
(type) "fields" \<leftharpoondown> (type) "fname => val option" 
28 
(type) "obj" \<leftharpoondown> (type) "cname \<times> fields" 

11376  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: *} 
42463  34 
type_synonym heap = "loc \<rightharpoonup> obj" 
35 
type_synonym 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 tabwidth;
wenzelm
parents:
30235
diff
changeset

39 
= heap :: heap 
11376  40 
locals :: locals 
41 

42 
translations 

35431  43 
(type) "heap" \<leftharpoondown> (type) "loc => obj option" 
44 
(type) "locals" \<leftharpoondown> (type) "vname => val option" 

45 
(type) "state" \<leftharpoondown> (type) "(heap :: heap, locals :: locals)" 

11376  46 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32960
diff
changeset

47 
definition del_locs :: "state => state" where 
11772  48 
"del_locs s \<equiv> s ( locals := empty )" 
11497
0e66e0114d9a
corrected initialization of locals, streamlined Impl
oheimb
parents:
11376
diff
changeset

49 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32960
diff
changeset

50 
definition init_locs :: "cname => mname => state => state" where 
11565  51 
"init_locs C m s \<equiv> s ( locals := locals s ++ 
52 
init_vars (map_of (lcl (the (method C m)))) )" 

11376  53 

54 
text {* The first parameter of @{term set_locs} is of type @{typ state} 

55 
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

56 
definition set_locs :: "state => state => state" where 
11376  57 
"set_locs s s' \<equiv> s' ( locals := locals s )" 
58 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32960
diff
changeset

59 
definition get_local :: "state => vname => val" ("_<_>" [99,0] 99) where 
11376  60 
"get_local s x \<equiv> the (locals s x)" 
61 

11558
6539627881e8
simplified vnam/vname, introduced fname, improved comments
oheimb
parents:
11507
diff
changeset

62 
{* local function: *} 
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32960
diff
changeset

63 
definition get_obj :: "state => loc => obj" where 
11376  64 
"get_obj s a \<equiv> the (heap s a)" 
65 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32960
diff
changeset

66 
definition obj_class :: "state => loc => cname" where 
11376  67 
"obj_class s a \<equiv> fst (get_obj s a)" 
68 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32960
diff
changeset

69 
definition get_field :: "state => loc => fname => val" where 
11376  70 
"get_field s a f \<equiv> the (snd (get_obj s a) f)" 
71 

11558
6539627881e8
simplified vnam/vname, introduced fname, improved comments
oheimb
parents:
11507
diff
changeset

72 
{* local function: *} 
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32960
diff
changeset

73 
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

74 
"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

75 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32960
diff
changeset

76 
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

77 
"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

78 

35355
613e133966ea
modernized syntax declarations, and make them actually work with authentic syntax;
wenzelm
parents:
32960
diff
changeset

79 
notation (xsymbols) 
613e133966ea
modernized syntax declarations, and make them actually work with authentic syntax;
wenzelm
parents:
32960
diff
changeset

80 
hupd ("hupd'(_\<mapsto>_')" [10,10] 1000) and 
613e133966ea
modernized syntax declarations, and make them actually work with authentic syntax;
wenzelm
parents:
32960
diff
changeset

81 
lupd ("lupd'(_\<mapsto>_')" [10,10] 1000) 
11558
6539627881e8
simplified vnam/vname, introduced fname, improved comments
oheimb
parents:
11507
diff
changeset

82 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32960
diff
changeset

83 
definition new_obj :: "loc => cname => state => state" where 
11376  84 
"new_obj a C \<equiv> hupd(a\<mapsto>(C,init_vars (field C)))" 
85 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32960
diff
changeset

86 
definition upd_obj :: "loc => fname => val => state => state" where 
11376  87 
"upd_obj a f v s \<equiv> let (C,fs) = the (heap s a) in hupd(a\<mapsto>(C,fs(f\<mapsto>v))) s" 
88 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32960
diff
changeset

89 
definition new_Addr :: "state => val" where 
11376  90 
"new_Addr s == SOME v. (\<exists>a. v = Addr a \<and> (heap s) a = None)  v = Null" 
91 

11565  92 

93 
subsection "Properties not used in the meta theory" 

94 

95 
lemma locals_upd_id [simp]: "s\<lparr>locals := locals s\<rparr> = s" 

96 
by simp 

97 

98 
lemma lupd_get_local_same [simp]: "lupd(x\<mapsto>v) s<x> = v" 

99 
by (simp add: lupd_def get_local_def) 

100 

101 
lemma lupd_get_local_other [simp]: "x \<noteq> y \<Longrightarrow> lupd(x\<mapsto>v) s<y> = s<y>" 

102 
apply (drule not_sym) 

103 
by (simp add: lupd_def get_local_def) 

104 

105 
lemma get_field_lupd [simp]: 

106 
"get_field (lupd(x\<mapsto>y) s) a f = get_field s a f" 

107 
by (simp add: lupd_def get_field_def get_obj_def) 

108 

109 
lemma get_field_set_locs [simp]: 

110 
"get_field (set_locs l s) a f = get_field s a f" 

111 
by (simp add: lupd_def get_field_def set_locs_def get_obj_def) 

112 

13524  113 
lemma get_field_del_locs [simp]: 
11772  114 
"get_field (del_locs s) a f = get_field s a f" 
115 
by (simp add: lupd_def get_field_def del_locs_def get_obj_def) 

11565  116 

117 
lemma new_obj_get_local [simp]: "new_obj a C s <x> = s<x>" 

118 
by (simp add: new_obj_def hupd_def get_local_def) 

119 

120 
lemma heap_lupd [simp]: "heap (lupd(x\<mapsto>y) s) = heap s" 

121 
by (simp add: lupd_def) 

122 

123 
lemma heap_hupd_same [simp]: "heap (hupd(a\<mapsto>obj) s) a = Some obj" 

124 
by (simp add: hupd_def) 

125 

126 
lemma heap_hupd_other [simp]: "aa \<noteq> a \<Longrightarrow> heap (hupd(aa\<mapsto>obj) s) a = heap s a" 

127 
apply (drule not_sym) 

128 
by (simp add: hupd_def) 

129 

130 
lemma hupd_hupd [simp]: "hupd(a\<mapsto>obj) (hupd(a\<mapsto>obj') s) = hupd(a\<mapsto>obj) s" 

131 
by (simp add: hupd_def) 

132 

11772  133 
lemma heap_del_locs [simp]: "heap (del_locs s) = heap s" 
134 
by (simp add: del_locs_def) 

11565  135 

136 
lemma heap_set_locs [simp]: "heap (set_locs l s) = heap s" 

137 
by (simp add: set_locs_def) 

138 

139 
lemma hupd_lupd [simp]: 

140 
"hupd(a\<mapsto>obj) (lupd(x\<mapsto>y) s) = lupd(x\<mapsto>y) (hupd(a\<mapsto>obj) s)" 

141 
by (simp add: hupd_def lupd_def) 

142 

11772  143 
lemma hupd_del_locs [simp]: 
144 
"hupd(a\<mapsto>obj) (del_locs s) = del_locs (hupd(a\<mapsto>obj) s)" 

145 
by (simp add: hupd_def del_locs_def) 

11565  146 

147 
lemma new_obj_lupd [simp]: 

148 
"new_obj a C (lupd(x\<mapsto>y) s) = lupd(x\<mapsto>y) (new_obj a C s)" 

149 
by (simp add: new_obj_def) 

150 

11772  151 
lemma new_obj_del_locs [simp]: 
152 
"new_obj a C (del_locs s) = del_locs (new_obj a C s)" 

11565  153 
by (simp add: new_obj_def) 
154 

155 
lemma upd_obj_lupd [simp]: 

156 
"upd_obj a f v (lupd(x\<mapsto>y) s) = lupd(x\<mapsto>y) (upd_obj a f v s)" 

157 
by (simp add: upd_obj_def Let_def split_beta) 

158 

11772  159 
lemma upd_obj_del_locs [simp]: 
160 
"upd_obj a f v (del_locs s) = del_locs (upd_obj a f v s)" 

11565  161 
by (simp add: upd_obj_def Let_def split_beta) 
162 

163 
lemma get_field_hupd_same [simp]: 

164 
"get_field (hupd(a\<mapsto>(C, fs)) s) a = the \<circ> fs" 

165 
apply (rule ext) 

166 
by (simp add: get_field_def get_obj_def) 

167 

168 
lemma get_field_hupd_other [simp]: 

169 
"aa \<noteq> a \<Longrightarrow> get_field (hupd(aa\<mapsto>obj) s) a = get_field s a" 

170 
apply (rule ext) 

171 
by (simp add: get_field_def get_obj_def) 

172 

11376  173 
lemma new_AddrD: 
174 
"new_Addr s = v \<Longrightarrow> (\<exists>a. v = Addr a \<and> heap s a = None)  v = Null" 

175 
apply (unfold new_Addr_def) 

176 
apply (erule subst) 

177 
apply (rule someI) 

178 
apply (rule disjI2) 

179 
apply (rule HOL.refl) 

180 
done 

181 

182 
end 