src/HOL/Imperative_HOL/Heap_Monad.thy
 changeset 37771 1bec64044b5e parent 37758 bf86a65403a8 child 37772 026ed2fc15d4
```     1.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Mon Jul 12 11:39:27 2010 +0200
1.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Mon Jul 12 16:05:08 2010 +0200
1.3 @@ -2,7 +2,7 @@
1.4      Author:     John Matthews, Galois Connections; Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen
1.5  *)
1.6
1.7 -header {* A monad with a polymorphic heap *}
1.8 +header {* A monad with a polymorphic heap and primitive reasoning infrastructure *}
1.9
1.10  theory Heap_Monad
1.11  imports Heap
1.12 @@ -81,8 +81,10 @@
1.13
1.14  lemma successE:
1.15    assumes "success f h"
1.16 -  obtains r h' where "execute f h = Some (r, h')"
1.17 -  using assms by (auto simp add: success_def)
1.18 +  obtains r h' where "r = fst (the (execute c h))"
1.19 +    and "h' = snd (the (execute c h))"
1.20 +    and "execute f h \<noteq> None"
1.21 +  using assms by (simp add: success_def)
1.22
1.23  ML {* structure Success_Intros = Named_Thms(
1.24    val name = "success_intros"
1.25 @@ -107,6 +109,121 @@
1.26    "x = t \<Longrightarrow> success (f x) h \<Longrightarrow> success (let x = t in f x) h"
1.27    by (simp add: Let_def)
1.28
1.29 +lemma success_ifI:
1.30 +  "(c \<Longrightarrow> success t h) \<Longrightarrow> (\<not> c \<Longrightarrow> success e h) \<Longrightarrow>
1.31 +    success (if c then t else e) h"
1.32 +  by (simp add: success_def)
1.33 +
1.34 +
1.35 +subsubsection {* Predicate for a simple relational calculus *}
1.36 +
1.37 +text {*
1.38 +  The @{text crel} predicate states that when a computation @{text c}
1.39 +  runs with the heap @{text h} will result in return value @{text r}
1.40 +  and a heap @{text "h'"}, i.e.~no exception occurs.
1.41 +*}
1.42 +
1.43 +definition crel :: "'a Heap \<Rightarrow> heap \<Rightarrow> heap \<Rightarrow> 'a \<Rightarrow> bool" where
1.44 +  crel_def: "crel c h h' r \<longleftrightarrow> Heap_Monad.execute c h = Some (r, h')"
1.45 +
1.46 +lemma crelI:
1.47 +  "Heap_Monad.execute c h = Some (r, h') \<Longrightarrow> crel c h h' r"
1.48 +  by (simp add: crel_def)
1.49 +
1.50 +lemma crelE:
1.51 +  assumes "crel c h h' r"
1.52 +  obtains "r = fst (the (execute c h))"
1.53 +    and "h' = snd (the (execute c h))"
1.54 +    and "success c h"
1.55 +proof (rule that)
1.56 +  from assms have *: "execute c h = Some (r, h')" by (simp add: crel_def)
1.57 +  then show "success c h" by (simp add: success_def)
1.58 +  from * have "fst (the (execute c h)) = r" and "snd (the (execute c h)) = h'"
1.59 +    by simp_all
1.60 +  then show "r = fst (the (execute c h))"
1.61 +    and "h' = snd (the (execute c h))" by simp_all
1.62 +qed
1.63 +
1.64 +lemma crel_success:
1.65 +  "crel c h h' r \<Longrightarrow> success c h"
1.66 +  by (simp add: crel_def success_def)
1.67 +
1.68 +lemma success_crelE:
1.69 +  assumes "success c h"
1.70 +  obtains r h' where "crel c h h' r"
1.71 +  using assms by (auto simp add: crel_def success_def)
1.72 +
1.73 +lemma crel_deterministic:
1.74 +  assumes "crel f h h' a"
1.75 +    and "crel f h h'' b"
1.76 +  shows "a = b" and "h' = h''"
1.77 +  using assms unfolding crel_def by auto
1.78 +
1.79 +ML {* structure Crel_Intros = Named_Thms(
1.80 +  val name = "crel_intros"
1.81 +  val description = "introduction rules for crel"
1.82 +) *}
1.83 +
1.84 +ML {* structure Crel_Elims = Named_Thms(
1.85 +  val name = "crel_elims"
1.86 +  val description = "elimination rules for crel"
1.87 +) *}
1.88 +
1.89 +setup "Crel_Intros.setup #> Crel_Elims.setup"
1.90 +
1.91 +lemma crel_LetI [crel_intros]:
1.92 +  assumes "x = t" "crel (f x) h h' r"
1.93 +  shows "crel (let x = t in f x) h h' r"
1.94 +  using assms by simp
1.95 +
1.96 +lemma crel_LetE [crel_elims]:
1.97 +  assumes "crel (let x = t in f x) h h' r"
1.98 +  obtains "crel (f t) h h' r"
1.99 +  using assms by simp
1.100 +
1.101 +lemma crel_ifI:
1.102 +  assumes "c \<Longrightarrow> crel t h h' r"
1.103 +    and "\<not> c \<Longrightarrow> crel e h h' r"
1.104 +  shows "crel (if c then t else e) h h' r"
1.105 +  by (cases c) (simp_all add: assms)
1.106 +
1.107 +lemma crel_ifE:
1.108 +  assumes "crel (if c then t else e) h h' r"
1.109 +  obtains "c" "crel t h h' r"
1.110 +    | "\<not> c" "crel e h h' r"
1.111 +  using assms by (cases c) simp_all
1.112 +
1.113 +lemma crel_tapI [crel_intros]:
1.114 +  assumes "h' = h" "r = f h"
1.115 +  shows "crel (tap f) h h' r"
1.116 +  by (rule crelI) (simp add: assms)
1.117 +
1.118 +lemma crel_tapE [crel_elims]:
1.119 +  assumes "crel (tap f) h h' r"
1.120 +  obtains "h' = h" and "r = f h"
1.121 +  using assms by (rule crelE) auto
1.122 +
1.123 +lemma crel_heapI [crel_intros]:
1.124 +  assumes "h' = snd (f h)" "r = fst (f h)"
1.125 +  shows "crel (heap f) h h' r"
1.126 +  by (rule crelI) (simp add: assms)
1.127 +
1.128 +lemma crel_heapE [crel_elims]:
1.129 +  assumes "crel (heap f) h h' r"
1.130 +  obtains "h' = snd (f h)" and "r = fst (f h)"
1.131 +  using assms by (rule crelE) simp
1.132 +
1.133 +lemma crel_guardI [crel_intros]:
1.134 +  assumes "P h" "h' = snd (f h)" "r = fst (f h)"
1.135 +  shows "crel (guard P f) h h' r"
1.136 +  by (rule crelI) (simp add: assms execute_simps)
1.137 +
1.138 +lemma crel_guardE [crel_elims]:
1.139 +  assumes "crel (guard P f) h h' r"
1.140 +  obtains "h' = snd (f h)" "r = fst (f h)" "P h"
1.141 +  using assms by (rule crelE)
1.142 +    (auto simp add: execute_simps elim!: successE, cases "P h", auto simp add: execute_simps)
1.143 +
1.144
1.145  subsubsection {* Monad combinators *}
1.146
1.147 @@ -121,6 +238,15 @@
1.148    "success (return x) h"
1.149    by (rule successI) simp
1.150
1.151 +lemma crel_returnI [crel_intros]:
1.152 +  "h = h' \<Longrightarrow> crel (return x) h h' x"
1.153 +  by (rule crelI) simp
1.154 +
1.155 +lemma crel_returnE [crel_elims]:
1.156 +  assumes "crel (return x) h h' r"
1.157 +  obtains "r = x" "h' = h"
1.158 +  using assms by (rule crelE) simp
1.159 +
1.160  definition raise :: "string \<Rightarrow> 'a Heap" where -- {* the string is just decoration *}
1.161    [code del]: "raise s = Heap (\<lambda>_. None)"
1.162
1.163 @@ -128,6 +254,11 @@
1.164    "execute (raise s) = (\<lambda>_. None)"
1.165    by (simp add: raise_def)
1.166
1.167 +lemma crel_raiseE [crel_elims]:
1.168 +  assumes "crel (raise x) h h' r"
1.169 +  obtains "False"
1.170 +  using assms by (rule crelE) (simp add: success_def)
1.171 +
1.172  definition bind :: "'a Heap \<Rightarrow> ('a \<Rightarrow> 'b Heap) \<Rightarrow> 'b Heap" (infixl ">>=" 54) where
1.173    [code del]: "f >>= g = Heap (\<lambda>h. case execute f h of
1.174                    Some (x, h') \<Rightarrow> execute (g x) h'
1.175 @@ -140,15 +271,32 @@
1.176    "execute f h = None \<Longrightarrow> execute (f \<guillemotright>= g) h = None"
1.177    by (simp_all add: bind_def)
1.178
1.179 -lemma success_bindI [success_intros]:
1.180 -  "success f h \<Longrightarrow> success (g (fst (the (execute f h)))) (snd (the (execute f h))) \<Longrightarrow> success (f \<guillemotright>= g) h"
1.181 +lemma execute_bind_success:
1.182 +  "success f h \<Longrightarrow> execute (f \<guillemotright>= g) h = execute (g (fst (the (execute f h)))) (snd (the (execute f h)))"
1.183 +  by (cases f h rule: Heap_cases) (auto elim!: successE simp add: bind_def)
1.184 +
1.185 +lemma success_bind_executeI:
1.186 +  "execute f h = Some (x, h') \<Longrightarrow> success (g x) h' \<Longrightarrow> success (f \<guillemotright>= g) h"
1.187    by (auto intro!: successI elim!: successE simp add: bind_def)
1.188
1.189 -lemma execute_bind_successI [execute_simps]:
1.190 -  "success f h \<Longrightarrow> execute (f \<guillemotright>= g) h = execute (g (fst (the (execute f h)))) (snd (the (execute f h)))"
1.191 -  by (cases f h rule: Heap_cases) (auto elim!: successE simp add: bind_def)
1.192 -
1.193 -lemma execute_eq_SomeI:
1.194 +lemma success_bind_crelI [success_intros]:
1.195 +  "crel f h h' x \<Longrightarrow> success (g x) h' \<Longrightarrow> success (f \<guillemotright>= g) h"
1.196 +  by (auto simp add: crel_def success_def bind_def)
1.197 +
1.198 +lemma crel_bindI [crel_intros]:
1.199 +  assumes "crel f h h' r" "crel (g r) h' h'' r'"
1.200 +  shows "crel (f \<guillemotright>= g) h h'' r'"
1.201 +  using assms
1.202 +  apply (auto intro!: crelI elim!: crelE successE)
1.203 +  apply (subst execute_bind, simp_all)
1.204 +  done
1.205 +
1.206 +lemma crel_bindE [crel_elims]:
1.207 +  assumes "crel (f \<guillemotright>= g) h h'' r'"
1.208 +  obtains h' r where "crel f h h' r" "crel (g r) h' h'' r'"
1.209 +  using assms by (auto simp add: crel_def bind_def split: option.split_asm)
1.210 +
1.211 +lemma execute_bind_eq_SomeI:
1.212    assumes "Heap_Monad.execute f h = Some (x, h')"
1.213      and "Heap_Monad.execute (g x) h' = Some (y, h'')"
1.214    shows "Heap_Monad.execute (f \<guillemotright>= g) h = Some (y, h'')"
1.215 @@ -269,6 +417,15 @@
1.216    "P x \<Longrightarrow> success (assert P x) h"
1.217    by (rule successI) (simp add: execute_assert)
1.218
1.219 +lemma crel_assertI [crel_intros]:
1.220 +  "P x \<Longrightarrow> h' = h \<Longrightarrow> r = x \<Longrightarrow> crel (assert P x) h h' r"
1.221 +  by (rule crelI) (simp add: execute_assert)
1.222 +
1.223 +lemma crel_assertE [crel_elims]:
1.224 +  assumes "crel (assert P x) h h' r"
1.225 +  obtains "P x" "r = x" "h' = h"
1.226 +  using assms by (rule crelE) (cases "P x", simp_all add: execute_assert success_def)
1.227 +
1.228  lemma assert_cong [fundef_cong]:
1.229    assumes "P = P'"
1.230    assumes "\<And>x. P' x \<Longrightarrow> f x = f' x"
```