40 |
40 |
41 definition ref :: "'a\<Colon>heap \<Rightarrow> 'a ref Heap" where |
41 definition ref :: "'a\<Colon>heap \<Rightarrow> 'a ref Heap" where |
42 [code del]: "ref v = Heap_Monad.heap (alloc v)" |
42 [code del]: "ref v = Heap_Monad.heap (alloc v)" |
43 |
43 |
44 definition lookup :: "'a\<Colon>heap ref \<Rightarrow> 'a Heap" ("!_" 61) where |
44 definition lookup :: "'a\<Colon>heap ref \<Rightarrow> 'a Heap" ("!_" 61) where |
45 [code del]: "lookup r = Heap_Monad.heap (\<lambda>h. (get h r, h))" |
45 [code del]: "lookup r = Heap_Monad.tap (\<lambda>h. get h r)" |
46 |
46 |
47 definition update :: "'a ref \<Rightarrow> 'a\<Colon>heap \<Rightarrow> unit Heap" ("_ := _" 62) where |
47 definition update :: "'a ref \<Rightarrow> 'a\<Colon>heap \<Rightarrow> unit Heap" ("_ := _" 62) where |
48 [code del]: "update r v = Heap_Monad.heap (\<lambda>h. ((), set r v h))" |
48 [code del]: "update r v = Heap_Monad.heap (\<lambda>h. ((), set r v h))" |
49 |
49 |
50 definition change :: "('a\<Colon>heap \<Rightarrow> 'a) \<Rightarrow> 'a ref \<Rightarrow> 'a Heap" where |
50 definition change :: "('a\<Colon>heap \<Rightarrow> 'a) \<Rightarrow> 'a ref \<Rightarrow> 'a Heap" where |
124 |
126 |
125 lemma noteq_I: |
127 lemma noteq_I: |
126 "present h r \<Longrightarrow> \<not> present h r' \<Longrightarrow> r =!= r'" |
128 "present h r \<Longrightarrow> \<not> present h r' \<Longrightarrow> r =!= r'" |
127 by (auto simp add: noteq_def present_def) |
129 by (auto simp add: noteq_def present_def) |
128 |
130 |
129 lemma execute_ref [simp]: |
131 |
130 "Heap_Monad.execute (ref v) h = Some (alloc v h)" |
132 text {* Monad operations *} |
|
133 |
|
134 lemma execute_ref [simp, execute_simps]: |
|
135 "execute (ref v) h = Some (alloc v h)" |
131 by (simp add: ref_def) |
136 by (simp add: ref_def) |
132 |
137 |
133 lemma execute_lookup [simp]: |
138 lemma success_refI [iff, success_intros]: |
|
139 "success (ref v) h" |
|
140 by (auto simp add: ref_def) |
|
141 |
|
142 lemma execute_lookup [simp, execute_simps]: |
134 "Heap_Monad.execute (lookup r) h = Some (get h r, h)" |
143 "Heap_Monad.execute (lookup r) h = Some (get h r, h)" |
135 by (simp add: lookup_def) |
144 by (simp add: lookup_def) |
136 |
145 |
137 lemma execute_update [simp]: |
146 lemma success_lookupI [iff, success_intros]: |
|
147 "success (lookup r) h" |
|
148 by (auto simp add: lookup_def) |
|
149 |
|
150 lemma execute_update [simp, execute_simps]: |
138 "Heap_Monad.execute (update r v) h = Some ((), set r v h)" |
151 "Heap_Monad.execute (update r v) h = Some ((), set r v h)" |
139 by (simp add: update_def) |
152 by (simp add: update_def) |
140 |
153 |
141 lemma execute_change [simp]: |
154 lemma success_updateI [iff, success_intros]: |
|
155 "success (update r v) h" |
|
156 by (auto simp add: update_def) |
|
157 |
|
158 lemma execute_change [simp, execute_simps]: |
142 "Heap_Monad.execute (change f r) h = Some (f (get h r), set r (f (get h r)) h)" |
159 "Heap_Monad.execute (change f r) h = Some (f (get h r), set r (f (get h r)) h)" |
143 by (cases "!r" h rule: heap_cases) |
160 by (simp add: change_def bind_def Let_def) |
144 (simp_all only: change_def execute_bind, auto simp add: Let_def) |
161 |
|
162 lemma success_changeI [iff, success_intros]: |
|
163 "success (change f r) h" |
|
164 by (auto intro!: success_intros simp add: change_def) |
145 |
165 |
146 lemma lookup_chain: |
166 lemma lookup_chain: |
147 "(!r \<guillemotright> f) = f" |
167 "(!r \<guillemotright> f) = f" |
148 by (rule Heap_eqI) (simp add: lookup_def) |
168 by (rule Heap_eqI) (auto simp add: lookup_def execute_simps) |
149 |
169 |
150 lemma update_change [code]: |
170 lemma update_change [code]: |
151 "r := e = change (\<lambda>_. e) r \<guillemotright> return ()" |
171 "r := e = change (\<lambda>_. e) r \<guillemotright> return ()" |
152 by (rule Heap_eqI) (simp add: change_def lookup_chain) |
172 by (rule Heap_eqI) (simp add: change_def lookup_chain) |
153 |
173 |