src/HOL/Imperative_HOL/Relational.thy

 text {* The crel predicate states that when a computation c runs with the heap h
   will result in return value r and a heap h' (if no exception occurs). *}  
 
 definition crel :: "'a Heap \<Rightarrow> heap \<Rightarrow> heap \<Rightarrow> 'a \<Rightarrow> bool"
 where
-  crel_def': "crel c h h' r \<longleftrightarrow> Heap_Monad.execute c h = (Inl r, h')"
+  crel_def': "crel c h h' r \<longleftrightarrow> Heap_Monad.execute c h = Some (r, h')"
 
 lemma crel_def: -- FIXME
-  "crel c h h' r \<longleftrightarrow> (Inl r, h') = Heap_Monad.execute c h"
+  "crel c h h' r \<longleftrightarrow> Some (r, h') = Heap_Monad.execute c h"
   unfolding crel_def' by auto
 
 lemma crel_deterministic: "\<lbrakk> crel f h h' a; crel f h h'' b \<rbrakk> \<Longrightarrow> (a = b) \<and> (h' = h'')"
 unfolding crel_def' by auto
 

 subsection {* Elimination rules for basic monadic commands *}
 
 lemma crelE[consumes 1]:
   assumes "crel (f >>= g) h h'' r'"
   obtains h' r where "crel f h h' r" "crel (g r) h' h'' r'"
-  using assms
-  by (auto simp add: crel_def bindM_def Let_def prod_case_beta split_def Pair_fst_snd_eq split add: sum.split_asm)
+  using assms by (auto simp add: crel_def bindM_def split: option.split_asm)
 
 lemma crelE'[consumes 1]:
   assumes "crel (f >> g) h h'' r'"
   obtains h' r where "crel f h h' r" "crel g h' h'' r'"
   using assms

 qed
 
 lemma crel_heap:
   assumes "crel (Heap_Monad.heap f) h h' r"
   obtains "h' = snd (f h)" "r = fst (f h)"
-  using assms
-  unfolding heap_def crel_def apfst_def split_def prod_fun_def by simp_all
+  using assms by (cases "f h") (simp add: crel_def)
+
 
 subsection {* Elimination rules for array commands *}
 
 lemma crel_length:
   assumes "crel (length a) h h' r"

 unfolding crel_def bindM_def Let_def assert_def
   raise_def return_def prod_case_beta
 apply (cases f)
 apply simp
 apply (simp add: expand_fun_eq split_def)
+apply (auto split: option.split)
+apply (erule_tac x="x" in meta_allE)
 apply auto
-apply (case_tac "fst (fun x)")
-apply (simp_all add: Pair_fst_snd_eq)
-apply (erule_tac x="x" in meta_allE)
-apply fastsimp
 done
 
 section {* Introduction rules *}
 
 subsection {* Introduction rules for basic monadic commands *}

   assumes "\<And> x h h1 h2 h' s z r. crel (f x) h h1 (Inr s) \<Longrightarrow> crel (MREC f g s) h1 h2 z \<Longrightarrow> P s h1 h2 z
     \<Longrightarrow> crel (g x s z) h2 h' r \<Longrightarrow> P x h h' r"
   shows "P x h h' r"
 proof (rule MREC_pinduct[OF assms(1)[unfolded crel_def, symmetric]])
   fix x h h1 h2 h' s z r
-  assume "Heap_Monad.execute (f x) h = (Inl (Inr s), h1)"
-    "Heap_Monad.execute (MREC f g s) h1 = (Inl z, h2)"
+  assume "Heap_Monad.execute (f x) h = Some (Inr s, h1)"
+    "Heap_Monad.execute (MREC f g s) h1 = Some (z, h2)"
     "P s h1 h2 z"
-    "Heap_Monad.execute (g x s z) h2 = (Inl r, h')"
+    "Heap_Monad.execute (g x s z) h2 = Some (r, h')"
   from assms(3)[unfolded crel_def, OF this(1)[symmetric] this(2)[symmetric] this(3) this(4)[symmetric]]
   show "P x h h' r" .
 next
 qed (auto simp add: assms(2)[unfolded crel_def])
 

   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'. (Inl r, h') = Heap_Monad.execute c h)"
+  "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 = (Inl r, h'))"
+  "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 "(Inl r, h') = Heap_Monad.execute c h"
-  then have "Heap_Monad.execute c h = (Inl r, h')" ..
-  then show "\<exists>r h'. Heap_Monad.execute c h = (Inl r, h')" by blast
+  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:

   by (auto intro: noError_of_list)
 
 (*TODO: move to HeapMonad *)
 lemma mapM_append:
   "mapM f (xs @ ys) = mapM f xs \<guillemotright>= (\<lambda>xs. mapM f ys \<guillemotright>= (\<lambda>ys. return (xs @ ys)))"
-  by (induct xs) (simp_all add: monad_simp)
+  by (induct xs) simp_all
 
 lemma noError_freeze:
   shows "noError (freeze a) h"
 unfolding freeze_def
 by (auto intro!: noErrorI noError_length noError_mapM[of _ _ _ "\<lambda>x. get_array a h ! x"]