1.1 --- a/src/HOL/Imperative_HOL/Array.thy Mon Jul 05 10:42:27 2010 +0200
1.2 +++ b/src/HOL/Imperative_HOL/Array.thy Mon Jul 05 14:34:28 2010 +0200
1.3 @@ -28,7 +28,7 @@
1.4 [code del]: "nth a i = (do len \<leftarrow> length a;
1.5 (if i < len
1.6 then Heap_Monad.heap (\<lambda>h. (get_array a h ! i, h))
1.7 - else raise (''array lookup: index out of range''))
1.8 + else raise ''array lookup: index out of range'')
1.9 done)"
1.10
1.11 definition
1.12 @@ -37,18 +37,12 @@
1.13 [code del]: "upd i x a = (do len \<leftarrow> length a;
1.14 (if i < len
1.15 then Heap_Monad.heap (\<lambda>h. (a, Heap.upd a i x h))
1.16 - else raise (''array update: index out of range''))
1.17 + else raise ''array update: index out of range'')
1.18 done)"
1.19
1.20 lemma upd_return:
1.21 "upd i x a \<guillemotright> return a = upd i x a"
1.22 -proof (rule Heap_eqI)
1.23 - fix h
1.24 - obtain len h' where "Heap_Monad.execute (Array.length a) h = (len, h')"
1.25 - by (cases "Heap_Monad.execute (Array.length a) h")
1.26 - then show "Heap_Monad.execute (upd i x a \<guillemotright> return a) h = Heap_Monad.execute (upd i x a) h"
1.27 - by (auto simp add: upd_def bindM_def split: sum.split)
1.28 -qed
1.29 + by (rule Heap_eqI) (simp add: upd_def bindM_def split: option.split)
1.30
1.31
1.32 subsection {* Derivates *}
1.33 @@ -99,14 +93,11 @@
1.34
1.35 lemma array_make [code]:
1.36 "Array.new n x = make n (\<lambda>_. x)"
1.37 - by (induct n) (simp_all add: make_def new_def Heap_Monad.heap_def
1.38 - monad_simp array_of_list_replicate [symmetric]
1.39 - map_replicate_trivial replicate_append_same
1.40 - of_list_def)
1.41 + by (rule Heap_eqI) (simp add: make_def new_def array_of_list_replicate map_replicate_trivial of_list_def)
1.42
1.43 lemma array_of_list_make [code]:
1.44 "of_list xs = make (List.length xs) (\<lambda>n. xs ! n)"
1.45 - unfolding make_def map_nth ..
1.46 + by (rule Heap_eqI) (simp add: make_def map_nth)
1.47
1.48
1.49 subsection {* Code generator setup *}
1.50 @@ -135,13 +126,11 @@
1.51 by (simp add: make'_def o_def)
1.52
1.53 definition length' where
1.54 - [code del]: "length' = Array.length \<guillemotright>== liftM Code_Numeral.of_nat"
1.55 + [code del]: "length' a = Array.length a \<guillemotright>= (\<lambda>n. return (Code_Numeral.of_nat n))"
1.56 hide_const (open) length'
1.57 lemma [code]:
1.58 - "Array.length = Array.length' \<guillemotright>== liftM Code_Numeral.nat_of"
1.59 - by (simp add: length'_def monad_simp',
1.60 - simp add: liftM_def comp_def monad_simp,
1.61 - simp add: monad_simp')
1.62 + "Array.length a = Array.length' a \<guillemotright>= (\<lambda>i. return (Code_Numeral.nat_of i))"
1.63 + by (simp add: length'_def)
1.64
1.65 definition nth' where
1.66 [code del]: "nth' a = Array.nth a o Code_Numeral.nat_of"
1.67 @@ -155,7 +144,7 @@
1.68 hide_const (open) upd'
1.69 lemma [code]:
1.70 "Array.upd i x a = Array.upd' a (Code_Numeral.of_nat i) x \<guillemotright> return a"
1.71 - by (simp add: upd'_def monad_simp upd_return)
1.72 + by (simp add: upd'_def upd_return)
1.73
1.74
1.75 subsubsection {* SML *}
2.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy Mon Jul 05 10:42:27 2010 +0200
2.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Mon Jul 05 14:34:28 2010 +0200
2.3 @@ -12,16 +12,12 @@
2.4
2.5 subsubsection {* Monad combinators *}
2.6
2.7 -datatype exception = Exn
2.8 -
2.9 text {* Monadic heap actions either produce values
2.10 and transform the heap, or fail *}
2.11 -datatype 'a Heap = Heap "heap \<Rightarrow> ('a + exception) \<times> heap"
2.12 +datatype 'a Heap = Heap "heap \<Rightarrow> ('a \<times> heap) option"
2.13
2.14 -primrec
2.15 - execute :: "'a Heap \<Rightarrow> heap \<Rightarrow> ('a + exception) \<times> heap" where
2.16 - "execute (Heap f) = f"
2.17 -lemmas [code del] = execute.simps
2.18 +primrec execute :: "'a Heap \<Rightarrow> heap \<Rightarrow> ('a \<times> heap) option" where
2.19 + [code del]: "execute (Heap f) = f"
2.20
2.21 lemma Heap_execute [simp]:
2.22 "Heap (execute f) = f" by (cases f) simp_all
2.23 @@ -34,58 +30,67 @@
2.24 "(\<And>h. (\<lambda>x. execute (f x) h) = (\<lambda>y. execute (g y) h)) \<Longrightarrow> f = g"
2.25 by (auto simp: expand_fun_eq intro: Heap_eqI)
2.26
2.27 -lemma Heap_strip: "(\<And>f. PROP P f) \<equiv> (\<And>g. PROP P (Heap g))"
2.28 -proof
2.29 - fix g :: "heap \<Rightarrow> ('a + exception) \<times> heap"
2.30 - assume "\<And>f. PROP P f"
2.31 - then show "PROP P (Heap g)" .
2.32 -next
2.33 - fix f :: "'a Heap"
2.34 - assume assm: "\<And>g. PROP P (Heap g)"
2.35 - then have "PROP P (Heap (execute f))" .
2.36 - then show "PROP P f" by simp
2.37 -qed
2.38 -
2.39 -definition
2.40 - heap :: "(heap \<Rightarrow> 'a \<times> heap) \<Rightarrow> 'a Heap" where
2.41 - [code del]: "heap f = Heap (\<lambda>h. apfst Inl (f h))"
2.42 +definition heap :: "(heap \<Rightarrow> 'a \<times> heap) \<Rightarrow> 'a Heap" where
2.43 + [code del]: "heap f = Heap (Some \<circ> f)"
2.44
2.45 lemma execute_heap [simp]:
2.46 - "execute (heap f) h = apfst Inl (f h)"
2.47 + "execute (heap f) = Some \<circ> f"
2.48 by (simp add: heap_def)
2.49
2.50 -definition
2.51 - bindM :: "'a Heap \<Rightarrow> ('a \<Rightarrow> 'b Heap) \<Rightarrow> 'b Heap" (infixl ">>=" 54) where
2.52 - [code del]: "f >>= g = Heap (\<lambda>h. case execute f h of
2.53 - (Inl x, h') \<Rightarrow> execute (g x) h'
2.54 - | r \<Rightarrow> r)"
2.55 +lemma heap_cases [case_names succeed fail]:
2.56 + fixes f and h
2.57 + assumes succeed: "\<And>x h'. execute f h = Some (x, h') \<Longrightarrow> P"
2.58 + assumes fail: "execute f h = None \<Longrightarrow> P"
2.59 + shows P
2.60 + using assms by (cases "execute f h") auto
2.61
2.62 -notation
2.63 - bindM (infixl "\<guillemotright>=" 54)
2.64 -
2.65 -abbreviation
2.66 - chainM :: "'a Heap \<Rightarrow> 'b Heap \<Rightarrow> 'b Heap" (infixl ">>" 54) where
2.67 - "f >> g \<equiv> f >>= (\<lambda>_. g)"
2.68 -
2.69 -notation
2.70 - chainM (infixl "\<guillemotright>" 54)
2.71 -
2.72 -definition
2.73 - return :: "'a \<Rightarrow> 'a Heap" where
2.74 +definition return :: "'a \<Rightarrow> 'a Heap" where
2.75 [code del]: "return x = heap (Pair x)"
2.76
2.77 lemma execute_return [simp]:
2.78 - "execute (return x) h = apfst Inl (x, h)"
2.79 + "execute (return x) = Some \<circ> Pair x"
2.80 by (simp add: return_def)
2.81
2.82 -definition
2.83 - raise :: "string \<Rightarrow> 'a Heap" where -- {* the string is just decoration *}
2.84 - [code del]: "raise s = Heap (Pair (Inr Exn))"
2.85 +definition raise :: "string \<Rightarrow> 'a Heap" where -- {* the string is just decoration *}
2.86 + [code del]: "raise s = Heap (\<lambda>_. None)"
2.87
2.88 lemma execute_raise [simp]:
2.89 - "execute (raise s) h = (Inr Exn, h)"
2.90 + "execute (raise s) = (\<lambda>_. None)"
2.91 by (simp add: raise_def)
2.92
2.93 +definition bindM :: "'a Heap \<Rightarrow> ('a \<Rightarrow> 'b Heap) \<Rightarrow> 'b Heap" (infixl ">>=" 54) where
2.94 + [code del]: "f >>= g = Heap (\<lambda>h. case execute f h of
2.95 + Some (x, h') \<Rightarrow> execute (g x) h'
2.96 + | None \<Rightarrow> None)"
2.97 +
2.98 +notation bindM (infixl "\<guillemotright>=" 54)
2.99 +
2.100 +lemma execute_bind [simp]:
2.101 + "execute f h = Some (x, h') \<Longrightarrow> execute (f \<guillemotright>= g) h = execute (g x) h'"
2.102 + "execute f h = None \<Longrightarrow> execute (f \<guillemotright>= g) h = None"
2.103 + by (simp_all add: bindM_def)
2.104 +
2.105 +lemma execute_bind_heap [simp]:
2.106 + "execute (heap f \<guillemotright>= g) h = execute (g (fst (f h))) (snd (f h))"
2.107 + by (simp add: bindM_def split_def)
2.108 +
2.109 +lemma return_bind [simp]: "return x \<guillemotright>= f = f x"
2.110 + by (rule Heap_eqI) simp
2.111 +
2.112 +lemma bind_return [simp]: "f \<guillemotright>= return = f"
2.113 + by (rule Heap_eqI) (simp add: bindM_def split: option.splits)
2.114 +
2.115 +lemma bind_bind [simp]: "(f \<guillemotright>= g) \<guillemotright>= k = f \<guillemotright>= (\<lambda>x. g x \<guillemotright>= k)"
2.116 + by (rule Heap_eqI) (simp add: bindM_def split: option.splits)
2.117 +
2.118 +lemma raise_bind [simp]: "raise e \<guillemotright>= f = raise e"
2.119 + by (rule Heap_eqI) simp
2.120 +
2.121 +abbreviation chainM :: "'a Heap \<Rightarrow> 'b Heap \<Rightarrow> 'b Heap" (infixl ">>" 54) where
2.122 + "f >> g \<equiv> f >>= (\<lambda>_. g)"
2.123 +
2.124 +notation chainM (infixl "\<guillemotright>" 54)
2.125 +
2.126
2.127 subsubsection {* do-syntax *}
2.128
2.129 @@ -170,88 +175,10 @@
2.130
2.131 subsection {* Monad properties *}
2.132
2.133 -subsubsection {* Monad laws *}
2.134 -
2.135 -lemma return_bind: "return x \<guillemotright>= f = f x"
2.136 - by (simp add: bindM_def return_def)
2.137 -
2.138 -lemma bind_return: "f \<guillemotright>= return = f"
2.139 -proof (rule Heap_eqI)
2.140 - fix h
2.141 - show "execute (f \<guillemotright>= return) h = execute f h"
2.142 - by (auto simp add: bindM_def return_def split: sum.splits prod.splits)
2.143 -qed
2.144 -
2.145 -lemma bind_bind: "(f \<guillemotright>= g) \<guillemotright>= h = f \<guillemotright>= (\<lambda>x. g x \<guillemotright>= h)"
2.146 - by (rule Heap_eqI) (auto simp add: bindM_def split: split: sum.splits prod.splits)
2.147 -
2.148 -lemma bind_bind': "f \<guillemotright>= (\<lambda>x. g x \<guillemotright>= h x) = f \<guillemotright>= (\<lambda>x. g x \<guillemotright>= (\<lambda>y. return (x, y))) \<guillemotright>= (\<lambda>(x, y). h x y)"
2.149 - by (rule Heap_eqI) (auto simp add: bindM_def split: split: sum.splits prod.splits)
2.150 -
2.151 -lemma raise_bind: "raise e \<guillemotright>= f = raise e"
2.152 - by (simp add: raise_def bindM_def)
2.153 -
2.154 -
2.155 -lemmas monad_simp = return_bind bind_return bind_bind raise_bind
2.156 -
2.157 -
2.158 subsection {* Generic combinators *}
2.159
2.160 -definition
2.161 - liftM :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b Heap"
2.162 -where
2.163 - "liftM f = return o f"
2.164 -
2.165 -definition
2.166 - compM :: "('a \<Rightarrow> 'b Heap) \<Rightarrow> ('b \<Rightarrow> 'c Heap) \<Rightarrow> 'a \<Rightarrow> 'c Heap" (infixl ">>==" 54)
2.167 -where
2.168 - "(f >>== g) = (\<lambda>x. f x \<guillemotright>= g)"
2.169 -
2.170 -notation
2.171 - compM (infixl "\<guillemotright>==" 54)
2.172 -
2.173 -lemma liftM_collapse: "liftM f x = return (f x)"
2.174 - by (simp add: liftM_def)
2.175 -
2.176 -lemma liftM_compM: "liftM f \<guillemotright>== g = g o f"
2.177 - by (auto intro: Heap_eqI' simp add: expand_fun_eq liftM_def compM_def bindM_def)
2.178 -
2.179 -lemma compM_return: "f \<guillemotright>== return = f"
2.180 - by (simp add: compM_def monad_simp)
2.181 -
2.182 -lemma compM_compM: "(f \<guillemotright>== g) \<guillemotright>== h = f \<guillemotright>== (g \<guillemotright>== h)"
2.183 - by (simp add: compM_def monad_simp)
2.184 -
2.185 -lemma liftM_bind:
2.186 - "(\<lambda>x. liftM f x \<guillemotright>= liftM g) = liftM (\<lambda>x. g (f x))"
2.187 - by (rule Heap_eqI') (simp add: monad_simp liftM_def bindM_def)
2.188 -
2.189 -lemma liftM_comp:
2.190 - "liftM f o g = liftM (f o g)"
2.191 - by (rule Heap_eqI') (simp add: liftM_def)
2.192 -
2.193 -lemmas monad_simp' = monad_simp liftM_compM compM_return
2.194 - compM_compM liftM_bind liftM_comp
2.195 -
2.196 -primrec
2.197 - mapM :: "('a \<Rightarrow> 'b Heap) \<Rightarrow> 'a list \<Rightarrow> 'b list Heap"
2.198 -where
2.199 - "mapM f [] = return []"
2.200 - | "mapM f (x#xs) = do y \<leftarrow> f x;
2.201 - ys \<leftarrow> mapM f xs;
2.202 - return (y # ys)
2.203 - done"
2.204 -
2.205 -primrec
2.206 - foldM :: "('a \<Rightarrow> 'b \<Rightarrow> 'b Heap) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b Heap"
2.207 -where
2.208 - "foldM f [] s = return s"
2.209 - | "foldM f (x#xs) s = f x s \<guillemotright>= foldM f xs"
2.210 -
2.211 -definition
2.212 - assert :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a Heap"
2.213 -where
2.214 - "assert P x = (if P x then return x else raise (''assert''))"
2.215 +definition assert :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a Heap" where
2.216 + "assert P x = (if P x then return x else raise ''assert'')"
2.217
2.218 lemma assert_cong [fundef_cong]:
2.219 assumes "P = P'"
2.220 @@ -259,28 +186,42 @@
2.221 shows "(assert P x >>= f) = (assert P' x >>= f')"
2.222 using assms by (auto simp add: assert_def return_bind raise_bind)
2.223
2.224 +definition liftM :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b Heap" where
2.225 + "liftM f = return o f"
2.226 +
2.227 +lemma liftM_collapse [simp]:
2.228 + "liftM f x = return (f x)"
2.229 + by (simp add: liftM_def)
2.230 +
2.231 +lemma bind_liftM:
2.232 + "(f \<guillemotright>= liftM g) = (f \<guillemotright>= (\<lambda>x. return (g x)))"
2.233 + by (simp add: liftM_def comp_def)
2.234 +
2.235 +primrec mapM :: "('a \<Rightarrow> 'b Heap) \<Rightarrow> 'a list \<Rightarrow> 'b list Heap" where
2.236 + "mapM f [] = return []"
2.237 +| "mapM f (x#xs) = do
2.238 + y \<leftarrow> f x;
2.239 + ys \<leftarrow> mapM f xs;
2.240 + return (y # ys)
2.241 + done"
2.242 +
2.243 +
2.244 subsubsection {* A monadic combinator for simple recursive functions *}
2.245
2.246 text {* Using a locale to fix arguments f and g of MREC *}
2.247
2.248 locale mrec =
2.249 -fixes
2.250 - f :: "'a => ('b + 'a) Heap"
2.251 - and g :: "'a => 'a => 'b => 'b Heap"
2.252 + fixes f :: "'a \<Rightarrow> ('b + 'a) Heap"
2.253 + and g :: "'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b Heap"
2.254 begin
2.255
2.256 -function (default "\<lambda>(x,h). (Inr Exn, undefined)")
2.257 - mrec
2.258 -where
2.259 - "mrec x h =
2.260 - (case Heap_Monad.execute (f x) h of
2.261 - (Inl (Inl r), h') \<Rightarrow> (Inl r, h')
2.262 - | (Inl (Inr s), h') \<Rightarrow>
2.263 - (case mrec s h' of
2.264 - (Inl z, h'') \<Rightarrow> Heap_Monad.execute (g x s z) h''
2.265 - | (Inr e, h'') \<Rightarrow> (Inr e, h''))
2.266 - | (Inr e, h') \<Rightarrow> (Inr e, h')
2.267 - )"
2.268 +function (default "\<lambda>(x, h). None") mrec :: "'a \<Rightarrow> heap \<Rightarrow> ('b \<times> heap) option" where
2.269 + "mrec x h = (case execute (f x) h of
2.270 + Some (Inl r, h') \<Rightarrow> Some (r, h')
2.271 + | Some (Inr s, h') \<Rightarrow> (case mrec s h' of
2.272 + Some (z, h'') \<Rightarrow> execute (g x s z) h''
2.273 + | None \<Rightarrow> None)
2.274 + | None \<Rightarrow> None)"
2.275 by auto
2.276
2.277 lemma graph_implies_dom:
2.278 @@ -290,38 +231,37 @@
2.279 apply (erule mrec_rel.cases)
2.280 by simp
2.281
2.282 -lemma mrec_default: "\<not> mrec_dom (x, h) \<Longrightarrow> mrec x h = (Inr Exn, undefined)"
2.283 +lemma mrec_default: "\<not> mrec_dom (x, h) \<Longrightarrow> mrec x h = None"
2.284 unfolding mrec_def
2.285 by (rule fundef_default_value[OF mrec_sumC_def graph_implies_dom, of _ _ "(x, h)", simplified])
2.286
2.287 lemma mrec_di_reverse:
2.288 assumes "\<not> mrec_dom (x, h)"
2.289 shows "
2.290 - (case Heap_Monad.execute (f x) h of
2.291 - (Inl (Inl r), h') \<Rightarrow> False
2.292 - | (Inl (Inr s), h') \<Rightarrow> \<not> mrec_dom (s, h')
2.293 - | (Inr e, h') \<Rightarrow> False
2.294 + (case execute (f x) h of
2.295 + Some (Inl r, h') \<Rightarrow> False
2.296 + | Some (Inr s, h') \<Rightarrow> \<not> mrec_dom (s, h')
2.297 + | None \<Rightarrow> False
2.298 )"
2.299 -using assms
2.300 -by (auto split:prod.splits sum.splits)
2.301 - (erule notE, rule accpI, elim mrec_rel.cases, simp)+
2.302 -
2.303 +using assms apply (auto split: option.split sum.split)
2.304 +apply (rule ccontr)
2.305 +apply (erule notE, rule accpI, elim mrec_rel.cases, auto)+
2.306 +done
2.307
2.308 lemma mrec_rule:
2.309 "mrec x h =
2.310 - (case Heap_Monad.execute (f x) h of
2.311 - (Inl (Inl r), h') \<Rightarrow> (Inl r, h')
2.312 - | (Inl (Inr s), h') \<Rightarrow>
2.313 + (case execute (f x) h of
2.314 + Some (Inl r, h') \<Rightarrow> Some (r, h')
2.315 + | Some (Inr s, h') \<Rightarrow>
2.316 (case mrec s h' of
2.317 - (Inl z, h'') \<Rightarrow> Heap_Monad.execute (g x s z) h''
2.318 - | (Inr e, h'') \<Rightarrow> (Inr e, h''))
2.319 - | (Inr e, h') \<Rightarrow> (Inr e, h')
2.320 + Some (z, h'') \<Rightarrow> execute (g x s z) h''
2.321 + | None \<Rightarrow> None)
2.322 + | None \<Rightarrow> None
2.323 )"
2.324 apply (cases "mrec_dom (x,h)", simp)
2.325 apply (frule mrec_default)
2.326 apply (frule mrec_di_reverse, simp)
2.327 -by (auto split: sum.split prod.split simp: mrec_default)
2.328 -
2.329 +by (auto split: sum.split option.split simp: mrec_default)
2.330
2.331 definition
2.332 "MREC x = Heap (mrec x)"
2.333 @@ -340,32 +280,31 @@
2.334 apply simp
2.335 apply (rule ext)
2.336 apply (unfold mrec_rule[of x])
2.337 - by (auto split:prod.splits sum.splits)
2.338 -
2.339 + by (auto split: option.splits prod.splits sum.splits)
2.340
2.341 lemma MREC_pinduct:
2.342 - assumes "Heap_Monad.execute (MREC x) h = (Inl r, h')"
2.343 - assumes non_rec_case: "\<And> x h h' r. Heap_Monad.execute (f x) h = (Inl (Inl r), h') \<Longrightarrow> P x h h' r"
2.344 - assumes rec_case: "\<And> x h h1 h2 h' s z r. Heap_Monad.execute (f x) h = (Inl (Inr s), h1) \<Longrightarrow> Heap_Monad.execute (MREC s) h1 = (Inl z, h2) \<Longrightarrow> P s h1 h2 z
2.345 - \<Longrightarrow> Heap_Monad.execute (g x s z) h2 = (Inl r, h') \<Longrightarrow> P x h h' r"
2.346 + assumes "execute (MREC x) h = Some (r, h')"
2.347 + assumes non_rec_case: "\<And> x h h' r. execute (f x) h = Some (Inl r, h') \<Longrightarrow> P x h h' r"
2.348 + assumes rec_case: "\<And> x h h1 h2 h' s z r. execute (f x) h = Some (Inr s, h1) \<Longrightarrow> execute (MREC s) h1 = Some (z, h2) \<Longrightarrow> P s h1 h2 z
2.349 + \<Longrightarrow> execute (g x s z) h2 = Some (r, h') \<Longrightarrow> P x h h' r"
2.350 shows "P x h h' r"
2.351 proof -
2.352 - from assms(1) have mrec: "mrec x h = (Inl r, h')"
2.353 + from assms(1) have mrec: "mrec x h = Some (r, h')"
2.354 unfolding MREC_def execute.simps .
2.355 from mrec have dom: "mrec_dom (x, h)"
2.356 apply -
2.357 apply (rule ccontr)
2.358 apply (drule mrec_default) by auto
2.359 - from mrec have h'_r: "h' = (snd (mrec x h))" "r = (Sum_Type.Projl (fst (mrec x h)))"
2.360 + from mrec have h'_r: "h' = snd (the (mrec x h))" "r = fst (the (mrec x h))"
2.361 by auto
2.362 - from mrec have "P x h (snd (mrec x h)) (Sum_Type.Projl (fst (mrec x h)))"
2.363 + from mrec have "P x h (snd (the (mrec x h))) (fst (the (mrec x h)))"
2.364 proof (induct arbitrary: r h' rule: mrec.pinduct[OF dom])
2.365 case (1 x h)
2.366 - obtain rr h' where "mrec x h = (rr, h')" by fastsimp
2.367 - obtain fret h1 where exec_f: "Heap_Monad.execute (f x) h = (fret, h1)" by fastsimp
2.368 + obtain rr h' where "the (mrec x h) = (rr, h')" by fastsimp
2.369 show ?case
2.370 - proof (cases fret)
2.371 - case (Inl a)
2.372 + proof (cases "execute (f x) h")
2.373 + case (Some result)
2.374 + then obtain a h1 where exec_f: "execute (f x) h = Some (a, h1)" by fastsimp
2.375 note Inl' = this
2.376 show ?thesis
2.377 proof (cases a)
2.378 @@ -375,23 +314,28 @@
2.379 next
2.380 case (Inr b)
2.381 note Inr' = this
2.382 - obtain ret_mrec h2 where mrec_rec: "mrec b h1 = (ret_mrec, h2)" by fastsimp
2.383 - from this Inl 1(1) exec_f mrec show ?thesis
2.384 - proof (cases "ret_mrec")
2.385 - case (Inl aaa)
2.386 - from this mrec exec_f Inl' Inr' 1(1) mrec_rec 1(2) [OF exec_f [symmetric] Inl' Inr', of "aaa" "h2"] 1(3)
2.387 - show ?thesis
2.388 - apply auto
2.389 - apply (rule rec_case)
2.390 - unfolding MREC_def by auto
2.391 + show ?thesis
2.392 + proof (cases "mrec b h1")
2.393 + case (Some result)
2.394 + then obtain aaa h2 where mrec_rec: "mrec b h1 = Some (aaa, h2)" by fastsimp
2.395 + moreover from this have "P b h1 (snd (the (mrec b h1))) (fst (the (mrec b h1)))"
2.396 + apply (intro 1(2))
2.397 + apply (auto simp add: Inr Inl')
2.398 + done
2.399 + moreover note mrec mrec_rec exec_f Inl' Inr' 1(1) 1(3)
2.400 + ultimately show ?thesis
2.401 + apply auto
2.402 + apply (rule rec_case)
2.403 + apply auto
2.404 + unfolding MREC_def by auto
2.405 next
2.406 - case (Inr b)
2.407 - from this Inl 1(1) exec_f mrec Inr' mrec_rec 1(3) show ?thesis by auto
2.408 + case None
2.409 + from this 1(1) exec_f mrec Inr' 1(3) show ?thesis by auto
2.410 qed
2.411 qed
2.412 next
2.413 - case (Inr b)
2.414 - from this 1(1) mrec exec_f 1(3) show ?thesis by simp
2.415 + case None
2.416 + from this 1(1) mrec 1(3) show ?thesis by simp
2.417 qed
2.418 qed
2.419 from this h'_r show ?thesis by simp
2.420 @@ -412,38 +356,29 @@
2.421
2.422 subsubsection {* Logical intermediate layer *}
2.423
2.424 -definition
2.425 - Fail :: "String.literal \<Rightarrow> exception"
2.426 -where
2.427 - [code del]: "Fail s = Exn"
2.428 +primrec raise' :: "String.literal \<Rightarrow> 'a Heap" where
2.429 + [code del, code_post]: "raise' (STR s) = raise s"
2.430
2.431 -definition
2.432 - raise_exc :: "exception \<Rightarrow> 'a Heap"
2.433 -where
2.434 - [code del]: "raise_exc e = raise []"
2.435 +lemma raise_raise' [code_inline]:
2.436 + "raise s = raise' (STR s)"
2.437 + by simp
2.438
2.439 -lemma raise_raise_exc [code, code_unfold]:
2.440 - "raise s = raise_exc (Fail (STR s))"
2.441 - unfolding Fail_def raise_exc_def raise_def ..
2.442 +code_datatype raise' -- {* avoid @{const "Heap"} formally *}
2.443
2.444 -hide_const (open) Fail raise_exc
2.445 +hide_const (open) raise'
2.446
2.447
2.448 subsubsection {* SML and OCaml *}
2.449
2.450 code_type Heap (SML "unit/ ->/ _")
2.451 -code_const Heap (SML "raise/ (Fail/ \"bare Heap\")")
2.452 code_const "op \<guillemotright>=" (SML "!(fn/ f'_/ =>/ fn/ ()/ =>/ f'_/ (_/ ())/ ())")
2.453 code_const return (SML "!(fn/ ()/ =>/ _)")
2.454 -code_const "Heap_Monad.Fail" (SML "Fail")
2.455 -code_const "Heap_Monad.raise_exc" (SML "!(fn/ ()/ =>/ raise/ _)")
2.456 +code_const Heap_Monad.raise' (SML "!(raise/ Fail/ _)")
2.457
2.458 code_type Heap (OCaml "_")
2.459 -code_const Heap (OCaml "failwith/ \"bare Heap\"")
2.460 code_const "op \<guillemotright>=" (OCaml "!(fun/ f'_/ ()/ ->/ f'_/ (_/ ())/ ())")
2.461 code_const return (OCaml "!(fun/ ()/ ->/ _)")
2.462 -code_const "Heap_Monad.Fail" (OCaml "Failure")
2.463 -code_const "Heap_Monad.raise_exc" (OCaml "!(fun/ ()/ ->/ raise/ _)")
2.464 +code_const Heap_Monad.raise' (OCaml "failwith/ _")
2.465
2.466 setup {*
2.467
2.468 @@ -514,8 +449,6 @@
2.469
2.470 *}
2.471
2.472 -code_reserved OCaml Failure raise
2.473 -
2.474
2.475 subsubsection {* Haskell *}
2.476
2.477 @@ -556,10 +489,8 @@
2.478 text {* Monad *}
2.479
2.480 code_type Heap (Haskell "Heap.ST/ Heap.RealWorld/ _")
2.481 -code_const Heap (Haskell "error/ \"bare Heap\"")
2.482 code_monad "op \<guillemotright>=" Haskell
2.483 code_const return (Haskell "return")
2.484 -code_const "Heap_Monad.Fail" (Haskell "_")
2.485 -code_const "Heap_Monad.raise_exc" (Haskell "error")
2.486 +code_const Heap_Monad.raise' (Haskell "error/ _")
2.487
2.488 end
3.1 --- a/src/HOL/Imperative_HOL/Ref.thy Mon Jul 05 10:42:27 2010 +0200
3.2 +++ b/src/HOL/Imperative_HOL/Ref.thy Mon Jul 05 14:34:28 2010 +0200
3.3 @@ -1,5 +1,4 @@
3.4 (* Title: HOL/Library/Ref.thy
3.5 - ID: $Id$
3.6 Author: John Matthews, Galois Connections; Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen
3.7 *)
3.8
3.9 @@ -53,7 +52,7 @@
3.10
3.11 lemma update_change [code]:
3.12 "r := e = Ref.change (\<lambda>_. e) r \<guillemotright> return ()"
3.13 - by (auto simp add: monad_simp change_def lookup_chain)
3.14 + by (auto simp add: change_def lookup_chain)
3.15
3.16
3.17 subsection {* Code generator setup *}
4.1 --- a/src/HOL/Imperative_HOL/Relational.thy Mon Jul 05 10:42:27 2010 +0200
4.2 +++ b/src/HOL/Imperative_HOL/Relational.thy Mon Jul 05 14:34:28 2010 +0200
4.3 @@ -9,10 +9,10 @@
4.4
4.5 definition crel :: "'a Heap \<Rightarrow> heap \<Rightarrow> heap \<Rightarrow> 'a \<Rightarrow> bool"
4.6 where
4.7 - crel_def': "crel c h h' r \<longleftrightarrow> Heap_Monad.execute c h = (Inl r, h')"
4.8 + crel_def': "crel c h h' r \<longleftrightarrow> Heap_Monad.execute c h = Some (r, h')"
4.9
4.10 lemma crel_def: -- FIXME
4.11 - "crel c h h' r \<longleftrightarrow> (Inl r, h') = Heap_Monad.execute c h"
4.12 + "crel c h h' r \<longleftrightarrow> Some (r, h') = Heap_Monad.execute c h"
4.13 unfolding crel_def' by auto
4.14
4.15 lemma crel_deterministic: "\<lbrakk> crel f h h' a; crel f h h'' b \<rbrakk> \<Longrightarrow> (a = b) \<and> (h' = h'')"
4.16 @@ -28,8 +28,7 @@
4.17 lemma crelE[consumes 1]:
4.18 assumes "crel (f >>= g) h h'' r'"
4.19 obtains h' r where "crel f h h' r" "crel (g r) h' h'' r'"
4.20 - using assms
4.21 - by (auto simp add: crel_def bindM_def Let_def prod_case_beta split_def Pair_fst_snd_eq split add: sum.split_asm)
4.22 + using assms by (auto simp add: crel_def bindM_def split: option.split_asm)
4.23
4.24 lemma crelE'[consumes 1]:
4.25 assumes "crel (f >> g) h h'' r'"
4.26 @@ -86,8 +85,8 @@
4.27 lemma crel_heap:
4.28 assumes "crel (Heap_Monad.heap f) h h' r"
4.29 obtains "h' = snd (f h)" "r = fst (f h)"
4.30 - using assms
4.31 - unfolding heap_def crel_def apfst_def split_def prod_fun_def by simp_all
4.32 + using assms by (cases "f h") (simp add: crel_def)
4.33 +
4.34
4.35 subsection {* Elimination rules for array commands *}
4.36
4.37 @@ -369,11 +368,9 @@
4.38 apply (cases f)
4.39 apply simp
4.40 apply (simp add: expand_fun_eq split_def)
4.41 +apply (auto split: option.split)
4.42 +apply (erule_tac x="x" in meta_allE)
4.43 apply auto
4.44 -apply (case_tac "fst (fun x)")
4.45 -apply (simp_all add: Pair_fst_snd_eq)
4.46 -apply (erule_tac x="x" in meta_allE)
4.47 -apply fastsimp
4.48 done
4.49
4.50 section {* Introduction rules *}
4.51 @@ -502,10 +499,10 @@
4.52 shows "P x h h' r"
4.53 proof (rule MREC_pinduct[OF assms(1)[unfolded crel_def, symmetric]])
4.54 fix x h h1 h2 h' s z r
4.55 - assume "Heap_Monad.execute (f x) h = (Inl (Inr s), h1)"
4.56 - "Heap_Monad.execute (MREC f g s) h1 = (Inl z, h2)"
4.57 + assume "Heap_Monad.execute (f x) h = Some (Inr s, h1)"
4.58 + "Heap_Monad.execute (MREC f g s) h1 = Some (z, h2)"
4.59 "P s h1 h2 z"
4.60 - "Heap_Monad.execute (g x s z) h2 = (Inl r, h')"
4.61 + "Heap_Monad.execute (g x s z) h2 = Some (r, h')"
4.62 from assms(3)[unfolded crel_def, OF this(1)[symmetric] this(2)[symmetric] this(3) this(4)[symmetric]]
4.63 show "P x h h' r" .
4.64 next
4.65 @@ -519,15 +516,15 @@
4.66
4.67 definition noError :: "'a Heap \<Rightarrow> heap \<Rightarrow> bool"
4.68 where
4.69 - "noError c h \<longleftrightarrow> (\<exists>r h'. (Inl r, h') = Heap_Monad.execute c h)"
4.70 + "noError c h \<longleftrightarrow> (\<exists>r h'. Some (r, h') = Heap_Monad.execute c h)"
4.71
4.72 lemma noError_def': -- FIXME
4.73 - "noError c h \<longleftrightarrow> (\<exists>r h'. Heap_Monad.execute c h = (Inl r, h'))"
4.74 + "noError c h \<longleftrightarrow> (\<exists>r h'. Heap_Monad.execute c h = Some (r, h'))"
4.75 unfolding noError_def apply auto proof -
4.76 fix r h'
4.77 - assume "(Inl r, h') = Heap_Monad.execute c h"
4.78 - then have "Heap_Monad.execute c h = (Inl r, h')" ..
4.79 - then show "\<exists>r h'. Heap_Monad.execute c h = (Inl r, h')" by blast
4.80 + assume "Some (r, h') = Heap_Monad.execute c h"
4.81 + then have "Heap_Monad.execute c h = Some (r, h')" ..
4.82 + then show "\<exists>r h'. Heap_Monad.execute c h = Some (r, h')" by blast
4.83 qed
4.84
4.85 subsection {* Introduction rules for basic monadic commands *}
4.86 @@ -640,7 +637,7 @@
4.87 (*TODO: move to HeapMonad *)
4.88 lemma mapM_append:
4.89 "mapM f (xs @ ys) = mapM f xs \<guillemotright>= (\<lambda>xs. mapM f ys \<guillemotright>= (\<lambda>ys. return (xs @ ys)))"
4.90 - by (induct xs) (simp_all add: monad_simp)
4.91 + by (induct xs) simp_all
4.92
4.93 lemma noError_freeze:
4.94 shows "noError (freeze a) h"
5.1 --- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy Mon Jul 05 10:42:27 2010 +0200
5.2 +++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy Mon Jul 05 14:34:28 2010 +0200
5.3 @@ -56,7 +56,7 @@
5.4 return (x#xs)
5.5 done"
5.6 unfolding traverse_def
5.7 -by (auto simp: traverse_def monad_simp MREC_rule)
5.8 +by (auto simp: traverse_def MREC_rule)
5.9
5.10
5.11 section {* Proving correctness with relational abstraction *}
5.12 @@ -531,7 +531,7 @@
5.13 done"
5.14 unfolding rev'_def MREC_rule[of _ _ "(q, p)"] unfolding rev'_def[symmetric]
5.15 thm arg_cong2
5.16 - by (auto simp add: monad_simp expand_fun_eq intro: arg_cong2[where f = "op \<guillemotright>="] split: node.split)
5.17 + by (auto simp add: expand_fun_eq intro: arg_cong2[where f = "op \<guillemotright>="] split: node.split)
5.18
5.19 fun rev :: "('a:: heap) node \<Rightarrow> 'a node Heap"
5.20 where
6.1 --- a/src/HOL/Imperative_HOL/ex/SatChecker.thy Mon Jul 05 10:42:27 2010 +0200
6.2 +++ b/src/HOL/Imperative_HOL/ex/SatChecker.thy Mon Jul 05 14:34:28 2010 +0200
6.3 @@ -402,6 +402,12 @@
6.4 res_thm' l cli clj
6.5 done))"
6.6
6.7 +primrec
6.8 + foldM :: "('a \<Rightarrow> 'b \<Rightarrow> 'b Heap) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b Heap"
6.9 +where
6.10 + "foldM f [] s = return s"
6.11 + | "foldM f (x#xs) s = f x s \<guillemotright>= foldM f xs"
6.12 +
6.13 fun doProofStep2 :: "Clause option array \<Rightarrow> ProofStep \<Rightarrow> Clause list \<Rightarrow> Clause list Heap"
6.14 where
6.15 "doProofStep2 a (Conflict saveTo (i, rs)) rcs =