renamed slightly ambivalent crel to effect
authorhaftmann
Mon Nov 22 09:37:39 2010 +0100 (2010-11-22)
changeset 406715e46057ba8e0
parent 40630 3b5c31e55540
child 40672 abd4e7358847
renamed slightly ambivalent crel to effect
src/HOL/Imperative_HOL/Array.thy
src/HOL/Imperative_HOL/Heap_Monad.thy
src/HOL/Imperative_HOL/Mrec.thy
src/HOL/Imperative_HOL/Overview.thy
src/HOL/Imperative_HOL/Ref.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 Nov 22 09:19:34 2010 +0100
     1.2 +++ b/src/HOL/Imperative_HOL/Array.thy	Mon Nov 22 09:37:39 2010 +0100
     1.3 @@ -170,16 +170,16 @@
     1.4    "success (new n x) h"
     1.5    by (auto intro: success_intros simp add: new_def)
     1.6  
     1.7 -lemma crel_newI [crel_intros]:
     1.8 +lemma effect_newI [effect_intros]:
     1.9    assumes "(a, h') = alloc (replicate n x) h"
    1.10 -  shows "crel (new n x) h h' a"
    1.11 -  by (rule crelI) (simp add: assms execute_simps)
    1.12 +  shows "effect (new n x) h h' a"
    1.13 +  by (rule effectI) (simp add: assms execute_simps)
    1.14  
    1.15 -lemma crel_newE [crel_elims]:
    1.16 -  assumes "crel (new n x) h h' r"
    1.17 +lemma effect_newE [effect_elims]:
    1.18 +  assumes "effect (new n x) h h' r"
    1.19    obtains "r = fst (alloc (replicate n x) h)" "h' = snd (alloc (replicate n x) h)" 
    1.20      "get h' r = replicate n x" "present h' r" "\<not> present h r"
    1.21 -  using assms by (rule crelE) (simp add: get_alloc execute_simps)
    1.22 +  using assms by (rule effectE) (simp add: get_alloc execute_simps)
    1.23  
    1.24  lemma execute_of_list [execute_simps]:
    1.25    "execute (of_list xs) h = Some (alloc xs h)"
    1.26 @@ -189,16 +189,16 @@
    1.27    "success (of_list xs) h"
    1.28    by (auto intro: success_intros simp add: of_list_def)
    1.29  
    1.30 -lemma crel_of_listI [crel_intros]:
    1.31 +lemma effect_of_listI [effect_intros]:
    1.32    assumes "(a, h') = alloc xs h"
    1.33 -  shows "crel (of_list xs) h h' a"
    1.34 -  by (rule crelI) (simp add: assms execute_simps)
    1.35 +  shows "effect (of_list xs) h h' a"
    1.36 +  by (rule effectI) (simp add: assms execute_simps)
    1.37  
    1.38 -lemma crel_of_listE [crel_elims]:
    1.39 -  assumes "crel (of_list xs) h h' r"
    1.40 +lemma effect_of_listE [effect_elims]:
    1.41 +  assumes "effect (of_list xs) h h' r"
    1.42    obtains "r = fst (alloc xs h)" "h' = snd (alloc xs h)" 
    1.43      "get h' r = xs" "present h' r" "\<not> present h r"
    1.44 -  using assms by (rule crelE) (simp add: get_alloc execute_simps)
    1.45 +  using assms by (rule effectE) (simp add: get_alloc execute_simps)
    1.46  
    1.47  lemma execute_make [execute_simps]:
    1.48    "execute (make n f) h = Some (alloc (map f [0 ..< n]) h)"
    1.49 @@ -208,16 +208,16 @@
    1.50    "success (make n f) h"
    1.51    by (auto intro: success_intros simp add: make_def)
    1.52  
    1.53 -lemma crel_makeI [crel_intros]:
    1.54 +lemma effect_makeI [effect_intros]:
    1.55    assumes "(a, h') = alloc (map f [0 ..< n]) h"
    1.56 -  shows "crel (make n f) h h' a"
    1.57 -  by (rule crelI) (simp add: assms execute_simps)
    1.58 +  shows "effect (make n f) h h' a"
    1.59 +  by (rule effectI) (simp add: assms execute_simps)
    1.60  
    1.61 -lemma crel_makeE [crel_elims]:
    1.62 -  assumes "crel (make n f) h h' r"
    1.63 +lemma effect_makeE [effect_elims]:
    1.64 +  assumes "effect (make n f) h h' r"
    1.65    obtains "r = fst (alloc (map f [0 ..< n]) h)" "h' = snd (alloc (map f [0 ..< n]) h)" 
    1.66      "get h' r = map f [0 ..< n]" "present h' r" "\<not> present h r"
    1.67 -  using assms by (rule crelE) (simp add: get_alloc execute_simps)
    1.68 +  using assms by (rule effectE) (simp add: get_alloc execute_simps)
    1.69  
    1.70  lemma execute_len [execute_simps]:
    1.71    "execute (len a) h = Some (length h a, h)"
    1.72 @@ -227,15 +227,15 @@
    1.73    "success (len a) h"
    1.74    by (auto intro: success_intros simp add: len_def)
    1.75  
    1.76 -lemma crel_lengthI [crel_intros]:
    1.77 +lemma effect_lengthI [effect_intros]:
    1.78    assumes "h' = h" "r = length h a"
    1.79 -  shows "crel (len a) h h' r"
    1.80 -  by (rule crelI) (simp add: assms execute_simps)
    1.81 +  shows "effect (len a) h h' r"
    1.82 +  by (rule effectI) (simp add: assms execute_simps)
    1.83  
    1.84 -lemma crel_lengthE [crel_elims]:
    1.85 -  assumes "crel (len a) h h' r"
    1.86 +lemma effect_lengthE [effect_elims]:
    1.87 +  assumes "effect (len a) h h' r"
    1.88    obtains "r = length h' a" "h' = h" 
    1.89 -  using assms by (rule crelE) (simp add: execute_simps)
    1.90 +  using assms by (rule effectE) (simp add: execute_simps)
    1.91  
    1.92  lemma execute_nth [execute_simps]:
    1.93    "i < length h a \<Longrightarrow>
    1.94 @@ -247,15 +247,15 @@
    1.95    "i < length h a \<Longrightarrow> success (nth a i) h"
    1.96    by (auto intro: success_intros simp add: nth_def)
    1.97  
    1.98 -lemma crel_nthI [crel_intros]:
    1.99 +lemma effect_nthI [effect_intros]:
   1.100    assumes "i < length h a" "h' = h" "r = get h a ! i"
   1.101 -  shows "crel (nth a i) h h' r"
   1.102 -  by (rule crelI) (insert assms, simp add: execute_simps)
   1.103 +  shows "effect (nth a i) h h' r"
   1.104 +  by (rule effectI) (insert assms, simp add: execute_simps)
   1.105  
   1.106 -lemma crel_nthE [crel_elims]:
   1.107 -  assumes "crel (nth a i) h h' r"
   1.108 +lemma effect_nthE [effect_elims]:
   1.109 +  assumes "effect (nth a i) h h' r"
   1.110    obtains "i < length h a" "r = get h a ! i" "h' = h"
   1.111 -  using assms by (rule crelE)
   1.112 +  using assms by (rule effectE)
   1.113      (erule successE, cases "i < length h a", simp_all add: execute_simps)
   1.114  
   1.115  lemma execute_upd [execute_simps]:
   1.116 @@ -268,15 +268,15 @@
   1.117    "i < length h a \<Longrightarrow> success (upd i x a) h"
   1.118    by (auto intro: success_intros simp add: upd_def)
   1.119  
   1.120 -lemma crel_updI [crel_intros]:
   1.121 +lemma effect_updI [effect_intros]:
   1.122    assumes "i < length h a" "h' = update a i v h"
   1.123 -  shows "crel (upd i v a) h h' a"
   1.124 -  by (rule crelI) (insert assms, simp add: execute_simps)
   1.125 +  shows "effect (upd i v a) h h' a"
   1.126 +  by (rule effectI) (insert assms, simp add: execute_simps)
   1.127  
   1.128 -lemma crel_updE [crel_elims]:
   1.129 -  assumes "crel (upd i v a) h h' r"
   1.130 +lemma effect_updE [effect_elims]:
   1.131 +  assumes "effect (upd i v a) h h' r"
   1.132    obtains "r = a" "h' = update a i v h" "i < length h a"
   1.133 -  using assms by (rule crelE)
   1.134 +  using assms by (rule effectE)
   1.135      (erule successE, cases "i < length h a", simp_all add: execute_simps)
   1.136  
   1.137  lemma execute_map_entry [execute_simps]:
   1.138 @@ -290,15 +290,15 @@
   1.139    "i < length h a \<Longrightarrow> success (map_entry i f a) h"
   1.140    by (auto intro: success_intros simp add: map_entry_def)
   1.141  
   1.142 -lemma crel_map_entryI [crel_intros]:
   1.143 +lemma effect_map_entryI [effect_intros]:
   1.144    assumes "i < length h a" "h' = update a i (f (get h a ! i)) h" "r = a"
   1.145 -  shows "crel (map_entry i f a) h h' r"
   1.146 -  by (rule crelI) (insert assms, simp add: execute_simps)
   1.147 +  shows "effect (map_entry i f a) h h' r"
   1.148 +  by (rule effectI) (insert assms, simp add: execute_simps)
   1.149  
   1.150 -lemma crel_map_entryE [crel_elims]:
   1.151 -  assumes "crel (map_entry i f a) h h' r"
   1.152 +lemma effect_map_entryE [effect_elims]:
   1.153 +  assumes "effect (map_entry i f a) h h' r"
   1.154    obtains "r = a" "h' = update a i (f (get h a ! i)) h" "i < length h a"
   1.155 -  using assms by (rule crelE)
   1.156 +  using assms by (rule effectE)
   1.157      (erule successE, cases "i < length h a", simp_all add: execute_simps)
   1.158  
   1.159  lemma execute_swap [execute_simps]:
   1.160 @@ -312,15 +312,15 @@
   1.161    "i < length h a \<Longrightarrow> success (swap i x a) h"
   1.162    by (auto intro: success_intros simp add: swap_def)
   1.163  
   1.164 -lemma crel_swapI [crel_intros]:
   1.165 +lemma effect_swapI [effect_intros]:
   1.166    assumes "i < length h a" "h' = update a i x h" "r = get h a ! i"
   1.167 -  shows "crel (swap i x a) h h' r"
   1.168 -  by (rule crelI) (insert assms, simp add: execute_simps)
   1.169 +  shows "effect (swap i x a) h h' r"
   1.170 +  by (rule effectI) (insert assms, simp add: execute_simps)
   1.171  
   1.172 -lemma crel_swapE [crel_elims]:
   1.173 -  assumes "crel (swap i x a) h h' r"
   1.174 +lemma effect_swapE [effect_elims]:
   1.175 +  assumes "effect (swap i x a) h h' r"
   1.176    obtains "r = get h a ! i" "h' = update a i x h" "i < length h a"
   1.177 -  using assms by (rule crelE)
   1.178 +  using assms by (rule effectE)
   1.179      (erule successE, cases "i < length h a", simp_all add: execute_simps)
   1.180  
   1.181  lemma execute_freeze [execute_simps]:
   1.182 @@ -331,15 +331,15 @@
   1.183    "success (freeze a) h"
   1.184    by (auto intro: success_intros simp add: freeze_def)
   1.185  
   1.186 -lemma crel_freezeI [crel_intros]:
   1.187 +lemma effect_freezeI [effect_intros]:
   1.188    assumes "h' = h" "r = get h a"
   1.189 -  shows "crel (freeze a) h h' r"
   1.190 -  by (rule crelI) (insert assms, simp add: execute_simps)
   1.191 +  shows "effect (freeze a) h h' r"
   1.192 +  by (rule effectI) (insert assms, simp add: execute_simps)
   1.193  
   1.194 -lemma crel_freezeE [crel_elims]:
   1.195 -  assumes "crel (freeze a) h h' r"
   1.196 +lemma effect_freezeE [effect_elims]:
   1.197 +  assumes "effect (freeze a) h h' r"
   1.198    obtains "h' = h" "r = get h a"
   1.199 -  using assms by (rule crelE) (simp add: execute_simps)
   1.200 +  using assms by (rule effectE) (simp add: execute_simps)
   1.201  
   1.202  lemma upd_return:
   1.203    "upd i x a \<guillemotright> return a = upd i x a"
     2.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Mon Nov 22 09:19:34 2010 +0100
     2.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Mon Nov 22 09:37:39 2010 +0100
     2.3 @@ -122,25 +122,25 @@
     2.4  subsubsection {* Predicate for a simple relational calculus *}
     2.5  
     2.6  text {*
     2.7 -  The @{text crel} predicate states that when a computation @{text c}
     2.8 +  The @{text effect} predicate states that when a computation @{text c}
     2.9    runs with the heap @{text h} will result in return value @{text r}
    2.10    and a heap @{text "h'"}, i.e.~no exception occurs.
    2.11  *}  
    2.12  
    2.13 -definition crel :: "'a Heap \<Rightarrow> heap \<Rightarrow> heap \<Rightarrow> 'a \<Rightarrow> bool" where
    2.14 -  crel_def: "crel c h h' r \<longleftrightarrow> execute c h = Some (r, h')"
    2.15 +definition effect :: "'a Heap \<Rightarrow> heap \<Rightarrow> heap \<Rightarrow> 'a \<Rightarrow> bool" where
    2.16 +  effect_def: "effect c h h' r \<longleftrightarrow> execute c h = Some (r, h')"
    2.17  
    2.18 -lemma crelI:
    2.19 -  "execute c h = Some (r, h') \<Longrightarrow> crel c h h' r"
    2.20 -  by (simp add: crel_def)
    2.21 +lemma effectI:
    2.22 +  "execute c h = Some (r, h') \<Longrightarrow> effect c h h' r"
    2.23 +  by (simp add: effect_def)
    2.24  
    2.25 -lemma crelE:
    2.26 -  assumes "crel c h h' r"
    2.27 +lemma effectE:
    2.28 +  assumes "effect c h h' r"
    2.29    obtains "r = fst (the (execute c h))"
    2.30      and "h' = snd (the (execute c h))"
    2.31      and "success c h"
    2.32  proof (rule that)
    2.33 -  from assms have *: "execute c h = Some (r, h')" by (simp add: crel_def)
    2.34 +  from assms have *: "execute c h = Some (r, h')" by (simp add: effect_def)
    2.35    then show "success c h" by (simp add: success_def)
    2.36    from * have "fst (the (execute c h)) = r" and "snd (the (execute c h)) = h'"
    2.37      by simp_all
    2.38 @@ -148,84 +148,84 @@
    2.39      and "h' = snd (the (execute c h))" by simp_all
    2.40  qed
    2.41  
    2.42 -lemma crel_success:
    2.43 -  "crel c h h' r \<Longrightarrow> success c h"
    2.44 -  by (simp add: crel_def success_def)
    2.45 +lemma effect_success:
    2.46 +  "effect c h h' r \<Longrightarrow> success c h"
    2.47 +  by (simp add: effect_def success_def)
    2.48  
    2.49 -lemma success_crelE:
    2.50 +lemma success_effectE:
    2.51    assumes "success c h"
    2.52 -  obtains r h' where "crel c h h' r"
    2.53 -  using assms by (auto simp add: crel_def success_def)
    2.54 +  obtains r h' where "effect c h h' r"
    2.55 +  using assms by (auto simp add: effect_def success_def)
    2.56  
    2.57 -lemma crel_deterministic:
    2.58 -  assumes "crel f h h' a"
    2.59 -    and "crel f h h'' b"
    2.60 +lemma effect_deterministic:
    2.61 +  assumes "effect f h h' a"
    2.62 +    and "effect f h h'' b"
    2.63    shows "a = b" and "h' = h''"
    2.64 -  using assms unfolding crel_def by auto
    2.65 +  using assms unfolding effect_def by auto
    2.66  
    2.67  ML {* structure Crel_Intros = Named_Thms(
    2.68 -  val name = "crel_intros"
    2.69 -  val description = "introduction rules for crel"
    2.70 +  val name = "effect_intros"
    2.71 +  val description = "introduction rules for effect"
    2.72  ) *}
    2.73  
    2.74  ML {* structure Crel_Elims = Named_Thms(
    2.75 -  val name = "crel_elims"
    2.76 -  val description = "elimination rules for crel"
    2.77 +  val name = "effect_elims"
    2.78 +  val description = "elimination rules for effect"
    2.79  ) *}
    2.80  
    2.81  setup "Crel_Intros.setup #> Crel_Elims.setup"
    2.82  
    2.83 -lemma crel_LetI [crel_intros]:
    2.84 -  assumes "x = t" "crel (f x) h h' r"
    2.85 -  shows "crel (let x = t in f x) h h' r"
    2.86 +lemma effect_LetI [effect_intros]:
    2.87 +  assumes "x = t" "effect (f x) h h' r"
    2.88 +  shows "effect (let x = t in f x) h h' r"
    2.89    using assms by simp
    2.90  
    2.91 -lemma crel_LetE [crel_elims]:
    2.92 -  assumes "crel (let x = t in f x) h h' r"
    2.93 -  obtains "crel (f t) h h' r"
    2.94 +lemma effect_LetE [effect_elims]:
    2.95 +  assumes "effect (let x = t in f x) h h' r"
    2.96 +  obtains "effect (f t) h h' r"
    2.97    using assms by simp
    2.98  
    2.99 -lemma crel_ifI:
   2.100 -  assumes "c \<Longrightarrow> crel t h h' r"
   2.101 -    and "\<not> c \<Longrightarrow> crel e h h' r"
   2.102 -  shows "crel (if c then t else e) h h' r"
   2.103 +lemma effect_ifI:
   2.104 +  assumes "c \<Longrightarrow> effect t h h' r"
   2.105 +    and "\<not> c \<Longrightarrow> effect e h h' r"
   2.106 +  shows "effect (if c then t else e) h h' r"
   2.107    by (cases c) (simp_all add: assms)
   2.108  
   2.109 -lemma crel_ifE:
   2.110 -  assumes "crel (if c then t else e) h h' r"
   2.111 -  obtains "c" "crel t h h' r"
   2.112 -    | "\<not> c" "crel e h h' r"
   2.113 +lemma effect_ifE:
   2.114 +  assumes "effect (if c then t else e) h h' r"
   2.115 +  obtains "c" "effect t h h' r"
   2.116 +    | "\<not> c" "effect e h h' r"
   2.117    using assms by (cases c) simp_all
   2.118  
   2.119 -lemma crel_tapI [crel_intros]:
   2.120 +lemma effect_tapI [effect_intros]:
   2.121    assumes "h' = h" "r = f h"
   2.122 -  shows "crel (tap f) h h' r"
   2.123 -  by (rule crelI) (simp add: assms execute_simps)
   2.124 +  shows "effect (tap f) h h' r"
   2.125 +  by (rule effectI) (simp add: assms execute_simps)
   2.126  
   2.127 -lemma crel_tapE [crel_elims]:
   2.128 -  assumes "crel (tap f) h h' r"
   2.129 +lemma effect_tapE [effect_elims]:
   2.130 +  assumes "effect (tap f) h h' r"
   2.131    obtains "h' = h" and "r = f h"
   2.132 -  using assms by (rule crelE) (auto simp add: execute_simps)
   2.133 +  using assms by (rule effectE) (auto simp add: execute_simps)
   2.134  
   2.135 -lemma crel_heapI [crel_intros]:
   2.136 +lemma effect_heapI [effect_intros]:
   2.137    assumes "h' = snd (f h)" "r = fst (f h)"
   2.138 -  shows "crel (heap f) h h' r"
   2.139 -  by (rule crelI) (simp add: assms execute_simps)
   2.140 +  shows "effect (heap f) h h' r"
   2.141 +  by (rule effectI) (simp add: assms execute_simps)
   2.142  
   2.143 -lemma crel_heapE [crel_elims]:
   2.144 -  assumes "crel (heap f) h h' r"
   2.145 +lemma effect_heapE [effect_elims]:
   2.146 +  assumes "effect (heap f) h h' r"
   2.147    obtains "h' = snd (f h)" and "r = fst (f h)"
   2.148 -  using assms by (rule crelE) (simp add: execute_simps)
   2.149 +  using assms by (rule effectE) (simp add: execute_simps)
   2.150  
   2.151 -lemma crel_guardI [crel_intros]:
   2.152 +lemma effect_guardI [effect_intros]:
   2.153    assumes "P h" "h' = snd (f h)" "r = fst (f h)"
   2.154 -  shows "crel (guard P f) h h' r"
   2.155 -  by (rule crelI) (simp add: assms execute_simps)
   2.156 +  shows "effect (guard P f) h h' r"
   2.157 +  by (rule effectI) (simp add: assms execute_simps)
   2.158  
   2.159 -lemma crel_guardE [crel_elims]:
   2.160 -  assumes "crel (guard P f) h h' r"
   2.161 +lemma effect_guardE [effect_elims]:
   2.162 +  assumes "effect (guard P f) h h' r"
   2.163    obtains "h' = snd (f h)" "r = fst (f h)" "P h"
   2.164 -  using assms by (rule crelE)
   2.165 +  using assms by (rule effectE)
   2.166      (auto simp add: execute_simps elim!: successE, cases "P h", auto simp add: execute_simps)
   2.167  
   2.168  
   2.169 @@ -242,14 +242,14 @@
   2.170    "success (return x) h"
   2.171    by (rule successI) (simp add: execute_simps)
   2.172  
   2.173 -lemma crel_returnI [crel_intros]:
   2.174 -  "h = h' \<Longrightarrow> crel (return x) h h' x"
   2.175 -  by (rule crelI) (simp add: execute_simps)
   2.176 +lemma effect_returnI [effect_intros]:
   2.177 +  "h = h' \<Longrightarrow> effect (return x) h h' x"
   2.178 +  by (rule effectI) (simp add: execute_simps)
   2.179  
   2.180 -lemma crel_returnE [crel_elims]:
   2.181 -  assumes "crel (return x) h h' r"
   2.182 +lemma effect_returnE [effect_elims]:
   2.183 +  assumes "effect (return x) h h' r"
   2.184    obtains "r = x" "h' = h"
   2.185 -  using assms by (rule crelE) (simp add: execute_simps)
   2.186 +  using assms by (rule effectE) (simp add: execute_simps)
   2.187  
   2.188  definition raise :: "string \<Rightarrow> 'a Heap" where -- {* the string is just decoration *}
   2.189    [code del]: "raise s = Heap (\<lambda>_. None)"
   2.190 @@ -258,10 +258,10 @@
   2.191    "execute (raise s) = (\<lambda>_. None)"
   2.192    by (simp add: raise_def)
   2.193  
   2.194 -lemma crel_raiseE [crel_elims]:
   2.195 -  assumes "crel (raise x) h h' r"
   2.196 +lemma effect_raiseE [effect_elims]:
   2.197 +  assumes "effect (raise x) h h' r"
   2.198    obtains "False"
   2.199 -  using assms by (rule crelE) (simp add: success_def execute_simps)
   2.200 +  using assms by (rule effectE) (simp add: success_def execute_simps)
   2.201  
   2.202  definition bind :: "'a Heap \<Rightarrow> ('a \<Rightarrow> 'b Heap) \<Rightarrow> 'b Heap" where
   2.203    [code del]: "bind f g = Heap (\<lambda>h. case execute f h of
   2.204 @@ -291,22 +291,22 @@
   2.205    "execute f h = Some (x, h') \<Longrightarrow> success (g x) h' \<Longrightarrow> success (f \<guillemotright>= g) h"
   2.206    by (auto intro!: successI elim!: successE simp add: bind_def)
   2.207  
   2.208 -lemma success_bind_crelI [success_intros]:
   2.209 -  "crel f h h' x \<Longrightarrow> success (g x) h' \<Longrightarrow> success (f \<guillemotright>= g) h"
   2.210 -  by (auto simp add: crel_def success_def bind_def)
   2.211 +lemma success_bind_effectI [success_intros]:
   2.212 +  "effect f h h' x \<Longrightarrow> success (g x) h' \<Longrightarrow> success (f \<guillemotright>= g) h"
   2.213 +  by (auto simp add: effect_def success_def bind_def)
   2.214  
   2.215 -lemma crel_bindI [crel_intros]:
   2.216 -  assumes "crel f h h' r" "crel (g r) h' h'' r'"
   2.217 -  shows "crel (f \<guillemotright>= g) h h'' r'"
   2.218 +lemma effect_bindI [effect_intros]:
   2.219 +  assumes "effect f h h' r" "effect (g r) h' h'' r'"
   2.220 +  shows "effect (f \<guillemotright>= g) h h'' r'"
   2.221    using assms
   2.222 -  apply (auto intro!: crelI elim!: crelE successE)
   2.223 +  apply (auto intro!: effectI elim!: effectE successE)
   2.224    apply (subst execute_bind, simp_all)
   2.225    done
   2.226  
   2.227 -lemma crel_bindE [crel_elims]:
   2.228 -  assumes "crel (f \<guillemotright>= g) h h'' r'"
   2.229 -  obtains h' r where "crel f h h' r" "crel (g r) h' h'' r'"
   2.230 -  using assms by (auto simp add: crel_def bind_def split: option.split_asm)
   2.231 +lemma effect_bindE [effect_elims]:
   2.232 +  assumes "effect (f \<guillemotright>= g) h h'' r'"
   2.233 +  obtains h' r where "effect f h h' r" "effect (g r) h' h'' r'"
   2.234 +  using assms by (auto simp add: effect_def bind_def split: option.split_asm)
   2.235  
   2.236  lemma execute_bind_eq_SomeI:
   2.237    assumes "execute f h = Some (x, h')"
   2.238 @@ -343,14 +343,14 @@
   2.239    "P x \<Longrightarrow> success (assert P x) h"
   2.240    by (rule successI) (simp add: execute_assert)
   2.241  
   2.242 -lemma crel_assertI [crel_intros]:
   2.243 -  "P x \<Longrightarrow> h' = h \<Longrightarrow> r = x \<Longrightarrow> crel (assert P x) h h' r"
   2.244 -  by (rule crelI) (simp add: execute_assert)
   2.245 +lemma effect_assertI [effect_intros]:
   2.246 +  "P x \<Longrightarrow> h' = h \<Longrightarrow> r = x \<Longrightarrow> effect (assert P x) h h' r"
   2.247 +  by (rule effectI) (simp add: execute_assert)
   2.248   
   2.249 -lemma crel_assertE [crel_elims]:
   2.250 -  assumes "crel (assert P x) h h' r"
   2.251 +lemma effect_assertE [effect_elims]:
   2.252 +  assumes "effect (assert P x) h h' r"
   2.253    obtains "P x" "r = x" "h' = h"
   2.254 -  using assms by (rule crelE) (cases "P x", simp_all add: execute_assert success_def)
   2.255 +  using assms by (rule effectE) (cases "P x", simp_all add: execute_assert success_def)
   2.256  
   2.257  lemma assert_cong [fundef_cong]:
   2.258    assumes "P = P'"
     3.1 --- a/src/HOL/Imperative_HOL/Mrec.thy	Mon Nov 22 09:19:34 2010 +0100
     3.2 +++ b/src/HOL/Imperative_HOL/Mrec.thy	Mon Nov 22 09:37:39 2010 +0100
     3.3 @@ -145,20 +145,20 @@
     3.4  lemmas MREC_pinduct = mrec.MREC_pinduct
     3.5  
     3.6  lemma MREC_induct:
     3.7 -  assumes "crel (MREC f g x) h h' r"
     3.8 -  assumes "\<And> x h h' r. crel (f x) h h' (Inl r) \<Longrightarrow> P x h h' r"
     3.9 -  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
    3.10 -    \<Longrightarrow> crel (g x s z) h2 h' r \<Longrightarrow> P x h h' r"
    3.11 +  assumes "effect (MREC f g x) h h' r"
    3.12 +  assumes "\<And> x h h' r. effect (f x) h h' (Inl r) \<Longrightarrow> P x h h' r"
    3.13 +  assumes "\<And> x h h1 h2 h' s z r. effect (f x) h h1 (Inr s) \<Longrightarrow> effect (MREC f g s) h1 h2 z \<Longrightarrow> P s h1 h2 z
    3.14 +    \<Longrightarrow> effect (g x s z) h2 h' r \<Longrightarrow> P x h h' r"
    3.15    shows "P x h h' r"
    3.16 -proof (rule MREC_pinduct[OF assms(1) [unfolded crel_def]])
    3.17 +proof (rule MREC_pinduct[OF assms(1) [unfolded effect_def]])
    3.18    fix x h h1 h2 h' s z r
    3.19    assume "Heap_Monad.execute (f x) h = Some (Inr s, h1)"
    3.20      "Heap_Monad.execute (MREC f g s) h1 = Some (z, h2)"
    3.21      "P s h1 h2 z"
    3.22      "Heap_Monad.execute (g x s z) h2 = Some (r, h')"
    3.23 -  from assms(3) [unfolded crel_def, OF this(1) this(2) this(3) this(4)]
    3.24 +  from assms(3) [unfolded effect_def, OF this(1) this(2) this(3) this(4)]
    3.25    show "P x h h' r" .
    3.26  next
    3.27 -qed (auto simp add: assms(2)[unfolded crel_def])
    3.28 +qed (auto simp add: assms(2)[unfolded effect_def])
    3.29  
    3.30  end
     4.1 --- a/src/HOL/Imperative_HOL/Overview.thy	Mon Nov 22 09:19:34 2010 +0100
     4.2 +++ b/src/HOL/Imperative_HOL/Overview.thy	Mon Nov 22 09:37:39 2010 +0100
     4.3 @@ -96,13 +96,13 @@
     4.4    To establish correctness of imperative programs, predicate
     4.5  
     4.6    \begin{quote}
     4.7 -    @{term_type crel}
     4.8 +    @{term_type effect}
     4.9    \end{quote}
    4.10  
    4.11    provides a simple relational calculus.  Primitive rules are @{text
    4.12 -  crelI} and @{text crelE}, rules appropriate for reasoning about
    4.13 -  imperative operations are available in the @{text crel_intros} and
    4.14 -  @{text crel_elims} fact collections.
    4.15 +  effectI} and @{text effectE}, rules appropriate for reasoning about
    4.16 +  imperative operations are available in the @{text effect_intros} and
    4.17 +  @{text effect_elims} fact collections.
    4.18  
    4.19    Often non-failure of imperative computations does not depend
    4.20    on the heap at all;  reasoning then can be easier using predicate
    4.21 @@ -114,10 +114,10 @@
    4.22    Introduction rules for @{const success} are available in the
    4.23    @{text success_intro} fact collection.
    4.24  
    4.25 -  @{const execute}, @{const crel}, @{const success} and @{const bind}
    4.26 +  @{const execute}, @{const effect}, @{const success} and @{const bind}
    4.27    are related by rules @{text execute_bind_success}, @{text
    4.28 -  success_bind_executeI}, @{text success_bind_crelI}, @{text
    4.29 -  crel_bindI}, @{text crel_bindE} and @{text execute_bind_eq_SomeI}.
    4.30 +  success_bind_executeI}, @{text success_bind_effectI}, @{text
    4.31 +  effect_bindI}, @{text effect_bindE} and @{text execute_bind_eq_SomeI}.
    4.32  *}
    4.33  
    4.34  
    4.35 @@ -235,7 +235,7 @@
    4.36        
    4.37      \item Whether one should prefer equational reasoning (fact
    4.38        collection @{text execute_simps} or relational reasoning (fact
    4.39 -      collections @{text crel_intros} and @{text crel_elims}) depends
    4.40 +      collections @{text effect_intros} and @{text effect_elims}) depends
    4.41        on the problems to solve.  For complex expressions or
    4.42        expressions involving binders, the relation style usually is
    4.43        superior but requires more proof text.
     5.1 --- a/src/HOL/Imperative_HOL/Ref.thy	Mon Nov 22 09:19:34 2010 +0100
     5.2 +++ b/src/HOL/Imperative_HOL/Ref.thy	Mon Nov 22 09:37:39 2010 +0100
     5.3 @@ -143,15 +143,15 @@
     5.4    "success (ref v) h"
     5.5    by (auto intro: success_intros simp add: ref_def)
     5.6  
     5.7 -lemma crel_refI [crel_intros]:
     5.8 +lemma effect_refI [effect_intros]:
     5.9    assumes "(r, h') = alloc v h"
    5.10 -  shows "crel (ref v) h h' r"
    5.11 -  by (rule crelI) (insert assms, simp add: execute_simps)
    5.12 +  shows "effect (ref v) h h' r"
    5.13 +  by (rule effectI) (insert assms, simp add: execute_simps)
    5.14  
    5.15 -lemma crel_refE [crel_elims]:
    5.16 -  assumes "crel (ref v) h h' r"
    5.17 +lemma effect_refE [effect_elims]:
    5.18 +  assumes "effect (ref v) h h' r"
    5.19    obtains "get h' r = v" and "present h' r" and "\<not> present h r"
    5.20 -  using assms by (rule crelE) (simp add: execute_simps)
    5.21 +  using assms by (rule effectE) (simp add: execute_simps)
    5.22  
    5.23  lemma execute_lookup [execute_simps]:
    5.24    "Heap_Monad.execute (lookup r) h = Some (get h r, h)"
    5.25 @@ -161,15 +161,15 @@
    5.26    "success (lookup r) h"
    5.27    by (auto intro: success_intros  simp add: lookup_def)
    5.28  
    5.29 -lemma crel_lookupI [crel_intros]:
    5.30 +lemma effect_lookupI [effect_intros]:
    5.31    assumes "h' = h" "x = get h r"
    5.32 -  shows "crel (!r) h h' x"
    5.33 -  by (rule crelI) (insert assms, simp add: execute_simps)
    5.34 +  shows "effect (!r) h h' x"
    5.35 +  by (rule effectI) (insert assms, simp add: execute_simps)
    5.36  
    5.37 -lemma crel_lookupE [crel_elims]:
    5.38 -  assumes "crel (!r) h h' x"
    5.39 +lemma effect_lookupE [effect_elims]:
    5.40 +  assumes "effect (!r) h h' x"
    5.41    obtains "h' = h" "x = get h r"
    5.42 -  using assms by (rule crelE) (simp add: execute_simps)
    5.43 +  using assms by (rule effectE) (simp add: execute_simps)
    5.44  
    5.45  lemma execute_update [execute_simps]:
    5.46    "Heap_Monad.execute (update r v) h = Some ((), set r v h)"
    5.47 @@ -179,15 +179,15 @@
    5.48    "success (update r v) h"
    5.49    by (auto intro: success_intros  simp add: update_def)
    5.50  
    5.51 -lemma crel_updateI [crel_intros]:
    5.52 +lemma effect_updateI [effect_intros]:
    5.53    assumes "h' = set r v h"
    5.54 -  shows "crel (r := v) h h' x"
    5.55 -  by (rule crelI) (insert assms, simp add: execute_simps)
    5.56 +  shows "effect (r := v) h h' x"
    5.57 +  by (rule effectI) (insert assms, simp add: execute_simps)
    5.58  
    5.59 -lemma crel_updateE [crel_elims]:
    5.60 -  assumes "crel (r' := v) h h' r"
    5.61 +lemma effect_updateE [effect_elims]:
    5.62 +  assumes "effect (r' := v) h h' r"
    5.63    obtains "h' = set r' v h"
    5.64 -  using assms by (rule crelE) (simp add: execute_simps)
    5.65 +  using assms by (rule effectE) (simp add: execute_simps)
    5.66  
    5.67  lemma execute_change [execute_simps]:
    5.68    "Heap_Monad.execute (change f r) h = Some (f (get h r), set r (f (get h r)) h)"
    5.69 @@ -195,17 +195,17 @@
    5.70  
    5.71  lemma success_changeI [success_intros]:
    5.72    "success (change f r) h"
    5.73 -  by (auto intro!: success_intros crel_intros simp add: change_def)
    5.74 +  by (auto intro!: success_intros effect_intros simp add: change_def)
    5.75  
    5.76 -lemma crel_changeI [crel_intros]: 
    5.77 +lemma effect_changeI [effect_intros]: 
    5.78    assumes "h' = set r (f (get h r)) h" "x = f (get h r)"
    5.79 -  shows "crel (change f r) h h' x"
    5.80 -  by (rule crelI) (insert assms, simp add: execute_simps)  
    5.81 +  shows "effect (change f r) h h' x"
    5.82 +  by (rule effectI) (insert assms, simp add: execute_simps)  
    5.83  
    5.84 -lemma crel_changeE [crel_elims]:
    5.85 -  assumes "crel (change f r') h h' r"
    5.86 +lemma effect_changeE [effect_elims]:
    5.87 +  assumes "effect (change f r') h h' r"
    5.88    obtains "h' = set r' (f (get h r')) h" "r = f (get h r')"
    5.89 -  using assms by (rule crelE) (simp add: execute_simps)
    5.90 +  using assms by (rule effectE) (simp add: execute_simps)
    5.91  
    5.92  lemma lookup_chain:
    5.93    "(!r \<guillemotright> f) = f"
     6.1 --- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Mon Nov 22 09:19:34 2010 +0100
     6.2 +++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Mon Nov 22 09:37:39 2010 +0100
     6.3 @@ -21,20 +21,20 @@
     6.4         return ()
     6.5       }"
     6.6  
     6.7 -lemma crel_swapI [crel_intros]:
     6.8 +lemma effect_swapI [effect_intros]:
     6.9    assumes "i < Array.length h a" "j < Array.length h a"
    6.10      "x = Array.get h a ! i" "y = Array.get h a ! j"
    6.11      "h' = Array.update a j x (Array.update a i y h)"
    6.12 -  shows "crel (swap a i j) h h' r"
    6.13 -  unfolding swap_def using assms by (auto intro!: crel_intros)
    6.14 +  shows "effect (swap a i j) h h' r"
    6.15 +  unfolding swap_def using assms by (auto intro!: effect_intros)
    6.16  
    6.17  lemma swap_permutes:
    6.18 -  assumes "crel (swap a i j) h h' rs"
    6.19 +  assumes "effect (swap a i j) h h' rs"
    6.20    shows "multiset_of (Array.get h' a) 
    6.21    = multiset_of (Array.get h a)"
    6.22    using assms
    6.23    unfolding swap_def
    6.24 -  by (auto simp add: Array.length_def multiset_of_swap dest: sym [of _ "h'"] elim!: crel_bindE crel_nthE crel_returnE crel_updE)
    6.25 +  by (auto simp add: Array.length_def multiset_of_swap dest: sym [of _ "h'"] elim!: effect_bindE effect_nthE effect_returnE effect_updE)
    6.26  
    6.27  function part1 :: "nat array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat Heap"
    6.28  where
    6.29 @@ -54,7 +54,7 @@
    6.30  declare part1.simps[simp del]
    6.31  
    6.32  lemma part_permutes:
    6.33 -  assumes "crel (part1 a l r p) h h' rs"
    6.34 +  assumes "effect (part1 a l r p) h h' rs"
    6.35    shows "multiset_of (Array.get h' a) 
    6.36    = multiset_of (Array.get h a)"
    6.37    using assms
    6.38 @@ -62,23 +62,23 @@
    6.39    case (1 a l r p h h' rs)
    6.40    thus ?case
    6.41      unfolding part1.simps [of a l r p]
    6.42 -    by (elim crel_bindE crel_ifE crel_returnE crel_nthE) (auto simp add: swap_permutes)
    6.43 +    by (elim effect_bindE effect_ifE effect_returnE effect_nthE) (auto simp add: swap_permutes)
    6.44  qed
    6.45  
    6.46  lemma part_returns_index_in_bounds:
    6.47 -  assumes "crel (part1 a l r p) h h' rs"
    6.48 +  assumes "effect (part1 a l r p) h h' rs"
    6.49    assumes "l \<le> r"
    6.50    shows "l \<le> rs \<and> rs \<le> r"
    6.51  using assms
    6.52  proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
    6.53    case (1 a l r p h h' rs)
    6.54 -  note cr = `crel (part1 a l r p) h h' rs`
    6.55 +  note cr = `effect (part1 a l r p) h h' rs`
    6.56    show ?case
    6.57    proof (cases "r \<le> l")
    6.58      case True (* Terminating case *)
    6.59      with cr `l \<le> r` show ?thesis
    6.60        unfolding part1.simps[of a l r p]
    6.61 -      by (elim crel_bindE crel_ifE crel_returnE crel_nthE) auto
    6.62 +      by (elim effect_bindE effect_ifE effect_returnE effect_nthE) auto
    6.63    next
    6.64      case False (* recursive case *)
    6.65      note rec_condition = this
    6.66 @@ -87,19 +87,19 @@
    6.67      proof (cases "?v \<le> p")
    6.68        case True
    6.69        with cr False
    6.70 -      have rec1: "crel (part1 a (l + 1) r p) h h' rs"
    6.71 +      have rec1: "effect (part1 a (l + 1) r p) h h' rs"
    6.72          unfolding part1.simps[of a l r p]
    6.73 -        by (elim crel_bindE crel_nthE crel_ifE crel_returnE) auto
    6.74 +        by (elim effect_bindE effect_nthE effect_ifE effect_returnE) auto
    6.75        from rec_condition have "l + 1 \<le> r" by arith
    6.76        from 1(1)[OF rec_condition True rec1 `l + 1 \<le> r`]
    6.77        show ?thesis by simp
    6.78      next
    6.79        case False
    6.80        with rec_condition cr
    6.81 -      obtain h1 where swp: "crel (swap a l r) h h1 ()"
    6.82 -        and rec2: "crel (part1 a l (r - 1) p) h1 h' rs"
    6.83 +      obtain h1 where swp: "effect (swap a l r) h h1 ()"
    6.84 +        and rec2: "effect (part1 a l (r - 1) p) h1 h' rs"
    6.85          unfolding part1.simps[of a l r p]
    6.86 -        by (elim crel_bindE crel_nthE crel_ifE crel_returnE) auto
    6.87 +        by (elim effect_bindE effect_nthE effect_ifE effect_returnE) auto
    6.88        from rec_condition have "l \<le> r - 1" by arith
    6.89        from 1(2) [OF rec_condition False rec2 `l \<le> r - 1`] show ?thesis by fastsimp
    6.90      qed
    6.91 @@ -107,41 +107,41 @@
    6.92  qed
    6.93  
    6.94  lemma part_length_remains:
    6.95 -  assumes "crel (part1 a l r p) h h' rs"
    6.96 +  assumes "effect (part1 a l r p) h h' rs"
    6.97    shows "Array.length h a = Array.length h' a"
    6.98  using assms
    6.99  proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
   6.100    case (1 a l r p h h' rs)
   6.101 -  note cr = `crel (part1 a l r p) h h' rs`
   6.102 +  note cr = `effect (part1 a l r p) h h' rs`
   6.103    
   6.104    show ?case
   6.105    proof (cases "r \<le> l")
   6.106      case True (* Terminating case *)
   6.107      with cr show ?thesis
   6.108        unfolding part1.simps[of a l r p]
   6.109 -      by (elim crel_bindE crel_ifE crel_returnE crel_nthE) auto
   6.110 +      by (elim effect_bindE effect_ifE effect_returnE effect_nthE) auto
   6.111    next
   6.112      case False (* recursive case *)
   6.113      with cr 1 show ?thesis
   6.114        unfolding part1.simps [of a l r p] swap_def
   6.115 -      by (auto elim!: crel_bindE crel_ifE crel_nthE crel_returnE crel_updE) fastsimp
   6.116 +      by (auto elim!: effect_bindE effect_ifE effect_nthE effect_returnE effect_updE) fastsimp
   6.117    qed
   6.118  qed
   6.119  
   6.120  lemma part_outer_remains:
   6.121 -  assumes "crel (part1 a l r p) h h' rs"
   6.122 +  assumes "effect (part1 a l r p) h h' rs"
   6.123    shows "\<forall>i. i < l \<or> r < i \<longrightarrow> Array.get h (a::nat array) ! i = Array.get h' a ! i"
   6.124    using assms
   6.125  proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
   6.126    case (1 a l r p h h' rs)
   6.127 -  note cr = `crel (part1 a l r p) h h' rs`
   6.128 +  note cr = `effect (part1 a l r p) h h' rs`
   6.129    
   6.130    show ?case
   6.131    proof (cases "r \<le> l")
   6.132      case True (* Terminating case *)
   6.133      with cr show ?thesis
   6.134        unfolding part1.simps[of a l r p]
   6.135 -      by (elim crel_bindE crel_ifE crel_returnE crel_nthE) auto
   6.136 +      by (elim effect_bindE effect_ifE effect_returnE effect_nthE) auto
   6.137    next
   6.138      case False (* recursive case *)
   6.139      note rec_condition = this
   6.140 @@ -150,22 +150,22 @@
   6.141      proof (cases "?v \<le> p")
   6.142        case True
   6.143        with cr False
   6.144 -      have rec1: "crel (part1 a (l + 1) r p) h h' rs"
   6.145 +      have rec1: "effect (part1 a (l + 1) r p) h h' rs"
   6.146          unfolding part1.simps[of a l r p]
   6.147 -        by (elim crel_bindE crel_nthE crel_ifE crel_returnE) auto
   6.148 +        by (elim effect_bindE effect_nthE effect_ifE effect_returnE) auto
   6.149        from 1(1)[OF rec_condition True rec1]
   6.150        show ?thesis by fastsimp
   6.151      next
   6.152        case False
   6.153        with rec_condition cr
   6.154 -      obtain h1 where swp: "crel (swap a l r) h h1 ()"
   6.155 -        and rec2: "crel (part1 a l (r - 1) p) h1 h' rs"
   6.156 +      obtain h1 where swp: "effect (swap a l r) h h1 ()"
   6.157 +        and rec2: "effect (part1 a l (r - 1) p) h1 h' rs"
   6.158          unfolding part1.simps[of a l r p]
   6.159 -        by (elim crel_bindE crel_nthE crel_ifE crel_returnE) auto
   6.160 +        by (elim effect_bindE effect_nthE effect_ifE effect_returnE) auto
   6.161        from swp rec_condition have
   6.162          "\<forall>i. i < l \<or> r < i \<longrightarrow> Array.get h a ! i = Array.get h1 a ! i"
   6.163          unfolding swap_def
   6.164 -        by (elim crel_bindE crel_nthE crel_updE crel_returnE) auto
   6.165 +        by (elim effect_bindE effect_nthE effect_updE effect_returnE) auto
   6.166        with 1(2) [OF rec_condition False rec2] show ?thesis by fastsimp
   6.167      qed
   6.168    qed
   6.169 @@ -173,20 +173,20 @@
   6.170  
   6.171  
   6.172  lemma part_partitions:
   6.173 -  assumes "crel (part1 a l r p) h h' rs"
   6.174 +  assumes "effect (part1 a l r p) h h' rs"
   6.175    shows "(\<forall>i. l \<le> i \<and> i < rs \<longrightarrow> Array.get h' (a::nat array) ! i \<le> p)
   6.176    \<and> (\<forall>i. rs < i \<and> i \<le> r \<longrightarrow> Array.get h' a ! i \<ge> p)"
   6.177    using assms
   6.178  proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
   6.179    case (1 a l r p h h' rs)
   6.180 -  note cr = `crel (part1 a l r p) h h' rs`
   6.181 +  note cr = `effect (part1 a l r p) h h' rs`
   6.182    
   6.183    show ?case
   6.184    proof (cases "r \<le> l")
   6.185      case True (* Terminating case *)
   6.186      with cr have "rs = r"
   6.187        unfolding part1.simps[of a l r p]
   6.188 -      by (elim crel_bindE crel_ifE crel_returnE crel_nthE) auto
   6.189 +      by (elim effect_bindE effect_ifE effect_returnE effect_nthE) auto
   6.190      with True
   6.191      show ?thesis by auto
   6.192    next
   6.193 @@ -197,9 +197,9 @@
   6.194      proof (cases "?v \<le> p")
   6.195        case True
   6.196        with lr cr
   6.197 -      have rec1: "crel (part1 a (l + 1) r p) h h' rs"
   6.198 +      have rec1: "effect (part1 a (l + 1) r p) h h' rs"
   6.199          unfolding part1.simps[of a l r p]
   6.200 -        by (elim crel_bindE crel_nthE crel_ifE crel_returnE) auto
   6.201 +        by (elim effect_bindE effect_nthE effect_ifE effect_returnE) auto
   6.202        from True part_outer_remains[OF rec1] have a_l: "Array.get h' a ! l \<le> p"
   6.203          by fastsimp
   6.204        have "\<forall>i. (l \<le> i = (l = i \<or> Suc l \<le> i))" by arith
   6.205 @@ -208,13 +208,13 @@
   6.206      next
   6.207        case False
   6.208        with lr cr
   6.209 -      obtain h1 where swp: "crel (swap a l r) h h1 ()"
   6.210 -        and rec2: "crel (part1 a l (r - 1) p) h1 h' rs"
   6.211 +      obtain h1 where swp: "effect (swap a l r) h h1 ()"
   6.212 +        and rec2: "effect (part1 a l (r - 1) p) h1 h' rs"
   6.213          unfolding part1.simps[of a l r p]
   6.214 -        by (elim crel_bindE crel_nthE crel_ifE crel_returnE) auto
   6.215 +        by (elim effect_bindE effect_nthE effect_ifE effect_returnE) auto
   6.216        from swp False have "Array.get h1 a ! r \<ge> p"
   6.217          unfolding swap_def
   6.218 -        by (auto simp add: Array.length_def elim!: crel_bindE crel_nthE crel_updE crel_returnE)
   6.219 +        by (auto simp add: Array.length_def elim!: effect_bindE effect_nthE effect_updE effect_returnE)
   6.220        with part_outer_remains [OF rec2] lr have a_r: "Array.get h' a ! r \<ge> p"
   6.221          by fastsimp
   6.222        have "\<forall>i. (i \<le> r = (i = r \<or> i \<le> r - 1))" by arith
   6.223 @@ -239,70 +239,70 @@
   6.224  declare partition.simps[simp del]
   6.225  
   6.226  lemma partition_permutes:
   6.227 -  assumes "crel (partition a l r) h h' rs"
   6.228 +  assumes "effect (partition a l r) h h' rs"
   6.229    shows "multiset_of (Array.get h' a) 
   6.230    = multiset_of (Array.get h a)"
   6.231  proof -
   6.232      from assms part_permutes swap_permutes show ?thesis
   6.233        unfolding partition.simps
   6.234 -      by (elim crel_bindE crel_returnE crel_nthE crel_ifE crel_updE) auto
   6.235 +      by (elim effect_bindE effect_returnE effect_nthE effect_ifE effect_updE) auto
   6.236  qed
   6.237  
   6.238  lemma partition_length_remains:
   6.239 -  assumes "crel (partition a l r) h h' rs"
   6.240 +  assumes "effect (partition a l r) h h' rs"
   6.241    shows "Array.length h a = Array.length h' a"
   6.242  proof -
   6.243    from assms part_length_remains show ?thesis
   6.244      unfolding partition.simps swap_def
   6.245 -    by (elim crel_bindE crel_returnE crel_nthE crel_ifE crel_updE) auto
   6.246 +    by (elim effect_bindE effect_returnE effect_nthE effect_ifE effect_updE) auto
   6.247  qed
   6.248  
   6.249  lemma partition_outer_remains:
   6.250 -  assumes "crel (partition a l r) h h' rs"
   6.251 +  assumes "effect (partition a l r) h h' rs"
   6.252    assumes "l < r"
   6.253    shows "\<forall>i. i < l \<or> r < i \<longrightarrow> Array.get h (a::nat array) ! i = Array.get h' a ! i"
   6.254  proof -
   6.255    from assms part_outer_remains part_returns_index_in_bounds show ?thesis
   6.256      unfolding partition.simps swap_def
   6.257 -    by (elim crel_bindE crel_returnE crel_nthE crel_ifE crel_updE) fastsimp
   6.258 +    by (elim effect_bindE effect_returnE effect_nthE effect_ifE effect_updE) fastsimp
   6.259  qed
   6.260  
   6.261  lemma partition_returns_index_in_bounds:
   6.262 -  assumes crel: "crel (partition a l r) h h' rs"
   6.263 +  assumes effect: "effect (partition a l r) h h' rs"
   6.264    assumes "l < r"
   6.265    shows "l \<le> rs \<and> rs \<le> r"
   6.266  proof -
   6.267 -  from crel obtain middle h'' p where part: "crel (part1 a l (r - 1) p) h h'' middle"
   6.268 +  from effect obtain middle h'' p where part: "effect (part1 a l (r - 1) p) h h'' middle"
   6.269      and rs_equals: "rs = (if Array.get h'' a ! middle \<le> Array.get h a ! r then middle + 1
   6.270           else middle)"
   6.271      unfolding partition.simps
   6.272 -    by (elim crel_bindE crel_returnE crel_nthE crel_ifE crel_updE) simp 
   6.273 +    by (elim effect_bindE effect_returnE effect_nthE effect_ifE effect_updE) simp 
   6.274    from `l < r` have "l \<le> r - 1" by arith
   6.275    from part_returns_index_in_bounds[OF part this] rs_equals `l < r` show ?thesis by auto
   6.276  qed
   6.277  
   6.278  lemma partition_partitions:
   6.279 -  assumes crel: "crel (partition a l r) h h' rs"
   6.280 +  assumes effect: "effect (partition a l r) h h' rs"
   6.281    assumes "l < r"
   6.282    shows "(\<forall>i. l \<le> i \<and> i < rs \<longrightarrow> Array.get h' (a::nat array) ! i \<le> Array.get h' a ! rs) \<and>
   6.283    (\<forall>i. rs < i \<and> i \<le> r \<longrightarrow> Array.get h' a ! rs \<le> Array.get h' a ! i)"
   6.284  proof -
   6.285    let ?pivot = "Array.get h a ! r" 
   6.286 -  from crel obtain middle h1 where part: "crel (part1 a l (r - 1) ?pivot) h h1 middle"
   6.287 -    and swap: "crel (swap a rs r) h1 h' ()"
   6.288 +  from effect obtain middle h1 where part: "effect (part1 a l (r - 1) ?pivot) h h1 middle"
   6.289 +    and swap: "effect (swap a rs r) h1 h' ()"
   6.290      and rs_equals: "rs = (if Array.get h1 a ! middle \<le> ?pivot then middle + 1
   6.291           else middle)"
   6.292      unfolding partition.simps
   6.293 -    by (elim crel_bindE crel_returnE crel_nthE crel_ifE crel_updE) simp
   6.294 +    by (elim effect_bindE effect_returnE effect_nthE effect_ifE effect_updE) simp
   6.295    from swap have h'_def: "h' = Array.update a r (Array.get h1 a ! rs)
   6.296      (Array.update a rs (Array.get h1 a ! r) h1)"
   6.297      unfolding swap_def
   6.298 -    by (elim crel_bindE crel_returnE crel_nthE crel_updE) simp
   6.299 +    by (elim effect_bindE effect_returnE effect_nthE effect_updE) simp
   6.300    from swap have in_bounds: "r < Array.length h1 a \<and> rs < Array.length h1 a"
   6.301      unfolding swap_def
   6.302 -    by (elim crel_bindE crel_returnE crel_nthE crel_updE) simp
   6.303 +    by (elim effect_bindE effect_returnE effect_nthE effect_updE) simp
   6.304    from swap have swap_length_remains: "Array.length h1 a = Array.length h' a"
   6.305 -    unfolding swap_def by (elim crel_bindE crel_returnE crel_nthE crel_updE) auto
   6.306 +    unfolding swap_def by (elim effect_bindE effect_returnE effect_nthE effect_updE) auto
   6.307    from `l < r` have "l \<le> r - 1" by simp
   6.308    note middle_in_bounds = part_returns_index_in_bounds[OF part this]
   6.309    from part_outer_remains[OF part] `l < r`
   6.310 @@ -311,7 +311,7 @@
   6.311    with swap
   6.312    have right_remains: "Array.get h a ! r = Array.get h' a ! rs"
   6.313      unfolding swap_def
   6.314 -    by (auto simp add: Array.length_def elim!: crel_bindE crel_returnE crel_nthE crel_updE) (cases "r = rs", auto)
   6.315 +    by (auto simp add: Array.length_def elim!: effect_bindE effect_returnE effect_nthE effect_updE) (cases "r = rs", auto)
   6.316    from part_partitions [OF part]
   6.317    show ?thesis
   6.318    proof (cases "Array.get h1 a ! middle \<le> ?pivot")
   6.319 @@ -419,7 +419,7 @@
   6.320  
   6.321  
   6.322  lemma quicksort_permutes:
   6.323 -  assumes "crel (quicksort a l r) h h' rs"
   6.324 +  assumes "effect (quicksort a l r) h h' rs"
   6.325    shows "multiset_of (Array.get h' a) 
   6.326    = multiset_of (Array.get h a)"
   6.327    using assms
   6.328 @@ -427,41 +427,41 @@
   6.329    case (1 a l r h h' rs)
   6.330    with partition_permutes show ?case
   6.331      unfolding quicksort.simps [of a l r]
   6.332 -    by (elim crel_ifE crel_bindE crel_assertE crel_returnE) auto
   6.333 +    by (elim effect_ifE effect_bindE effect_assertE effect_returnE) auto
   6.334  qed
   6.335  
   6.336  lemma length_remains:
   6.337 -  assumes "crel (quicksort a l r) h h' rs"
   6.338 +  assumes "effect (quicksort a l r) h h' rs"
   6.339    shows "Array.length h a = Array.length h' a"
   6.340  using assms
   6.341  proof (induct a l r arbitrary: h h' rs rule: quicksort.induct)
   6.342    case (1 a l r h h' rs)
   6.343    with partition_length_remains show ?case
   6.344      unfolding quicksort.simps [of a l r]
   6.345 -    by (elim crel_ifE crel_bindE crel_assertE crel_returnE) auto
   6.346 +    by (elim effect_ifE effect_bindE effect_assertE effect_returnE) auto
   6.347  qed
   6.348  
   6.349  lemma quicksort_outer_remains:
   6.350 -  assumes "crel (quicksort a l r) h h' rs"
   6.351 +  assumes "effect (quicksort a l r) h h' rs"
   6.352     shows "\<forall>i. i < l \<or> r < i \<longrightarrow> Array.get h (a::nat array) ! i = Array.get h' a ! i"
   6.353    using assms
   6.354  proof (induct a l r arbitrary: h h' rs rule: quicksort.induct)
   6.355    case (1 a l r h h' rs)
   6.356 -  note cr = `crel (quicksort a l r) h h' rs`
   6.357 +  note cr = `effect (quicksort a l r) h h' rs`
   6.358    thus ?case
   6.359    proof (cases "r > l")
   6.360      case False
   6.361      with cr have "h' = h"
   6.362        unfolding quicksort.simps [of a l r]
   6.363 -      by (elim crel_ifE crel_returnE) auto
   6.364 +      by (elim effect_ifE effect_returnE) auto
   6.365      thus ?thesis by simp
   6.366    next
   6.367    case True
   6.368     { 
   6.369        fix h1 h2 p ret1 ret2 i
   6.370 -      assume part: "crel (partition a l r) h h1 p"
   6.371 -      assume qs1: "crel (quicksort a l (p - 1)) h1 h2 ret1"
   6.372 -      assume qs2: "crel (quicksort a (p + 1) r) h2 h' ret2"
   6.373 +      assume part: "effect (partition a l r) h h1 p"
   6.374 +      assume qs1: "effect (quicksort a l (p - 1)) h1 h2 ret1"
   6.375 +      assume qs2: "effect (quicksort a (p + 1) r) h2 h' ret2"
   6.376        assume pivot: "l \<le> p \<and> p \<le> r"
   6.377        assume i_outer: "i < l \<or> r < i"
   6.378        from  partition_outer_remains [OF part True] i_outer
   6.379 @@ -476,25 +476,25 @@
   6.380      }
   6.381      with cr show ?thesis
   6.382        unfolding quicksort.simps [of a l r]
   6.383 -      by (elim crel_ifE crel_bindE crel_assertE crel_returnE) auto
   6.384 +      by (elim effect_ifE effect_bindE effect_assertE effect_returnE) auto
   6.385    qed
   6.386  qed
   6.387  
   6.388  lemma quicksort_is_skip:
   6.389 -  assumes "crel (quicksort a l r) h h' rs"
   6.390 +  assumes "effect (quicksort a l r) h h' rs"
   6.391    shows "r \<le> l \<longrightarrow> h = h'"
   6.392    using assms
   6.393    unfolding quicksort.simps [of a l r]
   6.394 -  by (elim crel_ifE crel_returnE) auto
   6.395 +  by (elim effect_ifE effect_returnE) auto
   6.396   
   6.397  lemma quicksort_sorts:
   6.398 -  assumes "crel (quicksort a l r) h h' rs"
   6.399 +  assumes "effect (quicksort a l r) h h' rs"
   6.400    assumes l_r_length: "l < Array.length h a" "r < Array.length h a" 
   6.401    shows "sorted (subarray l (r + 1) a h')"
   6.402    using assms
   6.403  proof (induct a l r arbitrary: h h' rs rule: quicksort.induct)
   6.404    case (1 a l r h h' rs)
   6.405 -  note cr = `crel (quicksort a l r) h h' rs`
   6.406 +  note cr = `effect (quicksort a l r) h h' rs`
   6.407    thus ?case
   6.408    proof (cases "r > l")
   6.409      case False
   6.410 @@ -505,9 +505,9 @@
   6.411      case True
   6.412      { 
   6.413        fix h1 h2 p
   6.414 -      assume part: "crel (partition a l r) h h1 p"
   6.415 -      assume qs1: "crel (quicksort a l (p - 1)) h1 h2 ()"
   6.416 -      assume qs2: "crel (quicksort a (p + 1) r) h2 h' ()"
   6.417 +      assume part: "effect (partition a l r) h h1 p"
   6.418 +      assume qs1: "effect (quicksort a l (p - 1)) h1 h2 ()"
   6.419 +      assume qs2: "effect (quicksort a (p + 1) r) h2 h' ()"
   6.420        from partition_returns_index_in_bounds [OF part True]
   6.421        have pivot: "l\<le> p \<and> p \<le> r" .
   6.422       note length_remains = length_remains[OF qs2] length_remains[OF qs1] partition_length_remains[OF part]
   6.423 @@ -557,25 +557,25 @@
   6.424      }
   6.425      with True cr show ?thesis
   6.426        unfolding quicksort.simps [of a l r]
   6.427 -      by (elim crel_ifE crel_returnE crel_bindE crel_assertE) auto
   6.428 +      by (elim effect_ifE effect_returnE effect_bindE effect_assertE) auto
   6.429    qed
   6.430  qed
   6.431  
   6.432  
   6.433  lemma quicksort_is_sort:
   6.434 -  assumes crel: "crel (quicksort a 0 (Array.length h a - 1)) h h' rs"
   6.435 +  assumes effect: "effect (quicksort a 0 (Array.length h a - 1)) h h' rs"
   6.436    shows "Array.get h' a = sort (Array.get h a)"
   6.437  proof (cases "Array.get h a = []")
   6.438    case True
   6.439 -  with quicksort_is_skip[OF crel] show ?thesis
   6.440 +  with quicksort_is_skip[OF effect] show ?thesis
   6.441    unfolding Array.length_def by simp
   6.442  next
   6.443    case False
   6.444 -  from quicksort_sorts [OF crel] False have "sorted (sublist' 0 (List.length (Array.get h a)) (Array.get h' a))"
   6.445 +  from quicksort_sorts [OF effect] False have "sorted (sublist' 0 (List.length (Array.get h a)) (Array.get h' a))"
   6.446      unfolding Array.length_def subarray_def by auto
   6.447 -  with length_remains[OF crel] have "sorted (Array.get h' a)"
   6.448 +  with length_remains[OF effect] have "sorted (Array.get h' a)"
   6.449      unfolding Array.length_def by simp
   6.450 -  with quicksort_permutes [OF crel] properties_for_sort show ?thesis by fastsimp
   6.451 +  with quicksort_permutes [OF effect] properties_for_sort show ?thesis by fastsimp
   6.452  qed
   6.453  
   6.454  subsection {* No Errors in quicksort *}
   6.455 @@ -590,26 +590,26 @@
   6.456    case (1 a l r p)
   6.457    thus ?case unfolding part1.simps [of a l r]
   6.458    apply (auto intro!: success_intros del: success_ifI simp add: not_le)
   6.459 -  apply (auto intro!: crel_intros crel_swapI)
   6.460 +  apply (auto intro!: effect_intros effect_swapI)
   6.461    done
   6.462  qed
   6.463  
   6.464  lemma success_bindI' [success_intros]: (*FIXME move*)
   6.465    assumes "success f h"
   6.466 -  assumes "\<And>h' r. crel f h h' r \<Longrightarrow> success (g r) h'"
   6.467 +  assumes "\<And>h' r. effect f h h' r \<Longrightarrow> success (g r) h'"
   6.468    shows "success (f \<guillemotright>= g) h"
   6.469 -using assms(1) proof (rule success_crelE)
   6.470 +using assms(1) proof (rule success_effectE)
   6.471    fix h' r
   6.472 -  assume "crel f h h' r"
   6.473 +  assume "effect f h h' r"
   6.474    moreover with assms(2) have "success (g r) h'" .
   6.475 -  ultimately show "success (f \<guillemotright>= g) h" by (rule success_bind_crelI)
   6.476 +  ultimately show "success (f \<guillemotright>= g) h" by (rule success_bind_effectI)
   6.477  qed
   6.478  
   6.479  lemma success_partitionI:
   6.480    assumes "l < r" "l < Array.length h a" "r < Array.length h a"
   6.481    shows "success (partition a l r) h"
   6.482  using assms unfolding partition.simps swap_def
   6.483 -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.484 +apply (auto intro!: success_bindI' success_ifI success_returnI success_nthI success_updI success_part1I elim!: effect_bindE effect_updE effect_nthE effect_returnE simp add:)
   6.485  apply (frule part_length_remains)
   6.486  apply (frule part_returns_index_in_bounds)
   6.487  apply auto
   6.488 @@ -633,7 +633,7 @@
   6.489      apply auto
   6.490      apply (frule partition_returns_index_in_bounds)
   6.491      apply auto
   6.492 -    apply (auto elim!: crel_assertE dest!: partition_length_remains length_remains)
   6.493 +    apply (auto elim!: effect_assertE dest!: partition_length_remains length_remains)
   6.494      apply (subgoal_tac "Suc r \<le> ri \<or> r = ri") 
   6.495      apply (erule disjE)
   6.496      apply auto
     7.1 --- a/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy	Mon Nov 22 09:19:34 2010 +0100
     7.2 +++ b/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy	Mon Nov 22 09:37:39 2010 +0100
     7.3 @@ -26,15 +26,15 @@
     7.4  
     7.5  declare swap.simps [simp del] rev.simps [simp del]
     7.6  
     7.7 -lemma swap_pointwise: assumes "crel (swap a i j) h h' r"
     7.8 +lemma swap_pointwise: assumes "effect (swap a i j) h h' r"
     7.9    shows "Array.get h' a ! k = (if k = i then Array.get h a ! j
    7.10        else if k = j then Array.get h a ! i
    7.11        else Array.get h a ! k)"
    7.12  using assms unfolding swap.simps
    7.13 -by (elim crel_elims)
    7.14 +by (elim effect_elims)
    7.15   (auto simp: length_def)
    7.16  
    7.17 -lemma rev_pointwise: assumes "crel (rev a i j) h h' r"
    7.18 +lemma rev_pointwise: assumes "effect (rev a i j) h h' r"
    7.19    shows "Array.get h' a ! k = (if k < i then Array.get h a ! k
    7.20        else if j < k then Array.get h a ! k
    7.21        else Array.get h a ! (j - (k - i)))" (is "?P a i j h h'")
    7.22 @@ -45,9 +45,9 @@
    7.23      case True
    7.24      with 1[unfolded rev.simps[of a i j]]
    7.25      obtain h' where
    7.26 -      swp: "crel (swap a i j) h h' ()"
    7.27 -      and rev: "crel (rev a (i + 1) (j - 1)) h' h'' ()"
    7.28 -      by (auto elim: crel_elims)
    7.29 +      swp: "effect (swap a i j) h h' ()"
    7.30 +      and rev: "effect (rev a (i + 1) (j - 1)) h' h'' ()"
    7.31 +      by (auto elim: effect_elims)
    7.32      from rev 1 True
    7.33      have eq: "?P a (i + 1) (j - 1) h' h''" by auto
    7.34  
    7.35 @@ -58,12 +58,12 @@
    7.36      case False
    7.37      with 1[unfolded rev.simps[of a i j]]
    7.38      show ?thesis
    7.39 -      by (cases "k = j") (auto elim: crel_elims)
    7.40 +      by (cases "k = j") (auto elim: effect_elims)
    7.41    qed
    7.42  qed
    7.43  
    7.44  lemma rev_length:
    7.45 -  assumes "crel (rev a i j) h h' r"
    7.46 +  assumes "effect (rev a i j) h h' r"
    7.47    shows "Array.length h a = Array.length h' a"
    7.48  using assms
    7.49  proof (induct a i j arbitrary: h h' rule: rev.induct)
    7.50 @@ -73,21 +73,21 @@
    7.51      case True
    7.52      with 1[unfolded rev.simps[of a i j]]
    7.53      obtain h' where
    7.54 -      swp: "crel (swap a i j) h h' ()"
    7.55 -      and rev: "crel (rev a (i + 1) (j - 1)) h' h'' ()"
    7.56 -      by (auto elim: crel_elims)
    7.57 +      swp: "effect (swap a i j) h h' ()"
    7.58 +      and rev: "effect (rev a (i + 1) (j - 1)) h' h'' ()"
    7.59 +      by (auto elim: effect_elims)
    7.60      from swp rev 1 True show ?thesis
    7.61        unfolding swap.simps
    7.62 -      by (elim crel_elims) fastsimp
    7.63 +      by (elim effect_elims) fastsimp
    7.64    next
    7.65      case False
    7.66      with 1[unfolded rev.simps[of a i j]]
    7.67      show ?thesis
    7.68 -      by (auto elim: crel_elims)
    7.69 +      by (auto elim: effect_elims)
    7.70    qed
    7.71  qed
    7.72  
    7.73 -lemma rev2_rev': assumes "crel (rev a i j) h h' u"
    7.74 +lemma rev2_rev': assumes "effect (rev a i j) h h' u"
    7.75    assumes "j < Array.length h a"
    7.76    shows "subarray i (j + 1) a h' = List.rev (subarray i (j + 1) a h)"
    7.77  proof - 
    7.78 @@ -103,11 +103,11 @@
    7.79  qed
    7.80  
    7.81  lemma rev2_rev: 
    7.82 -  assumes "crel (rev a 0 (Array.length h a - 1)) h h' u"
    7.83 +  assumes "effect (rev a 0 (Array.length h a - 1)) h h' u"
    7.84    shows "Array.get h' a = List.rev (Array.get h a)"
    7.85    using rev2_rev'[OF assms] rev_length[OF assms] assms
    7.86      by (cases "Array.length h a = 0", auto simp add: Array.length_def
    7.87 -      subarray_def sublist'_all rev.simps[where j=0] elim!: crel_elims)
    7.88 +      subarray_def sublist'_all rev.simps[where j=0] elim!: effect_elims)
    7.89    (drule sym[of "List.length (Array.get h a)"], simp)
    7.90  
    7.91  definition "example = (Array.make 10 id \<guillemotright>= (\<lambda>a. rev a 0 9))"
     8.1 --- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Mon Nov 22 09:19:34 2010 +0100
     8.2 +++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Mon Nov 22 09:37:39 2010 +0100
     8.3 @@ -448,8 +448,8 @@
     8.4      by simp
     8.5  qed
     8.6  
     8.7 -lemma crel_ref:
     8.8 -  assumes "crel (ref v) h h' x"
     8.9 +lemma effect_ref:
    8.10 +  assumes "effect (ref v) h h' x"
    8.11    obtains "Ref.get h' x = v"
    8.12    and "\<not> Ref.present h x"
    8.13    and "Ref.present h' x"
    8.14 @@ -458,7 +458,7 @@
    8.15    and "\<forall>y. Ref.present h y \<longrightarrow> Ref.present h' y"
    8.16    using assms
    8.17    unfolding Ref.ref_def
    8.18 -  apply (elim crel_heapE)
    8.19 +  apply (elim effect_heapE)
    8.20    unfolding Ref.alloc_def
    8.21    apply (simp add: Let_def)
    8.22    unfolding Ref.present_def
    8.23 @@ -468,56 +468,56 @@
    8.24    done
    8.25  
    8.26  lemma make_llist:
    8.27 -assumes "crel (make_llist xs) h h' r"
    8.28 +assumes "effect (make_llist xs) h h' r"
    8.29  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.30  using assms 
    8.31  proof (induct xs arbitrary: h h' r)
    8.32 -  case Nil thus ?case by (auto elim: crel_returnE simp add: make_llist.simps)
    8.33 +  case Nil thus ?case by (auto elim: effect_returnE simp add: make_llist.simps)
    8.34  next
    8.35    case (Cons x xs')
    8.36 -  from Cons.prems obtain h1 r1 r' where make_llist: "crel (make_llist xs') h h1 r1"
    8.37 -    and crel_refnew:"crel (ref r1) h1 h' r'" and Node: "r = Node x r'"
    8.38 +  from Cons.prems obtain h1 r1 r' where make_llist: "effect (make_llist xs') h h1 r1"
    8.39 +    and effect_refnew:"effect (ref r1) h1 h' r'" and Node: "r = Node x r'"
    8.40      unfolding make_llist.simps
    8.41 -    by (auto elim!: crel_bindE crel_returnE)
    8.42 +    by (auto elim!: effect_bindE effect_returnE)
    8.43    from Cons.hyps[OF make_llist] have list_of_h1: "list_of h1 r1 xs'" ..
    8.44    from Cons.hyps[OF make_llist] obtain rs' where rs'_def: "refs_of h1 r1 rs'" by (auto intro: list_of_refs_of)
    8.45    from Cons.hyps[OF make_llist] rs'_def have refs_present: "\<forall>ref\<in>set rs'. Ref.present h1 ref" by simp
    8.46 -  from crel_refnew rs'_def refs_present have refs_unchanged: "\<forall>refs. refs_of h1 r1 refs \<longrightarrow>
    8.47 +  from effect_refnew rs'_def refs_present have refs_unchanged: "\<forall>refs. refs_of h1 r1 refs \<longrightarrow>
    8.48           (\<forall>ref\<in>set refs. Ref.present h1 ref \<and> Ref.present h' ref \<and> Ref.get h1 ref = Ref.get h' ref)"
    8.49 -    by (auto elim!: crel_ref dest: refs_of_is_fun)
    8.50 -  with list_of_invariant[OF list_of_h1 refs_unchanged] Node crel_refnew have fstgoal: "list_of h' r (x # xs')"
    8.51 +    by (auto elim!: effect_ref dest: refs_of_is_fun)
    8.52 +  with list_of_invariant[OF list_of_h1 refs_unchanged] Node effect_refnew have fstgoal: "list_of h' r (x # xs')"
    8.53      unfolding list_of.simps
    8.54 -    by (auto elim!: crel_refE)
    8.55 +    by (auto elim!: effect_refE)
    8.56    from refs_unchanged rs'_def have refs_still_present: "\<forall>ref\<in>set rs'. Ref.present h' ref" by auto
    8.57 -  from refs_of_invariant[OF rs'_def refs_unchanged] refs_unchanged Node crel_refnew refs_still_present
    8.58 +  from refs_of_invariant[OF rs'_def refs_unchanged] refs_unchanged Node effect_refnew refs_still_present
    8.59    have sndgoal: "\<forall>rs. refs_of h' r rs \<longrightarrow> (\<forall>ref\<in>set rs. Ref.present h' ref)"
    8.60 -    by (fastsimp elim!: crel_refE dest: refs_of_is_fun)
    8.61 +    by (fastsimp elim!: effect_refE dest: refs_of_is_fun)
    8.62    from fstgoal sndgoal show ?case ..
    8.63  qed
    8.64  
    8.65 -lemma traverse: "list_of h n r \<Longrightarrow> crel (traverse n) h h r"
    8.66 +lemma traverse: "list_of h n r \<Longrightarrow> effect (traverse n) h h r"
    8.67  proof (induct r arbitrary: n)
    8.68    case Nil
    8.69    thus ?case
    8.70 -    by (auto intro: crel_returnI)
    8.71 +    by (auto intro: effect_returnI)
    8.72  next
    8.73    case (Cons x xs)
    8.74    thus ?case
    8.75    apply (cases n, auto)
    8.76 -  by (auto intro!: crel_bindI crel_returnI crel_lookupI)
    8.77 +  by (auto intro!: effect_bindI effect_returnI effect_lookupI)
    8.78  qed
    8.79  
    8.80  lemma traverse_make_llist':
    8.81 -  assumes crel: "crel (make_llist xs \<guillemotright>= traverse) h h' r"
    8.82 +  assumes effect: "effect (make_llist xs \<guillemotright>= traverse) h h' r"
    8.83    shows "r = xs"
    8.84  proof -
    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!: crel_bindE)
    8.89 +  from effect obtain h1 r1
    8.90 +    where makell: "effect (make_llist xs) h h1 r1"
    8.91 +    and trav: "effect (traverse r1) h1 h' r"
    8.92 +    by (auto elim!: effect_bindE)
    8.93    from make_llist[OF makell] have "list_of h1 r1 xs" ..
    8.94    from traverse [OF this] trav show ?thesis
    8.95 -    using crel_deterministic by fastsimp
    8.96 +    using effect_deterministic by fastsimp
    8.97  qed
    8.98  
    8.99  section {* Proving correctness of in-place reversal *}
   8.100 @@ -546,7 +546,7 @@
   8.101  subsection {* Correctness Proof *}
   8.102  
   8.103  lemma rev'_invariant:
   8.104 -  assumes "crel (rev' q p) h h' v"
   8.105 +  assumes "effect (rev' q p) h h' v"
   8.106    assumes "list_of' h q qs"
   8.107    assumes "list_of' h p ps"
   8.108    assumes "\<forall>qrs prs. refs_of' h q qrs \<and> refs_of' h p prs \<longrightarrow> set prs \<inter> set qrs = {}"
   8.109 @@ -556,7 +556,7 @@
   8.110    case Nil
   8.111    thus ?case
   8.112      unfolding rev'.simps[of q p] list_of'_def
   8.113 -    by (auto elim!: crel_bindE crel_lookupE crel_returnE)
   8.114 +    by (auto elim!: effect_bindE effect_lookupE effect_returnE)
   8.115  next
   8.116    case (Cons x xs)
   8.117    (*"LinkedList.list_of h' (get_ref v h') (List.rev xs @ x # qsa)"*)
   8.118 @@ -565,8 +565,8 @@
   8.119      (*and "ref_present ref h"*)
   8.120      and list_of'_ref: "list_of' h ref xs"
   8.121      unfolding list_of'_def by (cases "Ref.get h p", auto)
   8.122 -  from p_is_Node Cons(2) have crel_rev': "crel (rev' p ref) (Ref.set p (Node x q) h) h' v"
   8.123 -    by (auto simp add: rev'.simps [of q p] elim!: crel_bindE crel_lookupE crel_updateE)
   8.124 +  from p_is_Node Cons(2) have effect_rev': "effect (rev' p ref) (Ref.set p (Node x q) h) h' v"
   8.125 +    by (auto simp add: rev'.simps [of q p] elim!: effect_bindE effect_lookupE effect_updateE)
   8.126    from Cons(3) obtain qrs where qrs_def: "refs_of' h q qrs" by (elim list_of'_refs_of')
   8.127    from Cons(4) obtain prs where prs_def: "refs_of' h p prs" by (elim list_of'_refs_of')
   8.128    from qrs_def prs_def Cons(5) have distinct_pointers: "set qrs \<inter> set prs = {}" by fastsimp
   8.129 @@ -594,60 +594,60 @@
   8.130      apply (drule refs_of'_is_fun) back back apply assumption
   8.131      apply (drule refs_of'_is_fun) back back apply assumption
   8.132      apply auto done
   8.133 -  from Cons.hyps [OF crel_rev' 1 2 3] show ?case by simp
   8.134 +  from Cons.hyps [OF effect_rev' 1 2 3] show ?case by simp
   8.135  qed
   8.136  
   8.137  
   8.138  lemma rev_correctness:
   8.139    assumes list_of_h: "list_of h r xs"
   8.140    assumes validHeap: "\<forall>refs. refs_of h r refs \<longrightarrow> (\<forall>r \<in> set refs. Ref.present h r)"
   8.141 -  assumes crel_rev: "crel (rev r) h h' r'"
   8.142 +  assumes effect_rev: "effect (rev r) h h' r'"
   8.143    shows "list_of h' r' (List.rev xs)"
   8.144  using assms
   8.145  proof (cases r)
   8.146    case Empty
   8.147 -  with list_of_h crel_rev show ?thesis
   8.148 -    by (auto simp add: list_of_Empty elim!: crel_returnE)
   8.149 +  with list_of_h effect_rev show ?thesis
   8.150 +    by (auto simp add: list_of_Empty elim!: effect_returnE)
   8.151  next
   8.152    case (Node x ps)
   8.153 -  with crel_rev obtain p q h1 h2 h3 v where
   8.154 -    init: "crel (ref Empty) h h1 q"
   8.155 -    "crel (ref (Node x ps)) h1 h2 p"
   8.156 -    and crel_rev':"crel (rev' q p) h2 h3 v"
   8.157 -    and lookup: "crel (!v) h3 h' r'"
   8.158 +  with effect_rev obtain p q h1 h2 h3 v where
   8.159 +    init: "effect (ref Empty) h h1 q"
   8.160 +    "effect (ref (Node x ps)) h1 h2 p"
   8.161 +    and effect_rev':"effect (rev' q p) h2 h3 v"
   8.162 +    and lookup: "effect (!v) h3 h' r'"
   8.163      using rev.simps
   8.164 -    by (auto elim!: crel_bindE)
   8.165 +    by (auto elim!: effect_bindE)
   8.166    from init have a1:"list_of' h2 q []"
   8.167      unfolding list_of'_def
   8.168 -    by (auto elim!: crel_ref)
   8.169 +    by (auto elim!: effect_ref)
   8.170    from list_of_h obtain refs where refs_def: "refs_of h r refs" by (rule list_of_refs_of)
   8.171    from validHeap init refs_def have heap_eq: "\<forall>refs. refs_of h r refs \<longrightarrow> (\<forall>ref\<in>set refs. Ref.present h ref \<and> Ref.present h2 ref \<and> Ref.get h ref = Ref.get h2 ref)"
   8.172 -    by (fastsimp elim!: crel_ref dest: refs_of_is_fun)
   8.173 +    by (fastsimp elim!: effect_ref dest: refs_of_is_fun)
   8.174    from list_of_invariant[OF list_of_h heap_eq] have "list_of h2 r xs" .
   8.175    from init this Node have a2: "list_of' h2 p xs"
   8.176      apply -
   8.177      unfolding list_of'_def
   8.178 -    apply (auto elim!: crel_refE)
   8.179 +    apply (auto elim!: effect_refE)
   8.180      done
   8.181    from init have refs_of_q: "refs_of' h2 q [q]"
   8.182 -    by (auto elim!: crel_ref)
   8.183 +    by (auto elim!: effect_ref)
   8.184    from refs_def Node have refs_of'_ps: "refs_of' h ps refs"
   8.185      by (auto simp add: refs_of'_def'[symmetric])
   8.186    from validHeap refs_def have all_ref_present: "\<forall>r\<in>set refs. Ref.present h r" by simp
   8.187    from init refs_of'_ps this
   8.188      have heap_eq: "\<forall>refs. refs_of' h ps refs \<longrightarrow> (\<forall>ref\<in>set refs. Ref.present h ref \<and> Ref.present h2 ref \<and> Ref.get h ref = Ref.get h2 ref)"
   8.189 -    by (auto elim!: crel_ref [where ?'a="'a node", where ?'b="'a node", where ?'c="'a node"] dest: refs_of'_is_fun)
   8.190 +    by (auto elim!: effect_ref [where ?'a="'a node", where ?'b="'a node", where ?'c="'a node"] dest: refs_of'_is_fun)
   8.191    from refs_of'_invariant[OF refs_of'_ps this] have "refs_of' h2 ps refs" .
   8.192    with init have refs_of_p: "refs_of' h2 p (p#refs)"
   8.193 -    by (auto elim!: crel_refE simp add: refs_of'_def')
   8.194 +    by (auto elim!: effect_refE simp add: refs_of'_def')
   8.195    with init all_ref_present have q_is_new: "q \<notin> set (p#refs)"
   8.196 -    by (auto elim!: crel_refE intro!: Ref.noteq_I)
   8.197 +    by (auto elim!: effect_refE intro!: Ref.noteq_I)
   8.198    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.199      by (fastsimp simp only: set.simps dest: refs_of'_is_fun)
   8.200 -  from rev'_invariant [OF crel_rev' a1 a2 a3] have "list_of h3 (Ref.get h3 v) (List.rev xs)" 
   8.201 +  from rev'_invariant [OF effect_rev' a1 a2 a3] have "list_of h3 (Ref.get h3 v) (List.rev xs)" 
   8.202      unfolding list_of'_def by auto
   8.203    with lookup show ?thesis
   8.204 -    by (auto elim: crel_lookupE)
   8.205 +    by (auto elim: effect_lookupE)
   8.206  qed
   8.207  
   8.208  
   8.209 @@ -780,21 +780,21 @@
   8.210  qed
   8.211  
   8.212  
   8.213 -text {* secondly, we add the crel statement in the premise, and derive the crel statements for the single cases which we then eliminate with our crel elim rules. *}
   8.214 +text {* secondly, we add the effect statement in the premise, and derive the effect statements for the single cases which we then eliminate with our effect elim rules. *}
   8.215    
   8.216  lemma merge_induct3: 
   8.217  assumes  "list_of' h p xs"
   8.218  assumes  "list_of' h q ys"
   8.219 -assumes  "crel (merge p q) h h' r"
   8.220 +assumes  "effect (merge p q) h h' r"
   8.221  assumes  "\<And> ys p q. \<lbrakk> list_of' h p []; list_of' h q ys; Ref.get h p = Empty \<rbrakk> \<Longrightarrow> P p q h h q [] ys"
   8.222  assumes  "\<And> x xs' p q pn. \<lbrakk> list_of' h p (x#xs'); list_of' h q []; Ref.get h p = Node x pn; Ref.get h q = Empty \<rbrakk> \<Longrightarrow> P p q h h p (x#xs') []"
   8.223  assumes  "\<And> x xs' y ys' p q pn qn h1 r1 h'.
   8.224    \<lbrakk> list_of' h p (x#xs'); list_of' h q (y#ys');Ref.get h p = Node x pn; Ref.get h q = Node y qn;
   8.225 -  x \<le> y; crel (merge pn q) h h1 r1 ; P pn q h h1 r1 xs' (y#ys'); h' = Ref.set p (Node x r1) h1 \<rbrakk>
   8.226 +  x \<le> y; effect (merge pn q) h h1 r1 ; P pn q h h1 r1 xs' (y#ys'); h' = Ref.set p (Node x r1) h1 \<rbrakk>
   8.227    \<Longrightarrow> P p q h h' p (x#xs') (y#ys')"
   8.228  assumes "\<And> x xs' y ys' p q pn qn h1 r1 h'.
   8.229    \<lbrakk> list_of' h p (x#xs'); list_of' h q (y#ys'); Ref.get h p = Node x pn; Ref.get h q = Node y qn;
   8.230 -  \<not> x \<le> y; crel (merge p qn) h h1 r1; P p qn h h1 r1 (x#xs') ys'; h' = Ref.set q (Node y r1) h1 \<rbrakk>
   8.231 +  \<not> x \<le> y; effect (merge p qn) h h1 r1; P p qn h h1 r1 (x#xs') ys'; h' = Ref.set q (Node y r1) h1 \<rbrakk>
   8.232    \<Longrightarrow> P p q h h' q (x#xs') (y#ys')"
   8.233  shows "P p q h h' r xs ys"
   8.234  using assms(3)
   8.235 @@ -802,29 +802,29 @@
   8.236    case (1 ys p q)
   8.237    from 1(3-4) have "h = h' \<and> r = q"
   8.238      unfolding merge_simps[of p q]
   8.239 -    by (auto elim!: crel_lookupE crel_bindE crel_returnE)
   8.240 +    by (auto elim!: effect_lookupE effect_bindE effect_returnE)
   8.241    with assms(4)[OF 1(1) 1(2) 1(3)] show ?case by simp
   8.242  next
   8.243    case (2 x xs' p q pn)
   8.244    from 2(3-5) have "h = h' \<and> r = p"
   8.245      unfolding merge_simps[of p q]
   8.246 -    by (auto elim!: crel_lookupE crel_bindE crel_returnE)
   8.247 +    by (auto elim!: effect_lookupE effect_bindE effect_returnE)
   8.248    with assms(5)[OF 2(1-4)] show ?case by simp
   8.249  next
   8.250    case (3 x xs' y ys' p q pn qn)
   8.251    from 3(3-5) 3(7) obtain h1 r1 where
   8.252 -    1: "crel (merge pn q) h h1 r1" 
   8.253 +    1: "effect (merge pn q) h h1 r1" 
   8.254      and 2: "h' = Ref.set p (Node x r1) h1 \<and> r = p"
   8.255      unfolding merge_simps[of p q]
   8.256 -    by (auto elim!: crel_lookupE crel_bindE crel_returnE crel_ifE crel_updateE)
   8.257 +    by (auto elim!: effect_lookupE effect_bindE effect_returnE effect_ifE effect_updateE)
   8.258    from 3(6)[OF 1] assms(6) [OF 3(1-5)] 1 2 show ?case by simp
   8.259  next
   8.260    case (4 x xs' y ys' p q pn qn)
   8.261    from 4(3-5) 4(7) obtain h1 r1 where
   8.262 -    1: "crel (merge p qn) h h1 r1" 
   8.263 +    1: "effect (merge p qn) h h1 r1" 
   8.264      and 2: "h' = Ref.set q (Node y r1) h1 \<and> r = q"
   8.265      unfolding merge_simps[of p q]
   8.266 -    by (auto elim!: crel_lookupE crel_bindE crel_returnE crel_ifE crel_updateE)
   8.267 +    by (auto elim!: effect_lookupE effect_bindE effect_returnE effect_ifE effect_updateE)
   8.268    from 4(6)[OF 1] assms(7) [OF 4(1-5)] 1 2 show ?case by simp
   8.269  qed
   8.270  
   8.271 @@ -837,7 +837,7 @@
   8.272  lemma merge_unchanged:
   8.273    assumes "refs_of' h p xs"
   8.274    assumes "refs_of' h q ys"  
   8.275 -  assumes "crel (merge p q) h h' r'"
   8.276 +  assumes "effect (merge p q) h h' r'"
   8.277    assumes "set xs \<inter> set ys = {}"
   8.278    assumes "r \<notin> set xs \<union> set ys"
   8.279    shows "Ref.get h r = Ref.get h' r"
   8.280 @@ -882,7 +882,7 @@
   8.281  lemma refs_of'_merge:
   8.282    assumes "refs_of' h p xs"
   8.283    assumes "refs_of' h q ys"
   8.284 -  assumes "crel (merge p q) h h' r"
   8.285 +  assumes "effect (merge p q) h h' r"
   8.286    assumes "set xs \<inter> set ys = {}"
   8.287    assumes "refs_of' h' r rs"
   8.288    shows "set rs \<subseteq> set xs \<union> set ys"
   8.289 @@ -930,7 +930,7 @@
   8.290  lemma
   8.291    assumes "list_of' h p xs"
   8.292    assumes "list_of' h q ys"
   8.293 -  assumes "crel (merge p q) h h' r"
   8.294 +  assumes "effect (merge p q) h h' r"
   8.295    assumes "\<forall>qrs prs. refs_of' h q qrs \<and> refs_of' h p prs \<longrightarrow> set prs \<inter> set qrs = {}"
   8.296    shows "list_of' h' r (Lmerge xs ys)"
   8.297  using assms(4)
     9.1 --- a/src/HOL/Imperative_HOL/ex/SatChecker.thy	Mon Nov 22 09:19:34 2010 +0100
     9.2 +++ b/src/HOL/Imperative_HOL/ex/SatChecker.thy	Mon Nov 22 09:37:39 2010 +0100
     9.3 @@ -212,33 +212,33 @@
     9.4  subsection {* Proofs about these functions *}
     9.5  
     9.6  lemma res_mem:
     9.7 -assumes "crel (res_mem l xs) h h' r"
     9.8 +assumes "effect (res_mem l xs) h h' r"
     9.9    shows "l \<in> set xs \<and> r = remove1 l xs"
    9.10  using assms
    9.11  proof (induct xs arbitrary: r)
    9.12    case Nil
    9.13 -  thus ?case unfolding res_mem.simps by (auto elim: crel_raiseE)
    9.14 +  thus ?case unfolding res_mem.simps by (auto elim: effect_raiseE)
    9.15  next
    9.16    case (Cons x xs')
    9.17    thus ?case
    9.18      unfolding res_mem.simps
    9.19 -    by (elim crel_raiseE crel_returnE crel_ifE crel_bindE) auto
    9.20 +    by (elim effect_raiseE effect_returnE effect_ifE effect_bindE) auto
    9.21  qed
    9.22  
    9.23  lemma resolve1_Inv:
    9.24 -assumes "crel (resolve1 l xs ys) h h' r"
    9.25 +assumes "effect (resolve1 l xs ys) h h' r"
    9.26    shows "l \<in> set xs \<and> r = merge (remove1 l xs) ys"
    9.27  using assms
    9.28  proof (induct xs ys arbitrary: r rule: resolve1.induct)
    9.29    case (1 l x xs y ys r)
    9.30    thus ?case
    9.31      unfolding resolve1.simps
    9.32 -    by (elim crel_bindE crel_ifE crel_returnE) auto
    9.33 +    by (elim effect_bindE effect_ifE effect_returnE) auto
    9.34  next
    9.35    case (2 l ys r)
    9.36    thus ?case
    9.37      unfolding resolve1.simps
    9.38 -    by (elim crel_raiseE) auto
    9.39 +    by (elim effect_raiseE) auto
    9.40  next
    9.41    case (3 l v va r)
    9.42    thus ?case
    9.43 @@ -247,19 +247,19 @@
    9.44  qed
    9.45  
    9.46  lemma resolve2_Inv: 
    9.47 -  assumes "crel (resolve2 l xs ys) h h' r"
    9.48 +  assumes "effect (resolve2 l xs ys) h h' r"
    9.49    shows "l \<in> set ys \<and> r = merge xs (remove1 l ys)"
    9.50  using assms
    9.51  proof (induct xs ys arbitrary: r rule: resolve2.induct)
    9.52    case (1 l x xs y ys r)
    9.53    thus ?case
    9.54      unfolding resolve2.simps
    9.55 -    by (elim crel_bindE crel_ifE crel_returnE) auto
    9.56 +    by (elim effect_bindE effect_ifE effect_returnE) auto
    9.57  next
    9.58    case (2 l ys r)
    9.59    thus ?case
    9.60      unfolding resolve2.simps
    9.61 -    by (elim crel_raiseE) auto
    9.62 +    by (elim effect_raiseE) auto
    9.63  next
    9.64    case (3 l v va r)
    9.65    thus ?case
    9.66 @@ -268,7 +268,7 @@
    9.67  qed
    9.68  
    9.69  lemma res_thm'_Inv:
    9.70 -assumes "crel (res_thm' l xs ys) h h' r"
    9.71 +assumes "effect (res_thm' l xs ys) h h' r"
    9.72  shows "\<exists>l'. (l' \<in> set xs \<and> compl l' \<in> set ys \<and> (l' = compl l \<or> l' = l)) \<and> r = merge (remove1 l' xs) (remove1 (compl l') ys)"
    9.73  using assms
    9.74  proof (induct xs ys arbitrary: r rule: res_thm'.induct)
    9.75 @@ -276,14 +276,14 @@
    9.76  (* There are five cases for res_thm: We will consider them one after another: *) 
    9.77    {
    9.78      assume cond: "x = l \<or> x = compl l"
    9.79 -    assume resolve2: "crel (resolve2 (compl x) xs (y # ys)) h h' r"   
    9.80 +    assume resolve2: "effect (resolve2 (compl x) xs (y # ys)) h h' r"   
    9.81      from resolve2_Inv [OF resolve2] cond have ?case
    9.82        apply -
    9.83        by (rule exI[of _ "x"]) fastsimp
    9.84    } moreover
    9.85    {
    9.86      assume cond: "\<not> (x = l \<or> x = compl l)" "y = l \<or> y = compl l" 
    9.87 -    assume resolve1: "crel (resolve1 (compl y) (x # xs) ys) h h' r"
    9.88 +    assume resolve1: "effect (resolve1 (compl y) (x # xs) ys) h h' r"
    9.89      from resolve1_Inv [OF resolve1] cond have ?case
    9.90        apply -
    9.91        by (rule exI[of _ "compl y"]) fastsimp
    9.92 @@ -291,28 +291,28 @@
    9.93    {
    9.94      fix r'
    9.95      assume cond: "\<not> (x = l \<or> x = compl l)" "\<not> (y = l \<or> y = compl l)" "x < y"
    9.96 -    assume res_thm: "crel (res_thm' l xs (y # ys)) h h' r'"
    9.97 +    assume res_thm: "effect (res_thm' l xs (y # ys)) h h' r'"
    9.98      assume return: "r = x # r'"
    9.99      from "1.hyps"(1) [OF cond res_thm] cond return have ?case by auto
   9.100    } moreover
   9.101    {
   9.102      fix r'
   9.103      assume cond: "\<not> (x = l \<or> x = compl l)" "\<not> (y = l \<or> y = compl l)" "\<not> x < y" "y < x"
   9.104 -    assume res_thm: "crel (res_thm' l (x # xs) ys) h h' r'"
   9.105 +    assume res_thm: "effect (res_thm' l (x # xs) ys) h h' r'"
   9.106      assume return: "r = y # r'"
   9.107      from "1.hyps"(2) [OF cond res_thm] cond return have ?case by auto
   9.108    } moreover
   9.109    {
   9.110      fix r'
   9.111      assume cond: "\<not> (x = l \<or> x = compl l)" "\<not> (y = l \<or> y = compl l)" "\<not> x < y" "\<not> y < x"
   9.112 -    assume res_thm: "crel (res_thm' l xs ys) h h' r'"
   9.113 +    assume res_thm: "effect (res_thm' l xs ys) h h' r'"
   9.114      assume return: "r = x # r'"
   9.115      from "1.hyps"(3) [OF cond res_thm] cond return have ?case by auto
   9.116    } moreover
   9.117    note "1.prems"
   9.118    ultimately show ?case
   9.119      unfolding res_thm'.simps
   9.120 -    apply (elim crel_bindE crel_ifE crel_returnE)
   9.121 +    apply (elim effect_bindE effect_ifE effect_returnE)
   9.122      apply simp
   9.123      apply simp
   9.124      apply simp
   9.125 @@ -323,72 +323,72 @@
   9.126    case (2 l ys r)
   9.127    thus ?case
   9.128      unfolding res_thm'.simps
   9.129 -    by (elim crel_raiseE) auto
   9.130 +    by (elim effect_raiseE) auto
   9.131  next
   9.132    case (3 l v va r)
   9.133    thus ?case
   9.134      unfolding res_thm'.simps
   9.135 -    by (elim crel_raiseE) auto
   9.136 +    by (elim effect_raiseE) auto
   9.137  qed
   9.138  
   9.139  lemma res_mem_no_heap:
   9.140 -assumes "crel (res_mem l xs) h h' r"
   9.141 +assumes "effect (res_mem l xs) h h' r"
   9.142    shows "h = h'"
   9.143  using assms
   9.144  apply (induct xs arbitrary: r)
   9.145  unfolding res_mem.simps
   9.146 -apply (elim crel_raiseE)
   9.147 +apply (elim effect_raiseE)
   9.148  apply auto
   9.149 -apply (elim crel_ifE crel_bindE crel_raiseE crel_returnE)
   9.150 +apply (elim effect_ifE effect_bindE effect_raiseE effect_returnE)
   9.151  apply auto
   9.152  done
   9.153  
   9.154  lemma resolve1_no_heap:
   9.155 -assumes "crel (resolve1 l xs ys) h h' r"
   9.156 +assumes "effect (resolve1 l xs ys) h h' r"
   9.157    shows "h = h'"
   9.158  using assms
   9.159  apply (induct xs ys arbitrary: r rule: resolve1.induct)
   9.160  unfolding resolve1.simps
   9.161 -apply (elim crel_bindE crel_ifE crel_returnE crel_raiseE)
   9.162 +apply (elim effect_bindE effect_ifE effect_returnE effect_raiseE)
   9.163  apply (auto simp add: res_mem_no_heap)
   9.164 -by (elim crel_raiseE) auto
   9.165 +by (elim effect_raiseE) auto
   9.166  
   9.167  lemma resolve2_no_heap:
   9.168 -assumes "crel (resolve2 l xs ys) h h' r"
   9.169 +assumes "effect (resolve2 l xs ys) h h' r"
   9.170    shows "h = h'"
   9.171  using assms
   9.172  apply (induct xs ys arbitrary: r rule: resolve2.induct)
   9.173  unfolding resolve2.simps
   9.174 -apply (elim crel_bindE crel_ifE crel_returnE crel_raiseE)
   9.175 +apply (elim effect_bindE effect_ifE effect_returnE effect_raiseE)
   9.176  apply (auto simp add: res_mem_no_heap)
   9.177 -by (elim crel_raiseE) auto
   9.178 +by (elim effect_raiseE) auto
   9.179  
   9.180  
   9.181  lemma res_thm'_no_heap:
   9.182 -  assumes "crel (res_thm' l xs ys) h h' r"
   9.183 +  assumes "effect (res_thm' l xs ys) h h' r"
   9.184    shows "h = h'"
   9.185    using assms
   9.186  proof (induct xs ys arbitrary: r rule: res_thm'.induct)
   9.187    case (1 l x xs y ys r)
   9.188    thus ?thesis
   9.189      unfolding res_thm'.simps
   9.190 -    by (elim crel_bindE crel_ifE crel_returnE)
   9.191 +    by (elim effect_bindE effect_ifE effect_returnE)
   9.192    (auto simp add: resolve1_no_heap resolve2_no_heap)
   9.193  next
   9.194    case (2 l ys r)
   9.195    thus ?case
   9.196      unfolding res_thm'.simps
   9.197 -    by (elim crel_raiseE) auto
   9.198 +    by (elim effect_raiseE) auto
   9.199  next
   9.200    case (3 l v va r)
   9.201    thus ?case
   9.202      unfolding res_thm'.simps
   9.203 -    by (elim crel_raiseE) auto
   9.204 +    by (elim effect_raiseE) auto
   9.205  qed
   9.206  
   9.207  
   9.208  lemma res_thm'_Inv2:
   9.209 -  assumes res_thm: "crel (res_thm' l xs ys) h h' rcl"
   9.210 +  assumes res_thm: "effect (res_thm' l xs ys) h h' rcl"
   9.211    assumes l_not_null: "l \<noteq> 0"
   9.212    assumes ys: "correctClause r ys \<and> sorted ys \<and> distinct ys"
   9.213    assumes xs: "correctClause r xs \<and> sorted xs \<and> distinct xs"
   9.214 @@ -459,20 +459,20 @@
   9.215                  else raise(''No empty clause''))
   9.216    }"
   9.217  
   9.218 -lemma crel_option_case:
   9.219 -  assumes "crel (case x of None \<Rightarrow> n | Some y \<Rightarrow> s y) h h' r"
   9.220 -  obtains "x = None" "crel n h h' r"
   9.221 -         | y where "x = Some y" "crel (s y) h h' r" 
   9.222 -  using assms unfolding crel_def by (auto split: option.splits)
   9.223 +lemma effect_option_case:
   9.224 +  assumes "effect (case x of None \<Rightarrow> n | Some y \<Rightarrow> s y) h h' r"
   9.225 +  obtains "x = None" "effect n h h' r"
   9.226 +         | y where "x = Some y" "effect (s y) h h' r" 
   9.227 +  using assms unfolding effect_def by (auto split: option.splits)
   9.228  
   9.229  lemma res_thm2_Inv:
   9.230 -  assumes res_thm: "crel (res_thm2 a (l, j) cli) h h' rs"
   9.231 +  assumes res_thm: "effect (res_thm2 a (l, j) cli) h h' rs"
   9.232    assumes correct_a: "correctArray r a h"
   9.233    assumes correct_cli: "correctClause r cli \<and> sorted cli \<and> distinct cli"
   9.234    shows "h = h' \<and> correctClause r rs \<and> sorted rs \<and> distinct rs"
   9.235  proof -
   9.236    from res_thm have l_not_zero: "l \<noteq> 0" 
   9.237 -    by (auto elim: crel_raiseE)
   9.238 +    by (auto elim: effect_raiseE)
   9.239    {
   9.240      fix clj
   9.241      let ?rs = "merge (remove l cli) (remove (compl l) clj)"
   9.242 @@ -494,17 +494,17 @@
   9.243      assume "Some clj = Array.get h a ! j" "j < Array.length h a"
   9.244      with correct_a have clj: "correctClause r clj \<and> sorted clj \<and> distinct clj"
   9.245        unfolding correctArray_def by (auto intro: array_ranI)
   9.246 -    assume "crel (res_thm' l cli clj) h h' rs"
   9.247 +    assume "effect (res_thm' l cli clj) h h' rs"
   9.248      from res_thm'_no_heap[OF this] res_thm'_Inv2[OF this l_not_zero clj correct_cli]
   9.249      have "h = h' \<and> correctClause r rs \<and> sorted rs \<and> distinct rs" by simp
   9.250    }
   9.251    with assms show ?thesis
   9.252      unfolding res_thm2.simps get_clause_def
   9.253 -    by (elim crel_bindE crel_ifE crel_nthE crel_raiseE crel_returnE crel_option_case) auto
   9.254 +    by (elim effect_bindE effect_ifE effect_nthE effect_raiseE effect_returnE effect_option_case) auto
   9.255  qed
   9.256  
   9.257  lemma foldM_Inv2:
   9.258 -  assumes "crel (foldM (res_thm2 a) rs cli) h h' rcl"
   9.259 +  assumes "effect (foldM (res_thm2 a) rs cli) h h' rcl"
   9.260    assumes correct_a: "correctArray r a h"
   9.261    assumes correct_cli: "correctClause r cli \<and> sorted cli \<and> distinct cli"
   9.262    shows "h = h' \<and> correctClause r rcl \<and> sorted rcl \<and> distinct rcl"
   9.263 @@ -512,39 +512,39 @@
   9.264  proof (induct rs arbitrary: h h' cli)
   9.265    case Nil thus ?case
   9.266      unfolding foldM.simps
   9.267 -    by (elim crel_returnE) auto
   9.268 +    by (elim effect_returnE) auto
   9.269  next
   9.270    case (Cons x xs)
   9.271    {
   9.272      fix h1 ret
   9.273      obtain l j where x_is: "x = (l, j)" by fastsimp
   9.274 -    assume res_thm2: "crel (res_thm2 a x cli) h h1 ret"
   9.275 -    with x_is have res_thm2': "crel (res_thm2 a (l, j) cli) h h1 ret" by simp
   9.276 +    assume res_thm2: "effect (res_thm2 a x cli) h h1 ret"
   9.277 +    with x_is have res_thm2': "effect (res_thm2 a (l, j) cli) h h1 ret" by simp
   9.278      note step = res_thm2_Inv [OF res_thm2' Cons.prems(2) Cons.prems(3)]
   9.279      from step have ret: "correctClause r ret \<and> sorted ret \<and> distinct ret" by simp
   9.280      from step Cons.prems(2) have correct_a: "correctArray r a h1"  by simp
   9.281 -    assume foldM: "crel (foldM (res_thm2 a) xs ret) h1 h' rcl"
   9.282 +    assume foldM: "effect (foldM (res_thm2 a) xs ret) h1 h' rcl"
   9.283      from step Cons.hyps [OF foldM correct_a ret] have
   9.284      "h = h' \<and> correctClause r rcl \<and> sorted rcl \<and> distinct rcl" by auto
   9.285    }
   9.286    with Cons show ?case
   9.287      unfolding foldM.simps
   9.288 -    by (elim crel_bindE) auto
   9.289 +    by (elim effect_bindE) auto
   9.290  qed
   9.291  
   9.292  
   9.293  lemma step_correct2:
   9.294 -  assumes crel: "crel (doProofStep2 a step rcs) h h' res"
   9.295 +  assumes effect: "effect (doProofStep2 a step rcs) h h' res"
   9.296    assumes correctArray: "correctArray rcs a h"
   9.297    shows "correctArray res a h'"
   9.298  proof (cases "(a,step,rcs)" rule: doProofStep2.cases)
   9.299    case (1 a saveTo i rs rcs)
   9.300 -  with crel correctArray
   9.301 +  with effect correctArray
   9.302    show ?thesis
   9.303      apply auto
   9.304 -    apply (auto simp: get_clause_def elim!: crel_bindE crel_nthE)
   9.305 -    apply (auto elim!: crel_bindE crel_nthE crel_option_case crel_raiseE
   9.306 -      crel_returnE crel_updE)
   9.307 +    apply (auto simp: get_clause_def elim!: effect_bindE effect_nthE)
   9.308 +    apply (auto elim!: effect_bindE effect_nthE effect_option_case effect_raiseE
   9.309 +      effect_returnE effect_updE)
   9.310      apply (frule foldM_Inv2)
   9.311      apply assumption
   9.312      apply (simp add: correctArray_def)
   9.313 @@ -553,42 +553,42 @@
   9.314      by (auto intro: correctArray_update)
   9.315  next
   9.316    case (2 a cid rcs)
   9.317 -  with crel correctArray
   9.318 +  with effect correctArray
   9.319    show ?thesis
   9.320 -    by (auto simp: correctArray_def elim!: crel_bindE crel_updE crel_returnE
   9.321 +    by (auto simp: correctArray_def elim!: effect_bindE effect_updE effect_returnE
   9.322       dest: array_ran_upd_array_None)
   9.323  next
   9.324    case (3 a cid c rcs)
   9.325 -  with crel correctArray
   9.326 +  with effect correctArray
   9.327    show ?thesis
   9.328 -    apply (auto elim!: crel_bindE crel_updE crel_returnE)
   9.329 +    apply (auto elim!: effect_bindE effect_updE effect_returnE)
   9.330      apply (auto simp: correctArray_def dest!: array_ran_upd_array_Some)
   9.331      apply (auto intro: correctClause_mono)
   9.332      by (auto simp: correctClause_def)
   9.333  next
   9.334    case 4
   9.335 -  with crel correctArray
   9.336 -  show ?thesis by (auto elim: crel_raiseE)
   9.337 +  with effect correctArray
   9.338 +  show ?thesis by (auto elim: effect_raiseE)
   9.339  next
   9.340    case 5
   9.341 -  with crel correctArray
   9.342 -  show ?thesis by (auto elim: crel_raiseE)
   9.343 +  with effect correctArray
   9.344 +  show ?thesis by (auto elim: effect_raiseE)
   9.345  qed
   9.346    
   9.347  
   9.348  theorem fold_steps_correct:
   9.349 -  assumes "crel (foldM (doProofStep2 a) steps rcs) h h' res"
   9.350 +  assumes "effect (foldM (doProofStep2 a) steps rcs) h h' res"
   9.351    assumes "correctArray rcs a h"
   9.352    shows "correctArray res a h'"
   9.353  using assms
   9.354  by (induct steps arbitrary: rcs h h' res)
   9.355 - (auto elim!: crel_bindE crel_returnE dest:step_correct2)
   9.356 + (auto elim!: effect_bindE effect_returnE dest:step_correct2)
   9.357  
   9.358  theorem checker_soundness:
   9.359 -  assumes "crel (checker n p i) h h' cs"
   9.360 +  assumes "effect (checker n p i) h h' cs"
   9.361    shows "inconsistent cs"
   9.362  using assms unfolding checker_def
   9.363 -apply (elim crel_bindE crel_nthE crel_ifE crel_returnE crel_raiseE crel_newE)
   9.364 +apply (elim effect_bindE effect_nthE effect_ifE effect_returnE effect_raiseE effect_newE)
   9.365  prefer 2 apply simp
   9.366  apply auto
   9.367  apply (drule fold_steps_correct)