From 3333395cc32f5b88a1b239ae2922ae90d761014f 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_Lemmas.thy | 3 +- lib/Monads/nondet/Nondet_Monad.thy | 105 +++++++++--------- lib/Monads/nondet/Nondet_No_Fail.thy | 4 +- lib/Monads/nondet/Nondet_Sat.thy | 3 +- lib/Monads/nondet/Nondet_Total.thy | 6 +- lib/Monads/nondet/Nondet_VCG.thy | 8 +- lib/Monads/nondet/Nondet_While_Loop_Rules.thy | 8 +- lib/Monads/trace/Trace_Monad.thy | 85 +++++++------- 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 | 5 +- lib/Monads/trace/Trace_Total.thy | 6 +- lib/Monads/trace/Trace_VCG.thy | 88 ++++++++++++++- lib/concurrency/Triv_Refinement.thy | 2 +- 15 files changed, 219 insertions(+), 140 deletions(-) diff --git a/lib/Monads/nondet/Nondet_Lemmas.thy b/lib/Monads/nondet/Nondet_Lemmas.thy index 20f676bccb..23e0b56b96 100644 --- a/lib/Monads/nondet/Nondet_Lemmas.thy +++ b/lib/Monads/nondet/Nondet_Lemmas.thy @@ -277,7 +277,8 @@ lemma monad_state_eqI [intro]: subsection \General @{const whileLoop} reasoning\ definition whileLoop_terminatesE :: - "('a \ 's \ bool) \ ('a \ ('s, 'e + 'a) nondet_monad) \ 'a \ 's \ bool" where + "('a \ 's \ bool) \ ('a \ ('s, 'e + 'a) nondet_monad) \ 'a \ 's \ bool" + where "whileLoop_terminatesE C B \ \r. whileLoop_terminates (\r s. case r of Inr v \ C v s | _ \ False) (lift B) (Inr r)" diff --git a/lib/Monads/nondet/Nondet_Monad.thy b/lib/Monads/nondet/Nondet_Monad.thy index 38ed3d4f78..e14cf17fd2 100644 --- a/lib/Monads/nondet/Nondet_Monad.thy +++ b/lib/Monads/nondet/Nondet_Monad.thy @@ -71,16 +71,15 @@ text \ operation may have failed, if @{text f} may have failed or @{text g} may have failed on any of the results of @{text f}.\ definition bind :: - "('s, 'a) nondet_monad \ ('a \ ('s, 'b) nondet_monad) \ ('s, 'b) nondet_monad" - (infixl ">>=" 60) where + "('s, 'a) nondet_monad \ ('a \ ('s, 'b) nondet_monad) \ ('s, 'b) nondet_monad" (infixl ">>=" 60) + where "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 + "('c \ ('a, 'b) nondet_monad) \ ('a, 'c) nondet_monad \ ('a, 'b) nondet_monad" (infixl "=<<" 60) + where "g =<< f \ f >>= g" text \ @@ -107,7 +106,8 @@ definition select :: "'a set \ ('s,'a) nondet_monad" where "select A \ \s. (A \ {s}, False)" definition alternative :: - "('s, 'a) nondet_monad \ ('s, 'a) nondet_monad \ ('s, 'a) nondet_monad" (infixl "\" 20) where + "('s, 'a) nondet_monad \ ('s, 'a) nondet_monad \ ('s, 'a) nondet_monad" (infixl "\" 20) + where "f \ g \ \s. (fst (f s) \ fst (g s), snd (f s) \ snd (g s))" text \ @@ -125,20 +125,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 +149,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))" @@ -174,7 +175,8 @@ text \ Perform a test on the current state, performing the left monad if the result is true or the right monad if the result is false. \ definition condition :: - "('s \ bool) \ ('s, 'r) nondet_monad \ ('s, 'r) nondet_monad \ ('s, 'r) nondet_monad" where + "('s \ bool) \ ('s, 'r) nondet_monad \ ('s, 'r) nondet_monad \ ('s, 'r) nondet_monad" + where "condition P L R \ \s. if (P s) then (L s) else (R s)" notation (output) @@ -189,14 +191,13 @@ definition gets_the :: "('s \ 'a option) \ ('s, 'a) nond text \ Get a map (such as a heap) from the current state and apply an argument to the map. Fail if the map returns @{const None}, otherwise return the value.\ -definition - gets_map :: "('s \ 'a \ 'b option) \ 'a \ ('s, 'b) nondet_monad" where +definition gets_map :: "('s \ 'a \ 'b option) \ 'a \ ('s, 'b) nondet_monad" where "gets_map f p \ gets f >>= (\m. assert_opt (m p))" 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 +213,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 +266,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 +273,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 +282,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 +295,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 +414,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 +424,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 ())" @@ -447,10 +443,10 @@ text \ going through both lists simultaneously, left to right, ignoring return values.\ definition zipWithM_x :: - "('a \ 'b \ ('s,'c) nondet_monad) \ 'a list \ 'b list \ ('s, unit) nondet_monad" where + "('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}\ @@ -462,15 +458,18 @@ definition mapM :: "('a \ ('s,'b) nondet_monad) \ 'a lis "mapM f xs \ sequence (map f xs)" definition zipWithM :: - "('a \ 'b \ ('s,'c) nondet_monad) \ 'a list \ 'b list \ ('s, 'c list) nondet_monad" where + "('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" +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 :: - "('b \ 'a \ ('s,('e + 'b)) nondet_monad) \ 'b \ 'a list \ ('s, ('e + 'b)) nondet_monad" where + "('b \ 'a \ ('s,('e + 'b)) nondet_monad) \ 'b \ 'a list \ ('s, ('e + 'b)) nondet_monad" + where "foldME m a xs \ foldr (\p q. q >>=E swp m p) xs (returnOk a)" text \ @@ -486,11 +485,11 @@ 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" +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 []" @@ -536,8 +535,7 @@ text \ The handler may throw a type of exceptions different from the left side.\ definition handleE' :: - "('s, 'e1 + 'a) nondet_monad \ ('e1 \ ('s, 'e2 + 'a) nondet_monad) \ - ('s, 'e2 + 'a) nondet_monad" + "('s, 'e1 + 'a) nondet_monad \ ('e1 \ ('s, 'e2 + 'a) nondet_monad) \ ('s, 'e2 + 'a) nondet_monad" (infix "" 10) where "f handler \ do @@ -556,15 +554,13 @@ 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 + ('a \ ('s, 'ee + 'b) nondet_monad) \ ('s, 'ee + 'b) nondet_monad" ("_ _ _" 10) + where "f handler continue \ do v \ f; case v of Inl e \ handler e @@ -593,7 +589,8 @@ inductive_simps whileLoop_results_simps_valid: "(Some x, Some y) \ whileLoop inductive_simps whileLoop_results_simps_start_fail[simp]: "(None, x) \ whileLoop_results C B" inductive whileLoop_terminates :: - "('r \ 's \ bool) \ ('r \ ('s, 'r) nondet_monad) \ 'r \ 's \ bool" for C B where + "('r \ 's \ bool) \ ('r \ ('s, 'r) nondet_monad) \ 'r \ 's \ bool" + for C B where "\ C r s \ whileLoop_terminates C B r s" | "\ C r s; \(r', s') \ fst (B r s). whileLoop_terminates C B r' s' \ \ whileLoop_terminates C B r s" @@ -602,7 +599,8 @@ inductive_cases whileLoop_terminates_cases: "whileLoop_terminates C B r s" inductive_simps whileLoop_terminates_simps: "whileLoop_terminates C B r s" definition whileLoop :: - "('a \ 'b \ bool) \ ('a \ ('b, 'a) nondet_monad) \ 'a \ ('b, 'a) nondet_monad" where + "('a \ 'b \ bool) \ ('a \ ('b, 'a) nondet_monad) \ 'a \ ('b, 'a) nondet_monad" + where "whileLoop C B \ \r s. ({(r',s'). (Some (r, s), Some (r', s')) \ whileLoop_results C B}, (Some (r, s), None) \ whileLoop_results C B \ \whileLoop_terminates C B r s)" @@ -626,7 +624,8 @@ definition notM :: "('s, bool) nondet_monad \ ('s, bool) nondet_mona "notM m = do c \ m; return (\ c) od" definition whileM :: - "('s, bool) nondet_monad \ ('s, 'a) nondet_monad \ ('s, unit) nondet_monad" where + "('s, bool) nondet_monad \ ('s, 'a) nondet_monad \ ('s, unit) nondet_monad" + where "whileM C B \ do c \ C; whileLoop (\c s. c) (\_. do B; C od) c; @@ -634,8 +633,8 @@ definition whileM :: od" definition ifM :: - "('s, bool) nondet_monad \ ('s, 'a) nondet_monad \ ('s, 'a) nondet_monad \ - ('s, 'a) nondet_monad" where + "('s, bool) nondet_monad \ ('s, 'a) nondet_monad \ ('s, 'a) nondet_monad \ ('s, 'a) nondet_monad" + where "ifM test t f = do c \ test; if c then t else f @@ -643,22 +642,26 @@ definition ifM :: definition ifME :: "('a, 'b + bool) nondet_monad \ ('a, 'b + 'c) nondet_monad \ ('a, 'b + 'c) nondet_monad - \ ('a, 'b + 'c) nondet_monad" where + \ ('a, 'b + 'c) nondet_monad" + where "ifME test t f = doE c \ test; if c then t else f odE" definition whenM :: - "('s, bool) nondet_monad \ ('s, unit) nondet_monad \ ('s, unit) nondet_monad" where + "('s, bool) nondet_monad \ ('s, unit) nondet_monad \ ('s, unit) nondet_monad" + where "whenM t m = ifM t m (return ())" definition orM :: - "('s, bool) nondet_monad \ ('s, bool) nondet_monad \ ('s, bool) nondet_monad" where + "('s, bool) nondet_monad \ ('s, bool) nondet_monad \ ('s, bool) nondet_monad" + where "orM a b = ifM a (return True) b" definition andM :: - "('s, bool) nondet_monad \ ('s, bool) nondet_monad \ ('s, bool) nondet_monad" where + "('s, bool) nondet_monad \ ('s, bool) nondet_monad \ ('s, bool) nondet_monad" + where "andM a b = ifM a b (return False)" end 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_Sat.thy b/lib/Monads/nondet/Nondet_Sat.thy index ed49330050..f49ff82b8e 100644 --- a/lib/Monads/nondet/Nondet_Sat.thy +++ b/lib/Monads/nondet/Nondet_Sat.thy @@ -17,7 +17,8 @@ text \ The dual to validity: an existential instead of a universal quantifier for the post condition. In refinement, it is often sufficient to know that there is one state that satisfies a condition.\ definition exs_valid :: - "('a \ bool) \ ('a, 'b) nondet_monad \ ('b \ 'a \ bool) \ bool" ("\_\ _ \\_\") where + "('a \ bool) \ ('a, 'b) nondet_monad \ ('b \ 'a \ bool) \ bool" + ("\_\ _ \\_\") where "\P\ f \\Q\ \ \s. P s \ (\(rv, s') \ fst (f s). Q rv s')" text \The above for the exception monad\ diff --git a/lib/Monads/nondet/Nondet_Total.thy b/lib/Monads/nondet/Nondet_Total.thy index bcdea51247..5eac5abd4b 100644 --- a/lib/Monads/nondet/Nondet_Total.thy +++ b/lib/Monads/nondet/Nondet_Total.thy @@ -20,7 +20,8 @@ text \ is often similar. The following definitions allow such reasoning to take place.\ definition validNF :: - "('s \ bool) \ ('s,'a) nondet_monad \ ('a \ 's \ bool) \ bool" ("\_\/ _ /\_\!") where + "('s \ bool) \ ('s,'a) nondet_monad \ ('a \ 's \ bool) \ bool" + ("\_\/ _ /\_\!") where "\P\ f \Q\! \ \P\ f \Q\ \ no_fail P f" lemma validNF_alt_def: @@ -304,7 +305,8 @@ lemma validNF_nobindE[wp]: text \ Set up triple rules for @{term validE_NF} so that we can use @{method wp} combinator rules.\ definition validE_NF_property :: - "('a \ 's \ bool) \ ('c \ 's \ bool) \ 's \ ('s, 'c+'a) nondet_monad \ bool" where + "('a \ 's \ bool) \ ('c \ 's \ bool) \ 's \ ('s, 'c+'a) nondet_monad \ bool" + where "validE_NF_property Q E s b \ \ snd (b s) \ (\(r', s') \ fst (b s). case r' of Inl x \ E x s' | Inr x \ Q x s')" diff --git a/lib/Monads/nondet/Nondet_VCG.thy b/lib/Monads/nondet/Nondet_VCG.thy index 94654fe46d..e8304f0f9a 100644 --- a/lib/Monads/nondet/Nondet_VCG.thy +++ b/lib/Monads/nondet/Nondet_VCG.thy @@ -35,14 +35,16 @@ text \ to assume @{term P}! Proving non-failure is done via a separate predicate and calculus (see Nondet_No_Fail).\ definition valid :: - "('s \ bool) \ ('s,'a) nondet_monad \ ('a \ 's \ bool) \ bool" ("\_\/ _ /\_\") where + "('s \ bool) \ ('s,'a) nondet_monad \ ('a \ 's \ bool) \ bool" + ("\_\/ _ /\_\") where "\P\ f \Q\ \ \s. P s \ (\(r,s') \ fst (f s). Q r s')" text \ We often reason about invariant predicates. The following provides shorthand syntax that avoids repeating potentially long predicates.\ abbreviation (input) invariant :: - "('s,'a) nondet_monad \ ('s \ bool) \ bool" ("_ \_\" [59,0] 60) where + "('s,'a) nondet_monad \ ('s \ bool) \ bool" + ("_ \_\" [59,0] 60) where "invariant f P \ \P\ f \\_. P\" text \ @@ -708,7 +710,7 @@ lemma hoare_vcg_if_lift: by (auto simp: valid_def split_def) lemma hoare_vcg_disj_lift_R: - assumes x: "\P\ f \Q\,-" + 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 diff --git a/lib/Monads/nondet/Nondet_While_Loop_Rules.thy b/lib/Monads/nondet/Nondet_While_Loop_Rules.thy index cea7c51e4b..f216454e70 100644 --- a/lib/Monads/nondet/Nondet_While_Loop_Rules.thy +++ b/lib/Monads/nondet/Nondet_While_Loop_Rules.thy @@ -47,12 +47,14 @@ text \ \ definition whileLoop_inv :: "('a \ 'b \ bool) \ ('a \ ('b, 'a) nondet_monad) \ 'a \ ('a \ 'b \ bool) \ - (('a \ 'b) \ 'a \ 'b) set \ ('b, 'a) nondet_monad" where + (('a \ 'b) \ 'a \ 'b) set \ ('b, 'a) nondet_monad" + where "whileLoop_inv C B x I R \ whileLoop C B x" definition whileLoopE_inv :: "('a \ 'b \ bool) \ ('a \ ('b, 'c + 'a) nondet_monad) \ 'a \ ('a \ 'b \ bool) \ - (('a \ 'b) \ 'a \ 'b) set \ ('b, 'c + 'a) nondet_monad" where + (('a \ 'b) \ 'a \ 'b) set \ ('b, 'c + 'a) nondet_monad" + where "whileLoopE_inv C B x I R \ whileLoopE C B x" lemma whileLoop_add_inv: @@ -287,7 +289,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..f0d093b77e 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,7 +98,7 @@ 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 :: +abbreviation (input) bind_rev :: "('c \ ('a, 'b) tmonad) \ ('a, 'c) tmonad \ ('a, 'b) tmonad" (infixl "=<<" 60) where "g =<< f \ f >>= g" @@ -123,6 +123,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 \ @@ -134,8 +135,9 @@ text \ definition select :: "'a set \ ('s, 'a) tmonad" where "select A \ \s. (Pair [] ` Result ` (A \ {s}))" -definition alternative :: "('s,'a) tmonad \ ('s,'a) tmonad \ ('s,'a) tmonad" - (infixl "\" 20) where +definition alternative :: + "('s,'a) tmonad \ ('s,'a) tmonad \ ('s,'a) tmonad" (infixl "\" 20) + where "f \ g \ \s. (f s \ g s)" text \ @@ -153,6 +155,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 \ @@ -202,7 +205,8 @@ text \ Perform a test on the current state, performing the left monad if the result is true or the right monad if the result is false.\ definition condition :: - "('s \ bool) \ ('s, 'r) tmonad \ ('s, 'r) tmonad \ ('s, 'r) tmonad" where + "('s \ bool) \ ('s, 'r) tmonad \ ('s, 'r) tmonad \ ('s, 'r) tmonad" + where "condition P L R \ \s. if (P s) then (L s) else (R s)" notation (output) @@ -217,15 +221,14 @@ definition gets_the :: "('s \ 'a option) \ ('s, 'a) tmon text \ Get a map (such as a heap) from the current state and apply an argument to the map. Fail if the map returns @{const None}, otherwise return the value.\ -definition - gets_map :: "('s \ 'a \ 'b option) \ 'a \ ('s, 'b) tmonad" where +definition gets_map :: "('s \ 'a \ 'b option) \ 'a \ ('s, 'b) tmonad" where "gets_map f p \ gets f >>= (\m. assert_opt (m p))" 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 +245,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 +280,7 @@ lemma bind_assoc: apply (simp add: image_image) done + section \Adding Exceptions\ text \ @@ -312,8 +316,8 @@ text \ the right-hand side is skipped if the left-hand side produced an exception.\ definition bindE :: - "('s, 'e + 'a) tmonad \ ('a \ ('s, 'e + 'b) tmonad) \ ('s, 'e + 'b) tmonad" - (infixl ">>=E" 60) where + "('s, 'e + 'a) tmonad \ ('a \ ('s, 'e + 'b) tmonad) \ ('s, 'e + 'b) tmonad" (infixl ">>=E" 60) + where "f >>=E g \ f >>= lift g" text \ @@ -345,6 +349,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}:\ @@ -545,7 +550,8 @@ text \ going through both lists simultaneously, left to right, ignoring return values.\ definition zipWithM_x :: - "('a \ 'b \ ('s,'c) tmonad) \ 'a list \ 'b list \ ('s, unit) tmonad" where + "('a \ 'b \ ('s,'c) tmonad) \ 'a list \ 'b list \ ('s, unit) tmonad" + where "zipWithM_x f xs ys \ sequence_x (zipWith f xs ys)" text \ @@ -559,14 +565,16 @@ definition mapM :: "('a \ ('s,'b) tmonad) \ 'a list \ sequence (map f xs)" definition zipWithM :: - "('a \ 'b \ ('s,'c) tmonad) \ 'a list \ 'b list \ ('s, 'c list) tmonad" where + "('a \ 'b \ ('s,'c) tmonad) \ 'a list \ 'b list \ ('s, 'c list) tmonad" + where "zipWithM f xs ys \ sequence (zipWith f xs ys)" definition foldM :: "('b \ 'a \ ('s, 'a) tmonad) \ 'b list \ 'a \ ('s, 'a) tmonad" where "foldM m xs a \ foldr (\p q. q >>= m p) xs (return a) " definition foldME :: - "('b \ 'a \ ('s,('e + 'b)) tmonad) \ 'b \ 'a list \ ('s, ('e + 'b)) tmonad" where + "('b \ 'a \ ('s,('e + 'b)) tmonad) \ 'b \ 'a list \ ('s, ('e + 'b)) tmonad" + where "foldME m a xs \ foldr (\p q. q >>=E swp m p) xs (returnOk a)" text \ @@ -585,7 +593,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 []" @@ -617,7 +624,8 @@ text \ Turning an exception monad into a normal state monad by catching and handling any potential exceptions:\ definition catch :: - "('s, 'e + 'a) tmonad \ ('e \ ('s, 'a) tmonad) \ ('s, 'a) tmonad" (infix "" 10) where + "('s, 'e + 'a) tmonad \ ('e \ ('s, 'a) tmonad) \ ('s, 'a) tmonad" (infix "" 10) + where "f handler \ do x \ f; case x of @@ -645,8 +653,8 @@ text \ practice: the exception handle (potentially) throws exception of the same type as the left-hand side.\ definition handleE :: - "('s, 'x + 'a) tmonad \ ('x \ ('s, 'x + 'a) tmonad) \ ('s, 'x + 'a) tmonad" - (infix "" 10) where + "('s, 'x + 'a) tmonad \ ('x \ ('s, 'x + 'a) tmonad) \ ('s, 'x + 'a) tmonad" (infix "" 10) + where "handleE \ handleE'" text \ @@ -654,8 +662,8 @@ text \ if the left-hand side throws no exception:\ definition handle_elseE :: "('s, 'e + 'a) tmonad \ ('e \ ('s, 'ee + 'b) tmonad) \ ('a \ ('s, 'ee + 'b) tmonad) \ - ('s, 'ee + 'b) tmonad" - ("_ _ _" 10) where + ('s, 'ee + 'b) tmonad" ("_ _ _" 10) + where "f handler continue \ do v \ f; case v of Inl e \ handler e @@ -698,7 +706,8 @@ inductive_cases whileLoop_terminates_cases: "whileLoop_terminates C B r s" inductive_simps whileLoop_terminates_simps: "whileLoop_terminates C B r s" definition whileLoop :: - "('r \ 's \ bool) \ ('r \ ('s, 'r) tmonad) \ 'r \ ('s, 'r) tmonad" where + "('r \ 's \ bool) \ ('r \ ('s, 'r) tmonad) \ 'r \ ('s, 'r) tmonad" + where "whileLoop C B \ (\r s. {(ts, res). ((r,s), ts,res) \ whileLoop_results C B})" notation (output) @@ -706,7 +715,8 @@ notation (output) \ \FIXME: why does this differ to Nondet_Monad?\ definition whileLoopT :: - "('r \ 's \ bool) \ ('r \ ('s, 'r) tmonad) \ 'r \ ('s, 'r) tmonad" where + "('r \ 's \ bool) \ ('r \ ('s, 'r) tmonad) \ 'r \ ('s, 'r) tmonad" + where "whileLoopT C B \ (\r s. {(ts, res). ((r,s), ts,res) \ whileLoop_results C B \ whileLoop_terminates C B r s})" @@ -714,7 +724,8 @@ notation (output) whileLoopT ("(whileLoopT (_)// (_))" [1000, 1000] 1000) definition whileLoopE :: - "('r \ 's \ bool) \ ('r \ ('s, 'e + 'r) tmonad) \ 'r \ ('s, ('e + 'r)) tmonad" where + "('r \ 's \ bool) \ ('r \ ('s, 'e + 'r) tmonad) \ 'r \ ('s, ('e + 'r)) tmonad" + where "whileLoopE C body \ \r. whileLoop (\r s. (case r of Inr v \ C v s | _ \ False)) (lift body) (Inr r)" @@ -727,44 +738,38 @@ section "Combinators that have conditions with side effects" definition notM :: "('s, bool) tmonad \ ('s, bool) tmonad" where "notM m = do c \ m; return (\ c) od" -definition whileM :: - "('s, bool) tmonad \ ('s, 'a) tmonad \ ('s, unit) tmonad" where +definition whileM :: "('s, bool) tmonad \ ('s, 'a) tmonad \ ('s, unit) tmonad" where "whileM C B \ do c \ C; whileLoop (\c s. c) (\_. do B; C od) c; return () od" -definition ifM :: - "('s, bool) tmonad \ ('s, 'a) tmonad \ ('s, 'a) tmonad \ - ('s, 'a) tmonad" where +definition ifM :: "('s, bool) tmonad \ ('s, 'a) tmonad \ ('s, 'a) tmonad \ ('s, 'a) tmonad" where "ifM test t f = do c \ test; if c then t else f od" definition ifME :: - "('a, 'b + bool) tmonad \ ('a, 'b + 'c) tmonad \ ('a, 'b + 'c) tmonad - \ ('a, 'b + 'c) tmonad" where + "('a, 'b + bool) tmonad \ ('a, 'b + 'c) tmonad \ ('a, 'b + 'c) tmonad \ ('a, 'b + 'c) tmonad" + where "ifME test t f = doE c \ test; 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 +787,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..af8fcc8ce7 100644 --- a/lib/Monads/trace/Trace_Sat.thy +++ b/lib/Monads/trace/Trace_Sat.thy @@ -17,7 +17,8 @@ text \ The dual to validity: an existential instead of a universal quantifier for the post condition. In refinement, it is often sufficient to know that there is one state that satisfies a condition.\ definition exs_valid :: - "('a \ bool) \ ('a, 'b) tmonad \ ('b \ 'a \ bool) \ bool" ("\_\ _ \\_\") where + "('a \ bool) \ ('a, 'b) tmonad \ ('b \ 'a \ bool) \ bool" + ("\_\ _ \\_\") where "\P\ f \\Q\ \ \s. P s \ (\(rv, s') \ mres (f s). Q rv s')" text \The above for the exception monad\ @@ -86,7 +87,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_Total.thy b/lib/Monads/trace/Trace_Total.thy index 1c08d8460c..ea86da1600 100644 --- a/lib/Monads/trace/Trace_Total.thy +++ b/lib/Monads/trace/Trace_Total.thy @@ -20,7 +20,8 @@ text \ is often similar. The following definitions allow such reasoning to take place.\ definition validNF :: - "('s \ bool) \ ('s,'a) tmonad \ ('a \ 's \ bool) \ bool" ("\_\/ _ /\_\!") where + "('s \ bool) \ ('s,'a) tmonad \ ('a \ 's \ bool) \ bool" + ("\_\/ _ /\_\!") where "\P\ f \Q\! \ \P\ f \Q\ \ no_fail P f" lemma validNF_alt_def: @@ -304,7 +305,8 @@ lemma validNF_nobindE[wp]: text \ Set up triple rules for @{term validE_NF} so that we can use @{method wp} combinator rules.\ definition validE_NF_property :: - "('a \ 's \ bool) \ ('c \ 's \ bool) \ 's \ ('s, 'c+'a) tmonad \ bool" where + "('a \ 's \ bool) \ ('c \ 's \ bool) \ 's \ ('s, 'c+'a) tmonad \ bool" + where "validE_NF_property Q E s b \ Failed \ snd ` (b s) \ (\(r', s') \ mres (b s). case r' of Inl x \ E x s' | Inr x \ Q x s')" diff --git a/lib/Monads/trace/Trace_VCG.thy b/lib/Monads/trace/Trace_VCG.thy index dd0a2f57a8..f3fca936c0 100644 --- a/lib/Monads/trace/Trace_VCG.thy +++ b/lib/Monads/trace/Trace_VCG.thy @@ -34,15 +34,15 @@ text \ @{term "assert P"} does not require us to prove that @{term P} holds, but rather allows us to assume @{term P}! Proving non-failure is done via a separate predicate and calculus (see Trace_No_Fail).\ -definition valid :: "('s \ bool) \ ('s,'a) tmonad \ ('a \ 's \ bool) \ bool" +definition valid :: + "('s \ bool) \ ('s,'a) tmonad \ ('a \ 's \ bool) \ bool" ("\_\/ _ /\_\") where "\P\ f \Q\ \ \s. P s \ (\(r,s') \ mres (f s). Q r s')" text \ We often reason about invariant predicates. The following provides shorthand syntax that avoids repeating potentially long predicates.\ -abbreviation (input) invariant :: - "('s,'a) tmonad \ ('s \ bool) \ bool" ("_ \_\" [59,0] 60) where +abbreviation (input) invariant :: "('s,'a) tmonad \ ('s \ bool) \ bool" ("_ \_\" [59,0] 60) where "invariant f P \ \P\ f \\_. P\" text \ @@ -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