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"