tuned Heap_Monad.successE

--- a/src/HOL/Imperative_HOL/Array.thy	Thu Oct 02 12:02:29 2014 +0200
+++ b/src/HOL/Imperative_HOL/Array.thy	Thu Oct 02 11:33:04 2014 +0200
@@ -255,8 +255,7 @@
 lemma effect_nthE [effect_elims]:
   assumes "effect (nth a i) h h' r"
   obtains "i < length h a" "r = get h a ! i" "h' = h"
-  using assms by (rule effectE)
-    (erule successE, cases "i < length h a", simp_all add: execute_simps)
+  using assms by (rule effectE) (cases "i < length h a", auto simp: execute_simps elim: successE)
 
 lemma execute_upd [execute_simps]:
   "i < length h a \<Longrightarrow>
@@ -276,8 +275,7 @@
 lemma effect_updE [effect_elims]:
   assumes "effect (upd i v a) h h' r"
   obtains "r = a" "h' = update a i v h" "i < length h a"
-  using assms by (rule effectE)
-    (erule successE, cases "i < length h a", simp_all add: execute_simps)
+  using assms by (rule effectE) (cases "i < length h a", auto simp: execute_simps elim: successE)
 
 lemma execute_map_entry [execute_simps]:
   "i < length h a \<Longrightarrow>
@@ -298,8 +296,7 @@
 lemma effect_map_entryE [effect_elims]:
   assumes "effect (map_entry i f a) h h' r"
   obtains "r = a" "h' = update a i (f (get h a ! i)) h" "i < length h a"
-  using assms by (rule effectE)
-    (erule successE, cases "i < length h a", simp_all add: execute_simps)
+  using assms by (rule effectE) (cases "i < length h a", auto simp: execute_simps elim: successE)
 
 lemma execute_swap [execute_simps]:
   "i < length h a \<Longrightarrow>
@@ -320,8 +317,7 @@
 lemma effect_swapE [effect_elims]:
   assumes "effect (swap i x a) h h' r"
   obtains "r = get h a ! i" "h' = update a i x h" "i < length h a"
-  using assms by (rule effectE)
-    (erule successE, cases "i < length h a", simp_all add: execute_simps)
+  using assms by (rule effectE) (cases "i < length h a", auto simp: execute_simps elim: successE)
 
 lemma execute_freeze [execute_simps]:
   "execute (freeze a) h = Some (get h a, h)"

--- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Thu Oct 02 12:02:29 2014 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Thu Oct 02 11:33:04 2014 +0200
@@ -82,10 +82,8 @@
 
 lemma successE:
   assumes "success f h"
-  obtains r h' where "r = fst (the (execute c h))"
-    and "h' = snd (the (execute c h))"
-    and "execute f h \<noteq> None"
-  using assms by (simp add: success_def)
+  obtains r h' where "execute f h = Some (r, h')"
+  using assms by (auto simp: success_def)
 
 named_theorems success_intros "introduction rules for success"
 
@@ -266,11 +264,11 @@
 
 lemma execute_bind_success:
   "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)
+  by (cases f h rule: Heap_cases) (auto elim: successE simp add: bind_def)
 
 lemma success_bind_executeI:
   "execute f h = Some (x, h') \<Longrightarrow> success (g x) h' \<Longrightarrow> success (f \<guillemotright>= g) h"
-  by (auto intro!: successI elim!: successE simp add: bind_def)
+  by (auto intro!: successI elim: successE simp add: bind_def)
 
 lemma success_bind_effectI [success_intros]:
   "effect f h h' x \<Longrightarrow> success (g x) h' \<Longrightarrow> success (f \<guillemotright>= g) h"