1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6theory TraceMonad 7imports 8 Lib 9 Strengthen 10begin 11 12text \<open> 13The ``Interference Trace Monad''. This nondeterministic monad 14records the state at every interference point, permitting 15nondeterministic interference by the environment at interference 16points. 17 18The trace set initially includes all possible environment behaviours. 19Trace steps are tagged as environment or self actions, and can then 20be constrained to a smaller set where the environment acts according 21to a rely constraint (i.e. rely-guarantee reasoning), or to set the 22environment actions to be the self actions of another program (parallel 23composition). 24\<close> 25 26section "The Trace Monad" 27 28text \<open>Trace monad identifier. Me corresponds to the current thread running and Env to the environment.\<close> 29datatype tmid = Me | Env 30 31text \<open>Results associated with traces. Traces may correspond to incomplete, failed, or completed executions.\<close> 32datatype ('s, 'a) tmres = Failed | Incomplete | Result "('a \<times> 's)" 33 34abbreviation 35 map_tmres_rv :: "('a \<Rightarrow> 'b) \<Rightarrow> ('s, 'a) tmres \<Rightarrow> ('s, 'b) tmres" 36where 37 "map_tmres_rv f \<equiv> map_tmres id f" 38 39section "The Monad" 40 41text \<open> tmonad returns a set of non-deterministic computations, including 42 a trace as a list of "thread identifier" \<times> state, and an optional 43 pair result, state when the computation did not fail. \<close> 44type_synonym ('s, 'a) tmonad = "'s \<Rightarrow> ((tmid \<times> 's) list \<times> ('s, 'a) tmres) set" 45 46text \<open>Returns monad results, ignoring failures and traces.\<close> 47definition 48 mres :: "((tmid \<times> 's) list \<times> ('s, 'a) tmres) set \<Rightarrow> ('a \<times> 's) set" 49where 50 "mres r = Result -` (snd ` r)" 51 52text \<open> 53 The definition of fundamental monad functions @{text return} and 54 @{text bind}. The monad function @{text "return x"} does not change 55 the state, does not fail, and returns @{text "x"}. 56\<close> 57definition 58 return :: "'a \<Rightarrow> ('s,'a) tmonad" 59where 60 "return a \<equiv> \<lambda>s. ({([], Result (a, s))})" 61 62text \<open> 63 The monad function @{text "bind f g"}, also written @{text "f >>= g"}, 64 is the execution of @{term f} followed by the execution of @{text g}. 65 The function @{text g} takes the result value \emph{and} the result 66 state of @{text f} as parameter. The definition says that the result of 67 the combined operation is the union of the set of sets that is created 68 by @{text g} applied to the result sets of @{text f}. The combined 69 operation may have failed, if @{text f} may have failed or @{text g} may 70 have failed on any of the results of @{text f}. 71\<close> 72 73abbreviation (input) 74 fst_upd :: "('a \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c \<times> 'b" 75where 76 "fst_upd f \<equiv> \<lambda>(a,b). (f a, b)" 77 78abbreviation (input) 79 snd_upd :: "('b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'a \<times> 'c" 80where 81 "snd_upd f \<equiv> \<lambda>(a,b). (a, f b)" 82 83definition 84 bind :: "('s, 'a) tmonad \<Rightarrow> ('a \<Rightarrow> ('s, 'b) tmonad) \<Rightarrow> 85 ('s, 'b) tmonad" (infixl ">>=" 60) 86where 87 "bind f g \<equiv> \<lambda>s. \<Union>(xs, r) \<in> (f s). case r of Failed \<Rightarrow> {(xs, Failed)} 88 | Incomplete \<Rightarrow> {(xs, Incomplete)} 89 | Result (rv, s) \<Rightarrow> fst_upd (\<lambda>ys. ys @ xs) ` g rv s" 90 91text \<open>Sometimes it is convenient to write @{text bind} in reverse order.\<close> 92abbreviation(input) 93 bind_rev :: "('c \<Rightarrow> ('a, 'b) tmonad) \<Rightarrow> ('a, 'c) tmonad \<Rightarrow> 94 ('a, 'b) tmonad" (infixl "=<<" 60) 95where 96 "g =<< f \<equiv> f >>= g" 97 98text \<open> 99 The basic accessor functions of the state monad. @{text get} returns 100 the current state as result, does not fail, and does not change the state. 101 @{text "put s"} returns nothing (@{typ unit}), changes the current state 102 to @{text s} and does not fail. 103\<close> 104definition 105 get :: "('s,'s) tmonad" 106where 107 "get \<equiv> \<lambda>s. {([], Result (s, s))}" 108 109definition 110 put :: "'s \<Rightarrow> ('s, unit) tmonad" 111where 112 "put s \<equiv> \<lambda>st. {([], Result ((), s))}" 113 114definition 115 put_trace_elem :: "(tmid \<times> 's) \<Rightarrow> ('s, unit) tmonad" 116where 117 "put_trace_elem x = (\<lambda>s. {([], Incomplete), ([x], Result ((), s))})" 118 119primrec 120 put_trace :: "(tmid \<times> 's) list \<Rightarrow> ('s, unit) tmonad" 121where 122 "put_trace [] = return ()" 123 | "put_trace (x # xs) = (put_trace xs >>= (\<lambda>_. put_trace_elem x))" 124 125subsection "Nondeterminism" 126 127text \<open> 128 Basic nondeterministic functions. @{text "select A"} chooses an element 129 of the set @{text A}, does not change the state, and does not fail 130 (even if the set is empty). @{text "f OR g"} executes @{text f} or 131 executes @{text g}. It retuns the union of results of @{text f} and 132 @{text g}, and may have failed if either may have failed. 133\<close> 134definition 135 select :: "'a set \<Rightarrow> ('s, 'a) tmonad" 136where 137 (* Should we have Failed when A = {} ? *) 138 "select A \<equiv> \<lambda>s. (Pair [] ` Result ` (A \<times> {s}))" 139 140definition 141 alternative :: "('s,'a) tmonad \<Rightarrow> ('s,'a) tmonad \<Rightarrow> 142 ('s,'a) tmonad" 143 (infixl "OR" 20) 144where 145 "f OR g \<equiv> \<lambda>s. (f s \<union> g s)" 146 147text \<open> Alternative notation for @{text OR} \<close> 148notation (xsymbols) alternative (infixl "\<sqinter>" 20) 149 150 151text \<open> The @{text selet_f} function was left out here until we figure 152 out what variant we actually need. 153\<close> 154 155subsection "Failure" 156 157text \<open> The monad function that always fails. Returns an empty set of 158results and sets the failure flag. \<close> 159definition 160 fail :: "('s, 'a) tmonad" 161where 162 "fail \<equiv> \<lambda>s. {([], Failed)}" 163 164text \<open> Assertions: fail if the property @{text P} is not true \<close> 165definition 166 assert :: "bool \<Rightarrow> ('a, unit) tmonad" 167where 168 "assert P \<equiv> if P then return () else fail" 169 170text \<open> Fail if the value is @{const None}, 171 return result @{text v} for @{term "Some v"} \<close> 172definition 173 assert_opt :: "'a option \<Rightarrow> ('b, 'a) tmonad" 174where 175 "assert_opt v \<equiv> case v of None \<Rightarrow> fail | Some v \<Rightarrow> return v" 176 177text \<open> An assertion that also can introspect the current state. \<close> 178 179definition 180 state_assert :: "('s \<Rightarrow> bool) \<Rightarrow> ('s, unit) tmonad" 181where 182 "state_assert P \<equiv> get >>= (\<lambda>s. assert (P s))" 183 184subsection "Generic functions on top of the state monad" 185 186text \<open> Apply a function to the current state and return the result 187without changing the state. \<close> 188definition 189 gets :: "('s \<Rightarrow> 'a) \<Rightarrow> ('s, 'a) tmonad" 190where 191 "gets f \<equiv> get >>= (\<lambda>s. return (f s))" 192 193text \<open> Modify the current state using the function passed in. \<close> 194definition 195 modify :: "('s \<Rightarrow> 's) \<Rightarrow> ('s, unit) tmonad" 196where 197 "modify f \<equiv> get >>= (\<lambda>s. put (f s))" 198 199lemma simpler_gets_def: "gets f = (\<lambda>s. {([], Result ((f s), s))})" 200 by (simp add: fun_eq_iff gets_def return_def bind_def get_def split_def) 201 202lemma simpler_modify_def: 203 "modify f = (\<lambda>s. {([], Result ((),(f s)))})" 204 by (simp add: fun_eq_iff modify_def bind_def get_def put_def split_def) 205 206text \<open> Execute the given monad when the condition is true, 207 return @{text "()"} otherwise. \<close> 208definition 209 "when" :: "bool \<Rightarrow> ('s, unit) tmonad \<Rightarrow> 210 ('s, unit) tmonad" 211where 212 "when P m \<equiv> if P then m else return ()" 213 214text \<open> Execute the given monad unless the condition is true, 215 return @{text "()"} otherwise. \<close> 216definition 217 unless :: "bool \<Rightarrow> ('s, unit) tmonad \<Rightarrow> 218 ('s, unit) tmonad" 219where 220 "unless P m \<equiv> when (\<not>P) m" 221 222text \<open> 223 Perform a test on the current state, performing the left monad if 224 the result is true or the right monad if the result is false. 225\<close> 226definition 227 condition :: "('s \<Rightarrow> bool) \<Rightarrow> ('s, 'r) tmonad \<Rightarrow> ('s, 'r) tmonad \<Rightarrow> ('s, 'r) tmonad" 228where 229 "condition P L R \<equiv> \<lambda>s. if (P s) then (L s) else (R s)" 230 231notation (output) 232 condition ("(condition (_)// (_)// (_))" [1000,1000,1000] 1000) 233 234text \<open> 235Apply an option valued function to the current state, fail 236if it returns @{const None}, return @{text v} if it returns 237@{term "Some v"}. 238\<close> 239definition 240 gets_the :: "('s \<Rightarrow> 'a option) \<Rightarrow> ('s, 'a) tmonad" 241where 242 "gets_the f \<equiv> gets f >>= assert_opt" 243 244 245subsection \<open> The Monad Laws \<close> 246 247text \<open>An alternative definition of bind, sometimes more convenient.\<close> 248lemma bind_def2: 249 "bind f g \<equiv> (\<lambda>s. ((\<lambda>xs. (xs, Failed)) ` {xs. (xs, Failed) \<in> f s}) 250 \<union> ((\<lambda>xs. (xs, Incomplete)) ` {xs. (xs, Incomplete) \<in> f s}) 251 \<union> (\<Union>(xs, rv, s) \<in> {(xs, rv, s'). (xs, Result (rv, s')) \<in> f s}. fst_upd (\<lambda>ys. ys @ xs) ` g rv s))" 252 apply (clarsimp simp add: bind_def fun_eq_iff 253 Un_Union_image split_def 254 intro!: eq_reflection) 255 apply (auto split: tmres.splits elim!:rev_bexI[where A="f x" for x]) 256 apply (fastforce intro: image_eqI[rotated]) 257 done 258 259lemma elem_bindE: 260 "(tr, res) \<in> bind f (\<lambda>x. g x) s 261 \<Longrightarrow> ((res = Incomplete | res = Failed) \<Longrightarrow> (tr, map_tmres undefined undefined res) \<in> f s \<Longrightarrow> P) 262 \<Longrightarrow> (\<And>tr' tr'' x s'. (tr', Result (x, s')) \<in> f s \<Longrightarrow> (tr'', res) \<in> g x s' 263 \<Longrightarrow> tr = tr'' @ tr' \<Longrightarrow> P) 264 \<Longrightarrow> P" 265 by (auto simp: bind_def2) 266 267text \<open> Each monad satisfies at least the following three laws. \<close> 268 269text \<open> @{term return} is absorbed at the left of a @{term bind}, 270 applying the return value directly: \<close> 271 272declare map_option.identity[simp] 273 274lemma return_bind [simp]: "(return x >>= f) = f x" 275 by (auto simp add: return_def bind_def split_def split:if_splits) 276 277text \<open> @{term return} is absorbed on the right of a @{term bind} \<close> 278lemma bind_return [simp]: "(m >>= return) = m" 279 by (auto simp add: fun_eq_iff bind_def return_def 280 split: tmres.splits) 281 282text \<open> @{term bind} is associative \<close> 283lemma bind_assoc: 284 fixes m :: "('a,'b) tmonad" 285 fixes f :: "'b \<Rightarrow> ('a,'c) tmonad" 286 fixes g :: "'c \<Rightarrow> ('a,'d) tmonad" 287 shows "(m >>= f) >>= g = m >>= (\<lambda>x. f x >>= g)" 288 apply (unfold bind_def Let_def split_def) 289 apply (rule ext) 290 apply clarsimp 291 apply (rule SUP_cong[OF refl], clarsimp) 292 apply (split tmres.split; intro conjI impI; clarsimp) 293 apply (simp add: image_Union) 294 apply (rule SUP_cong[OF refl], clarsimp) 295 apply (split tmres.split; intro conjI impI; clarsimp) 296 apply (simp add: image_image) 297 done 298 299section \<open> Adding Exceptions \<close> 300 301text \<open> 302 The type @{typ "('s,'a) tmonad"} gives us nondeterminism and 303 failure. We now extend this monad with exceptional return values 304 that abort normal execution, but can be handled explicitly. 305 We use the sum type to indicate exceptions. 306 307 In @{typ "('s, 'e + 'a) tmonad"}, @{typ "'s"} is the state, 308 @{typ 'e} is an exception, and @{typ 'a} is a normal return value. 309 310 This new type itself forms a monad again. Since type classes in 311 Isabelle are not powerful enough to express the class of monads, 312 we provide new names for the @{term return} and @{term bind} functions 313 in this monad. We call them @{text returnOk} (for normal return values) 314 and @{text bindE} (for composition). We also define @{text throwError} 315 to return an exceptional value. 316\<close> 317definition 318 returnOk :: "'a \<Rightarrow> ('s, 'e + 'a) tmonad" 319where 320 "returnOk \<equiv> return o Inr" 321 322definition 323 throwError :: "'e \<Rightarrow> ('s, 'e + 'a) tmonad" 324where 325 "throwError \<equiv> return o Inl" 326 327text \<open> 328 Lifting a function over the exception type: if the input is an 329 exception, return that exception; otherwise continue execution. 330\<close> 331definition 332 lift :: "('a \<Rightarrow> ('s, 'e + 'b) tmonad) \<Rightarrow> 333 'e +'a \<Rightarrow> ('s, 'e + 'b) tmonad" 334where 335 "lift f v \<equiv> case v of Inl e \<Rightarrow> throwError e 336 | Inr v' \<Rightarrow> f v'" 337 338text \<open> 339 The definition of @{term bind} in the exception monad (new 340 name @{text bindE}): the same as normal @{term bind}, but 341 the right-hand side is skipped if the left-hand side 342 produced an exception. 343\<close> 344definition 345 bindE :: "('s, 'e + 'a) tmonad \<Rightarrow> 346 ('a \<Rightarrow> ('s, 'e + 'b) tmonad) \<Rightarrow> 347 ('s, 'e + 'b) tmonad" (infixl ">>=E" 60) 348where 349 "bindE f g \<equiv> bind f (lift g)" 350 351 352text \<open> 353 Lifting a normal nondeterministic monad into the 354 exception monad is achieved by always returning its 355 result as normal result and never throwing an exception. 356\<close> 357definition 358 liftE :: "('s,'a) tmonad \<Rightarrow> ('s, 'e+'a) tmonad" 359where 360 "liftE f \<equiv> f >>= (\<lambda>r. return (Inr r))" 361 362 363text \<open> 364 Since the underlying type and @{text return} function changed, 365 we need new definitions for when and unless: 366\<close> 367definition 368 whenE :: "bool \<Rightarrow> ('s, 'e + unit) tmonad \<Rightarrow> 369 ('s, 'e + unit) tmonad" 370where 371 "whenE P f \<equiv> if P then f else returnOk ()" 372 373definition 374 unlessE :: "bool \<Rightarrow> ('s, 'e + unit) tmonad \<Rightarrow> 375 ('s, 'e + unit) tmonad" 376where 377 "unlessE P f \<equiv> if P then returnOk () else f" 378 379 380text \<open> 381 Throwing an exception when the parameter is @{term None}, otherwise 382 returning @{term "v"} for @{term "Some v"}. 383\<close> 384definition 385 throw_opt :: "'e \<Rightarrow> 'a option \<Rightarrow> ('s, 'e + 'a) tmonad" 386where 387 "throw_opt ex x \<equiv> 388 case x of None \<Rightarrow> throwError ex | Some v \<Rightarrow> returnOk v" 389 390 391text \<open> 392 Failure in the exception monad is redefined in the same way 393 as @{const whenE} and @{const unlessE}, with @{term returnOk} 394 instead of @{term return}. 395\<close> 396definition 397 assertE :: "bool \<Rightarrow> ('a, 'e + unit) tmonad" 398where 399 "assertE P \<equiv> if P then returnOk () else fail" 400 401subsection "Monad Laws for the Exception Monad" 402 403text \<open> More direct definition of @{const liftE}: \<close> 404lemma liftE_def2: 405 "liftE f = (\<lambda>s. snd_upd (map_tmres_rv Inr) ` (f s))" 406 apply (clarsimp simp: fun_eq_iff liftE_def return_def split_def bind_def image_def) 407 apply (rule set_eqI) 408 apply (rule iffI) 409 apply clarsimp 410 apply (erule rev_bexI[where A="f s" for s]) 411 apply (clarsimp split: tmres.splits) 412 apply clarsimp 413 apply (rule exI) 414 apply (rule conjI) 415 apply (erule rev_bexI[where A="f s" for s]) 416 apply (rule refl) 417 apply (clarsimp split: tmres.splits) 418 done 419 420text \<open> Left @{const returnOk} absorbtion over @{term bindE}: \<close> 421lemma returnOk_bindE [simp]: "(returnOk x >>=E f) = f x" 422 apply (unfold bindE_def returnOk_def) 423 apply (clarsimp simp: lift_def) 424 done 425 426lemma lift_return [simp]: 427 "lift (return \<circ> Inr) = return" 428 by (simp add: fun_eq_iff lift_def throwError_def split: sum.splits) 429 430text \<open> Right @{const returnOk} absorbtion over @{term bindE}: \<close> 431lemma bindE_returnOk [simp]: "(m >>=E returnOk) = m" 432 by (simp add: bindE_def returnOk_def) 433 434text \<open> Associativity of @{const bindE}: \<close> 435lemma bindE_assoc: 436 "(m >>=E f) >>=E g = m >>=E (\<lambda>x. f x >>=E g)" 437 apply (simp add: bindE_def bind_assoc) 438 apply (rule arg_cong [where f="\<lambda>x. m >>= x"]) 439 apply (rule ext) 440 apply (case_tac x, simp_all add: lift_def throwError_def) 441 done 442 443text \<open> @{const returnOk} could also be defined via @{const liftE}: \<close> 444lemma returnOk_liftE: 445 "returnOk x = liftE (return x)" 446 by (simp add: liftE_def returnOk_def) 447 448text \<open> Execution after throwing an exception is skipped: \<close> 449lemma throwError_bindE [simp]: 450 "(throwError E >>=E f) = throwError E" 451 by (simp add: fun_eq_iff bindE_def bind_def throwError_def lift_def return_def split_def) 452 453 454section "Syntax" 455 456text \<open> This section defines traditional Haskell-like do-syntax 457 for the state monad in Isabelle. \<close> 458 459subsection "Syntax for the Nondeterministic State Monad" 460 461text \<open> We use @{text K_bind} to syntactically indicate the 462 case where the return argument of the left side of a @{term bind} 463 is ignored \<close> 464definition 465 K_bind_def [iff]: "K_bind \<equiv> \<lambda>x y. x" 466 467nonterminal 468 dobinds and dobind and nobind 469 470syntax 471 "_dobind" :: "[pttrn, 'a] => dobind" ("(_ <-/ _)" 10) 472 "" :: "dobind => dobinds" ("_") 473 "_nobind" :: "'a => dobind" ("_") 474 "_dobinds" :: "[dobind, dobinds] => dobinds" ("(_);//(_)") 475 476 "_do" :: "[dobinds, 'a] => 'a" ("(do ((_);//(_))//od)" 100) 477syntax (xsymbols) 478 "_dobind" :: "[pttrn, 'a] => dobind" ("(_ \<leftarrow>/ _)" 10) 479 480translations 481 "_do (_dobinds b bs) e" == "_do b (_do bs e)" 482 "_do (_nobind b) e" == "b >>= (CONST K_bind e)" 483 "do x <- a; e od" == "a >>= (\<lambda>x. e)" 484 485text \<open> Syntax examples: \<close> 486lemma "do x \<leftarrow> return 1; 487 return (2::nat); 488 return x 489 od = 490 return 1 >>= 491 (\<lambda>x. return (2::nat) >>= 492 K_bind (return x))" 493 by (rule refl) 494 495lemma "do x \<leftarrow> return 1; 496 return 2; 497 return x 498 od = return 1" 499 by simp 500 501subsection "Interference command" 502 503text \<open>Interference commands must be inserted in between actions that can be interfered with commands 504running in other threads. \<close> 505 506definition 507 last_st_tr :: "(tmid * 's) list \<Rightarrow> 's \<Rightarrow> 's" 508where 509 "last_st_tr tr s0 = (hd (map snd tr @ [s0]))" 510 511definition 512 env_steps :: "('s,unit) tmonad" 513where 514 "env_steps \<equiv> 515 do 516 s \<leftarrow> get; 517 \<comment> \<open>Add unfiltered environment events to the trace\<close> 518 xs \<leftarrow> select UNIV; 519 tr \<leftarrow> return (map (Pair Env) xs); 520 put_trace tr; 521 \<comment> \<open>Pick the last event of the trace as the final state\<close> 522 put (last_st_tr tr s) 523 od" 524 525definition 526 commit_step :: "('s, unit) tmonad" 527where 528 "commit_step \<equiv> 529 do 530 s \<leftarrow> get; 531 put_trace [(Me,s)] 532 od" 533 534definition 535 interference :: "('s,unit) tmonad" 536where 537 "interference \<equiv> 538 do 539 commit_step; 540 env_steps 541 od" 542 543subsection "Syntax for the Exception Monad" 544 545text \<open> 546 Since the exception monad is a different type, we 547 need to syntactically distinguish it in the syntax. 548 We use @{text doE}/@{text odE} for this, but can re-use 549 most of the productions from @{text do}/@{text od} 550 above. 551\<close> 552 553syntax 554 "_doE" :: "[dobinds, 'a] => 'a" ("(doE ((_);//(_))//odE)" 100) 555 556translations 557 "_doE (_dobinds b bs) e" == "_doE b (_doE bs e)" 558 "_doE (_nobind b) e" == "b >>=E (CONST K_bind e)" 559 "doE x <- a; e odE" == "a >>=E (\<lambda>x. e)" 560 561text \<open> Syntax examples: \<close> 562lemma "doE x \<leftarrow> returnOk 1; 563 returnOk (2::nat); 564 returnOk x 565 odE = 566 returnOk 1 >>=E 567 (\<lambda>x. returnOk (2::nat) >>=E 568 K_bind (returnOk x))" 569 by (rule refl) 570 571lemma "doE x \<leftarrow> returnOk 1; 572 returnOk 2; 573 returnOk x 574 odE = returnOk 1" 575 by simp 576 577 578 579section "Library of additional Monadic Functions and Combinators" 580 581 582text \<open> Lifting a normal function into the monad type: \<close> 583definition 584 liftM :: "('a \<Rightarrow> 'b) \<Rightarrow> ('s,'a) tmonad \<Rightarrow> ('s, 'b) tmonad" 585where 586 "liftM f m \<equiv> do x \<leftarrow> m; return (f x) od" 587 588text \<open> The same for the exception monad: \<close> 589definition 590 liftME :: "('a \<Rightarrow> 'b) \<Rightarrow> ('s,'e+'a) tmonad \<Rightarrow> ('s,'e+'b) tmonad" 591where 592 "liftME f m \<equiv> doE x \<leftarrow> m; returnOk (f x) odE" 593 594text \<open> Run a sequence of monads from left to right, ignoring return values. \<close> 595definition 596 sequence_x :: "('s, 'a) tmonad list \<Rightarrow> ('s, unit) tmonad" 597where 598 "sequence_x xs \<equiv> foldr (\<lambda>x y. x >>= (\<lambda>_. y)) xs (return ())" 599 600text \<open> 601 Map a monadic function over a list by applying it to each element 602 of the list from left to right, ignoring return values. 603\<close> 604definition 605 mapM_x :: "('a \<Rightarrow> ('s,'b) tmonad) \<Rightarrow> 'a list \<Rightarrow> ('s, unit) tmonad" 606where 607 "mapM_x f xs \<equiv> sequence_x (map f xs)" 608 609text \<open> 610 Map a monadic function with two parameters over two lists, 611 going through both lists simultaneously, left to right, ignoring 612 return values. 613\<close> 614definition 615 zipWithM_x :: "('a \<Rightarrow> 'b \<Rightarrow> ('s,'c) tmonad) \<Rightarrow> 616 'a list \<Rightarrow> 'b list \<Rightarrow> ('s, unit) tmonad" 617where 618 "zipWithM_x f xs ys \<equiv> sequence_x (zipWith f xs ys)" 619 620 621text \<open> The same three functions as above, but returning a list of 622return values instead of @{text unit} \<close> 623definition 624 sequence :: "('s, 'a) tmonad list \<Rightarrow> ('s, 'a list) tmonad" 625where 626 "sequence xs \<equiv> let mcons = (\<lambda>p q. p >>= (\<lambda>x. q >>= (\<lambda>y. return (x#y)))) 627 in foldr mcons xs (return [])" 628 629definition 630 mapM :: "('a \<Rightarrow> ('s,'b) tmonad) \<Rightarrow> 'a list \<Rightarrow> ('s, 'b list) tmonad" 631where 632 "mapM f xs \<equiv> sequence (map f xs)" 633 634definition 635 zipWithM :: "('a \<Rightarrow> 'b \<Rightarrow> ('s,'c) tmonad) \<Rightarrow> 636 'a list \<Rightarrow> 'b list \<Rightarrow> ('s, 'c list) tmonad" 637where 638 "zipWithM f xs ys \<equiv> sequence (zipWith f xs ys)" 639 640definition 641 foldM :: "('b \<Rightarrow> 'a \<Rightarrow> ('s, 'a) tmonad) \<Rightarrow> 'b list \<Rightarrow> 'a \<Rightarrow> ('s, 'a) tmonad" 642where 643 "foldM m xs a \<equiv> foldr (\<lambda>p q. q >>= m p) xs (return a) " 644 645definition 646 foldME ::"('b \<Rightarrow> 'a \<Rightarrow> ('s,('e + 'b)) tmonad) \<Rightarrow> 'b \<Rightarrow> 'a list \<Rightarrow> ('s, ('e + 'b)) tmonad" 647where "foldME m a xs \<equiv> foldr (\<lambda>p q. q >>=E swp m p) xs (returnOk a)" 648 649text \<open> The sequence and map functions above for the exception monad, 650with and without lists of return value \<close> 651definition 652 sequenceE_x :: "('s, 'e+'a) tmonad list \<Rightarrow> ('s, 'e+unit) tmonad" 653where 654 "sequenceE_x xs \<equiv> foldr (\<lambda>x y. doE _ <- x; y odE) xs (returnOk ())" 655 656definition 657 mapME_x :: "('a \<Rightarrow> ('s,'e+'b) tmonad) \<Rightarrow> 'a list \<Rightarrow> 658 ('s,'e+unit) tmonad" 659where 660 "mapME_x f xs \<equiv> sequenceE_x (map f xs)" 661 662definition 663 sequenceE :: "('s, 'e+'a) tmonad list \<Rightarrow> ('s, 'e+'a list) tmonad" 664where 665 "sequenceE xs \<equiv> let mcons = (\<lambda>p q. p >>=E (\<lambda>x. q >>=E (\<lambda>y. returnOk (x#y)))) 666 in foldr mcons xs (returnOk [])" 667 668definition 669 mapME :: "('a \<Rightarrow> ('s,'e+'b) tmonad) \<Rightarrow> 'a list \<Rightarrow> 670 ('s,'e+'b list) tmonad" 671where 672 "mapME f xs \<equiv> sequenceE (map f xs)" 673 674 675text \<open> Filtering a list using a monadic function as predicate: \<close> 676primrec 677 filterM :: "('a \<Rightarrow> ('s, bool) tmonad) \<Rightarrow> 'a list \<Rightarrow> ('s, 'a list) tmonad" 678where 679 "filterM P [] = return []" 680| "filterM P (x # xs) = do 681 b <- P x; 682 ys <- filterM P xs; 683 return (if b then (x # ys) else ys) 684 od" 685 686text \<open> @{text select_state} takes a relationship between 687 states, and outputs nondeterministically a state 688 related to the input state. \<close> 689 690definition 691 state_select :: "('s \<times> 's) set \<Rightarrow> ('s, unit) tmonad" 692where 693 "state_select r \<equiv> (do 694 s \<leftarrow> get; 695 S \<leftarrow> return {s'. (s, s') \<in> r}; 696 assert (S \<noteq> {}); 697 s' \<leftarrow> select S; 698 put s' 699 od)" 700section "Catching and Handling Exceptions" 701 702text \<open> 703 Turning an exception monad into a normal state monad 704 by catching and handling any potential exceptions: 705\<close> 706definition 707 catch :: "('s, 'e + 'a) tmonad \<Rightarrow> 708 ('e \<Rightarrow> ('s, 'a) tmonad) \<Rightarrow> 709 ('s, 'a) tmonad" (infix "<catch>" 10) 710where 711 "f <catch> handler \<equiv> 712 do x \<leftarrow> f; 713 case x of 714 Inr b \<Rightarrow> return b 715 | Inl e \<Rightarrow> handler e 716 od" 717 718text \<open> 719 Handling exceptions, but staying in the exception monad. 720 The handler may throw a type of exceptions different from 721 the left side. 722\<close> 723definition 724 handleE' :: "('s, 'e1 + 'a) tmonad \<Rightarrow> 725 ('e1 \<Rightarrow> ('s, 'e2 + 'a) tmonad) \<Rightarrow> 726 ('s, 'e2 + 'a) tmonad" (infix "<handle2>" 10) 727where 728 "f <handle2> handler \<equiv> 729 do 730 v \<leftarrow> f; 731 case v of 732 Inl e \<Rightarrow> handler e 733 | Inr v' \<Rightarrow> return (Inr v') 734 od" 735 736text \<open> 737 A type restriction of the above that is used more commonly in 738 practice: the exception handle (potentially) throws exception 739 of the same type as the left-hand side. 740\<close> 741definition 742 handleE :: "('s, 'x + 'a) tmonad \<Rightarrow> 743 ('x \<Rightarrow> ('s, 'x + 'a) tmonad) \<Rightarrow> 744 ('s, 'x + 'a) tmonad" (infix "<handle>" 10) 745where 746 "handleE \<equiv> handleE'" 747 748 749text \<open> 750 Handling exceptions, and additionally providing a continuation 751 if the left-hand side throws no exception: 752\<close> 753definition 754 handle_elseE :: "('s, 'e + 'a) tmonad \<Rightarrow> 755 ('e \<Rightarrow> ('s, 'ee + 'b) tmonad) \<Rightarrow> 756 ('a \<Rightarrow> ('s, 'ee + 'b) tmonad) \<Rightarrow> 757 ('s, 'ee + 'b) tmonad" 758 ("_ <handle> _ <else> _" 10) 759where 760 "f <handle> handler <else> continue \<equiv> 761 do v \<leftarrow> f; 762 case v of Inl e \<Rightarrow> handler e 763 | Inr v' \<Rightarrow> continue v' 764 od" 765 766subsection "Loops" 767 768text \<open> 769 Loops are handled using the following inductive predicate; 770 non-termination is represented using the failure flag of the 771 monad. 772\<close> 773inductive_set 774 whileLoop_results :: "('r \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> ('r \<Rightarrow> ('s, 'r) tmonad) \<Rightarrow> (('r \<times> 's) \<times> ((tmid \<times> 's) list \<times> ('s, 'r) tmres)) set" 775 for C B 776where 777 "\<lbrakk> \<not> C r s \<rbrakk> \<Longrightarrow> ((r, s), ([], Result (r, s))) \<in> whileLoop_results C B" 778 | "\<lbrakk> C r s; (ts, Failed) \<in> B r s \<rbrakk> \<Longrightarrow> ((r, s), (ts, Failed)) \<in> whileLoop_results C B" 779 | "\<lbrakk> C r s; (ts, Incomplete) \<in> B r s \<rbrakk> \<Longrightarrow> ((r, s), (ts, Incomplete)) \<in> whileLoop_results C B" 780 | "\<lbrakk> C r s; (ts, Result (r', s')) \<in> B r s; ((r', s'), (ts',z)) \<in> whileLoop_results C B \<rbrakk> 781 \<Longrightarrow> ((r, s), (ts'@ts,z)) \<in> whileLoop_results C B" 782 783inductive_cases whileLoop_results_cases_result_end: "((x,y), ([],Result r)) \<in> whileLoop_results C B" 784inductive_cases whileLoop_results_cases_fail: "((x,y), (ts, Failed)) \<in> whileLoop_results C B" 785inductive_cases whileLoop_results_cases_incomplete: "((x,y), (ts, Incomplete)) \<in> whileLoop_results C B" 786 787inductive_simps whileLoop_results_simps_valid: "((x,y), ([], Result z)) \<in> whileLoop_results C B" 788 789inductive 790 whileLoop_terminates :: "('r \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> ('r \<Rightarrow> ('s, 'r) tmonad) \<Rightarrow> 'r \<Rightarrow> 's \<Rightarrow> bool" 791 for C B 792where 793 "\<not> C r s \<Longrightarrow> whileLoop_terminates C B r s" 794 | "\<lbrakk> C r s; \<forall>(r', s') \<in> Result -` snd ` (B r s). whileLoop_terminates C B r' s' \<rbrakk> 795 \<Longrightarrow> whileLoop_terminates C B r s" 796 797 798inductive_cases whileLoop_terminates_cases: "whileLoop_terminates C B r s" 799inductive_simps whileLoop_terminates_simps: "whileLoop_terminates C B r s" 800 801definition 802 whileLoop :: "('r \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> ('r \<Rightarrow> ('s, 'r) tmonad) \<Rightarrow> 'r \<Rightarrow> ('s, 'r) tmonad" 803where 804 "whileLoop C B \<equiv> (\<lambda>r s. {(ts, res). ((r,s), ts,res) \<in> whileLoop_results C B})" 805 806notation (output) 807 whileLoop ("(whileLoop (_)// (_))" [1000, 1000] 1000) 808 809definition 810 whileLoopT :: "('r \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> ('r \<Rightarrow> ('s, 'r) tmonad) \<Rightarrow> 'r \<Rightarrow> ('s, 'r) tmonad" 811where 812 "whileLoopT C B \<equiv> (\<lambda>r s. {(ts, res). ((r,s), ts,res) \<in> whileLoop_results C B 813 \<and> whileLoop_terminates C B r s})" 814 815notation (output) 816 whileLoopT ("(whileLoopT (_)// (_))" [1000, 1000] 1000) 817 818definition 819 whileLoopE :: "('r \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> ('r \<Rightarrow> ('s, 'e + 'r) tmonad) 820 \<Rightarrow> 'r \<Rightarrow> ('s, ('e + 'r)) tmonad" 821where 822 "whileLoopE C body \<equiv> 823 \<lambda>r. whileLoop (\<lambda>r s. (case r of Inr v \<Rightarrow> C v s | _ \<Rightarrow> False)) (lift body) (Inr r)" 824 825notation (output) 826 whileLoopE ("(whileLoopE (_)// (_))" [1000, 1000] 1000) 827 828subsection "Await command" 829 830text \<open> @{term "Await c f"} blocks the execution until the @{term "c"} is true, 831 and atomically executes @{term "f"}. 832\<close> 833 834definition 835 Await :: "('s \<Rightarrow> bool) \<Rightarrow> ('s,unit) tmonad" 836where 837 "Await c \<equiv> 838 do 839 s \<leftarrow> get; 840 \<comment> \<open>Add unfiltered environment events, with the last one 841 satisfying the `c' state predicate\<close> 842 xs \<leftarrow> select {xs. c (last_st_tr (map (Pair Env) xs) s)}; 843 tr \<leftarrow> return (map (Pair Env) xs); 844 put_trace tr; 845 \<comment> \<open>Pick the last event of the trace\<close> 846 put (last_st_tr tr s) 847 od" 848 849section "Hoare Logic" 850 851subsection "Validity" 852 853text \<open> This section defines a Hoare logic for partial correctness for 854 the nondeterministic state monad as well as the exception monad. 855 The logic talks only about the behaviour part of the monad and ignores 856 the failure flag. 857 858 The logic is defined semantically. Rules work directly on the 859 validity predicate. 860 861 In the nondeterministic state monad, validity is a triple of precondition, 862 monad, and postcondition. The precondition is a function from state to 863 bool (a state predicate), the postcondition is a function from return value 864 to state to bool. A triple is valid if for all states that satisfy the 865 precondition, all result values and result states that are returned by 866 the monad satisfy the postcondition. Note that if the computation returns 867 the empty set, the triple is trivially valid. This means @{term "assert P"} 868 does not require us to prove that @{term P} holds, but rather allows us 869 to assume @{term P}! Proving non-failure is done via separate predicate and 870 calculus (see below). 871\<close> 872 873 874definition 875 valid :: "('s \<Rightarrow> bool) \<Rightarrow> ('s,'a) tmonad \<Rightarrow> ('a \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> bool" 876 ("\<lbrace>_\<rbrace>/ _ /\<lbrace>_\<rbrace>") 877where 878 "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<equiv> \<forall>s. P s \<longrightarrow> (\<forall>(r,s') \<in> mres (f s). Q r s')" 879 880text \<open> 881 We often reason about invariant predicates. The following provides shorthand syntax 882 that avoids repeating potentially long predicates. 883\<close> 884abbreviation (input) 885 invariant :: "('s,'a) tmonad \<Rightarrow> ('s \<Rightarrow> bool) \<Rightarrow> bool" ("_ \<lbrace>_\<rbrace>" [59,0] 60) 886where 887 "invariant f P \<equiv> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>" 888 889text \<open>rg_pred type: Rely-Guaranty predicates (state before => state after => bool)\<close> 890type_synonym 's rg_pred = "'s \<Rightarrow> 's \<Rightarrow> bool" 891 892 893text \<open> 894 Validity for the exception monad is similar and build on the standard 895 validity above. Instead of one postcondition, we have two: one for 896 normal and one for exceptional results. 897\<close> 898definition 899 validE :: "('s \<Rightarrow> bool) \<Rightarrow> ('s, 'a + 'b) tmonad \<Rightarrow> 900 ('b \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> 901 ('a \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> bool" 902("\<lbrace>_\<rbrace>/ _ /(\<lbrace>_\<rbrace>,/ \<lbrace>_\<rbrace>)" ) 903where 904 "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace> \<equiv> \<lbrace>P\<rbrace> f \<lbrace> \<lambda>v s. case v of Inr r \<Rightarrow> Q r s | Inl e \<Rightarrow> E e s \<rbrace>" 905(* 906text \<open> Validity for exception monad with interferences. Not as easy to phrase 907 as we need to \<close> 908definition 909 validIE :: "('s, 'a + 'b) tmonad \<Rightarrow> 910 's rg_pred \<Rightarrow> 911 's rg_pred \<Rightarrow> 's rg_pred \<Rightarrow> 912 ('b \<Rightarrow> 's rg_pred) \<Rightarrow> 913 ('a \<Rightarrow> 's rg_pred) \<Rightarrow> bool" 914 ("_ //PRE _//RELY _//GUAR _//POST _//EXC _" [59,0,0,0,0,0] 60) 915where 916 "validIE f P R G Q E \<equiv> f SAT [P,R,G,\<lambda>v. case v of Inr r \<Rightarrow> Q r | Inl e \<Rightarrow> E e]" 917 918abbreviation (input) 919 validIEsat :: "('s, 'a + 'b) tmonad \<Rightarrow> 920 's rg_pred \<Rightarrow> 921 's rg_pred \<Rightarrow> 's rg_pred \<Rightarrow> 922 ('b \<Rightarrow> 's rg_pred) \<Rightarrow> 923 ('a \<Rightarrow> 's rg_pred) \<Rightarrow> bool" 924 ("_ //SAT [_, _, _, _, _]" [59,0,0,0,0,0] 60) 925 where 926 "validIEsat f P R G Q E \<equiv> validIE f P R G Q E" 927 *) 928text \<open> 929 The following two instantiations are convenient to separate reasoning 930 for exceptional and normal case. 931\<close> 932definition 933 validE_R :: "('s \<Rightarrow> bool) \<Rightarrow> ('s, 'e + 'a) tmonad \<Rightarrow> 934 ('a \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> bool" 935 ("\<lbrace>_\<rbrace>/ _ /\<lbrace>_\<rbrace>, -") 936where 937 "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,- \<equiv> validE P f Q (\<lambda>x y. True)" 938 939definition 940 validE_E :: "('s \<Rightarrow> bool) \<Rightarrow> ('s, 'e + 'a) tmonad \<Rightarrow> 941 ('e \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> bool" 942 ("\<lbrace>_\<rbrace>/ _ /-, \<lbrace>_\<rbrace>") 943where 944 "\<lbrace>P\<rbrace> f -,\<lbrace>Q\<rbrace> \<equiv> validE P f (\<lambda>x y. True) Q" 945 946 947text \<open> Abbreviations for trivial preconditions: \<close> 948abbreviation(input) 949 top :: "'a \<Rightarrow> bool" ("\<top>") 950where 951 "\<top> \<equiv> \<lambda>_. True" 952 953abbreviation(input) 954 bottom :: "'a \<Rightarrow> bool" ("\<bottom>") 955where 956 "\<bottom> \<equiv> \<lambda>_. False" 957 958text \<open> Abbreviations for trivial postconditions (taking two arguments): \<close> 959abbreviation(input) 960 toptop :: "'a \<Rightarrow> 'b \<Rightarrow> bool" ("\<top>\<top>") 961where 962 "\<top>\<top> \<equiv> \<lambda>_ _. True" 963 964abbreviation(input) 965 toptoptop :: "'a \<Rightarrow> 'b \<Rightarrow> 'b \<Rightarrow> bool" ("\<top>\<top>\<top>") 966where 967 "\<top>\<top>\<top> \<equiv> \<lambda>_ _ _. True" 968 969abbreviation(input) 970 botbot :: "'a \<Rightarrow> 'b \<Rightarrow> bool" ("\<bottom>\<bottom>") 971where 972 "\<bottom>\<bottom> \<equiv> \<lambda>_ _. False" 973 974abbreviation(input) 975 botbotbot :: "'a \<Rightarrow> 'b \<Rightarrow> 'b \<Rightarrow> bool" ("\<bottom>\<bottom>\<bottom>") 976where 977 "\<bottom>\<bottom>\<bottom> \<equiv> \<lambda>_ _ _. False" 978 979text \<open> 980 Lifting @{text "\<and>"} and @{text "\<or>"} over two arguments. 981 Lifting @{text "\<and>"} and @{text "\<or>"} over one argument is already 982 defined (written @{text "and"} and @{text "or"}). 983\<close> 984definition 985 bipred_conj :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> bool)" 986 (infixl "And" 96) 987where 988 "bipred_conj P Q \<equiv> \<lambda>x y. P x y \<and> Q x y" 989 990definition 991 bipred_disj :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> bool)" 992 (infixl "Or" 91) 993where 994 "bipred_disj P Q \<equiv> \<lambda>x y. P x y \<or> Q x y" 995 996subsection "Determinism" 997 998text \<open> A monad of type @{text tmonad} is deterministic iff it 999returns an empty trace, exactly one state and result and does not fail \<close> 1000definition 1001 det :: "('a,'s) tmonad \<Rightarrow> bool" 1002where 1003 "det f \<equiv> \<forall>s. \<exists>r. f s = {([], Result r)}" 1004 1005text \<open> A deterministic @{text tmonad} can be turned 1006 into a normal state monad: \<close> 1007definition 1008 the_run_state :: "('s,'a) tmonad \<Rightarrow> 's \<Rightarrow> 'a \<times> 's" 1009where 1010 "the_run_state M \<equiv> \<lambda>s. THE s'. mres (M s) = {s'}" 1011 1012 1013subsection "Non-Failure" 1014 1015text \<open> 1016 We can formulate non-failure separately from validity. 1017\<close> 1018definition 1019 no_fail :: "('s \<Rightarrow> bool) \<Rightarrow> ('s,'a) tmonad \<Rightarrow> bool" 1020where 1021 "no_fail P m \<equiv> \<forall>s. P s \<longrightarrow> Failed \<notin> snd ` (m s)" 1022 1023text \<open> 1024 It is often desired to prove non-failure and a Hoare triple 1025 simultaneously, as the reasoning is often similar. The following 1026 definitions allow such reasoning to take place. 1027\<close> 1028 1029definition 1030 validNF ::"('s \<Rightarrow> bool) \<Rightarrow> ('s,'a) tmonad \<Rightarrow> ('a \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> bool" 1031 ("\<lbrace>_\<rbrace>/ _ /\<lbrace>_\<rbrace>!") 1032where 1033 "validNF P f Q \<equiv> valid P f Q \<and> no_fail P f" 1034 1035definition 1036 validE_NF :: "('s \<Rightarrow> bool) \<Rightarrow> ('s, 'a + 'b) tmonad \<Rightarrow> 1037 ('b \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> 1038 ('a \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> bool" 1039 ("\<lbrace>_\<rbrace>/ _ /(\<lbrace>_\<rbrace>,/ \<lbrace>_\<rbrace>!)") 1040where 1041 "validE_NF P f Q E \<equiv> validE P f Q E \<and> no_fail P f" 1042 1043lemma validE_NF_alt_def: 1044 "\<lbrace> P \<rbrace> B \<lbrace> Q \<rbrace>,\<lbrace> E \<rbrace>! = \<lbrace> P \<rbrace> B \<lbrace> \<lambda>v s. case v of Inl e \<Rightarrow> E e s | Inr r \<Rightarrow> Q r s \<rbrace>!" 1045 by (clarsimp simp: validE_NF_def validE_def validNF_def) 1046 1047(* text \<open> 1048 Usually, well-formed monads constructed from the primitives 1049 above will have the following property: if they return an 1050 empty set of results, they will have the failure flag set. 1051\<close> 1052definition 1053 empty_fail :: "('s,'a) tmonad \<Rightarrow> bool" 1054where 1055 "empty_fail m \<equiv> \<forall>s. fst (m s) = {} \<longrightarrow> snd (m s)" 1056 1057text \<open> 1058 Useful in forcing otherwise unknown executions to have 1059 the @{const empty_fail} property. 1060\<close> 1061definition 1062 mk_ef :: "'a set \<times> bool \<Rightarrow> 'a set \<times> bool" 1063where 1064 "mk_ef S \<equiv> (fst S, fst S = {} \<or> snd S)" 1065 *) 1066section "Basic exception reasoning" 1067 1068text \<open> 1069 The following predicates @{text no_throw} and @{text no_return} allow 1070 reasoning that functions in the exception monad either do 1071 no throw an exception or never return normally. 1072\<close> 1073 1074definition "no_throw P A \<equiv> \<lbrace> P \<rbrace> A \<lbrace> \<lambda>_ _. True \<rbrace>,\<lbrace> \<lambda>_ _. False \<rbrace>" 1075 1076definition "no_return P A \<equiv> \<lbrace> P \<rbrace> A \<lbrace>\<lambda>_ _. False\<rbrace>,\<lbrace>\<lambda>_ _. True \<rbrace>" 1077 1078section "Trace monad Parallel" 1079 1080definition 1081 parallel :: "('s,'a) tmonad \<Rightarrow> ('s,'a) tmonad \<Rightarrow> ('s,'a) tmonad" 1082where 1083 "parallel f g = (\<lambda>s. {(xs, rv). \<exists>f_steps. length f_steps = length xs 1084 \<and> (map (\<lambda>(f_step, (id, s)). (if f_step then id else Env, s)) (zip f_steps xs), rv) \<in> f s 1085 \<and> (map (\<lambda>(f_step, (id, s)). (if f_step then Env else id, s)) (zip f_steps xs), rv) \<in> g s})" 1086 1087abbreviation(input) 1088 "parallel_mrg \<equiv> ((\<lambda>((idn, s), (idn', _)). (if idn = Env then idn' else idn, s)))" 1089 1090lemma parallel_def2: 1091 "parallel f g = (\<lambda>s. {(xs, rv). \<exists>ys zs. (ys, rv) \<in> f s \<and> (zs, rv) \<in> g s 1092 \<and> list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) ys zs 1093 \<and> xs = map parallel_mrg (zip ys zs)})" 1094 apply (simp add: parallel_def fun_eq_iff set_eq_iff) 1095 apply safe 1096 apply (rule exI, rule conjI, assumption)+ 1097 apply (simp add: list_all2_conv_all_nth list_eq_iff_nth_eq split_def prod_eq_iff) 1098 apply clarsimp 1099 apply (rule_tac x="map (((\<noteq>) Env) o fst) ys" in exI) 1100 apply (simp add: zip_map1 o_def split_def) 1101 apply (strengthen subst[where P="\<lambda>xs. (xs, v) \<in> S" for v S, mk_strg I _ E]) 1102 apply (clarsimp simp: list_all2_conv_all_nth list_eq_iff_nth_eq 1103 split_def prod_eq_iff 1104 split del: if_split cong: if_cong) 1105 apply auto 1106 done 1107 1108lemma parallel_def3: 1109 "parallel f g = (\<lambda>s. (\<lambda>(ys, zs, rv). (map parallel_mrg (zip ys zs), rv)) 1110 ` {(ys, zs, rv). (ys, rv) \<in> f s \<and> (zs, rv) \<in> g s 1111 \<and> list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) ys zs})" 1112 by (simp add: parallel_def2, rule ext, auto simp: image_def) 1113 1114primrec 1115 trace_steps :: "(tmid \<times> 's) list \<Rightarrow> 's \<Rightarrow> (tmid \<times> 's \<times> 's) set" 1116where 1117 "trace_steps (elem # trace) s0 = {(fst elem, s0, snd elem)} \<union> trace_steps trace (snd elem)" 1118| "trace_steps [] s0 = {}" 1119 1120lemma trace_steps_nth: 1121 "trace_steps xs s0 = (\<lambda>i. (fst (xs ! i), (if i = 0 then s0 else snd (xs ! (i - 1))), snd (xs ! i))) ` {..< length xs}" 1122proof (induct xs arbitrary: s0) 1123 case Nil 1124 show ?case by simp 1125next 1126 case (Cons a xs) 1127 show ?case 1128 apply (simp add: lessThan_Suc_eq_insert_0 Cons image_image nth_Cons') 1129 apply (intro arg_cong2[where f=insert] refl image_cong) 1130 apply simp 1131 done 1132qed 1133 1134definition 1135 rely_cond :: "'s rg_pred \<Rightarrow> 's \<Rightarrow> (tmid \<times> 's) list \<Rightarrow> bool" 1136where 1137 "rely_cond R s0s tr = (\<forall>(ident, s0, s) \<in> trace_steps (rev tr) s0s. ident = Env \<longrightarrow> R s0 s)" 1138 1139definition 1140 guar_cond :: "'s rg_pred \<Rightarrow> 's \<Rightarrow> (tmid \<times> 's) list \<Rightarrow> bool" 1141where 1142 "guar_cond G s0s tr = (\<forall>(ident, s0, s) \<in> trace_steps (rev tr) s0s. ident = Me \<longrightarrow> G s0 s)" 1143 1144lemma rg_empty_conds[simp]: 1145 "rely_cond R s0s []" 1146 "guar_cond G s0s []" 1147 by (simp_all add: rely_cond_def guar_cond_def) 1148 1149definition 1150 rely :: "('s, 'a) tmonad \<Rightarrow> 's rg_pred \<Rightarrow> 's \<Rightarrow> ('s, 'a) tmonad" 1151where 1152 "rely f R s0s \<equiv> (\<lambda>s. f s \<inter> ({tr. rely_cond R s0s tr} \<times> UNIV))" 1153 1154definition 1155 prefix_closed :: "('s, 'a) tmonad \<Rightarrow> bool" 1156where 1157 "prefix_closed f = (\<forall>s. \<forall>x xs. (x # xs) \<in> fst ` f s \<longrightarrow> (xs, Incomplete) \<in> f s)" 1158 1159definition 1160 validI :: "('s \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> 's rg_pred \<Rightarrow> ('s,'a) tmonad 1161 \<Rightarrow> 's rg_pred \<Rightarrow> ('a \<Rightarrow> 's \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> bool" 1162 ("(\<lbrace>_\<rbrace>,/ \<lbrace>_\<rbrace>)/ _ /(\<lbrace>_\<rbrace>,/ \<lbrace>_\<rbrace>)") 1163where 1164 "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace> \<equiv> prefix_closed f \<and> (\<forall>s0 s. P s0 s 1165 \<longrightarrow> (\<forall>tr res. (tr, res) \<in> (rely f R s0 s) \<longrightarrow> guar_cond G s0 tr 1166 \<and> (\<forall>rv s'. res = Result (rv, s') \<longrightarrow> Q rv (last_st_tr tr s0) s')))" 1167 1168lemma in_rely: 1169 "\<lbrakk> (tr, res) \<in> f s; rely_cond R s0s tr \<rbrakk> \<Longrightarrow> (tr, res) \<in> rely f R s0s s" 1170 by (simp add: rely_def) 1171 1172lemmas validI_D = validI_def[THEN meta_eq_to_obj_eq, THEN iffD1, 1173 THEN conjunct2, rule_format, OF _ _ in_rely] 1174lemmas validI_GD = validI_D[THEN conjunct1] 1175lemmas validI_rvD = validI_D[THEN conjunct2, rule_format, rotated -1, OF refl] 1176lemmas validI_prefix_closed = validI_def[THEN meta_eq_to_obj_eq, THEN iffD1, THEN conjunct1] 1177lemmas validI_prefix_closed_T = validI_prefix_closed[where P="\<lambda>_ _. False" and R="\<lambda>_ _. False" 1178 and G="\<lambda>_ _. True" and Q="\<lambda>_ _ _. True"] 1179 1180lemmas prefix_closedD1 = prefix_closed_def[THEN iffD1, rule_format] 1181 1182lemma in_fst_snd_image_eq: 1183 "x \<in> fst ` S = (\<exists>y. (x, y) \<in> S)" 1184 "y \<in> snd ` S = (\<exists>x. (x, y) \<in> S)" 1185 by (auto elim: image_eqI[rotated]) 1186 1187lemma in_fst_snd_image: 1188 "(x, y) \<in> S \<Longrightarrow> x \<in> fst ` S" 1189 "(x, y) \<in> S \<Longrightarrow> y \<in> snd ` S" 1190 by (auto simp: in_fst_snd_image_eq) 1191 1192lemmas prefix_closedD = prefix_closedD1[OF _ in_fst_snd_image(1)] 1193 1194end 1195