forked from afp-mirror/Core_DOM
Added more heap-related methods.
This commit is contained in:
parent
7e21f2119d
commit
544feb6b9c
|
@ -96,6 +96,11 @@ definition
|
|||
lemma [code]: "returns_result_heap h p r h' \<longleftrightarrow> (case h \<turnstile> p of Inr (r', h'') \<Rightarrow> r = r' \<and> h' = h'' | Inl _ \<Rightarrow> False)"
|
||||
by(auto simp add: returns_result_heap_def returns_result_def returns_heap_def split: sum.splits)
|
||||
|
||||
fun select_result_heap ("|(_)|\<^sub>r\<^sub>h")
|
||||
where
|
||||
"select_result_heap (Inr (r, h)) = (r, h)"
|
||||
| "select_result_heap (Inl _) = undefined"
|
||||
|
||||
definition
|
||||
returns_error :: "'heap \<Rightarrow> ('heap, 'e, 'result) prog \<Rightarrow> 'e \<Rightarrow> bool"
|
||||
("((_)/ \<turnstile> (_)/ \<rightarrow>\<^sub>e (_))" [60, 35, 61] 65)
|
||||
|
|
Reference in New Issue