# HG changeset patch
# User krauss
# Date 1288088342 -7200
# Node ID 0ffdd6baec03de13e5a11e0b22863db245184585
# Parent  008dc2d2c39584fcb7446e5261358e047d82dcee
added Heap monad instance of partial_function package

diff -r 008dc2d2c395 -r 0ffdd6baec03 src/HOL/Imperative_HOL/Heap_Monad.thy
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Tue Oct 26 12:19:02 2010 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Tue Oct 26 12:19:02 2010 +0200
@@ -594,6 +594,75 @@
 *}
 
 
+section {* Partial function definition setup *}
+
+definition "Heap_ord = img_ord execute (fun_ord option_ord)"
+definition "Heap_lub = img_lub execute Heap (fun_lub (flat_lub None))"
+
+interpretation heap!:
+  partial_function_definitions Heap_ord Heap_lub
+unfolding Heap_ord_def Heap_lub_def
+apply (rule partial_function_image)
+apply (rule partial_function_lift)
+apply (rule flat_interpretation)
+by (auto intro: Heap_eqI)
+
+abbreviation "mono_Heap \<equiv> monotone (fun_ord Heap_ord) Heap_ord"
+
+lemma Heap_ordI:
+  assumes "\<And>h. execute x h = None \<or> execute x h = execute y h"
+  shows "Heap_ord x y"
+using assms unfolding Heap_ord_def img_ord_def fun_ord_def flat_ord_def
+by blast
+
+lemma Heap_ordE:
+  assumes "Heap_ord x y"
+  obtains "execute x h = None" | "execute x h = execute y h"
+using assms unfolding Heap_ord_def img_ord_def fun_ord_def flat_ord_def
+by atomize_elim blast
+
+
+lemma bind_mono[partial_function_mono]:
+assumes mf: "mono_Heap B" and mg: "\<And>y. mono_Heap (\<lambda>f. C y f)"
+shows "mono_Heap (\<lambda>f. B f \<guillemotright>= (\<lambda>y. C y f))"
+proof (rule monotoneI)
+  fix f g :: "'a \<Rightarrow> 'b Heap" assume fg: "fun_ord Heap_ord f g"
+  from mf
+  have 1: "Heap_ord (B f) (B g)" by (rule monotoneD) (rule fg)
+  from mg
+  have 2: "\<And>y'. Heap_ord (C y' f) (C y' g)" by (rule monotoneD) (rule fg)
+
+  have "Heap_ord (B f \<guillemotright>= (\<lambda>y. C y f)) (B g \<guillemotright>= (\<lambda>y. C y f))"
+    (is "Heap_ord ?L ?R")
+  proof (rule Heap_ordI)
+    fix h
+    from 1 show "execute ?L h = None \<or> execute ?L h = execute ?R h"
+      by (rule Heap_ordE[where h = h]) (auto simp: execute_bind_case)
+  qed
+  also
+  have "Heap_ord (B g \<guillemotright>= (\<lambda>y'. C y' f)) (B g \<guillemotright>= (\<lambda>y'. C y' g))"
+    (is "Heap_ord ?L ?R")
+  proof (rule Heap_ordI)
+    fix h
+    show "execute ?L h = None \<or> execute ?L h = execute ?R h"
+    proof (cases "execute (B g) h")
+      case None
+      then have "execute ?L h = None" by (auto simp: execute_bind_case)
+      thus ?thesis ..
+    next
+      case Some
+      then obtain r h' where "execute (B g) h = Some (r, h')"
+        by (metis surjective_pairing)
+      then have "execute ?L h = execute (C r f) h'"
+        "execute ?R h = execute (C r g) h'"
+        by (auto simp: execute_bind_case)
+      with 2[of r] show ?thesis by (auto elim: Heap_ordE)
+    qed
+  qed
+  finally (heap.leq_trans)
+  show "Heap_ord (B f \<guillemotright>= (\<lambda>y. C y f)) (B g \<guillemotright>= (\<lambda>y'. C y' g))" .
+qed
+
 hide_const (open) Heap heap guard raise' fold_map
 
 end