# HG changeset patch
# User haftmann
# Date 1278687642 -7200
# Node ID 00ff97087ab54925821f8ceb5f0c81c578a5ff4d
# Parent  dc78d2d9e90a1f22691d8683cbc51cbe7ef8a84a# Parent  bf86a65403a8a6a39a3e08c17e91d55057c4fd70
merged

diff -r dc78d2d9e90a -r 00ff97087ab5 src/HOL/Imperative_HOL/Array.thy
--- a/src/HOL/Imperative_HOL/Array.thy	Fri Jul 09 16:32:25 2010 +0200
+++ b/src/HOL/Imperative_HOL/Array.thy	Fri Jul 09 17:00:42 2010 +0200
@@ -56,7 +56,7 @@
   [code del]: "make n f = Heap_Monad.heap (array (map f [0 ..< n]))"
 
 definition len :: "'a\<Colon>heap array \<Rightarrow> nat Heap" where
-  [code del]: "len a = Heap_Monad.heap (\<lambda>h. (length a h, h))"
+  [code del]: "len a = Heap_Monad.tap (\<lambda>h. length a h)"
 
 definition nth :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> 'a Heap" where
   [code del]: "nth a i = Heap_Monad.guard (\<lambda>h. i < length a h)
@@ -75,7 +75,7 @@
     (\<lambda>h. (get_array a h ! i, change a i x h))"
 
 definition freeze :: "'a\<Colon>heap array \<Rightarrow> 'a list Heap" where
-  [code del]: "freeze a = Heap_Monad.heap (\<lambda>h. (get_array a h, h))"
+  [code del]: "freeze a = Heap_Monad.tap (\<lambda>h. get_array a h)"
 
 
 subsection {* Properties *}
@@ -83,6 +83,8 @@
 text {* FIXME: Does there exist a "canonical" array axiomatisation in
 the literature?  *}
 
+text {* Primitives *}
+
 lemma noteq_arrs_sym: "a =!!= b \<Longrightarrow> b =!!= a"
   and unequal_arrs [simp]: "a \<noteq> a' \<longleftrightarrow> a =!!= a'"
   unfolding noteq_arrs_def by auto
@@ -153,50 +155,89 @@
   "array_present a (change b i v h) = array_present a h"
   by (simp add: change_def array_present_def set_array_def get_array_def)
 
-lemma execute_new [simp]:
-  "Heap_Monad.execute (new n x) h = Some (array (replicate n x) h)"
+
+text {* Monad operations *}
+
+lemma execute_new [simp, execute_simps]:
+  "execute (new n x) h = Some (array (replicate n x) h)"
+  by (simp add: new_def)
+
+lemma success_newI [iff, success_intros]:
+  "success (new n x) h"
   by (simp add: new_def)
 
-lemma execute_of_list [simp]:
-  "Heap_Monad.execute (of_list xs) h = Some (array xs h)"
+lemma execute_of_list [simp, execute_simps]:
+  "execute (of_list xs) h = Some (array xs h)"
+  by (simp add: of_list_def)
+
+lemma success_of_listI [iff, success_intros]:
+  "success (of_list xs) h"
   by (simp add: of_list_def)
 
-lemma execute_make [simp]:
-  "Heap_Monad.execute (make n f) h = Some (array (map f [0 ..< n]) h)"
+lemma execute_make [simp, execute_simps]:
+  "execute (make n f) h = Some (array (map f [0 ..< n]) h)"
   by (simp add: make_def)
 
-lemma execute_len [simp]:
-  "Heap_Monad.execute (len a) h = Some (length a h, h)"
+lemma success_makeI [iff, success_intros]:
+  "success (make n f) h"
+  by (simp add: make_def)
+
+lemma execute_len [simp, execute_simps]:
+  "execute (len a) h = Some (length a h, h)"
+  by (simp add: len_def)
+
+lemma success_lenI [iff, success_intros]:
+  "success (len a) h"
   by (simp add: len_def)
 
-lemma execute_nth [simp]:
+lemma execute_nth [execute_simps]:
   "i < length a h \<Longrightarrow>
-    Heap_Monad.execute (nth a i) h = Some (get_array a h ! i, h)"
-  "i \<ge> length a h \<Longrightarrow> Heap_Monad.execute (nth a i) h = None"
-  by (simp_all add: nth_def)
+    execute (nth a i) h = Some (get_array a h ! i, h)"
+  "i \<ge> length a h \<Longrightarrow> execute (nth a i) h = None"
+  by (simp_all add: nth_def execute_simps)
+
+lemma success_nthI [success_intros]:
+  "i < length a h \<Longrightarrow> success (nth a i) h"
+  by (auto intro: success_intros simp add: nth_def)
 
-lemma execute_upd [simp]:
+lemma execute_upd [execute_simps]:
   "i < length a h \<Longrightarrow>
-    Heap_Monad.execute (upd i x a) h = Some (a, change a i x h)"
-  "i \<ge> length a h \<Longrightarrow> Heap_Monad.execute (nth a i) h = None"
-  by (simp_all add: upd_def)
+    execute (upd i x a) h = Some (a, change a i x h)"
+  "i \<ge> length a h \<Longrightarrow> execute (nth a i) h = None"
+  by (simp_all add: upd_def execute_simps)
 
-lemma execute_map_entry [simp]:
+lemma success_updI [success_intros]:
+  "i < length a h \<Longrightarrow> success (upd i x a) h"
+  by (auto intro: success_intros simp add: upd_def)
+
+lemma execute_map_entry [execute_simps]:
   "i < length a h \<Longrightarrow>
-   Heap_Monad.execute (map_entry i f a) h =
+   execute (map_entry i f a) h =
       Some (a, change a i (f (get_array a h ! i)) h)"
-  "i \<ge> length a h \<Longrightarrow> Heap_Monad.execute (nth a i) h = None"
-  by (simp_all add: map_entry_def)
+  "i \<ge> length a h \<Longrightarrow> execute (nth a i) h = None"
+  by (simp_all add: map_entry_def execute_simps)
 
-lemma execute_swap [simp]:
+lemma success_map_entryI [success_intros]:
+  "i < length a h \<Longrightarrow> success (map_entry i f a) h"
+  by (auto intro: success_intros simp add: map_entry_def)
+
+lemma execute_swap [execute_simps]:
   "i < length a h \<Longrightarrow>
-   Heap_Monad.execute (swap i x a) h =
+   execute (swap i x a) h =
       Some (get_array a h ! i, change a i x h)"
-  "i \<ge> length a h \<Longrightarrow> Heap_Monad.execute (nth a i) h = None"
-  by (simp_all add: swap_def)
+  "i \<ge> length a h \<Longrightarrow> execute (nth a i) h = None"
+  by (simp_all add: swap_def execute_simps)
+
+lemma success_swapI [success_intros]:
+  "i < length a h \<Longrightarrow> success (swap i x a) h"
+  by (auto intro: success_intros simp add: swap_def)
 
-lemma execute_freeze [simp]:
-  "Heap_Monad.execute (freeze a) h = Some (get_array a h, h)"
+lemma execute_freeze [simp, execute_simps]:
+  "execute (freeze a) h = Some (get_array a h, h)"
+  by (simp add: freeze_def)
+
+lemma success_freezeI [iff, success_intros]:
+  "success (freeze a) h"
   by (simp add: freeze_def)
 
 lemma upd_return:
@@ -265,7 +306,7 @@
      x \<leftarrow> nth a i;
      upd i (f x) a
    done)"
-  by (rule Heap_eqI) (simp add: bind_def guard_def map_entry_def)
+  by (rule Heap_eqI) (simp add: bind_def guard_def map_entry_def execute_simps)
 
 lemma [code]:
   "swap i x a = (do
@@ -273,7 +314,7 @@
      upd i x a;
      return y
    done)"
-  by (rule Heap_eqI) (simp add: bind_def guard_def swap_def)
+  by (rule Heap_eqI) (simp add: bind_def guard_def swap_def execute_simps)
 
 lemma [code]:
   "freeze a = (do
@@ -288,18 +329,18 @@
      [0..<length a h] =
        List.map (List.nth (get_array a h)) [0..<length a h]"
     by simp
-  have "Heap_Monad.execute (Heap_Monad.fold_map (Array.nth a) [0..<length a h]) h =
+  have "execute (Heap_Monad.fold_map (Array.nth a) [0..<length a h]) h =
     Some (get_array a h, h)"
     apply (subst execute_fold_map_unchanged_heap)
     apply (simp_all add: nth_def guard_def *)
     apply (simp add: length_def map_nth)
     done
-  then have "Heap_Monad.execute (do
+  then have "execute (do
       n \<leftarrow> len a;
       Heap_Monad.fold_map (Array.nth a) [0..<n]
     done) h = Some (get_array a h, h)"
     by (auto intro: execute_eq_SomeI)
-  then show "Heap_Monad.execute (freeze a) h = Heap_Monad.execute (do
+  then show "execute (freeze a) h = execute (do
       n \<leftarrow> len a;
       Heap_Monad.fold_map (Array.nth a) [0..<n]
     done) h" by simp
diff -r dc78d2d9e90a -r 00ff97087ab5 src/HOL/Imperative_HOL/Heap_Monad.thy
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Jul 09 16:32:25 2010 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Jul 09 17:00:42 2010 +0200
@@ -10,7 +10,7 @@
 
 subsection {* The monad *}
 
-subsubsection {* Monad combinators *}
+subsubsection {* Monad construction *}
 
 text {* Monadic heap actions either produce values
   and transform the heap, or fail *}
@@ -19,6 +19,13 @@
 primrec execute :: "'a Heap \<Rightarrow> heap \<Rightarrow> ('a \<times> heap) option" where
   [code del]: "execute (Heap f) = f"
 
+lemma Heap_cases [case_names succeed fail]:
+  fixes f and h
+  assumes succeed: "\<And>x h'. execute f h = Some (x, h') \<Longrightarrow> P"
+  assumes fail: "execute f h = None \<Longrightarrow> P"
+  shows P
+  using assms by (cases "execute f h") auto
+
 lemma Heap_execute [simp]:
   "Heap (execute f) = f" by (cases f) simp_all
 
@@ -26,43 +33,98 @@
   "(\<And>h. execute f h = execute g h) \<Longrightarrow> f = g"
     by (cases f, cases g) (auto simp: expand_fun_eq)
 
-lemma Heap_eqI':
-  "(\<And>h. (\<lambda>x. execute (f x) h) = (\<lambda>y. execute (g y) h)) \<Longrightarrow> f = g"
-    by (auto simp: expand_fun_eq intro: Heap_eqI)
+ML {* structure Execute_Simps = Named_Thms(
+  val name = "execute_simps"
+  val description = "simplification rules for execute"
+) *}
+
+setup Execute_Simps.setup
+
+lemma execute_Let [simp, execute_simps]:
+  "execute (let x = t in f x) = (let x = t in execute (f x))"
+  by (simp add: Let_def)
+
+
+subsubsection {* Specialised lifters *}
+
+definition tap :: "(heap \<Rightarrow> 'a) \<Rightarrow> 'a Heap" where
+  [code del]: "tap f = Heap (\<lambda>h. Some (f h, h))"
+
+lemma execute_tap [simp, execute_simps]:
+  "execute (tap f) h = Some (f h, h)"
+  by (simp add: tap_def)
 
 definition heap :: "(heap \<Rightarrow> 'a \<times> heap) \<Rightarrow> 'a Heap" where
   [code del]: "heap f = Heap (Some \<circ> f)"
 
-lemma execute_heap [simp]:
+lemma execute_heap [simp, execute_simps]:
   "execute (heap f) = Some \<circ> f"
   by (simp add: heap_def)
 
 definition guard :: "(heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> 'a \<times> heap) \<Rightarrow> 'a Heap" where
   [code del]: "guard P f = Heap (\<lambda>h. if P h then Some (f h) else None)"
 
-lemma execute_guard [simp]:
+lemma execute_guard [execute_simps]:
   "\<not> P h \<Longrightarrow> execute (guard P f) h = None"
   "P h \<Longrightarrow> execute (guard P f) h = Some (f h)"
   by (simp_all add: guard_def)
 
-lemma heap_cases [case_names succeed fail]:
-  fixes f and h
-  assumes succeed: "\<And>x h'. execute f h = Some (x, h') \<Longrightarrow> P"
-  assumes fail: "execute f h = None \<Longrightarrow> P"
-  shows P
-  using assms by (cases "execute f h") auto
+
+subsubsection {* Predicate classifying successful computations *}
+
+definition success :: "'a Heap \<Rightarrow> heap \<Rightarrow> bool" where
+  "success f h \<longleftrightarrow> execute f h \<noteq> None"
+
+lemma successI:
+  "execute f h \<noteq> None \<Longrightarrow> success f h"
+  by (simp add: success_def)
+
+lemma successE:
+  assumes "success f h"
+  obtains r h' where "execute f h = Some (r, h')"
+  using assms by (auto simp add: success_def)
+
+ML {* structure Success_Intros = Named_Thms(
+  val name = "success_intros"
+  val description = "introduction rules for success"
+) *}
+
+setup Success_Intros.setup
+
+lemma success_tapI [iff, success_intros]:
+  "success (tap f) h"
+  by (rule successI) simp
+
+lemma success_heapI [iff, success_intros]:
+  "success (heap f) h"
+  by (rule successI) simp
+
+lemma success_guardI [success_intros]:
+  "P h \<Longrightarrow> success (guard P f) h"
+  by (rule successI) (simp add: execute_guard)
+
+lemma success_LetI [success_intros]:
+  "x = t \<Longrightarrow> success (f x) h \<Longrightarrow> success (let x = t in f x) h"
+  by (simp add: Let_def)
+
+
+subsubsection {* Monad combinators *}
 
 definition return :: "'a \<Rightarrow> 'a Heap" where
   [code del]: "return x = heap (Pair x)"
 
-lemma execute_return [simp]:
+lemma execute_return [simp, execute_simps]:
   "execute (return x) = Some \<circ> Pair x"
   by (simp add: return_def)
 
+lemma success_returnI [iff, success_intros]:
+  "success (return x) h"
+  by (rule successI) simp
+
 definition raise :: "string \<Rightarrow> 'a Heap" where -- {* the string is just decoration *}
   [code del]: "raise s = Heap (\<lambda>_. None)"
 
-lemma execute_raise [simp]:
+lemma execute_raise [simp, execute_simps]:
   "execute (raise s) = (\<lambda>_. None)"
   by (simp add: raise_def)
 
@@ -73,14 +135,18 @@
 
 notation bind (infixl "\<guillemotright>=" 54)
 
-lemma execute_bind [simp]:
+lemma execute_bind [execute_simps]:
   "execute f h = Some (x, h') \<Longrightarrow> execute (f \<guillemotright>= g) h = execute (g x) h'"
   "execute f h = None \<Longrightarrow> execute (f \<guillemotright>= g) h = None"
   by (simp_all add: bind_def)
 
-lemma execute_bind_heap [simp]:
-  "execute (heap f \<guillemotright>= g) h = execute (g (fst (f h))) (snd (f h))"
-  by (simp add: bind_def split_def)
+lemma success_bindI [success_intros]:
+  "success f h \<Longrightarrow> success (g (fst (the (execute f h)))) (snd (the (execute f h))) \<Longrightarrow> success (f \<guillemotright>= g) h"
+  by (auto intro!: successI elim!: successE simp add: bind_def)
+
+lemma execute_bind_successI [execute_simps]:
+  "success f h \<Longrightarrow> execute (f \<guillemotright>= g) h = execute (g (fst (the (execute f h)))) (snd (the (execute f h)))"
+  by (cases f h rule: Heap_cases) (auto elim!: successE simp add: bind_def)
   
 lemma execute_eq_SomeI:
   assumes "Heap_Monad.execute f h = Some (x, h')"
@@ -89,7 +155,7 @@
   using assms by (simp add: bind_def)
 
 lemma return_bind [simp]: "return x \<guillemotright>= f = f x"
-  by (rule Heap_eqI) simp
+  by (rule Heap_eqI) (simp add: execute_bind)
 
 lemma bind_return [simp]: "f \<guillemotright>= return = f"
   by (rule Heap_eqI) (simp add: bind_def split: option.splits)
@@ -98,7 +164,7 @@
   by (rule Heap_eqI) (simp add: bind_def split: option.splits)
 
 lemma raise_bind [simp]: "raise e \<guillemotright>= f = raise e"
-  by (rule Heap_eqI) simp
+  by (rule Heap_eqI) (simp add: execute_bind)
 
 abbreviation chain :: "'a Heap \<Rightarrow> 'b Heap \<Rightarrow> 'b Heap"  (infixl ">>" 54) where
   "f >> g \<equiv> f >>= (\<lambda>_. g)"
@@ -187,24 +253,31 @@
 *}
 
 
-subsection {* Monad properties *}
+subsection {* Generic combinators *}
 
-subsection {* Generic combinators *}
+subsubsection {* Assertions *}
 
 definition assert :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a Heap" where
   "assert P x = (if P x then return x else raise ''assert'')"
 
-lemma execute_assert [simp]:
+lemma execute_assert [execute_simps]:
   "P x \<Longrightarrow> execute (assert P x) h = Some (x, h)"
   "\<not> P x \<Longrightarrow> execute (assert P x) h = None"
   by (simp_all add: assert_def)
 
+lemma success_assertI [success_intros]:
+  "P x \<Longrightarrow> success (assert P x) h"
+  by (rule successI) (simp add: execute_assert)
+
 lemma assert_cong [fundef_cong]:
   assumes "P = P'"
   assumes "\<And>x. P' x \<Longrightarrow> f x = f' x"
   shows "(assert P x >>= f) = (assert P' x >>= f')"
   by (rule Heap_eqI) (insert assms, simp add: assert_def)
 
+
+subsubsection {* Plain lifting *}
+
 definition lift :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b Heap" where
   "lift f = return o f"
 
@@ -216,6 +289,9 @@
   "(f \<guillemotright>= lift g) = (f \<guillemotright>= (\<lambda>x. return (g x)))"
   by (simp add: lift_def comp_def)
 
+
+subsubsection {* Iteration -- warning: this is rarely useful! *}
+
 primrec fold_map :: "('a \<Rightarrow> 'b Heap) \<Rightarrow> 'a list \<Rightarrow> 'b list Heap" where
   "fold_map f [] = return []"
 | "fold_map f (x # xs) = do
@@ -228,7 +304,7 @@
   "fold_map f (xs @ ys) = fold_map f xs \<guillemotright>= (\<lambda>xs. fold_map f ys \<guillemotright>= (\<lambda>ys. return (xs @ ys)))"
   by (induct xs) simp_all
 
-lemma execute_fold_map_unchanged_heap:
+lemma execute_fold_map_unchanged_heap [execute_simps]:
   assumes "\<And>x. x \<in> set xs \<Longrightarrow> \<exists>y. execute (f x) h = Some (y, h)"
   shows "execute (fold_map f xs) h =
     Some (List.map (\<lambda>x. fst (the (execute (f x) h))) xs, h)"
@@ -527,6 +603,6 @@
 code_const return (Haskell "return")
 code_const Heap_Monad.raise' (Haskell "error/ _")
 
-hide_const (open) Heap heap guard execute raise' fold_map
+hide_const (open) Heap heap guard raise' fold_map
 
 end
diff -r dc78d2d9e90a -r 00ff97087ab5 src/HOL/Imperative_HOL/Ref.thy
--- a/src/HOL/Imperative_HOL/Ref.thy	Fri Jul 09 16:32:25 2010 +0200
+++ b/src/HOL/Imperative_HOL/Ref.thy	Fri Jul 09 17:00:42 2010 +0200
@@ -42,7 +42,7 @@
   [code del]: "ref v = Heap_Monad.heap (alloc v)"
 
 definition lookup :: "'a\<Colon>heap ref \<Rightarrow> 'a Heap" ("!_" 61) where
-  [code del]: "lookup r = Heap_Monad.heap (\<lambda>h. (get h r, h))"
+  [code del]: "lookup r = Heap_Monad.tap (\<lambda>h. get h r)"
 
 definition update :: "'a ref \<Rightarrow> 'a\<Colon>heap \<Rightarrow> unit Heap" ("_ := _" 62) where
   [code del]: "update r v = Heap_Monad.heap (\<lambda>h. ((), set r v h))"
@@ -58,6 +58,8 @@
 
 subsection {* Properties *}
 
+text {* Primitives *}
+
 lemma noteq_sym: "r =!= s \<Longrightarrow> s =!= r"
   and unequal [simp]: "r \<noteq> r' \<longleftrightarrow> r =!= r'" -- "same types!"
   by (auto simp add: noteq_def)
@@ -126,26 +128,44 @@
   "present h r \<Longrightarrow> \<not> present h r' \<Longrightarrow> r =!= r'"
   by (auto simp add: noteq_def present_def)
 
-lemma execute_ref [simp]:
-  "Heap_Monad.execute (ref v) h = Some (alloc v h)"
+
+text {* Monad operations *}
+
+lemma execute_ref [simp, execute_simps]:
+  "execute (ref v) h = Some (alloc v h)"
   by (simp add: ref_def)
 
-lemma execute_lookup [simp]:
+lemma success_refI [iff, success_intros]:
+  "success (ref v) h"
+  by (auto simp add: ref_def)
+
+lemma execute_lookup [simp, execute_simps]:
   "Heap_Monad.execute (lookup r) h = Some (get h r, h)"
   by (simp add: lookup_def)
 
-lemma execute_update [simp]:
+lemma success_lookupI [iff, success_intros]:
+  "success (lookup r) h"
+  by (auto simp add: lookup_def)
+
+lemma execute_update [simp, execute_simps]:
   "Heap_Monad.execute (update r v) h = Some ((), set r v h)"
   by (simp add: update_def)
 
-lemma execute_change [simp]:
+lemma success_updateI [iff, success_intros]:
+  "success (update r v) h"
+  by (auto simp add: update_def)
+
+lemma execute_change [simp, execute_simps]:
   "Heap_Monad.execute (change f r) h = Some (f (get h r), set r (f (get h r)) h)"
-  by (cases "!r" h rule: heap_cases)
-    (simp_all only: change_def execute_bind, auto simp add: Let_def)
+  by (simp add: change_def bind_def Let_def)
+
+lemma success_changeI [iff, success_intros]:
+  "success (change f r) h"
+  by (auto intro!: success_intros simp add: change_def)
 
 lemma lookup_chain:
   "(!r \<guillemotright> f) = f"
-  by (rule Heap_eqI) (simp add: lookup_def)
+  by (rule Heap_eqI) (auto simp add: lookup_def execute_simps)
 
 lemma update_change [code]:
   "r := e = change (\<lambda>_. e) r \<guillemotright> return ()"
@@ -233,4 +253,4 @@
 code_const Ref.lookup (Haskell "Heap.readSTRef")
 code_const Ref.update (Haskell "Heap.writeSTRef")
 
-end
\ No newline at end of file
+end
diff -r dc78d2d9e90a -r 00ff97087ab5 src/HOL/Imperative_HOL/Relational.thy
--- a/src/HOL/Imperative_HOL/Relational.thy	Fri Jul 09 16:32:25 2010 +0200
+++ b/src/HOL/Imperative_HOL/Relational.thy	Fri Jul 09 17:00:42 2010 +0200
@@ -23,6 +23,11 @@
 text {* For all commands, we define simple elimination rules. *}
 (* FIXME: consumes 1 necessary ?? *)
 
+lemma crel_tap:
+  assumes "crel (Heap_Monad.tap f) h h' r"
+  obtains "h' = h" "r = f h"
+  using assms by (simp add: crel_def)
+
 lemma crel_heap:
   assumes "crel (Heap_Monad.heap f) h h' r"
   obtains "h' = snd (f h)" "r = fst (f h)"
@@ -31,7 +36,7 @@
 lemma crel_guard:
   assumes "crel (Heap_Monad.guard P f) h h' r"
   obtains "h' = snd (f h)" "r = fst (f h)" "P h"
-  using assms by (cases "f h", cases "P h") (simp_all add: crel_def)
+  using assms by (cases "f h", cases "P h") (simp_all add: crel_def execute_simps)
 
 
 subsection {* Elimination rules for basic monadic commands *}
@@ -121,7 +126,7 @@
   assumes "crel (len a) h h' r"
   obtains "h = h'" "r = Array.length a h'"
   using assms unfolding Array.len_def
-  by (elim crel_heap) simp
+  by (elim crel_tap) simp
 
 lemma crel_nth[consumes 1]:
   assumes "crel (nth a i) h h' r"
@@ -184,7 +189,7 @@
   assumes "crel (Array.freeze a) h h' xs"
   obtains "h = h'" "xs = get_array a h"
   using assms unfolding freeze_def
-  by (elim crel_heap) simp
+  by (elim crel_tap) simp
 
 lemma crel_fold_map_map_entry_remains:
   assumes "crel (Heap_Monad.fold_map (\<lambda>n. map_entry n f a) [Array.length a h - n..<Array.length a h]) h h' r"
@@ -314,23 +319,20 @@
 lemma crel_lookup:
   assumes "crel (!r') h h' r"
   obtains "h = h'" "r = Ref.get h r'"
-using assms
-unfolding Ref.lookup_def
-by (auto elim: crel_heap)
+  using assms unfolding Ref.lookup_def
+  by (auto elim: crel_tap)
 
 lemma crel_update:
   assumes "crel (r' := v) h h' r"
   obtains "h' = Ref.set r' v h" "r = ()"
-using assms
-unfolding Ref.update_def
-by (auto elim: crel_heap)
+  using assms unfolding Ref.update_def
+  by (auto elim: crel_heap)
 
 lemma crel_change:
   assumes "crel (Ref.change f r') h h' r"
   obtains "h' = Ref.set r' (f (Ref.get h r')) h" "r = f (Ref.get h r')"
-using assms
-unfolding Ref.change_def Let_def
-by (auto elim!: crelE crel_lookup crel_update crel_return)
+  using assms unfolding Ref.change_def Let_def
+  by (auto elim!: crelE crel_lookup crel_update crel_return)
 
 subsection {* Elimination rules for the assert command *}
 
@@ -388,6 +390,11 @@
 using assms
 by (auto split: option.split)
 
+lemma crel_tapI:
+  assumes "h' = h" "r = f h"
+  shows "crel (Heap_Monad.tap f) h h' r"
+  using assms by (simp add: crel_def)
+
 lemma crel_heapI:
   shows "crel (Heap_Monad.heap f) h (snd (f h)) (fst (f h))"
   by (simp add: crel_def apfst_def split_def prod_fun_def)
@@ -401,7 +408,7 @@
 lemma crel_guardI:
   assumes "P h" "h' = snd (f h)" "r = fst (f h)"
   shows "crel (Heap_Monad.guard P f) h h' r"
-  using assms by (simp add: crel_def)
+  using assms by (simp add: crel_def execute_simps)
 
 lemma crelI2:
   assumes "\<exists>h' rs'. crel f h h' rs' \<and> (\<exists>h'' rs. crel (g rs') h' h'' rs)"
@@ -418,8 +425,7 @@
 
 lemma crel_lengthI:
   shows "crel (Array.len a) h h (Array.length a h)"
-  unfolding len_def
-  by (rule crel_heapI') auto
+  unfolding len_def by (rule crel_tapI) simp_all
 
 (* thm crel_newI for Array.new is missing *)
 
@@ -449,7 +455,7 @@
 
 lemma crel_lookupI:
   shows "crel (!r) h h (Ref.get h r)"
-  unfolding lookup_def by (auto intro!: crel_heapI')
+  unfolding lookup_def by (auto intro!: crel_tapI)
 
 lemma crel_updateI:
   shows "crel (r := v) h (Ref.set r v h) ()"
@@ -457,7 +463,7 @@
 
 lemma crel_changeI: 
   shows "crel (Ref.change f r) h (Ref.set r (f (Ref.get h r)) h) (f (Ref.get h r))"
-unfolding change_def Let_def by (auto intro!: crelI crel_returnI crel_lookupI crel_updateI)
+  unfolding change_def Let_def by (auto intro!: crelI crel_returnI crel_lookupI crel_updateI)
 
 subsubsection {* Introduction rules for the assert command *}
 
@@ -487,173 +493,26 @@
 next
 qed (auto simp add: assms(2)[unfolded crel_def])
 
-section {* Definition of the noError predicate *}
 
-text {* We add a simple definitional setting for crel intro rules
-  where we only would like to show that the computation does not result in a exception for heap h,
-  but we do not care about statements about the resulting heap and return value.*}
-
-definition noError :: "'a Heap \<Rightarrow> heap \<Rightarrow> bool"
-where
-  "noError c h \<longleftrightarrow> (\<exists>r h'. Some (r, h') = Heap_Monad.execute c h)"
-
-lemma noError_def': -- FIXME
-  "noError c h \<longleftrightarrow> (\<exists>r h'. Heap_Monad.execute c h = Some (r, h'))"
-  unfolding noError_def apply auto proof -
-  fix r h'
-  assume "Some (r, h') = Heap_Monad.execute c h"
-  then have "Heap_Monad.execute c h = Some (r, h')" ..
-  then show "\<exists>r h'. Heap_Monad.execute c h = Some (r, h')" by blast
-qed
-
-subsection {* Introduction rules for basic monadic commands *}
-
-lemma noErrorI:
-  assumes "noError f h"
-  assumes "\<And>h' r. crel f h h' r \<Longrightarrow> noError (g r) h'"
-  shows "noError (f \<guillemotright>= g) h"
-  using assms
-  by (auto simp add: noError_def' crel_def' bind_def)
-
-lemma noErrorI':
-  assumes "noError f h"
-  assumes "\<And>h' r. crel f h h' r \<Longrightarrow> noError g h'"
-  shows "noError (f \<guillemotright> g) h"
-  using assms
-  by (auto simp add: noError_def' crel_def' bind_def)
-
-lemma noErrorI2:
-"\<lbrakk>crel f h h' r ; noError f h; noError (g r) h'\<rbrakk>
-\<Longrightarrow> noError (f \<guillemotright>= g) h"
-by (auto simp add: noError_def' crel_def' bind_def)
-
-lemma noError_return: 
-  shows "noError (return x) h"
-  unfolding noError_def return_def
-  by auto
-
-lemma noError_if:
-  assumes "c \<Longrightarrow> noError t h" "\<not> c \<Longrightarrow> noError e h"
-  shows "noError (if c then t else e) h"
-  using assms
-  unfolding noError_def
-  by auto
-
-lemma noError_option_case:
-  assumes "\<And>y. x = Some y \<Longrightarrow> noError (s y) h"
-  assumes "noError n h"
-  shows "noError (case x of None \<Rightarrow> n | Some y \<Rightarrow> s y) h"
-using assms
-by (auto split: option.split)
-
-lemma noError_fold_map: 
-assumes "\<forall>x \<in> set xs. noError (f x) h \<and> crel (f x) h h (r x)" 
-shows "noError (Heap_Monad.fold_map f xs) h"
-using assms
-proof (induct xs)
-  case Nil
-  thus ?case
-    unfolding fold_map.simps by (intro noError_return)
-next
-  case (Cons x xs)
-  thus ?case
-    unfolding fold_map.simps
-    by (auto intro: noErrorI2[of "f x"] noErrorI noError_return)
-qed
-
-lemma noError_heap [simp]:
-  "noError (Heap_Monad.heap f) h"
-  by (simp add: noError_def')
-
-lemma noError_guard [simp]:
-  "P h \<Longrightarrow> noError (Heap_Monad.guard P f) h"
-  by (simp add: noError_def')
-
-subsection {* Introduction rules for array commands *}
-
-lemma noError_length:
-  shows "noError (Array.len a) h"
-  by (simp add: len_def)
-
-lemma noError_new:
-  shows "noError (Array.new n v) h"
-  by (simp add: Array.new_def)
-
-lemma noError_upd:
-  assumes "i < Array.length a h"
-  shows "noError (Array.upd i v a) h"
-  using assms by (simp add: upd_def)
-
-lemma noError_nth:
-  assumes "i < Array.length a h"
-  shows "noError (Array.nth a i) h"
-  using assms by (simp add: nth_def)
-
-lemma noError_of_list:
-  "noError (of_list ls) h"
-  by (simp add: of_list_def)
-
-lemma noError_map_entry:
-  assumes "i < Array.length a h"
-  shows "noError (map_entry i f a) h"
-  using assms by (simp add: map_entry_def)
-
-lemma noError_swap:
-  assumes "i < Array.length a h"
-  shows "noError (swap i x a) h"
-  using assms by (simp add: swap_def)
-
-lemma noError_make:
-  "noError (make n f) h"
-  by (simp add: make_def)
-
-lemma noError_freeze:
-  "noError (freeze a) h"
-  by (simp add: freeze_def)
-
-lemma noError_fold_map_map_entry:
+lemma success_fold_map_map_entry:
   assumes "n \<le> Array.length a h"
-  shows "noError (Heap_Monad.fold_map (\<lambda>n. map_entry n f a) [Array.length a h - n..<Array.length a h]) h"
+  shows "success (Heap_Monad.fold_map (\<lambda>n. map_entry n f a) [Array.length a h - n..<Array.length a h]) h"
 using assms
 proof (induct n arbitrary: h)
   case 0
-  thus ?case by (auto intro: noError_return)
+  thus ?case by (auto intro: success_returnI)
 next
   case (Suc n)
-  from Suc.prems have "[Array.length a h - Suc n..<Array.length a h] = (Array.length a h - Suc n)#[Array.length a h - n..<Array.length a h]"
+  from Suc.prems have "[Array.length a h - Suc n..<Array.length a h] =
+    (Array.length a h - Suc n) # [Array.length a h - n..<Array.length a h]"
     by (simp add: upt_conv_Cons')
-  with Suc.hyps[of "(Array.change a (Array.length a h - Suc n) (f (get_array a h ! (Array.length a h - Suc n))) h)"] Suc.prems show ?case
-    by (auto simp add: intro!: noErrorI noError_return noError_map_entry elim: crel_map_entry)
+  with Suc.hyps [of "(Array.change a (Array.length a h - Suc n) (f (get_array a h ! (Array.length a h - Suc n))) h)"] Suc.prems show ?case apply -
+    apply (auto simp add: execute_simps intro!: successI success_returnI success_map_entryI elim: crel_map_entry)
+    apply (subst execute_bind) apply (auto simp add: execute_simps)
+    done
 qed
 
 
-subsection {* Introduction rules for the reference commands *}
-
-lemma noError_Ref_new:
-  shows "noError (ref v) h"
-  by (simp add: Ref.ref_def)
-
-lemma noError_lookup:
-  shows "noError (!r) h"
-  by (simp add: lookup_def)
-
-lemma noError_update:
-  shows "noError (r := v) h"
-  by (simp add: update_def)
-
-lemma noError_change:
-  shows "noError (Ref.change f r) h"
-  by (simp add: change_def)
-    (auto intro!: noErrorI2 noError_lookup noError_update noError_return crel_lookupI crel_updateI simp add: Let_def)
-
-subsection {* Introduction rules for the assert command *}
-
-lemma noError_assert:
-  assumes "P x"
-  shows "noError (assert P x) h"
-  using assms unfolding assert_def
-  by (auto intro: noError_if noError_return)
-
 section {* Cumulative lemmas *}
 
 lemmas crel_elim_all =
@@ -668,10 +527,5 @@
   (* crel_Ref_newI *) crel_lookupI crel_updateI crel_changeI
   crel_assert
 
-lemmas noError_intro_all = 
-  noErrorI noErrorI' noError_return noError_if noError_option_case
-  noError_length noError_new noError_nth noError_upd noError_of_list noError_map_entry noError_swap noError_make noError_freeze
-  noError_Ref_new noError_lookup noError_update noError_change
-  noError_assert
 
 end
\ No newline at end of file
diff -r dc78d2d9e90a -r 00ff97087ab5 src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy
--- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Fri Jul 09 16:32:25 2010 +0200
+++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Fri Jul 09 17:00:42 2010 +0200
@@ -575,23 +575,35 @@
 text {* We have proved that quicksort sorts (if no exceptions occur).
 We will now show that exceptions do not occur. *}
 
-lemma noError_part1: 
+lemma success_part1I: 
   assumes "l < Array.length a h" "r < Array.length a h"
-  shows "noError (part1 a l r p) h"
+  shows "success (part1 a l r p) h"
   using assms
 proof (induct a l r p arbitrary: h rule: part1.induct)
   case (1 a l r p)
   thus ?case
     unfolding part1.simps [of a l r] swap_def
-    by (auto intro!: noError_if noErrorI noError_return noError_nth noError_upd elim!: crelE crel_upd crel_nth crel_return)
+    by (auto simp add: execute_simps intro!: success_intros elim!: crelE crel_upd crel_nth crel_return)
 qed
 
-lemma noError_partition:
+lemma success_ifI: (*FIXME move*)
+  assumes "c \<Longrightarrow> success t h" "\<not> c \<Longrightarrow> success e h"
+  shows "success (if c then t else e) h"
+  using assms
+  unfolding success_def
+  by auto
+
+lemma success_bindI' [success_intros]: (*FIXME move*)
+  assumes "success f h"
+  assumes "\<And>h' r. crel f h h' r \<Longrightarrow> success (g r) h'"
+  shows "success (f \<guillemotright>= g) h"
+  using assms by (auto intro!: successI elim!: successE simp add: bind_def crel_def success_def) blast
+
+lemma success_partitionI:
   assumes "l < r" "l < Array.length a h" "r < Array.length a h"
-  shows "noError (partition a l r) h"
-using assms
-unfolding partition.simps swap_def
-apply (auto intro!: noError_if noErrorI noError_return noError_nth noError_upd noError_part1 elim!: crelE crel_upd crel_nth crel_return)
+  shows "success (partition a l r) h"
+using assms unfolding partition.simps swap_def
+apply (auto intro!: success_bindI' success_ifI success_returnI success_nthI success_updI success_part1I elim!: crelE crel_upd crel_nth crel_return simp add:)
 apply (frule part_length_remains)
 apply (frule part_returns_index_in_bounds)
 apply auto
@@ -602,15 +614,15 @@
 apply auto
 done
 
-lemma noError_quicksort:
+lemma success_quicksortI:
   assumes "l < Array.length a h" "r < Array.length a h"
-  shows "noError (quicksort a l r) h"
+  shows "success (quicksort a l r) h"
 using assms
 proof (induct a l r arbitrary: h rule: quicksort.induct)
   case (1 a l ri h)
   thus ?case
     unfolding quicksort.simps [of a l ri]
-    apply (auto intro!: noError_if noErrorI noError_return noError_nth noError_upd noError_assert noError_partition)
+    apply (auto intro!: success_ifI success_bindI' success_returnI success_nthI success_updI success_assertI success_partitionI)
     apply (frule partition_returns_index_in_bounds)
     apply auto
     apply (frule partition_returns_index_in_bounds)
@@ -620,7 +632,7 @@
     apply (erule disjE)
     apply auto
     unfolding quicksort.simps [of a "Suc ri" ri]
-    apply (auto intro!: noError_if noError_return)
+    apply (auto intro!: success_ifI success_returnI)
     done
 qed