From ca50a02739f2e74100b356e0a1ab0fe160ba3b37 Mon Sep 17 00:00:00 2001 From: Corey Lewis Date: Thu, 5 Oct 2023 13:18:14 +1100 Subject: [PATCH] lib/monads: improve style of nondet and trace Signed-off-by: Corey Lewis --- lib/Monads/nondet/Nondet_Monad.thy | 49 +++++------ lib/Monads/nondet/Nondet_No_Fail.thy | 4 +- lib/Monads/nondet/Nondet_While_Loop_Rules.thy | 2 +- lib/Monads/trace/Trace_Monad.thy | 33 ++++---- lib/Monads/trace/Trace_Monad_Equations.thy | 8 ++ lib/Monads/trace/Trace_More_VCG.thy | 26 ------ lib/Monads/trace/Trace_No_Fail.thy | 2 +- lib/Monads/trace/Trace_Sat.thy | 2 +- lib/Monads/trace/Trace_VCG.thy | 82 ++++++++++++++++++- lib/concurrency/Triv_Refinement.thy | 2 +- 10 files changed, 130 insertions(+), 80 deletions(-) diff --git a/lib/Monads/nondet/Nondet_Monad.thy b/lib/Monads/nondet/Nondet_Monad.thy index 38ed3d4f78..9231ae3c1a 100644 --- a/lib/Monads/nondet/Nondet_Monad.thy +++ b/lib/Monads/nondet/Nondet_Monad.thy @@ -76,8 +76,7 @@ definition bind :: "bind f g \ \s. (\(fst ` case_prod g ` fst (f s)), True \ snd ` case_prod g ` fst (f s) \ snd (f s))" -text \ - Sometimes it is convenient to write @{text bind} in reverse order.\ +text \Sometimes it is convenient to write @{text bind} in reverse order.\ abbreviation (input) bind_rev :: "('c \ ('a, 'b) nondet_monad) \ ('a, 'c) nondet_monad \ ('a, 'b) nondet_monad" (infixl "=<<" 60) where @@ -125,20 +124,21 @@ text \ definition state_select :: "('s \ 's) set \ ('s, unit) nondet_monad" where "state_select r \ \s. ((\x. ((), x)) ` {s'. (s, s') \ r}, \ (\s'. (s, s') \ r))" + subsection "Failure" text \ The monad function that always fails. Returns an empty set of results and sets the failure flag.\ definition fail :: "('s, 'a) nondet_monad" where - "fail \ \s. ({}, True)" + "fail \ \s. ({}, True)" text \Assertions: fail if the property @{text P} is not true\ definition assert :: "bool \ ('a, unit) nondet_monad" where - "assert P \ if P then return () else fail" + "assert P \ if P then return () else fail" text \Fail if the value is @{const None}, return result @{text v} for @{term "Some v"}\ definition assert_opt :: "'a option \ ('b, 'a) nondet_monad" where - "assert_opt v \ case v of None \ fail | Some v \ return v" + "assert_opt v \ case v of None \ fail | Some v \ return v" text \An assertion that also can introspect the current state.\ definition state_assert :: "('s \ bool) \ ('s, unit) nondet_monad" where @@ -148,11 +148,11 @@ subsection "Generic functions on top of the state monad" text \Apply a function to the current state and return the result without changing the state.\ definition gets :: "('s \ 'a) \ ('s, 'a) nondet_monad" where - "gets f \ get >>= (\s. return (f s))" + "gets f \ get >>= (\s. return (f s))" text \Modify the current state using the function passed in.\ definition modify :: "('s \ 's) \ ('s, unit) nondet_monad" where - "modify f \ get >>= (\s. put (f s))" + "modify f \ get >>= (\s. put (f s))" lemma simpler_gets_def: "gets f = (\s. ({(f s, s)}, False))" @@ -196,7 +196,7 @@ definition subsection \The Monad Laws\ -text \A more expanded definition of @{text bind}\ +text \An alternative definition of @{term bind}, sometimes more convenient.\ lemma bind_def': "(f >>= g) \ \s. ({(r'', s''). \(r', s') \ fst (f s). (r'', s'') \ fst (g r' s') }, @@ -212,7 +212,8 @@ lemma return_bind[simp]: by (simp add: return_def bind_def) text \@{term return} is absorbed on the right of a @{term bind}\ -lemma bind_return[simp]: "(m >>= return) = m" +lemma bind_return[simp]: + "(m >>= return) = m" by (simp add: bind_def return_def split_def) text \@{term bind} is associative\ @@ -264,7 +265,6 @@ definition bindE :: (infixl ">>=E" 60) where "f >>=E g \ f >>= lift g" - text \ Lifting a normal nondeterministic monad into the exception monad is achieved by always returning its @@ -272,7 +272,6 @@ text \ definition liftE :: "('s,'a) nondet_monad \ ('s, 'e+'a) nondet_monad" where "liftE f \ f >>= (\r. return (Inr r))" - text \ Since the underlying type and @{text return} function changed, we need new definitions for when and unless:\ @@ -282,13 +281,11 @@ definition whenE :: "bool \ ('s, 'e + unit) nondet_monad \ ('s, 'e + unit) nondet_monad \ ('s, 'e + unit) nondet_monad" where "unlessE P f \ if P then returnOk () else f" - text \ Throwing an exception when the parameter is @{term None}, otherwise returning @{term "v"} for @{term "Some v"}.\ definition throw_opt :: "'e \ 'a option \ ('s, 'e + 'a) nondet_monad" where - "throw_opt ex x \ case x of None \ throwError ex | Some v \ returnOk v" - + "throw_opt ex x \ case x of None \ throwError ex | Some v \ returnOk v" text \ Failure in the exception monad is redefined in the same way @@ -297,6 +294,7 @@ text \ definition assertE :: "bool \ ('a, 'e + unit) nondet_monad" where "assertE P \ if P then returnOk () else fail" + subsection "Monad Laws for the Exception Monad" text \More direct definition of @{const liftE}:\ @@ -415,9 +413,7 @@ lemma "doE x \ returnOk 1; by simp - -section "Library of Monadic Functions and Combinators" - +section "Library of additional Monadic Functions and Combinators" text \Lifting a normal function into the monad type:\ definition liftM :: "('a \ 'b) \ ('s,'a) nondet_monad \ ('s, 'b) nondet_monad" where @@ -427,12 +423,11 @@ text \The same for the exception monad:\ definition liftME :: "('a \ 'b) \ ('s,'e+'a) nondet_monad \ ('s,'e+'b) nondet_monad" where "liftME f m \ doE x \ m; returnOk (f x) odE" -text \ Execute @{term f} for @{term "Some x"}, otherwise do nothing. \ +text \Execute @{term f} for @{term "Some x"}, otherwise do nothing.\ definition maybeM :: "('a \ ('s, unit) nondet_monad) \ 'a option \ ('s, unit) nondet_monad" where "maybeM f y \ case y of Some x \ f x | None \ return ()" -text \ - Run a sequence of monads from left to right, ignoring return values.\ +text \Run a sequence of monads from left to right, ignoring return values.\ definition sequence_x :: "('s, 'a) nondet_monad list \ ('s, unit) nondet_monad" where "sequence_x xs \ foldr (\x y. x >>= (\_. y)) xs (return ())" @@ -450,7 +445,6 @@ definition zipWithM_x :: "('a \ 'b \ ('s,'c) nondet_monad) \ 'a list \ 'b list \ ('s, unit) nondet_monad" where "zipWithM_x f xs ys \ sequence_x (zipWith f xs ys)" - text \ The same three functions as above, but returning a list of return values instead of @{text unit}\ @@ -465,8 +459,8 @@ definition zipWithM :: "('a \ 'b \ ('s,'c) nondet_monad) \ 'a list \ 'b list \ ('s, 'c list) nondet_monad" where "zipWithM f xs ys \ sequence (zipWith f xs ys)" -definition foldM :: "('b \ 'a \ ('s, 'a) nondet_monad) \ 'b list \ 'a \ ('s, 'a) nondet_monad" - where +definition foldM :: + "('b \ 'a \ ('s, 'a) nondet_monad) \ 'b list \ 'a \ ('s, 'a) nondet_monad" where "foldM m xs a \ foldr (\p q. q >>= m p) xs (return a) " definition foldME :: @@ -486,11 +480,10 @@ definition sequenceE :: "('s, 'e+'a) nondet_monad list \ ('s, 'e+'a "sequenceE xs \ let mcons = (\p q. p >>=E (\x. q >>=E (\y. returnOk (x#y)))) in foldr mcons xs (returnOk [])" -definition mapME :: "('a \ ('s,'e+'b) nondet_monad) \ 'a list \ ('s,'e+'b list) nondet_monad" - where +definition mapME :: + "('a \ ('s,'e+'b) nondet_monad) \ 'a list \ ('s,'e+'b list) nondet_monad" where "mapME f xs \ sequenceE (map f xs)" - text \Filtering a list using a monadic function as predicate:\ primrec filterM :: "('a \ ('s, bool) nondet_monad) \ 'a list \ ('s, 'a list) nondet_monad" where "filterM P [] = return []" @@ -556,12 +549,10 @@ definition handleE :: (infix "" 10) where "handleE \ handleE'" - text \ Handling exceptions, and additionally providing a continuation if the left-hand side throws no exception:\ -definition - handle_elseE :: +definition handle_elseE :: "('s, 'e + 'a) nondet_monad \ ('e \ ('s, 'ee + 'b) nondet_monad) \ ('a \ ('s, 'ee + 'b) nondet_monad) \ ('s, 'ee + 'b) nondet_monad" ("_ _ _" 10) where diff --git a/lib/Monads/nondet/Nondet_No_Fail.thy b/lib/Monads/nondet/Nondet_No_Fail.thy index 9b59fc178f..9d5fc534e9 100644 --- a/lib/Monads/nondet/Nondet_No_Fail.thy +++ b/lib/Monads/nondet/Nondet_No_Fail.thy @@ -160,7 +160,7 @@ lemma no_fail_spec: lemma no_fail_assertE[wp]: "no_fail (\_. P) (assertE P)" - by (simp add: assertE_def split: if_split) + by (simp add: assertE_def) lemma no_fail_spec_pre: "\ no_fail (((=) s) and P') f; \s. P s \ P' s \ \ no_fail (((=) s) and P) f" @@ -168,7 +168,7 @@ lemma no_fail_spec_pre: lemma no_fail_whenE[wp]: "\ G \ no_fail P f \ \ no_fail (\s. G \ P s) (whenE G f)" - by (simp add: whenE_def split: if_split) + by (simp add: whenE_def) lemma no_fail_unlessE[wp]: "\ \ G \ no_fail P f \ \ no_fail (\s. \ G \ P s) (unlessE G f)" diff --git a/lib/Monads/nondet/Nondet_While_Loop_Rules.thy b/lib/Monads/nondet/Nondet_While_Loop_Rules.thy index cea7c51e4b..14d9836b8a 100644 --- a/lib/Monads/nondet/Nondet_While_Loop_Rules.thy +++ b/lib/Monads/nondet/Nondet_While_Loop_Rules.thy @@ -287,7 +287,7 @@ lemma fst_whileLoop_cond_false: lemma snd_whileLoop: assumes init_I: "I r s" and cond_I: "C r s" - and non_term: "\r. \ \s. I r s \ C r s \ \ snd (B r s) \ B r \\ \r' s'. C r' s' \ I r' s' \" + and non_term: "\r. \ \s. I r s \ C r s \ \ snd (B r s) \ B r \\ \r' s'. C r' s' \ I r' s' \" shows "snd (whileLoop C B r s)" apply (clarsimp simp: whileLoop_def) apply (rotate_tac) diff --git a/lib/Monads/trace/Trace_Monad.thy b/lib/Monads/trace/Trace_Monad.thy index 7ddffb245c..b3268c35df 100644 --- a/lib/Monads/trace/Trace_Monad.thy +++ b/lib/Monads/trace/Trace_Monad.thy @@ -38,14 +38,13 @@ datatype ('s, 'a) tmres = Failed | Incomplete | Result "('a \ 's)" abbreviation map_tmres_rv :: "('a \ 'b) \ ('s, 'a) tmres \ ('s, 'b) tmres" where "map_tmres_rv f \ map_tmres id f" -section "The Monad" - text \ tmonad returns a set of non-deterministic computations, including a trace as a list of "thread identifier" \ state, and an optional pair of result and state when the computation did not fail.\ type_synonym ('s, 'a) tmonad = "'s \ ((tmid \ 's) list \ ('s, 'a) tmres) set" + text \ Print the type @{typ "('s,'a) tmonad"} instead of its unwieldy expansion. Needs an AST translation in code, because it needs to check that the state variable @@ -64,6 +63,7 @@ print_ast_translation \ else raise Match in [(@{type_syntax "fun"}, tmonad_tr)] end\ + text \Returns monad results, ignoring failures and traces.\ definition mres :: "((tmid \ 's) list \ ('s, 'a) tmres) set \ ('a \ 's) set" where "mres r = Result -` (snd ` r)" @@ -98,9 +98,8 @@ definition bind :: | Result (rv, s) \ fst_upd (\ys. ys @ xs) ` g rv s" text \Sometimes it is convenient to write @{text bind} in reverse order.\ -abbreviation(input) bind_rev :: - "('c \ ('a, 'b) tmonad) \ ('a, 'c) tmonad \ ('a, 'b) tmonad" (infixl "=<<" 60) - where +abbreviation (input) bind_rev :: + "('c \ ('a, 'b) tmonad) \ ('a, 'c) tmonad \ ('a, 'b) tmonad" (infixl "=<<" 60) where "g =<< f \ f >>= g" text \ @@ -123,6 +122,7 @@ primrec put_trace :: "(tmid \ 's) list \ ('s, unit) tmonad" w "put_trace [] = return ()" | "put_trace (x # xs) = (put_trace xs >>= (\_. put_trace_elem x))" + subsection "Nondeterminism" text \ @@ -153,6 +153,7 @@ definition state_select :: "('s \ 's) set \ ('s, unit) tmonad "state_select r \ \s. (Pair [] ` default_elem Failed (Result ` (\x. ((), x)) ` {s'. (s, s') \ r}))" + subsection "Failure" text \ @@ -224,8 +225,8 @@ definition subsection \The Monad Laws\ -text \An alternative definition of bind, sometimes more convenient.\ -lemma bind_def2: +text \An alternative definition of @{term bind}, sometimes more convenient.\ +lemma bind_def': "bind f g \ \s. ((\xs. (xs, Failed)) ` {xs. (xs, Failed) \ f s}) \ ((\xs. (xs, Incomplete)) ` {xs. (xs, Incomplete) \ f s}) @@ -242,7 +243,7 @@ lemma elem_bindE: \res = Incomplete \ res = Failed; (tr, map_tmres undefined undefined res) \ f s\ \ P; \tr' tr'' x s'. \(tr', Result (x, s')) \ f s; (tr'', res) \ g x s'; tr = tr'' @ tr'\ \ P\ \ P" - by (auto simp: bind_def2) + by (auto simp: bind_def') text \Each monad satisfies at least the following three laws.\ @@ -277,6 +278,7 @@ lemma bind_assoc: apply (simp add: image_image) done + section \Adding Exceptions\ text \ @@ -345,6 +347,7 @@ text \ definition assertE :: "bool \ ('a, 'e + unit) tmonad" where "assertE P \ if P then returnOk () else fail" + subsection "Monad Laws for the Exception Monad" text \More direct definition of @{const liftE}:\ @@ -585,7 +588,6 @@ definition sequenceE :: "('s, 'e+'a) tmonad list \ ('s, 'e+'a list) definition mapME :: "('a \ ('s,'e+'b) tmonad) \ 'a list \ ('s,'e+'b list) tmonad" where "mapME f xs \ sequenceE (map f xs)" - text \Filtering a list using a monadic function as predicate:\ primrec filterM :: "('a \ ('s, bool) tmonad) \ 'a list \ ('s, 'a list) tmonad" where "filterM P [] = return []" @@ -751,20 +753,17 @@ definition ifME :: if c then t else f odE" -definition whenM :: - "('s, bool) tmonad \ ('s, unit) tmonad \ ('s, unit) tmonad" where +definition whenM :: "('s, bool) tmonad \ ('s, unit) tmonad \ ('s, unit) tmonad" where "whenM t m = ifM t m (return ())" -definition orM :: - "('s, bool) tmonad \ ('s, bool) tmonad \ ('s, bool) tmonad" where +definition orM :: "('s, bool) tmonad \ ('s, bool) tmonad \ ('s, bool) tmonad" where "orM a b = ifM a (return True) b" -definition - andM :: "('s, bool) tmonad \ ('s, bool) tmonad \ ('s, bool) tmonad" where +definition andM :: "('s, bool) tmonad \ ('s, bool) tmonad \ ('s, bool) tmonad" where "andM a b = ifM a b (return False)" -subsection "Await command" +section "Await command" text \@{term "Await c f"} blocks the execution until @{term "c"} is true, and then atomically executes @{term "f"}.\ @@ -782,7 +781,7 @@ definition Await :: "('s \ bool) \ ('s,unit) tmonad" whe od" -section "Trace monad Parallel" +section "Parallel combinator" definition parallel :: "('s,'a) tmonad \ ('s,'a) tmonad \ ('s,'a) tmonad" where "parallel f g = (\s. {(xs, rv). \f_steps. length f_steps = length xs diff --git a/lib/Monads/trace/Trace_Monad_Equations.thy b/lib/Monads/trace/Trace_Monad_Equations.thy index 2e0815222d..00156438b8 100644 --- a/lib/Monads/trace/Trace_Monad_Equations.thy +++ b/lib/Monads/trace/Trace_Monad_Equations.thy @@ -286,6 +286,14 @@ lemma gets_fold_into_modify: by (simp_all add: fun_eq_iff modify_def bind_assoc exec_gets exec_get exec_put) +lemma gets_return_gets_eq: + "gets f >>= (\g. return (h g)) = gets (\s. h (f s))" + by (simp add: simpler_gets_def bind_def return_def) + +lemma gets_prod_comp: + "gets (case x of (a, b) \ f a b) = (case x of (a, b) \ gets (f a b))" + by (auto simp: split_def) + lemma bind_assoc2: "(do x \ a; _ \ b; c x od) = (do x \ (do x' \ a; _ \ b; return x' od); c x od)" by (simp add: bind_assoc) diff --git a/lib/Monads/trace/Trace_More_VCG.thy b/lib/Monads/trace/Trace_More_VCG.thy index 80f4ab5f7a..927bb04272 100644 --- a/lib/Monads/trace/Trace_More_VCG.thy +++ b/lib/Monads/trace/Trace_More_VCG.thy @@ -45,14 +45,6 @@ lemma hoare_name_pre_stateE: "\\s. P s \ \(=) s\ f \Q\, \E\\ \ \P\ f \Q\, \E\" by (clarsimp simp: validE_def2) -lemma hoare_vcg_if_lift: - "\R\ f \\rv s. (P \ X rv s) \ (\P \ Y rv s)\ \ - \R\ f \\rv s. if P then X rv s else Y rv s\" - - "\R\ f \\rv s. (P \ X rv s) \ (\P \ Y rv s)\ \ - \R\ f \\rv. if P then X rv else Y rv\" - by (auto simp: valid_def split_def) - lemma hoare_vcg_if_lift_strong: "\ \P'\ f \P\; \\s. \ P' s\ f \\rv s. \ P rv s\; \Q'\ f \Q\; \R'\ f \R\ \ \ \\s. if P' s then Q' s else R' s\ f \\rv s. if P rv s then Q rv s else R rv s\" @@ -240,13 +232,6 @@ lemma hoare_vcg_if_lift_ER: (* Required because of lack of rv in lifting rules * \R\ f \\rv. if P' rv then X rv else Y rv\, -" by (auto simp: valid_def validE_R_def validE_def split_def) -lemma hoare_vcg_imp_liftE: - "\ \P'\ f \\rv s. \ P rv s\, \A\; \Q'\ f \Q\, \A\ \ - \ \\s. \ P' s \ Q' s\ f \\rv s. P rv s \ Q rv s\, \A\" - apply (simp only: imp_conv_disj) - apply (clarsimp simp: validE_def valid_def split_def sum.case_eq_if) - done - lemma hoare_list_all_lift: "(\r. r \ set xs \ \Q r\ f \\rv. Q r\) \ \\s. list_all (\r. Q r s) xs\ f \\rv s. list_all (\r. Q r s) xs\" @@ -394,13 +379,6 @@ lemma hoare_validE_R_conj: "\\P\ f \Q\, -; \P\ f \R\, -\ \ \P\ f \Q and R\, -" by (simp add: valid_def validE_def validE_R_def Let_def split_def split: sum.splits) -lemma hoare_vcg_disj_lift_R: - assumes x: "\P\ f \Q\,-" - assumes y: "\P'\ f \Q'\,-" - shows "\\s. P s \ P' s\ f \\rv s. Q rv s \ Q' rv s\,-" - using assms - by (fastforce simp: validE_R_def validE_def valid_def split: sum.splits) - lemmas throwError_validE_R = throwError_wp [where E="\\", folded validE_R_def] lemma valid_case_option_post_wp: @@ -552,10 +530,6 @@ lemma wp_split_const_if_R: shows "\\s. (G \ P s) \ (\ G \ P' s)\ f \\rv s. (G \ Q rv s) \ (\ G \ Q' rv s)\,-" by (case_tac G, simp_all add: x y) -lemma hoare_vcg_imp_lift_R: - "\ \P'\ f \\rv s. \ P rv s\, -; \Q'\ f \Q\, - \ \ \\s. P' s \ Q' s\ f \\rv s. P rv s \ Q rv s\, -" - by (auto simp add: valid_def validE_R_def validE_def split_def split: sum.splits) - lemma hoare_disj_division: "\ P \ Q; P \ \R\ f \S\; Q \ \T\ f \S\ \ \ \\s. (P \ R s) \ (Q \ T s)\ f \S\" diff --git a/lib/Monads/trace/Trace_No_Fail.thy b/lib/Monads/trace/Trace_No_Fail.thy index 3630aa911a..0c0d958edf 100644 --- a/lib/Monads/trace/Trace_No_Fail.thy +++ b/lib/Monads/trace/Trace_No_Fail.thy @@ -131,7 +131,7 @@ lemma no_fail_returnOK[simp, wp]: lemma no_fail_bind[wp]: "\ no_fail P f; \x. no_fail (R x) (g x); \Q\ f \R\ \ \ no_fail (P and Q) (f >>= (\rv. g rv))" - apply (simp add: no_fail_def bind_def2 image_Un image_image + apply (simp add: no_fail_def bind_def' image_Un image_image in_image_constant) apply (intro allI conjI impI) apply (fastforce simp: image_def) diff --git a/lib/Monads/trace/Trace_Sat.thy b/lib/Monads/trace/Trace_Sat.thy index 213303f21a..a329369ea3 100644 --- a/lib/Monads/trace/Trace_Sat.thy +++ b/lib/Monads/trace/Trace_Sat.thy @@ -86,7 +86,7 @@ lemma exs_valid_assume_pre: lemma exs_valid_bind[wp_split]: "\ \rv. \B rv\ g rv \\C\; \A\ f \\B\ \ \ \A\ f >>= (\rv. g rv) \\C\" apply atomize - apply (clarsimp simp: exs_valid_def bind_def2 mres_def) + apply (clarsimp simp: exs_valid_def bind_def' mres_def) apply (drule spec, drule(1) mp, clarsimp) apply (drule spec2, drule(1) mp, clarsimp) apply (simp add: image_def bex_Un) diff --git a/lib/Monads/trace/Trace_VCG.thy b/lib/Monads/trace/Trace_VCG.thy index dd0a2f57a8..f6318eb904 100644 --- a/lib/Monads/trace/Trace_VCG.thy +++ b/lib/Monads/trace/Trace_VCG.thy @@ -143,7 +143,7 @@ subsection "Hoare Logic Rules" lemma bind_wp[wp_split]: "\ \r. \Q' r\ g r \Q\; \P\f \Q'\ \ \ \P\ f >>= (\rv. g rv) \Q\" - by (fastforce simp: valid_def bind_def2 mres_def intro: image_eqI[rotated]) + by (fastforce simp: valid_def bind_def' mres_def intro: image_eqI[rotated]) lemma seq': "\ \A\ f \B\; \x. P x \ \C\ g x \D\; \x s. B x s \ P x \ C s \ \ @@ -467,7 +467,7 @@ lemma in_image_constant: lemma hoare_liftM_subst: "\P\ liftM f m \Q\ = \P\ m \Q \ f\" - apply (simp add: liftM_def bind_def2 return_def split_def) + apply (simp add: liftM_def bind_def' return_def split_def) apply (simp add: valid_def Ball_def mres_def image_Un) apply (simp add: image_image in_image_constant) apply force @@ -554,6 +554,15 @@ lemma hoare_vcg_conj_liftE1: unfolding valid_def validE_R_def validE_def by (fastforce simp: split_def split: sum.splits) +lemma hoare_vcg_conj_liftE_weaker: + assumes "\P\ f \Q\, \E\" + assumes "\P'\ f \Q'\, \E\" + shows "\\s. P s \ P' s\ f \\rv s. Q rv s \ Q' rv s\, \E\" + apply (rule hoare_pre) + apply (fastforce intro: assms hoare_vcg_conj_liftE1 validE_validE_R hoare_post_impErr) + apply simp + done + lemma hoare_vcg_disj_lift: "\ \P\ f \Q\; \P'\ f \Q'\ \ \ \\s. P s \ P' s\ f \\rv s. Q rv s \ Q' rv s\" unfolding valid_def @@ -585,6 +594,19 @@ lemma hoare_vcg_imp_lift': "\ \P'\ f \\rv s. \ P rv s\; \Q'\ f \Q\ \ \ \\s. \ P' s \ Q' s\ f \\rv s. P rv s \ Q rv s\" by (wpsimp wp: hoare_vcg_imp_lift) +lemma hoare_vcg_imp_liftE: + "\ \P'\ f \\rv s. \ P rv s\, \A\; \Q'\ f \Q\, \A\ \ + \ \\s. \ P' s \ Q' s\ f \\rv s. P rv s \ Q rv s\, \A\" + by (fastforce simp: validE_def valid_def split: sum.splits) + +lemma hoare_vcg_imp_lift_R: + "\ \P'\ f \\rv s. \ P rv s\, -; \Q'\ f \Q\, - \ \ \\s. P' s \ Q' s\ f \\rv s. P rv s \ Q rv s\, -" + by (auto simp add: valid_def validE_R_def validE_def split_def split: sum.splits) + +lemma hoare_vcg_imp_lift_R': + "\ \P'\ f \\rv s. \ P rv s\, -; \Q'\ f \Q\, - \ \ \\s. \P' s \ Q' s\ f \\rv s. P rv s \ Q rv s\, -" + by (auto simp add: valid_def validE_R_def validE_def split_def split: sum.splits) + lemma hoare_vcg_imp_conj_lift[wp_comb]: "\ \P\ f \\rv s. Q rv s \ Q' rv s\; \P'\ f \\rv s. (Q rv s \ Q'' rv s) \ Q''' rv s\ \ \ \P and P'\ f \\rv s. (Q rv s \ Q' rv s \ Q'' rv s) \ Q''' rv s\" @@ -605,6 +627,10 @@ lemma hoare_vcg_const_imp_lift: "\ P \ \Q\ m \R\ \ \ \\s. P \ Q s\ m \\rv s. P \ R rv s\" by (cases P, simp_all add: hoare_vcg_prop) +lemma hoare_vcg_const_imp_lift_E: + "(P \ \Q\ f -, \R\) \ \\s. P \ Q s\ f -, \\rv s. P \ R rv s\" + by (fastforce simp: validE_E_def validE_def valid_def split_def split: sum.splits) + lemma hoare_vcg_const_imp_lift_R: "(P \ \Q\ m \R\,-) \ \\s. P \ Q s\ m \\rv s. P \ R rv s\,-" by (fastforce simp: validE_R_def validE_def valid_def split_def split: sum.splits) @@ -708,6 +734,58 @@ lemma hoare_post_comb_imp_conj: "\ \P'\ f \Q\; \P\ f \Q'\; \s. P s \ P' s \ \ \P\ f \\rv s. Q rv s \ Q' rv s\" by (wpsimp wp: hoare_vcg_conj_lift) +lemma hoare_vcg_if_lift: + "\R\ f \\rv s. (P \ X rv s) \ (\P \ Y rv s)\ \ + \R\ f \\rv s. if P then X rv s else Y rv s\" + + "\R\ f \\rv s. (P \ X rv s) \ (\P \ Y rv s)\ \ + \R\ f \\rv. if P then X rv else Y rv\" + by (auto simp: valid_def split_def) + +lemma hoare_vcg_disj_lift_R: + assumes x: "\P\ f \Q\,-" + assumes y: "\P'\ f \Q'\,-" + shows "\\s. P s \ P' s\ f \\rv s. Q rv s \ Q' rv s\,-" + using assms + by (fastforce simp: validE_R_def validE_def valid_def split: sum.splits) + +lemma hoare_vcg_all_liftE: + "\ \x. \P x\ f \Q x\,\E\ \ \ \\s. \x. P x s\ f \\rv s. \x. Q x rv s\,\E\" + by (fastforce simp: validE_def valid_def split: sum.splits) + +lemma hoare_vcg_const_Ball_liftE: + "\ \x. x \ S \ \P x\ f \Q x\,\E\; \\s. True\ f \\r s. True\, \E\ \ \ \\s. \x\S. P x s\ f \\rv s. \x\S. Q x rv s\,\E\" + by (fastforce simp: validE_def valid_def split: sum.splits) + +lemma hoare_vcg_split_lift[wp]: + "\P\ f x y \Q\ \ \P\ case (x, y) of (a, b) \ f a b \Q\" + by simp + +named_theorems hoare_vcg_op_lift +lemmas [hoare_vcg_op_lift] = + hoare_vcg_const_imp_lift + hoare_vcg_const_imp_lift_E + hoare_vcg_const_imp_lift_R + (* leaving out hoare_vcg_conj_lift*, because that is built into wp *) + hoare_vcg_disj_lift + hoare_vcg_disj_lift_R + hoare_vcg_ex_lift + hoare_vcg_ex_liftE + hoare_vcg_ex_liftE_E + hoare_vcg_all_lift + hoare_vcg_all_liftE + hoare_vcg_all_liftE_E + hoare_vcg_all_lift_R + hoare_vcg_const_Ball_lift + hoare_vcg_const_Ball_lift_R + hoare_vcg_const_Ball_lift_E_E + hoare_vcg_split_lift + hoare_vcg_if_lift + hoare_vcg_imp_lift' + hoare_vcg_imp_liftE + hoare_vcg_imp_lift_R + hoare_vcg_imp_liftE_E + subsection \Weakest Precondition Rules\ diff --git a/lib/concurrency/Triv_Refinement.thy b/lib/concurrency/Triv_Refinement.thy index b31995381f..b7dcb869b4 100644 --- a/lib/concurrency/Triv_Refinement.thy +++ b/lib/concurrency/Triv_Refinement.thy @@ -23,7 +23,7 @@ lemma triv_refinement_mono_bind: "(\x. triv_refinement (b x) (d x)) \ triv_refinement (a >>= b) (a >>= d)" apply (simp add: triv_refinement_def bind_def) apply (intro allI UN_mono; simp) - apply (simp only: triv_refinement_def bind_def2 split_def) + apply (simp only: triv_refinement_def bind_def' split_def) apply (intro Un_mono allI order_refl UN_mono image_mono) apply simp done