1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7(* 8 Nondeterministic state and error monads with failure in Isabelle. 9*) 10 11chapter "Nondeterministic State Monad with Failure" 12 13theory NonDetMonad 14imports Lib 15begin 16 17text \<open> 18 \label{c:monads} 19 20 State monads are used extensively in the seL4 specification. They are 21 defined below. 22\<close> 23 24section "The Monad" 25 26text \<open> 27 The basic type of the nondeterministic state monad with failure is 28 very similar to the normal state monad. Instead of a pair consisting 29 of result and new state, we return a set of these pairs coupled with 30 a failure flag. Each element in the set is a potential result of the 31 computation. The flag is @{const True} if there is an execution path 32 in the computation that may have failed. Conversely, if the flag is 33 @{const False}, none of the computations resulting in the returned 34 set can have failed.\<close> 35type_synonym ('s,'a) nondet_monad = "'s \<Rightarrow> ('a \<times> 's) set \<times> bool" 36 37 38text \<open> 39 Print the type @{typ "('s,'a) nondet_monad"} instead of its unwieldy expansion. 40 Needs an AST translation in code, because it needs to check that the state variable 41 @{typ 's} occurs twice. This comparison is not guaranteed to always work as expected 42 (AST instances might have different decoration), but it does seem to work here. 43\<close> 44print_ast_translation \<open> 45 let 46 fun monad_tr _ [t1, Ast.Appl [Ast.Constant @{type_syntax prod}, 47 Ast.Appl [Ast.Constant @{type_syntax set}, 48 Ast.Appl [Ast.Constant @{type_syntax prod}, t2, t3]], 49 Ast.Constant @{type_syntax bool}]] = 50 if t3 = t1 51 then Ast.Appl [Ast.Constant @{type_syntax "nondet_monad"}, t1, t2] 52 else raise Match 53 in [(@{type_syntax "fun"}, monad_tr)] end 54\<close> 55 56 57text \<open> 58 The definition of fundamental monad functions @{text return} and 59 @{text bind}. The monad function @{text "return x"} does not change 60 the state, does not fail, and returns @{text "x"}. 61\<close> 62definition 63 return :: "'a \<Rightarrow> ('s,'a) nondet_monad" where 64 "return a \<equiv> \<lambda>s. ({(a,s)},False)" 65 66text \<open> 67 The monad function @{text "bind f g"}, also written @{text "f >>= g"}, 68 is the execution of @{term f} followed by the execution of @{text g}. 69 The function @{text g} takes the result value \emph{and} the result 70 state of @{text f} as parameter. The definition says that the result of 71 the combined operation is the union of the set of sets that is created 72 by @{text g} applied to the result sets of @{text f}. The combined 73 operation may have failed, if @{text f} may have failed or @{text g} may 74 have failed on any of the results of @{text f}. 75\<close> 76definition 77 bind :: "('s, 'a) nondet_monad \<Rightarrow> ('a \<Rightarrow> ('s, 'b) nondet_monad) \<Rightarrow> 78 ('s, 'b) nondet_monad" (infixl ">>=" 60) 79 where 80 "bind f g \<equiv> \<lambda>s. (\<Union>(fst ` case_prod g ` fst (f s)), 81 True \<in> snd ` case_prod g ` fst (f s) \<or> snd (f s))" 82 83text \<open> 84 Sometimes it is convenient to write @{text bind} in reverse order. 85\<close> 86abbreviation(input) 87 bind_rev :: "('c \<Rightarrow> ('a, 'b) nondet_monad) \<Rightarrow> ('a, 'c) nondet_monad \<Rightarrow> 88 ('a, 'b) nondet_monad" (infixl "=<<" 60) where 89 "g =<< f \<equiv> f >>= g" 90 91text \<open> 92 The basic accessor functions of the state monad. @{text get} returns 93 the current state as result, does not fail, and does not change the state. 94 @{text "put s"} returns nothing (@{typ unit}), changes the current state 95 to @{text s} and does not fail. 96\<close> 97definition 98 get :: "('s,'s) nondet_monad" where 99 "get \<equiv> \<lambda>s. ({(s,s)}, False)" 100 101definition 102 put :: "'s \<Rightarrow> ('s, unit) nondet_monad" where 103 "put s \<equiv> \<lambda>_. ({((),s)}, False)" 104 105 106subsection "Nondeterminism" 107 108text \<open> 109 Basic nondeterministic functions. @{text "select A"} chooses an element 110 of the set @{text A}, does not change the state, and does not fail 111 (even if the set is empty). @{text "f OR g"} executes @{text f} or 112 executes @{text g}. It retuns the union of results of @{text f} and 113 @{text g}, and may have failed if either may have failed. 114\<close> 115definition 116 select :: "'a set \<Rightarrow> ('s,'a) nondet_monad" where 117 "select A \<equiv> \<lambda>s. (A \<times> {s}, False)" 118 119definition 120 alternative :: "('s,'a) nondet_monad \<Rightarrow> ('s,'a) nondet_monad \<Rightarrow> 121 ('s,'a) nondet_monad" 122 (infixl "OR" 20) 123where 124 "f OR g \<equiv> \<lambda>s. (fst (f s) \<union> fst (g s), snd (f s) \<or> snd (g s))" 125 126text \<open>Alternative notation for @{text OR}\<close> 127notation (xsymbols) alternative (infixl "\<sqinter>" 20) 128 129 130text \<open>A variant of @{text select} that takes a pair. The first component 131 is a set as in normal @{text select}, the second component indicates 132 whether the execution failed. This is useful to lift monads between 133 different state spaces. 134\<close> 135definition 136 select_f :: "'a set \<times> bool \<Rightarrow> ('s,'a) nondet_monad" where 137 "select_f S \<equiv> \<lambda>s. (fst S \<times> {s}, snd S)" 138 139text \<open>@{text select_state} takes a relationship between 140 states, and outputs nondeterministically a state 141 related to the input state.\<close> 142 143definition 144 state_select :: "('s \<times> 's) set \<Rightarrow> ('s, unit) nondet_monad" 145where 146 "state_select r \<equiv> \<lambda>s. ((\<lambda>x. ((), x)) ` {s'. (s, s') \<in> r}, \<not> (\<exists>s'. (s, s') \<in> r))" 147 148subsection "Failure" 149 150text \<open>The monad function that always fails. Returns an empty set of 151results and sets the failure flag.\<close> 152definition 153 fail :: "('s, 'a) nondet_monad" where 154 "fail \<equiv> \<lambda>s. ({}, True)" 155 156text \<open>Assertions: fail if the property @{text P} is not true\<close> 157definition 158 assert :: "bool \<Rightarrow> ('a, unit) nondet_monad" where 159 "assert P \<equiv> if P then return () else fail" 160 161text \<open>Fail if the value is @{const None}, 162 return result @{text v} for @{term "Some v"}\<close> 163definition 164 assert_opt :: "'a option \<Rightarrow> ('b, 'a) nondet_monad" where 165 "assert_opt v \<equiv> case v of None \<Rightarrow> fail | Some v \<Rightarrow> return v" 166 167text \<open>An assertion that also can introspect the current state.\<close> 168 169definition 170 state_assert :: "('s \<Rightarrow> bool) \<Rightarrow> ('s, unit) nondet_monad" 171where 172 "state_assert P \<equiv> get >>= (\<lambda>s. assert (P s))" 173 174subsection "Generic functions on top of the state monad" 175 176text \<open>Apply a function to the current state and return the result 177without changing the state.\<close> 178definition 179 gets :: "('s \<Rightarrow> 'a) \<Rightarrow> ('s, 'a) nondet_monad" where 180 "gets f \<equiv> get >>= (\<lambda>s. return (f s))" 181 182text \<open>Modify the current state using the function passed in.\<close> 183definition 184 modify :: "('s \<Rightarrow> 's) \<Rightarrow> ('s, unit) nondet_monad" where 185 "modify f \<equiv> get >>= (\<lambda>s. put (f s))" 186 187lemma simpler_gets_def: "gets f = (\<lambda>s. ({(f s, s)}, False))" 188 apply (simp add: gets_def return_def bind_def get_def) 189 done 190 191lemma simpler_modify_def: 192 "modify f = (\<lambda>s. ({((), f s)}, False))" 193 by (simp add: modify_def bind_def get_def put_def) 194 195text \<open>Execute the given monad when the condition is true, 196 return @{text "()"} otherwise.\<close> 197definition 198 "when" :: "bool \<Rightarrow> ('s, unit) nondet_monad \<Rightarrow> 199 ('s, unit) nondet_monad" where 200 "when P m \<equiv> if P then m else return ()" 201 202text \<open>Execute the given monad unless the condition is true, 203 return @{text "()"} otherwise.\<close> 204definition 205 unless :: "bool \<Rightarrow> ('s, unit) nondet_monad \<Rightarrow> 206 ('s, unit) nondet_monad" where 207 "unless P m \<equiv> when (\<not>P) m" 208 209text \<open> 210 Perform a test on the current state, performing the left monad if 211 the result is true or the right monad if the result is false. 212\<close> 213definition 214 condition :: "('s \<Rightarrow> bool) \<Rightarrow> ('s, 'r) nondet_monad \<Rightarrow> ('s, 'r) nondet_monad \<Rightarrow> ('s, 'r) nondet_monad" 215where 216 "condition P L R \<equiv> \<lambda>s. if (P s) then (L s) else (R s)" 217 218notation (output) 219 condition ("(condition (_)// (_)// (_))" [1000,1000,1000] 1000) 220 221text \<open> 222Apply an option valued function to the current state, fail 223if it returns @{const None}, return @{text v} if it returns 224@{term "Some v"}. 225\<close> 226definition 227 gets_the :: "('s \<Rightarrow> 'a option) \<Rightarrow> ('s, 'a) nondet_monad" where 228 "gets_the f \<equiv> gets f >>= assert_opt" 229 230 231text \<open> 232 Get a map (such as a heap) from the current state and apply an argument to the map. 233 Fail if the map returns @{const None}, otherwise return the value. 234\<close> 235definition 236 gets_map :: "('s \<Rightarrow> 'a \<Rightarrow> 'b option) \<Rightarrow> 'a \<Rightarrow> ('s, 'b) nondet_monad" where 237 "gets_map f p \<equiv> gets f >>= (\<lambda>m. assert_opt (m p))" 238 239 240subsection \<open>The Monad Laws\<close> 241 242text \<open>A more expanded definition of @{text bind}\<close> 243lemma bind_def': 244 "(f >>= g) \<equiv> 245 \<lambda>s. ({(r'', s''). \<exists>(r', s') \<in> fst (f s). (r'', s'') \<in> fst (g r' s') }, 246 snd (f s) \<or> (\<exists>(r', s') \<in> fst (f s). snd (g r' s')))" 247 apply (rule eq_reflection) 248 apply (auto simp add: bind_def split_def Let_def) 249 done 250 251text \<open>Each monad satisfies at least the following three laws.\<close> 252 253text \<open>@{term return} is absorbed at the left of a @{term bind}, 254 applying the return value directly:\<close> 255lemma return_bind [simp]: "(return x >>= f) = f x" 256 by (simp add: return_def bind_def) 257 258text \<open>@{term return} is absorbed on the right of a @{term bind}\<close> 259lemma bind_return [simp]: "(m >>= return) = m" 260 apply (rule ext) 261 apply (simp add: bind_def return_def split_def) 262 done 263 264text \<open>@{term bind} is associative\<close> 265lemma bind_assoc: 266 fixes m :: "('a,'b) nondet_monad" 267 fixes f :: "'b \<Rightarrow> ('a,'c) nondet_monad" 268 fixes g :: "'c \<Rightarrow> ('a,'d) nondet_monad" 269 shows "(m >>= f) >>= g = m >>= (\<lambda>x. f x >>= g)" 270 apply (unfold bind_def Let_def split_def) 271 apply (rule ext) 272 apply clarsimp 273 apply (auto intro: rev_image_eqI) 274 done 275 276 277section \<open>Adding Exceptions\<close> 278 279text \<open> 280 The type @{typ "('s,'a) nondet_monad"} gives us nondeterminism and 281 failure. We now extend this monad with exceptional return values 282 that abort normal execution, but can be handled explicitly. 283 We use the sum type to indicate exceptions. 284 285 In @{typ "('s, 'e + 'a) nondet_monad"}, @{typ "'s"} is the state, 286 @{typ 'e} is an exception, and @{typ 'a} is a normal return value. 287 288 This new type itself forms a monad again. Since type classes in 289 Isabelle are not powerful enough to express the class of monads, 290 we provide new names for the @{term return} and @{term bind} functions 291 in this monad. We call them @{text returnOk} (for normal return values) 292 and @{text bindE} (for composition). We also define @{text throwError} 293 to return an exceptional value. 294\<close> 295definition 296 returnOk :: "'a \<Rightarrow> ('s, 'e + 'a) nondet_monad" where 297 "returnOk \<equiv> return o Inr" 298 299definition 300 throwError :: "'e \<Rightarrow> ('s, 'e + 'a) nondet_monad" where 301 "throwError \<equiv> return o Inl" 302 303text \<open> 304 Lifting a function over the exception type: if the input is an 305 exception, return that exception; otherwise continue execution. 306\<close> 307definition 308 lift :: "('a \<Rightarrow> ('s, 'e + 'b) nondet_monad) \<Rightarrow> 309 'e +'a \<Rightarrow> ('s, 'e + 'b) nondet_monad" 310where 311 "lift f v \<equiv> case v of Inl e \<Rightarrow> throwError e 312 | Inr v' \<Rightarrow> f v'" 313 314text \<open> 315 The definition of @{term bind} in the exception monad (new 316 name @{text bindE}): the same as normal @{term bind}, but 317 the right-hand side is skipped if the left-hand side 318 produced an exception. 319\<close> 320definition 321 bindE :: "('s, 'e + 'a) nondet_monad \<Rightarrow> 322 ('a \<Rightarrow> ('s, 'e + 'b) nondet_monad) \<Rightarrow> 323 ('s, 'e + 'b) nondet_monad" (infixl ">>=E" 60) 324where 325 "bindE f g \<equiv> bind f (lift g)" 326 327 328text \<open> 329 Lifting a normal nondeterministic monad into the 330 exception monad is achieved by always returning its 331 result as normal result and never throwing an exception. 332\<close> 333definition 334 liftE :: "('s,'a) nondet_monad \<Rightarrow> ('s, 'e+'a) nondet_monad" 335where 336 "liftE f \<equiv> f >>= (\<lambda>r. return (Inr r))" 337 338 339text \<open> 340 Since the underlying type and @{text return} function changed, 341 we need new definitions for when and unless: 342\<close> 343definition 344 whenE :: "bool \<Rightarrow> ('s, 'e + unit) nondet_monad \<Rightarrow> 345 ('s, 'e + unit) nondet_monad" 346 where 347 "whenE P f \<equiv> if P then f else returnOk ()" 348 349definition 350 unlessE :: "bool \<Rightarrow> ('s, 'e + unit) nondet_monad \<Rightarrow> 351 ('s, 'e + unit) nondet_monad" 352 where 353 "unlessE P f \<equiv> if P then returnOk () else f" 354 355 356text \<open> 357 Throwing an exception when the parameter is @{term None}, otherwise 358 returning @{term "v"} for @{term "Some v"}. 359\<close> 360definition 361 throw_opt :: "'e \<Rightarrow> 'a option \<Rightarrow> ('s, 'e + 'a) nondet_monad" where 362 "throw_opt ex x \<equiv> 363 case x of None \<Rightarrow> throwError ex | Some v \<Rightarrow> returnOk v" 364 365 366text \<open> 367 Failure in the exception monad is redefined in the same way 368 as @{const whenE} and @{const unlessE}, with @{term returnOk} 369 instead of @{term return}. 370\<close> 371definition 372 assertE :: "bool \<Rightarrow> ('a, 'e + unit) nondet_monad" where 373 "assertE P \<equiv> if P then returnOk () else fail" 374 375subsection "Monad Laws for the Exception Monad" 376 377text \<open>More direct definition of @{const liftE}:\<close> 378lemma liftE_def2: 379 "liftE f = (\<lambda>s. ((\<lambda>(v,s'). (Inr v, s')) ` fst (f s), snd (f s)))" 380 by (auto simp: liftE_def return_def split_def bind_def) 381 382text \<open>Left @{const returnOk} absorbtion over @{term bindE}:\<close> 383lemma returnOk_bindE [simp]: "(returnOk x >>=E f) = f x" 384 apply (unfold bindE_def returnOk_def) 385 apply (clarsimp simp: lift_def) 386 done 387 388lemma lift_return [simp]: 389 "lift (return \<circ> Inr) = return" 390 by (rule ext) 391 (simp add: lift_def throwError_def split: sum.splits) 392 393text \<open>Right @{const returnOk} absorbtion over @{term bindE}:\<close> 394lemma bindE_returnOk [simp]: "(m >>=E returnOk) = m" 395 by (simp add: bindE_def returnOk_def) 396 397text \<open>Associativity of @{const bindE}:\<close> 398lemma bindE_assoc: 399 "(m >>=E f) >>=E g = m >>=E (\<lambda>x. f x >>=E g)" 400 apply (simp add: bindE_def bind_assoc) 401 apply (rule arg_cong [where f="\<lambda>x. m >>= x"]) 402 apply (rule ext) 403 apply (case_tac x, simp_all add: lift_def throwError_def) 404 done 405 406text \<open>@{const returnOk} could also be defined via @{const liftE}:\<close> 407lemma returnOk_liftE: 408 "returnOk x = liftE (return x)" 409 by (simp add: liftE_def returnOk_def) 410 411text \<open>Execution after throwing an exception is skipped:\<close> 412lemma throwError_bindE [simp]: 413 "(throwError E >>=E f) = throwError E" 414 by (simp add: bindE_def bind_def throwError_def lift_def return_def) 415 416 417section "Syntax" 418 419text \<open>This section defines traditional Haskell-like do-syntax 420 for the state monad in Isabelle.\<close> 421 422subsection "Syntax for the Nondeterministic State Monad" 423 424text \<open>We use @{text K_bind} to syntactically indicate the 425 case where the return argument of the left side of a @{term bind} 426 is ignored\<close> 427definition 428 K_bind_def [iff]: "K_bind \<equiv> \<lambda>x y. x" 429 430nonterminal 431 dobinds and dobind and nobind 432 433syntax 434 "_dobind" :: "[pttrn, 'a] => dobind" ("(_ <-/ _)" 10) 435 "" :: "dobind => dobinds" ("_") 436 "_nobind" :: "'a => dobind" ("_") 437 "_dobinds" :: "[dobind, dobinds] => dobinds" ("(_);//(_)") 438 439 "_do" :: "[dobinds, 'a] => 'a" ("(do ((_);//(_))//od)" 100) 440syntax (xsymbols) 441 "_dobind" :: "[pttrn, 'a] => dobind" ("(_ \<leftarrow>/ _)" 10) 442 443translations 444 "_do (_dobinds b bs) e" == "_do b (_do bs e)" 445 "_do (_nobind b) e" == "b >>= (CONST K_bind e)" 446 "do x <- a; e od" == "a >>= (\<lambda>x. e)" 447 448text \<open>Syntax examples:\<close> 449lemma "do x \<leftarrow> return 1; 450 return (2::nat); 451 return x 452 od = 453 return 1 >>= 454 (\<lambda>x. return (2::nat) >>= 455 K_bind (return x))" 456 by (rule refl) 457 458lemma "do x \<leftarrow> return 1; 459 return 2; 460 return x 461 od = return 1" 462 by simp 463 464subsection "Syntax for the Exception Monad" 465 466text \<open> 467 Since the exception monad is a different type, we 468 need to syntactically distinguish it in the syntax. 469 We use @{text doE}/@{text odE} for this, but can re-use 470 most of the productions from @{text do}/@{text od} 471 above. 472\<close> 473 474syntax 475 "_doE" :: "[dobinds, 'a] => 'a" ("(doE ((_);//(_))//odE)" 100) 476 477translations 478 "_doE (_dobinds b bs) e" == "_doE b (_doE bs e)" 479 "_doE (_nobind b) e" == "b >>=E (CONST K_bind e)" 480 "doE x <- a; e odE" == "a >>=E (\<lambda>x. e)" 481 482text \<open>Syntax examples:\<close> 483lemma "doE x \<leftarrow> returnOk 1; 484 returnOk (2::nat); 485 returnOk x 486 odE = 487 returnOk 1 >>=E 488 (\<lambda>x. returnOk (2::nat) >>=E 489 K_bind (returnOk x))" 490 by (rule refl) 491 492lemma "doE x \<leftarrow> returnOk 1; 493 returnOk 2; 494 returnOk x 495 odE = returnOk 1" 496 by simp 497 498 499 500section "Library of Monadic Functions and Combinators" 501 502 503text \<open>Lifting a normal function into the monad type:\<close> 504definition 505 liftM :: "('a \<Rightarrow> 'b) \<Rightarrow> ('s,'a) nondet_monad \<Rightarrow> ('s, 'b) nondet_monad" 506where 507 "liftM f m \<equiv> do x \<leftarrow> m; return (f x) od" 508 509text \<open>The same for the exception monad:\<close> 510definition 511 liftME :: "('a \<Rightarrow> 'b) \<Rightarrow> ('s,'e+'a) nondet_monad \<Rightarrow> ('s,'e+'b) nondet_monad" 512where 513 "liftME f m \<equiv> doE x \<leftarrow> m; returnOk (f x) odE" 514 515text \<open> 516 Run a sequence of monads from left to right, ignoring return values.\<close> 517definition 518 sequence_x :: "('s, 'a) nondet_monad list \<Rightarrow> ('s, unit) nondet_monad" 519where 520 "sequence_x xs \<equiv> foldr (\<lambda>x y. x >>= (\<lambda>_. y)) xs (return ())" 521 522text \<open> 523 Map a monadic function over a list by applying it to each element 524 of the list from left to right, ignoring return values. 525\<close> 526definition 527 mapM_x :: "('a \<Rightarrow> ('s,'b) nondet_monad) \<Rightarrow> 'a list \<Rightarrow> ('s, unit) nondet_monad" 528where 529 "mapM_x f xs \<equiv> sequence_x (map f xs)" 530 531text \<open> 532 Map a monadic function with two parameters over two lists, 533 going through both lists simultaneously, left to right, ignoring 534 return values. 535\<close> 536definition 537 zipWithM_x :: "('a \<Rightarrow> 'b \<Rightarrow> ('s,'c) nondet_monad) \<Rightarrow> 538 'a list \<Rightarrow> 'b list \<Rightarrow> ('s, unit) nondet_monad" 539where 540 "zipWithM_x f xs ys \<equiv> sequence_x (zipWith f xs ys)" 541 542 543text \<open>The same three functions as above, but returning a list of 544return values instead of @{text unit}\<close> 545definition 546 sequence :: "('s, 'a) nondet_monad list \<Rightarrow> ('s, 'a list) nondet_monad" 547where 548 "sequence xs \<equiv> let mcons = (\<lambda>p q. p >>= (\<lambda>x. q >>= (\<lambda>y. return (x#y)))) 549 in foldr mcons xs (return [])" 550 551definition 552 mapM :: "('a \<Rightarrow> ('s,'b) nondet_monad) \<Rightarrow> 'a list \<Rightarrow> ('s, 'b list) nondet_monad" 553where 554 "mapM f xs \<equiv> sequence (map f xs)" 555 556definition 557 zipWithM :: "('a \<Rightarrow> 'b \<Rightarrow> ('s,'c) nondet_monad) \<Rightarrow> 558 'a list \<Rightarrow> 'b list \<Rightarrow> ('s, 'c list) nondet_monad" 559where 560 "zipWithM f xs ys \<equiv> sequence (zipWith f xs ys)" 561 562definition 563 foldM :: "('b \<Rightarrow> 'a \<Rightarrow> ('s, 'a) nondet_monad) \<Rightarrow> 'b list \<Rightarrow> 'a \<Rightarrow> ('s, 'a) nondet_monad" 564where 565 "foldM m xs a \<equiv> foldr (\<lambda>p q. q >>= m p) xs (return a) " 566 567definition 568 foldME ::"('b \<Rightarrow> 'a \<Rightarrow> ('s,('e + 'b)) nondet_monad) \<Rightarrow> 'b \<Rightarrow> 'a list \<Rightarrow> ('s, ('e + 'b)) nondet_monad" 569where "foldME m a xs \<equiv> foldr (\<lambda>p q. q >>=E swp m p) xs (returnOk a)" 570 571text \<open>The sequence and map functions above for the exception monad, 572with and without lists of return value\<close> 573definition 574 sequenceE_x :: "('s, 'e+'a) nondet_monad list \<Rightarrow> ('s, 'e+unit) nondet_monad" 575where 576 "sequenceE_x xs \<equiv> foldr (\<lambda>x y. doE _ <- x; y odE) xs (returnOk ())" 577 578definition 579 mapME_x :: "('a \<Rightarrow> ('s,'e+'b) nondet_monad) \<Rightarrow> 'a list \<Rightarrow> 580 ('s,'e+unit) nondet_monad" 581where 582 "mapME_x f xs \<equiv> sequenceE_x (map f xs)" 583 584definition 585 sequenceE :: "('s, 'e+'a) nondet_monad list \<Rightarrow> ('s, 'e+'a list) nondet_monad" 586where 587 "sequenceE xs \<equiv> let mcons = (\<lambda>p q. p >>=E (\<lambda>x. q >>=E (\<lambda>y. returnOk (x#y)))) 588 in foldr mcons xs (returnOk [])" 589 590definition 591 mapME :: "('a \<Rightarrow> ('s,'e+'b) nondet_monad) \<Rightarrow> 'a list \<Rightarrow> 592 ('s,'e+'b list) nondet_monad" 593where 594 "mapME f xs \<equiv> sequenceE (map f xs)" 595 596 597text \<open>Filtering a list using a monadic function as predicate:\<close> 598primrec 599 filterM :: "('a \<Rightarrow> ('s, bool) nondet_monad) \<Rightarrow> 'a list \<Rightarrow> ('s, 'a list) nondet_monad" 600where 601 "filterM P [] = return []" 602| "filterM P (x # xs) = do 603 b <- P x; 604 ys <- filterM P xs; 605 return (if b then (x # ys) else ys) 606 od" 607 608 609section "Catching and Handling Exceptions" 610 611text \<open> 612 Turning an exception monad into a normal state monad 613 by catching and handling any potential exceptions: 614\<close> 615definition 616 catch :: "('s, 'e + 'a) nondet_monad \<Rightarrow> 617 ('e \<Rightarrow> ('s, 'a) nondet_monad) \<Rightarrow> 618 ('s, 'a) nondet_monad" (infix "<catch>" 10) 619where 620 "f <catch> handler \<equiv> 621 do x \<leftarrow> f; 622 case x of 623 Inr b \<Rightarrow> return b 624 | Inl e \<Rightarrow> handler e 625 od" 626 627text \<open> 628 Handling exceptions, but staying in the exception monad. 629 The handler may throw a type of exceptions different from 630 the left side. 631\<close> 632definition 633 handleE' :: "('s, 'e1 + 'a) nondet_monad \<Rightarrow> 634 ('e1 \<Rightarrow> ('s, 'e2 + 'a) nondet_monad) \<Rightarrow> 635 ('s, 'e2 + 'a) nondet_monad" (infix "<handle2>" 10) 636where 637 "f <handle2> handler \<equiv> 638 do 639 v \<leftarrow> f; 640 case v of 641 Inl e \<Rightarrow> handler e 642 | Inr v' \<Rightarrow> return (Inr v') 643 od" 644 645text \<open> 646 A type restriction of the above that is used more commonly in 647 practice: the exception handle (potentially) throws exception 648 of the same type as the left-hand side. 649\<close> 650definition 651 handleE :: "('s, 'x + 'a) nondet_monad \<Rightarrow> 652 ('x \<Rightarrow> ('s, 'x + 'a) nondet_monad) \<Rightarrow> 653 ('s, 'x + 'a) nondet_monad" (infix "<handle>" 10) 654where 655 "handleE \<equiv> handleE'" 656 657 658text \<open> 659 Handling exceptions, and additionally providing a continuation 660 if the left-hand side throws no exception: 661\<close> 662definition 663 handle_elseE :: "('s, 'e + 'a) nondet_monad \<Rightarrow> 664 ('e \<Rightarrow> ('s, 'ee + 'b) nondet_monad) \<Rightarrow> 665 ('a \<Rightarrow> ('s, 'ee + 'b) nondet_monad) \<Rightarrow> 666 ('s, 'ee + 'b) nondet_monad" 667 ("_ <handle> _ <else> _" 10) 668where 669 "f <handle> handler <else> continue \<equiv> 670 do v \<leftarrow> f; 671 case v of Inl e \<Rightarrow> handler e 672 | Inr v' \<Rightarrow> continue v' 673 od" 674 675subsection "Loops" 676 677text \<open> 678 Loops are handled using the following inductive predicate; 679 non-termination is represented using the failure flag of the 680 monad. 681\<close> 682 683inductive_set 684 whileLoop_results :: "('r \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> ('r \<Rightarrow> ('s, 'r) nondet_monad) \<Rightarrow> ((('r \<times> 's) option) \<times> (('r \<times> 's) option)) set" 685 for C B 686where 687 "\<lbrakk> \<not> C r s \<rbrakk> \<Longrightarrow> (Some (r, s), Some (r, s)) \<in> whileLoop_results C B" 688 | "\<lbrakk> C r s; snd (B r s) \<rbrakk> \<Longrightarrow> (Some (r, s), None) \<in> whileLoop_results C B" 689 | "\<lbrakk> C r s; (r', s') \<in> fst (B r s); (Some (r', s'), z) \<in> whileLoop_results C B \<rbrakk> 690 \<Longrightarrow> (Some (r, s), z) \<in> whileLoop_results C B" 691 692inductive_cases whileLoop_results_cases_valid: "(Some x, Some y) \<in> whileLoop_results C B" 693inductive_cases whileLoop_results_cases_fail: "(Some x, None) \<in> whileLoop_results C B" 694inductive_simps whileLoop_results_simps: "(Some x, y) \<in> whileLoop_results C B" 695inductive_simps whileLoop_results_simps_valid: "(Some x, Some y) \<in> whileLoop_results C B" 696inductive_simps whileLoop_results_simps_start_fail [simp]: "(None, x) \<in> whileLoop_results C B" 697 698inductive 699 whileLoop_terminates :: "('r \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> ('r \<Rightarrow> ('s, 'r) nondet_monad) \<Rightarrow> 'r \<Rightarrow> 's \<Rightarrow> bool" 700 for C B 701where 702 "\<not> C r s \<Longrightarrow> whileLoop_terminates C B r s" 703 | "\<lbrakk> C r s; \<forall>(r', s') \<in> fst (B r s). whileLoop_terminates C B r' s' \<rbrakk> 704 \<Longrightarrow> whileLoop_terminates C B r s" 705 706inductive_cases whileLoop_terminates_cases: "whileLoop_terminates C B r s" 707inductive_simps whileLoop_terminates_simps: "whileLoop_terminates C B r s" 708 709definition 710 "whileLoop C B \<equiv> (\<lambda>r s. 711 ({(r',s'). (Some (r, s), Some (r', s')) \<in> whileLoop_results C B}, 712 (Some (r, s), None) \<in> whileLoop_results C B \<or> (\<not> whileLoop_terminates C B r s)))" 713 714notation (output) 715 whileLoop ("(whileLoop (_)// (_))" [1000, 1000] 1000) 716 717definition 718 whileLoopE :: "('r \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> ('r \<Rightarrow> ('s, 'e + 'r) nondet_monad) 719 \<Rightarrow> 'r \<Rightarrow> 's \<Rightarrow> (('e + 'r) \<times> 's) set \<times> bool" 720where 721 "whileLoopE C body \<equiv> 722 \<lambda>r. whileLoop (\<lambda>r s. (case r of Inr v \<Rightarrow> C v s | _ \<Rightarrow> False)) (lift body) (Inr r)" 723 724notation (output) 725 whileLoopE ("(whileLoopE (_)// (_))" [1000, 1000] 1000) 726 727section "Hoare Logic" 728 729subsection "Validity" 730 731text \<open>This section defines a Hoare logic for partial correctness for 732 the nondeterministic state monad as well as the exception monad. 733 The logic talks only about the behaviour part of the monad and ignores 734 the failure flag. 735 736 The logic is defined semantically. Rules work directly on the 737 validity predicate. 738 739 In the nondeterministic state monad, validity is a triple of precondition, 740 monad, and postcondition. The precondition is a function from state to 741 bool (a state predicate), the postcondition is a function from return value 742 to state to bool. A triple is valid if for all states that satisfy the 743 precondition, all result values and result states that are returned by 744 the monad satisfy the postcondition. Note that if the computation returns 745 the empty set, the triple is trivially valid. This means @{term "assert P"} 746 does not require us to prove that @{term P} holds, but rather allows us 747 to assume @{term P}! Proving non-failure is done via separate predicate and 748 calculus (see below). 749\<close> 750definition 751 valid :: "('s \<Rightarrow> bool) \<Rightarrow> ('s,'a) nondet_monad \<Rightarrow> ('a \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> bool" 752 ("\<lbrace>_\<rbrace>/ _ /\<lbrace>_\<rbrace>") 753where 754 "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<equiv> \<forall>s. P s \<longrightarrow> (\<forall>(r,s') \<in> fst (f s). Q r s')" 755 756text \<open> 757 We often reason about invariant predicates. The following provides shorthand syntax 758 that avoids repeating potentially long predicates. 759\<close> 760abbreviation (input) 761 invariant :: "('s,'a) nondet_monad \<Rightarrow> ('s \<Rightarrow> bool) \<Rightarrow> bool" ("_ \<lbrace>_\<rbrace>" [59,0] 60) 762where 763 "invariant f P \<equiv> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>" 764 765text \<open> 766 Validity for the exception monad is similar and build on the standard 767 validity above. Instead of one postcondition, we have two: one for 768 normal and one for exceptional results. 769\<close> 770definition 771 validE :: "('s \<Rightarrow> bool) \<Rightarrow> ('s, 'a + 'b) nondet_monad \<Rightarrow> 772 ('b \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> 773 ('a \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> bool" 774("\<lbrace>_\<rbrace>/ _ /(\<lbrace>_\<rbrace>,/ \<lbrace>_\<rbrace>)") 775where 776 "\<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>" 777 778 779text \<open> 780 The following two instantiations are convenient to separate reasoning 781 for exceptional and normal case. 782\<close> 783definition 784 validE_R :: "('s \<Rightarrow> bool) \<Rightarrow> ('s, 'e + 'a) nondet_monad \<Rightarrow> 785 ('a \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> bool" 786 ("\<lbrace>_\<rbrace>/ _ /\<lbrace>_\<rbrace>, -") 787where 788 "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,- \<equiv> validE P f Q (\<lambda>x y. True)" 789 790definition 791 validE_E :: "('s \<Rightarrow> bool) \<Rightarrow> ('s, 'e + 'a) nondet_monad \<Rightarrow> 792 ('e \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> bool" 793 ("\<lbrace>_\<rbrace>/ _ /-, \<lbrace>_\<rbrace>") 794where 795 "\<lbrace>P\<rbrace> f -,\<lbrace>Q\<rbrace> \<equiv> validE P f (\<lambda>x y. True) Q" 796 797 798text \<open>Abbreviations for trivial preconditions:\<close> 799abbreviation(input) 800 top :: "'a \<Rightarrow> bool" ("\<top>") 801where 802 "\<top> \<equiv> \<lambda>_. True" 803 804abbreviation(input) 805 bottom :: "'a \<Rightarrow> bool" ("\<bottom>") 806where 807 "\<bottom> \<equiv> \<lambda>_. False" 808 809text \<open>Abbreviations for trivial postconditions (taking two arguments):\<close> 810abbreviation(input) 811 toptop :: "'a \<Rightarrow> 'b \<Rightarrow> bool" ("\<top>\<top>") 812where 813 "\<top>\<top> \<equiv> \<lambda>_ _. True" 814 815abbreviation(input) 816 botbot :: "'a \<Rightarrow> 'b \<Rightarrow> bool" ("\<bottom>\<bottom>") 817where 818 "\<bottom>\<bottom> \<equiv> \<lambda>_ _. False" 819 820text \<open> 821 Lifting @{text "\<and>"} and @{text "\<or>"} over two arguments. 822 Lifting @{text "\<and>"} and @{text "\<or>"} over one argument is already 823 defined (written @{text "and"} and @{text "or"}). 824\<close> 825definition 826 bipred_conj :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> bool)" 827 (infixl "And" 96) 828where 829 "bipred_conj P Q \<equiv> \<lambda>x y. P x y \<and> Q x y" 830 831definition 832 bipred_disj :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> bool)" 833 (infixl "Or" 91) 834where 835 "bipred_disj P Q \<equiv> \<lambda>x y. P x y \<or> Q x y" 836 837 838subsection "Determinism" 839 840text \<open>A monad of type @{text nondet_monad} is deterministic iff it 841returns exactly one state and result and does not fail\<close> 842definition 843 det :: "('a,'s) nondet_monad \<Rightarrow> bool" 844where 845 "det f \<equiv> \<forall>s. \<exists>r. f s = ({r},False)" 846 847text \<open>A deterministic @{text nondet_monad} can be turned 848 into a normal state monad:\<close> 849definition 850 the_run_state :: "('s,'a) nondet_monad \<Rightarrow> 's \<Rightarrow> 'a \<times> 's" 851where 852 "the_run_state M \<equiv> \<lambda>s. THE s'. fst (M s) = {s'}" 853 854 855subsection "Non-Failure" 856 857text \<open> 858 With the failure flag, we can formulate non-failure separately 859 from validity. A monad @{text m} does not fail under precondition 860 @{text P}, if for no start state in that precondition it sets 861 the failure flag. 862\<close> 863definition 864 no_fail :: "('s \<Rightarrow> bool) \<Rightarrow> ('s,'a) nondet_monad \<Rightarrow> bool" 865where 866 "no_fail P m \<equiv> \<forall>s. P s \<longrightarrow> \<not> (snd (m s))" 867 868 869text \<open> 870 It is often desired to prove non-failure and a Hoare triple 871 simultaneously, as the reasoning is often similar. The following 872 definitions allow such reasoning to take place. 873\<close> 874 875definition 876 validNF ::"('s \<Rightarrow> bool) \<Rightarrow> ('s,'a) nondet_monad \<Rightarrow> ('a \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> bool" 877 ("\<lbrace>_\<rbrace>/ _ /\<lbrace>_\<rbrace>!") 878where 879 "validNF P f Q \<equiv> valid P f Q \<and> no_fail P f" 880 881definition 882 validE_NF :: "('s \<Rightarrow> bool) \<Rightarrow> ('s, 'a + 'b) nondet_monad \<Rightarrow> 883 ('b \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> 884 ('a \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> bool" 885 ("\<lbrace>_\<rbrace>/ _ /(\<lbrace>_\<rbrace>,/ \<lbrace>_\<rbrace>!)") 886where 887 "validE_NF P f Q E \<equiv> validE P f Q E \<and> no_fail P f" 888 889lemma validE_NF_alt_def: 890 "\<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>!" 891 by (clarsimp simp: validE_NF_def validE_def validNF_def) 892 893text \<open> 894 Usually, well-formed monads constructed from the primitives 895 above will have the following property: if they return an 896 empty set of results, they will have the failure flag set. 897\<close> 898definition 899 empty_fail :: "('s,'a) nondet_monad \<Rightarrow> bool" 900where 901 "empty_fail m \<equiv> \<forall>s. fst (m s) = {} \<longrightarrow> snd (m s)" 902 903 904text \<open> 905 Useful in forcing otherwise unknown executions to have 906 the @{const empty_fail} property. 907\<close> 908definition 909 mk_ef :: "'a set \<times> bool \<Rightarrow> 'a set \<times> bool" 910where 911 "mk_ef S \<equiv> (fst S, fst S = {} \<or> snd S)" 912 913section "Basic exception reasoning" 914 915text \<open> 916 The following predicates @{text no_throw} and @{text no_return} allow 917 reasoning that functions in the exception monad either do 918 no throw an exception or never return normally. 919\<close> 920 921definition "no_throw P A \<equiv> \<lbrace> P \<rbrace> A \<lbrace> \<lambda>_ _. True \<rbrace>,\<lbrace> \<lambda>_ _. False \<rbrace>" 922 923definition "no_return P A \<equiv> \<lbrace> P \<rbrace> A \<lbrace>\<lambda>_ _. False\<rbrace>,\<lbrace>\<lambda>_ _. True \<rbrace>" 924 925end 926