src/HOL/Imperative_HOL/Heap_Monad.thy
changeset 37758 bf86a65403a8
parent 37756 59caa6180fff
child 37771 1bec64044b5e
     1.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Jul 09 10:08:10 2010 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Jul 09 16:58:44 2010 +0200
     1.3 @@ -10,7 +10,7 @@
     1.4  
     1.5  subsection {* The monad *}
     1.6  
     1.7 -subsubsection {* Monad combinators *}
     1.8 +subsubsection {* Monad construction *}
     1.9  
    1.10  text {* Monadic heap actions either produce values
    1.11    and transform the heap, or fail *}
    1.12 @@ -19,6 +19,13 @@
    1.13  primrec execute :: "'a Heap \<Rightarrow> heap \<Rightarrow> ('a \<times> heap) option" where
    1.14    [code del]: "execute (Heap f) = f"
    1.15  
    1.16 +lemma Heap_cases [case_names succeed fail]:
    1.17 +  fixes f and h
    1.18 +  assumes succeed: "\<And>x h'. execute f h = Some (x, h') \<Longrightarrow> P"
    1.19 +  assumes fail: "execute f h = None \<Longrightarrow> P"
    1.20 +  shows P
    1.21 +  using assms by (cases "execute f h") auto
    1.22 +
    1.23  lemma Heap_execute [simp]:
    1.24    "Heap (execute f) = f" by (cases f) simp_all
    1.25  
    1.26 @@ -26,43 +33,98 @@
    1.27    "(\<And>h. execute f h = execute g h) \<Longrightarrow> f = g"
    1.28      by (cases f, cases g) (auto simp: expand_fun_eq)
    1.29  
    1.30 -lemma Heap_eqI':
    1.31 -  "(\<And>h. (\<lambda>x. execute (f x) h) = (\<lambda>y. execute (g y) h)) \<Longrightarrow> f = g"
    1.32 -    by (auto simp: expand_fun_eq intro: Heap_eqI)
    1.33 +ML {* structure Execute_Simps = Named_Thms(
    1.34 +  val name = "execute_simps"
    1.35 +  val description = "simplification rules for execute"
    1.36 +) *}
    1.37 +
    1.38 +setup Execute_Simps.setup
    1.39 +
    1.40 +lemma execute_Let [simp, execute_simps]:
    1.41 +  "execute (let x = t in f x) = (let x = t in execute (f x))"
    1.42 +  by (simp add: Let_def)
    1.43 +
    1.44 +
    1.45 +subsubsection {* Specialised lifters *}
    1.46 +
    1.47 +definition tap :: "(heap \<Rightarrow> 'a) \<Rightarrow> 'a Heap" where
    1.48 +  [code del]: "tap f = Heap (\<lambda>h. Some (f h, h))"
    1.49 +
    1.50 +lemma execute_tap [simp, execute_simps]:
    1.51 +  "execute (tap f) h = Some (f h, h)"
    1.52 +  by (simp add: tap_def)
    1.53  
    1.54  definition heap :: "(heap \<Rightarrow> 'a \<times> heap) \<Rightarrow> 'a Heap" where
    1.55    [code del]: "heap f = Heap (Some \<circ> f)"
    1.56  
    1.57 -lemma execute_heap [simp]:
    1.58 +lemma execute_heap [simp, execute_simps]:
    1.59    "execute (heap f) = Some \<circ> f"
    1.60    by (simp add: heap_def)
    1.61  
    1.62  definition guard :: "(heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> 'a \<times> heap) \<Rightarrow> 'a Heap" where
    1.63    [code del]: "guard P f = Heap (\<lambda>h. if P h then Some (f h) else None)"
    1.64  
    1.65 -lemma execute_guard [simp]:
    1.66 +lemma execute_guard [execute_simps]:
    1.67    "\<not> P h \<Longrightarrow> execute (guard P f) h = None"
    1.68    "P h \<Longrightarrow> execute (guard P f) h = Some (f h)"
    1.69    by (simp_all add: guard_def)
    1.70  
    1.71 -lemma heap_cases [case_names succeed fail]:
    1.72 -  fixes f and h
    1.73 -  assumes succeed: "\<And>x h'. execute f h = Some (x, h') \<Longrightarrow> P"
    1.74 -  assumes fail: "execute f h = None \<Longrightarrow> P"
    1.75 -  shows P
    1.76 -  using assms by (cases "execute f h") auto
    1.77 +
    1.78 +subsubsection {* Predicate classifying successful computations *}
    1.79 +
    1.80 +definition success :: "'a Heap \<Rightarrow> heap \<Rightarrow> bool" where
    1.81 +  "success f h \<longleftrightarrow> execute f h \<noteq> None"
    1.82 +
    1.83 +lemma successI:
    1.84 +  "execute f h \<noteq> None \<Longrightarrow> success f h"
    1.85 +  by (simp add: success_def)
    1.86 +
    1.87 +lemma successE:
    1.88 +  assumes "success f h"
    1.89 +  obtains r h' where "execute f h = Some (r, h')"
    1.90 +  using assms by (auto simp add: success_def)
    1.91 +
    1.92 +ML {* structure Success_Intros = Named_Thms(
    1.93 +  val name = "success_intros"
    1.94 +  val description = "introduction rules for success"
    1.95 +) *}
    1.96 +
    1.97 +setup Success_Intros.setup
    1.98 +
    1.99 +lemma success_tapI [iff, success_intros]:
   1.100 +  "success (tap f) h"
   1.101 +  by (rule successI) simp
   1.102 +
   1.103 +lemma success_heapI [iff, success_intros]:
   1.104 +  "success (heap f) h"
   1.105 +  by (rule successI) simp
   1.106 +
   1.107 +lemma success_guardI [success_intros]:
   1.108 +  "P h \<Longrightarrow> success (guard P f) h"
   1.109 +  by (rule successI) (simp add: execute_guard)
   1.110 +
   1.111 +lemma success_LetI [success_intros]:
   1.112 +  "x = t \<Longrightarrow> success (f x) h \<Longrightarrow> success (let x = t in f x) h"
   1.113 +  by (simp add: Let_def)
   1.114 +
   1.115 +
   1.116 +subsubsection {* Monad combinators *}
   1.117  
   1.118  definition return :: "'a \<Rightarrow> 'a Heap" where
   1.119    [code del]: "return x = heap (Pair x)"
   1.120  
   1.121 -lemma execute_return [simp]:
   1.122 +lemma execute_return [simp, execute_simps]:
   1.123    "execute (return x) = Some \<circ> Pair x"
   1.124    by (simp add: return_def)
   1.125  
   1.126 +lemma success_returnI [iff, success_intros]:
   1.127 +  "success (return x) h"
   1.128 +  by (rule successI) simp
   1.129 +
   1.130  definition raise :: "string \<Rightarrow> 'a Heap" where -- {* the string is just decoration *}
   1.131    [code del]: "raise s = Heap (\<lambda>_. None)"
   1.132  
   1.133 -lemma execute_raise [simp]:
   1.134 +lemma execute_raise [simp, execute_simps]:
   1.135    "execute (raise s) = (\<lambda>_. None)"
   1.136    by (simp add: raise_def)
   1.137  
   1.138 @@ -73,14 +135,18 @@
   1.139  
   1.140  notation bind (infixl "\<guillemotright>=" 54)
   1.141  
   1.142 -lemma execute_bind [simp]:
   1.143 +lemma execute_bind [execute_simps]:
   1.144    "execute f h = Some (x, h') \<Longrightarrow> execute (f \<guillemotright>= g) h = execute (g x) h'"
   1.145    "execute f h = None \<Longrightarrow> execute (f \<guillemotright>= g) h = None"
   1.146    by (simp_all add: bind_def)
   1.147  
   1.148 -lemma execute_bind_heap [simp]:
   1.149 -  "execute (heap f \<guillemotright>= g) h = execute (g (fst (f h))) (snd (f h))"
   1.150 -  by (simp add: bind_def split_def)
   1.151 +lemma success_bindI [success_intros]:
   1.152 +  "success f h \<Longrightarrow> success (g (fst (the (execute f h)))) (snd (the (execute f h))) \<Longrightarrow> success (f \<guillemotright>= g) h"
   1.153 +  by (auto intro!: successI elim!: successE simp add: bind_def)
   1.154 +
   1.155 +lemma execute_bind_successI [execute_simps]:
   1.156 +  "success f h \<Longrightarrow> execute (f \<guillemotright>= g) h = execute (g (fst (the (execute f h)))) (snd (the (execute f h)))"
   1.157 +  by (cases f h rule: Heap_cases) (auto elim!: successE simp add: bind_def)
   1.158    
   1.159  lemma execute_eq_SomeI:
   1.160    assumes "Heap_Monad.execute f h = Some (x, h')"
   1.161 @@ -89,7 +155,7 @@
   1.162    using assms by (simp add: bind_def)
   1.163  
   1.164  lemma return_bind [simp]: "return x \<guillemotright>= f = f x"
   1.165 -  by (rule Heap_eqI) simp
   1.166 +  by (rule Heap_eqI) (simp add: execute_bind)
   1.167  
   1.168  lemma bind_return [simp]: "f \<guillemotright>= return = f"
   1.169    by (rule Heap_eqI) (simp add: bind_def split: option.splits)
   1.170 @@ -98,7 +164,7 @@
   1.171    by (rule Heap_eqI) (simp add: bind_def split: option.splits)
   1.172  
   1.173  lemma raise_bind [simp]: "raise e \<guillemotright>= f = raise e"
   1.174 -  by (rule Heap_eqI) simp
   1.175 +  by (rule Heap_eqI) (simp add: execute_bind)
   1.176  
   1.177  abbreviation chain :: "'a Heap \<Rightarrow> 'b Heap \<Rightarrow> 'b Heap"  (infixl ">>" 54) where
   1.178    "f >> g \<equiv> f >>= (\<lambda>_. g)"
   1.179 @@ -187,24 +253,31 @@
   1.180  *}
   1.181  
   1.182  
   1.183 -subsection {* Monad properties *}
   1.184 +subsection {* Generic combinators *}
   1.185  
   1.186 -subsection {* Generic combinators *}
   1.187 +subsubsection {* Assertions *}
   1.188  
   1.189  definition assert :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a Heap" where
   1.190    "assert P x = (if P x then return x else raise ''assert'')"
   1.191  
   1.192 -lemma execute_assert [simp]:
   1.193 +lemma execute_assert [execute_simps]:
   1.194    "P x \<Longrightarrow> execute (assert P x) h = Some (x, h)"
   1.195    "\<not> P x \<Longrightarrow> execute (assert P x) h = None"
   1.196    by (simp_all add: assert_def)
   1.197  
   1.198 +lemma success_assertI [success_intros]:
   1.199 +  "P x \<Longrightarrow> success (assert P x) h"
   1.200 +  by (rule successI) (simp add: execute_assert)
   1.201 +
   1.202  lemma assert_cong [fundef_cong]:
   1.203    assumes "P = P'"
   1.204    assumes "\<And>x. P' x \<Longrightarrow> f x = f' x"
   1.205    shows "(assert P x >>= f) = (assert P' x >>= f')"
   1.206    by (rule Heap_eqI) (insert assms, simp add: assert_def)
   1.207  
   1.208 +
   1.209 +subsubsection {* Plain lifting *}
   1.210 +
   1.211  definition lift :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b Heap" where
   1.212    "lift f = return o f"
   1.213  
   1.214 @@ -216,6 +289,9 @@
   1.215    "(f \<guillemotright>= lift g) = (f \<guillemotright>= (\<lambda>x. return (g x)))"
   1.216    by (simp add: lift_def comp_def)
   1.217  
   1.218 +
   1.219 +subsubsection {* Iteration -- warning: this is rarely useful! *}
   1.220 +
   1.221  primrec fold_map :: "('a \<Rightarrow> 'b Heap) \<Rightarrow> 'a list \<Rightarrow> 'b list Heap" where
   1.222    "fold_map f [] = return []"
   1.223  | "fold_map f (x # xs) = do
   1.224 @@ -228,7 +304,7 @@
   1.225    "fold_map f (xs @ ys) = fold_map f xs \<guillemotright>= (\<lambda>xs. fold_map f ys \<guillemotright>= (\<lambda>ys. return (xs @ ys)))"
   1.226    by (induct xs) simp_all
   1.227  
   1.228 -lemma execute_fold_map_unchanged_heap:
   1.229 +lemma execute_fold_map_unchanged_heap [execute_simps]:
   1.230    assumes "\<And>x. x \<in> set xs \<Longrightarrow> \<exists>y. execute (f x) h = Some (y, h)"
   1.231    shows "execute (fold_map f xs) h =
   1.232      Some (List.map (\<lambda>x. fst (the (execute (f x) h))) xs, h)"
   1.233 @@ -527,6 +603,6 @@
   1.234  code_const return (Haskell "return")
   1.235  code_const Heap_Monad.raise' (Haskell "error/ _")
   1.236  
   1.237 -hide_const (open) Heap heap guard execute raise' fold_map
   1.238 +hide_const (open) Heap heap guard raise' fold_map
   1.239  
   1.240  end