spelt out relational framework in a consistent way
authorhaftmann
Mon Jul 12 16:05:08 2010 +0200 (2010-07-12 ago)
changeset 377711bec64044b5e
parent 37770 cddb3106adb8
child 37772 026ed2fc15d4
spelt out relational framework in a consistent way
src/HOL/Imperative_HOL/Array.thy
src/HOL/Imperative_HOL/Heap_Monad.thy
src/HOL/Imperative_HOL/Imperative_HOL_ex.thy
src/HOL/Imperative_HOL/Ref.thy
src/HOL/Imperative_HOL/Relational.thy
src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy
src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy
src/HOL/Imperative_HOL/ex/Linked_Lists.thy
src/HOL/Imperative_HOL/ex/SatChecker.thy
     1.1 --- a/src/HOL/Imperative_HOL/Array.thy	Mon Jul 12 11:39:27 2010 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/Array.thy	Mon Jul 12 16:05:08 2010 +0200
     1.3 @@ -155,6 +155,14 @@
     1.4    "array_present a (change b i v h) = array_present a h"
     1.5    by (simp add: change_def array_present_def set_array_def get_array_def)
     1.6  
     1.7 +lemma array_present_array [simp]:
     1.8 +  "array_present (fst (array xs h)) (snd (array xs h))"
     1.9 +  by (simp add: array_present_def array_def set_array_def Let_def)
    1.10 +
    1.11 +lemma not_array_present_array [simp]:
    1.12 +  "\<not> array_present (fst (array xs h)) h"
    1.13 +  by (simp add: array_present_def array_def Let_def)
    1.14 +
    1.15  
    1.16  text {* Monad operations *}
    1.17  
    1.18 @@ -166,6 +174,17 @@
    1.19    "success (new n x) h"
    1.20    by (simp add: new_def)
    1.21  
    1.22 +lemma crel_newI [crel_intros]:
    1.23 +  assumes "(a, h') = array (replicate n x) h"
    1.24 +  shows "crel (new n x) h h' a"
    1.25 +  by (rule crelI) (simp add: assms)
    1.26 +
    1.27 +lemma crel_newE [crel_elims]:
    1.28 +  assumes "crel (new n x) h h' r"
    1.29 +  obtains "r = fst (array (replicate n x) h)" "h' = snd (array (replicate n x) h)" 
    1.30 +    "get_array r h' = replicate n x" "array_present r h'" "\<not> array_present r h"
    1.31 +  using assms by (rule crelE) (simp add: get_array_init_array_list)
    1.32 +
    1.33  lemma execute_of_list [simp, execute_simps]:
    1.34    "execute (of_list xs) h = Some (array xs h)"
    1.35    by (simp add: of_list_def)
    1.36 @@ -174,6 +193,17 @@
    1.37    "success (of_list xs) h"
    1.38    by (simp add: of_list_def)
    1.39  
    1.40 +lemma crel_of_listI [crel_intros]:
    1.41 +  assumes "(a, h') = array xs h"
    1.42 +  shows "crel (of_list xs) h h' a"
    1.43 +  by (rule crelI) (simp add: assms)
    1.44 +
    1.45 +lemma crel_of_listE [crel_elims]:
    1.46 +  assumes "crel (of_list xs) h h' r"
    1.47 +  obtains "r = fst (array xs h)" "h' = snd (array xs h)" 
    1.48 +    "get_array r h' = xs" "array_present r h'" "\<not> array_present r h"
    1.49 +  using assms by (rule crelE) (simp add: get_array_init_array_list)
    1.50 +
    1.51  lemma execute_make [simp, execute_simps]:
    1.52    "execute (make n f) h = Some (array (map f [0 ..< n]) h)"
    1.53    by (simp add: make_def)
    1.54 @@ -182,6 +212,17 @@
    1.55    "success (make n f) h"
    1.56    by (simp add: make_def)
    1.57  
    1.58 +lemma crel_makeI [crel_intros]:
    1.59 +  assumes "(a, h') = array (map f [0 ..< n]) h"
    1.60 +  shows "crel (make n f) h h' a"
    1.61 +  by (rule crelI) (simp add: assms)
    1.62 +
    1.63 +lemma crel_makeE [crel_elims]:
    1.64 +  assumes "crel (make n f) h h' r"
    1.65 +  obtains "r = fst (array (map f [0 ..< n]) h)" "h' = snd (array (map f [0 ..< n]) h)" 
    1.66 +    "get_array r h' = map f [0 ..< n]" "array_present r h'" "\<not> array_present r h"
    1.67 +  using assms by (rule crelE) (simp add: get_array_init_array_list)
    1.68 +
    1.69  lemma execute_len [simp, execute_simps]:
    1.70    "execute (len a) h = Some (length a h, h)"
    1.71    by (simp add: len_def)
    1.72 @@ -190,6 +231,16 @@
    1.73    "success (len a) h"
    1.74    by (simp add: len_def)
    1.75  
    1.76 +lemma crel_lengthI [crel_intros]:
    1.77 +  assumes "h' = h" "r = length a h"
    1.78 +  shows "crel (len a) h h' r"
    1.79 +  by (rule crelI) (simp add: assms)
    1.80 +
    1.81 +lemma crel_lengthE [crel_elims]:
    1.82 +  assumes "crel (len a) h h' r"
    1.83 +  obtains "r = length a h'" "h' = h" 
    1.84 +  using assms by (rule crelE) simp
    1.85 +
    1.86  lemma execute_nth [execute_simps]:
    1.87    "i < length a h \<Longrightarrow>
    1.88      execute (nth a i) h = Some (get_array a h ! i, h)"
    1.89 @@ -200,38 +251,82 @@
    1.90    "i < length a h \<Longrightarrow> success (nth a i) h"
    1.91    by (auto intro: success_intros simp add: nth_def)
    1.92  
    1.93 +lemma crel_nthI [crel_intros]:
    1.94 +  assumes "i < length a h" "h' = h" "r = get_array a h ! i"
    1.95 +  shows "crel (nth a i) h h' r"
    1.96 +  by (rule crelI) (insert assms, simp add: execute_simps)
    1.97 +
    1.98 +lemma crel_nthE [crel_elims]:
    1.99 +  assumes "crel (nth a i) h h' r"
   1.100 +  obtains "i < length a h" "r = get_array a h ! i" "h' = h"
   1.101 +  using assms by (rule crelE)
   1.102 +    (erule successE, cases "i < length a h", simp_all add: execute_simps)
   1.103 +
   1.104  lemma execute_upd [execute_simps]:
   1.105    "i < length a h \<Longrightarrow>
   1.106      execute (upd i x a) h = Some (a, change a i x h)"
   1.107 -  "i \<ge> length a h \<Longrightarrow> execute (nth a i) h = None"
   1.108 +  "i \<ge> length a h \<Longrightarrow> execute (upd i x a) h = None"
   1.109    by (simp_all add: upd_def execute_simps)
   1.110  
   1.111  lemma success_updI [success_intros]:
   1.112    "i < length a h \<Longrightarrow> success (upd i x a) h"
   1.113    by (auto intro: success_intros simp add: upd_def)
   1.114  
   1.115 +lemma crel_updI [crel_intros]:
   1.116 +  assumes "i < length a h" "h' = change a i v h"
   1.117 +  shows "crel (upd i v a) h h' a"
   1.118 +  by (rule crelI) (insert assms, simp add: execute_simps)
   1.119 +
   1.120 +lemma crel_updE [crel_elims]:
   1.121 +  assumes "crel (upd i v a) h h' r"
   1.122 +  obtains "r = a" "h' = change a i v h" "i < length a h"
   1.123 +  using assms by (rule crelE)
   1.124 +    (erule successE, cases "i < length a h", simp_all add: execute_simps)
   1.125 +
   1.126  lemma execute_map_entry [execute_simps]:
   1.127    "i < length a h \<Longrightarrow>
   1.128     execute (map_entry i f a) h =
   1.129        Some (a, change a i (f (get_array a h ! i)) h)"
   1.130 -  "i \<ge> length a h \<Longrightarrow> execute (nth a i) h = None"
   1.131 +  "i \<ge> length a h \<Longrightarrow> execute (map_entry i f a) h = None"
   1.132    by (simp_all add: map_entry_def execute_simps)
   1.133  
   1.134  lemma success_map_entryI [success_intros]:
   1.135    "i < length a h \<Longrightarrow> success (map_entry i f a) h"
   1.136    by (auto intro: success_intros simp add: map_entry_def)
   1.137  
   1.138 +lemma crel_map_entryI [crel_intros]:
   1.139 +  assumes "i < length a h" "h' = change a i (f (get_array a h ! i)) h" "r = a"
   1.140 +  shows "crel (map_entry i f a) h h' r"
   1.141 +  by (rule crelI) (insert assms, simp add: execute_simps)
   1.142 +
   1.143 +lemma crel_map_entryE [crel_elims]:
   1.144 +  assumes "crel (map_entry i f a) h h' r"
   1.145 +  obtains "r = a" "h' = change a i (f (get_array a h ! i)) h" "i < length a h"
   1.146 +  using assms by (rule crelE)
   1.147 +    (erule successE, cases "i < length a h", simp_all add: execute_simps)
   1.148 +
   1.149  lemma execute_swap [execute_simps]:
   1.150    "i < length a h \<Longrightarrow>
   1.151     execute (swap i x a) h =
   1.152        Some (get_array a h ! i, change a i x h)"
   1.153 -  "i \<ge> length a h \<Longrightarrow> execute (nth a i) h = None"
   1.154 +  "i \<ge> length a h \<Longrightarrow> execute (swap i x a) h = None"
   1.155    by (simp_all add: swap_def execute_simps)
   1.156  
   1.157  lemma success_swapI [success_intros]:
   1.158    "i < length a h \<Longrightarrow> success (swap i x a) h"
   1.159    by (auto intro: success_intros simp add: swap_def)
   1.160  
   1.161 +lemma crel_swapI [crel_intros]:
   1.162 +  assumes "i < length a h" "h' = change a i x h" "r = get_array a h ! i"
   1.163 +  shows "crel (swap i x a) h h' r"
   1.164 +  by (rule crelI) (insert assms, simp add: execute_simps)
   1.165 +
   1.166 +lemma crel_swapE [crel_elims]:
   1.167 +  assumes "crel (swap i x a) h h' r"
   1.168 +  obtains "r = get_array a h ! i" "h' = change a i x h" "i < length a h"
   1.169 +  using assms by (rule crelE)
   1.170 +    (erule successE, cases "i < length a h", simp_all add: execute_simps)
   1.171 +
   1.172  lemma execute_freeze [simp, execute_simps]:
   1.173    "execute (freeze a) h = Some (get_array a h, h)"
   1.174    by (simp add: freeze_def)
   1.175 @@ -240,6 +335,16 @@
   1.176    "success (freeze a) h"
   1.177    by (simp add: freeze_def)
   1.178  
   1.179 +lemma crel_freezeI [crel_intros]:
   1.180 +  assumes "h' = h" "r = get_array a h"
   1.181 +  shows "crel (freeze a) h h' r"
   1.182 +  by (rule crelI) (insert assms, simp add: execute_simps)
   1.183 +
   1.184 +lemma crel_freezeE [crel_elims]:
   1.185 +  assumes "crel (freeze a) h h' r"
   1.186 +  obtains "h' = h" "r = get_array a h"
   1.187 +  using assms by (rule crelE) simp
   1.188 +
   1.189  lemma upd_return:
   1.190    "upd i x a \<guillemotright> return a = upd i x a"
   1.191    by (rule Heap_eqI) (simp add: bind_def guard_def upd_def)
   1.192 @@ -252,7 +357,7 @@
   1.193    "of_list xs = make (List.length xs) (\<lambda>n. xs ! n)"
   1.194    by (rule Heap_eqI) (simp add: map_nth)
   1.195  
   1.196 -hide_const (open) new map
   1.197 +hide_const (open) new
   1.198  
   1.199  
   1.200  subsection {* Code generator setup *}
   1.201 @@ -339,7 +444,7 @@
   1.202        n \<leftarrow> len a;
   1.203        Heap_Monad.fold_map (Array.nth a) [0..<n]
   1.204      done) h = Some (get_array a h, h)"
   1.205 -    by (auto intro: execute_eq_SomeI)
   1.206 +    by (auto intro: execute_bind_eq_SomeI)
   1.207    then show "execute (freeze a) h = execute (do
   1.208        n \<leftarrow> len a;
   1.209        Heap_Monad.fold_map (Array.nth a) [0..<n]
     2.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Mon Jul 12 11:39:27 2010 +0200
     2.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Mon Jul 12 16:05:08 2010 +0200
     2.3 @@ -2,7 +2,7 @@
     2.4      Author:     John Matthews, Galois Connections; Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen
     2.5  *)
     2.6  
     2.7 -header {* A monad with a polymorphic heap *}
     2.8 +header {* A monad with a polymorphic heap and primitive reasoning infrastructure *}
     2.9  
    2.10  theory Heap_Monad
    2.11  imports Heap
    2.12 @@ -81,8 +81,10 @@
    2.13  
    2.14  lemma successE:
    2.15    assumes "success f h"
    2.16 -  obtains r h' where "execute f h = Some (r, h')"
    2.17 -  using assms by (auto simp add: success_def)
    2.18 +  obtains r h' where "r = fst (the (execute c h))"
    2.19 +    and "h' = snd (the (execute c h))"
    2.20 +    and "execute f h \<noteq> None"
    2.21 +  using assms by (simp add: success_def)
    2.22  
    2.23  ML {* structure Success_Intros = Named_Thms(
    2.24    val name = "success_intros"
    2.25 @@ -107,6 +109,121 @@
    2.26    "x = t \<Longrightarrow> success (f x) h \<Longrightarrow> success (let x = t in f x) h"
    2.27    by (simp add: Let_def)
    2.28  
    2.29 +lemma success_ifI:
    2.30 +  "(c \<Longrightarrow> success t h) \<Longrightarrow> (\<not> c \<Longrightarrow> success e h) \<Longrightarrow>
    2.31 +    success (if c then t else e) h"
    2.32 +  by (simp add: success_def)
    2.33 +
    2.34 +
    2.35 +subsubsection {* Predicate for a simple relational calculus *}
    2.36 +
    2.37 +text {*
    2.38 +  The @{text crel} predicate states that when a computation @{text c}
    2.39 +  runs with the heap @{text h} will result in return value @{text r}
    2.40 +  and a heap @{text "h'"}, i.e.~no exception occurs.
    2.41 +*}  
    2.42 +
    2.43 +definition crel :: "'a Heap \<Rightarrow> heap \<Rightarrow> heap \<Rightarrow> 'a \<Rightarrow> bool" where
    2.44 +  crel_def: "crel c h h' r \<longleftrightarrow> Heap_Monad.execute c h = Some (r, h')"
    2.45 +
    2.46 +lemma crelI:
    2.47 +  "Heap_Monad.execute c h = Some (r, h') \<Longrightarrow> crel c h h' r"
    2.48 +  by (simp add: crel_def)
    2.49 +
    2.50 +lemma crelE:
    2.51 +  assumes "crel c h h' r"
    2.52 +  obtains "r = fst (the (execute c h))"
    2.53 +    and "h' = snd (the (execute c h))"
    2.54 +    and "success c h"
    2.55 +proof (rule that)
    2.56 +  from assms have *: "execute c h = Some (r, h')" by (simp add: crel_def)
    2.57 +  then show "success c h" by (simp add: success_def)
    2.58 +  from * have "fst (the (execute c h)) = r" and "snd (the (execute c h)) = h'"
    2.59 +    by simp_all
    2.60 +  then show "r = fst (the (execute c h))"
    2.61 +    and "h' = snd (the (execute c h))" by simp_all
    2.62 +qed
    2.63 +
    2.64 +lemma crel_success:
    2.65 +  "crel c h h' r \<Longrightarrow> success c h"
    2.66 +  by (simp add: crel_def success_def)
    2.67 +
    2.68 +lemma success_crelE:
    2.69 +  assumes "success c h"
    2.70 +  obtains r h' where "crel c h h' r"
    2.71 +  using assms by (auto simp add: crel_def success_def)
    2.72 +
    2.73 +lemma crel_deterministic:
    2.74 +  assumes "crel f h h' a"
    2.75 +    and "crel f h h'' b"
    2.76 +  shows "a = b" and "h' = h''"
    2.77 +  using assms unfolding crel_def by auto
    2.78 +
    2.79 +ML {* structure Crel_Intros = Named_Thms(
    2.80 +  val name = "crel_intros"
    2.81 +  val description = "introduction rules for crel"
    2.82 +) *}
    2.83 +
    2.84 +ML {* structure Crel_Elims = Named_Thms(
    2.85 +  val name = "crel_elims"
    2.86 +  val description = "elimination rules for crel"
    2.87 +) *}
    2.88 +
    2.89 +setup "Crel_Intros.setup #> Crel_Elims.setup"
    2.90 +
    2.91 +lemma crel_LetI [crel_intros]:
    2.92 +  assumes "x = t" "crel (f x) h h' r"
    2.93 +  shows "crel (let x = t in f x) h h' r"
    2.94 +  using assms by simp
    2.95 +
    2.96 +lemma crel_LetE [crel_elims]:
    2.97 +  assumes "crel (let x = t in f x) h h' r"
    2.98 +  obtains "crel (f t) h h' r"
    2.99 +  using assms by simp
   2.100 +
   2.101 +lemma crel_ifI:
   2.102 +  assumes "c \<Longrightarrow> crel t h h' r"
   2.103 +    and "\<not> c \<Longrightarrow> crel e h h' r"
   2.104 +  shows "crel (if c then t else e) h h' r"
   2.105 +  by (cases c) (simp_all add: assms)
   2.106 +
   2.107 +lemma crel_ifE:
   2.108 +  assumes "crel (if c then t else e) h h' r"
   2.109 +  obtains "c" "crel t h h' r"
   2.110 +    | "\<not> c" "crel e h h' r"
   2.111 +  using assms by (cases c) simp_all
   2.112 +
   2.113 +lemma crel_tapI [crel_intros]:
   2.114 +  assumes "h' = h" "r = f h"
   2.115 +  shows "crel (tap f) h h' r"
   2.116 +  by (rule crelI) (simp add: assms)
   2.117 +
   2.118 +lemma crel_tapE [crel_elims]:
   2.119 +  assumes "crel (tap f) h h' r"
   2.120 +  obtains "h' = h" and "r = f h"
   2.121 +  using assms by (rule crelE) auto
   2.122 +
   2.123 +lemma crel_heapI [crel_intros]:
   2.124 +  assumes "h' = snd (f h)" "r = fst (f h)"
   2.125 +  shows "crel (heap f) h h' r"
   2.126 +  by (rule crelI) (simp add: assms)
   2.127 +
   2.128 +lemma crel_heapE [crel_elims]:
   2.129 +  assumes "crel (heap f) h h' r"
   2.130 +  obtains "h' = snd (f h)" and "r = fst (f h)"
   2.131 +  using assms by (rule crelE) simp
   2.132 +
   2.133 +lemma crel_guardI [crel_intros]:
   2.134 +  assumes "P h" "h' = snd (f h)" "r = fst (f h)"
   2.135 +  shows "crel (guard P f) h h' r"
   2.136 +  by (rule crelI) (simp add: assms execute_simps)
   2.137 +
   2.138 +lemma crel_guardE [crel_elims]:
   2.139 +  assumes "crel (guard P f) h h' r"
   2.140 +  obtains "h' = snd (f h)" "r = fst (f h)" "P h"
   2.141 +  using assms by (rule crelE)
   2.142 +    (auto simp add: execute_simps elim!: successE, cases "P h", auto simp add: execute_simps)
   2.143 +
   2.144  
   2.145  subsubsection {* Monad combinators *}
   2.146  
   2.147 @@ -121,6 +238,15 @@
   2.148    "success (return x) h"
   2.149    by (rule successI) simp
   2.150  
   2.151 +lemma crel_returnI [crel_intros]:
   2.152 +  "h = h' \<Longrightarrow> crel (return x) h h' x"
   2.153 +  by (rule crelI) simp
   2.154 +
   2.155 +lemma crel_returnE [crel_elims]:
   2.156 +  assumes "crel (return x) h h' r"
   2.157 +  obtains "r = x" "h' = h"
   2.158 +  using assms by (rule crelE) simp
   2.159 +
   2.160  definition raise :: "string \<Rightarrow> 'a Heap" where -- {* the string is just decoration *}
   2.161    [code del]: "raise s = Heap (\<lambda>_. None)"
   2.162  
   2.163 @@ -128,6 +254,11 @@
   2.164    "execute (raise s) = (\<lambda>_. None)"
   2.165    by (simp add: raise_def)
   2.166  
   2.167 +lemma crel_raiseE [crel_elims]:
   2.168 +  assumes "crel (raise x) h h' r"
   2.169 +  obtains "False"
   2.170 +  using assms by (rule crelE) (simp add: success_def)
   2.171 +
   2.172  definition bind :: "'a Heap \<Rightarrow> ('a \<Rightarrow> 'b Heap) \<Rightarrow> 'b Heap" (infixl ">>=" 54) where
   2.173    [code del]: "f >>= g = Heap (\<lambda>h. case execute f h of
   2.174                    Some (x, h') \<Rightarrow> execute (g x) h'
   2.175 @@ -140,15 +271,32 @@
   2.176    "execute f h = None \<Longrightarrow> execute (f \<guillemotright>= g) h = None"
   2.177    by (simp_all add: bind_def)
   2.178  
   2.179 -lemma success_bindI [success_intros]:
   2.180 -  "success f h \<Longrightarrow> success (g (fst (the (execute f h)))) (snd (the (execute f h))) \<Longrightarrow> success (f \<guillemotright>= g) h"
   2.181 +lemma execute_bind_success:
   2.182 +  "success f h \<Longrightarrow> execute (f \<guillemotright>= g) h = execute (g (fst (the (execute f h)))) (snd (the (execute f h)))"
   2.183 +  by (cases f h rule: Heap_cases) (auto elim!: successE simp add: bind_def)
   2.184 +
   2.185 +lemma success_bind_executeI:
   2.186 +  "execute f h = Some (x, h') \<Longrightarrow> success (g x) h' \<Longrightarrow> success (f \<guillemotright>= g) h"
   2.187    by (auto intro!: successI elim!: successE simp add: bind_def)
   2.188  
   2.189 -lemma execute_bind_successI [execute_simps]:
   2.190 -  "success f h \<Longrightarrow> execute (f \<guillemotright>= g) h = execute (g (fst (the (execute f h)))) (snd (the (execute f h)))"
   2.191 -  by (cases f h rule: Heap_cases) (auto elim!: successE simp add: bind_def)
   2.192 -  
   2.193 -lemma execute_eq_SomeI:
   2.194 +lemma success_bind_crelI [success_intros]:
   2.195 +  "crel f h h' x \<Longrightarrow> success (g x) h' \<Longrightarrow> success (f \<guillemotright>= g) h"
   2.196 +  by (auto simp add: crel_def success_def bind_def)
   2.197 +
   2.198 +lemma crel_bindI [crel_intros]:
   2.199 +  assumes "crel f h h' r" "crel (g r) h' h'' r'"
   2.200 +  shows "crel (f \<guillemotright>= g) h h'' r'"
   2.201 +  using assms
   2.202 +  apply (auto intro!: crelI elim!: crelE successE)
   2.203 +  apply (subst execute_bind, simp_all)
   2.204 +  done
   2.205 +
   2.206 +lemma crel_bindE [crel_elims]:
   2.207 +  assumes "crel (f \<guillemotright>= g) h h'' r'"
   2.208 +  obtains h' r where "crel f h h' r" "crel (g r) h' h'' r'"
   2.209 +  using assms by (auto simp add: crel_def bind_def split: option.split_asm)
   2.210 +
   2.211 +lemma execute_bind_eq_SomeI:
   2.212    assumes "Heap_Monad.execute f h = Some (x, h')"
   2.213      and "Heap_Monad.execute (g x) h' = Some (y, h'')"
   2.214    shows "Heap_Monad.execute (f \<guillemotright>= g) h = Some (y, h'')"
   2.215 @@ -269,6 +417,15 @@
   2.216    "P x \<Longrightarrow> success (assert P x) h"
   2.217    by (rule successI) (simp add: execute_assert)
   2.218  
   2.219 +lemma crel_assertI [crel_intros]:
   2.220 +  "P x \<Longrightarrow> h' = h \<Longrightarrow> r = x \<Longrightarrow> crel (assert P x) h h' r"
   2.221 +  by (rule crelI) (simp add: execute_assert)
   2.222 + 
   2.223 +lemma crel_assertE [crel_elims]:
   2.224 +  assumes "crel (assert P x) h h' r"
   2.225 +  obtains "P x" "r = x" "h' = h"
   2.226 +  using assms by (rule crelE) (cases "P x", simp_all add: execute_assert success_def)
   2.227 +
   2.228  lemma assert_cong [fundef_cong]:
   2.229    assumes "P = P'"
   2.230    assumes "\<And>x. P' x \<Longrightarrow> f x = f' x"
     3.1 --- a/src/HOL/Imperative_HOL/Imperative_HOL_ex.thy	Mon Jul 12 11:39:27 2010 +0200
     3.2 +++ b/src/HOL/Imperative_HOL/Imperative_HOL_ex.thy	Mon Jul 12 16:05:08 2010 +0200
     3.3 @@ -6,8 +6,8 @@
     3.4  header {* Monadic imperative HOL with examples *}
     3.5  
     3.6  theory Imperative_HOL_ex
     3.7 -imports Imperative_HOL "ex/Imperative_Quicksort" "ex/Imperative_Reverse" "ex/Linked_Lists"
     3.8 -  "ex/SatChecker"
     3.9 +imports Imperative_HOL
    3.10 +  "ex/Imperative_Quicksort" "ex/Imperative_Reverse" "ex/Linked_Lists" "ex/SatChecker"
    3.11  begin
    3.12  
    3.13  end
     4.1 --- a/src/HOL/Imperative_HOL/Ref.thy	Mon Jul 12 11:39:27 2010 +0200
     4.2 +++ b/src/HOL/Imperative_HOL/Ref.thy	Mon Jul 12 16:05:08 2010 +0200
     4.3 @@ -92,6 +92,10 @@
     4.4    "set r x (set r y h) = set r x h"
     4.5    by (simp add: set_def)
     4.6  
     4.7 +lemma not_present_alloc [simp]:
     4.8 +  "\<not> present h (fst (alloc v h))"
     4.9 +  by (simp add: present_def alloc_def Let_def)
    4.10 +
    4.11  lemma set_set_swap:
    4.12    "r =!= r' \<Longrightarrow> set r x (set r' x' h) = set r' x' (set r x h)"
    4.13    by (simp add: noteq_def set_def expand_fun_eq)
    4.14 @@ -139,6 +143,16 @@
    4.15    "success (ref v) h"
    4.16    by (auto simp add: ref_def)
    4.17  
    4.18 +lemma crel_refI [crel_intros]:
    4.19 +  assumes "(r, h') = alloc v h"
    4.20 +  shows "crel (ref v) h h' r"
    4.21 +  by (rule crelI) (insert assms, simp)
    4.22 +
    4.23 +lemma crel_refE [crel_elims]:
    4.24 +  assumes "crel (ref v) h h' r"
    4.25 +  obtains "Ref.get h' r = v" and "Ref.present h' r" and "\<not> Ref.present h r"
    4.26 +  using assms by (rule crelE) simp
    4.27 +
    4.28  lemma execute_lookup [simp, execute_simps]:
    4.29    "Heap_Monad.execute (lookup r) h = Some (get h r, h)"
    4.30    by (simp add: lookup_def)
    4.31 @@ -147,6 +161,16 @@
    4.32    "success (lookup r) h"
    4.33    by (auto simp add: lookup_def)
    4.34  
    4.35 +lemma crel_lookupI [crel_intros]:
    4.36 +  assumes "h' = h" "x = Ref.get h r"
    4.37 +  shows "crel (!r) h h' x"
    4.38 +  by (rule crelI) (insert assms, simp)
    4.39 +
    4.40 +lemma crel_lookupE [crel_elims]:
    4.41 +  assumes "crel (!r) h h' x"
    4.42 +  obtains "h' = h" "x = Ref.get h r"
    4.43 +  using assms by (rule crelE) simp
    4.44 +
    4.45  lemma execute_update [simp, execute_simps]:
    4.46    "Heap_Monad.execute (update r v) h = Some ((), set r v h)"
    4.47    by (simp add: update_def)
    4.48 @@ -155,17 +179,37 @@
    4.49    "success (update r v) h"
    4.50    by (auto simp add: update_def)
    4.51  
    4.52 +lemma crel_updateI [crel_intros]:
    4.53 +  assumes "h' = Ref.set r v h"
    4.54 +  shows "crel (r := v) h h' x"
    4.55 +  by (rule crelI) (insert assms, simp)
    4.56 +
    4.57 +lemma crel_updateE [crel_elims]:
    4.58 +  assumes "crel (r' := v) h h' r"
    4.59 +  obtains "h' = Ref.set r' v h"
    4.60 +  using assms by (rule crelE) simp
    4.61 +
    4.62  lemma execute_change [simp, execute_simps]:
    4.63    "Heap_Monad.execute (change f r) h = Some (f (get h r), set r (f (get h r)) h)"
    4.64    by (simp add: change_def bind_def Let_def)
    4.65  
    4.66  lemma success_changeI [iff, success_intros]:
    4.67    "success (change f r) h"
    4.68 -  by (auto intro!: success_intros simp add: change_def)
    4.69 +  by (auto intro!: success_intros crel_intros simp add: change_def)
    4.70 +
    4.71 +lemma crel_changeI [crel_intros]: 
    4.72 +  assumes "h' = Ref.set r (f (Ref.get h r)) h" "x = f (Ref.get h r)"
    4.73 +  shows "crel (Ref.change f r) h h' x"
    4.74 +  by (rule crelI) (insert assms, simp)  
    4.75 +
    4.76 +lemma crel_changeE [crel_elims]:
    4.77 +  assumes "crel (Ref.change f r') h h' r"
    4.78 +  obtains "h' = Ref.set r' (f (Ref.get h r')) h" "r = f (Ref.get h r')"
    4.79 +  using assms by (rule crelE) simp
    4.80  
    4.81  lemma lookup_chain:
    4.82    "(!r \<guillemotright> f) = f"
    4.83 -  by (rule Heap_eqI) (auto simp add: lookup_def execute_simps)
    4.84 +  by (rule Heap_eqI) (auto simp add: lookup_def execute_simps intro: execute_bind)
    4.85  
    4.86  lemma update_change [code]:
    4.87    "r := e = change (\<lambda>_. e) r \<guillemotright> return ()"
     5.1 --- a/src/HOL/Imperative_HOL/Relational.thy	Mon Jul 12 11:39:27 2010 +0200
     5.2 +++ b/src/HOL/Imperative_HOL/Relational.thy	Mon Jul 12 16:05:08 2010 +0200
     5.3 @@ -2,81 +2,38 @@
     5.4  imports Array Ref
     5.5  begin
     5.6  
     5.7 -section{* Definition of the Relational framework *}
     5.8 -
     5.9 -text {* The crel predicate states that when a computation c runs with the heap h
    5.10 -  will result in return value r and a heap h' (if no exception occurs). *}  
    5.11 -
    5.12 -definition crel :: "'a Heap \<Rightarrow> heap \<Rightarrow> heap \<Rightarrow> 'a \<Rightarrow> bool"
    5.13 -where
    5.14 -  crel_def': "crel c h h' r \<longleftrightarrow> Heap_Monad.execute c h = Some (r, h')"
    5.15 -
    5.16 -lemma crel_def: -- FIXME
    5.17 -  "crel c h h' r \<longleftrightarrow> Some (r, h') = Heap_Monad.execute c h"
    5.18 -  unfolding crel_def' by auto
    5.19 -
    5.20 -lemma crel_deterministic: "\<lbrakk> crel f h h' a; crel f h h'' b \<rbrakk> \<Longrightarrow> (a = b) \<and> (h' = h'')"
    5.21 -unfolding crel_def' by auto
    5.22 -
    5.23 -section {* Elimination rules *}
    5.24 -
    5.25 -text {* For all commands, we define simple elimination rules. *}
    5.26 -(* FIXME: consumes 1 necessary ?? *)
    5.27 -
    5.28 -lemma crel_tap:
    5.29 -  assumes "crel (Heap_Monad.tap f) h h' r"
    5.30 -  obtains "h' = h" "r = f h"
    5.31 -  using assms by (simp add: crel_def)
    5.32 -
    5.33 -lemma crel_heap:
    5.34 -  assumes "crel (Heap_Monad.heap f) h h' r"
    5.35 -  obtains "h' = snd (f h)" "r = fst (f h)"
    5.36 -  using assms by (cases "f h") (simp add: crel_def)
    5.37 +lemma crel_assert_eq: "(\<And>h h' r. crel f h h' r \<Longrightarrow> P r) \<Longrightarrow> f \<guillemotright>= assert P = f"
    5.38 +unfolding crel_def bind_def Let_def assert_def
    5.39 +  raise_def return_def prod_case_beta
    5.40 +apply (cases f)
    5.41 +apply simp
    5.42 +apply (simp add: expand_fun_eq split_def)
    5.43 +apply (auto split: option.split)
    5.44 +done
    5.45  
    5.46 -lemma crel_guard:
    5.47 -  assumes "crel (Heap_Monad.guard P f) h h' r"
    5.48 -  obtains "h' = snd (f h)" "r = fst (f h)" "P h"
    5.49 -  using assms by (cases "f h", cases "P h") (simp_all add: crel_def execute_simps)
    5.50 -
    5.51 -
    5.52 -subsection {* Elimination rules for basic monadic commands *}
    5.53 -
    5.54 -lemma crelE[consumes 1]:
    5.55 -  assumes "crel (f >>= g) h h'' r'"
    5.56 -  obtains h' r where "crel f h h' r" "crel (g r) h' h'' r'"
    5.57 -  using assms by (auto simp add: crel_def bind_def split: option.split_asm)
    5.58 -
    5.59 -lemma crelE'[consumes 1]:
    5.60 -  assumes "crel (f >> g) h h'' r'"
    5.61 -  obtains h' r where "crel f h h' r" "crel g h' h'' r'"
    5.62 -  using assms
    5.63 -  by (elim crelE) auto
    5.64 +lemma crel_option_caseI:
    5.65 +  assumes "\<And>y. x = Some y \<Longrightarrow> crel (s y) h h' r"
    5.66 +  assumes "x = None \<Longrightarrow> crel n h h' r"
    5.67 +  shows "crel (case x of None \<Rightarrow> n | Some y \<Rightarrow> s y) h h' r"
    5.68 +using assms
    5.69 +by (auto split: option.split)
    5.70  
    5.71 -lemma crel_return[consumes 1]:
    5.72 -  assumes "crel (return x) h h' r"
    5.73 -  obtains "r = x" "h = h'"
    5.74 -  using assms
    5.75 -  unfolding crel_def return_def by simp
    5.76 +lemma crelI2:
    5.77 +  assumes "\<exists>h' rs'. crel f h h' rs' \<and> (\<exists>h'' rs. crel (g rs') h' h'' rs)"
    5.78 +  shows "\<exists>h'' rs. crel (f\<guillemotright>= g) h h'' rs"
    5.79 +  oops
    5.80  
    5.81 -lemma crel_raise[consumes 1]:
    5.82 -  assumes "crel (raise x) h h' r"
    5.83 -  obtains "False"
    5.84 -  using assms
    5.85 -  unfolding crel_def raise_def by simp
    5.86 -
    5.87 -lemma crel_if:
    5.88 -  assumes "crel (if c then t else e) h h' r"
    5.89 -  obtains "c" "crel t h h' r"
    5.90 -        | "\<not>c" "crel e h h' r"
    5.91 -  using assms
    5.92 -  unfolding crel_def by auto
    5.93 +lemma crel_ifI2:
    5.94 +  assumes "c \<Longrightarrow> \<exists>h' r. crel t h h' r"
    5.95 +  "\<not> c \<Longrightarrow> \<exists>h' r. crel e h h' r"
    5.96 +  shows "\<exists> h' r. crel (if c then t else e) h h' r"
    5.97 +  oops
    5.98  
    5.99  lemma crel_option_case:
   5.100    assumes "crel (case x of None \<Rightarrow> n | Some y \<Rightarrow> s y) h h' r"
   5.101    obtains "x = None" "crel n h h' r"
   5.102          | y where "x = Some y" "crel (s y) h h' r" 
   5.103 -  using assms
   5.104 -  unfolding crel_def by auto
   5.105 +  using assms unfolding crel_def by (auto split: option.splits)
   5.106  
   5.107  lemma crel_fold_map:
   5.108    assumes "crel (Heap_Monad.fold_map f xs) h h' r"
   5.109 @@ -86,73 +43,19 @@
   5.110  using assms(1)
   5.111  proof (induct xs arbitrary: h h' r)
   5.112    case Nil  with assms(2) show ?case
   5.113 -    by (auto elim: crel_return)
   5.114 +    by (auto elim: crel_returnE)
   5.115  next
   5.116    case (Cons x xs)
   5.117    from Cons(2) obtain h1 y ys where crel_f: "crel (f x) h h1 y"
   5.118      and crel_fold_map: "crel (Heap_Monad.fold_map f xs) h1 h' ys"
   5.119      and r_def: "r = y#ys"
   5.120      unfolding fold_map.simps
   5.121 -    by (auto elim!: crelE crel_return)
   5.122 +    by (auto elim!: crel_bindE crel_returnE)
   5.123    from Cons(1)[OF crel_fold_map] crel_fold_map crel_f assms(3) r_def
   5.124    show ?case by auto
   5.125  qed
   5.126  
   5.127 -
   5.128 -subsection {* Elimination rules for array commands *}
   5.129 -
   5.130 -(* Strong version of the lemma for this operation is missing *) 
   5.131 -lemma crel_new_weak:
   5.132 -  assumes "crel (Array.new n v) h h' r"
   5.133 -  obtains "get_array r h' = List.replicate n v"
   5.134 -  using assms unfolding Array.new_def
   5.135 -  by (elim crel_heap) (auto simp: array_def Let_def split_def)
   5.136 -
   5.137 -(* Strong version of the lemma for this operation is missing *)
   5.138 -lemma crel_of_list_weak:
   5.139 -  assumes "crel (Array.of_list xs) h h' r"
   5.140 -  obtains "get_array r h' = xs"
   5.141 -  using assms unfolding of_list_def 
   5.142 -  by (elim crel_heap) (simp add: get_array_init_array_list)
   5.143 -
   5.144 -(* Strong version of the lemma for this operation is missing *)
   5.145 -lemma crel_make_weak:
   5.146 -  assumes "crel (Array.make n f) h h' r"
   5.147 -  obtains "i < n \<Longrightarrow> get_array r h' ! i = f i"
   5.148 -  using assms unfolding Array.make_def
   5.149 -  by (elim crel_heap) (auto simp: array_def Let_def split_def)
   5.150 -
   5.151 -lemma crel_length:
   5.152 -  assumes "crel (len a) h h' r"
   5.153 -  obtains "h = h'" "r = Array.length a h'"
   5.154 -  using assms unfolding Array.len_def
   5.155 -  by (elim crel_tap) simp
   5.156 -
   5.157 -lemma crel_nth[consumes 1]:
   5.158 -  assumes "crel (nth a i) h h' r"
   5.159 -  obtains "r = get_array a h ! i" "h = h'" "i < Array.length a h"
   5.160 -  using assms unfolding nth_def
   5.161 -  by (elim crel_guard) (clarify, simp)
   5.162 -
   5.163 -lemma crel_upd[consumes 1]:
   5.164 -  assumes "crel (upd i v a) h h' r"
   5.165 -  obtains "r = a" "h' = Array.change a i v h" "i < Array.length a h"
   5.166 -  using assms unfolding upd_def
   5.167 -  by (elim crel_guard) simp
   5.168 -
   5.169 -lemma crel_map_entry:
   5.170 -  assumes "crel (Array.map_entry i f a) h h' r"
   5.171 -  obtains "r = a" "h' = Array.change a i (f (get_array a h ! i)) h" "i < Array.length a h"
   5.172 -  using assms unfolding Array.map_entry_def
   5.173 -  by (elim crel_guard) simp
   5.174 -
   5.175 -lemma crel_swap:
   5.176 -  assumes "crel (Array.swap i x a) h h' r"
   5.177 -  obtains "r = get_array a h ! i" "h' = Array.change a i x h"
   5.178 -  using assms unfolding Array.swap_def
   5.179 -  by (elim crel_guard) simp
   5.180 -
   5.181 -lemma upt_conv_Cons': (*FIXME move*)
   5.182 +lemma upt_conv_Cons':
   5.183    assumes "Suc a \<le> b"
   5.184    shows "[b - Suc a..<b] = (b - Suc a)#[b - a..<b]"
   5.185  proof -
   5.186 @@ -169,7 +72,7 @@
   5.187  using assms
   5.188  proof (induct n arbitrary: xs h h')
   5.189    case 0 thus ?case
   5.190 -    by (auto elim!: crel_return simp add: Array.length_def)
   5.191 +    by (auto elim!: crel_returnE simp add: Array.length_def)
   5.192  next
   5.193    case (Suc n)
   5.194    from Suc(3) 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]"
   5.195 @@ -177,7 +80,7 @@
   5.196    with Suc(2) obtain r where
   5.197      crel_fold_map: "crel (Heap_Monad.fold_map (Array.nth a) [Array.length a h - n..<Array.length a h]) h h' r"
   5.198      and xs_def: "xs = get_array a h ! (Array.length a h - Suc n) # r"
   5.199 -    by (auto elim!: crelE crel_nth crel_return)
   5.200 +    by (auto elim!: crel_bindE crel_nthE crel_returnE)
   5.201    from Suc(3) have "Array.length a h - n = Suc (Array.length a h - Suc n)" 
   5.202      by arith
   5.203    with Suc.hyps[OF crel_fold_map] xs_def show ?case
   5.204 @@ -185,12 +88,6 @@
   5.205      by (auto simp add: nth_drop')
   5.206  qed
   5.207  
   5.208 -lemma crel_freeze:
   5.209 -  assumes "crel (Array.freeze a) h h' xs"
   5.210 -  obtains "h = h'" "xs = get_array a h"
   5.211 -  using assms unfolding freeze_def
   5.212 -  by (elim crel_tap) simp
   5.213 -
   5.214  lemma crel_fold_map_map_entry_remains:
   5.215    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"
   5.216    assumes "i < Array.length a h - n"
   5.217 @@ -199,7 +96,7 @@
   5.218  proof (induct n arbitrary: h h' r)
   5.219    case 0
   5.220    thus ?case
   5.221 -    by (auto elim: crel_return)
   5.222 +    by (auto elim: crel_returnE)
   5.223  next
   5.224    case (Suc n)
   5.225    let ?h1 = "Array.change a (Array.length a h - Suc n) (f (get_array a h ! (Array.length a h - Suc n))) h"
   5.226 @@ -207,7 +104,7 @@
   5.227      by (simp add: upt_conv_Cons')
   5.228    from Suc(2) this obtain r where
   5.229      crel_fold_map: "crel (Heap_Monad.fold_map (\<lambda>n. map_entry n f a) [Array.length a h - n..<Array.length a h]) ?h1 h' r"
   5.230 -    by (auto simp add: elim!: crelE crel_map_entry crel_return)
   5.231 +    by (auto simp add: elim!: crel_bindE crel_map_entryE crel_returnE)
   5.232    have length_remains: "Array.length a ?h1 = Array.length a h" by simp
   5.233    from crel_fold_map have crel_fold_map': "crel (Heap_Monad.fold_map (\<lambda>n. map_entry n f a) [Array.length a ?h1 - n..<Array.length a ?h1]) ?h1 h' r"
   5.234      by simp
   5.235 @@ -224,7 +121,7 @@
   5.236  proof (induct n arbitrary: h h' r)
   5.237    case 0
   5.238    thus ?case
   5.239 -    by (auto elim!: crel_return)
   5.240 +    by (auto elim!: crel_returnE)
   5.241  next
   5.242    case (Suc n)
   5.243    let ?h1 = "Array.change a (Array.length a h - Suc n) (f (get_array a h ! (Array.length a h - Suc n))) h"
   5.244 @@ -232,7 +129,7 @@
   5.245      by (simp add: upt_conv_Cons')
   5.246    from Suc(2) this obtain r where
   5.247      crel_fold_map: "crel (Heap_Monad.fold_map (\<lambda>n. map_entry n f a) [Array.length a h - n..<Array.length a h]) ?h1 h' r"
   5.248 -    by (auto simp add: elim!: crelE crel_map_entry crel_return)
   5.249 +    by (auto simp add: elim!: crel_bindE crel_map_entryE crel_returnE)
   5.250    have length_remains: "Array.length a ?h1 = Array.length a h" by simp
   5.251    from Suc(3) have less: "Array.length a h - Suc n < Array.length a h - n" by arith
   5.252    from Suc(3) have less2: "Array.length a h - Suc n < Array.length a h" by arith
   5.253 @@ -252,7 +149,7 @@
   5.254  using assms
   5.255  proof (induct n arbitrary: h h' r)
   5.256    case 0
   5.257 -  thus ?case by (auto elim!: crel_return)
   5.258 +  thus ?case by (auto elim!: crel_returnE)
   5.259  next
   5.260    case (Suc n)
   5.261    let ?h1 = "Array.change a (Array.length a h - Suc n) (f (get_array a h ! (Array.length a h - Suc n))) h"
   5.262 @@ -260,7 +157,7 @@
   5.263      by (simp add: upt_conv_Cons')
   5.264    from Suc(2) this obtain r where 
   5.265      crel_fold_map: "crel (Heap_Monad.fold_map (\<lambda>n. map_entry n f a) [Array.length a h - n..<Array.length a h]) ?h1 h' r"
   5.266 -    by (auto elim!: crelE crel_map_entry crel_return)
   5.267 +    by (auto elim!: crel_bindE crel_map_entryE crel_returnE)
   5.268    have length_remains: "Array.length a ?h1 = Array.length a h" by simp
   5.269    from crel_fold_map have crel_fold_map': "crel (Heap_Monad.fold_map (\<lambda>n. map_entry n f a) [Array.length a ?h1 - n..<Array.length a ?h1]) ?h1 h' r"
   5.270      by simp
   5.271 @@ -278,222 +175,6 @@
   5.272      by (auto intro: nth_equalityI)
   5.273  qed
   5.274  
   5.275 -
   5.276 -subsection {* Elimination rules for reference commands *}
   5.277 -
   5.278 -(* TODO:
   5.279 -maybe introduce a new predicate "extends h' h x"
   5.280 -which means h' extends h with a new reference x.
   5.281 -Then crel_new: would be
   5.282 -assumes "crel (Ref.new v) h h' x"
   5.283 -obtains "get_ref x h' = v"
   5.284 -and "extends h' h x"
   5.285 -
   5.286 -and we would need further rules for extends:
   5.287 -extends h' h x \<Longrightarrow> \<not> ref_present x h
   5.288 -extends h' h x \<Longrightarrow>  ref_present x h'
   5.289 -extends h' h x \<Longrightarrow> ref_present y h \<Longrightarrow> ref_present y h'
   5.290 -extends h' h x \<Longrightarrow> ref_present y h \<Longrightarrow> get_ref y h = get_ref y h'
   5.291 -extends h' h x \<Longrightarrow> lim h' = Suc (lim h)
   5.292 -*)
   5.293 -
   5.294 -lemma crel_ref:
   5.295 -  assumes "crel (ref v) h h' x"
   5.296 -  obtains "Ref.get h' x = v"
   5.297 -  and "\<not> Ref.present h x"
   5.298 -  and "Ref.present h' x"
   5.299 -  and "\<forall>y. Ref.present h y \<longrightarrow> Ref.get h y = Ref.get h' y"
   5.300 - (* and "lim h' = Suc (lim h)" *)
   5.301 -  and "\<forall>y. Ref.present h y \<longrightarrow> Ref.present h' y"
   5.302 -  using assms
   5.303 -  unfolding Ref.ref_def
   5.304 -  apply (elim crel_heap)
   5.305 -  unfolding Ref.alloc_def
   5.306 -  apply (simp add: Let_def)
   5.307 -  unfolding Ref.present_def
   5.308 -  apply auto
   5.309 -  unfolding Ref.get_def Ref.set_def
   5.310 -  apply auto
   5.311 -  done
   5.312 -
   5.313 -lemma crel_lookup:
   5.314 -  assumes "crel (!r') h h' r"
   5.315 -  obtains "h = h'" "r = Ref.get h r'"
   5.316 -  using assms unfolding Ref.lookup_def
   5.317 -  by (auto elim: crel_tap)
   5.318 -
   5.319 -lemma crel_update:
   5.320 -  assumes "crel (r' := v) h h' r"
   5.321 -  obtains "h' = Ref.set r' v h" "r = ()"
   5.322 -  using assms unfolding Ref.update_def
   5.323 -  by (auto elim: crel_heap)
   5.324 -
   5.325 -lemma crel_change:
   5.326 -  assumes "crel (Ref.change f r') h h' r"
   5.327 -  obtains "h' = Ref.set r' (f (Ref.get h r')) h" "r = f (Ref.get h r')"
   5.328 -  using assms unfolding Ref.change_def Let_def
   5.329 -  by (auto elim!: crelE crel_lookup crel_update crel_return)
   5.330 -
   5.331 -subsection {* Elimination rules for the assert command *}
   5.332 -
   5.333 -lemma crel_assert[consumes 1]:
   5.334 -  assumes "crel (assert P x) h h' r"
   5.335 -  obtains "P x" "r = x" "h = h'"
   5.336 -  using assms
   5.337 -  unfolding assert_def
   5.338 -  by (elim crel_if crel_return crel_raise) auto
   5.339 -
   5.340 -lemma crel_assert_eq: "(\<And>h h' r. crel f h h' r \<Longrightarrow> P r) \<Longrightarrow> f \<guillemotright>= assert P = f"
   5.341 -unfolding crel_def bind_def Let_def assert_def
   5.342 -  raise_def return_def prod_case_beta
   5.343 -apply (cases f)
   5.344 -apply simp
   5.345 -apply (simp add: expand_fun_eq split_def)
   5.346 -apply (auto split: option.split)
   5.347 -apply (erule_tac x="x" in meta_allE)
   5.348 -apply auto
   5.349 -done
   5.350 -
   5.351 -section {* Introduction rules *}
   5.352 -
   5.353 -subsection {* Introduction rules for basic monadic commands *}
   5.354 -
   5.355 -lemma crelI:
   5.356 -  assumes "crel f h h' r" "crel (g r) h' h'' r'"
   5.357 -  shows "crel (f >>= g) h h'' r'"
   5.358 -  using assms by (simp add: crel_def' bind_def)
   5.359 -
   5.360 -lemma crelI':
   5.361 -  assumes "crel f h h' r" "crel g h' h'' r'"
   5.362 -  shows "crel (f >> g) h h'' r'"
   5.363 -  using assms by (intro crelI) auto
   5.364 -
   5.365 -lemma crel_returnI:
   5.366 -  shows "crel (return x) h h x"
   5.367 -  unfolding crel_def return_def by simp
   5.368 -
   5.369 -lemma crel_raiseI:
   5.370 -  shows "\<not> (crel (raise x) h h' r)"
   5.371 -  unfolding crel_def raise_def by simp
   5.372 -
   5.373 -lemma crel_ifI:
   5.374 -  assumes "c \<longrightarrow> crel t h h' r"
   5.375 -  "\<not>c \<longrightarrow> crel e h h' r"
   5.376 -  shows "crel (if c then t else e) h h' r"
   5.377 -  using assms
   5.378 -  unfolding crel_def by auto
   5.379 -
   5.380 -lemma crel_option_caseI:
   5.381 -  assumes "\<And>y. x = Some y \<Longrightarrow> crel (s y) h h' r"
   5.382 -  assumes "x = None \<Longrightarrow> crel n h h' r"
   5.383 -  shows "crel (case x of None \<Rightarrow> n | Some y \<Rightarrow> s y) h h' r"
   5.384 -using assms
   5.385 -by (auto split: option.split)
   5.386 -
   5.387 -lemma crel_tapI:
   5.388 -  assumes "h' = h" "r = f h"
   5.389 -  shows "crel (Heap_Monad.tap f) h h' r"
   5.390 -  using assms by (simp add: crel_def)
   5.391 -
   5.392 -lemma crel_heapI:
   5.393 -  shows "crel (Heap_Monad.heap f) h (snd (f h)) (fst (f h))"
   5.394 -  by (simp add: crel_def apfst_def split_def prod_fun_def)
   5.395 -
   5.396 -lemma crel_heapI': (*FIXME keep only this version*)
   5.397 -  assumes "h' = snd (f h)" "r = fst (f h)"
   5.398 -  shows "crel (Heap_Monad.heap f) h h' r"
   5.399 -  using assms
   5.400 -  by (simp add: crel_def split_def apfst_def prod_fun_def)
   5.401 -
   5.402 -lemma crel_guardI:
   5.403 -  assumes "P h" "h' = snd (f h)" "r = fst (f h)"
   5.404 -  shows "crel (Heap_Monad.guard P f) h h' r"
   5.405 -  using assms by (simp add: crel_def execute_simps)
   5.406 -
   5.407 -lemma crelI2:
   5.408 -  assumes "\<exists>h' rs'. crel f h h' rs' \<and> (\<exists>h'' rs. crel (g rs') h' h'' rs)"
   5.409 -  shows "\<exists>h'' rs. crel (f\<guillemotright>= g) h h'' rs"
   5.410 -  oops
   5.411 -
   5.412 -lemma crel_ifI2:
   5.413 -  assumes "c \<Longrightarrow> \<exists>h' r. crel t h h' r"
   5.414 -  "\<not> c \<Longrightarrow> \<exists>h' r. crel e h h' r"
   5.415 -  shows "\<exists> h' r. crel (if c then t else e) h h' r"
   5.416 -  oops
   5.417 -
   5.418 -subsection {* Introduction rules for array commands *}
   5.419 -
   5.420 -lemma crel_lengthI:
   5.421 -  shows "crel (Array.len a) h h (Array.length a h)"
   5.422 -  unfolding len_def by (rule crel_tapI) simp_all
   5.423 -
   5.424 -(* thm crel_newI for Array.new is missing *)
   5.425 -
   5.426 -lemma crel_nthI:
   5.427 -  assumes "i < Array.length a h"
   5.428 -  shows "crel (nth a i) h h ((get_array a h) ! i)"
   5.429 -  using assms unfolding nth_def by (auto intro: crel_guardI)
   5.430 -
   5.431 -lemma crel_updI:
   5.432 -  assumes "i < Array.length a h"
   5.433 -  shows "crel (upd i v a) h (Array.change a i v h) a"
   5.434 -  using assms unfolding upd_def by (auto intro: crel_guardI)
   5.435 -
   5.436 -(* thm crel_of_listI is missing *)
   5.437 -
   5.438 -(* thm crel_map_entryI is missing *)
   5.439 -
   5.440 -(* thm crel_swapI is missing *)
   5.441 -
   5.442 -(* thm crel_makeI is missing *)
   5.443 -
   5.444 -(* thm crel_freezeI is missing *)
   5.445 -
   5.446 -(* thm crel_mapI is missing *)
   5.447 -
   5.448 -subsubsection {* Introduction rules for reference commands *}
   5.449 -
   5.450 -lemma crel_lookupI:
   5.451 -  shows "crel (!r) h h (Ref.get h r)"
   5.452 -  unfolding lookup_def by (auto intro!: crel_tapI)
   5.453 -
   5.454 -lemma crel_updateI:
   5.455 -  shows "crel (r := v) h (Ref.set r v h) ()"
   5.456 -  unfolding update_def by (auto intro!: crel_heapI')
   5.457 -
   5.458 -lemma crel_changeI: 
   5.459 -  shows "crel (Ref.change f r) h (Ref.set r (f (Ref.get h r)) h) (f (Ref.get h r))"
   5.460 -  unfolding change_def Let_def by (auto intro!: crelI crel_returnI crel_lookupI crel_updateI)
   5.461 -
   5.462 -subsubsection {* Introduction rules for the assert command *}
   5.463 -
   5.464 -lemma crel_assertI:
   5.465 -  assumes "P x"
   5.466 -  shows "crel (assert P x) h h x"
   5.467 -  using assms
   5.468 -  unfolding assert_def
   5.469 -  by (auto intro!: crel_ifI crel_returnI crel_raiseI)
   5.470 - 
   5.471 -subsection {* Induction rule for the MREC combinator *}
   5.472 -
   5.473 -lemma MREC_induct:
   5.474 -  assumes "crel (MREC f g x) h h' r"
   5.475 -  assumes "\<And> x h h' r. crel (f x) h h' (Inl r) \<Longrightarrow> P x h h' r"
   5.476 -  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
   5.477 -    \<Longrightarrow> crel (g x s z) h2 h' r \<Longrightarrow> P x h h' r"
   5.478 -  shows "P x h h' r"
   5.479 -proof (rule MREC_pinduct[OF assms(1)[unfolded crel_def, symmetric]])
   5.480 -  fix x h h1 h2 h' s z r
   5.481 -  assume "Heap_Monad.execute (f x) h = Some (Inr s, h1)"
   5.482 -    "Heap_Monad.execute (MREC f g s) h1 = Some (z, h2)"
   5.483 -    "P s h1 h2 z"
   5.484 -    "Heap_Monad.execute (g x s z) h2 = Some (r, h')"
   5.485 -  from assms(3)[unfolded crel_def, OF this(1)[symmetric] this(2)[symmetric] this(3) this(4)[symmetric]]
   5.486 -  show "P x h h' r" .
   5.487 -next
   5.488 -qed (auto simp add: assms(2)[unfolded crel_def])
   5.489 -
   5.490 -
   5.491  lemma success_fold_map_map_entry:
   5.492    assumes "n \<le> Array.length a h"
   5.493    shows "success (Heap_Monad.fold_map (\<lambda>n. map_entry n f a) [Array.length a h - n..<Array.length a h]) h"
   5.494 @@ -507,25 +188,26 @@
   5.495      (Array.length a h - Suc n) # [Array.length a h - n..<Array.length a h]"
   5.496      by (simp add: upt_conv_Cons')
   5.497    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 -
   5.498 -    apply (auto simp add: execute_simps intro!: successI success_returnI success_map_entryI elim: crel_map_entry)
   5.499 -    apply (subst execute_bind) apply (auto simp add: execute_simps)
   5.500 +    apply (auto simp add: execute_simps execute_bind_success intro!: successI success_returnI success_map_entryI elim: crel_map_entryE)
   5.501 +    apply (subst execute_bind) apply (auto simp add: execute_simps execute_bind_success intro: execute_bind)
   5.502      done
   5.503  qed
   5.504  
   5.505 -
   5.506 -section {* Cumulative lemmas *}
   5.507 -
   5.508 -lemmas crel_elim_all =
   5.509 -  crelE crelE' crel_return crel_raise crel_if crel_option_case
   5.510 -  crel_length crel_new_weak crel_nth crel_upd crel_of_list_weak crel_map_entry crel_swap crel_make_weak crel_freeze
   5.511 -  crel_ref crel_lookup crel_update crel_change
   5.512 -  crel_assert
   5.513 +lemma MREC_induct:
   5.514 +  assumes "crel (MREC f g x) h h' r"
   5.515 +  assumes "\<And> x h h' r. crel (f x) h h' (Inl r) \<Longrightarrow> P x h h' r"
   5.516 +  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
   5.517 +    \<Longrightarrow> crel (g x s z) h2 h' r \<Longrightarrow> P x h h' r"
   5.518 +  shows "P x h h' r"
   5.519 +proof (rule MREC_pinduct[OF assms(1) [unfolded crel_def]])
   5.520 +  fix x h h1 h2 h' s z r
   5.521 +  assume "Heap_Monad.execute (f x) h = Some (Inr s, h1)"
   5.522 +    "Heap_Monad.execute (MREC f g s) h1 = Some (z, h2)"
   5.523 +    "P s h1 h2 z"
   5.524 +    "Heap_Monad.execute (g x s z) h2 = Some (r, h')"
   5.525 +  from assms(3) [unfolded crel_def, OF this(1) this(2) this(3) this(4)]
   5.526 +  show "P x h h' r" .
   5.527 +next
   5.528 +qed (auto simp add: assms(2)[unfolded crel_def])
   5.529  
   5.530 -lemmas crel_intro_all =
   5.531 -  crelI crelI' crel_returnI crel_raiseI crel_ifI crel_option_caseI
   5.532 -  crel_lengthI (* crel_newI *) crel_nthI crel_updI (* crel_of_listI crel_map_entryI crel_swapI crel_makeI crel_freezeI crel_mapI *)
   5.533 -  (* crel_Ref_newI *) crel_lookupI crel_updateI crel_changeI
   5.534 -  crel_assert
   5.535 -
   5.536 -
   5.537 -end
   5.538 \ No newline at end of file
   5.539 +end
     6.1 --- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Mon Jul 12 11:39:27 2010 +0200
     6.2 +++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Mon Jul 12 16:05:08 2010 +0200
     6.3 @@ -5,7 +5,7 @@
     6.4  header {* An imperative implementation of Quicksort on arrays *}
     6.5  
     6.6  theory Imperative_Quicksort
     6.7 -imports "~~/src/HOL/Imperative_HOL/Imperative_HOL" Subarray Multiset Efficient_Nat
     6.8 +imports Imperative_HOL Subarray Multiset Efficient_Nat
     6.9  begin
    6.10  
    6.11  text {* We prove QuickSort correct in the Relational Calculus. *}
    6.12 @@ -21,13 +21,20 @@
    6.13         return ()
    6.14       done)"
    6.15  
    6.16 +lemma crel_swapI [crel_intros]:
    6.17 +  assumes "i < Array.length a h" "j < Array.length a h"
    6.18 +    "x = get_array a h ! i" "y = get_array a h ! j"
    6.19 +    "h' = Array.change a j x (Array.change a i y h)"
    6.20 +  shows "crel (swap a i j) h h' r"
    6.21 +  unfolding swap_def using assms by (auto intro!: crel_intros)
    6.22 +
    6.23  lemma swap_permutes:
    6.24    assumes "crel (swap a i j) h h' rs"
    6.25    shows "multiset_of (get_array a h') 
    6.26    = multiset_of (get_array a h)"
    6.27    using assms
    6.28    unfolding swap_def
    6.29 -  by (auto simp add: Array.length_def multiset_of_swap dest: sym [of _ "h'"] elim!: crelE crel_nth crel_return crel_upd)
    6.30 +  by (auto simp add: Array.length_def multiset_of_swap dest: sym [of _ "h'"] elim!: crel_bindE crel_nthE crel_returnE crel_updE)
    6.31  
    6.32  function part1 :: "nat array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat Heap"
    6.33  where
    6.34 @@ -55,7 +62,7 @@
    6.35    case (1 a l r p h h' rs)
    6.36    thus ?case
    6.37      unfolding part1.simps [of a l r p]
    6.38 -    by (elim crelE crel_if crel_return crel_nth) (auto simp add: swap_permutes)
    6.39 +    by (elim crel_bindE crel_ifE crel_returnE crel_nthE) (auto simp add: swap_permutes)
    6.40  qed
    6.41  
    6.42  lemma part_returns_index_in_bounds:
    6.43 @@ -71,7 +78,7 @@
    6.44      case True (* Terminating case *)
    6.45      with cr `l \<le> r` show ?thesis
    6.46        unfolding part1.simps[of a l r p]
    6.47 -      by (elim crelE crel_if crel_return crel_nth) auto
    6.48 +      by (elim crel_bindE crel_ifE crel_returnE crel_nthE) auto
    6.49    next
    6.50      case False (* recursive case *)
    6.51      note rec_condition = this
    6.52 @@ -82,7 +89,7 @@
    6.53        with cr False
    6.54        have rec1: "crel (part1 a (l + 1) r p) h h' rs"
    6.55          unfolding part1.simps[of a l r p]
    6.56 -        by (elim crelE crel_nth crel_if crel_return) auto
    6.57 +        by (elim crel_bindE crel_nthE crel_ifE crel_returnE) auto
    6.58        from rec_condition have "l + 1 \<le> r" by arith
    6.59        from 1(1)[OF rec_condition True rec1 `l + 1 \<le> r`]
    6.60        show ?thesis by simp
    6.61 @@ -92,7 +99,7 @@
    6.62        obtain h1 where swp: "crel (swap a l r) h h1 ()"
    6.63          and rec2: "crel (part1 a l (r - 1) p) h1 h' rs"
    6.64          unfolding part1.simps[of a l r p]
    6.65 -        by (elim crelE crel_nth crel_if crel_return) auto
    6.66 +        by (elim crel_bindE crel_nthE crel_ifE crel_returnE) auto
    6.67        from rec_condition have "l \<le> r - 1" by arith
    6.68        from 1(2) [OF rec_condition False rec2 `l \<le> r - 1`] show ?thesis by fastsimp
    6.69      qed
    6.70 @@ -112,12 +119,12 @@
    6.71      case True (* Terminating case *)
    6.72      with cr show ?thesis
    6.73        unfolding part1.simps[of a l r p]
    6.74 -      by (elim crelE crel_if crel_return crel_nth) auto
    6.75 +      by (elim crel_bindE crel_ifE crel_returnE crel_nthE) auto
    6.76    next
    6.77      case False (* recursive case *)
    6.78      with cr 1 show ?thesis
    6.79        unfolding part1.simps [of a l r p] swap_def
    6.80 -      by (auto elim!: crelE crel_if crel_nth crel_return crel_upd) fastsimp
    6.81 +      by (auto elim!: crel_bindE crel_ifE crel_nthE crel_returnE crel_updE) fastsimp
    6.82    qed
    6.83  qed
    6.84  
    6.85 @@ -134,7 +141,7 @@
    6.86      case True (* Terminating case *)
    6.87      with cr show ?thesis
    6.88        unfolding part1.simps[of a l r p]
    6.89 -      by (elim crelE crel_if crel_return crel_nth) auto
    6.90 +      by (elim crel_bindE crel_ifE crel_returnE crel_nthE) auto
    6.91    next
    6.92      case False (* recursive case *)
    6.93      note rec_condition = this
    6.94 @@ -145,7 +152,7 @@
    6.95        with cr False
    6.96        have rec1: "crel (part1 a (l + 1) r p) h h' rs"
    6.97          unfolding part1.simps[of a l r p]
    6.98 -        by (elim crelE crel_nth crel_if crel_return) auto
    6.99 +        by (elim crel_bindE crel_nthE crel_ifE crel_returnE) auto
   6.100        from 1(1)[OF rec_condition True rec1]
   6.101        show ?thesis by fastsimp
   6.102      next
   6.103 @@ -154,11 +161,11 @@
   6.104        obtain h1 where swp: "crel (swap a l r) h h1 ()"
   6.105          and rec2: "crel (part1 a l (r - 1) p) h1 h' rs"
   6.106          unfolding part1.simps[of a l r p]
   6.107 -        by (elim crelE crel_nth crel_if crel_return) auto
   6.108 +        by (elim crel_bindE crel_nthE crel_ifE crel_returnE) auto
   6.109        from swp rec_condition have
   6.110          "\<forall>i. i < l \<or> r < i \<longrightarrow> get_array a h ! i = get_array a h1 ! i"
   6.111          unfolding swap_def
   6.112 -        by (elim crelE crel_nth crel_upd crel_return) auto
   6.113 +        by (elim crel_bindE crel_nthE crel_updE crel_returnE) auto
   6.114        with 1(2) [OF rec_condition False rec2] show ?thesis by fastsimp
   6.115      qed
   6.116    qed
   6.117 @@ -179,7 +186,7 @@
   6.118      case True (* Terminating case *)
   6.119      with cr have "rs = r"
   6.120        unfolding part1.simps[of a l r p]
   6.121 -      by (elim crelE crel_if crel_return crel_nth) auto
   6.122 +      by (elim crel_bindE crel_ifE crel_returnE crel_nthE) auto
   6.123      with True
   6.124      show ?thesis by auto
   6.125    next
   6.126 @@ -192,7 +199,7 @@
   6.127        with lr cr
   6.128        have rec1: "crel (part1 a (l + 1) r p) h h' rs"
   6.129          unfolding part1.simps[of a l r p]
   6.130 -        by (elim crelE crel_nth crel_if crel_return) auto
   6.131 +        by (elim crel_bindE crel_nthE crel_ifE crel_returnE) auto
   6.132        from True part_outer_remains[OF rec1] have a_l: "get_array a h' ! l \<le> p"
   6.133          by fastsimp
   6.134        have "\<forall>i. (l \<le> i = (l = i \<or> Suc l \<le> i))" by arith
   6.135 @@ -204,10 +211,10 @@
   6.136        obtain h1 where swp: "crel (swap a l r) h h1 ()"
   6.137          and rec2: "crel (part1 a l (r - 1) p) h1 h' rs"
   6.138          unfolding part1.simps[of a l r p]
   6.139 -        by (elim crelE crel_nth crel_if crel_return) auto
   6.140 +        by (elim crel_bindE crel_nthE crel_ifE crel_returnE) auto
   6.141        from swp False have "get_array a h1 ! r \<ge> p"
   6.142          unfolding swap_def
   6.143 -        by (auto simp add: Array.length_def elim!: crelE crel_nth crel_upd crel_return)
   6.144 +        by (auto simp add: Array.length_def elim!: crel_bindE crel_nthE crel_updE crel_returnE)
   6.145        with part_outer_remains [OF rec2] lr have a_r: "get_array a h' ! r \<ge> p"
   6.146          by fastsimp
   6.147        have "\<forall>i. (i \<le> r = (i = r \<or> i \<le> r - 1))" by arith
   6.148 @@ -238,7 +245,7 @@
   6.149  proof -
   6.150      from assms part_permutes swap_permutes show ?thesis
   6.151        unfolding partition.simps
   6.152 -      by (elim crelE crel_return crel_nth crel_if crel_upd) auto
   6.153 +      by (elim crel_bindE crel_returnE crel_nthE crel_ifE crel_updE) auto
   6.154  qed
   6.155  
   6.156  lemma partition_length_remains:
   6.157 @@ -247,7 +254,7 @@
   6.158  proof -
   6.159    from assms part_length_remains show ?thesis
   6.160      unfolding partition.simps swap_def
   6.161 -    by (elim crelE crel_return crel_nth crel_if crel_upd) auto
   6.162 +    by (elim crel_bindE crel_returnE crel_nthE crel_ifE crel_updE) auto
   6.163  qed
   6.164  
   6.165  lemma partition_outer_remains:
   6.166 @@ -257,7 +264,7 @@
   6.167  proof -
   6.168    from assms part_outer_remains part_returns_index_in_bounds show ?thesis
   6.169      unfolding partition.simps swap_def
   6.170 -    by (elim crelE crel_return crel_nth crel_if crel_upd) fastsimp
   6.171 +    by (elim crel_bindE crel_returnE crel_nthE crel_ifE crel_updE) fastsimp
   6.172  qed
   6.173  
   6.174  lemma partition_returns_index_in_bounds:
   6.175 @@ -269,7 +276,7 @@
   6.176      and rs_equals: "rs = (if get_array a h'' ! middle \<le> get_array a h ! r then middle + 1
   6.177           else middle)"
   6.178      unfolding partition.simps
   6.179 -    by (elim crelE crel_return crel_nth crel_if crel_upd) simp
   6.180 +    by (elim crel_bindE crel_returnE crel_nthE crel_ifE crel_updE) simp
   6.181    from `l < r` have "l \<le> r - 1" by arith
   6.182    from part_returns_index_in_bounds[OF part this] rs_equals `l < r` show ?thesis by auto
   6.183  qed
   6.184 @@ -286,17 +293,17 @@
   6.185      and rs_equals: "rs = (if get_array a h1 ! middle \<le> ?pivot then middle + 1
   6.186           else middle)"
   6.187      unfolding partition.simps
   6.188 -    by (elim crelE crel_return crel_nth crel_if crel_upd) simp
   6.189 +    by (elim crel_bindE crel_returnE crel_nthE crel_ifE crel_updE) simp
   6.190    from swap have h'_def: "h' = Array.change a r (get_array a h1 ! rs)
   6.191      (Array.change a rs (get_array a h1 ! r) h1)"
   6.192      unfolding swap_def
   6.193 -    by (elim crelE crel_return crel_nth crel_upd) simp
   6.194 +    by (elim crel_bindE crel_returnE crel_nthE crel_updE) simp
   6.195    from swap have in_bounds: "r < Array.length a h1 \<and> rs < Array.length a h1"
   6.196      unfolding swap_def
   6.197 -    by (elim crelE crel_return crel_nth crel_upd) simp
   6.198 +    by (elim crel_bindE crel_returnE crel_nthE crel_updE) simp
   6.199    from swap have swap_length_remains: "Array.length a h1 = Array.length a h'"
   6.200 -    unfolding swap_def by (elim crelE crel_return crel_nth crel_upd) auto
   6.201 -  from `l < r` have "l \<le> r - 1" by simp 
   6.202 +    unfolding swap_def by (elim crel_bindE crel_returnE crel_nthE crel_updE) auto
   6.203 +  from `l < r` have "l \<le> r - 1" by simp
   6.204    note middle_in_bounds = part_returns_index_in_bounds[OF part this]
   6.205    from part_outer_remains[OF part] `l < r`
   6.206    have "get_array a h ! r = get_array a h1 ! r"
   6.207 @@ -304,7 +311,7 @@
   6.208    with swap
   6.209    have right_remains: "get_array a h ! r = get_array a h' ! rs"
   6.210      unfolding swap_def
   6.211 -    by (auto simp add: Array.length_def elim!: crelE crel_return crel_nth crel_upd) (cases "r = rs", auto)
   6.212 +    by (auto simp add: Array.length_def elim!: crel_bindE crel_returnE crel_nthE crel_updE) (cases "r = rs", auto)
   6.213    from part_partitions [OF part]
   6.214    show ?thesis
   6.215    proof (cases "get_array a h1 ! middle \<le> ?pivot")
   6.216 @@ -420,7 +427,7 @@
   6.217    case (1 a l r h h' rs)
   6.218    with partition_permutes show ?case
   6.219      unfolding quicksort.simps [of a l r]
   6.220 -    by (elim crel_if crelE crel_assert crel_return) auto
   6.221 +    by (elim crel_ifE crel_bindE crel_assertE crel_returnE) auto
   6.222  qed
   6.223  
   6.224  lemma length_remains:
   6.225 @@ -431,7 +438,7 @@
   6.226    case (1 a l r h h' rs)
   6.227    with partition_length_remains show ?case
   6.228      unfolding quicksort.simps [of a l r]
   6.229 -    by (elim crel_if crelE crel_assert crel_return) auto
   6.230 +    by (elim crel_ifE crel_bindE crel_assertE crel_returnE) auto
   6.231  qed
   6.232  
   6.233  lemma quicksort_outer_remains:
   6.234 @@ -446,7 +453,7 @@
   6.235      case False
   6.236      with cr have "h' = h"
   6.237        unfolding quicksort.simps [of a l r]
   6.238 -      by (elim crel_if crel_return) auto
   6.239 +      by (elim crel_ifE crel_returnE) auto
   6.240      thus ?thesis by simp
   6.241    next
   6.242    case True
   6.243 @@ -469,7 +476,7 @@
   6.244      }
   6.245      with cr show ?thesis
   6.246        unfolding quicksort.simps [of a l r]
   6.247 -      by (elim crel_if crelE crel_assert crel_return) auto
   6.248 +      by (elim crel_ifE crel_bindE crel_assertE crel_returnE) auto
   6.249    qed
   6.250  qed
   6.251  
   6.252 @@ -478,7 +485,7 @@
   6.253    shows "r \<le> l \<longrightarrow> h = h'"
   6.254    using assms
   6.255    unfolding quicksort.simps [of a l r]
   6.256 -  by (elim crel_if crel_return) auto
   6.257 +  by (elim crel_ifE crel_returnE) auto
   6.258   
   6.259  lemma quicksort_sorts:
   6.260    assumes "crel (quicksort a l r) h h' rs"
   6.261 @@ -550,7 +557,7 @@
   6.262      }
   6.263      with True cr show ?thesis
   6.264        unfolding quicksort.simps [of a l r]
   6.265 -      by (elim crel_if crel_return crelE crel_assert) auto
   6.266 +      by (elim crel_ifE crel_returnE crel_bindE crel_assertE) auto
   6.267    qed
   6.268  qed
   6.269  
   6.270 @@ -581,29 +588,28 @@
   6.271    using assms
   6.272  proof (induct a l r p arbitrary: h rule: part1.induct)
   6.273    case (1 a l r p)
   6.274 -  thus ?case
   6.275 -    unfolding part1.simps [of a l r] swap_def
   6.276 -    by (auto simp add: execute_simps intro!: success_intros elim!: crelE crel_upd crel_nth crel_return)
   6.277 +  thus ?case unfolding part1.simps [of a l r]
   6.278 +  apply (auto intro!: success_intros del: success_ifI simp add: not_le)
   6.279 +  apply (auto intro!: crel_intros crel_swapI)
   6.280 +  done
   6.281  qed
   6.282  
   6.283 -lemma success_ifI: (*FIXME move*)
   6.284 -  assumes "c \<Longrightarrow> success t h" "\<not> c \<Longrightarrow> success e h"
   6.285 -  shows "success (if c then t else e) h"
   6.286 -  using assms
   6.287 -  unfolding success_def
   6.288 -  by auto
   6.289 -
   6.290  lemma success_bindI' [success_intros]: (*FIXME move*)
   6.291    assumes "success f h"
   6.292    assumes "\<And>h' r. crel f h h' r \<Longrightarrow> success (g r) h'"
   6.293    shows "success (f \<guillemotright>= g) h"
   6.294 -  using assms by (auto intro!: successI elim!: successE simp add: bind_def crel_def success_def) blast
   6.295 +using assms(1) proof (rule success_crelE)
   6.296 +  fix h' r
   6.297 +  assume "crel f h h' r"
   6.298 +  moreover with assms(2) have "success (g r) h'" .
   6.299 +  ultimately show "success (f \<guillemotright>= g) h" by (rule success_bind_crelI)
   6.300 +qed
   6.301  
   6.302  lemma success_partitionI:
   6.303    assumes "l < r" "l < Array.length a h" "r < Array.length a h"
   6.304    shows "success (partition a l r) h"
   6.305  using assms unfolding partition.simps swap_def
   6.306 -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:)
   6.307 +apply (auto intro!: success_bindI' success_ifI success_returnI success_nthI success_updI success_part1I elim!: crel_bindE crel_updE crel_nthE crel_returnE simp add:)
   6.308  apply (frule part_length_remains)
   6.309  apply (frule part_returns_index_in_bounds)
   6.310  apply auto
   6.311 @@ -627,7 +633,7 @@
   6.312      apply auto
   6.313      apply (frule partition_returns_index_in_bounds)
   6.314      apply auto
   6.315 -    apply (auto elim!: crel_assert dest!: partition_length_remains length_remains)
   6.316 +    apply (auto elim!: crel_assertE dest!: partition_length_remains length_remains)
   6.317      apply (subgoal_tac "Suc r \<le> ri \<or> r = ri") 
   6.318      apply (erule disjE)
   6.319      apply auto
     7.1 --- a/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy	Mon Jul 12 11:39:27 2010 +0200
     7.2 +++ b/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy	Mon Jul 12 16:05:08 2010 +0200
     7.3 @@ -5,7 +5,7 @@
     7.4  header {* An imperative in-place reversal on arrays *}
     7.5  
     7.6  theory Imperative_Reverse
     7.7 -imports "~~/src/HOL/Imperative_HOL/Imperative_HOL" Subarray
     7.8 +imports Imperative_HOL Subarray
     7.9  begin
    7.10  
    7.11  hide_const (open) swap rev
    7.12 @@ -36,7 +36,7 @@
    7.13        else if k = j then get_array a h ! i
    7.14        else get_array a h ! k)"
    7.15  using assms unfolding swap.simps
    7.16 -by (elim crel_elim_all)
    7.17 +by (elim crel_elims)
    7.18   (auto simp: length_def)
    7.19  
    7.20  lemma rev_pointwise: assumes "crel (rev a i j) h h' r"
    7.21 @@ -52,7 +52,7 @@
    7.22      obtain h' where
    7.23        swp: "crel (swap a i j) h h' ()"
    7.24        and rev: "crel (rev a (i + 1) (j - 1)) h' h'' ()"
    7.25 -      by (auto elim: crel_elim_all)
    7.26 +      by (auto elim: crel_elims)
    7.27      from rev 1 True
    7.28      have eq: "?P a (i + 1) (j - 1) h' h''" by auto
    7.29  
    7.30 @@ -63,7 +63,7 @@
    7.31      case False
    7.32      with 1[unfolded rev.simps[of a i j]]
    7.33      show ?thesis
    7.34 -      by (cases "k = j") (auto elim: crel_elim_all)
    7.35 +      by (cases "k = j") (auto elim: crel_elims)
    7.36    qed
    7.37  qed
    7.38  
    7.39 @@ -80,15 +80,15 @@
    7.40      obtain h' where
    7.41        swp: "crel (swap a i j) h h' ()"
    7.42        and rev: "crel (rev a (i + 1) (j - 1)) h' h'' ()"
    7.43 -      by (auto elim: crel_elim_all)
    7.44 +      by (auto elim: crel_elims)
    7.45      from swp rev 1 True show ?thesis
    7.46        unfolding swap.simps
    7.47 -      by (elim crel_elim_all) fastsimp
    7.48 +      by (elim crel_elims) fastsimp
    7.49    next
    7.50      case False
    7.51      with 1[unfolded rev.simps[of a i j]]
    7.52      show ?thesis
    7.53 -      by (auto elim: crel_elim_all)
    7.54 +      by (auto elim: crel_elims)
    7.55    qed
    7.56  qed
    7.57  
    7.58 @@ -112,7 +112,7 @@
    7.59    shows "get_array a h' = List.rev (get_array a h)"
    7.60    using rev2_rev'[OF assms] rev_length[OF assms] assms
    7.61      by (cases "Array.length a h = 0", auto simp add: Array.length_def
    7.62 -      subarray_def sublist'_all rev.simps[where j=0] elim!: crel_elim_all)
    7.63 +      subarray_def sublist'_all rev.simps[where j=0] elim!: crel_elims)
    7.64    (drule sym[of "List.length (get_array a h)"], simp)
    7.65  
    7.66  end
     8.1 --- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Mon Jul 12 11:39:27 2010 +0200
     8.2 +++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Mon Jul 12 16:05:08 2010 +0200
     8.3 @@ -5,7 +5,7 @@
     8.4  header {* Linked Lists by ML references *}
     8.5  
     8.6  theory Linked_Lists
     8.7 -imports "~~/src/HOL/Imperative_HOL/Imperative_HOL" Code_Integer
     8.8 +imports Imperative_HOL Code_Integer
     8.9  begin
    8.10  
    8.11  section {* Definition of Linked Lists *}
    8.12 @@ -42,7 +42,7 @@
    8.13  definition
    8.14    traverse :: "'a\<Colon>heap node \<Rightarrow> 'a list Heap"
    8.15  where
    8.16 -  "traverse = MREC (\<lambda>n. case n of Empty \<Rightarrow> return (Inl [])
    8.17 +[code del]: "traverse = MREC (\<lambda>n. case n of Empty \<Rightarrow> return (Inl [])
    8.18                                  | Node x r \<Rightarrow> (do tl \<leftarrow> Ref.lookup r;
    8.19                                                    return (Inr tl) done))
    8.20                     (\<lambda>n tl xs. case n of Empty \<Rightarrow> undefined
    8.21 @@ -452,18 +452,37 @@
    8.22      by simp
    8.23  qed
    8.24  
    8.25 +lemma crel_ref:
    8.26 +  assumes "crel (ref v) h h' x"
    8.27 +  obtains "Ref.get h' x = v"
    8.28 +  and "\<not> Ref.present h x"
    8.29 +  and "Ref.present h' x"
    8.30 +  and "\<forall>y. Ref.present h y \<longrightarrow> Ref.get h y = Ref.get h' y"
    8.31 + (* and "lim h' = Suc (lim h)" *)
    8.32 +  and "\<forall>y. Ref.present h y \<longrightarrow> Ref.present h' y"
    8.33 +  using assms
    8.34 +  unfolding Ref.ref_def
    8.35 +  apply (elim crel_heapE)
    8.36 +  unfolding Ref.alloc_def
    8.37 +  apply (simp add: Let_def)
    8.38 +  unfolding Ref.present_def
    8.39 +  apply auto
    8.40 +  unfolding Ref.get_def Ref.set_def
    8.41 +  apply auto
    8.42 +  done
    8.43 +
    8.44  lemma make_llist:
    8.45  assumes "crel (make_llist xs) h h' r"
    8.46  shows "list_of h' r xs \<and> (\<forall>rs. refs_of h' r rs \<longrightarrow> (\<forall>ref \<in> (set rs). Ref.present h' ref))"
    8.47  using assms 
    8.48  proof (induct xs arbitrary: h h' r)
    8.49 -  case Nil thus ?case by (auto elim: crel_return simp add: make_llist.simps)
    8.50 +  case Nil thus ?case by (auto elim: crel_returnE simp add: make_llist.simps)
    8.51  next
    8.52    case (Cons x xs')
    8.53    from Cons.prems obtain h1 r1 r' where make_llist: "crel (make_llist xs') h h1 r1"
    8.54      and crel_refnew:"crel (ref r1) h1 h' r'" and Node: "r = Node x r'"
    8.55      unfolding make_llist.simps
    8.56 -    by (auto elim!: crelE crel_return)
    8.57 +    by (auto elim!: crel_bindE crel_returnE)
    8.58    from Cons.hyps[OF make_llist] have list_of_h1: "list_of h1 r1 xs'" ..
    8.59    from Cons.hyps[OF make_llist] obtain rs' where rs'_def: "refs_of h1 r1 rs'" by (auto intro: list_of_refs_of)
    8.60    from Cons.hyps[OF make_llist] rs'_def have refs_present: "\<forall>ref\<in>set rs'. Ref.present h1 ref" by simp
    8.61 @@ -472,11 +491,11 @@
    8.62      by (auto elim!: crel_ref dest: refs_of_is_fun)
    8.63    with list_of_invariant[OF list_of_h1 refs_unchanged] Node crel_refnew have fstgoal: "list_of h' r (x # xs')"
    8.64      unfolding list_of.simps
    8.65 -    by (auto elim!: crel_ref)
    8.66 +    by (auto elim!: crel_refE)
    8.67    from refs_unchanged rs'_def have refs_still_present: "\<forall>ref\<in>set rs'. Ref.present h' ref" by auto
    8.68    from refs_of_invariant[OF rs'_def refs_unchanged] refs_unchanged Node crel_refnew refs_still_present
    8.69    have sndgoal: "\<forall>rs. refs_of h' r rs \<longrightarrow> (\<forall>ref\<in>set rs. Ref.present h' ref)"
    8.70 -    by (fastsimp elim!: crel_ref dest: refs_of_is_fun)
    8.71 +    by (fastsimp elim!: crel_refE dest: refs_of_is_fun)
    8.72    from fstgoal sndgoal show ?case ..
    8.73  qed
    8.74  
    8.75 @@ -489,7 +508,7 @@
    8.76    case (Cons x xs)
    8.77    thus ?case
    8.78    apply (cases n, auto)
    8.79 -  by (auto intro!: crelI crel_returnI crel_lookupI)
    8.80 +  by (auto intro!: crel_bindI crel_returnI crel_lookupI)
    8.81  qed
    8.82  
    8.83  lemma traverse_make_llist':
    8.84 @@ -499,7 +518,7 @@
    8.85    from crel obtain h1 r1
    8.86      where makell: "crel (make_llist xs) h h1 r1"
    8.87      and trav: "crel (traverse r1) h1 h' r"
    8.88 -    by (auto elim!: crelE)
    8.89 +    by (auto elim!: crel_bindE)
    8.90    from make_llist[OF makell] have "list_of h1 r1 xs" ..
    8.91    from traverse [OF this] trav show ?thesis
    8.92      using crel_deterministic by fastsimp
    8.93 @@ -551,7 +570,7 @@
    8.94    case Nil
    8.95    thus ?case
    8.96      unfolding rev'_simps[of q p] list_of'_def
    8.97 -    by (auto elim!: crelE crel_lookup crel_return)
    8.98 +    by (auto elim!: crel_bindE crel_lookupE crel_returnE)
    8.99  next
   8.100    case (Cons x xs)
   8.101    (*"LinkedList.list_of h' (get_ref v h') (List.rev xs @ x # qsa)"*)
   8.102 @@ -561,7 +580,7 @@
   8.103      and list_of'_ref: "list_of' h ref xs"
   8.104      unfolding list_of'_def by (cases "Ref.get h p", auto)
   8.105    from p_is_Node Cons(2) have crel_rev': "crel (rev' (p, ref)) (Ref.set p (Node x q) h) h' v"
   8.106 -    by (auto simp add: rev'_simps [of q p] elim!: crelE crel_lookup crel_update)
   8.107 +    by (auto simp add: rev'_simps [of q p] elim!: crel_bindE crel_lookupE crel_updateE)
   8.108    from Cons(3) obtain qrs where qrs_def: "refs_of' h q qrs" by (elim list_of'_refs_of')
   8.109    from Cons(4) obtain prs where prs_def: "refs_of' h p prs" by (elim list_of'_refs_of')
   8.110    from qrs_def prs_def Cons(5) have distinct_pointers: "set qrs \<inter> set prs = {}" by fastsimp
   8.111 @@ -602,7 +621,7 @@
   8.112  proof (cases r)
   8.113    case Empty
   8.114    with list_of_h crel_rev show ?thesis
   8.115 -    by (auto simp add: list_of_Empty elim!: crel_return)
   8.116 +    by (auto simp add: list_of_Empty elim!: crel_returnE)
   8.117  next
   8.118    case (Node x ps)
   8.119    with crel_rev obtain p q h1 h2 h3 v where
   8.120 @@ -611,7 +630,7 @@
   8.121      and crel_rev':"crel (rev' (q, p)) h2 h3 v"
   8.122      and lookup: "crel (!v) h3 h' r'"
   8.123      using rev.simps
   8.124 -    by (auto elim!: crelE)
   8.125 +    by (auto elim!: crel_bindE)
   8.126    from init have a1:"list_of' h2 q []"
   8.127      unfolding list_of'_def
   8.128      by (auto elim!: crel_ref)
   8.129 @@ -622,7 +641,7 @@
   8.130    from init this Node have a2: "list_of' h2 p xs"
   8.131      apply -
   8.132      unfolding list_of'_def
   8.133 -    apply (auto elim!: crel_ref)
   8.134 +    apply (auto elim!: crel_refE)
   8.135      done
   8.136    from init have refs_of_q: "refs_of' h2 q [q]"
   8.137      by (auto elim!: crel_ref)
   8.138 @@ -633,15 +652,15 @@
   8.139      by (fastsimp elim!: crel_ref dest: refs_of'_is_fun)
   8.140    from refs_of'_invariant[OF refs_of'_ps this] have "refs_of' h2 ps refs" .
   8.141    with init have refs_of_p: "refs_of' h2 p (p#refs)"
   8.142 -    by (auto elim!: crel_ref simp add: refs_of'_def')
   8.143 +    by (auto elim!: crel_refE simp add: refs_of'_def')
   8.144    with init all_ref_present have q_is_new: "q \<notin> set (p#refs)"
   8.145 -    by (auto elim!: crel_ref intro!: Ref.noteq_I)
   8.146 +    by (auto elim!: crel_refE intro!: Ref.noteq_I)
   8.147    from refs_of_p refs_of_q q_is_new have a3: "\<forall>qrs prs. refs_of' h2 q qrs \<and> refs_of' h2 p prs \<longrightarrow> set prs \<inter> set qrs = {}"
   8.148      by (fastsimp simp only: set.simps dest: refs_of'_is_fun)
   8.149    from rev'_invariant [OF crel_rev' a1 a2 a3] have "list_of h3 (Ref.get h3 v) (List.rev xs)" 
   8.150      unfolding list_of'_def by auto
   8.151    with lookup show ?thesis
   8.152 -    by (auto elim: crel_lookup)
   8.153 +    by (auto elim: crel_lookupE)
   8.154  qed
   8.155  
   8.156  
   8.157 @@ -796,13 +815,13 @@
   8.158    case (1 ys p q)
   8.159    from 1(3-4) have "h = h' \<and> r = q"
   8.160      unfolding merge_simps[of p q]
   8.161 -    by (auto elim!: crel_lookup crelE crel_return)
   8.162 +    by (auto elim!: crel_lookupE crel_bindE crel_returnE)
   8.163    with assms(4)[OF 1(1) 1(2) 1(3)] show ?case by simp
   8.164  next
   8.165    case (2 x xs' p q pn)
   8.166    from 2(3-5) have "h = h' \<and> r = p"
   8.167      unfolding merge_simps[of p q]
   8.168 -    by (auto elim!: crel_lookup crelE crel_return)
   8.169 +    by (auto elim!: crel_lookupE crel_bindE crel_returnE)
   8.170    with assms(5)[OF 2(1-4)] show ?case by simp
   8.171  next
   8.172    case (3 x xs' y ys' p q pn qn)
   8.173 @@ -810,7 +829,7 @@
   8.174      1: "crel (merge pn q) h h1 r1" 
   8.175      and 2: "h' = Ref.set p (Node x r1) h1 \<and> r = p"
   8.176      unfolding merge_simps[of p q]
   8.177 -    by (auto elim!: crel_lookup crelE crel_return crel_if crel_update)
   8.178 +    by (auto elim!: crel_lookupE crel_bindE crel_returnE crel_ifE crel_updateE)
   8.179    from 3(6)[OF 1] assms(6) [OF 3(1-5)] 1 2 show ?case by simp
   8.180  next
   8.181    case (4 x xs' y ys' p q pn qn)
   8.182 @@ -818,7 +837,7 @@
   8.183      1: "crel (merge p qn) h h1 r1" 
   8.184      and 2: "h' = Ref.set q (Node y r1) h1 \<and> r = q"
   8.185      unfolding merge_simps[of p q]
   8.186 -    by (auto elim!: crel_lookup crelE crel_return crel_if crel_update)
   8.187 +    by (auto elim!: crel_lookupE crel_bindE crel_returnE crel_ifE crel_updateE)
   8.188    from 4(6)[OF 1] assms(7) [OF 4(1-5)] 1 2 show ?case by simp
   8.189  qed
   8.190  
     9.1 --- a/src/HOL/Imperative_HOL/ex/SatChecker.thy	Mon Jul 12 11:39:27 2010 +0200
     9.2 +++ b/src/HOL/Imperative_HOL/ex/SatChecker.thy	Mon Jul 12 16:05:08 2010 +0200
     9.3 @@ -5,7 +5,7 @@
     9.4  header {* An efficient checker for proofs from a SAT solver *}
     9.5  
     9.6  theory SatChecker
     9.7 -imports RBT_Impl Sorted_List "~~/src/HOL/Imperative_HOL/Imperative_HOL" 
     9.8 +imports RBT_Impl Sorted_List Imperative_HOL
     9.9  begin
    9.10  
    9.11  section{* General settings and functions for our representation of clauses *}
    9.12 @@ -217,12 +217,12 @@
    9.13  using assms
    9.14  proof (induct xs arbitrary: r)
    9.15    case Nil
    9.16 -  thus ?case unfolding res_mem.simps by (auto elim: crel_raise)
    9.17 +  thus ?case unfolding res_mem.simps by (auto elim: crel_raiseE)
    9.18  next
    9.19    case (Cons x xs')
    9.20    thus ?case
    9.21      unfolding res_mem.simps
    9.22 -    by (elim crel_raise crel_return crel_if crelE) auto
    9.23 +    by (elim crel_raiseE crel_returnE crel_ifE crel_bindE) auto
    9.24  qed
    9.25  
    9.26  lemma resolve1_Inv:
    9.27 @@ -233,12 +233,12 @@
    9.28    case (1 l x xs y ys r)
    9.29    thus ?case
    9.30      unfolding resolve1.simps
    9.31 -    by (elim crelE crel_if crel_return) auto
    9.32 +    by (elim crel_bindE crel_ifE crel_returnE) auto
    9.33  next
    9.34    case (2 l ys r)
    9.35    thus ?case
    9.36      unfolding resolve1.simps
    9.37 -    by (elim crel_raise) auto
    9.38 +    by (elim crel_raiseE) auto
    9.39  next
    9.40    case (3 l v va r)
    9.41    thus ?case
    9.42 @@ -254,12 +254,12 @@
    9.43    case (1 l x xs y ys r)
    9.44    thus ?case
    9.45      unfolding resolve2.simps
    9.46 -    by (elim crelE crel_if crel_return) auto
    9.47 +    by (elim crel_bindE crel_ifE crel_returnE) auto
    9.48  next
    9.49    case (2 l ys r)
    9.50    thus ?case
    9.51      unfolding resolve2.simps
    9.52 -    by (elim crel_raise) auto
    9.53 +    by (elim crel_raiseE) auto
    9.54  next
    9.55    case (3 l v va r)
    9.56    thus ?case
    9.57 @@ -312,7 +312,7 @@
    9.58    note "1.prems"
    9.59    ultimately show ?case
    9.60      unfolding res_thm'.simps
    9.61 -    apply (elim crelE crel_if crel_return)
    9.62 +    apply (elim crel_bindE crel_ifE crel_returnE)
    9.63      apply simp
    9.64      apply simp
    9.65      apply simp
    9.66 @@ -323,12 +323,12 @@
    9.67    case (2 l ys r)
    9.68    thus ?case
    9.69      unfolding res_thm'.simps
    9.70 -    by (elim crel_raise) auto
    9.71 +    by (elim crel_raiseE) auto
    9.72  next
    9.73    case (3 l v va r)
    9.74    thus ?case
    9.75      unfolding res_thm'.simps
    9.76 -    by (elim crel_raise) auto
    9.77 +    by (elim crel_raiseE) auto
    9.78  qed
    9.79  
    9.80  lemma res_mem_no_heap:
    9.81 @@ -337,9 +337,9 @@
    9.82  using assms
    9.83  apply (induct xs arbitrary: r)
    9.84  unfolding res_mem.simps
    9.85 -apply (elim crel_raise)
    9.86 +apply (elim crel_raiseE)
    9.87  apply auto
    9.88 -apply (elim crel_if crelE crel_raise crel_return)
    9.89 +apply (elim crel_ifE crel_bindE crel_raiseE crel_returnE)
    9.90  apply auto
    9.91  done
    9.92  
    9.93 @@ -349,9 +349,9 @@
    9.94  using assms
    9.95  apply (induct xs ys arbitrary: r rule: resolve1.induct)
    9.96  unfolding resolve1.simps
    9.97 -apply (elim crelE crel_if crel_return crel_raise)
    9.98 +apply (elim crel_bindE crel_ifE crel_returnE crel_raiseE)
    9.99  apply (auto simp add: res_mem_no_heap)
   9.100 -by (elim crel_raise) auto
   9.101 +by (elim crel_raiseE) auto
   9.102  
   9.103  lemma resolve2_no_heap:
   9.104  assumes "crel (resolve2 l xs ys) h h' r"
   9.105 @@ -359,9 +359,9 @@
   9.106  using assms
   9.107  apply (induct xs ys arbitrary: r rule: resolve2.induct)
   9.108  unfolding resolve2.simps
   9.109 -apply (elim crelE crel_if crel_return crel_raise)
   9.110 +apply (elim crel_bindE crel_ifE crel_returnE crel_raiseE)
   9.111  apply (auto simp add: res_mem_no_heap)
   9.112 -by (elim crel_raise) auto
   9.113 +by (elim crel_raiseE) auto
   9.114  
   9.115  
   9.116  lemma res_thm'_no_heap:
   9.117 @@ -372,18 +372,18 @@
   9.118    case (1 l x xs y ys r)
   9.119    thus ?thesis
   9.120      unfolding res_thm'.simps
   9.121 -    by (elim crelE crel_if crel_return)
   9.122 +    by (elim crel_bindE crel_ifE crel_returnE)
   9.123    (auto simp add: resolve1_no_heap resolve2_no_heap)
   9.124  next
   9.125    case (2 l ys r)
   9.126    thus ?case
   9.127      unfolding res_thm'.simps
   9.128 -    by (elim crel_raise) auto
   9.129 +    by (elim crel_raiseE) auto
   9.130  next
   9.131    case (3 l v va r)
   9.132    thus ?case
   9.133      unfolding res_thm'.simps
   9.134 -    by (elim crel_raise) auto
   9.135 +    by (elim crel_raiseE) auto
   9.136  qed
   9.137  
   9.138  
   9.139 @@ -466,7 +466,7 @@
   9.140    shows "h = h' \<and> correctClause r rs \<and> sorted rs \<and> distinct rs"
   9.141  proof -
   9.142    from res_thm have l_not_zero: "l \<noteq> 0" 
   9.143 -    by (auto elim: crel_raise)
   9.144 +    by (auto elim: crel_raiseE)
   9.145    {
   9.146      fix clj
   9.147      let ?rs = "merge (remove l cli) (remove (compl l) clj)"
   9.148 @@ -494,7 +494,7 @@
   9.149    }
   9.150    with assms show ?thesis
   9.151      unfolding res_thm2.simps get_clause_def
   9.152 -    by (elim crelE crelE' crel_if crel_nth crel_raise crel_return crel_option_case) auto
   9.153 +    by (elim crel_bindE crel_ifE crel_nthE crel_raiseE crel_returnE crel_option_case) auto
   9.154  qed
   9.155  
   9.156  lemma foldM_Inv2:
   9.157 @@ -506,7 +506,7 @@
   9.158  proof (induct rs arbitrary: h h' cli)
   9.159    case Nil thus ?case
   9.160      unfolding foldM.simps
   9.161 -    by (elim crel_return) auto
   9.162 +    by (elim crel_returnE) auto
   9.163  next
   9.164    case (Cons x xs)
   9.165    {
   9.166 @@ -523,7 +523,7 @@
   9.167    }
   9.168    with Cons show ?case
   9.169      unfolding foldM.simps
   9.170 -    by (elim crelE) auto
   9.171 +    by (elim crel_bindE) auto
   9.172  qed
   9.173  
   9.174  
   9.175 @@ -536,9 +536,9 @@
   9.176    with crel correctArray
   9.177    show ?thesis
   9.178      apply auto
   9.179 -    apply (auto simp: get_clause_def elim!: crelE crel_nth)
   9.180 -    apply (auto elim!: crelE crel_nth crel_option_case crel_raise 
   9.181 -      crel_return crel_upd)
   9.182 +    apply (auto simp: get_clause_def elim!: crel_bindE crel_nthE)
   9.183 +    apply (auto elim!: crel_bindE crel_nthE crel_option_case crel_raiseE
   9.184 +      crel_returnE crel_updE)
   9.185      apply (frule foldM_Inv2)
   9.186      apply assumption
   9.187      apply (simp add: correctArray_def)
   9.188 @@ -549,24 +549,24 @@
   9.189    case (2 a cid rcs)
   9.190    with crel correctArray
   9.191    show ?thesis
   9.192 -    by (auto simp: correctArray_def elim!: crelE crel_upd crel_return
   9.193 +    by (auto simp: correctArray_def elim!: crel_bindE crel_updE crel_returnE
   9.194       dest: array_ran_upd_array_None)
   9.195  next
   9.196    case (3 a cid c rcs)
   9.197    with crel correctArray
   9.198    show ?thesis
   9.199 -    apply (auto elim!: crelE crel_upd crel_return)
   9.200 +    apply (auto elim!: crel_bindE crel_updE crel_returnE)
   9.201      apply (auto simp: correctArray_def dest!: array_ran_upd_array_Some)
   9.202      apply (auto intro: correctClause_mono)
   9.203      by (auto simp: correctClause_def)
   9.204  next
   9.205    case 4
   9.206    with crel correctArray
   9.207 -  show ?thesis by (auto elim: crel_raise)
   9.208 +  show ?thesis by (auto elim: crel_raiseE)
   9.209  next
   9.210    case 5
   9.211    with crel correctArray
   9.212 -  show ?thesis by (auto elim: crel_raise)
   9.213 +  show ?thesis by (auto elim: crel_raiseE)
   9.214  qed
   9.215    
   9.216  
   9.217 @@ -576,13 +576,13 @@
   9.218    shows "correctArray res a h'"
   9.219  using assms
   9.220  by (induct steps arbitrary: rcs h h' res)
   9.221 - (auto elim!: crelE crel_return dest:step_correct2)
   9.222 + (auto elim!: crel_bindE crel_returnE dest:step_correct2)
   9.223  
   9.224  theorem checker_soundness:
   9.225    assumes "crel (checker n p i) h h' cs"
   9.226    shows "inconsistent cs"
   9.227  using assms unfolding checker_def
   9.228 -apply (elim crelE crel_nth crel_if crel_return crel_raise crel_new_weak)
   9.229 +apply (elim crel_bindE crel_nthE crel_ifE crel_returnE crel_raiseE crel_newE)
   9.230  prefer 2 apply simp
   9.231  apply auto
   9.232  apply (drule fold_steps_correct)