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.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'"
```