1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7(* 8 The state and error monads in Isabelle, 9*) 10 11chapter "Monads" 12 13theory StateMonad (* FIXME: untested/unused *) 14imports Lib 15begin 16 17type_synonym ('s,'a) state_monad = "'s \<Rightarrow> 'a \<times> 's" 18 19definition 20 runState :: "('s,'a) state_monad \<Rightarrow> 's \<Rightarrow> 'a \<times> 's" 21where 22 "runState \<equiv> id" 23 24definition 25 "return a \<equiv> \<lambda>s. (a,s)" 26 27definition 28 bind :: "('s, 'a) state_monad \<Rightarrow> ('a \<Rightarrow> ('s, 'b) state_monad) \<Rightarrow> 29 ('s, 'b) state_monad" (infixl ">>=" 60) 30where 31 "bind f g \<equiv> (\<lambda>s. let (v,s') = f s in (g v) s')" 32 33definition 34 "bind' f g \<equiv> bind f (\<lambda>_. g)" 35 36declare bind'_def [iff] 37 38 39definition 40 "get \<equiv> \<lambda>s. (s,s)" 41 42definition 43 "put s \<equiv> \<lambda>_. ((),s)" 44 45definition 46 "gets f \<equiv> get >>= (\<lambda>s. return $ f s)" 47 48definition 49 "modify f \<equiv> get >>= (\<lambda>s. put $ f s)" 50 51definition 52 "when p s \<equiv> if p then s else return ()" 53 54definition 55 "unless p s \<equiv> when (\<not>p) s" 56 57 58text \<open>The monad laws:\<close> 59 60lemma return_bind [simp]: "(return x >>= f) = f x" 61 by (simp add: return_def bind_def runState_def) 62 63lemma bind_return [simp]: "(m >>= return) = m" 64 unfolding bind_def return_def runState_def 65 by (simp add: Let_def split_def) 66 67lemma bind_assoc: 68 fixes m :: "('s,'a) state_monad" 69 fixes f :: "'a \<Rightarrow> ('s,'b) state_monad" 70 fixes g :: "'b \<Rightarrow> ('s,'c) state_monad" 71 shows "(m >>= f) >>= g = m >>= (\<lambda>x. f x >>= g)" 72 unfolding bind_def 73 by (clarsimp simp add: Let_def split_def) 74 75 76text \<open>An errorT state\_monad (returnOk=return, bindE=bind):\<close> 77 78definition 79 "returnOk \<equiv> return o Inr" 80 81definition 82 "throwError \<equiv> return o Inl" 83 84definition 85 "Ok \<equiv> Inr" 86 87definition 88 lift :: "('a \<Rightarrow> ('s, 'e + 'b) state_monad) \<Rightarrow> 'e+'a \<Rightarrow> ('s, 'e + 'b) state_monad" 89where 90 "lift f v \<equiv> case v of Inl e \<Rightarrow> throwError e | Inr v' \<Rightarrow> f v'" 91 92definition 93 lift2 :: "('c \<Rightarrow> ('a, 'b + 'e + 'd) state_monad) \<Rightarrow> 'b+'e+'c \<Rightarrow> ('a, 'b+'e+'d) state_monad" 94where 95 "lift2 f v \<equiv> case v of 96 Inl e \<Rightarrow> throwError e 97 | Inr v'' \<Rightarrow> (case v'' of Inl e' \<Rightarrow> return $ Inr $ Inl e' | Inr v' \<Rightarrow> f v')" 98 99(* This is used if you are just trying to throwError by itself *) 100definition 101 raise :: "'a \<Rightarrow> 's \<Rightarrow> ('a + unit) \<times> 's" 102where 103 "raise \<equiv> return \<circ> Inl" 104 105definition 106 bindE :: "('s, 'e + 'a) state_monad \<Rightarrow> ('a \<Rightarrow> ('s, 'e + 'b) state_monad) \<Rightarrow> 107 ('s, 'e + 'b) state_monad" (infixl ">>=E" 60) 108where 109 "bindE f g \<equiv> bind f (lift g)" 110 111 112definition 113 "bindE' f g \<equiv> bindE f (\<lambda>_. g)" 114 115definition 116 liftE :: "('s,'a) state_monad \<Rightarrow> ('s, 'e+'a) state_monad" where 117 "liftE f \<equiv> \<lambda>s. let (v,s') = f s in (Inr v, s')" 118 119definition 120 "whenE P f \<equiv> if P then f else returnOk ()" 121 122definition 123 "unlessE P f \<equiv> if P then returnOk () else f" 124 125definition 126 "throw_opt ex x \<equiv> case x of None \<Rightarrow> throwError ex | Some v \<Rightarrow> returnOk v" 127 128definition 129 "bindEE f g \<equiv> bind f (lift2 g)" 130definition 131 "bindEE' f g \<equiv> bindEE f (\<lambda>_. g)" 132 133definition 134 "modifyE \<equiv> (liftE \<circ> modify)" 135definition 136 "getsE x \<equiv> liftE $ gets x" 137 138syntax 139 bindEE :: "'a \<Rightarrow> 'b \<Rightarrow> 'c" (infixl ">>=EE" 60) 140 141declare 142 bindE'_def [iff] 143 bindEE_def [iff] 144 bindEE'_def [iff] 145 146lemma returnOk_bindE [simp]: "(returnOk x >>=E f) = f x" 147 unfolding bindE_def return_def returnOk_def 148 by (clarsimp simp: lift_def bind_def) 149 150lemma lift_return [simp]: 151 "lift (return \<circ> Inr) = return" 152 by (auto simp: lift_def throwError_def split: sum.splits) 153 154lemma bindE_returnOk [simp]: "(m >>=E returnOk) = m" 155 by (simp add: bindE_def returnOk_def) 156 157 lemma bindE_assoc: 158 shows "(m >>=E f) >>=E g = m >>=E (\<lambda>x. f x >>=E g)" 159 by (auto simp: Let_def bindE_def bind_def lift_def split_def runState_def throwError_def return_def 160 split: sum.splits) 161 162lemma throwError_bindE [simp]: 163 "throwError E >>=E f = throwError E" 164 by (simp add: bindE_def bind_def throwError_def lift_def return_def) 165 166 167subsection "Syntax for state monad" 168 169 170nonterminal 171 dobinds and dobind and nobind 172 173syntax 174 "_dobind" :: "[pttrn, 'a] => dobind" ("(_ <-/ _)" 10) 175 "" :: "dobind => dobinds" ("_") 176 "_nobind" :: "'a => dobind" ("_") 177 "_dobinds" :: "[dobind, dobinds] => dobinds" ("(_);//(_)") 178 179 "_do" :: "[dobinds, 'a] => 'a" ("(do (_);// (_)//od)" 100) 180syntax (xsymbols) 181 "_dobind" :: "[pttrn, 'a] => dobind" ("(_ \<leftarrow>/ _)" 10) 182 183 184translations 185 "_do (_dobinds b bs) e" == "_do b (_do bs e)" 186 "_do (_nobind b) e" == "CONST bind' b e" 187 "do x <- a; e od" == "a >>= (\<lambda>x. e)" 188 189lemma "do x \<leftarrow> return 1; return 2; return x od = return 1" 190 by simp 191 192 193subsection "Syntax for errorT state monad" 194 195 196syntax 197 "_doE" :: "[dobinds, 'a] => 'a" ("(doE (_);// (_)//odE)" 100) 198 199translations 200 "_doE (_dobinds b bs) e" == "_doE b (_doE bs e)" 201 "_doE (_nobind b) e" == "CONST bindE' b e" 202 "doE x <- a; e odE" == "a >>=E (\<lambda>x. e)" 203 204 205subsection "Syntax for errorT errorT state monad" 206 207syntax 208 "_doEE" :: "[dobinds, 'a] => 'a" ("(doEE (_);// (_)//odEE)" 100) 209 210translations 211 "_doEE (_dobinds b bs) e" == "_doEE b (_doEE bs e)" 212 "_doEE (_nobind b) e" == "CONST bindEE' b e" 213 "doEE x <- a; e odEE" == "a >>=EE (\<lambda>x. e)" 214 215primrec 216 inc_forloop :: "nat \<Rightarrow> 'g::{plus,one} \<Rightarrow> ('g \<Rightarrow> ('a, 'b + unit) state_monad) \<Rightarrow> 217 ('a, 'b + unit) state_monad" 218where 219 "inc_forloop 0 current body = returnOk ()" 220| "inc_forloop (Suc left) current body = doE body current ; inc_forloop left (current+1) body odE" 221 222primrec 223 do_times :: "nat \<Rightarrow> ('a, 'b + unit) state_monad \<Rightarrow> ('a, 'b + unit) state_monad \<Rightarrow> 224 ('a, 'b + unit) state_monad" 225where 226 "do_times 0 body increment = returnOk ()" 227| "do_times (Suc left) body increment = doE body ; increment ; do_times left body increment odE" 228 229definition 230 function_update :: "'a \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)" where 231 "function_update index modifier f \<equiv> 232 \<lambda>x. if x = index then modifier (f x) else (f x)" 233 234lemma "doE x \<leftarrow> returnOk 1; returnOk 2; returnOk x odE = returnOk 1" 235 by simp 236 237term "doEE x \<leftarrow> returnOk $ Ok 1; returnOk $ Ok 2; returnOk $ Ok x odEE" 238 239definition 240 "skip \<equiv> returnOk $ Ok ()" 241 242definition 243 "liftM f m \<equiv> do x \<leftarrow> m; return (f x) od" 244definition 245 "liftME f m \<equiv> doE x \<leftarrow> m; returnOk (f x) odE" 246 247definition 248 "sequence_x xs \<equiv> foldr (\<lambda>x y. x >>= (\<lambda>_. y)) xs (return ())" 249 250definition 251 "zipWithM_x f xs ys \<equiv> sequence_x (zipWith f xs ys)" 252definition 253 "mapM_x f xs \<equiv> sequence_x (map f xs)" 254 255definition 256 "sequence xs \<equiv> let mcons = (\<lambda>p q. p >>= (\<lambda>x. q >>= (\<lambda>y. return (x#y)))) 257 in foldr mcons xs (return [])" 258 259definition 260 "mapM f xs \<equiv> sequence (map f xs)" 261 262definition 263 "sequenceE_x xs \<equiv> foldr (\<lambda>x y. doE uu <- x; y odE) xs (returnOk ())" 264definition 265 "mapME_x f xs \<equiv> sequenceE_x (map f xs)" 266 267definition 268 "sequenceEE_x xs \<equiv> foldr bindEE' xs (skip)" 269definition 270 "mapMEE_x f xs \<equiv> sequenceEE_x (map f xs)" 271 272definition 273 catch :: "('s, 'a + 'b) state_monad \<Rightarrow> ('a \<Rightarrow> ('s, 'b) state_monad) \<Rightarrow> ('s, 'b) state_monad" 274where 275 "catch f handler \<equiv> do x \<leftarrow> f; 276 case x of 277 Inr b \<Rightarrow> return b 278 | Inl e \<Rightarrow> handler e 279 od" 280 281definition 282 handleE :: "('s, 'x + 'a) state_monad \<Rightarrow> 283 ('x \<Rightarrow> ('s, 'x + 'a) state_monad) \<Rightarrow> 284 ('s, 'x + 'a) state_monad" (infix "<handle>" 11) where 285 "f <handle> handler \<equiv> 286 do v \<leftarrow> f; case v of Inl e \<Rightarrow> handler e | Inr v' \<Rightarrow> return v od" 287 288definition 289 handle_elseE :: "('s, 'x + 'a) state_monad \<Rightarrow> 290 ('x \<Rightarrow> ('s, 'x + 'a) state_monad) \<Rightarrow> 291 ('a \<Rightarrow> ('s, 'x + 'a) state_monad) \<Rightarrow> 292 ('s, 'x + 'a) state_monad" ("_ <handle> _ <else> _" 10) 293where 294 "f <handle> handler <else> continue \<equiv> 295 do v \<leftarrow> f; 296 case v of Inl e \<Rightarrow> handler e 297 | Inr v \<Rightarrow> continue v 298 od" 299 300definition 301 isSkip :: "('s, 'a) state_monad \<Rightarrow> bool" where 302 "isSkip m \<equiv> \<forall>s. \<exists>r. m s = (r,s)" 303 304lemma isSkip_bindI: "\<lbrakk> isSkip f; \<And>x. isSkip (g x) \<rbrakk> \<Longrightarrow> isSkip (f >>= g)" 305 apply (clarsimp simp: isSkip_def bind_def Let_def) 306 apply (erule_tac x=s in allE) 307 apply clarsimp 308 done 309 310lemma isSkip_return [simp,intro!]: 311 "isSkip (return x)" 312 by (simp add: isSkip_def return_def) 313 314lemma isSkip_gets [simp,intro!]: 315 "isSkip (gets x)" 316 by (simp add: isSkip_def gets_def get_def bind_def return_def) 317 318lemma isSkip_liftE [iff]: "isSkip (liftE f) = isSkip f" 319 apply (simp add: isSkip_def liftE_def Let_def split_def) 320 apply rule 321 apply clarsimp 322 apply (case_tac "f s") 323 apply (erule_tac x = s in allE) 324 apply simp 325 apply clarsimp 326 apply (case_tac "f s") 327 apply (erule_tac x = s in allE) 328 apply simp 329 done 330 331lemma isSkip_liftI [simp, intro!]: 332 "\<lbrakk> \<And>y. x = Inr y \<Longrightarrow> isSkip (f y) \<rbrakk> \<Longrightarrow> isSkip (lift f x)" 333 by (simp add: lift_def throwError_def return_def isSkip_def split: sum.splits) 334 335lemma isSkip_Error [iff]: 336 "isSkip (throwError x)" 337 by (simp add: throwError_def) 338 339lemma isSkip_returnOk [iff]: 340 "isSkip (returnOk x)" 341 by (simp add: returnOk_def) 342 343lemma isSkip_throw_opt [iff]: 344 "isSkip (throw_opt e x)" 345 by (simp add: throw_opt_def split: option.splits) 346 347lemma nested_bind [simp]: 348 "do x <- do y <- f; return (g y) od; h x od = 349 do y <- f; h (g y) od" 350 apply (clarsimp simp add: bind_def) 351 apply (rule ext) 352 apply (clarsimp simp add: Let_def split_def runState_def return_def) 353 done 354 355lemma skip_bind: 356 "isSkip s \<Longrightarrow> do _ \<leftarrow> s; g od = g" 357 apply (clarsimp simp add: bind_def) 358 apply (rule ext) 359 apply (clarsimp simp add: isSkip_def Let_def) 360 apply (erule_tac x=sa in allE) 361 apply clarsimp 362 done 363 364lemma bind_eqI: 365 "\<lbrakk> f = f'; \<And>x. g x = g' x \<rbrakk> \<Longrightarrow> f >>= g = f' >>= g'" 366 by (simp add: bind_def) 367 368lemma bind_cong [fundef_cong]: 369 "\<lbrakk> f = f'; \<And>v s s'. f' s = (v, s') \<Longrightarrow> g v s' = g' v s' \<rbrakk> \<Longrightarrow> f >>= g = f' >>= g'" 370 by (simp add: bind_def Let_def split_def) 371 372lemma bind'_cong [fundef_cong]: 373 "\<lbrakk> f = f'; \<And>v s s'. f' s = (v, s') \<Longrightarrow> g s' = g' s' \<rbrakk> \<Longrightarrow> bind' f g = bind' f' g'" 374 by (auto intro: bind_cong) 375 376lemma bindE_cong[fundef_cong]: 377 "\<lbrakk> M = M' ; \<And>v s s'. M' s = (Inr v, s') \<Longrightarrow> N v s' = N' v s' \<rbrakk> \<Longrightarrow> bindE M N = bindE M' N'" 378 apply (simp add: bindE_def) 379 apply (rule bind_cong) 380 apply (rule refl) 381 apply (unfold lift_def) 382 apply (case_tac v, simp_all) 383 done 384 385lemma bindE'_cong[fundef_cong]: 386 "\<lbrakk> M = M' ; \<And>v s s'. M' s = (Inr v, s') \<Longrightarrow> N s' = N' s' \<rbrakk> \<Longrightarrow> bindE' M N = bindE' M' N'" 387 by (auto intro: bindE_cong) 388 389definition 390 valid :: "('s \<Rightarrow> bool) \<Rightarrow> ('s,'a) state_monad \<Rightarrow> ('a \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> bool" ("\<lbrace>_\<rbrace> _ \<lbrace>_\<rbrace>") where 391 "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<equiv> \<forall>s. P s \<longrightarrow> split Q (f s)" 392 393definition 394 validE :: "('s \<Rightarrow> bool) \<Rightarrow> ('s, 'a + 'b) state_monad \<Rightarrow> ('b \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> 395 ('a \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> bool" ("\<lbrace>_\<rbrace> _ \<lbrace>_\<rbrace>, \<lbrace>_\<rbrace>") where 396 "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>R\<rbrace> \<equiv> \<forall>s. P s \<longrightarrow> split (\<lambda>r s. case r of Inr b \<Rightarrow> Q b s 397 | Inl a \<Rightarrow> R a s) (f s)" 398 399lemma validE_def2: 400 "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>R\<rbrace> \<equiv> \<lbrace>P\<rbrace> f \<lbrace> \<lambda>r s. case r of Inr b \<Rightarrow> Q b s | Inl a \<Rightarrow> R a s \<rbrace>" 401 by (unfold valid_def validE_def) 402 403(* FIXME: modernize *) 404syntax top :: "'a \<Rightarrow> bool" ("\<top>") 405 bottom :: "'a \<Rightarrow> bool" ("\<bottom>") 406 407translations 408 "\<top>" == "\<lambda>_. CONST True" 409 "\<bottom>" == "\<lambda>_. CONST False" 410 411definition 412 bipred_conj :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> bool)" (infixl "And" 96) 413where 414 "bipred_conj P Q \<equiv> \<lambda>x y. P x y \<and> Q x y" 415 416definition 417 bipred_disj :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> bool)" (infixl "Or" 91) 418where 419 "bipred_disj P Q \<equiv> \<lambda>x y. P x y \<or> Q x y" 420 421definition 422 bipred_neg :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> bool)" ("Not _") where 423 "bipred_neg P \<equiv> \<lambda>x y. \<not> P x y" 424 425syntax toptop :: "'a \<Rightarrow> 'b \<Rightarrow> bool" ("\<top>\<top>") 426 botbot :: "'a \<Rightarrow> 'b \<Rightarrow> bool" ("\<bottom>\<bottom>") 427 428translations "\<top>\<top>" == "\<lambda>_ _. CONST True" 429 "\<bottom>\<bottom>" == "\<lambda>_ _. CONST False" 430 431definition 432 pred_lift_exact :: "('a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> bool)" ("\<guillemotleft>_,_\<guillemotright>") where 433 "pred_lift_exact P Q \<equiv> \<lambda>x y. P x \<and> Q y" 434 435lemma pred_lift_taut[simp]: "\<guillemotleft>\<top>,\<top>\<guillemotright> = \<top>\<top>" 436 by (simp add:pred_lift_exact_def) 437 438lemma pred_lift_cont_l[simp]: "\<guillemotleft>\<bottom>,x\<guillemotright> = \<bottom>\<bottom>" 439 by (simp add:pred_lift_exact_def) 440 441lemma pred_lift_cont_r[simp]: "\<guillemotleft>x,\<bottom>\<guillemotright> = \<bottom>\<bottom>" 442 by (simp add:pred_lift_exact_def) 443 444lemma pred_liftI[intro!]: "\<lbrakk> P x; Q y \<rbrakk> \<Longrightarrow> \<guillemotleft>P,Q\<guillemotright> x y" 445 by (simp add:pred_lift_exact_def) 446 447lemma pred_exact_split: 448 "\<guillemotleft>P,Q\<guillemotright> = (\<guillemotleft>P,\<top>\<guillemotright> And \<guillemotleft>\<top>,Q\<guillemotright>)" 449 by (simp add:pred_lift_exact_def bipred_conj_def) 450 451lemma pred_andE[elim!]: "\<lbrakk> (A and B) x; \<lbrakk> A x; B x \<rbrakk> \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R" 452 by (simp add:pred_conj_def) 453 454lemma pred_andI[intro!]: "\<lbrakk> A x; B x \<rbrakk> \<Longrightarrow> (A and B) x" 455 by (simp add:pred_conj_def) 456 457lemma bipred_conj_app[simp]: "(P And Q) x = (P x and Q x)" 458 by (simp add:pred_conj_def bipred_conj_def) 459 460lemma bipred_disj_app[simp]: "(P Or Q) x = (P x or Q x)" 461 by (simp add:pred_disj_def bipred_disj_def) 462 463lemma pred_conj_app[simp]: "(P and Q) x = (P x \<and> Q x)" 464 by (simp add:pred_conj_def) 465 466lemma pred_disj_app[simp]: "(P or Q) x = (P x \<or> Q x)" 467 by (simp add:pred_disj_def) 468 469lemma pred_notnotD[simp]: "(not not P) = P" 470 by (simp add:pred_neg_def) 471 472lemma bipred_notnotD[simp]: "(Not Not P) = P" 473 by (simp add:bipred_neg_def) 474 475lemma pred_lift_add[simp]: "\<guillemotleft>P,Q\<guillemotright> x = ((\<lambda>s. P x) and Q)" 476 by (simp add:pred_lift_exact_def pred_conj_def) 477 478lemma pred_and_true[simp]: "(P and \<top>) = P" 479 by (simp add:pred_conj_def) 480 481lemma pred_and_true_var[simp]: "(\<top> and P) = P" 482 by (simp add:pred_conj_def) 483 484lemma pred_and_false[simp]: "(P and \<bottom>) = \<bottom>" 485 by (simp add:pred_conj_def) 486 487lemma pred_and_false_var[simp]: "(\<bottom> and P) = \<bottom>" 488 by (simp add:pred_conj_def) 489 490lemma seq': 491 "\<lbrakk> \<lbrace>A\<rbrace> f \<lbrace>B\<rbrace>; 492 \<forall>x. P x \<longrightarrow> \<lbrace>C\<rbrace> g x \<lbrace>D\<rbrace>; 493 \<forall>x s. B x s \<longrightarrow> P x \<and> C s \<rbrakk> \<Longrightarrow> 494 \<lbrace>A\<rbrace> do x \<leftarrow> f; g x od \<lbrace>D\<rbrace>" 495 apply (clarsimp simp: valid_def runState_def bind_def Let_def split_def) 496 apply (case_tac "f s") 497 apply fastforce 498 done 499 500 501lemma seq: 502 assumes "\<lbrace>A\<rbrace> f \<lbrace>B\<rbrace>" 503 assumes "\<And>x. P x \<Longrightarrow> \<lbrace>C\<rbrace> g x \<lbrace>D\<rbrace>" 504 assumes "\<And>x s. B x s \<Longrightarrow> P x \<and> C s" 505 shows "\<lbrace>A\<rbrace> do x \<leftarrow> f; g x od \<lbrace>D\<rbrace>" 506 using assms by (blast intro: seq') 507 508lemma seq_invar_nobind: 509 assumes f_valid: "\<lbrace>A\<rbrace> f \<lbrace>\<guillemotleft>\<top>,A\<guillemotright>\<rbrace>" 510 assumes g_valid: "\<And>x. \<lbrace>A\<rbrace> g x \<lbrace>\<guillemotleft>\<top>,A\<guillemotright>\<rbrace>" 511 shows "\<lbrace>A\<rbrace> do x \<leftarrow> f; g x od \<lbrace>\<guillemotleft>\<top>,A\<guillemotright>\<rbrace>" 512 apply(rule_tac B="\<guillemotleft>\<top>,A\<guillemotright>" and C="A" and P="\<top>" in seq) 513 apply(insert f_valid g_valid) 514 apply(simp_all add:pred_lift_exact_def) 515 done 516 517lemma seq_invar_bind: 518 assumes f_valid: "\<lbrace>A\<rbrace> f \<lbrace>\<guillemotleft>B,A\<guillemotright>\<rbrace>" 519 assumes g_valid: "\<And>x. P x \<Longrightarrow> \<lbrace>A\<rbrace> g x \<lbrace>\<guillemotleft>\<top>,A\<guillemotright>\<rbrace>" 520 assumes bind: "\<And>x. B x \<Longrightarrow> P x" 521 shows "\<lbrace>A\<rbrace> do x \<leftarrow> f; g x od \<lbrace>\<guillemotleft>\<top>,A\<guillemotright>\<rbrace>" 522 apply(rule_tac B="\<guillemotleft>B,A\<guillemotright>" and C="A" and P="P" in seq) 523 apply(insert f_valid g_valid bind) 524 apply(simp_all add: pred_lift_exact_def) 525 done 526 527lemma seq_noimp: 528 assumes f_valid: "\<lbrace>A\<rbrace> f \<lbrace>\<guillemotleft>C,B\<guillemotright>\<rbrace>" 529 assumes g_valid: "\<And>x. C x \<Longrightarrow> \<lbrace>B\<rbrace> g x \<lbrace>D\<rbrace>" 530 shows "\<lbrace>A\<rbrace> do x \<leftarrow> f; g x od \<lbrace>D\<rbrace>" 531 apply(rule_tac B="\<guillemotleft>C,B\<guillemotright>" and C="B" and P="C" in seq) 532 apply(insert f_valid g_valid, simp_all add:pred_lift_exact_def) 533 done 534 535lemma seq_ext': 536 "\<lbrakk> \<lbrace>A\<rbrace> f \<lbrace>B\<rbrace>; \<forall>x. \<lbrace>B x\<rbrace> g x \<lbrace>C\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>A\<rbrace> do x \<leftarrow> f; g x od \<lbrace>C\<rbrace>" 537 by (clarsimp simp: valid_def runState_def bind_def Let_def split_def) 538 539lemma seq_ext: 540 assumes "\<lbrace>A\<rbrace> f \<lbrace>B\<rbrace>" "\<And>x. \<lbrace>B x\<rbrace> g x \<lbrace>C\<rbrace>" 541 shows "\<lbrace>A\<rbrace> do x \<leftarrow> f; g x od \<lbrace>C\<rbrace>" 542 using assms by (blast intro: seq_ext') 543 544lemma seqE': 545 "\<lbrakk> \<lbrace>A\<rbrace> f \<lbrace>B\<rbrace>,\<lbrace>E\<rbrace>; 546 \<forall>x. \<lbrace>B x\<rbrace> g x \<lbrace>C\<rbrace>,\<lbrace>E\<rbrace> \<rbrakk> \<Longrightarrow> 547 \<lbrace>A\<rbrace> doE x \<leftarrow> f; g x odE \<lbrace>C\<rbrace>,\<lbrace>E\<rbrace>" 548 apply(simp add: bindE_def lift_def bind_def Let_def split_def) 549 apply(clarsimp simp: validE_def) 550 apply(rename_tac s r x) 551 apply(case_tac "fst (f s)"; case_tac r; fastforce simp:throwError_def return_def) 552 done 553 554lemma seqE: 555 assumes "\<lbrace>A\<rbrace> f \<lbrace>B\<rbrace>,\<lbrace>E\<rbrace>" "\<And>x. \<lbrace>B x\<rbrace> g x \<lbrace>C\<rbrace>,\<lbrace>E\<rbrace>" 556 shows "\<lbrace>A\<rbrace> doE x \<leftarrow> f; g x odE \<lbrace>C\<rbrace>,\<lbrace>E\<rbrace>" 557 using assms by(blast intro: seqE') 558 559lemma get_sp: 560 "\<lbrace>P\<rbrace> get \<lbrace>\<lambda>a s. s = a \<and> P s\<rbrace>" 561 by (simp add:get_def valid_def) 562 563lemma put_sp: 564 "\<lbrace>\<top>\<rbrace> put a \<lbrace>\<lambda>_ s. s = a\<rbrace>" 565 by (simp add:put_def valid_def) 566 567lemma return_sp: 568 "\<lbrace>P\<rbrace> return a \<lbrace>\<lambda>b s. b = a \<and> P s\<rbrace>" 569 by (simp add:return_def valid_def) 570 571lemma hoare_post_conj [intro!]: 572 "\<lbrakk> \<lbrace> P \<rbrace> a \<lbrace> Q \<rbrace>; \<lbrace> P \<rbrace> a \<lbrace> R \<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace> P \<rbrace> a \<lbrace> Q And R \<rbrace>" 573 by (simp add:valid_def split_def bipred_conj_def) 574 575lemma hoare_pre_disj [intro!]: 576 "\<lbrakk> \<lbrace> P \<rbrace> a \<lbrace> R \<rbrace>; \<lbrace> Q \<rbrace> a \<lbrace> R \<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace> P or Q \<rbrace> a \<lbrace> R \<rbrace>" 577 by (simp add:valid_def pred_disj_def) 578 579lemma hoare_post_taut [iff]: "\<lbrace> P \<rbrace> a \<lbrace> \<top>\<top> \<rbrace>" 580 by (simp add:valid_def) 581 582lemma hoare_pre_cont [iff]: "\<lbrace> \<bottom> \<rbrace> a \<lbrace> P \<rbrace>" 583 by (simp add:valid_def) 584 585lemma hoare_return [intro!]: "\<And>x. P x \<Longrightarrow> \<lbrace> Q \<rbrace> return x \<lbrace> \<guillemotleft>P,Q\<guillemotright> \<rbrace>" 586 by (simp add:valid_def return_def pred_lift_exact_def) 587 588lemma hoare_return_drop [iff]: "\<lbrace> Q \<rbrace> return x \<lbrace> \<guillemotleft>\<top>,Q\<guillemotright> \<rbrace>" 589 by (simp add:valid_def return_def pred_lift_exact_def) 590 591lemma hoare_return_drop_var [iff]: "\<lbrace> Q \<rbrace> return x \<lbrace> \<lambda>r. Q \<rbrace>" 592 by (simp add:valid_def return_def pred_lift_exact_def) 593 594lemma hoare_return_only [intro!]: "\<And>x. P x \<Longrightarrow> \<lbrace> Q \<rbrace> return x \<lbrace> \<guillemotleft>P,\<top>\<guillemotright> \<rbrace>" 595 by (simp add:valid_def return_def pred_lift_exact_def) 596 597lemma hoare_get [iff]: "\<lbrace> P \<rbrace> get \<lbrace> \<guillemotleft>P,P\<guillemotright> \<rbrace>" 598 by (simp add:valid_def get_def pred_lift_exact_def) 599 600lemma hoare_gets [intro!]: "\<lbrakk> \<And>s. P s \<Longrightarrow> Q (f s) s \<rbrakk> \<Longrightarrow> \<lbrace> P \<rbrace> gets f \<lbrace> Q \<rbrace>" 601 by (simp add:valid_def gets_def get_def bind_def return_def) 602 603lemma hoare_modify [iff]: "\<lbrace> P o f \<rbrace> modify f \<lbrace> \<guillemotleft>\<top>,P\<guillemotright> \<rbrace>" 604 by (simp add:valid_def modify_def pred_lift_exact_def put_def bind_def get_def) 605 606lemma hoare_modifyE [intro!]: "\<lbrakk> \<And>s. P s \<Longrightarrow> Q (f s) \<rbrakk> \<Longrightarrow> \<lbrace> P \<rbrace> modify f \<lbrace> \<guillemotleft>\<top>,Q\<guillemotright> \<rbrace>" 607 by (simp add:valid_def modify_def pred_lift_exact_def put_def bind_def get_def) 608 609lemma hoare_modifyE_var [intro!]: "\<lbrakk> \<And>s. P s \<Longrightarrow> Q (f s) \<rbrakk> \<Longrightarrow> \<lbrace> P \<rbrace> modify f \<lbrace> \<lambda>r s. Q s \<rbrace>" 610 by (simp add:valid_def modify_def pred_lift_exact_def put_def bind_def get_def) 611 612lemma hoare_put [intro!]: "P x \<Longrightarrow> \<lbrace> Q \<rbrace> put x \<lbrace> \<guillemotleft>\<top>,P\<guillemotright>\<rbrace>" 613 by (simp add:valid_def put_def pred_lift_exact_def) 614 615lemma hoare_if [intro!]: 616 "\<lbrakk> P \<Longrightarrow> \<lbrace> Q \<rbrace> a \<lbrace> R \<rbrace>; \<not> P \<Longrightarrow> \<lbrace> Q \<rbrace> b \<lbrace> R \<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace> Q \<rbrace> if P then a else b \<lbrace> R \<rbrace>" 617 by (simp add:valid_def) 618 619lemma hoare_when [intro!]: 620 "\<lbrakk> \<lbrakk> P \<rbrakk> \<Longrightarrow> \<lbrace> Q \<rbrace> a \<lbrace> \<guillemotleft>\<top>,R\<guillemotright> \<rbrace>; \<And>s. \<lbrakk> \<not> P; Q s \<rbrakk> \<Longrightarrow> R s \<rbrakk> \<Longrightarrow> 621 \<lbrace> Q \<rbrace> when P a \<lbrace> \<guillemotleft>\<top>,R\<guillemotright> \<rbrace>" 622 by (simp add:valid_def when_def split_def return_def pred_lift_exact_def) 623 624lemma hoare_unless [intro!]: 625 "\<lbrakk> \<And>s. \<lbrakk> P; Q s \<rbrakk> \<Longrightarrow> R s; \<lbrakk> \<not> P \<rbrakk> \<Longrightarrow> \<lbrace> Q \<rbrace> a \<lbrace> \<guillemotleft>\<top>,R\<guillemotright> \<rbrace> \<rbrakk> \<Longrightarrow> 626 \<lbrace> Q \<rbrace> unless P a \<lbrace> \<guillemotleft>\<top>,R\<guillemotright> \<rbrace>" 627 by (simp add:valid_def unless_def split_def when_def return_def pred_lift_exact_def) 628 629lemma hoare_pre_subst: "\<lbrakk> A = B; \<lbrace>A\<rbrace> a \<lbrace>C\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>B\<rbrace> a \<lbrace>C\<rbrace>" 630 by (clarsimp simp:valid_def split_def) 631 632lemma hoare_post_subst: "\<lbrakk> B = C; \<lbrace>A\<rbrace> a \<lbrace>B\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>A\<rbrace> a \<lbrace>C\<rbrace>" 633 by (clarsimp simp:valid_def split_def) 634 635lemma hoare_pre_tautI: "\<lbrakk> \<lbrace>A and P\<rbrace> a \<lbrace>B\<rbrace>; \<lbrace>A and not P\<rbrace> a \<lbrace>B\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>A\<rbrace> a \<lbrace>B\<rbrace>" 636 by (clarsimp simp:valid_def split_def pred_conj_def pred_neg_def, blast) 637 638lemma hoare_return_var[intro!]: "\<lbrakk> \<And>x. P x \<Longrightarrow> Q x \<rbrakk> \<Longrightarrow> (\<And>x. P x \<Longrightarrow> \<lbrace>R\<rbrace> return x \<lbrace>\<guillemotleft>Q,R\<guillemotright>\<rbrace>)" 639 by (rule hoare_return) 640 641lemma hoare_return_drop_imp[intro!]: "\<lbrakk> \<And>s. P s \<Longrightarrow> Q s \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> return x \<lbrace>\<guillemotleft>\<top>,Q\<guillemotright>\<rbrace>" 642 by (simp add:valid_def return_def) 643 644lemmas hoare_case_option_inference = option.exhaust 645 646lemma hoare_pre_imp: "\<lbrakk> \<lbrace>Q\<rbrace> a \<lbrace>R\<rbrace>; \<And>s. P s \<Longrightarrow> Q s \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> a \<lbrace>R\<rbrace>" 647 by (simp add:valid_def) 648 649lemma hoare_post_imp: "\<lbrakk> \<lbrace>P\<rbrace> a \<lbrace>Q\<rbrace>; \<And>r s. Q r s \<Longrightarrow> R r s \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> a \<lbrace>R\<rbrace>" 650 by (simp add:valid_def split_def) 651 652lemma hoare_post_impE: 653 "\<lbrakk> \<lbrace>P\<rbrace> a \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>; \<And>r s. Q r s \<Longrightarrow> R r s; \<And>e s. E e s \<Longrightarrow> F e s \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> a \<lbrace>R\<rbrace>,\<lbrace>F\<rbrace>" 654 apply(clarsimp simp: validE_def) 655 apply(rename_tac s r x) 656 apply(case_tac r; fastforce) 657 done 658 659lemma "isSkip f \<Longrightarrow> \<lbrace> P \<rbrace> f \<lbrace> \<guillemotleft>\<top>,P\<guillemotright> \<rbrace>" 660 apply (clarsimp simp: valid_def split_def isSkip_def) 661 apply (rename_tac s) 662 apply (case_tac "f s") 663 apply (erule_tac x=s in allE) 664 apply auto 665 done 666 667end 668