src/HOL/Imperative_HOL/Heap_Monad.thy
changeset 40671 5e46057ba8e0
parent 40267 a03e288d7902
child 41413 64cd30d6b0b8
     1.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Mon Nov 22 09:19:34 2010 +0100
     1.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Mon Nov 22 09:37:39 2010 +0100
     1.3 @@ -122,25 +122,25 @@
     1.4  subsubsection {* Predicate for a simple relational calculus *}
     1.5  
     1.6  text {*
     1.7 -  The @{text crel} predicate states that when a computation @{text c}
     1.8 +  The @{text effect} predicate states that when a computation @{text c}
     1.9    runs with the heap @{text h} will result in return value @{text r}
    1.10    and a heap @{text "h'"}, i.e.~no exception occurs.
    1.11  *}  
    1.12  
    1.13 -definition crel :: "'a Heap \<Rightarrow> heap \<Rightarrow> heap \<Rightarrow> 'a \<Rightarrow> bool" where
    1.14 -  crel_def: "crel c h h' r \<longleftrightarrow> execute c h = Some (r, h')"
    1.15 +definition effect :: "'a Heap \<Rightarrow> heap \<Rightarrow> heap \<Rightarrow> 'a \<Rightarrow> bool" where
    1.16 +  effect_def: "effect c h h' r \<longleftrightarrow> execute c h = Some (r, h')"
    1.17  
    1.18 -lemma crelI:
    1.19 -  "execute c h = Some (r, h') \<Longrightarrow> crel c h h' r"
    1.20 -  by (simp add: crel_def)
    1.21 +lemma effectI:
    1.22 +  "execute c h = Some (r, h') \<Longrightarrow> effect c h h' r"
    1.23 +  by (simp add: effect_def)
    1.24  
    1.25 -lemma crelE:
    1.26 -  assumes "crel c h h' r"
    1.27 +lemma effectE:
    1.28 +  assumes "effect c h h' r"
    1.29    obtains "r = fst (the (execute c h))"
    1.30      and "h' = snd (the (execute c h))"
    1.31      and "success c h"
    1.32  proof (rule that)
    1.33 -  from assms have *: "execute c h = Some (r, h')" by (simp add: crel_def)
    1.34 +  from assms have *: "execute c h = Some (r, h')" by (simp add: effect_def)
    1.35    then show "success c h" by (simp add: success_def)
    1.36    from * have "fst (the (execute c h)) = r" and "snd (the (execute c h)) = h'"
    1.37      by simp_all
    1.38 @@ -148,84 +148,84 @@
    1.39      and "h' = snd (the (execute c h))" by simp_all
    1.40  qed
    1.41  
    1.42 -lemma crel_success:
    1.43 -  "crel c h h' r \<Longrightarrow> success c h"
    1.44 -  by (simp add: crel_def success_def)
    1.45 +lemma effect_success:
    1.46 +  "effect c h h' r \<Longrightarrow> success c h"
    1.47 +  by (simp add: effect_def success_def)
    1.48  
    1.49 -lemma success_crelE:
    1.50 +lemma success_effectE:
    1.51    assumes "success c h"
    1.52 -  obtains r h' where "crel c h h' r"
    1.53 -  using assms by (auto simp add: crel_def success_def)
    1.54 +  obtains r h' where "effect c h h' r"
    1.55 +  using assms by (auto simp add: effect_def success_def)
    1.56  
    1.57 -lemma crel_deterministic:
    1.58 -  assumes "crel f h h' a"
    1.59 -    and "crel f h h'' b"
    1.60 +lemma effect_deterministic:
    1.61 +  assumes "effect f h h' a"
    1.62 +    and "effect f h h'' b"
    1.63    shows "a = b" and "h' = h''"
    1.64 -  using assms unfolding crel_def by auto
    1.65 +  using assms unfolding effect_def by auto
    1.66  
    1.67  ML {* structure Crel_Intros = Named_Thms(
    1.68 -  val name = "crel_intros"
    1.69 -  val description = "introduction rules for crel"
    1.70 +  val name = "effect_intros"
    1.71 +  val description = "introduction rules for effect"
    1.72  ) *}
    1.73  
    1.74  ML {* structure Crel_Elims = Named_Thms(
    1.75 -  val name = "crel_elims"
    1.76 -  val description = "elimination rules for crel"
    1.77 +  val name = "effect_elims"
    1.78 +  val description = "elimination rules for effect"
    1.79  ) *}
    1.80  
    1.81  setup "Crel_Intros.setup #> Crel_Elims.setup"
    1.82  
    1.83 -lemma crel_LetI [crel_intros]:
    1.84 -  assumes "x = t" "crel (f x) h h' r"
    1.85 -  shows "crel (let x = t in f x) h h' r"
    1.86 +lemma effect_LetI [effect_intros]:
    1.87 +  assumes "x = t" "effect (f x) h h' r"
    1.88 +  shows "effect (let x = t in f x) h h' r"
    1.89    using assms by simp
    1.90  
    1.91 -lemma crel_LetE [crel_elims]:
    1.92 -  assumes "crel (let x = t in f x) h h' r"
    1.93 -  obtains "crel (f t) h h' r"
    1.94 +lemma effect_LetE [effect_elims]:
    1.95 +  assumes "effect (let x = t in f x) h h' r"
    1.96 +  obtains "effect (f t) h h' r"
    1.97    using assms by simp
    1.98  
    1.99 -lemma crel_ifI:
   1.100 -  assumes "c \<Longrightarrow> crel t h h' r"
   1.101 -    and "\<not> c \<Longrightarrow> crel e h h' r"
   1.102 -  shows "crel (if c then t else e) h h' r"
   1.103 +lemma effect_ifI:
   1.104 +  assumes "c \<Longrightarrow> effect t h h' r"
   1.105 +    and "\<not> c \<Longrightarrow> effect e h h' r"
   1.106 +  shows "effect (if c then t else e) h h' r"
   1.107    by (cases c) (simp_all add: assms)
   1.108  
   1.109 -lemma crel_ifE:
   1.110 -  assumes "crel (if c then t else e) h h' r"
   1.111 -  obtains "c" "crel t h h' r"
   1.112 -    | "\<not> c" "crel e h h' r"
   1.113 +lemma effect_ifE:
   1.114 +  assumes "effect (if c then t else e) h h' r"
   1.115 +  obtains "c" "effect t h h' r"
   1.116 +    | "\<not> c" "effect e h h' r"
   1.117    using assms by (cases c) simp_all
   1.118  
   1.119 -lemma crel_tapI [crel_intros]:
   1.120 +lemma effect_tapI [effect_intros]:
   1.121    assumes "h' = h" "r = f h"
   1.122 -  shows "crel (tap f) h h' r"
   1.123 -  by (rule crelI) (simp add: assms execute_simps)
   1.124 +  shows "effect (tap f) h h' r"
   1.125 +  by (rule effectI) (simp add: assms execute_simps)
   1.126  
   1.127 -lemma crel_tapE [crel_elims]:
   1.128 -  assumes "crel (tap f) h h' r"
   1.129 +lemma effect_tapE [effect_elims]:
   1.130 +  assumes "effect (tap f) h h' r"
   1.131    obtains "h' = h" and "r = f h"
   1.132 -  using assms by (rule crelE) (auto simp add: execute_simps)
   1.133 +  using assms by (rule effectE) (auto simp add: execute_simps)
   1.134  
   1.135 -lemma crel_heapI [crel_intros]:
   1.136 +lemma effect_heapI [effect_intros]:
   1.137    assumes "h' = snd (f h)" "r = fst (f h)"
   1.138 -  shows "crel (heap f) h h' r"
   1.139 -  by (rule crelI) (simp add: assms execute_simps)
   1.140 +  shows "effect (heap f) h h' r"
   1.141 +  by (rule effectI) (simp add: assms execute_simps)
   1.142  
   1.143 -lemma crel_heapE [crel_elims]:
   1.144 -  assumes "crel (heap f) h h' r"
   1.145 +lemma effect_heapE [effect_elims]:
   1.146 +  assumes "effect (heap f) h h' r"
   1.147    obtains "h' = snd (f h)" and "r = fst (f h)"
   1.148 -  using assms by (rule crelE) (simp add: execute_simps)
   1.149 +  using assms by (rule effectE) (simp add: execute_simps)
   1.150  
   1.151 -lemma crel_guardI [crel_intros]:
   1.152 +lemma effect_guardI [effect_intros]:
   1.153    assumes "P h" "h' = snd (f h)" "r = fst (f h)"
   1.154 -  shows "crel (guard P f) h h' r"
   1.155 -  by (rule crelI) (simp add: assms execute_simps)
   1.156 +  shows "effect (guard P f) h h' r"
   1.157 +  by (rule effectI) (simp add: assms execute_simps)
   1.158  
   1.159 -lemma crel_guardE [crel_elims]:
   1.160 -  assumes "crel (guard P f) h h' r"
   1.161 +lemma effect_guardE [effect_elims]:
   1.162 +  assumes "effect (guard P f) h h' r"
   1.163    obtains "h' = snd (f h)" "r = fst (f h)" "P h"
   1.164 -  using assms by (rule crelE)
   1.165 +  using assms by (rule effectE)
   1.166      (auto simp add: execute_simps elim!: successE, cases "P h", auto simp add: execute_simps)
   1.167  
   1.168  
   1.169 @@ -242,14 +242,14 @@
   1.170    "success (return x) h"
   1.171    by (rule successI) (simp add: execute_simps)
   1.172  
   1.173 -lemma crel_returnI [crel_intros]:
   1.174 -  "h = h' \<Longrightarrow> crel (return x) h h' x"
   1.175 -  by (rule crelI) (simp add: execute_simps)
   1.176 +lemma effect_returnI [effect_intros]:
   1.177 +  "h = h' \<Longrightarrow> effect (return x) h h' x"
   1.178 +  by (rule effectI) (simp add: execute_simps)
   1.179  
   1.180 -lemma crel_returnE [crel_elims]:
   1.181 -  assumes "crel (return x) h h' r"
   1.182 +lemma effect_returnE [effect_elims]:
   1.183 +  assumes "effect (return x) h h' r"
   1.184    obtains "r = x" "h' = h"
   1.185 -  using assms by (rule crelE) (simp add: execute_simps)
   1.186 +  using assms by (rule effectE) (simp add: execute_simps)
   1.187  
   1.188  definition raise :: "string \<Rightarrow> 'a Heap" where -- {* the string is just decoration *}
   1.189    [code del]: "raise s = Heap (\<lambda>_. None)"
   1.190 @@ -258,10 +258,10 @@
   1.191    "execute (raise s) = (\<lambda>_. None)"
   1.192    by (simp add: raise_def)
   1.193  
   1.194 -lemma crel_raiseE [crel_elims]:
   1.195 -  assumes "crel (raise x) h h' r"
   1.196 +lemma effect_raiseE [effect_elims]:
   1.197 +  assumes "effect (raise x) h h' r"
   1.198    obtains "False"
   1.199 -  using assms by (rule crelE) (simp add: success_def execute_simps)
   1.200 +  using assms by (rule effectE) (simp add: success_def execute_simps)
   1.201  
   1.202  definition bind :: "'a Heap \<Rightarrow> ('a \<Rightarrow> 'b Heap) \<Rightarrow> 'b Heap" where
   1.203    [code del]: "bind f g = Heap (\<lambda>h. case execute f h of
   1.204 @@ -291,22 +291,22 @@
   1.205    "execute f h = Some (x, h') \<Longrightarrow> success (g x) h' \<Longrightarrow> success (f \<guillemotright>= g) h"
   1.206    by (auto intro!: successI elim!: successE simp add: bind_def)
   1.207  
   1.208 -lemma success_bind_crelI [success_intros]:
   1.209 -  "crel f h h' x \<Longrightarrow> success (g x) h' \<Longrightarrow> success (f \<guillemotright>= g) h"
   1.210 -  by (auto simp add: crel_def success_def bind_def)
   1.211 +lemma success_bind_effectI [success_intros]:
   1.212 +  "effect f h h' x \<Longrightarrow> success (g x) h' \<Longrightarrow> success (f \<guillemotright>= g) h"
   1.213 +  by (auto simp add: effect_def success_def bind_def)
   1.214  
   1.215 -lemma crel_bindI [crel_intros]:
   1.216 -  assumes "crel f h h' r" "crel (g r) h' h'' r'"
   1.217 -  shows "crel (f \<guillemotright>= g) h h'' r'"
   1.218 +lemma effect_bindI [effect_intros]:
   1.219 +  assumes "effect f h h' r" "effect (g r) h' h'' r'"
   1.220 +  shows "effect (f \<guillemotright>= g) h h'' r'"
   1.221    using assms
   1.222 -  apply (auto intro!: crelI elim!: crelE successE)
   1.223 +  apply (auto intro!: effectI elim!: effectE successE)
   1.224    apply (subst execute_bind, simp_all)
   1.225    done
   1.226  
   1.227 -lemma crel_bindE [crel_elims]:
   1.228 -  assumes "crel (f \<guillemotright>= g) h h'' r'"
   1.229 -  obtains h' r where "crel f h h' r" "crel (g r) h' h'' r'"
   1.230 -  using assms by (auto simp add: crel_def bind_def split: option.split_asm)
   1.231 +lemma effect_bindE [effect_elims]:
   1.232 +  assumes "effect (f \<guillemotright>= g) h h'' r'"
   1.233 +  obtains h' r where "effect f h h' r" "effect (g r) h' h'' r'"
   1.234 +  using assms by (auto simp add: effect_def bind_def split: option.split_asm)
   1.235  
   1.236  lemma execute_bind_eq_SomeI:
   1.237    assumes "execute f h = Some (x, h')"
   1.238 @@ -343,14 +343,14 @@
   1.239    "P x \<Longrightarrow> success (assert P x) h"
   1.240    by (rule successI) (simp add: execute_assert)
   1.241  
   1.242 -lemma crel_assertI [crel_intros]:
   1.243 -  "P x \<Longrightarrow> h' = h \<Longrightarrow> r = x \<Longrightarrow> crel (assert P x) h h' r"
   1.244 -  by (rule crelI) (simp add: execute_assert)
   1.245 +lemma effect_assertI [effect_intros]:
   1.246 +  "P x \<Longrightarrow> h' = h \<Longrightarrow> r = x \<Longrightarrow> effect (assert P x) h h' r"
   1.247 +  by (rule effectI) (simp add: execute_assert)
   1.248   
   1.249 -lemma crel_assertE [crel_elims]:
   1.250 -  assumes "crel (assert P x) h h' r"
   1.251 +lemma effect_assertE [effect_elims]:
   1.252 +  assumes "effect (assert P x) h h' r"
   1.253    obtains "P x" "r = x" "h' = h"
   1.254 -  using assms by (rule crelE) (cases "P x", simp_all add: execute_assert success_def)
   1.255 +  using assms by (rule effectE) (cases "P x", simp_all add: execute_assert success_def)
   1.256  
   1.257  lemma assert_cong [fundef_cong]:
   1.258    assumes "P = P'"