diff --git a/lib/Crunch_Instances_Trace.thy b/lib/Crunch_Instances_Trace.thy index e7966c63b8..bf8acb44b1 100644 --- a/lib/Crunch_Instances_Trace.thy +++ b/lib/Crunch_Instances_Trace.thy @@ -7,7 +7,8 @@ theory Crunch_Instances_Trace imports Crunch - Monads.Trace_VCG + Monads.Trace_No_Fail + Monads.Trace_RG begin lemmas [crunch_param_rules] = Let_def return_bind returnOk_bindE diff --git a/lib/Monads/ROOT b/lib/Monads/ROOT index 5cfb076f10..5fe32ad49e 100644 --- a/lib/Monads/ROOT +++ b/lib/Monads/ROOT @@ -48,6 +48,7 @@ session Monads (lib) = HOL + Trace_Monad Trace_Lemmas Trace_VCG + Trace_Det Strengthen Nondet_Strengthen_Setup Strengthen_Demo diff --git a/lib/Monads/trace/Trace_Det.thy b/lib/Monads/trace/Trace_Det.thy new file mode 100644 index 0000000000..4b17f18dbf --- /dev/null +++ b/lib/Monads/trace/Trace_Det.thy @@ -0,0 +1,75 @@ +(* + * Copyright 2023, Proofcraft Pty Ltd + * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) + * + * SPDX-License-Identifier: BSD-2-Clause + *) + +theory Trace_Det + imports + Trace_Monad +begin + +subsection "Determinism" + +text \ + A monad of type @{text tmonad} is deterministic iff it + returns an empty trace, exactly one state and result and does not fail\ +definition det :: "('a,'s) tmonad \ bool" where + "det f \ \s. \r. f s = {([], Result r)}" + +text \A deterministic @{text tmonad} can be turned into a normal state monad:\ +definition the_run_state :: "('s,'a) tmonad \ 's \ 'a \ 's" where + "the_run_state M \ \s. THE s'. mres (M s) = {s'}" + + +lemma det_set_iff: + "det f \ (r \ mres (f s)) = (mres (f s) = {r})" + unfolding det_def mres_def + by (fastforce elim: allE[where x=s]) + +lemma return_det[iff]: + "det (return x)" + by (simp add: det_def return_def) + +lemma put_det[iff]: + "det (put s)" + by (simp add: det_def put_def) + +lemma get_det[iff]: + "det get" + by (simp add: det_def get_def) + +lemma det_gets[iff]: + "det (gets f)" + by (auto simp add: gets_def det_def get_def return_def bind_def) + +lemma det_UN: + "det f \ (\x \ mres (f s). g x) = (g (THE x. x \ mres (f s)))" + unfolding det_def mres_def + apply simp + apply (drule spec [of _ s]) + apply (clarsimp simp: vimage_def) + done + +lemma bind_detI[simp, intro!]: + "\ det f; \x. det (g x) \ \ det (f >>= g)" + unfolding bind_def det_def + apply clarsimp + apply (erule_tac x=s in allE) + apply clarsimp + done + +lemma det_modify[iff]: + "det (modify f)" + by (simp add: modify_def) + +lemma the_run_stateI: + "mres (M s) = {s'} \ the_run_state M s = s'" + by (simp add: the_run_state_def) + +lemma the_run_state_det: + "\ s' \ mres (M s); det M \ \ the_run_state M s = s'" + by (simp add: the_run_stateI det_set_iff) + +end diff --git a/lib/Monads/trace/Trace_In_Monad.thy b/lib/Monads/trace/Trace_In_Monad.thy new file mode 100644 index 0000000000..073d4096be --- /dev/null +++ b/lib/Monads/trace/Trace_In_Monad.thy @@ -0,0 +1,137 @@ +(* + * Copyright 2023, Proofcraft Pty Ltd + * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) + * + * SPDX-License-Identifier: BSD-2-Clause + *) + +theory Trace_In_Monad + imports Trace_Lemmas +begin + +section \Reasoning directly about states\ + +(* Lemmas about terms of the form "(v, s') \ mres (m s)" *) + +lemma in_throwError: + "((v, s') \ mres (throwError e s)) = (v = Inl e \ s' = s)" + by (simp add: throwError_def return_def mres_def) + +lemma in_returnOk: + "((v', s') \ mres (returnOk v s)) = (v' = Inr v \ s' = s)" + by (simp add: returnOk_def return_def mres_def) + +lemma in_bind: + "((r,s') \ mres ((do x \ f; g x od) s)) = + (\s'' x. (x, s'') \ mres (f s) \ (r, s') \ mres (g x s''))" + by (force simp: bind_def split_def mres_def split: tmres.splits) + +lemma in_bindE_R: + "((Inr r,s') \ mres ((doE x \ f; g x odE) s)) = + (\s'' x. (Inr x, s'') \ mres (f s) \ (Inr r, s') \ mres (g x s''))" + unfolding bindE_def lift_def split_def in_bind + by (force simp: throwError_def return_def mres_def split: sum.splits) + +lemma in_bindE_L: + "((Inl r, s') \ mres ((doE x \ f; g x odE) s)) \ + (\s'' x. (Inr x, s'') \ mres (f s) \ (Inl r, s') \ mres (g x s'')) \ ((Inl r, s') \ mres (f s))" + by (simp add: bindE_def in_bind) + (force simp: return_def throwError_def lift_def split_def mres_def split: sum.splits if_split_asm) + +lemma in_return: + "(r, s') \ mres (return v s) = (r = v \ s' = s)" + by (simp add: return_def mres_def) + +lemma in_liftE: + "((v, s') \ mres (liftE f s)) = (\v'. v = Inr v' \ (v', s') \ mres (f s))" + by (force simp: liftE_def in_bind in_return) + +lemma in_whenE: + "((v, s') \ mres (whenE P f s)) = ((P \ (v, s') \ mres (f s)) \ (\P \ v = Inr () \ s' = s))" + by (simp add: whenE_def in_returnOk) + +lemma inl_whenE: + "((Inl x, s') \ mres (whenE P f s)) = (P \ (Inl x, s') \ mres (f s))" + by (auto simp add: in_whenE) + +lemma in_fail: + "r \ mres (fail s) = False" + by (simp add: fail_def mres_def) + +lemma in_assert: + "(r, s') \ mres (assert P s) = (P \ s' = s)" + by (simp add: assert_def return_def fail_def mres_def) + +lemma in_assertE: + "(r, s') \ mres (assertE P s) = (P \ r = Inr () \ s' = s)" + by (simp add: assertE_def returnOk_def return_def fail_def mres_def) + +lemma in_assert_opt: + "(r, s') \ mres (assert_opt v s) = (v = Some r \ s' = s)" + by (auto simp: assert_opt_def in_fail in_return split: option.splits) + +lemma in_get: + "(r, s') \ mres (get s) = (r = s \ s' = s)" + by (simp add: get_def mres_def) + +lemma in_gets: + "(r, s') \ mres (gets f s) = (r = f s \ s' = s)" + by (simp add: simpler_gets_def mres_def) + +lemma in_put: + "(r, s') \ mres (put x s) = (s' = x \ r = ())" + by (simp add: put_def mres_def) + +lemma in_when: + "(v, s') \ mres (when P f s) = ((P \ (v, s') \ mres (f s)) \ (\P \ v = () \ s' = s))" + by (simp add: when_def in_return) + +lemma in_modify: + "(v, s') \ mres (modify f s) = (s'=f s \ v = ())" + by (auto simp add: modify_def bind_def get_def put_def mres_def) + +lemma gets_the_in_monad: + "((v, s') \ mres (gets_the f s)) = (s' = s \ f s = Some v)" + by (auto simp: gets_the_def in_bind in_gets in_assert_opt split: option.split) + +lemma in_alternative: + "(r,s') \ mres ((f \ g) s) = ((r,s') \ mres (f s) \ (r,s') \ mres (g s))" + by (auto simp add: alternative_def mres_def) + +lemma in_liftM: + "((r, s') \ mres (liftM t f s)) = (\r'. (r', s') \ mres (f s) \ r = t r')" + by (simp add: liftM_def in_return in_bind) + +lemma in_bindE: + "(rv, s') \ mres ((f >>=E (\rv'. g rv')) s) = + ((\ex. rv = Inl ex \ (Inl ex, s') \ mres (f s)) \ + (\rv' s''. (rv, s') \ mres (g rv' s'') \ (Inr rv', s'') \ mres (f s)))" + apply (clarsimp simp: bindE_def in_bind lift_def in_throwError) + apply (safe del: disjCI; strengthen subst[where P="\x. x \ mres (f s)", mk_strg I _ E]; + auto simp: in_throwError split: sum.splits) + done + +lemmas in_monad = inl_whenE in_whenE in_liftE in_bind in_bindE_L + in_bindE_R in_returnOk in_throwError in_fail + in_assertE in_assert in_return in_assert_opt + in_get in_gets in_put in_when (* unlessE_whenE *) + (* unless_when *) in_modify gets_the_in_monad + in_alternative in_liftM + +lemma bind_det_exec: + "mres (a s) = {(r,s')} \ mres ((a >>= b) s) = mres (b r s')" + by (simp add: in_bind set_eq_iff) + +lemma in_bind_det_exec: + "mres (a s) = {(r,s')} \ (s'' \ mres ((a >>= b) s)) = (s'' \ mres (b r s'))" + by (cases s'', simp add: in_bind) + +lemma exec_put: + "(put s' >>= m) s = m () s'" + by (simp add: bind_def put_def mres_def split_def) + +lemma bind_execI: + "\ (r'',s'') \ mres (f s); \x \ mres (g r'' s''). P x \ \ \x \ mres ((f >>= g) s). P x" + by (force simp: Bex_def in_bind) + +end diff --git a/lib/Monads/trace/Trace_Lemmas.thy b/lib/Monads/trace/Trace_Lemmas.thy index 6b5533d811..9ce793eea7 100644 --- a/lib/Monads/trace/Trace_Lemmas.thy +++ b/lib/Monads/trace/Trace_Lemmas.thy @@ -1,379 +1,89 @@ (* + * Copyright 2023, Proofcraft Pty Ltd * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) * * SPDX-License-Identifier: BSD-2-Clause *) + theory Trace_Lemmas -imports Trace_VCG + imports Trace_Monad begin -lemma mapM_Cons: - "mapM f (x # xs) = do - y \ f x; - ys \ mapM f xs; - return (y # ys) - od" - and mapM_Nil: - "mapM f [] = return []" - by (simp_all add: mapM_def sequence_def) - -lemma mapM_x_Cons: - "mapM_x f (x # xs) = do - y \ f x; - mapM_x f xs - od" - and mapM_x_Nil: - "mapM_x f [] = return ()" - by (simp_all add: mapM_x_def sequence_x_def) - -lemma mapM_append: - "mapM f (xs @ ys) = (do - fxs \ mapM f xs; - fys \ mapM f ys; - return (fxs @ fys) - od)" - by (induct xs, simp_all add: mapM_Cons mapM_Nil bind_assoc) - -lemma mapM_x_append: - "mapM_x f (xs @ ys) = (do - x \ mapM_x f xs; - mapM_x f ys - od)" - by (induct xs, simp_all add: mapM_x_Cons mapM_x_Nil bind_assoc) - -lemma mapM_map: - "mapM f (map g xs) = mapM (f o g) xs" - by (induct xs; simp add: mapM_Nil mapM_Cons) - -lemma mapM_x_map: - "mapM_x f (map g xs) = mapM_x (f o g) xs" - by (induct xs; simp add: mapM_x_Nil mapM_x_Cons) - -primrec - repeat_n :: "nat \ ('s, unit) tmonad \ ('s, unit) tmonad" -where - "repeat_n 0 f = return ()" - | "repeat_n (Suc n) f = do f; repeat_n n f od" - -lemma repeat_n_mapM_x: - "repeat_n n f = mapM_x (\_. f) (replicate n ())" - by (induct n, simp_all add: mapM_x_Cons mapM_x_Nil) - -definition - repeat :: "('s, unit) tmonad \ ('s, unit) tmonad" -where - "repeat f = do n \ select UNIV; repeat_n n f od" - -definition - env_step :: "('s,unit) tmonad" -where - "env_step = - (do - s' \ select UNIV; - put_trace_elem (Env, s'); - put s' - od)" - -abbreviation - "env_n_steps n \ repeat_n n env_step" - -lemma elem_select_bind: - "(tr, res) \ (do x \ select S; f x od) s - = (\x \ S. (tr, res) \ f x s)" - by (simp add: bind_def select_def) - -lemma select_bind_UN: - "(do x \ select S; f x od) = (\s. \x \ S. f x s)" - by (rule ext, auto simp: elem_select_bind) - -lemma select_early: - "S \ {} - \ do x \ f; y \ select S; g x y od - = do y \ select S; x \ f; g x y od" - apply (simp add: bind_def select_def Sigma_def) - apply (rule ext) - apply (fastforce elim: rev_bexI image_eqI[rotated] split: tmres.split_asm) - done - -lemma repeat_n_choice: - "S \ {} - \ repeat_n n (do x \ select S; f x od) - = (do xs \ select {xs. set xs \ S \ length xs = n}; mapM_x f xs od)" - apply (induct n; simp?) - apply (simp add: select_def bind_def mapM_x_Nil cong: conj_cong) - apply (simp add: select_early bind_assoc) - apply (subst select_early) - apply simp - apply (auto intro: exI[where x="replicate n xs" for n xs])[1] - apply (simp(no_asm) add: fun_eq_iff set_eq_iff elem_select_bind) - apply (simp only: conj_comms[where Q="length xs = n" for xs n]) - apply (simp only: ex_simps[symmetric] conj_assoc length_Suc_conv, simp) - apply (auto simp: mapM_x_Cons) - done - -lemma repeat_choice: - "S \ {} - \ repeat (do x \ select S; f x od) - = (do xs \ select {xs. set xs \ S}; mapM_x f xs od)" - apply (simp add: repeat_def repeat_n_choice) - apply (simp(no_asm) add: fun_eq_iff set_eq_iff elem_select_bind) - done - -lemma put_trace_append: - "put_trace (xs @ ys) = do put_trace ys; put_trace xs od" - by (induct xs; simp add: bind_assoc) - -lemma put_trace_elem_put_comm: - "do y \ put_trace_elem x; put s od - = do y \ put s; put_trace_elem x od" - by (simp add: put_def put_trace_elem_def bind_def insert_commute) - -lemma put_trace_put_comm: - "do y \ put_trace xs; put s od - = do y \ put s; put_trace xs od" - apply (rule sym; induct xs; simp) - apply (simp add: bind_assoc put_trace_elem_put_comm) - apply (simp add: bind_assoc[symmetric]) - done - -lemma mapM_x_comm: - "(\x \ set xs. do y \ g; f x od = do y \ f x; g od) - \ do y \ g; mapM_x f xs od = do y \ mapM_x f xs; g od" - apply (induct xs; simp add: mapM_x_Nil mapM_x_Cons) - apply (simp add: bind_assoc[symmetric], simp add: bind_assoc) - done - -lemma mapM_x_split: - "(\x \ set xs. \y \ set xs. do z \ g y; f x od = do (z :: unit) \ f x; g y od) - \ mapM_x (\x. do z \ f x; g x od) xs = do y \ mapM_x f xs; mapM_x g xs od" - apply (induct xs; simp add: mapM_x_Nil mapM_x_Cons bind_assoc) - apply (subst bind_assoc[symmetric], subst mapM_x_comm[where f=f and g="g x" for x]) - apply simp - apply (simp add: bind_assoc) - done - -lemma mapM_x_put: - "mapM_x put xs = unless (xs = []) (put (last xs))" - apply (induct xs rule: rev_induct) - apply (simp add: mapM_x_Nil unless_def when_def) - apply (simp add: mapM_x_append mapM_x_Cons mapM_x_Nil) - apply (simp add: bind_def unless_def when_def put_def return_def) - done - -lemma put_trace_mapM_x: - "put_trace xs = mapM_x put_trace_elem (rev xs)" - by (induct xs; simp add: mapM_x_Nil mapM_x_append mapM_x_Cons) +section \General Lemmas Regarding the Interference Trace Monad\ -lemma rev_surj: - "surj rev" - by (rule_tac f=rev in surjI, simp) +subsection \Congruence Rules for the Function Package\ -lemma select_image: - "select (f ` S) = do x \ select S; return (f x) od" - by (auto simp add: bind_def select_def return_def Sigma_def) +\ \FIXME: where should this go\ +lemma in_mres: + "(tr, Result (rv, s)) \ S \ (rv, s) \ mres S" + by (fastforce simp: mres_def intro: image_eqI[rotated]) -lemma env_steps_repeat: - "env_steps = repeat env_step" - apply (simp add: env_step_def repeat_choice env_steps_def - select_early) - apply (simp add: put_trace_elem_put_comm) - apply (simp add: mapM_x_split put_trace_elem_put_comm put_trace_put_comm - mapM_x_put) - apply (simp add: put_trace_mapM_x rev_map mapM_x_map o_def) - apply (subst rev_surj[symmetric], simp add: select_image bind_assoc) - apply (rule arg_cong2[where f=bind, OF refl ext]) - apply (simp add: bind_def get_def put_def unless_def when_def return_def) - apply (simp add: last_st_tr_def hd_map hd_rev) - done - -lemma repeat_n_plus: - "repeat_n (n + m) f = do repeat_n n f; repeat_n m f od" - by (induct n; simp add: bind_assoc) - -lemma repeat_eq_twice[simp]: - "(do x \ repeat f; repeat f od) = repeat f" - apply (simp add: repeat_def select_early) - apply (simp add: bind_assoc repeat_n_plus[symmetric, simplified]) - apply (simp add: bind_def select_def Sigma_def) - apply (rule ext, fastforce intro: exI[where x=0]) - done - -lemmas bind_then_eq = arg_cong2[where f=bind, OF _ refl] -lemmas repeat_eq_twice_then[simp] - = repeat_eq_twice[THEN bind_then_eq, simplified bind_assoc] - -lemmas env_steps_eq_twice[simp] - = repeat_eq_twice[where f=env_step, folded env_steps_repeat] -lemmas env_steps_eq_twice_then[simp] - = env_steps_eq_twice[THEN bind_then_eq, simplified bind_assoc] - -lemmas mapM_collapse_append = mapM_append[symmetric, THEN bind_then_eq, - simplified bind_assoc, simplified] - -lemma prefix_closed_mapM[rule_format, wp_split]: - "(\x \ set xs. prefix_closed (f x)) \ prefix_closed (mapM f xs)" - apply (induct xs) - apply (simp add: mapM_def sequence_def) - apply (clarsimp simp: mapM_Cons) - apply (intro prefix_closed_bind allI; clarsimp) +lemma bind_apply_cong': + "\f s = f' s'; (\rv st. (rv, st) \ mres (f s) \ g rv st = g' rv st)\ + \ bind f g s = bind f' g' s'" + apply (simp add: bind_def) + apply (rule SUP_cong; simp?) + apply (clarsimp split: tmres.split) + apply (drule spec2, drule mp, erule in_mres) + apply simp done -lemma modify_id: - "modify id = return ()" - by (simp add: modify_def get_def bind_def put_def return_def) +lemmas bind_apply_cong = bind_apply_cong'[rule_format, fundef_cong] -lemma modify_modify: - "(do x \ modify f; modify (g x) od) = modify (g () o f)" - by (simp add: bind_def simpler_modify_def) -lemmas modify_modify_bind = arg_cong2[where f=bind, - OF modify_modify refl, simplified bind_assoc] +subsection \Simplifying Monads\ -lemma select_single: - "select {x} = return x" - by (simp add: select_def return_def) +lemma fail_update[iff]: + "fail (f s) = fail s" + by (simp add: fail_def) -lemma put_then_get[unfolded K_bind_def]: - "do put s; get od = do put s; return s od" - by (simp add: put_def bind_def get_def return_def) +lemma assert_A_True[simp]: + "assert True = return ()" + by (simp add: assert_def) -lemmas put_then_get_then - = put_then_get[THEN bind_then_eq, simplified bind_assoc return_bind] -lemmas bind_promote_If - = if_distrib[where f="\f. bind f g" for g] - if_distrib[where f="\g. bind f g" for f] +subsection \Lifting and Alternative Basic Definitions\ -lemma bind_promote_If2: - "do x \ f; if P then g x else h x od - = (if P then bind f g else bind f h)" - by simp +lemma liftE_liftM: + "liftE = liftM Inr" + by (auto simp: liftE_def liftM_def) -lemma exec_put_trace[unfolded K_bind_def]: - "(do put_trace xs; f od) s - = (\n \ {n. 0 < n \ n \ length xs}. {(drop n xs, Incomplete)}) - \ ((\(a, b). (a @ xs, b)) ` f s)" - apply (simp add: put_trace_eq_drop bind_def) - apply (safe; (clarsimp split: if_split_asm)?; - fastforce intro: bexI[where x=0] rev_bexI) +lemma liftME_liftM: + "liftME f = liftM (case_sum Inl (Inr \ f))" + unfolding liftME_def liftM_def bindE_def returnOk_def lift_def + apply (rule ext, rename_tac x) + apply (rule_tac f="bind x" in arg_cong) + apply (fastforce simp: throwError_def split: sum.splits) done -lemma if_fun_lift: - "(if P then f else g) x = (if P then f x else g x)" - by simp +lemma liftE_bindE: + "liftE a >>=E b = a >>= b" + by (simp add: liftE_def bindE_def lift_def bind_assoc) -lemma UN_If_distrib: - "(\x \ S. if P x then A x else B x) - = ((\x \ S \ {x. P x}. A x) \ (\x \ S \ {x. \ P x}. B x))" - by (fastforce split: if_split_asm) +lemma liftM_id[simp]: + "liftM id = id" + by (auto simp: liftM_def) -lemma Await_redef: - "Await P = do - s1 \ select {s. P s}; - env_steps; - s \ get; - select (if P s then {()} else {}) - od" - apply (simp add: Await_def env_steps_def bind_assoc) - apply (cases "{s. P s} = {}") - apply (simp add: select_def bind_def get_def) - apply (rule ext) - apply (simp add: exec_get select_bind_UN put_then_get_then) - apply (simp add: bind_promote_If2 if_fun_lift if_distrib[where f=select]) - apply (simp add: exec_put_trace cong: if_cong) - apply (simp add: put_def bind_def select_def cong: if_cong) - apply (strengthen equalityI) - apply clarsimp - apply (strengthen exI[where x="s # xs" for s xs]) - apply (strengthen exI[where x="Suc n" for n]) - apply simp - apply blast - done - -lemma bind_apply_cong': - "f s = f' s - \ (\rv s'. (rv, s') \ mres (f s) \ g rv s' = g' rv s') - \ bind f g s = bind f' g' s" - apply (simp add: bind_def) - apply (rule SUP_cong; simp?) - apply (clarsimp split: tmres.split) - apply (drule spec2, drule mp, erule in_mres) - apply simp - done +lemma liftM_bind: + "liftM t f >>= g = (f >>= (\x. g (t x)))" + by (simp add: liftM_def bind_assoc) -lemmas bind_apply_cong = bind_apply_cong'[rule_format] +lemma gets_bind_ign: + "gets f >>= (\x. m) = m" + by (simp add: bind_def simpler_gets_def) -lemma select_empty_bind[simp]: - "select {} >>= f = select {}" - by (simp add: select_def bind_def) +lemma exec_get: + "(get >>= f) x = f x x" + by (simp add: get_def bind_def) -lemma fail_bind[simp]: - "fail >>= f = fail" - by (simp add: bind_def fail_def) +lemmas get_bind_apply = exec_get (* FIXME lib: eliminate *) -lemma eq_Me_neq_Env: - "(x = Me) = (x \ Env)" - by (cases x; simp) +lemma exec_gets: + "(gets f >>= m) s = m (f s) s" + by (simp add: simpler_gets_def bind_def) -lemma validI_invariant_imp: - assumes v: "\P\,\R\ f \G\,\Q\" - and P: "\s0 s. P s0 s \ I s0" - and R: "\s0 s. I s0 \ R s0 s \ I s" - and G: "\s0 s. I s0 \ G s0 s \ I s" - shows "\P\,\R\ f \\s0 s. I s0 \ I s \ G s0 s\,\\rv s0 s. I s0 \ Q rv s0 s\" -proof - - { fix tr s0 i - assume r: "rely_cond R s0 tr" and g: "guar_cond G s0 tr" - and I: "I s0" - hence imp: "\(_, s, s') \ trace_steps (rev tr) s0. I s \ I s'" - apply (clarsimp simp: guar_cond_def rely_cond_def) - apply (drule(1) bspec)+ - apply (clarsimp simp: eq_Me_neq_Env) - apply (metis R G) - done - hence "i < length tr \ I (snd (rev tr ! i))" - using I - apply (induct i) - apply (clarsimp simp: neq_Nil_conv[where xs="rev tr" for tr, simplified]) - apply clarsimp - apply (drule bspec, fastforce simp add: trace_steps_nth) - apply simp - done - } - note I = this - show ?thesis - using v - apply (clarsimp simp: validI_def rely_def imp_conjL) - apply (drule spec2, drule(1) mp)+ - apply clarsimp - apply (frule P[rule_format]) - apply (clarsimp simp: guar_cond_def trace_steps_nth I last_st_tr_def - hd_append last_rev[symmetric] - last_conv_nth rev_map) - done -qed - -lemma validI_guar_post_conj_lift: - "\P\,\R\ f \G1\,\Q1\ - \ \P\,\R\ f \G2\,\Q2\ - \ \P\,\R\ f \\s0 s. G1 s0 s \ G2 s0 s\,\\rv s0 s. Q1 rv s0 s \ Q2 rv s0 s\" - apply (frule validI_prefix_closed) - apply (subst validI_def, clarsimp simp: rely_def) - apply (drule(3) validI_D)+ - apply (auto simp: guar_cond_def) - done - -lemmas modify_prefix_closed[simp] = - modify_wp[THEN valid_validI_wp[OF no_trace_all(3)], THEN validI_prefix_closed] -lemmas await_prefix_closed[simp] = Await_sync_twp[THEN validI_prefix_closed] - -lemma repeat_prefix_closed[intro!]: - "prefix_closed f \ prefix_closed (repeat f)" - apply (simp add: repeat_def) - apply (rule prefix_closed_bind; clarsimp) - apply (rename_tac n) - apply (induct_tac n; simp) - apply (auto intro: prefix_closed_bind) - done +lemma bind_eqI: + "\ f = f'; \x. g x = g' x \ \ f >>= g = f' >>= g'" + by (auto simp: bind_def split_def) end diff --git a/lib/Monads/trace/Trace_Monad.thy b/lib/Monads/trace/Trace_Monad.thy index 506f8954ca..8ddf802f4d 100644 --- a/lib/Monads/trace/Trace_Monad.thy +++ b/lib/Monads/trace/Trace_Monad.thy @@ -1,62 +1,60 @@ (* + * Copyright 2023, Proofcraft Pty Ltd * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) * * SPDX-License-Identifier: BSD-2-Clause *) + +chapter "Interference Trace Monad" + theory Trace_Monad -imports - Monad_Lib - Strengthen + imports + Fun_Pred_Syntax + Monad_Lib + Strengthen begin text \ -The ``Interference Trace Monad''. This nondeterministic monad -records the state at every interference point, permitting -nondeterministic interference by the environment at interference -points. - -The trace set initially includes all possible environment behaviours. -Trace steps are tagged as environment or self actions, and can then -be constrained to a smaller set where the environment acts according -to a rely constraint (i.e. rely-guarantee reasoning), or to set the -environment actions to be the self actions of another program (parallel -composition). -\ + The ``Interference Trace Monad''. This nondeterministic monad + records the state at every interference point, permitting + nondeterministic interference by the environment at these points. + + The trace set initially includes all possible environment behaviours. + Trace steps are tagged as environment or self actions, and can then + be constrained to a smaller set where the environment acts according + to a rely constraint (i.e. rely-guarantee reasoning), or to set the + environment actions to be the self actions of another program (parallel + composition).\ section "The Trace Monad" text \Trace monad identifier. Me corresponds to the current thread running and Env to the environment.\ datatype tmid = Me | Env -text \Results associated with traces. Traces may correspond to incomplete, failed, or completed executions.\ +text \ + Results associated with traces. Traces may correspond to incomplete, failed, or completed executions.\ datatype ('s, 'a) tmres = Failed | Incomplete | Result "('a \ 's)" -abbreviation - map_tmres_rv :: "('a \ 'b) \ ('s, 'a) tmres \ ('s, 'b) tmres" -where +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 +text \ + tmonad returns a set of non-deterministic computations, including a trace as a list of "thread identifier" \ state, and an optional - pair result, state when the computation did not fail. \ + 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 \Returns monad results, ignoring failures and traces.\ -definition - mres :: "((tmid \ 's) list \ ('s, 'a) tmres) set \ ('a \ 's) set" -where +definition mres :: "((tmid \ 's) list \ ('s, 'a) tmres) set \ ('a \ 's) set" where "mres r = Result -` (snd ` r)" text \ The definition of fundamental monad functions @{text return} and @{text bind}. The monad function @{text "return x"} does not change - the state, does not fail, and returns @{text "x"}. -\ -definition - return :: "'a \ ('s,'a) tmonad" -where + the state, does not fail, and returns @{text "x"}.\ +definition return :: "'a \ ('s,'a) tmonad" where "return a \ \s. ({([], Result (a, s))})" text \ @@ -67,58 +65,43 @@ text \ the combined operation is the union of the set of sets that is created by @{text g} applied to the result sets of @{text f}. The combined operation may have failed, if @{text f} may have failed or @{text g} may - have failed on any of the results of @{text f}. -\ - -abbreviation (input) - fst_upd :: "('a \ 'c) \ 'a \ 'b \ 'c \ 'b" -where + have failed on any of the results of @{text f}.\ +abbreviation (input) fst_upd :: "('a \ 'c) \ 'a \ 'b \ 'c \ 'b" where "fst_upd f \ \(a,b). (f a, b)" -abbreviation (input) - snd_upd :: "('b \ 'c) \ 'a \ 'b \ 'a \ 'c" -where +abbreviation (input) snd_upd :: "('b \ 'c) \ 'a \ 'b \ 'a \ 'c" where "snd_upd f \ \(a,b). (a, f b)" -definition - bind :: "('s, 'a) tmonad \ ('a \ ('s, 'b) tmonad) \ - ('s, 'b) tmonad" (infixl ">>=" 60) -where +definition bind :: + "('s, 'a) tmonad \ ('a \ ('s, 'b) tmonad) \ ('s, 'b) tmonad" (infixl ">>=" 60) + where "bind f g \ \s. \(xs, r) \ (f s). case r of Failed \ {(xs, Failed)} | Incomplete \ {(xs, Incomplete)} | 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 \ - The basic accessor functions of the state monad. @{text get} returns - the current state as result, does not fail, and does not change the state. - @{text "put s"} returns nothing (@{typ unit}), changes the current state - to @{text s} and does not fail. -\ -definition - get :: "('s,'s) tmonad" -where + The basic accessor functions of the state monad. @{text get} returns the + current state as result, does not change the state, and does not add to the + trace. @{text "put s"} returns nothing (@{typ unit}), changes the current + state to @{text s}, and does not add to the trace. @{text "put_trace xs"} + returns nothing (@{typ unit}), does not change the state, and adds @{text xs} + to the trace.\ +definition get :: "('s,'s) tmonad" where "get \ \s. {([], Result (s, s))}" -definition - put :: "'s \ ('s, unit) tmonad" -where - "put s \ \st. {([], Result ((), s))}" +definition put :: "'s \ ('s, unit) tmonad" where + "put s \ \_. {([], Result ((), s))}" -definition - put_trace_elem :: "(tmid \ 's) \ ('s, unit) tmonad" -where +definition put_trace_elem :: "(tmid \ 's) \ ('s, unit) tmonad" where "put_trace_elem x = (\s. {([], Incomplete), ([x], Result ((), s))})" -primrec - put_trace :: "(tmid \ 's) list \ ('s, unit) tmonad" -where +primrec put_trace :: "(tmid \ 's) list \ ('s, unit) tmonad" where "put_trace [] = return ()" | "put_trace (x # xs) = (put_trace xs >>= (\_. put_trace_elem x))" @@ -126,157 +109,122 @@ subsection "Nondeterminism" text \ Basic nondeterministic functions. @{text "select A"} chooses an element - of the set @{text A}, does not change the state, and does not fail - (even if the set is empty). @{text "f \ g"} executes @{text f} or - executes @{text g}. It retuns the union of results of @{text f} and - @{text g}, and may have failed if either may have failed. -\ -definition - select :: "'a set \ ('s, 'a) tmonad" -where - (* Should we have Failed when A = {} ? *) + of the set @{text A} as the result, does not change the state, does not add + to the trace, and does not fail (even if the set is empty). @{text "f \ g"} + executes @{text f} or executes @{text g}. It returns the union of results and + traces of @{text f} and @{text g}.\ +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 \ The @{text selet_f} function was left out here until we figure - out what variant we actually need. -\ +text \ + FIXME: The @{text select_f} function was left out here until we figure + out what variant we actually need.\ subsection "Failure" -text \ The monad function that always fails. Returns an empty set of -results and sets the failure flag. \ -definition - fail :: "('s, 'a) tmonad" -where - "fail \ \s. {([], Failed)}" - -text \ Assertions: fail if the property @{text P} is not true \ -definition - assert :: "bool \ ('a, unit) tmonad" -where - "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) tmonad" -where - "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) tmonad" -where +text \ + The monad function that always fails. Returns an empty trace with a Failed result.\ +definition fail :: "('s, 'a) tmonad" where + "fail \ \s. {([], Failed)}" + +text \Assertions: fail if the property @{text P} is not true\ +definition assert :: "bool \ ('a, unit) tmonad" where + "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) tmonad" where + "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) tmonad" where "state_assert P \ get >>= (\s. assert (P s))" 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) tmonad" -where - "gets f \ get >>= (\s. return (f s))" - -text \ Modify the current state using the function passed in. \ -definition - modify :: "('s \ 's) \ ('s, unit) tmonad" -where +text \Apply a function to the current state and return the result without changing the state.\ +definition gets :: "('s \ 'a) \ ('s, 'a) tmonad" where + "gets f \ get >>= (\s. return (f s))" + +text \Modify the current state using the function passed in.\ +definition modify :: "('s \ 's) \ ('s, unit) tmonad" where "modify f \ get >>= (\s. put (f s))" -lemma simpler_gets_def: "gets f = (\s. {([], Result ((f s), s))})" - by (simp add: fun_eq_iff gets_def return_def bind_def get_def split_def) +lemma simpler_gets_def: + "gets f = (\s. {([], Result ((f s), s))})" + by (simp add: gets_def return_def bind_def get_def) lemma simpler_modify_def: "modify f = (\s. {([], Result ((),(f s)))})" - by (simp add: fun_eq_iff modify_def bind_def get_def put_def split_def) - -text \ Execute the given monad when the condition is true, - return @{text "()"} otherwise. \ -definition - "when" :: "bool \ ('s, unit) tmonad \ - ('s, unit) tmonad" -where + by (simp add: modify_def bind_def get_def put_def) + +text \Execute the given monad when the condition is true, return @{text "()"} otherwise.\ +definition "when" :: "bool \ ('s, unit) tmonad \ ('s, unit) tmonad" where "when P m \ if P then m else return ()" -text \ Execute the given monad unless the condition is true, - return @{text "()"} otherwise. \ -definition - unless :: "bool \ ('s, unit) tmonad \ - ('s, unit) tmonad" -where +text \Execute the given monad unless the condition is true, return @{text "()"} otherwise.\ +definition unless :: "bool \ ('s, unit) tmonad \ ('s, unit) tmonad" where "unless P m \ when (\P) m" 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 + 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 "condition P L R \ \s. if (P s) then (L s) else (R s)" notation (output) condition ("(condition (_)// (_)// (_))" [1000,1000,1000] 1000) text \ -Apply an option valued function to the current state, fail -if it returns @{const None}, return @{text v} if it returns -@{term "Some v"}. -\ -definition - gets_the :: "('s \ 'a option) \ ('s, 'a) tmonad" -where + Apply an option valued function to the current state, fail if it returns @{const None}, + return @{text v} if it returns @{term "Some v"}.\ +definition gets_the :: "('s \ 'a option) \ ('s, 'a) tmonad" where "gets_the f \ gets f >>= assert_opt" -subsection \ The Monad Laws \ +subsection \The Monad Laws\ text \An alternative definition of bind, sometimes more convenient.\ lemma bind_def2: - "bind f g \ (\s. ((\xs. (xs, Failed)) ` {xs. (xs, Failed) \ f s}) - \ ((\xs. (xs, Incomplete)) ` {xs. (xs, Incomplete) \ f s}) - \ (\(xs, rv, s) \ {(xs, rv, s'). (xs, Result (rv, s')) \ f s}. fst_upd (\ys. ys @ xs) ` g rv s))" + "bind f g \ + \s. ((\xs. (xs, Failed)) ` {xs. (xs, Failed) \ f s}) + \ ((\xs. (xs, Incomplete)) ` {xs. (xs, Incomplete) \ f s}) + \ (\(xs, rv, s) \ {(xs, rv, s'). (xs, Result (rv, s')) \ f s}. fst_upd (\ys. ys @ xs) ` g rv s)" apply (clarsimp simp add: bind_def fun_eq_iff Un_Union_image split_def intro!: eq_reflection) - apply (auto split: tmres.splits elim!:rev_bexI[where A="f x" for x]) - apply (fastforce intro: image_eqI[rotated]) + apply (fastforce split: tmres.splits elim!: rev_bexI[where A="f x" for x] + intro: image_eqI[rotated]) done lemma elem_bindE: - "(tr, res) \ bind f (\x. g x) s - \ ((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" + "\(tr, res) \ bind f g s; + \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) -text \ Each monad satisfies at least the following three laws. \ - -text \ @{term return} is absorbed at the left of a @{term bind}, - applying the return value directly: \ +text \Each monad satisfies at least the following three laws.\ +\ \FIXME: is this necessary? If it is, move it\ declare map_option.identity[simp] -lemma return_bind [simp]: "(return x >>= f) = f x" - by (auto simp add: return_def bind_def split_def split:if_splits) +text \@{term return} is absorbed at the left of a @{term bind}, applying the return value directly:\ +lemma return_bind[simp]: + "(return x >>= f) = f x" + 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" - by (auto simp add: fun_eq_iff bind_def return_def +text \@{term return} is absorbed on the right of a @{term bind}\ +lemma bind_return[simp]: + "(m >>= return) = m" + by (auto simp: fun_eq_iff bind_def return_def split: tmres.splits) -text \ @{term bind} is associative \ +text \@{term bind} is associative\ lemma bind_assoc: fixes m :: "('a,'b) tmonad" fixes f :: "'b \ ('a,'c) tmonad" @@ -293,7 +241,7 @@ lemma bind_assoc: apply (simp add: image_image) done -section \ Adding Exceptions \ +section \Adding Exceptions\ text \ The type @{typ "('s,'a) tmonad"} gives us nondeterminism and @@ -309,95 +257,61 @@ text \ we provide new names for the @{term return} and @{term bind} functions in this monad. We call them @{text returnOk} (for normal return values) and @{text bindE} (for composition). We also define @{text throwError} - to return an exceptional value. -\ -definition - returnOk :: "'a \ ('s, 'e + 'a) tmonad" -where + to return an exceptional value.\ +definition returnOk :: "'a \ ('s, 'e + 'a) tmonad" where "returnOk \ return o Inr" -definition - throwError :: "'e \ ('s, 'e + 'a) tmonad" -where +definition throwError :: "'e \ ('s, 'e + 'a) tmonad" where "throwError \ return o Inl" text \ Lifting a function over the exception type: if the input is an - exception, return that exception; otherwise continue execution. -\ -definition - lift :: "('a \ ('s, 'e + 'b) tmonad) \ - 'e +'a \ ('s, 'e + 'b) tmonad" -where - "lift f v \ case v of Inl e \ throwError e - | Inr v' \ f v'" + exception, return that exception; otherwise continue execution.\ +definition lift :: "('a \ ('s, 'e + 'b) tmonad) \ 'e +'a \ ('s, 'e + 'b) tmonad" where + "lift f v \ case v of Inl e \ throwError e | Inr v' \ f v'" text \ The definition of @{term bind} in the exception monad (new name @{text bindE}): the same as normal @{term bind}, but 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 - "bindE f g \ bind f (lift g)" - + produced an exception.\ +definition bindE :: + "('s, 'e + 'a) tmonad \ ('a \ ('s, 'e + 'b) tmonad) \ ('s, 'e + 'b) tmonad" + (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 - result as normal result and never throwing an exception. -\ -definition - liftE :: "('s,'a) tmonad \ ('s, 'e+'a) tmonad" -where + result as normal result and never throwing an exception.\ +definition liftE :: "('s,'a) tmonad \ ('s, 'e+'a) tmonad" 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: -\ -definition - whenE :: "bool \ ('s, 'e + unit) tmonad \ - ('s, 'e + unit) tmonad" -where + we need new definitions for when and unless:\ +definition whenE :: "bool \ ('s, 'e + unit) tmonad \ ('s, 'e + unit) tmonad" where "whenE P f \ if P then f else returnOk ()" -definition - unlessE :: "bool \ ('s, 'e + unit) tmonad \ - ('s, 'e + unit) tmonad" -where +definition unlessE :: "bool \ ('s, 'e + unit) tmonad \ ('s, 'e + unit) tmonad" 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) tmonad" -where - "throw_opt ex x \ - case x of None \ throwError ex | Some v \ returnOk v" - + returning @{term "v"} for @{term "Some v"}.\ +definition throw_opt :: "'e \ 'a option \ ('s, 'e + 'a) tmonad" where + "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 as @{const whenE} and @{const unlessE}, with @{term returnOk} - instead of @{term return}. -\ -definition - assertE :: "bool \ ('a, 'e + unit) tmonad" -where + instead of @{term return}.\ +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}: \ +text \More direct definition of @{const liftE}:\ lemma liftE_def2: "liftE f = (\s. snd_upd (map_tmres_rv Inr) ` (f s))" apply (clarsimp simp: fun_eq_iff liftE_def return_def split_def bind_def image_def) @@ -414,52 +328,51 @@ lemma liftE_def2: apply (clarsimp split: tmres.splits) done -text \ Left @{const returnOk} absorbtion over @{term bindE}: \ -lemma returnOk_bindE [simp]: "(returnOk x >>=E f) = f x" - apply (unfold bindE_def returnOk_def) - apply (clarsimp simp: lift_def) - done +text \Left @{const returnOk} absorbtion over @{term bindE}:\ +lemma returnOk_bindE[simp]: "(returnOk x >>=E f) = f x" + unfolding bindE_def returnOk_def + by (clarsimp simp: lift_def) -lemma lift_return [simp]: +lemma lift_return[simp]: "lift (return \ Inr) = return" - by (simp add: fun_eq_iff lift_def throwError_def split: sum.splits) + by (auto simp: lift_def throwError_def split: sum.splits) -text \ Right @{const returnOk} absorbtion over @{term bindE}: \ -lemma bindE_returnOk [simp]: "(m >>=E returnOk) = m" +text \Right @{const returnOk} absorbtion over @{term bindE}:\ +lemma bindE_returnOk[simp]: + "(m >>=E returnOk) = m" by (simp add: bindE_def returnOk_def) -text \ Associativity of @{const bindE}: \ +text \Associativity of @{const bindE}:\ lemma bindE_assoc: "(m >>=E f) >>=E g = m >>=E (\x. f x >>=E g)" - apply (simp add: bindE_def bind_assoc) - apply (rule arg_cong [where f="\x. m >>= x"]) - apply (rule ext) - apply (case_tac x, simp_all add: lift_def throwError_def) - done + unfolding bindE_def + by (fastforce simp: bind_assoc lift_def throwError_def + split: sum.splits + intro: arg_cong[where f="\x. m >>= x"]) -text \ @{const returnOk} could also be defined via @{const liftE}: \ +text \@{const returnOk} could also be defined via @{const liftE}:\ lemma returnOk_liftE: "returnOk x = liftE (return x)" by (simp add: liftE_def returnOk_def) -text \ Execution after throwing an exception is skipped: \ -lemma throwError_bindE [simp]: +text \Execution after throwing an exception is skipped:\ +lemma throwError_bindE[simp]: "(throwError E >>=E f) = throwError E" - by (simp add: fun_eq_iff bindE_def bind_def throwError_def lift_def return_def split_def) + by (simp add: bindE_def bind_def throwError_def lift_def return_def) section "Syntax" -text \ This section defines traditional Haskell-like do-syntax - for the state monad in Isabelle. \ +text \This section defines traditional Haskell-like do-syntax + for the state monad in Isabelle.\ -subsection "Syntax for the Nondeterministic State Monad" +subsection "Syntax for the Interference Trace Monad" -text \ We use @{text K_bind} to syntactically indicate the - case where the return argument of the left side of a @{term bind} - is ignored \ -definition - K_bind_def [iff]: "K_bind \ \x y. x" +text \ + We use @{text K_bind} to syntactically indicate the case where the return argument + of the left side of a @{term bind} is ignored\ +definition K_bind :: "'a \ 'b \ 'a" where + K_bind_def[iff]: "K_bind \ \x y. x" nonterminal dobinds and dobind and nobind @@ -479,7 +392,7 @@ translations "_do (_nobind b) e" == "b >>= (CONST K_bind e)" "do x <- a; e od" == "a >>= (\x. e)" -text \ Syntax examples: \ +text \Syntax examples:\ lemma "do x \ return 1; return (2::nat); return x @@ -495,58 +408,12 @@ lemma "do x \ return 1; od = return 1" by simp -subsection "Interference command" - -text \Interference commands must be inserted in between actions that can be interfered with commands -running in other threads. \ - -definition - last_st_tr :: "(tmid * 's) list \ 's \ 's" -where - "last_st_tr tr s0 = (hd (map snd tr @ [s0]))" - -definition - env_steps :: "('s,unit) tmonad" -where - "env_steps \ - do - s \ get; - \ \Add unfiltered environment events to the trace\ - xs \ select UNIV; - tr \ return (map (Pair Env) xs); - put_trace tr; - \ \Pick the last event of the trace as the final state\ - put (last_st_tr tr s) - od" - -definition - commit_step :: "('s, unit) tmonad" -where - "commit_step \ - do - s \ get; - put_trace [(Me,s)] - od" - -definition - interference :: "('s,unit) tmonad" -where - "interference \ - do - commit_step; - env_steps - od" - subsection "Syntax for the Exception Monad" text \ - Since the exception monad is a different type, we - need to syntactically distinguish it in the syntax. - We use @{text doE}/@{text odE} for this, but can re-use - most of the productions from @{text do}/@{text od} - above. -\ - + Since the exception monad is a different type, we need to distinguish it in the syntax + if we want to avoid ambiguous terms. We use @{text doE}/@{text odE} for this, but can + re-use most of the productions from @{text do}/@{text od} above. \ syntax "_doE" :: "[dobinds, 'a] => 'a" ("(doE ((_);//(_))//odE)" 100) @@ -555,7 +422,7 @@ translations "_doE (_nobind b) e" == "b >>=E (CONST K_bind e)" "doE x <- a; e odE" == "a >>=E (\x. e)" -text \ Syntax examples: \ +text \Syntax examples:\ lemma "doE x \ returnOk 1; returnOk (2::nat); returnOk x @@ -572,107 +439,115 @@ lemma "doE x \ returnOk 1; by simp +subsection "Interference command" -section "Library of additional Monadic Functions and Combinators" +text \ + Interference commands must be inserted in between actions that can be interfered with by + commands running in other threads.\ +definition last_st_tr :: "(tmid * 's) list \ 's \ 's" where + "last_st_tr tr s0 \ hd (map snd tr @ [s0])" -text \ Lifting a normal function into the monad type: \ -definition - liftM :: "('a \ 'b) \ ('s,'a) tmonad \ ('s, 'b) tmonad" -where +text \Nondeterministically add all possible environment events to the trace.\ +definition env_steps :: "('s,unit) tmonad" where + "env_steps \ + do + s \ get; + \ \Add unfiltered environment events to the trace\ + xs \ select UNIV; + tr \ return (map (Pair Env) xs); + put_trace tr; + \ \Pick the last event of the trace as the final state\ + put (last_st_tr tr s) + od" + +text \Add the current state to the trace, tagged as a self action.\ +definition commit_step :: "('s,unit) tmonad" where + "commit_step \ + do + s \ get; + put_trace [(Me,s)] + od" + +text \ + Record the action taken by the current thread since the last interference point and + then add unfiltered environment events.\ +definition interference :: "('s,unit) tmonad" where + "interference \ + do + commit_step; + env_steps + od" + + +section "Library of additional Monadic Functions and Combinators" + +text \Lifting a normal function into the monad type:\ +definition liftM :: "('a \ 'b) \ ('s,'a) tmonad \ ('s, 'b) tmonad" where "liftM f m \ do x \ m; return (f x) od" -text \ The same for the exception monad: \ -definition - liftME :: "('a \ 'b) \ ('s,'e+'a) tmonad \ ('s,'e+'b) tmonad" -where +text \The same for the exception monad:\ +definition liftME :: "('a \ 'b) \ ('s,'e+'a) tmonad \ ('s,'e+'b) tmonad" where "liftME f m \ doE x \ m; returnOk (f x) odE" -text \ Run a sequence of monads from left to right, ignoring return values. \ -definition - sequence_x :: "('s, 'a) tmonad list \ ('s, unit) tmonad" -where +text \Run a sequence of monads from left to right, ignoring return values.\ +definition sequence_x :: "('s, 'a) tmonad list \ ('s, unit) tmonad" where "sequence_x xs \ foldr (\x y. x >>= (\_. y)) xs (return ())" text \ Map a monadic function over a list by applying it to each element - of the list from left to right, ignoring return values. -\ -definition - mapM_x :: "('a \ ('s,'b) tmonad) \ 'a list \ ('s, unit) tmonad" -where + of the list from left to right, ignoring return values.\ +definition mapM_x :: "('a \ ('s,'b) tmonad) \ 'a list \ ('s, unit) tmonad" where "mapM_x f xs \ sequence_x (map f xs)" text \ Map a monadic function with two parameters over two lists, 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 + return values.\ +definition zipWithM_x :: + "('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 \ The same three functions as above, but returning a list of -return values instead of @{text unit} \ -definition - sequence :: "('s, 'a) tmonad list \ ('s, 'a list) tmonad" -where +text \ + The same three functions as above, but returning a list of + return values instead of @{text unit}\ +definition sequence :: "('s, 'a) tmonad list \ ('s, 'a list) tmonad" where "sequence xs \ let mcons = (\p q. p >>= (\x. q >>= (\y. return (x#y)))) in foldr mcons xs (return [])" -definition - mapM :: "('a \ ('s,'b) tmonad) \ 'a list \ ('s, 'b list) tmonad" -where +definition mapM :: "('a \ ('s,'b) tmonad) \ 'a list \ ('s, 'b list) tmonad" where "mapM f xs \ sequence (map f xs)" -definition - zipWithM :: "('a \ 'b \ ('s,'c) tmonad) \ - 'a list \ 'b list \ ('s, 'c list) tmonad" -where +definition zipWithM :: + "('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 +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 "foldME m a xs \ foldr (\p q. q >>=E swp m p) xs (returnOk a)" +definition foldME :: + "('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 \ The sequence and map functions above for the exception monad, -with and without lists of return value \ -definition - sequenceE_x :: "('s, 'e+'a) tmonad list \ ('s, 'e+unit) tmonad" -where +text \ + The sequence and map functions above for the exception monad, with and without + lists of return value\ +definition sequenceE_x :: "('s, 'e+'a) tmonad list \ ('s, 'e+unit) tmonad" where "sequenceE_x xs \ foldr (\x y. doE _ <- x; y odE) xs (returnOk ())" -definition - mapME_x :: "('a \ ('s,'e+'b) tmonad) \ 'a list \ - ('s,'e+unit) tmonad" -where +definition mapME_x :: "('a \ ('s,'e+'b) tmonad) \ 'a list \ ('s,'e+unit) tmonad" where "mapME_x f xs \ sequenceE_x (map f xs)" -definition - sequenceE :: "('s, 'e+'a) tmonad list \ ('s, 'e+'a list) tmonad" -where +definition sequenceE :: "('s, 'e+'a) tmonad list \ ('s, 'e+'a list) tmonad" where "sequenceE xs \ let mcons = (\p q. p >>=E (\x. q >>=E (\y. returnOk (x#y)))) - in foldr mcons xs (returnOk [])" + in foldr mcons xs (returnOk [])" -definition - mapME :: "('a \ ('s,'e+'b) tmonad) \ 'a list \ - ('s,'e+'b list) tmonad" -where +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 +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 []" | "filterM P (x # xs) = do b <- P x; @@ -680,13 +555,10 @@ where return (if b then (x # ys) else ys) od" -text \ @{text select_state} takes a relationship between - states, and outputs nondeterministically a state - related to the input state. \ - -definition - state_select :: "('s \ 's) set \ ('s, unit) tmonad" -where +text \ + @{text select_state} takes a relationship between states, and outputs + nondeterministically a state related to the input state.\ +definition state_select :: "('s \ 's) set \ ('s, unit) tmonad" where "state_select r \ (do s \ get; S \ return {s'. (s, s') \ r}; @@ -694,17 +566,15 @@ where s' \ select S; put s' od)" + + section "Catching and Handling Exceptions" 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 + by catching and handling any potential exceptions:\ +definition catch :: + "('s, 'e + 'a) tmonad \ ('e \ ('s, 'a) tmonad) \ ('s, 'a) tmonad" (infix "" 10) where "f handler \ do x \ f; case x of @@ -715,13 +585,10 @@ where text \ Handling exceptions, but staying in the exception monad. The handler may throw a type of exceptions different from - the left side. -\ -definition - handleE' :: "('s, 'e1 + 'a) tmonad \ - ('e1 \ ('s, 'e2 + 'a) tmonad) \ - ('s, 'e2 + 'a) tmonad" (infix "" 10) -where + the left side.\ +definition handleE' :: + "('s, 'e1 + 'a) tmonad \ ('e1 \ ('s, 'e2 + 'a) tmonad) \ ('s, 'e2 + 'a) tmonad" + (infix "" 10) where "f handler \ do v \ f; @@ -733,27 +600,19 @@ where text \ A type restriction of the above that is used more commonly in 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 + 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 "handleE \ handleE'" - text \ Handling exceptions, and additionally providing a continuation - 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 + 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 "f handler continue \ do v \ f; case v of Inl e \ handler e @@ -766,56 +625,53 @@ text \ Loops are handled using the following inductive predicate; non-termination is represented using the failure flag of the monad. -\ -inductive_set - whileLoop_results :: "('r \ 's \ bool) \ ('r \ ('s, 'r) tmonad) \ (('r \ 's) \ ((tmid \ 's) list \ ('s, 'r) tmres)) set" - for C B -where +FIXME: update comment about non-termination\ + +inductive_set whileLoop_results :: + "('r \ 's \ bool) \ ('r \ ('s, 'r) tmonad) \ (('r \ 's) \ ((tmid \ 's) list \ ('s, 'r) tmres)) set" + for C B where "\ \ C r s \ \ ((r, s), ([], Result (r, s))) \ whileLoop_results C B" | "\ C r s; (ts, Failed) \ B r s \ \ ((r, s), (ts, Failed)) \ whileLoop_results C B" | "\ C r s; (ts, Incomplete) \ B r s \ \ ((r, s), (ts, Incomplete)) \ whileLoop_results C B" | "\ C r s; (ts, Result (r', s')) \ B r s; ((r', s'), (ts',z)) \ whileLoop_results C B \ \ ((r, s), (ts'@ts,z)) \ whileLoop_results C B" +\ \FIXME: there are fewer lemmas here than in NonDetMonad and I don't understand this well enough + to know whether this is correct or not.\ inductive_cases whileLoop_results_cases_result_end: "((x,y), ([],Result r)) \ whileLoop_results C B" inductive_cases whileLoop_results_cases_fail: "((x,y), (ts, Failed)) \ whileLoop_results C B" inductive_cases whileLoop_results_cases_incomplete: "((x,y), (ts, Incomplete)) \ whileLoop_results C B" inductive_simps whileLoop_results_simps_valid: "((x,y), ([], Result z)) \ whileLoop_results C B" -inductive - whileLoop_terminates :: "('r \ 's \ bool) \ ('r \ ('s, 'r) tmonad) \ 'r \ 's \ bool" - for C B -where +inductive whileLoop_terminates :: + "('r \ 's \ bool) \ ('r \ ('s, 'r) tmonad) \ 'r \ 's \ bool" + for C B where "\ C r s \ whileLoop_terminates C B r s" | "\ C r s; \(r', s') \ Result -` snd ` (B r s). whileLoop_terminates C B r' s' \ \ whileLoop_terminates C B r s" - 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 +definition whileLoop :: + "('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) whileLoop ("(whileLoop (_)// (_))" [1000, 1000] 1000) -definition - whileLoopT :: "('r \ 's \ bool) \ ('r \ ('s, 'r) tmonad) \ 'r \ ('s, 'r) tmonad" -where +\ \FIXME: why does this differ to Nondet_Monad?\ +definition whileLoopT :: + "('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})" notation (output) whileLoopT ("(whileLoopT (_)// (_))" [1000, 1000] 1000) -definition - whileLoopE :: "('r \ 's \ bool) \ ('r \ ('s, 'e + 'r) tmonad) - \ 'r \ ('s, ('e + 'r)) tmonad" -where +definition whileLoopE :: + "('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)" @@ -824,13 +680,9 @@ notation (output) subsection "Await command" -text \ @{term "Await c f"} blocks the execution until the @{term "c"} is true, - and atomically executes @{term "f"}. -\ - -definition - Await :: "('s \ bool) \ ('s,unit) tmonad" -where +text \@{term "Await c f"} blocks the execution until @{term "c"} is true, + and then atomically executes @{term "f"}.\ +definition Await :: "('s \ bool) \ ('s,unit) tmonad" where "Await c \ do s \ get; @@ -843,203 +695,10 @@ where put (last_st_tr tr s) od" -section "Hoare Logic" - -subsection "Validity" - -text \ This section defines a Hoare logic for partial correctness for - the nondeterministic state monad as well as the exception monad. - The logic talks only about the behaviour part of the monad and ignores - the failure flag. - - The logic is defined semantically. Rules work directly on the - validity predicate. - - In the nondeterministic state monad, validity is a triple of precondition, - monad, and postcondition. The precondition is a function from state to - bool (a state predicate), the postcondition is a function from return value - to state to bool. A triple is valid if for all states that satisfy the - precondition, all result values and result states that are returned by - the monad satisfy the postcondition. Note that if the computation returns - the empty set, the triple is trivially valid. This means @{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 separate predicate and - calculus (see below). -\ - - -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 - "invariant f P \ \P\ f \\_. P\" - -text \rg_pred type: Rely-Guaranty predicates (state before => state after => bool)\ -type_synonym 's rg_pred = "'s \ 's \ bool" - - -text \ - Validity for the exception monad is similar and build on the standard - validity above. Instead of one postcondition, we have two: one for - normal and one for exceptional results. -\ -definition - validE :: "('s \ bool) \ ('s, 'a + 'b) tmonad \ - ('b \ 's \ bool) \ - ('a \ 's \ bool) \ bool" -("\_\/ _ /(\_\,/ \_\)" ) -where - "\P\ f \Q\,\E\ \ \P\ f \ \v s. case v of Inr r \ Q r s | Inl e \ E e s \" -(* -text \ Validity for exception monad with interferences. Not as easy to phrase - as we need to \ -definition - validIE :: "('s, 'a + 'b) tmonad \ - 's rg_pred \ - 's rg_pred \ 's rg_pred \ - ('b \ 's rg_pred) \ - ('a \ 's rg_pred) \ bool" - ("_ //PRE _//RELY _//GUAR _//POST _//EXC _" [59,0,0,0,0,0] 60) -where - "validIE f P R G Q E \ f SAT [P,R,G,\v. case v of Inr r \ Q r | Inl e \ E e]" - -abbreviation (input) - validIEsat :: "('s, 'a + 'b) tmonad \ - 's rg_pred \ - 's rg_pred \ 's rg_pred \ - ('b \ 's rg_pred) \ - ('a \ 's rg_pred) \ bool" - ("_ //SAT [_, _, _, _, _]" [59,0,0,0,0,0] 60) - where - "validIEsat f P R G Q E \ validIE f P R G Q E" - *) -text \ - The following two instantiations are convenient to separate reasoning - for exceptional and normal case. -\ -definition - validE_R :: "('s \ bool) \ ('s, 'e + 'a) tmonad \ - ('a \ 's \ bool) \ bool" - ("\_\/ _ /\_\, -") -where - "\P\ f \Q\,- \ validE P f Q (\x y. True)" - -definition - validE_E :: "('s \ bool) \ ('s, 'e + 'a) tmonad \ - ('e \ 's \ bool) \ bool" - ("\_\/ _ /-, \_\") -where - "\P\ f -,\Q\ \ validE P f (\x y. True) Q" - - -text \ Abbreviations for trivial postconditions (taking three arguments): \ -abbreviation(input) - toptoptop :: "'a \ 'b \ 'b \ bool" ("\\\") -where - "\\\ \ \_ _ _. True" - -abbreviation(input) - botbotbot :: "'a \ 'b \ 'b \ bool" ("\\\") -where - "\\\ \ \_ _ _. False" - - -subsection "Determinism" - -text \ A monad of type @{text tmonad} is deterministic iff it -returns an empty trace, exactly one state and result and does not fail \ -definition - det :: "('a,'s) tmonad \ bool" -where - "det f \ \s. \r. f s = {([], Result r)}" - -text \ A deterministic @{text tmonad} can be turned - into a normal state monad: \ -definition - the_run_state :: "('s,'a) tmonad \ 's \ 'a \ 's" -where - "the_run_state M \ \s. THE s'. mres (M s) = {s'}" - - -subsection "Non-Failure" - -text \ - We can formulate non-failure separately from validity. -\ -definition - no_fail :: "('s \ bool) \ ('s,'a) tmonad \ bool" -where - "no_fail P m \ \s. P s \ Failed \ snd ` (m s)" - -text \ - It is often desired to prove non-failure and a Hoare triple - simultaneously, as the reasoning is often similar. The following - definitions allow such reasoning to take place. -\ - -definition - validNF ::"('s \ bool) \ ('s,'a) tmonad \ ('a \ 's \ bool) \ bool" - ("\_\/ _ /\_\!") -where - "validNF P f Q \ valid P f Q \ no_fail P f" - -definition - validE_NF :: "('s \ bool) \ ('s, 'a + 'b) tmonad \ - ('b \ 's \ bool) \ - ('a \ 's \ bool) \ bool" - ("\_\/ _ /(\_\,/ \_\!)") -where - "validE_NF P f Q E \ validE P f Q E \ no_fail P f" - -lemma validE_NF_alt_def: - "\ P \ B \ Q \,\ E \! = \ P \ B \ \v s. case v of Inl e \ E e s | Inr r \ Q r s \!" - by (clarsimp simp: validE_NF_def validE_def validNF_def) - -(* text \ - Usually, well-formed monads constructed from the primitives - above will have the following property: if they return an - empty set of results, they will have the failure flag set. -\ -definition - empty_fail :: "('s,'a) tmonad \ bool" -where - "empty_fail m \ \s. fst (m s) = {} \ snd (m s)" - -text \ - Useful in forcing otherwise unknown executions to have - the @{const empty_fail} property. -\ -definition - mk_ef :: "'a set \ bool \ 'a set \ bool" -where - "mk_ef S \ (fst S, fst S = {} \ snd S)" - *) -section "Basic exception reasoning" - -text \ - The following predicates @{text no_throw} and @{text no_return} allow - reasoning that functions in the exception monad either do - no throw an exception or never return normally. -\ - -definition "no_throw P A \ \ P \ A \ \_ _. True \,\ \_ _. False \" - -definition "no_return P A \ \ P \ A \\_ _. False\,\\_ _. True \" section "Trace monad Parallel" -definition - parallel :: "('s,'a) tmonad \ ('s,'a) tmonad \ ('s,'a) tmonad" -where +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 \ (map (\(f_step, (id, s)). (if f_step then id else Env, s)) (zip f_steps xs), rv) \ f s \ (map (\(f_step, (id, s)). (if f_step then Env else id, s)) (zip f_steps xs), rv) \ g s})" @@ -1071,84 +730,4 @@ lemma parallel_def3: \ list_all2 (\y z. (fst y = Env \ fst z = Env) \ snd y = snd z) ys zs})" by (simp add: parallel_def2, rule ext, auto simp: image_def) -primrec - trace_steps :: "(tmid \ 's) list \ 's \ (tmid \ 's \ 's) set" -where - "trace_steps (elem # trace) s0 = {(fst elem, s0, snd elem)} \ trace_steps trace (snd elem)" -| "trace_steps [] s0 = {}" - -lemma trace_steps_nth: - "trace_steps xs s0 = (\i. (fst (xs ! i), (if i = 0 then s0 else snd (xs ! (i - 1))), snd (xs ! i))) ` {..< length xs}" -proof (induct xs arbitrary: s0) - case Nil - show ?case by simp -next - case (Cons a xs) - show ?case - apply (simp add: lessThan_Suc_eq_insert_0 Cons image_image nth_Cons') - apply (intro arg_cong2[where f=insert] refl image_cong) - apply simp - done -qed - -definition - rely_cond :: "'s rg_pred \ 's \ (tmid \ 's) list \ bool" -where - "rely_cond R s0s tr = (\(ident, s0, s) \ trace_steps (rev tr) s0s. ident = Env \ R s0 s)" - -definition - guar_cond :: "'s rg_pred \ 's \ (tmid \ 's) list \ bool" -where - "guar_cond G s0s tr = (\(ident, s0, s) \ trace_steps (rev tr) s0s. ident = Me \ G s0 s)" - -lemma rg_empty_conds[simp]: - "rely_cond R s0s []" - "guar_cond G s0s []" - by (simp_all add: rely_cond_def guar_cond_def) - -definition - rely :: "('s, 'a) tmonad \ 's rg_pred \ 's \ ('s, 'a) tmonad" -where - "rely f R s0s \ (\s. f s \ ({tr. rely_cond R s0s tr} \ UNIV))" - -definition - prefix_closed :: "('s, 'a) tmonad \ bool" -where - "prefix_closed f = (\s. \x xs. (x # xs) \ fst ` f s \ (xs, Incomplete) \ f s)" - -definition - validI :: "('s \ 's \ bool) \ 's rg_pred \ ('s,'a) tmonad - \ 's rg_pred \ ('a \ 's \ 's \ bool) \ bool" - ("(\_\,/ \_\)/ _ /(\_\,/ \_\)") -where - "\P\,\R\ f \G\,\Q\ \ prefix_closed f \ (\s0 s. P s0 s - \ (\tr res. (tr, res) \ (rely f R s0 s) \ guar_cond G s0 tr - \ (\rv s'. res = Result (rv, s') \ Q rv (last_st_tr tr s0) s')))" - -lemma in_rely: - "\ (tr, res) \ f s; rely_cond R s0s tr \ \ (tr, res) \ rely f R s0s s" - by (simp add: rely_def) - -lemmas validI_D = validI_def[THEN meta_eq_to_obj_eq, THEN iffD1, - THEN conjunct2, rule_format, OF _ _ in_rely] -lemmas validI_GD = validI_D[THEN conjunct1] -lemmas validI_rvD = validI_D[THEN conjunct2, rule_format, rotated -1, OF refl] -lemmas validI_prefix_closed = validI_def[THEN meta_eq_to_obj_eq, THEN iffD1, THEN conjunct1] -lemmas validI_prefix_closed_T = validI_prefix_closed[where P="\_ _. False" and R="\_ _. False" - and G="\_ _. True" and Q="\_ _ _. True"] - -lemmas prefix_closedD1 = prefix_closed_def[THEN iffD1, rule_format] - -lemma in_fst_snd_image_eq: - "x \ fst ` S = (\y. (x, y) \ S)" - "y \ snd ` S = (\x. (x, y) \ S)" - by (auto elim: image_eqI[rotated]) - -lemma in_fst_snd_image: - "(x, y) \ S \ x \ fst ` S" - "(x, y) \ S \ y \ snd ` S" - by (auto simp: in_fst_snd_image_eq) - -lemmas prefix_closedD = prefix_closedD1[OF _ in_fst_snd_image(1)] - end diff --git a/lib/Monads/trace/Trace_Monad_Equations.thy b/lib/Monads/trace/Trace_Monad_Equations.thy new file mode 100644 index 0000000000..ee0730def0 --- /dev/null +++ b/lib/Monads/trace/Trace_Monad_Equations.thy @@ -0,0 +1,247 @@ +(* + * Copyright 2023, Proofcraft Pty Ltd + * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) + * + * SPDX-License-Identifier: BSD-2-Clause + *) + +(* Equations between monads. Conclusions of the form "f = g" where f and g are monads. + Should not be Hoare triples (those go into a different theory). *) + +theory Trace_Monad_Equations + imports + Trace_Lemmas +begin + +lemmas bind_then_eq = arg_cong2[where f=bind, OF _ refl] + +lemma modify_id: + "modify id = return ()" + by (simp add: modify_def get_def bind_def put_def return_def) + +lemma modify_modify: + "(do x \ modify f; modify (g x) od) = modify (g () o f)" + by (simp add: bind_def simpler_modify_def) + +lemmas modify_modify_bind = arg_cong2[where f=bind, + OF modify_modify refl, simplified bind_assoc] + +lemma select_single: + "select {x} = return x" + by (simp add: select_def return_def) + +lemma put_then_get[unfolded K_bind_def]: + "do put s; get od = do put s; return s od" + by (simp add: put_def bind_def get_def return_def) + +lemmas put_then_get_then + = put_then_get[THEN bind_then_eq, simplified bind_assoc return_bind] + +lemma select_empty_bind[simp]: + "select {} >>= f = select {}" + by (simp add: select_def bind_def) + +lemma fail_bind[simp]: + "fail >>= f = fail" + by (simp add: bind_def fail_def) + + +subsection \Alternative env_steps with repeat\ + +lemma mapM_Cons: + "mapM f (x # xs) = do + y \ f x; + ys \ mapM f xs; + return (y # ys) + od" + and mapM_Nil: + "mapM f [] = return []" + by (simp_all add: mapM_def sequence_def) + +lemma mapM_x_Cons: + "mapM_x f (x # xs) = do + y \ f x; + mapM_x f xs + od" + and mapM_x_Nil: + "mapM_x f [] = return ()" + by (simp_all add: mapM_x_def sequence_x_def) + +lemma mapM_append: + "mapM f (xs @ ys) = (do + fxs \ mapM f xs; + fys \ mapM f ys; + return (fxs @ fys) + od)" + by (induct xs, simp_all add: mapM_Cons mapM_Nil bind_assoc) + +lemma mapM_x_append: + "mapM_x f (xs @ ys) = (do + x \ mapM_x f xs; + mapM_x f ys + od)" + by (induct xs, simp_all add: mapM_x_Cons mapM_x_Nil bind_assoc) + +lemma mapM_map: + "mapM f (map g xs) = mapM (f o g) xs" + by (induct xs; simp add: mapM_Nil mapM_Cons) + +lemma mapM_x_map: + "mapM_x f (map g xs) = mapM_x (f o g) xs" + by (induct xs; simp add: mapM_x_Nil mapM_x_Cons) + +primrec repeat_n :: "nat \ ('s, unit) tmonad \ ('s, unit) tmonad" where + "repeat_n 0 f = return ()" + | "repeat_n (Suc n) f = do f; repeat_n n f od" + +lemma repeat_n_mapM_x: + "repeat_n n f = mapM_x (\_. f) (replicate n ())" + by (induct n, simp_all add: mapM_x_Cons mapM_x_Nil) + +definition repeat :: "('s, unit) tmonad \ ('s, unit) tmonad" where + "repeat f = do n \ select UNIV; repeat_n n f od" + +definition env_step :: "('s,unit) tmonad" where + "env_step = + do + s' \ select UNIV; + put_trace_elem (Env, s'); + put s' + od" + +abbreviation + "env_n_steps n \ repeat_n n env_step" + +lemma elem_select_bind: + "(tr, res) \ (do x \ select S; f x od) s + = (\x \ S. (tr, res) \ f x s)" + by (simp add: bind_def select_def) + +lemma select_bind_UN: + "(do x \ select S; f x od) = (\s. \x \ S. f x s)" + by (rule ext, auto simp: elem_select_bind) + +lemma select_early: + "S \ {} + \ do x \ f; y \ select S; g x y od + = do y \ select S; x \ f; g x y od" + apply (simp add: bind_def select_def Sigma_def) + apply (rule ext) + apply (fastforce elim: rev_bexI image_eqI[rotated] split: tmres.split_asm) + done + +lemma repeat_n_choice: + "S \ {} + \ repeat_n n (do x \ select S; f x od) + = (do xs \ select {xs. set xs \ S \ length xs = n}; mapM_x f xs od)" + apply (induct n; simp?) + apply (simp add: select_def bind_def mapM_x_Nil cong: conj_cong) + apply (simp add: select_early bind_assoc) + apply (subst select_early) + apply simp + apply (auto intro: exI[where x="replicate n xs" for n xs])[1] + apply (simp(no_asm) add: fun_eq_iff set_eq_iff elem_select_bind) + apply (simp only: conj_comms[where Q="length xs = n" for xs n]) + apply (simp only: ex_simps[symmetric] conj_assoc length_Suc_conv, simp) + apply (auto simp: mapM_x_Cons) + done + +lemma repeat_choice: + "S \ {} + \ repeat (do x \ select S; f x od) + = (do xs \ select {xs. set xs \ S}; mapM_x f xs od)" + apply (simp add: repeat_def repeat_n_choice) + apply (simp(no_asm) add: fun_eq_iff set_eq_iff elem_select_bind) + done + +lemma put_trace_append: + "put_trace (xs @ ys) = do put_trace ys; put_trace xs od" + by (induct xs; simp add: bind_assoc) + +lemma put_trace_elem_put_comm: + "do y \ put_trace_elem x; put s od + = do y \ put s; put_trace_elem x od" + by (simp add: put_def put_trace_elem_def bind_def insert_commute) + +lemma put_trace_put_comm: + "do y \ put_trace xs; put s od + = do y \ put s; put_trace xs od" + apply (rule sym; induct xs; simp) + apply (simp add: bind_assoc put_trace_elem_put_comm) + apply (simp add: bind_assoc[symmetric]) + done + +lemma mapM_x_comm: + "(\x \ set xs. do y \ g; f x od = do y \ f x; g od) + \ do y \ g; mapM_x f xs od = do y \ mapM_x f xs; g od" + apply (induct xs; simp add: mapM_x_Nil mapM_x_Cons) + apply (simp add: bind_assoc[symmetric], simp add: bind_assoc) + done + +lemma mapM_x_split: + "(\x \ set xs. \y \ set xs. do z \ g y; f x od = do (z :: unit) \ f x; g y od) + \ mapM_x (\x. do z \ f x; g x od) xs = do y \ mapM_x f xs; mapM_x g xs od" + apply (induct xs; simp add: mapM_x_Nil mapM_x_Cons bind_assoc) + apply (subst bind_assoc[symmetric], subst mapM_x_comm[where f=f and g="g x" for x]) + apply simp + apply (simp add: bind_assoc) + done + +lemma mapM_x_put: + "mapM_x put xs = unless (xs = []) (put (last xs))" + apply (induct xs rule: rev_induct) + apply (simp add: mapM_x_Nil unless_def when_def) + apply (simp add: mapM_x_append mapM_x_Cons mapM_x_Nil) + apply (simp add: bind_def unless_def when_def put_def return_def) + done + +lemma put_trace_mapM_x: + "put_trace xs = mapM_x put_trace_elem (rev xs)" + by (induct xs; simp add: mapM_x_Nil mapM_x_append mapM_x_Cons) + +lemma rev_surj: + "surj rev" + by (rule_tac f=rev in surjI, simp) + +lemma select_image: + "select (f ` S) = do x \ select S; return (f x) od" + by (auto simp add: bind_def select_def return_def Sigma_def) + +lemma env_steps_repeat: + "env_steps = repeat env_step" + apply (simp add: env_step_def repeat_choice env_steps_def + select_early) + apply (simp add: put_trace_elem_put_comm) + apply (simp add: mapM_x_split put_trace_elem_put_comm put_trace_put_comm + mapM_x_put) + apply (simp add: put_trace_mapM_x rev_map mapM_x_map o_def) + apply (subst rev_surj[symmetric], simp add: select_image bind_assoc) + apply (rule arg_cong2[where f=bind, OF refl ext]) + apply (simp add: bind_def get_def put_def unless_def when_def return_def) + apply (simp add: last_st_tr_def hd_map hd_rev) + done + +lemma repeat_n_plus: + "repeat_n (n + m) f = do repeat_n n f; repeat_n m f od" + by (induct n; simp add: bind_assoc) + +lemma repeat_eq_twice[simp]: + "(do x \ repeat f; repeat f od) = repeat f" + apply (simp add: repeat_def select_early) + apply (simp add: bind_assoc repeat_n_plus[symmetric, simplified]) + apply (simp add: bind_def select_def Sigma_def) + apply (rule ext, fastforce intro: exI[where x=0]) + done + +lemmas repeat_eq_twice_then[simp] = + repeat_eq_twice[THEN bind_then_eq, simplified bind_assoc] + +lemmas env_steps_eq_twice[simp] = + repeat_eq_twice[where f=env_step, folded env_steps_repeat] +lemmas env_steps_eq_twice_then[simp] = + env_steps_eq_twice[THEN bind_then_eq, simplified bind_assoc] + +lemmas mapM_collapse_append = + mapM_append[symmetric, THEN bind_then_eq, simplified bind_assoc, simplified] + +end \ No newline at end of file diff --git a/lib/Monads/trace/Trace_More_VCG.thy b/lib/Monads/trace/Trace_More_VCG.thy new file mode 100644 index 0000000000..9a12ec1eeb --- /dev/null +++ b/lib/Monads/trace/Trace_More_VCG.thy @@ -0,0 +1,20 @@ +(* + * Copyright 2023, Proofcraft Pty Ltd + * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) + * + * SPDX-License-Identifier: BSD-2-Clause + *) + +(* Partial correctness Hoare logic lemmas over the trace monad. Hoare triples, lifting lemmas, etc. + If it doesn't contain a Hoare triple it likely doesn't belong in here. *) + +theory Trace_More_VCG + imports + Trace_VCG +begin + +lemma hoare_pre_tautI: + "\ \A and P\ a \B\; \A and not P\ a \B\ \ \ \A\ a \B\" + by (fastforce simp: valid_def split_def pred_conj_def pred_neg_def) + +end \ No newline at end of file diff --git a/lib/Monads/trace/Trace_No_Fail.thy b/lib/Monads/trace/Trace_No_Fail.thy new file mode 100644 index 0000000000..dd47142aac --- /dev/null +++ b/lib/Monads/trace/Trace_No_Fail.thy @@ -0,0 +1,142 @@ +(* + * Copyright 2023, Proofcraft Pty Ltd + * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) + * + * SPDX-License-Identifier: BSD-2-Clause + *) + +(* Lemmas about the no_fail predicate. *) + +theory Trace_No_Fail + imports + Trace_In_Monad + Trace_VCG + WPSimp +begin + +subsection "Non-Failure" + +text \ + With the failure result, we can formulate non-failure separately from validity. + A monad @{text m} does not fail under precondition @{text P}, if for no start + state that satisfies the precondition it returns a @{term Failed} result. +\ +definition no_fail :: "('s \ bool) \ ('s,'a) tmonad \ bool" where + "no_fail P m \ \s. P s \ Failed \ snd ` (m s)" + + +subsection \@{method wpc} setup\ + +lemma no_fail_pre[wp_pre]: + "\ no_fail P f; \s. Q s \ P s\ \ no_fail Q f" + by (simp add: no_fail_def) + +lemma wpc_helper_no_fail_final: + "no_fail Q f \ wpc_helper (P, P', P'') (Q, Q', Q'') (no_fail P f)" + by (clarsimp simp: wpc_helper_def elim!: no_fail_pre) + +wpc_setup "\m. no_fail P m" wpc_helper_no_fail_final + + +subsection \Bundles\ + +bundle no_pre = hoare_pre [wp_pre del] no_fail_pre [wp_pre del] + + +subsection \Lemmas\ + +lemma no_failD: + "\ no_fail P m; P s \ \ Failed \ snd ` m s" + by (simp add: no_fail_def) + +lemma no_fail_modify[wp,simp]: + "no_fail \ (modify f)" + by (simp add: no_fail_def modify_def get_def put_def bind_def) + +lemma no_fail_gets_simp[simp]: + "no_fail P (gets f)" + unfolding no_fail_def gets_def get_def return_def bind_def + by simp + +lemma no_fail_gets[wp]: + "no_fail \ (gets f)" + by simp + +lemma no_fail_select[simp]: + "no_fail \ (select S)" + by (simp add: no_fail_def select_def image_def) + +lemma no_fail_alt[wp]: + "\ no_fail P f; no_fail Q g \ \ no_fail (P and Q) (f \ g)" + by (auto simp: no_fail_def alternative_def) + +lemma no_fail_return[simp, wp]: + "no_fail \ (return x)" + by (simp add: return_def no_fail_def) + +lemma no_fail_get[simp, wp]: + "no_fail \ get" + by (simp add: get_def no_fail_def) + +lemma no_fail_put[simp, wp]: + "no_fail \ (put s)" + by (simp add: put_def no_fail_def) + +lemma no_fail_when[wp]: + "(P \ no_fail Q f) \ no_fail (if P then Q else \) (when P f)" + by (simp add: when_def) + +lemma no_fail_unless[wp]: + "(\P \ no_fail Q f) \ no_fail (if P then \ else Q) (unless P f)" + by (simp add: unless_def when_def) + +lemma no_fail_fail[simp, wp]: + "no_fail \ fail" + by (simp add: fail_def no_fail_def) + +lemma no_fail_assert[simp, wp]: + "no_fail (\_. P) (assert P)" + by (simp add: assert_def) + +lemma no_fail_assert_opt[simp, wp]: + "no_fail (\_. P \ None) (assert_opt P)" + by (simp add: assert_opt_def split: option.splits) + +lemma no_fail_case_option[wp]: + assumes f: "no_fail P f" + assumes g: "\x. no_fail (Q x) (g x)" + shows "no_fail (if x = None then P else Q (the x)) (case_option f g x)" + by (clarsimp simp add: f g) + +lemma no_fail_if[wp]: + "\ P \ no_fail Q f; \P \ no_fail R g \ \ no_fail (if P then Q else R) (if P then f else g)" + by simp + +lemma no_fail_apply[wp]: + "no_fail P (f (g x)) \ no_fail P (f $ g x)" + by simp + +lemma no_fail_undefined[simp, wp]: + "no_fail \ undefined" + by (simp add: no_fail_def) + +lemma no_fail_returnOK[simp, wp]: + "no_fail \ (returnOk x)" + by (simp add: returnOk_def) + +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 + in_image_constant) + apply (intro allI conjI impI) + apply (fastforce simp: image_def) + apply clarsimp + apply (drule(1) post_by_hoare, erule in_mres) + apply (fastforce simp: image_def) + done + +lemma no_fail_or: + "\no_fail P a; no_fail Q a\ \ no_fail (P or Q) a" + by (clarsimp simp: no_fail_def) + +end diff --git a/lib/Monads/trace/Trace_No_Throw.thy b/lib/Monads/trace/Trace_No_Throw.thy new file mode 100644 index 0000000000..c98ac96598 --- /dev/null +++ b/lib/Monads/trace/Trace_No_Throw.thy @@ -0,0 +1,28 @@ +(* + * Copyright 2023, Proofcraft Pty Ltd + * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) + * + * SPDX-License-Identifier: BSD-2-Clause + *) + +(* Lemmas about no_throw. Usually should have a conclusion "no_throw P m". + Includes some monad equations that have no_throw as a main assumption. *) + +theory Trace_No_Throw + imports + Trace_VCG +begin + +section "Basic exception reasoning" + +text \ + The predicates @{text no_throw} and @{text no_return} allow us to reason about functions in + the exception monad that never throw an exception or never return normally.\ + +definition no_throw :: "('s \ bool) \ ('s, 'e + 'a) tmonad \ bool" where + "no_throw P A \ \ P \ A \ \_ _. True \,\ \_ _. False \" + +definition no_return :: "('a \ bool) \ ('a, 'b + 'c) tmonad \ bool" where + "no_return P A \ \ P \ A \\_ _. False\,\\_ _. True \" + +end \ No newline at end of file diff --git a/lib/Monads/trace/Trace_No_Trace.thy b/lib/Monads/trace/Trace_No_Trace.thy new file mode 100644 index 0000000000..5b59c87d72 --- /dev/null +++ b/lib/Monads/trace/Trace_No_Trace.thy @@ -0,0 +1,77 @@ +(* + * Copyright 2023, Proofcraft Pty Ltd + * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) + * + * SPDX-License-Identifier: BSD-2-Clause + *) + +theory Trace_No_Trace + imports + Trace_Monad + WPSimp +begin + +subsection "No Trace" + +text \ + A monad of type @{text tmonad} does not have a trace iff for all starting + states, all of the potential outcomes have the empty list as a trace and do + not return an @{term Incomplete} result.\ +definition no_trace :: "('s,'a) tmonad \ bool" where + "no_trace f = (\tr res s. (tr, res) \ f s \ tr = [] \ res \ Incomplete)" + +lemmas no_traceD = no_trace_def[THEN iffD1, rule_format] + +lemma no_trace_emp: + "\no_trace f; (tr, r) \ f s\ \ tr = []" + by (simp add: no_traceD) + +lemma no_trace_Incomplete_mem: + "no_trace f \ (tr, Incomplete) \ f s" + by (auto dest: no_traceD) + +lemma no_trace_Incomplete_eq: + "\no_trace f; (tr, res) \ f s\ \ res \ Incomplete" + by (auto dest: no_traceD) + + +subsection \Set up for @{method wp}\ + +lemma no_trace_is_triple[wp_trip]: + "no_trace f = triple_judgement \ f (\() f. id no_trace f)" + by (simp add: triple_judgement_def split: unit.split) + + +subsection \Rules\ + +lemma no_trace_prim: + "no_trace get" + "no_trace (put s)" + "no_trace (modify f)" + "no_trace (return v)" + "no_trace fail" + by (simp_all add: no_trace_def get_def put_def modify_def bind_def + return_def select_def fail_def) + +lemma no_trace_select: + "no_trace (select S)" + by (clarsimp simp add: no_trace_def select_def) + +lemma no_trace_bind: + "no_trace f \ \rv. no_trace (g rv) + \ no_trace (do rv \ f; g rv od)" + apply (subst no_trace_def) + apply (clarsimp simp add: bind_def split: tmres.split_asm; + auto dest: no_traceD[rotated]) + done + +lemma no_trace_extra: + "no_trace (gets f)" + "no_trace (assert P)" + "no_trace (assert_opt Q)" + by (simp_all add: gets_def assert_def assert_opt_def no_trace_bind no_trace_prim + split: option.split) + +lemmas no_trace_all[wp, iff] = no_trace_prim no_trace_select no_trace_extra + +end \ No newline at end of file diff --git a/lib/Monads/trace/Trace_RG.thy b/lib/Monads/trace/Trace_RG.thy new file mode 100644 index 0000000000..fb844d0f18 --- /dev/null +++ b/lib/Monads/trace/Trace_RG.thy @@ -0,0 +1,728 @@ +(* + * Copyright 2023, Proofcraft Pty Ltd + * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) + * + * SPDX-License-Identifier: BSD-2-Clause + *) + +theory Trace_RG + imports + Trace_VCG + Trace_Monad_Equations + Trace_No_Trace +begin + +section \Rely-Guarantee Logic\ + +subsection \Validity\ + +text \ + This section defines a Rely_Guarantee logic for partial correctness for + the interference trace monad. + + The logic is defined semantically. Rules work directly on the + validity predicate. + + In the interference trace monad, RG validity is a quintuple of precondition, + rely, monad, guarantee, and postcondition. The precondition is a function + from initial state to current state to bool (a state predicate), the rely and + guarantee are functions from state before to state after to bool, and the + postcondition is a function from return value to last state in the trace to + final state to bool. A quintuple is valid if for all initial and current + states that satisfy the precondition and all traces that satisfy the rely, + all of the pssible self steps performed by the monad satisfy the guarantee + and all of the result values and result states that are returned by the monad + satisfy the postcondition. Note that if the computation returns an empty + trace and no successful results then the quintuple is trivially valid. This + means @{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).\ + +primrec trace_steps :: "(tmid \ 's) list \ 's \ (tmid \ 's \ 's) set" where + "trace_steps (elem # trace) s0 = {(fst elem, s0, snd elem)} \ trace_steps trace (snd elem)" + | "trace_steps [] s0 = {}" + +lemma trace_steps_nth: + "trace_steps xs s0 = (\i. (fst (xs ! i), (if i = 0 then s0 else snd (xs ! (i - 1))), snd (xs ! i))) ` {..< length xs}" +proof (induct xs arbitrary: s0) + case Nil + show ?case by simp +next + case (Cons a xs) + show ?case + apply (simp add: lessThan_Suc_eq_insert_0 Cons image_image nth_Cons') + apply (intro arg_cong2[where f=insert] refl image_cong) + apply simp + done +qed + +text \rg_pred type: Rely-Guaranty predicates (state before => state after => bool)\ +type_synonym 's rg_pred = "'s \ 's \ bool" + +text \Abbreviations for trivial postconditions (taking three arguments):\ +abbreviation(input) + toptoptop :: "'a \ 'b \ 'b \ bool" ("\\\") where + "\\\ \ \_ _ _. True" + +abbreviation(input) + botbotbot :: "'a \ 'b \ 'b \ bool" ("\\\") where + "\\\ \ \_ _ _. False" + +text \ + Test whether the enironment steps in @{text tr} satisfy the rely condition @{text R}, + assuming that @{text s0s} was the initial state before the first step in the trace.\ +definition rely_cond :: "'s rg_pred \ 's \ (tmid \ 's) list \ bool" where + "rely_cond R s0s tr = (\(ident, s0, s) \ trace_steps (rev tr) s0s. ident = Env \ R s0 s)" + +text \ + Test whether the self steps in @{text tr} satisfy the guarantee condition @{text G}, + assuming that @{text s0s} was the initial state before the first step in the trace.\ +definition guar_cond :: "'s rg_pred \ 's \ (tmid \ 's) list \ bool" where + "guar_cond G s0s tr = (\(ident, s0, s) \ trace_steps (rev tr) s0s. ident = Me \ G s0 s)" + +lemma rg_empty_conds[simp]: + "rely_cond R s0s []" + "guar_cond G s0s []" + by (simp_all add: rely_cond_def guar_cond_def) + +text \ + @{text "rely f R s0s"} constructs a new function from @{text f}, where the environment + steps are constrained by @{text R} and @{text s0s} was the initial state before the first + step in the trace.\ +definition rely :: "('s, 'a) tmonad \ 's rg_pred \ 's \ ('s, 'a) tmonad" where + "rely f R s0s \ (\s. f s \ ({tr. rely_cond R s0s tr} \ UNIV))" + +definition prefix_closed :: "('s, 'a) tmonad \ bool" where + "prefix_closed f = (\s. \x xs. (x # xs) \ fst ` f s \ (xs, Incomplete) \ f s)" + +definition validI :: + "('s \ 's \ bool) \ 's rg_pred \ ('s,'a) tmonad \ 's rg_pred \ ('a \ 's \ 's \ bool) \ bool" + ("(\_\,/ \_\)/ _ /(\_\,/ \_\)") where + "\P\,\R\ f \G\,\Q\ \ + prefix_closed f + \ (\s0 s tr res. P s0 s \ (tr, res) \ (rely f R s0 s) + \ guar_cond G s0 tr + \ (\rv s'. res = Result (rv, s') \ Q rv (last_st_tr tr s0) s'))" + +(* +text \Validity for exception monad with interferences. Not as easy to phrase + as we need to \ +definition validIE :: "('s, 'a + 'b) tmonad \ + 's rg_pred \ + 's rg_pred \ 's rg_pred \ + ('b \ 's rg_pred) \ + ('a \ 's rg_pred) \ bool" + ("_ //PRE _//RELY _//GUAR _//POST _//EXC _" [59,0,0,0,0,0] 60) where + "validIE f P R G Q E \ f SAT [P,R,G,\v. case v of Inr r \ Q r | Inl e \ E e]" + +abbreviation (input) + validIEsat :: "('s, 'a + 'b) tmonad \ + 's rg_pred \ + 's rg_pred \ 's rg_pred \ + ('b \ 's rg_pred) \ + ('a \ 's rg_pred) \ bool" + ("_ //SAT [_, _, _, _, _]" [59,0,0,0,0,0] 60) + where + "validIEsat f P R G Q E \ validIE f P R G Q E" + *) + +lemma in_rely: + "\ (tr, res) \ f s; rely_cond R s0s tr \ \ (tr, res) \ rely f R s0s s" + by (simp add: rely_def) + +lemmas validI_D = + validI_def[THEN meta_eq_to_obj_eq, THEN iffD1, THEN conjunct2, rule_format, + OF _ conjI, OF _ _ in_rely] +lemmas validI_GD = validI_D[THEN conjunct1] +lemmas validI_rvD = validI_D[THEN conjunct2, rule_format, rotated -1, OF refl] +lemmas validI_prefix_closed = validI_def[THEN meta_eq_to_obj_eq, THEN iffD1, THEN conjunct1] +lemmas validI_prefix_closed_T = + validI_prefix_closed[where P="\_ _. False" and R="\_ _. False" and G="\_ _. True" + and Q="\_ _ _. True"] + +lemmas prefix_closedD1 = prefix_closed_def[THEN iffD1, rule_format] + +lemma in_fst_snd_image_eq: + "x \ fst ` S = (\y. (x, y) \ S)" + "y \ snd ` S = (\x. (x, y) \ S)" + by (auto elim: image_eqI[rotated]) + +lemma in_fst_snd_image: + "(x, y) \ S \ x \ fst ` S" + "(x, y) \ S \ y \ snd ` S" + by (auto simp: in_fst_snd_image_eq) + +lemmas prefix_closedD = prefix_closedD1[OF _ in_fst_snd_image(1)] + + +section \Lemmas\ + +lemma validI_weaken_pre: + "\\P'\,\R\ f \G\,\Q\; \s0 s. P s0 s \ P' s0 s\ + \ \P\,\R\ f \G\,\Q\" + by (simp add: validI_def, blast) + +lemma rely_weaken: + "\\s0 s. R s0 s \ R' s0 s; (tr, res) \ rely f R s s0\ + \ (tr, res) \ rely f R' s s0" + by (simp add: rely_def rely_cond_def, blast) + +lemma validI_weaken_rely: + "\\P\,\R'\ f \G\,\Q\; \s0 s. R s0 s \ R' s0 s\ + \ \P\,\R\ f \G\,\Q\" + apply (simp add: validI_def) + by (metis rely_weaken) + +lemmas validI_pre[wp_pre] = + validI_weaken_pre + validI_weaken_rely + +lemma validI_strengthen_post: + "\\P\,\R\ f \G\,\Q'\; \v s0 s. Q' v s0 s \ Q v s0 s\ + \ \P\,\R\ f \G\,\Q\" + by (simp add: validI_def) + +lemma validI_strengthen_guar: + "\\P\, \R\ f \G'\, \Q\; \s0 s. G' s0 s \ G s0 s\ + \ \P\, \R\ f \G\, \Q\" + by (force simp: validI_def guar_cond_def) + + +subsection \Setting up the precondition case splitter.\ + +(* FIXME: this needs adjustment, case_prod Q is unlikely to unify *) +lemma wpc_helper_validI: + "(\Q\,\R\ g \G\,\S\) \ wpc_helper (P, P', P'') (case_prod Q, Q', Q'') (\curry P\,\R\ g \G\,\S\)" + by (clarsimp simp: wpc_helper_def elim!: validI_weaken_pre) + +wpc_setup "\m. \P\,\R\ m \G\,\S\" wpc_helper_validI + + +subsection \RG Logic Rules\ + +lemma trace_steps_append: + "trace_steps (xs @ ys) s + = trace_steps xs s \ trace_steps ys (last_st_tr (rev xs) s)" + by (induct xs arbitrary: s, simp_all add: last_st_tr_def hd_append) + +lemma rely_cond_append: + "rely_cond R s (xs @ ys) = (rely_cond R s ys \ rely_cond R (last_st_tr ys s) xs)" + by (simp add: rely_cond_def trace_steps_append ball_Un conj_comms) + +lemma guar_cond_append: + "guar_cond G s (xs @ ys) = (guar_cond G s ys \ guar_cond G (last_st_tr ys s) xs)" + by (simp add: guar_cond_def trace_steps_append ball_Un conj_comms) + +lemma prefix_closed_bind: + "\prefix_closed f; \x. prefix_closed (g x)\ \ prefix_closed (f >>= g)" + apply (subst prefix_closed_def, clarsimp simp: bind_def) + apply (auto simp: Cons_eq_append_conv split: tmres.split_asm + dest!: prefix_closedD[rotated]; + fastforce elim: rev_bexI) + done + +lemmas prefix_closed_bind[rule_format, wp_split] + +lemma last_st_tr_append[simp]: + "last_st_tr (tr @ tr') s = last_st_tr tr (last_st_tr tr' s)" + by (simp add: last_st_tr_def hd_append) + +lemma last_st_tr_Nil[simp]: + "last_st_tr [] s = s" + by (simp add: last_st_tr_def) + +lemma last_st_tr_Cons[simp]: + "last_st_tr (x # xs) s = snd x" + by (simp add: last_st_tr_def) + +lemma bind_twp[wp_split]: + "\ \r. \Q' r\,\R\ g r \G\,\Q\; \P\,\R\ f \G\,\Q'\ \ + \ \P\,\R\ f >>= (\r. g r) \G\,\Q\" + apply (subst validI_def, rule conjI) + apply (blast intro: prefix_closed_bind validI_prefix_closed) + apply (clarsimp simp: bind_def rely_def) + apply (drule(2) validI_D) + apply (clarsimp simp: rely_cond_append split: tmres.split_asm) + apply (clarsimp split: tmres.split_asm) + apply (drule meta_spec, frule(2) validI_D) + apply (clarsimp simp: rely_cond_append split: if_split_asm) + apply (clarsimp simp: guar_cond_append) + done + +lemma trace_steps_rev_drop_nth: + "trace_steps (rev (drop n tr)) s + = (\i. (fst (rev tr ! i), (if i = 0 then s else snd (rev tr ! (i - 1))), + snd (rev tr ! i))) ` {..< length tr - n}" + apply (simp add: trace_steps_nth) + apply (intro image_cong refl) + apply (simp add: rev_nth) + done + +lemma prefix_closed_drop: + "\(tr, res) \ f s; prefix_closed f\ \ \res'. (drop n tr, res') \ f s" +proof (induct n arbitrary: res) + case 0 then show ?case by auto +next + case (Suc n) + have drop_1: "\tr res. (tr, res) \ f s \ \res'. (drop 1 tr, res') \ f s" + by (case_tac tr; fastforce dest: prefix_closedD[rotated] intro: Suc) + show ?case + using Suc.hyps[OF Suc.prems] + by (metis drop_1[simplified] drop_drop add_0 add_Suc) +qed + +lemma validI_GD_drop: + "\ \P\, \R\ f \G\, \Q\; P s0 s; (tr, res) \ f s; + rely_cond R s0 (drop n tr) \ + \ guar_cond G s0 (drop n tr)" + apply (drule prefix_closed_drop[where n=n], erule validI_prefix_closed) + apply (auto dest: validI_GD) + done + +lemma parallel_prefix_closed[wp_split]: + "\prefix_closed f; prefix_closed g\ + \ prefix_closed (parallel f g)" + apply (subst prefix_closed_def, clarsimp simp: parallel_def) + apply (case_tac f_steps; clarsimp) + apply (drule(1) prefix_closedD)+ + apply fastforce + done + +lemma rely_cond_drop: + "rely_cond R s0 xs \ rely_cond R s0 (drop n xs)" + using rely_cond_append[where xs="take n xs" and ys="drop n xs"] + by simp + +lemma rely_cond_is_drop: + "\rely_cond R s0 xs; (ys = drop (length xs - length ys) xs)\ + \ rely_cond R s0 ys" + by (metis rely_cond_drop) + +lemma bounded_rev_nat_induct: + "\(\n. N \ n \ P n); \n. \n < N; P (Suc n)\ \ P n\ + \ P n" + by (induct diff\"N - n" arbitrary: n; simp) + +lemma drop_n_induct: + "\P []; \n. \n < length xs; P (drop (Suc n) xs)\ \ P (drop n xs)\ + \ P (drop n xs)" + by (induct len\"length (drop n xs)" arbitrary: n xs; simp) + +lemma guar_cond_Cons_eq: + "guar_cond R s0 (x # xs) + = (guar_cond R s0 xs \ (fst x \ Env \ R (last_st_tr xs s0) (snd x)))" + by (cases "fst x"; simp add: guar_cond_def trace_steps_append conj_comms) + +lemma guar_cond_Cons: + "\guar_cond R s0 xs; fst x \ Env \ R (last_st_tr xs s0) (snd x)\ + \ guar_cond R s0 (x # xs)" + by (simp add: guar_cond_Cons_eq) + +lemma guar_cond_drop_Suc_eq: + "n < length xs + \ guar_cond R s0 (drop n xs) = (guar_cond R s0 (drop (Suc n) xs) + \ (fst (xs ! n) \ Env \ R (last_st_tr (drop (Suc n) xs) s0) (snd (xs ! n))))" + apply (rule trans[OF _ guar_cond_Cons_eq]) + apply (simp add: Cons_nth_drop_Suc) + done + +lemma guar_cond_drop_Suc: + "\guar_cond R s0 (drop (Suc n) xs); + fst (xs ! n) \ Env \ R (last_st_tr (drop (Suc n) xs) s0) (snd (xs ! n))\ + \ guar_cond R s0 (drop n xs)" + by (case_tac "n < length xs"; simp add: guar_cond_drop_Suc_eq) + +lemma rely_cond_Cons_eq: + "rely_cond R s0 (x # xs) + = (rely_cond R s0 xs \ (fst x = Env \ R (last_st_tr xs s0) (snd x)))" + by (simp add: rely_cond_def trace_steps_append conj_comms) + +lemma rely_cond_Cons: + "\rely_cond R s0 xs; fst x = Env \ R (last_st_tr xs s0) (snd x)\ + \ rely_cond R s0 (x # xs)" + by (simp add: rely_cond_Cons_eq) + +lemma rely_cond_drop_Suc_eq: + "n < length xs + \ rely_cond R s0 (drop n xs) = (rely_cond R s0 (drop (Suc n) xs) + \ (fst (xs ! n) = Env \ R (last_st_tr (drop (Suc n) xs) s0) (snd (xs ! n))))" + apply (rule trans[OF _ rely_cond_Cons_eq]) + apply (simp add: Cons_nth_drop_Suc) + done + +lemma rely_cond_drop_Suc: + "\rely_cond R s0 (drop (Suc n) xs); + fst (xs ! n) = Env \ R (last_st_tr (drop (Suc n) xs) s0) (snd (xs ! n))\ + \ rely_cond R s0 (drop n xs)" + by (cases "n < length xs"; simp add: rely_cond_drop_Suc_eq) + +lemma last_st_tr_map_zip_hd: + "\length flags = length tr; tr \ [] \ snd (f (hd flags, hd tr)) = snd (hd tr)\ + \ last_st_tr (map f (zip flags tr)) = last_st_tr tr" + apply (cases tr; simp) + apply (cases flags; simp) + apply (simp add: fun_eq_iff) + done + +lemma last_st_tr_drop_map_zip_hd: + "\length flags = length tr; + n < length tr \ snd (f (flags ! n, tr ! n)) = snd (tr ! n)\ + \ last_st_tr (drop n (map f (zip flags tr))) = last_st_tr (drop n tr)" + apply (simp add: drop_map drop_zip) + apply (rule last_st_tr_map_zip_hd; clarsimp) + apply (simp add: hd_drop_conv_nth) + done + +lemma last_st_tr_map_zip: + "\length flags = length tr; \fl tmid s. snd (f (fl, (tmid, s))) = s\ + \ last_st_tr (map f (zip flags tr)) = last_st_tr tr" + apply (erule last_st_tr_map_zip_hd) + apply (clarsimp simp: neq_Nil_conv) + done + +lemma parallel_rely_induct: + assumes preds: "(tr, v) \ parallel f g s" "Pf s0 s" "Pg s0 s" + and validI: "\Pf\,\Rf\ f' \Gf\,\Qf\" + "\Pg\,\Rg\ g' \Gg\,\Qg\" + "f s \ f' s" "g s \ g' s" + and compat: "R \ Rf" "R \ Rg" "Gf \ G" "Gg \ G" "Gf \ Rg" "Gg \ Rf" + and rely: "rely_cond R s0 (drop n tr)" + shows + "\tr_f tr_g. (tr_f, v) \ f s \ (tr_g, v) \ g s + \ rely_cond Rf s0 (drop n tr_f) \ rely_cond Rg s0 (drop n tr_g) + \ map snd tr_f = map snd tr \ map snd tr_g = map snd tr + \ (\i \ length tr. last_st_tr (drop i tr_g) s0 = last_st_tr (drop i tr_f) s0) + \ guar_cond G s0 (drop n tr)" + (is "\ys zs. _ \ _ \ ?concl ys zs") +proof - + obtain ys zs where tr: "tr = map parallel_mrg (zip ys zs)" + and all2: "list_all2 (\y z. (fst y = Env \ fst z = Env) \ snd y = snd z) ys zs" + and ys: "(ys, v) \ f s" and zs: "(zs, v) \ g s" + using preds + by (clarsimp simp: parallel_def2) + note len[simp] = list_all2_lengthD[OF all2] + + have ys': "(ys, v) \ f' s" and zs': "(zs, v) \ g' s" + using ys zs validI by auto + + note rely_f_step = validI_GD_drop[OF validI(1) preds(2) ys' rely_cond_drop_Suc] + note rely_g_step = validI_GD_drop[OF validI(2) preds(3) zs' rely_cond_drop_Suc] + + note snd[simp] = list_all2_nthD[OF all2, THEN conjunct2] + + have "?concl ys zs" + using rely tr all2 rely_f_step rely_g_step + apply (induct n rule: bounded_rev_nat_induct) + apply (subst drop_all, assumption) + apply clarsimp + apply (simp add: list_all2_conv_all_nth last_st_tr_def drop_map[symmetric] + hd_drop_conv_nth hd_append) + apply (fastforce simp: split_def intro!: nth_equalityI) + apply clarsimp + apply (erule_tac x=n in meta_allE)+ + apply (drule meta_mp, erule rely_cond_is_drop, simp) + apply (subst(asm) rely_cond_drop_Suc_eq[where xs="map f xs" for f xs], simp) + apply (clarsimp simp: last_st_tr_drop_map_zip_hd if_split[where P="\x. x = Env"] + split_def) + apply (intro conjI; (rule guar_cond_drop_Suc rely_cond_drop_Suc, assumption)) + apply (auto simp: guar_cond_drop_Suc_eq last_st_tr_drop_map_zip_hd + intro: compat[THEN predicate2D]) + done + + thus ?thesis + using ys zs + by auto +qed + +lemmas parallel_rely_induct0 = parallel_rely_induct[where n=0, simplified] + +lemma rg_validI: + assumes validI: "\Pf\,\Rf\ f \Gf\,\Qf\" + "\Pg\,\Rg\ g \Gg\,\Qg\" + and compat: "R \ Rf" "R \ Rg" "Gf \ G" "Gg \ G" "Gf \ Rg" "Gg \ Rf" + shows "\Pf and Pg\,\R\ parallel f g \G\,\\rv. Qf rv and Qg rv\" + apply (clarsimp simp: validI_def rely_def pred_conj_def + parallel_prefix_closed validI[THEN validI_prefix_closed]) + apply (drule(3) parallel_rely_induct0[OF _ _ _ validI order_refl order_refl compat]) + apply clarsimp + apply (drule(2) validI[THEN validI_rvD])+ + apply (simp add: last_st_tr_def) + done + +lemma rely_prim[simp]: + "rely (\s. insert (v s) (f s)) R s0 = (\s. {x. x = v s \ rely_cond R s0 (fst x)} \ (rely f R s0 s))" + "rely (\s. {}) R s0 = (\_. {})" + by (auto simp: rely_def prod_eq_iff) + +lemma prefix_closed_put_trace_elem[iff]: + "prefix_closed (put_trace_elem x)" + by (clarsimp simp: prefix_closed_def put_trace_elem_def) + +lemma prefix_closed_return[iff]: + "prefix_closed (return x)" + by (simp add: prefix_closed_def return_def) + +lemma prefix_closed_put_trace[iff]: + "prefix_closed (put_trace tr)" + by (induct tr; clarsimp simp: prefix_closed_bind) + +lemma put_trace_eq_drop: + "put_trace xs s + = ((\n. (drop n xs, if n = 0 then Result ((), s) else Incomplete)) ` {.. length xs})" + apply (induct xs) + apply (clarsimp simp: return_def) + apply (clarsimp simp: put_trace_elem_def bind_def) + apply (simp add: atMost_Suc_eq_insert_0 image_image) + apply (rule equalityI; clarsimp) + apply (split if_split_asm; clarsimp) + apply (auto intro: image_eqI[where x=0])[1] + apply (rule rev_bexI, simp) + apply clarsimp + done + +lemma put_trace_res: + "(tr, res) \ put_trace xs s + \ \n. tr = drop n xs \ n \ length xs + \ res = (case n of 0 \ Result ((), s) | _ \ Incomplete)" + apply (clarsimp simp: put_trace_eq_drop) + apply (case_tac n; auto intro: exI[where x=0]) + done + +lemma put_trace_twp[wp]: + "\\s0 s. (\n. rely_cond R s0 (drop n xs) \ guar_cond G s0 (drop n xs)) + \ (rely_cond R s0 xs \ Q () (last_st_tr xs s0) s)\,\R\ + put_trace xs + \G\,\Q\" + apply (clarsimp simp: validI_def rely_def) + apply (drule put_trace_res) + apply (clarsimp; clarsimp split: nat.split_asm) + done + +lemmas put_trace_elem_twp = put_trace_twp[where xs="[x]" for x, simplified] + +lemma prefix_closed_select[iff]: + "prefix_closed (select S)" + by (simp add: prefix_closed_def select_def image_def) + +lemma rely_cond_rtranclp: + "rely_cond R s (map (Pair Env) xs) \ rtranclp R s (last_st_tr (map (Pair Env) xs) s)" + apply (induct xs arbitrary: s rule: rev_induct) + apply simp + apply (clarsimp simp add: rely_cond_def) + apply (erule converse_rtranclp_into_rtranclp) + apply simp + done + + +subsection \Setting up the @{method wp} method\ + +(* Attempt to define triple_judgement to use valid_validI_wp as wp_comb rule. + It doesn't work. It seems that wp_comb rules cannot take more than 1 assumption *) +lemma validI_is_triple[wp_trip]: + "\P\,\R\ f \G\,\Q\ + = triple_judgement (\(s0, s). prefix_closed f \ P s0 s) f + (\(s0,s) f. prefix_closed f \ (\tr res. (tr, res) \ rely f R s0 s + \ guar_cond G s0 tr + \ (\rv s'. res = Result (rv, s') \ Q rv (last_st_tr tr s0) s')))" + apply (simp add: triple_judgement_def validI_def ) + apply (cases "prefix_closed f"; fastforce) + done + +lemma no_trace_prefix_closed: + "no_trace f \ prefix_closed f" + by (auto simp add: prefix_closed_def dest: no_trace_emp) + +lemma valid_validI_wp[wp_comb]: + "\no_trace f; \s0. \P s0\ f \\v. Q v s0 \\ + \ \P\,\R\ f \G\,\Q\" + by (fastforce simp: rely_def validI_def valid_def mres_def no_trace_prefix_closed dest: no_trace_emp + elim: image_eqI[rotated]) + + +lemma env_steps_twp[wp]: + "\\s0 s. (\s'. R\<^sup>*\<^sup>* s0 s' \ Q () s' s') \ Q () s0 s\,\R\ env_steps \G\,\Q\" + apply (simp add: interference_def env_steps_def) + apply wp + apply (clarsimp simp: guar_cond_def trace_steps_rev_drop_nth rev_nth) + apply (drule rely_cond_rtranclp) + apply (clarsimp simp add: last_st_tr_def hd_append) + done + +lemma interference_twp[wp]: + "\\s0 s. (\s'. R\<^sup>*\<^sup>* s s' \ Q () s' s') \ G s0 s\,\R\ interference \G\,\Q\" + apply (simp add: interference_def commit_step_def del: put_trace.simps) + apply wp + apply clarsimp + apply (simp add: drop_Cons nat.split rely_cond_def guar_cond_def) + done + +(* what Await does if we haven't committed our step is a little + strange. this assumes we have, which means s0 = s. we should + revisit this if we find a use for Await when this isn't the + case *) +lemma Await_sync_twp: + "\\s0 s. s = s0 \ (\x. R\<^sup>*\<^sup>* s0 x \ c x \ Q () x x)\,\R\ Await c \G\,\Q\" + apply (simp add: Await_def split_def) + apply wp + apply clarsimp + apply (clarsimp simp: guar_cond_def trace_steps_rev_drop_nth rev_nth) + apply (drule rely_cond_rtranclp) + apply (simp add: o_def) + done + +lemma mres_union: + "mres (a \ b) = mres a \ mres b" + by (simp add: mres_def image_Un) + +lemma mres_Failed_empty: + "mres ((\xs. (xs, Failed)) ` X ) = {}" + "mres ((\xs. (xs, Incomplete)) ` X ) = {}" + by (auto simp add: mres_def image_def) + +lemma det_set_option_eq: + "(\a\m. set_option (snd a)) = {(r, s')} \ + (ts, Some (rr, ss)) \ m \ rr = r \ ss = s'" + by (metis UN_I option.set_intros prod.inject singleton_iff snd_conv) + +lemma det_set_option_eq': + "(\a\m. set_option (snd a)) = {(r, s')} \ + Some (r, s') \ snd ` m" + using image_iff by fastforce + +lemma validI_name_pre: + "prefix_closed f \ + (\s0 s. P s0 s \ \\s0' s'. s0' = s0 \ s' = s\,\R\ f \G\,\Q\) + \ \P\,\R\ f \G\,\Q\" + unfolding validI_def + by metis + +lemma validI_well_behaved': + "\prefix_closed f; \P\,\R'\ f \G'\,\Q\; R \ R'; G' \ G\ + \ \P\,\R\ f \G\,\Q\" + apply (subst validI_def, clarsimp) + apply (clarsimp simp add: rely_def) + apply (drule (2) validI_D) + apply (fastforce simp: rely_cond_def guar_cond_def)+ + done + +lemmas validI_well_behaved = validI_well_behaved'[unfolded le_fun_def, simplified] + +lemma prefix_closed_mapM[rule_format, wp_split]: + "(\x \ set xs. prefix_closed (f x)) \ prefix_closed (mapM f xs)" + apply (induct xs) + apply (simp add: mapM_def sequence_def) + apply (clarsimp simp: mapM_Cons) + apply (intro prefix_closed_bind allI; clarsimp) + done + +lemmas bind_promote_If = + if_distrib[where f="\f. bind f g" for g] + if_distrib[where f="\g. bind f g" for f] + +lemma bind_promote_If2: + "do x \ f; if P then g x else h x od + = (if P then bind f g else bind f h)" + by simp + +lemma exec_put_trace[unfolded K_bind_def]: + "(do put_trace xs; f od) s + = (\n \ {n. 0 < n \ n \ length xs}. {(drop n xs, Incomplete)}) + \ ((\(a, b). (a @ xs, b)) ` f s)" + apply (simp add: put_trace_eq_drop bind_def) + apply (safe; (clarsimp split: if_split_asm)?; + fastforce intro: bexI[where x=0] rev_bexI) + done + +lemma UN_If_distrib: + "(\x \ S. if P x then A x else B x) + = ((\x \ S \ {x. P x}. A x) \ (\x \ S \ {x. \ P x}. B x))" + by (fastforce split: if_split_asm) + +lemma Await_redef: + "Await P = do + s1 \ select {s. P s}; + env_steps; + s \ get; + select (if P s then {()} else {}) + od" + apply (simp add: Await_def env_steps_def bind_assoc) + apply (cases "{s. P s} = {}") + apply (simp add: select_def bind_def get_def) + apply (rule ext) + apply (simp add: exec_get select_bind_UN put_then_get_then) + apply (simp add: bind_promote_If2 if_distribR if_distrib[where f=select]) + apply (simp add: exec_put_trace cong: if_cong) + apply (simp add: put_def bind_def select_def cong: if_cong) + apply (strengthen equalityI) + apply clarsimp + apply (strengthen exI[where x="s # xs" for s xs]) + apply (strengthen exI[where x="Suc n" for n]) + apply simp + apply blast + done + +lemma eq_Me_neq_Env: + "(x = Me) = (x \ Env)" + by (cases x; simp) + +lemma validI_invariant_imp: + assumes v: "\P\,\R\ f \G\,\Q\" + and P: "\s0 s. P s0 s \ I s0" + and R: "\s0 s. I s0 \ R s0 s \ I s" + and G: "\s0 s. I s0 \ G s0 s \ I s" + shows "\P\,\R\ f \\s0 s. I s0 \ I s \ G s0 s\,\\rv s0 s. I s0 \ Q rv s0 s\" +proof - + { fix tr s0 i + assume r: "rely_cond R s0 tr" and g: "guar_cond G s0 tr" + and I: "I s0" + hence imp: "\(_, s, s') \ trace_steps (rev tr) s0. I s \ I s'" + apply (clarsimp simp: guar_cond_def rely_cond_def) + apply (drule(1) bspec)+ + apply (clarsimp simp: eq_Me_neq_Env) + apply (metis R G) + done + hence "i < length tr \ I (snd (rev tr ! i))" + using I + apply (induct i) + apply (clarsimp simp: neq_Nil_conv[where xs="rev tr" for tr, simplified]) + apply clarsimp + apply (drule bspec, fastforce simp add: trace_steps_nth) + apply simp + done + } + note I = this + show ?thesis + using v + apply (clarsimp simp: validI_def rely_def imp_conjL) + apply (drule spec2, drule(1) mp)+ + apply clarsimp + apply (frule P[rule_format]) + apply (clarsimp simp: guar_cond_def trace_steps_nth I last_st_tr_def + hd_append last_rev[symmetric] + last_conv_nth rev_map) + done +qed + +lemma validI_guar_post_conj_lift: + "\\P\,\R\ f \G1\,\Q1\; \P\,\R\ f \G2\,\Q2\\ + \ \P\,\R\ f \\s0 s. G1 s0 s \ G2 s0 s\,\\rv s0 s. Q1 rv s0 s \ Q2 rv s0 s\" + apply (frule validI_prefix_closed) + apply (subst validI_def, clarsimp simp: rely_def) + apply (drule(3) validI_D)+ + apply (auto simp: guar_cond_def) + done + +lemmas modify_prefix_closed[simp] = + modify_wp[THEN valid_validI_wp[OF no_trace_all(3)], THEN validI_prefix_closed] +lemmas await_prefix_closed[simp] = Await_sync_twp[THEN validI_prefix_closed] + +lemma repeat_prefix_closed[intro!]: + "prefix_closed f \ prefix_closed (repeat f)" + apply (simp add: repeat_def) + apply (rule prefix_closed_bind; clarsimp) + apply (rename_tac n) + apply (induct_tac n; simp) + apply (auto intro: prefix_closed_bind) + done + +end \ No newline at end of file diff --git a/lib/Monads/trace/Trace_Sat.thy b/lib/Monads/trace/Trace_Sat.thy new file mode 100644 index 0000000000..2f40ec7b78 --- /dev/null +++ b/lib/Monads/trace/Trace_Sat.thy @@ -0,0 +1,111 @@ +(* + * Copyright 2023, Proofcraft Pty Ltd + * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) + * + * SPDX-License-Identifier: BSD-2-Clause + *) + +theory Trace_Sat + imports + Trace_Monad + WPSimp +begin + +section \Satisfiability\ + +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 + "\P\ f \\Q\ \ \s. P s \ (\(rv, s') \ mres (f s). Q rv s')" + +text \The above for the exception monad\ +definition ex_exs_validE :: + "('a \ bool) \ ('a, 'e + 'b) tmonad \ ('b \ 'a \ bool) \ ('e \ 'a \ bool) \ bool" + ("\_\ _ \\_\, \_\") where + "\P\ f \\Q\, \E\ \ \P\ f \\\rv. case rv of Inl e \ E e | Inr v \ Q v\" + + +subsection \Set up for @{method wp}\ + +definition exs_postcondition where + "exs_postcondition P f \ \a b. \(rv, s) \ f a b. P rv s" + +lemma exs_valid_is_triple[wp_trip]: + "exs_valid P f Q = triple_judgement P f (exs_postcondition Q (\s f. mres (f s)))" + by (simp add: triple_judgement_def exs_postcondition_def exs_valid_def) + + +subsection \Rules\ + +lemma exs_hoare_post_imp: + "\\r s. Q r s \ R r s; \P\ a \\Q\\ \ \P\ a \\R\" + unfolding exs_valid_def by blast + +lemma use_exs_valid: + "\ \P\ f \\Q\; P s \ \ \(r, s') \ mres (f s). Q r s'" + by (simp add: exs_valid_def) + +lemma exs_valid_weaken_pre[wp_pre]: + "\ \P'\ f \\Q\; \s. P s \ P' s \ \ \P\ f \\Q\" + by (clarsimp simp: exs_valid_def) + +lemma exs_valid_chain: + "\ \P\ f \\Q\; \s. R s \ P s; \r s. Q r s \ S r s \ \ \R\ f \\S\" + by (fastforce simp: exs_valid_def Bex_def) + +lemma exs_valid_assume_pre: + "\ \s. P s \ \P\ f \\Q\ \ \ \P\ f \\Q\" + by (fastforce simp: exs_valid_def) + +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 (drule spec, drule(1) mp, clarsimp) + apply (drule spec2, drule(1) mp, clarsimp) + apply (simp add: image_def bex_Un) + apply (strengthen subst[where P="\x. x \ f s" for s, mk_strg I _ E], simp) + apply (fastforce elim: rev_bexI) + done + +lemma exs_valid_return[wp]: + "\Q v\ return v \\Q\" + by (clarsimp simp: exs_valid_def return_def mres_def) + +lemma exs_valid_select[wp]: + "\\s. \r \ S. Q r s\ select S \\Q\" + apply (clarsimp simp: exs_valid_def select_def mres_def) + apply (auto simp add: image_def) + done + +lemma exs_valid_get[wp]: + "\\s. Q s s\ get \\ Q \" + by (clarsimp simp: exs_valid_def get_def mres_def) + +lemma exs_valid_gets[wp]: + "\\s. Q (f s) s\ gets f \\Q\" + by (clarsimp simp: gets_def) wp + +lemma exs_valid_put[wp]: + "\Q v\ put v \\Q\" + by (clarsimp simp: put_def exs_valid_def mres_def) + +lemma exs_valid_fail[wp]: + "\\s. False\ fail \\Q\" + unfolding fail_def exs_valid_def + by simp + +lemma exs_valid_state_assert[wp]: + "\ \s. Q () s \ G s \ state_assert G \\ Q \" + by (clarsimp simp: state_assert_def exs_valid_def get_def + assert_def bind_def2 return_def mres_def) + +lemmas exs_valid_guard = exs_valid_state_assert + +lemma exs_valid_condition[wp]: + "\ \P\ l \\Q\; \P'\ r \\Q\ \ \ \\s. (C s \ P s) \ (\ C s \ P' s)\ condition C l r \\Q\" + by (clarsimp simp: condition_def exs_valid_def split: sum.splits) + +end \ No newline at end of file diff --git a/lib/Monads/trace/Trace_Strengthen_Setup.thy b/lib/Monads/trace/Trace_Strengthen_Setup.thy new file mode 100644 index 0000000000..024d370f8b --- /dev/null +++ b/lib/Monads/trace/Trace_Strengthen_Setup.thy @@ -0,0 +1,46 @@ +(* + * Copyright 2023, Proofcraft Pty Ltd + * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) + * + * SPDX-License-Identifier: BSD-2-Clause + *) + +theory Trace_Strengthen_Setup + imports + Strengthen + Trace_No_Fail + Trace_RG +begin + +section \Strengthen setup.\ + +context strengthen_implementation begin + +lemma strengthen_hoare[strg]: + "\\r s. st F (\) (Q r s) (R r s)\ + \ st F (\) (\P\ f \Q\) (\P\ f \R\)" + by (cases F, auto elim: hoare_strengthen_post) + +lemma strengthen_validE_R_cong[strg]: + "\\r s. st F (\) (Q r s) (R r s)\ + \ st F (\) (\P\ f \Q\, -) (\P\ f \R\, -)" + by (cases F, auto intro: hoare_post_imp_R) + +lemma strengthen_validE_cong[strg]: + "\\r s. st F (\) (Q r s) (R r s); \r s. st F (\) (S r s) (T r s)\ + \ st F (\) (\P\ f \Q\, \S\) (\P\ f \R\, \T\)" + by (cases F, auto elim: hoare_post_impErr) + +lemma strengthen_validE_E_cong[strg]: + "\\r s. st F (\) (S r s) (T r s)\ + \ st F (\) (\P\ f -, \S\) (\P\ f -, \T\)" + by (cases F, auto elim: hoare_post_impErr simp: validE_E_def) + +lemma strengthen_validI[strg]: + "\\r s0 s. st F (\) (Q r s0 s) (Q' r s0 s)\ + \ st F (\) (\P\,\G\ f \R\,\Q\) (\P\,\G\ f \R\,\Q'\)" + by (cases F, auto elim: validI_strengthen_post) + +end + +end \ No newline at end of file diff --git a/lib/Monads/trace/Trace_Total.thy b/lib/Monads/trace/Trace_Total.thy new file mode 100644 index 0000000000..97c804807c --- /dev/null +++ b/lib/Monads/trace/Trace_Total.thy @@ -0,0 +1,346 @@ +(* + * Copyright 2023, Proofcraft Pty Ltd + * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) + * + * SPDX-License-Identifier: BSD-2-Clause + *) + +(* Total correctness Hoare logic for the Trace_Monad (= valid + no_fail) *) + +theory Trace_Total + imports Trace_No_Fail +begin + +section \Total correctness for Trace_Monad and Trace_Monad with exceptions\ + +subsection Definitions + +text \ + It is often desired to prove non-failure and a Hoare triple simultaneously, as the reasoning + is often similar. The following definitions allow such reasoning to take place.\ + +definition validNF :: + "('s \ bool) \ ('s,'a) tmonad \ ('a \ 's \ bool) \ bool" ("\_\/ _ /\_\!") where + "\P\ f \Q\! \ \P\ f \Q\ \ no_fail P f" + +lemma validNF_alt_def: + "\P\ f \Q\! = (\s. P s \ ((\(r', s') \ mres (f s). Q r' s') \ Failed \ snd ` (f s)))" + by (auto simp: validNF_def valid_def no_fail_def) + +definition validE_NF :: + "('s \ bool) \ ('s, 'a + 'b) tmonad \ ('b \ 's \ bool) \ ('a \ 's \ bool) \ bool" + ("\_\/ _ /(\_\,/ \_\!)") where + "\P\ f \Q\, \E\! \ \P\ f \Q\, \E\ \ no_fail P f" + +lemma validE_NF_alt_def: + "\P\ f \Q\, \E\! = \P\ f \\v s. case v of Inl e \ E e s | Inr r \ Q r s\!" + by (clarsimp simp: validE_NF_def validE_def validNF_def) + + +subsection \@{method wpc} setup\ + +lemma wpc_helper_validNF: + "\Q\ g \S\! \ wpc_helper (P, P', P'') (Q, Q', Q'') \P\ g \S\!" + unfolding wpc_helper_def + by clarsimp (metis hoare_vcg_precond_imp no_fail_pre validNF_def) + +wpc_setup "\m. \P\ m \Q\!" wpc_helper_validNF + + +subsection \Basic @{const validNF} theorems\ + +lemma validNF[intro?]: (* FIXME lib: should be validNFI *) + "\ \ P \ f \ Q \; no_fail P f \ \ \ P \ f \ Q \!" + by (clarsimp simp: validNF_def) + +lemma validNF_valid: + "\ \ P \ f \ Q \! \ \ \ P \ f \ Q \" + by (clarsimp simp: validNF_def) + +lemma validNF_no_fail: + "\ \ P \ f \ Q \! \ \ no_fail P f" + by (clarsimp simp: validNF_def) + +lemma snd_validNF: + "\ \ P \ f \ Q \!; P s \ \ Failed \ snd ` (f s)" + by (clarsimp simp: validNF_def no_fail_def) + +lemma use_validNF: + "\ (r', s') \ mres (f s); \ P \ f \ Q \!; P s \ \ Q r' s'" + by (fastforce simp: validNF_def valid_def) + + +subsection \@{const validNF} weakest precondition rules\ + +lemma validNF_return[wp]: + "\ P x \ return x \ P \!" + by (wp validNF)+ + +lemma validNF_get[wp]: + "\ \s. P s s \ get \ P \!" + by (wp validNF)+ + +lemma validNF_put[wp]: + "\ \s. P () x \ put x \ P \!" + by (wp validNF)+ + +lemma validNF_K_bind[wp]: + "\ P \ x \ Q \! \ \ P \ K_bind x f \ Q \!" + by simp + +lemma validNF_fail[wp]: + "\ \s. False \ fail \ Q \!" + by (clarsimp simp: validNF_def fail_def no_fail_def) + +lemma validNF_prop[wp_unsafe]: + "\ no_fail (\s. P) f \ \ \ \s. P \ f \ \rv s. P \!" + by (wp validNF)+ + +lemma validNF_post_conj[intro!]: + "\ \ P \ a \ Q \!; \ P \ a \ R \! \ \ \ P \ a \ Q and R \!" + by (auto simp: validNF_def) + +lemma validNF_pre_disj[intro!]: + "\ \ P \ a \ R \!; \ Q \ a \ R \! \ \ \ P or Q \ a \ R \!" + by (rule validNF) (auto dest: validNF_valid validNF_no_fail intro: no_fail_or) + +text \ + Set up combination rules for @{method wp}, which also requires a @{text wp_trip} rule for + @{const validNF}.\ +definition validNF_property :: "('a \ 's \ bool) \ 's \ ('s,'a) tmonad \ bool" where + "validNF_property Q s b \ Failed \ snd ` (b s) \ (\(r', s') \ mres (b s). Q r' s')" + +lemma validNF_is_triple[wp_trip]: + "validNF P f Q = triple_judgement P f (validNF_property Q)" + by (auto simp: validNF_def triple_judgement_def validNF_property_def no_fail_def valid_def) + +lemma validNF_weaken_pre[wp_pre]: + "\\Q\ a \R\!; \s. P s \ Q s\ \ \P\ a \R\!" + by (metis hoare_pre_imp no_fail_pre validNF_def) + +lemma validNF_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 (fastforce simp: validNF_def valid_def) + +lemma validNF_post_comb_conj_L: + "\ \P'\ f \Q\!; \P\ f \Q'\ \ \ \\s. P s \ P' s \ f \\rv s. Q rv s \ Q' rv s\!" + by (fastforce simp: validNF_def valid_def no_fail_def) + +lemma validNF_post_comb_conj_R: + "\ \P'\ f \Q\; \P\ f \Q'\! \ \ \\s. P s \ P' s \ f \\rv s. Q rv s \ Q' rv s\!" + by (fastforce simp: validNF_def valid_def no_fail_def) + +lemma validNF_post_comb_conj: + "\ \P'\ f \Q\!; \P\ f \Q'\! \ \ \\s. P s \ P' s \ f \\rv s. Q rv s \ Q' rv s\!" + by (fastforce simp: validNF_def valid_def no_fail_def) + +lemma validNF_if_split[wp_split]: + "\P \ \Q\ f \S\!; \ P \ \R\ g \S\!\ \ + \\s. (P \ Q s) \ (\ P \ R s)\ if P then f else g \S\!" + by simp + +lemma validNF_vcg_conj_lift: + "\ \P\ f \Q\!; \P'\ f \Q'\! \ \ \\s. P s \ P' s\ f \\rv s. Q rv s \ Q' rv s\!" + by (fastforce intro!: validNF_post_conj[unfolded pred_conj_def] intro: validNF_weaken_pre) + +lemma validNF_vcg_disj_lift: + "\ \P\ f \Q\!; \P'\ f \Q'\! \ \ \\s. P s \ P' s\ f \\rv s. Q rv s \ Q' rv s\!" + by (auto simp: validNF_def no_fail_def intro!: hoare_vcg_disj_lift) + +lemma validNF_vcg_all_lift[wp]: + "\ \x. \P x\ f \Q x\! \ \ \\s. \x. P x s\ f \\rv s. \x. Q x rv s\!" + by (auto simp: validNF_def no_fail_def intro!: hoare_vcg_all_lift) + +lemma validNF_bind[wp_split]: + "\ \x. \B x\ g x \C\!; \A\ f \B\! \ \ \A\ do x \ f; g x od \C\!" + unfolding validNF_def + by (auto intro: hoare_seq_ext no_fail_bind[where P=Q and Q=Q for Q, simplified]) + +lemmas validNF_seq_ext = validNF_bind + + +subsection "validNF compound rules" + +lemma validNF_state_assert[wp]: + "\ \s. P () s \ G s \ state_assert G \ P \!" + apply (rule validNF) + apply wpsimp + apply (clarsimp simp: no_fail_def state_assert_def + bind_def2 assert_def return_def get_def) + done + +lemma validNF_modify[wp]: + "\ \s. P () (f s) \ modify f \ P \!" + apply (clarsimp simp: modify_def) + apply wp + done + +lemma validNF_gets[wp]: + "\\s. P (f s) s\ gets f \P\!" + apply (clarsimp simp: gets_def) + apply wp + done + +lemma validNF_condition[wp]: + "\ \ Q \ A \P\!; \ R \ B \P\!\ \ \\s. if C s then Q s else R s\ condition C A B \P\!" + apply rule + apply (drule validNF_valid)+ + apply (erule (1) condition_wp) + apply (drule validNF_no_fail)+ + apply (clarsimp simp: no_fail_def condition_def) + done + +lemma validNF_assert[wp]: + "\ (\s. P) and (R ()) \ assert P \ R \!" + apply (rule validNF) + apply (clarsimp simp: valid_def in_return) + apply (clarsimp simp: no_fail_def return_def) + done + +lemma validNF_false_pre: + "\ \_. False \ P \ Q \!" + by (clarsimp simp: validNF_def no_fail_def) + +lemma validNF_chain: + "\\P'\ a \R'\!; \s. P s \ P' s; \r s. R' r s \ R r s\ \ \P\ a \R\!" + by (fastforce simp: validNF_def valid_def no_fail_def Ball_def) + +lemma validNF_case_prod[wp]: + "\ \x y. validNF (P x y) (B x y) Q \ \ validNF (case_prod P v) (case_prod (\x y. B x y) v) Q" + by (metis prod.exhaust split_conv) + +lemma validE_NF_case_prod[wp]: + "\ \a b. \P a b\ f a b \Q\, \E\! \ \ + \case x of (a, b) \ P a b\ case x of (a, b) \ f a b \Q\, \E\!" + apply (clarsimp simp: validE_NF_alt_def) + apply (erule validNF_case_prod) + done + +lemma no_fail_is_validNF_True: "no_fail P s = (\ P \ s \ \_ _. True \!)" + by (clarsimp simp: no_fail_def validNF_def valid_def) + + +subsection \@{const validNF} reasoning in the exception monad\ + +lemma validE_NF[intro?]: + "\ \ P \ f \ Q \,\ E \; no_fail P f \ \ \ P \ f \ Q \,\ E \!" + by (clarsimp simp: validE_NF_def) + +lemma validE_NF_valid: + "\ \ P \ f \ Q \,\ E \! \ \ \ P \ f \ Q \,\ E \" + by (clarsimp simp: validE_NF_def) + +lemma validE_NF_no_fail: + "\ \ P \ f \ Q \,\ E \! \ \ no_fail P f" + by (clarsimp simp: validE_NF_def) + +lemma validE_NF_weaken_pre[wp_pre]: + "\\Q\ a \R\,\E\!; \s. P s \ Q s\ \ \P\ a \R\,\E\!" + by (simp add: validE_NF_alt_def validNF_weaken_pre) + +lemma validE_NF_post_comb_conj_L: + "\ \P\ f \Q\, \E\!; \P'\ f \Q'\, \\_ _. True\ \ \ + \\s. P s \ P' s\ f \\rv s. Q rv s \ Q' rv s\, \E\!" + unfolding validE_NF_alt_def + by (fastforce simp: validE_def validNF_def valid_def no_fail_def split: sum.splits) + +lemma validE_NF_post_comb_conj_R: + "\ \P\ f \Q\, \\_ _. True\; \P'\ f \Q'\, \E\! \ \ + \\s. P s \ P' s\ f \\rv s. Q rv s \ Q' rv s\, \E\!" + unfolding validE_NF_alt_def validE_def validNF_def valid_def no_fail_def + by (force split: sum.splits) + +lemma validE_NF_post_comb_conj: + "\ \P\ f \Q\, \E\!; \P'\ f \Q'\, \E\! \ \ \\s. P s \ P' s\ f \\rv s. Q rv s \ Q' rv s\, \E\!" + unfolding validE_NF_alt_def validE_def validNF_def valid_def no_fail_def + by (force split: sum.splits) + +lemma validE_NF_chain: + "\ \P'\ a \R'\,\E'\!; \s. P s \ P' s; \r' s'. R' r' s' \ R r' s'; + \r'' s''. E' r'' s'' \ E r'' s''\ \ + \\s. P s \ a \\r' s'. R r' s'\,\\r'' s''. E r'' s''\!" + by (fastforce simp: validE_NF_def validE_def2 no_fail_def Ball_def split: sum.splits) + +lemma validE_NF_bind_wp[wp]: + "\\x. \B x\ g x \C\, \E\!; \A\ f \B\, \E\!\ \ \A\ f >>=E (\x. g x) \C\, \E\!" + apply (unfold validE_NF_alt_def bindE_def) + apply (rule validNF_bind [rotated]) + apply assumption + apply (clarsimp simp: lift_def throwError_def split: sum.splits) + apply wpsimp + done + +lemma validNF_catch[wp]: + "\\x. \E x\ handler x \Q\!; \P\ f \Q\, \E\!\ \ \P\ f (\x. handler x) \Q\!" + apply (unfold validE_NF_alt_def catch_def) + apply (rule validNF_bind [rotated]) + apply assumption + apply (clarsimp simp: lift_def throwError_def split: sum.splits) + apply wp + done + +lemma validNF_throwError[wp]: + "\E e\ throwError e \P\, \E\!" + by (unfold validE_NF_alt_def throwError_def o_def) wpsimp + +lemma validNF_returnOk[wp]: + "\P e\ returnOk e \P\, \E\!" + by (clarsimp simp: validE_NF_alt_def returnOk_def) wpsimp + +lemma validNF_whenE[wp]: + "(P \ \Q\ f \R\, \E\!) \ \if P then Q else R ()\ whenE P f \R\, \E\!" + unfolding whenE_def by clarsimp wp + +lemma validNF_nobindE[wp]: + "\ \B\ g \C\,\E\!; \A\ f \\r s. B s\,\E\! \ \ \A\ doE f; g odE \C\,\E\!" + by clarsimp 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 + "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')" + +lemma validE_NF_is_triple[wp_trip]: + "validE_NF P f Q E = triple_judgement P f (validE_NF_property Q E)" + by (fastforce simp: validE_NF_def validE_def2 no_fail_def triple_judgement_def + validE_NF_property_def + split: sum.splits) + +lemma validNF_cong: + "\ \s. P s = P' s; \s. P s \ m s = m' s; + \r' s' s. \ P s; (r', s') \ mres (m s) \ \ Q r' s' = Q' r' s' \ \ + (\P\ m \Q\!) = (\P'\ m' \Q'\!)" + by (fastforce simp: validNF_alt_def) + +lemma validE_NF_liftE[wp]: + "\P\ f \Q\! \ \P\ liftE f \Q\,\E\!" + by (wpsimp simp: validE_NF_alt_def liftE_def) + +lemma validE_NF_handleE'[wp]: + "\ \x. \F x\ handler x \Q\,\E\!; \P\ f \Q\,\F\! \ \ + \P\ f (\x. handler x) \Q\,\E\!" + unfolding validE_NF_alt_def handleE'_def + apply (erule validNF_bind[rotated]) + apply (clarsimp split: sum.splits) + apply wpsimp + done + +lemma validE_NF_handleE[wp]: + "\ \x. \F x\ handler x \Q\,\E\!; \P\ f \Q\,\F\! \ \ + \P\ f handler \Q\,\E\!" + unfolding handleE_def + by (metis validE_NF_handleE') + +lemma validE_NF_condition[wp]: + "\ \ Q \ A \P\,\ E \!; \ R \ B \P\,\ E \!\ \ + \\s. if C s then Q s else R s\ condition C A B \P\,\ E \!" + apply rule + apply (drule validE_NF_valid)+ + apply wp + apply (drule validE_NF_no_fail)+ + apply (clarsimp simp: no_fail_def condition_def) + done + +end \ No newline at end of file diff --git a/lib/Monads/trace/Trace_VCG.thy b/lib/Monads/trace/Trace_VCG.thy index 9bdc420918..c20265ebd4 100644 --- a/lib/Monads/trace/Trace_VCG.thy +++ b/lib/Monads/trace/Trace_VCG.thy @@ -1,633 +1,131 @@ (* + * Copyright 2023, Proofcraft Pty Ltd * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) * * SPDX-License-Identifier: BSD-2-Clause *) + theory Trace_VCG -imports - Trace_Monad - Fun_Pred_Syntax - WPSimp + imports + Trace_Lemmas + WPSimp begin -lemma trace_steps_append: - "trace_steps (xs @ ys) s - = trace_steps xs s \ trace_steps ys (last_st_tr (rev xs) s)" - by (induct xs arbitrary: s, simp_all add: last_st_tr_def hd_append) - -lemma rely_cond_append: - "rely_cond R s (xs @ ys) = (rely_cond R s ys \ rely_cond R (last_st_tr ys s) xs)" - by (simp add: rely_cond_def trace_steps_append ball_Un conj_comms) - -lemma guar_cond_append: - "guar_cond G s (xs @ ys) = (guar_cond G s ys \ guar_cond G (last_st_tr ys s) xs)" - by (simp add: guar_cond_def trace_steps_append ball_Un conj_comms) - -lemma prefix_closed_bind: - "prefix_closed f \ (\x. prefix_closed (g x)) \ prefix_closed (f >>= g)" - apply (subst prefix_closed_def, clarsimp simp: bind_def) - apply (auto simp: Cons_eq_append_conv split: tmres.split_asm - dest!: prefix_closedD[rotated]; - fastforce elim: rev_bexI) - done - -lemmas prefix_closed_bind[rule_format, wp_split] - -lemma last_st_tr_append[simp]: - "last_st_tr (tr @ tr') s = last_st_tr tr (last_st_tr tr' s)" - by (simp add: last_st_tr_def hd_append) - -lemma last_st_tr_Nil[simp]: - "last_st_tr [] s = s" - by (simp add: last_st_tr_def) - -lemma last_st_tr_Cons[simp]: - "last_st_tr (x # xs) s = snd x" - by (simp add: last_st_tr_def) - -lemma bind_twp[wp_split]: - "\ \r. \Q' r\,\R\ g r \G\,\Q\; \P\,\R\ f \G\,\Q'\ \ - \ \P\,\R\ f >>= (\r. g r) \G\,\Q\" - apply (subst validI_def, rule conjI) - apply (blast intro: prefix_closed_bind validI_prefix_closed) - apply (clarsimp simp: bind_def rely_def) - apply (drule(2) validI_D) - apply (clarsimp simp: rely_cond_append split: tmres.split_asm) - apply (clarsimp split: tmres.split_asm) - apply (drule meta_spec, frule(2) validI_D) - apply (clarsimp simp: rely_cond_append split: if_split_asm) - apply (clarsimp simp: guar_cond_append) - done - -lemma trace_steps_rev_drop_nth: - "trace_steps (rev (drop n tr)) s - = (\i. (fst (rev tr ! i), (if i = 0 then s else snd (rev tr ! (i - 1))), - snd (rev tr ! i))) ` {..< length tr - n}" - apply (simp add: trace_steps_nth) - apply (intro image_cong refl) - apply (simp add: rev_nth) - done - -lemma prefix_closed_drop: - "(tr, res) \ f s \ prefix_closed f \ \res'. (drop n tr, res') \ f s" -proof (induct n arbitrary: res) - case 0 then show ?case by auto -next - case (Suc n) - have drop_1: "\tr res. (tr, res) \ f s \ \res'. (drop 1 tr, res') \ f s" - by (case_tac tr; fastforce dest: prefix_closedD[rotated] intro: Suc) - show ?case - using Suc.hyps[OF Suc.prems] - by (metis drop_1[simplified] drop_drop add_0 add_Suc) -qed - -lemma validI_GD_drop: - "\ \P\, \R\ f \G\, \Q\; P s0 s; (tr, res) \ f s; - rely_cond R s0 (drop n tr) \ - \ guar_cond G s0 (drop n tr)" - apply (drule prefix_closed_drop[where n=n], erule validI_prefix_closed) - apply (auto dest: validI_GD) - done - -lemma parallel_prefix_closed[wp_split]: - "prefix_closed f \ prefix_closed g - \ prefix_closed (parallel f g)" - apply (subst prefix_closed_def, clarsimp simp: parallel_def) - apply (case_tac f_steps; clarsimp) - apply (drule(1) prefix_closedD)+ - apply fastforce - done - -lemma rely_cond_drop: - "rely_cond R s0 xs \ rely_cond R s0 (drop n xs)" - using rely_cond_append[where xs="take n xs" and ys="drop n xs"] - by simp - -lemma rely_cond_is_drop: - "rely_cond R s0 xs - \ (ys = drop (length xs - length ys) xs) - \ rely_cond R s0 ys" - by (metis rely_cond_drop) - -lemma bounded_rev_nat_induct: - "(\n. N \ n \ P n) \ (\n. n < N \ P (Suc n) \ P n) - \ P n" - by (induct diff\"N - n" arbitrary: n; simp) - -lemma drop_n_induct: - "P [] \ (\n. n < length xs \ P (drop (Suc n) xs) \ P (drop n xs)) - \ P (drop n xs)" - by (induct len\"length (drop n xs)" arbitrary: n xs; simp) - -lemma guar_cond_Cons_eq: - "guar_cond R s0 (x # xs) - = (guar_cond R s0 xs \ (fst x \ Env \ R (last_st_tr xs s0) (snd x)))" - by (cases "fst x"; simp add: guar_cond_def trace_steps_append conj_comms) - -lemma guar_cond_Cons: - "guar_cond R s0 xs - \ fst x \ Env \ R (last_st_tr xs s0) (snd x) - \ guar_cond R s0 (x # xs)" - by (simp add: guar_cond_Cons_eq) - -lemma guar_cond_drop_Suc_eq: - "n < length xs - \ guar_cond R s0 (drop n xs) = (guar_cond R s0 (drop (Suc n) xs) - \ (fst (xs ! n) \ Env \ R (last_st_tr (drop (Suc n) xs) s0) (snd (xs ! n))))" - apply (rule trans[OF _ guar_cond_Cons_eq]) - apply (simp add: Cons_nth_drop_Suc) - done - -lemma guar_cond_drop_Suc: - "guar_cond R s0 (drop (Suc n) xs) - \ fst (xs ! n) \ Env \ R (last_st_tr (drop (Suc n) xs) s0) (snd (xs ! n)) - \ guar_cond R s0 (drop n xs)" - by (case_tac "n < length xs"; simp add: guar_cond_drop_Suc_eq) - -lemma rely_cond_Cons_eq: - "rely_cond R s0 (x # xs) - = (rely_cond R s0 xs \ (fst x = Env \ R (last_st_tr xs s0) (snd x)))" - by (simp add: rely_cond_def trace_steps_append conj_comms) - -lemma rely_cond_Cons: - "rely_cond R s0 xs - \ fst x = Env \ R (last_st_tr xs s0) (snd x) - \ rely_cond R s0 (x # xs)" - by (simp add: rely_cond_Cons_eq) - -lemma rely_cond_drop_Suc_eq: - "n < length xs - \ rely_cond R s0 (drop n xs) = (rely_cond R s0 (drop (Suc n) xs) - \ (fst (xs ! n) = Env \ R (last_st_tr (drop (Suc n) xs) s0) (snd (xs ! n))))" - apply (rule trans[OF _ rely_cond_Cons_eq]) - apply (simp add: Cons_nth_drop_Suc) - done - -lemma rely_cond_drop_Suc: - "rely_cond R s0 (drop (Suc n) xs) - \ fst (xs ! n) = Env \ R (last_st_tr (drop (Suc n) xs) s0) (snd (xs ! n)) - \ rely_cond R s0 (drop n xs)" - by (cases "n < length xs"; simp add: rely_cond_drop_Suc_eq) - -lemma last_st_tr_map_zip_hd: - "length flags = length tr - \ tr \ [] \ snd (f (hd flags, hd tr)) = snd (hd tr) - \ last_st_tr (map f (zip flags tr)) = last_st_tr tr" - apply (cases tr; simp) - apply (cases flags; simp) - apply (simp add: fun_eq_iff) - done - -lemma last_st_tr_drop_map_zip_hd: - "length flags = length tr - \ n < length tr \ snd (f (flags ! n, tr ! n)) = snd (tr ! n) - \ last_st_tr (drop n (map f (zip flags tr))) = last_st_tr (drop n tr)" - apply (simp add: drop_map drop_zip) - apply (rule last_st_tr_map_zip_hd; clarsimp) - apply (simp add: hd_drop_conv_nth) - done - -lemma last_st_tr_map_zip: - "length flags = length tr - \ \fl tmid s. snd (f (fl, (tmid, s))) = s - \ last_st_tr (map f (zip flags tr)) = last_st_tr tr" - apply (erule last_st_tr_map_zip_hd) - apply (clarsimp simp: neq_Nil_conv) - done - -lemma parallel_rely_induct: - assumes preds: "(tr, v) \ parallel f g s" "Pf s0 s" "Pg s0 s" - assumes validI: "\Pf\,\Rf\ f' \Gf\,\Qf\" - "\Pg\,\Rg\ g' \Gg\,\Qg\" - "f s \ f' s" "g s \ g' s" - and compat: "R \ Rf" "R \ Rg" "Gf \ G" "Gg \ G" - "Gf \ Rg" "Gg \ Rf" - and rely: "rely_cond R s0 (drop n tr)" - shows "\tr_f tr_g. (tr_f, v) \ f s \ (tr_g, v) \ g s - \ rely_cond Rf s0 (drop n tr_f) \ rely_cond Rg s0 (drop n tr_g) - \ map snd tr_f = map snd tr \ map snd tr_g = map snd tr - \ (\i \ length tr. last_st_tr (drop i tr_g) s0 = last_st_tr (drop i tr_f) s0) - \ guar_cond G s0 (drop n tr)" - (is "\ys zs. _ \ _ \ ?concl ys zs") -proof - - obtain ys zs where tr: "tr = map parallel_mrg (zip ys zs)" - and all2: "list_all2 (\y z. (fst y = Env \ fst z = Env) \ snd y = snd z) ys zs" - and ys: "(ys, v) \ f s" and zs: "(zs, v) \ g s" - using preds - by (clarsimp simp: parallel_def2) - note len[simp] = list_all2_lengthD[OF all2] - - have ys': "(ys, v) \ f' s" and zs': "(zs, v) \ g' s" - using ys zs validI by auto - - note rely_f_step = validI_GD_drop[OF validI(1) preds(2) ys' rely_cond_drop_Suc] - note rely_g_step = validI_GD_drop[OF validI(2) preds(3) zs' rely_cond_drop_Suc] - - note snd[simp] = list_all2_nthD[OF all2, THEN conjunct2] - - have "?concl ys zs" - using rely tr all2 rely_f_step rely_g_step - apply (induct n rule: bounded_rev_nat_induct) - apply (subst drop_all, assumption) - apply clarsimp - apply (simp add: list_all2_conv_all_nth last_st_tr_def drop_map[symmetric] - hd_drop_conv_nth hd_append) - apply (fastforce simp: split_def intro!: nth_equalityI) - apply clarsimp - apply (erule_tac x=n in meta_allE)+ - apply (drule meta_mp, erule rely_cond_is_drop, simp) - apply (subst(asm) rely_cond_drop_Suc_eq[where xs="map f xs" for f xs], simp) - apply (clarsimp simp: last_st_tr_drop_map_zip_hd if_split[where P="\x. x = Env"] - split_def) - apply (intro conjI; (rule guar_cond_drop_Suc rely_cond_drop_Suc, assumption)) - apply (auto simp: guar_cond_drop_Suc_eq last_st_tr_drop_map_zip_hd - intro: compat[THEN predicate2D]) - done - - thus ?thesis - using ys zs - by auto -qed - -lemmas parallel_rely_induct0 = parallel_rely_induct[where n=0, simplified] - -lemma rg_validI: - assumes validI: "\Pf\,\Rf\ f \Gf\,\Qf\" - "\Pg\,\Rg\ g \Gg\,\Qg\" - and compat: "R \ Rf" "R \ Rg" "Gf \ G" "Gg \ G" - "Gf \ Rg" "Gg \ Rf" - shows "\Pf and Pg\,\R\ parallel f g \G\,\\rv. Qf rv and Qg rv\" - apply (clarsimp simp: validI_def rely_def pred_conj_def - parallel_prefix_closed validI[THEN validI_prefix_closed]) - apply (drule(3) parallel_rely_induct0[OF _ _ _ validI order_refl order_refl compat]) - apply clarsimp - apply (drule(2) validI[THEN validI_rvD])+ - apply (simp add: last_st_tr_def) - done - -lemma validI_weaken_pre[wp_pre]: - "\P'\,\R\ f \G\,\Q\ - \ (\s0 s. P s0 s \ P' s0 s) - \ \P\,\R\ f \G\,\Q\" - by (simp add: validI_def, blast) - -lemma rely_weaken: - "(\s0 s. R s0 s \ R' s0 s) - \ (tr, res) \ rely f R s s0 \ (tr, res) \ rely f R' s s0" - by (simp add: rely_def rely_cond_def, blast) - -lemma validI_weaken_rely[wp_pre]: - "\P\,\R'\ f \G\,\Q\ - \ (\s0 s. R s0 s \ R' s0 s) - \ \P\,\R\ f \G\,\Q\" - apply (simp add: validI_def) - by (metis rely_weaken) - -lemma validI_strengthen_post: - "\P\,\R\ f \G\,\Q'\ - \ (\v s0 s. Q' v s0 s \ Q v s0 s) - \ \P\,\R\ f \G\,\Q\" - by (simp add: validI_def) - -lemma validI_strengthen_guar: - "\P\, \R\ f \G'\, \Q\ - \ (\s0 s. G' s0 s \ G s0 s) - \ \P\, \R\ f \G\, \Q\" - by (force simp: validI_def guar_cond_def) - -lemma rely_prim[simp]: - "rely (\s. insert (v s) (f s)) R s0 = (\s. {x. x = v s \ rely_cond R s0 (fst x)} \ (rely f R s0 s))" - "rely (\s. {}) R s0 = (\_. {})" - by (auto simp: rely_def prod_eq_iff) - -lemma prefix_closed_put_trace_elem[iff]: - "prefix_closed (put_trace_elem x)" - by (clarsimp simp: prefix_closed_def put_trace_elem_def) - -lemma prefix_closed_return[iff]: - "prefix_closed (return x)" - by (simp add: prefix_closed_def return_def) - -lemma prefix_closed_put_trace[iff]: - "prefix_closed (put_trace tr)" - by (induct tr; clarsimp simp: prefix_closed_bind) - -lemma put_trace_eq_drop: - "put_trace xs s - = ((\n. (drop n xs, if n = 0 then Result ((), s) else Incomplete)) ` {.. length xs})" - apply (induct xs) - apply (clarsimp simp: return_def) - apply (clarsimp simp: put_trace_elem_def bind_def) - apply (simp add: atMost_Suc_eq_insert_0 image_image) - apply (rule equalityI; clarsimp) - apply (split if_split_asm; clarsimp) - apply (auto intro: image_eqI[where x=0])[1] - apply (rule rev_bexI, simp) - apply clarsimp - done - -lemma put_trace_res: - "(tr, res) \ put_trace xs s - \ \n. tr = drop n xs \ n \ length xs - \ res = (case n of 0 \ Result ((), s) | _ \ Incomplete)" - apply (clarsimp simp: put_trace_eq_drop) - apply (case_tac n; auto intro: exI[where x=0]) - done - -lemma put_trace_twp[wp]: - "\\s0 s. (\n. rely_cond R s0 (drop n xs) \ guar_cond G s0 (drop n xs)) - \ (rely_cond R s0 xs \ Q () (last_st_tr xs s0) s)\,\R\ put_trace xs \G\,\Q\" - apply (clarsimp simp: validI_def rely_def) - apply (drule put_trace_res) - apply (clarsimp; clarsimp split: nat.split_asm) - done - -lemmas put_trace_elem_twp = put_trace_twp[where xs="[x]" for x, simplified] - -lemma prefix_closed_select[iff]: - "prefix_closed (select S)" - by (simp add: prefix_closed_def select_def image_def) +section \Hoare Logic\ -lemma select_wp[wp]: "\\s. \x \ S. Q x s\ select S \Q\" - by (simp add: select_def valid_def mres_def image_def) - -lemma rely_cond_rtranclp: - "rely_cond R s (map (Pair Env) xs) \ rtranclp R s (last_st_tr (map (Pair Env) xs) s)" - apply (induct xs arbitrary: s rule: rev_induct) - apply simp - apply (clarsimp simp add: rely_cond_def) - apply (erule converse_rtranclp_into_rtranclp) - apply simp - done - -lemma put_wp[wp]: - "\\_. Q () s\ put s \Q\" - by (simp add: put_def valid_def mres_def) - -lemma get_wp[wp]: - "\\s. Q s s\ get \Q\" - by (simp add: get_def valid_def mres_def) - -lemma bind_wp[wp_split]: - "\ \r. \Q' r\ g r \Q\; \P\f \Q'\ \ - \ \P\ f >>= (\r. g r) \Q\" - by (fastforce simp: valid_def bind_def2 mres_def intro: image_eqI[rotated]) - -lemma modify_wp[wp]: - "\\s. Q () (f s)\ modify f \Q\" - unfolding modify_def - by wp - -definition - no_trace :: "('s,'a) tmonad \ bool" -where - "no_trace f = (\tr res s. (tr, res) \ f s \ tr = [] \ res \ Incomplete)" - -lemmas no_traceD = no_trace_def[THEN iffD1, rule_format] - -lemma no_trace_emp: - "no_trace f \ (tr, r) \ f s \ tr = []" - by (simp add: no_traceD) - -lemma no_trace_Incomplete_mem: - "no_trace f \ (tr, Incomplete) \ f s" - by (auto dest: no_traceD) - -lemma no_trace_Incomplete_eq: - "no_trace f \ (tr, res) \ f s \ res \ Incomplete" - by (auto dest: no_traceD) - -lemma no_trace_prefix_closed: - "no_trace f \ prefix_closed f" - by (auto simp add: prefix_closed_def dest: no_trace_emp) - -(* Attempt to define triple_judgement to use valid_validI_wp as wp_comb rule. - It doesn't work. It seems that wp_comb rules cannot take more than 1 assumption *) -lemma validI_is_triple: - "\P\,\R\ f \G\,\Q\ = - triple_judgement (\(s0, s). prefix_closed f \ P s0 s) f - (\(s0,s) f. prefix_closed f \ (\tr res. (tr, res) \ rely f R s0 s - \ guar_cond G s0 tr - \ (\rv s'. res = Result (rv, s') \ Q rv (last_st_tr tr s0) s')))" - apply (simp add: triple_judgement_def validI_def ) - apply (cases "prefix_closed f"; simp) - done - -lemma valid_is_triple: - "valid P f Q = - triple_judgement P f - (\s f. (\(r,s') \ (mres (f s)). Q r s'))" - by (simp add: triple_judgement_def valid_def mres_def) - -lemma no_trace_is_triple: - "no_trace f = triple_judgement \ f (\() f. id no_trace f)" - by (simp add: triple_judgement_def split: unit.split) - -lemmas [wp_trip] = valid_is_triple validI_is_triple no_trace_is_triple - -lemma valid_validI_wp[wp_comb]: - "no_trace f \ (\s0. \P s0\ f \\v. Q v s0 \) - \ \P\,\R\ f \G\,\Q\" - by (fastforce simp: rely_def validI_def valid_def mres_def no_trace_prefix_closed dest: no_trace_emp - elim: image_eqI[rotated]) - -(* Since valid_validI_wp in wp_comb doesn't work, we add the rules directly in the wp set *) -lemma no_trace_prim: - "no_trace get" - "no_trace (put s)" - "no_trace (modify f)" - "no_trace (return v)" - "no_trace fail" - by (simp_all add: no_trace_def get_def put_def modify_def bind_def - return_def select_def fail_def) - -lemma no_trace_select: - "no_trace (select S)" - by (clarsimp simp add: no_trace_def select_def) - -lemma no_trace_bind: - "no_trace f \ \rv. no_trace (g rv) - \ no_trace (do rv \ f; g rv od)" - apply (subst no_trace_def) - apply (clarsimp simp add: bind_def split: tmres.split_asm; - auto dest: no_traceD[rotated]) - done - -lemma no_trace_extra: - "no_trace (gets f)" - "no_trace (assert P)" - "no_trace (assert_opt Q)" - by (simp_all add: gets_def assert_def assert_opt_def no_trace_bind no_trace_prim - split: option.split) - -lemmas no_trace_all[wp, iff] = no_trace_prim no_trace_select no_trace_extra - -lemma env_steps_twp[wp]: - "\\s0 s. (\s'. R\<^sup>*\<^sup>* s0 s' \ Q () s' s') \ Q () s0 s\,\R\ env_steps \G\,\Q\" - apply (simp add: interference_def env_steps_def) - apply wp - apply (clarsimp simp: guar_cond_def trace_steps_rev_drop_nth rev_nth) - apply (drule rely_cond_rtranclp) - apply (clarsimp simp add: last_st_tr_def hd_append) - done +subsection \Validity\ -lemma interference_twp[wp]: - "\\s0 s. (\s'. R\<^sup>*\<^sup>* s s' \ Q () s' s') \ G s0 s\,\R\ interference \G\,\Q\" - apply (simp add: interference_def commit_step_def del: put_trace.simps) - apply wp - apply clarsimp - apply (simp add: drop_Cons nat.split rely_cond_def guar_cond_def) - done +text \ + This section defines a Hoare logic for partial correctness for + the interference trace monad as well as the exception monad. + The logic talks only about the behaviour part of the monad and ignores + failures and the trace. + + The logic is defined semantically. Rules work directly on the + validity predicate. + + In the interference trace monad, validity is a triple of precondition, + monad, and postcondition. The precondition is a function from state to + bool (a state predicate), the postcondition is a function from return value + to state to bool. A triple is valid if for all states that satisfy the + precondition, all result values and result states that are returned by + the monad satisfy the postcondition. Note that if the result of the + computation is the empty set then the triple is trivially valid. This means + @{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" + ("\_\/ _ /\_\") where + "\P\ f \Q\ \ \s. P s \ (\(r,s') \ mres (f s). Q r s')" -(* what Await does if we haven't committed our step is a little - strange. this assumes we have, which means s0 = s. we should - revisit this if we find a use for Await when this isn't the - case *) -lemma Await_sync_twp: - "\\s0 s. s = s0 \ (\x. R\<^sup>*\<^sup>* s0 x \ c x \ Q () x x)\,\R\ Await c \G\,\Q\" - apply (simp add: Await_def split_def) - apply wp - apply clarsimp - apply (clarsimp simp: guar_cond_def trace_steps_rev_drop_nth rev_nth) - apply (drule rely_cond_rtranclp) - apply (simp add: o_def) - done +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 + "invariant f P \ \P\ f \\_. P\" -(* Wrap up the standard usage pattern of wp/wpc/simp into its own command: *) -method wpsimp uses wp simp split split_del cong = - ((determ \wp add: wp|wpc|clarsimp simp: simp split: split split del: split_del cong: cong\)+)[1] +text \ + Validity for the exception monad is similar and build on the standard + validity above. Instead of one postcondition, we have two: one for + normal and one for exceptional results.\ +definition validE :: + "('s \ bool) \ ('s, 'a + 'b) tmonad \ ('b \ 's \ bool) \ ('a \ 's \ bool) \ bool" + ("\_\/ _ /(\_\,/ \_\)" ) where + "\P\ f \Q\,\E\ \ \P\ f \ \v s. case v of Inr r \ Q r s | Inl e \ E e s \" -section "Satisfiability" +lemma validE_def2: + "\P\ f \Q\,\E\ \ \s. P s \ (\(r,s') \ mres (f s). case r of Inr b \ Q b s' | Inl a \ E a s')" + by (unfold valid_def validE_def) 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 - "exs_valid P f Q \ (\s. P s \ (\(rv, s') \ mres (f s). Q rv s'))" - - -text \The above for the exception monad\ -definition - ex_exs_validE :: "('a \ bool) \ ('a, 'e + 'b) tmonad \ - ('b \ 'a \ bool) \ ('e \ 'a \ bool) \ bool" - ("\_\ _ \\_\, \_\") -where - "ex_exs_validE P f Q E \ - exs_valid P f (\rv. case rv of Inl e \ E e | Inr v \ Q v)" - - -section "Lemmas" - -subsection \Determinism\ - -lemma det_set_iff: - "det f \ (r \ mres (f s)) = (mres (f s) = {r})" - apply (simp add: det_def mres_def) - apply (fastforce elim: allE[where x=s]) - done - -lemma return_det [iff]: - "det (return x)" - by (simp add: det_def return_def) + The following two instantiations are convenient to separate reasoning for exceptional and + normal case.\ +(* Narrator: they are in fact not convenient, and are now considered a mistake that should have + been an abbreviation instead. *) +definition validE_R :: (* FIXME lib: this should be an abbreviation *) + "('s \ bool) \ ('s, 'e + 'a) tmonad \ ('a \ 's \ bool) \ bool" ("\_\/ _ /\_\, -") where + "\P\ f \Q\,- \ validE P f Q (\x y. True)" -lemma put_det [iff]: - "det (put s)" - by (simp add: det_def put_def) +definition validE_E :: (* FIXME lib: this should be an abbreviation *) + "('s \ bool) \ ('s, 'e + 'a) tmonad \ ('e \ 's \ bool) \ bool" ("\_\/ _ /-, \_\") where + "\P\ f -,\Q\ \ validE P f (\x y. True) Q" -lemma get_det [iff]: - "det get" - by (simp add: det_def get_def) -lemma det_gets [iff]: - "det (gets f)" - by (auto simp add: gets_def det_def get_def return_def bind_def) +section \Lemmas\ -lemma det_UN: - "det f \ (\x \ mres (f s). g x) = (g (THE x. x \ mres (f s)))" - unfolding det_def mres_def - apply simp - apply (drule spec [of _ s]) - apply (clarsimp simp: vimage_def) - done +lemma hoare_pre_imp: + "\ \s. P s \ Q s; \Q\ a \R\ \ \ \P\ a \R\" + by (fastforce simp: valid_def) -lemma bind_detI [simp, intro!]: - "\ det f; \x. det (g x) \ \ det (f >>= g)" - apply (simp add: bind_def det_def split_def) - apply clarsimp - apply (erule_tac x=s in allE) - apply clarsimp - done +lemmas hoare_weaken_pre = hoare_pre_imp[rotated] -lemma det_modify[iff]: - "det (modify f)" - by (simp add: modify_def) +lemma hoare_vcg_precond_impE: (* FIXME lib: eliminate in favour of hoare_weaken_preE *) + "\ \Q\ f \R\,\E\; \s. P s \ Q s \ \ \P\ f \R\,\E\" + by (fastforce simp add:validE_def2) -lemma the_run_stateI: - "mres (M s) = {s'} \ the_run_state M s = s'" - by (simp add: the_run_state_def) +lemmas hoare_weaken_preE = hoare_vcg_precond_impE -lemma the_run_state_det: - "\ s' \ mres (M s); det M \ \ the_run_state M s = s'" - by (simp only: the_run_stateI det_set_iff[where f=M and s=s]) +lemma hoare_vcg_precond_impE_R: (* FIXME lib: rename to hoare_weaken_preE_R *) + "\ \P'\ f \Q\,-; \s. P s \ P' s \ \ \P\ f \Q\,-" + unfolding validE_R_def + by (rule hoare_vcg_precond_impE) -subsection "Lifting and Alternative Basic Definitions" +lemma hoare_weaken_preE_E: + "\ \P'\ f -,\Q\; \s. P s \ P' s \ \ \P\ f -,\Q\" + by (fastforce simp add: validE_E_def validE_def valid_def) -lemma liftE_liftM: "liftE = liftM Inr" - apply (rule ext) - apply (simp add: liftE_def liftM_def) - done +lemmas hoare_pre [wp_pre] = + hoare_weaken_pre + hoare_weaken_preE + hoare_vcg_precond_impE_R + hoare_weaken_preE_E -lemma liftME_liftM: "liftME f = liftM (case_sum Inl (Inr \ f))" - apply (rule ext) - apply (simp add: liftME_def liftM_def bindE_def returnOk_def lift_def) - apply (rule_tac f="bind x" in arg_cong) - apply (rule ext) - apply (case_tac xa) - apply (simp_all add: lift_def throwError_def) - done -lemma liftE_bindE: - "(liftE a) >>=E b = a >>= b" - apply (simp add: liftE_def bindE_def lift_def bind_assoc) - done +subsection \Setting up the precondition case splitter.\ -lemma liftM_id[simp]: "liftM id = id" - apply (rule ext) - apply (simp add: liftM_def) - done +lemma wpc_helper_valid: + "\Q\ g \S\ \ wpc_helper (P, P', P'') (Q, Q', Q'') \P\ g \S\" + by (clarsimp simp: wpc_helper_def elim!: hoare_pre) -lemma liftM_bind: - "(liftM t f >>= g) = (f >>= (\x. g (t x)))" - by (simp add: liftM_def bind_assoc) +lemma wpc_helper_validE: + "\Q\ f \R\,\E\ \ wpc_helper (P, P', P'') (Q, Q', Q'') \P\ f \R\,\E\" + by (clarsimp simp: wpc_helper_def elim!: hoare_pre) -lemma gets_bind_ign: "gets f >>= (\x. m) = m" - apply (rule ext) - apply (simp add: bind_def simpler_gets_def) - done +lemma wpc_helper_validE_R: + "\Q\ f \R\,- \ wpc_helper (P, P', P'') (Q, Q', Q'') \P\ f \R\,-" + by (clarsimp simp: wpc_helper_def elim!: hoare_pre) -lemma get_bind_apply: "(get >>= f) x = f x x" - by (simp add: get_def bind_def) +lemma wpc_helper_validR_R: + "\Q\ f -,\E\ \ wpc_helper (P, P', P'') (Q, Q', Q'') \P\ f -,\E\" + by (clarsimp simp: wpc_helper_def elim!: hoare_pre) -lemma exec_gets: - "(gets f >>= m) s = m (f s) s" - by (simp add: simpler_gets_def bind_def) -lemma exec_get: - "(get >>= m) s = m s s" - by (simp add: get_def bind_def) +wpc_setup "\m. \P\ m \Q\" wpc_helper_valid +wpc_setup "\m. \P\ m \Q\,\E\" wpc_helper_validE +wpc_setup "\m. \P\ m \Q\,-" wpc_helper_validE_R +wpc_setup "\m. \P\ m -,\E\" wpc_helper_validR_R -lemma bind_eqI: - "\ f = f'; \x. g x = g' x \ \ f >>= g = f' >>= g'" - apply (rule ext) - apply (simp add: bind_def) - done subsection "Simplification Rules for Lifted And/Or" @@ -642,15 +140,12 @@ lemma bipred_le_true[simp]: "R \ \\" subsection "Hoare Logic Rules" -lemma validE_def2: - "validE P f Q R \ \s. P s \ (\(r,s') \ mres (f s). case r of Inr b \ Q b s' - | Inl a \ R a s')" - by (unfold valid_def validE_def) +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]) lemma seq': - "\ \A\ f \B\; - \x. P x \ \C\ g x \D\; - \x s. B x s \ P x \ C s \ \ + "\ \A\ f \B\; \x. P x \ \C\ g x \D\; \x s. B x s \ P x \ C s \ \ \A\ do x \ f; g x od \D\" apply (erule bind_wp[rotated]) apply (clarsimp simp: valid_def) @@ -662,21 +157,19 @@ lemma seq: assumes g_valid: "\x. P x \ \C\ g x \D\" assumes bind: "\x s. B x s \ P x \ C s" shows "\A\ do x \ f; g x od \D\" -apply (insert f_valid g_valid bind) -apply (blast intro: seq') -done + apply (insert f_valid g_valid bind) + apply (blast intro: seq') + done lemma seq_ext': - "\ \A\ f \B\; - \x. \B x\ g x \C\ \ \ + "\ \A\ f \B\; \x. \B x\ g x \C\ \ \ \A\ do x \ f; g x od \C\" by (metis bind_wp) lemmas seq_ext = bind_wp[rotated] lemma seqE': - "\ \A\ f \B\,\E\ ; - \x. \B x\ g x \C\,\E\ \ \ + "\ \A\ f \B\,\E\; \x. \B x\ g x \C\,\E\ \ \ \A\ doE x \ f; g x odE \C\,\E\" apply (simp add: bindE_def validE_def) apply (erule seq_ext') @@ -688,147 +181,105 @@ lemma seqE: assumes f_valid: "\A\ f \B\,\E\" assumes g_valid: "\x. \B x\ g x \C\,\E\" shows "\A\ doE x \ f; g x odE \C\,\E\" - apply(insert f_valid g_valid) - apply(blast intro: seqE') + apply (insert f_valid g_valid) + apply (blast intro: seqE') done -lemma hoare_TrueI: "\P\ f \\_. \\" +lemma hoare_TrueI: + "\P\ f \\_. \\" by (simp add: valid_def) -lemma hoareE_TrueI: "\P\ f \\_. \\, \\r. \\" +lemma hoareE_TrueI: + "\P\ f \\_. \\, \\r. \\" by (simp add: validE_def valid_def) -lemma hoare_True_E_R [simp]: - "\P\ f \\r s. True\, -" - by (auto simp add: validE_R_def validE_def valid_def split: sum.splits) +lemma hoare_True_E_R[simp]: + "\P\ f \\_ s. True\, -" + by (auto simp: validE_R_def validE_def valid_def split: sum.splits) -lemma hoare_post_conj [intro!]: - "\ \ P \ a \ Q \; \ P \ a \ R \ \ \ \ P \ a \ Q and R \" - by (fastforce simp: valid_def split_def pred_conj_def) +lemma hoare_post_conj[intro]: + "\ \P\ f \Q\; \P\ f \R\ \ \ \P\ f \Q and R\" + by (fastforce simp: valid_def) -lemma hoare_pre_disj [intro!]: - "\ \ P \ a \ R \; \ Q \ a \ R \ \ \ \ P or Q \ a \ R \" +lemma hoare_pre_disj[intro]: + "\ \P\ f \R\; \Q\ f \R\ \ \ \P or Q\ f \R\" by (simp add:valid_def pred_disj_def) lemma hoare_conj: "\ \P\ f \Q\; \P'\ f \Q'\ \ \ \P and P'\ f \Q and Q'\" - unfolding valid_def - by (auto) - -lemma hoare_post_taut: "\ P \ a \ \\ \" - by (simp add:valid_def) + unfolding valid_def by auto -lemma wp_post_taut: "\\r. True\ f \\r s. True\" - by (rule hoare_post_taut) +lemmas hoare_post_taut = hoare_TrueI (* FIXME lib: eliminate *) -lemma wp_post_tautE: "\\r. True\ f \\r s. True\,\\f s. True\" -proof - - have P: "\r. (case r of Inl a \ True | _ \ True) = True" - by (case_tac r, simp_all) - show ?thesis - by (simp add: validE_def P wp_post_taut) -qed +lemmas wp_post_taut = hoare_TrueI[where P=\] +lemmas wp_post_tautE = hoareE_TrueI[where P=\] -lemma hoare_pre_cont [simp]: "\ \ \ a \ P \" +lemma hoare_pre_cont[simp]: + "\\\ f \P\" by (simp add:valid_def) +lemma hoare_return_drop_var[iff]: + "\Q\ return x \\r. Q\" + by (simp add: valid_def return_def mres_def) -subsection \Strongest Postcondition Rules\ - -lemma get_sp: - "\P\ get \\a s. s = a \ P s\" - by(simp add:get_def valid_def mres_def) - -lemma put_sp: - "\\\ put a \\_ s. s = a\" - by(simp add:put_def valid_def mres_def) - -lemma return_sp: - "\P\ return a \\b s. b = a \ P s\" - by(simp add:return_def valid_def mres_def) - -lemma assert_sp: - "\ P \ assert Q \ \r s. P s \ Q \" - by (simp add: assert_def fail_def return_def valid_def mres_def) - -lemma hoare_gets_sp: - "\P\ gets f \\rv s. rv = f s \ P s\" - by (simp add: valid_def simpler_gets_def mres_def) - -lemma hoare_return_drop_var [iff]: "\ Q \ return x \ \r. Q \" - by (simp add:valid_def return_def mres_def) - -lemma hoare_gets [intro!]: "\ \s. P s \ Q (f s) s \ \ \ P \ gets f \ Q \" +lemma hoare_gets[intro]: + "\ \s. P s \ Q (f s) s \ \ \P\ gets f \Q\" by (simp add:valid_def gets_def get_def bind_def return_def mres_def) -lemma hoare_modifyE_var [intro!]: - "\ \s. P s \ Q (f s) \ \ \ P \ modify f \ \r s. Q s \" +lemma hoare_modifyE_var: + "\ \s. P s \ Q (f s) \ \ \P\ modify f \\_ s. Q s\" by(simp add: valid_def modify_def put_def get_def bind_def mres_def) -lemma hoare_if [intro!]: - "\ P \ \ Q \ a \ R \; \ P \ \ Q \ b \ R \ \ \ - \ Q \ if P then a else b \ R \" - by (simp add:valid_def) - -lemma hoare_pre_subst: "\ A = B; \A\ a \C\ \ \ \B\ a \C\" - by(clarsimp simp:valid_def split_def) - -lemma hoare_post_subst: "\ B = C; \A\ a \B\ \ \ \A\ a \C\" - by(clarsimp simp:valid_def split_def) +lemma hoare_if: + "\ P \ \Q\ a \R\; \ P \ \Q\ b \R\ \ \ \Q\ if P then a else b \R\" + by (simp add: valid_def) -lemma hoare_pre_tautI: "\ \A and P\ a \B\; \A and not P\ a \B\ \ \ \A\ a \B\" - by(fastforce simp:valid_def split_def pred_conj_def pred_neg_def) +lemma hoare_pre_subst: + "\ A = B; \A\ a \C\ \ \ \B\ a \C\" + by (erule subst) -lemma hoare_pre_imp: "\ \s. P s \ Q s; \Q\ a \R\ \ \ \P\ a \R\" - by (fastforce simp add:valid_def) +lemma hoare_post_subst: + "\ B = C; \A\ a \B\ \ \ \A\ a \C\" + by (erule subst) -lemma hoare_post_imp: "\ \r s. Q r s \ R r s; \P\ a \Q\ \ \ \P\ a \R\" +lemma hoare_post_imp: + "\ \rv s. Q rv s \ R rv s; \P\ a \Q\ \ \ \P\ a \R\" by(fastforce simp:valid_def split_def) -lemma hoare_post_impErr': "\ \P\ a \Q\,\E\; - \r s. Q r s \ R r s; - \e s. E e s \ F e s \ \ - \P\ a \R\,\F\" - apply (simp add: validE_def) - apply (rule_tac Q="\r s. case r of Inl a \ E a s | Inr b \ Q b s" in hoare_post_imp) - apply (case_tac r) - apply simp_all - done - -lemma hoare_post_impErr: "\ \P\ a \Q\,\E\; - \r s. Q r s \ R r s; - \e s. E e s \ F e s \ \ - \P\ a \R\,\F\" - apply (blast intro: hoare_post_impErr') - done +lemma hoare_post_impErr': (* FIXME lib: eliminate *) + "\ \P\ a \Q\,\E\; \rv s. Q rv s \ R rv s; \e s. E e s \ F e s \ \ \P\ a \R\,\F\" + unfolding validE_def valid_def + by (fastforce split: sum.splits) + +lemma hoare_post_impErr: + "\ \P\ a \Q\,\E\; \rv s. Q rv s \ R rv s; \e s. E e s \ F e s \ \ \P\ a \R\,\F\" + by (blast intro: hoare_post_impErr') lemma hoare_validE_cases: - "\ \ P \ f \ Q \, \ \_ _. True \; \ P \ f \ \_ _. True \, \ R \ \ - \ \ P \ f \ Q \, \ R \" - by (simp add: validE_def valid_def split: sum.splits) blast + "\ \P\ f \Q\, \\_ _. True\; \P\ f \\_ _. True\, \R\ \ \ \P\ f \Q\, \R\" + by (fastforce simp: validE_def valid_def split: sum.splits) lemma hoare_post_imp_dc: - "\\P\ a \\r. Q\; \s. Q s \ R s\ \ \P\ a \\r. R\,\\r. R\" - by (simp add: validE_def valid_def split: sum.splits) blast + "\\P\ a \\_. Q\; \s. Q s \ R s\ \ \P\ a \\_. R\, \\_. R\" + by (fastforce simp: validE_def valid_def split: sum.splits) lemma hoare_post_imp_dc2: - "\\P\ a \\r. Q\; \s. Q s \ R s\ \ \P\ a \\r. R\,\\r s. True\" - by (simp add: validE_def valid_def split: sum.splits) blast + "\\P\ a \\_. Q\; \s. Q s \ R s\ \ \P\ a \\_. R\, \\_. \\" + by (fastforce simp: validE_def valid_def split: sum.splits) lemma hoare_post_imp_dc2E: - "\\P\ a \\r. Q\; \s. Q s \ R s\ \ \P\ a \\r s. True\, \\r. R\" - by (simp add: validE_def valid_def split: sum.splits) fast - -lemma hoare_post_imp_dc2E_actual: - "\\P\ a \\r. R\\ \ \P\ a \\r s. True\, \\r. R\" - by (simp add: validE_def valid_def split: sum.splits) fast + "\\P\ a \\_. Q\; \s. Q s \ R s\ \ \P\ a \\_. \\, \\_. R\" + by (fastforce simp: validE_def valid_def split: sum.splits) lemma hoare_post_imp_dc2_actual: - "\\P\ a \\r. R\\ \ \P\ a \\r. R\, \\r s. True\" - by (simp add: validE_def valid_def split: sum.splits) fast + "\P\ a \\_. R\ \ \P\ a \\_. R\, \\_. \\" + by (rule hoare_post_imp_dc2) -lemma hoare_post_impE: "\ \r s. Q r s \ R r s; \P\ a \Q\ \ \ \P\ a \R\" - by (fastforce simp:valid_def split_def) +lemma hoare_post_imp_dc2E_actual: + "\P\ a \\_. R\ \ \P\ a \\_. \\, \\_. R\" + by (rule hoare_post_imp_dc2E) + +lemmas hoare_post_impE = hoare_post_imp (* FIXME lib: eliminate; probably should be on validE *) lemma hoare_conjD1: "\P\ f \\rv. Q rv and R rv\ \ \P\ f \\rv. Q rv\" @@ -846,129 +297,28 @@ lemma hoare_post_disjI2: "\P\ f \\rv. R rv\ \ \P\ f \\rv. Q rv or R rv\" unfolding valid_def by auto -lemma hoare_weaken_pre: - "\\Q\ a \R\; \s. P s \ Q s\ \ \P\ a \R\" - apply (rule hoare_pre_imp) - prefer 2 - apply assumption - apply blast - done +lemmas hoare_strengthen_post = hoare_post_imp[rotated] -lemma hoare_strengthen_post: - "\\P\ a \Q\; \r s. Q r s \ R r s\ \ \P\ a \R\" - apply (rule hoare_post_imp) - prefer 2 - apply assumption - apply blast - done +lemma use_valid: + "\(r, s') \ mres (f s); \P\ f \Q\; P s \ \ Q r s'" + unfolding valid_def by blast -lemma use_valid: "\(r, s') \ mres (f s); \P\ f \Q\; P s \ \ Q r s'" - apply (simp add: valid_def) - apply blast - done +lemmas post_by_hoare = use_valid[rotated] -lemma use_validE_norm: "\ (Inr r', s') \ mres (B s); \ P \ B \ Q \,\ E \; P s \ \ Q r' s'" - apply (clarsimp simp: validE_def valid_def) - apply force - done +lemma use_validE_norm: + "\ (Inr r', s') \ mres (B s); \P\ B \Q\,\ E \; P s \ \ Q r' s'" + unfolding validE_def valid_def by force -lemma use_validE_except: "\ (Inl r', s') \ mres (B s); \ P \ B \ Q \,\ E \; P s \ \ E r' s'" - apply (clarsimp simp: validE_def valid_def) - apply force - done +lemma use_validE_except: + "\ (Inl r', s') \ mres (B s); \P\ B \Q\,\ E \; P s \ \ E r' s'" + unfolding validE_def valid_def by force lemma in_inv_by_hoareD: - "\ \P. \P\ f \\_. P\; (x,s') \ mres (f s) \ \ s' = s" - apply (drule_tac x="(=) s" in meta_spec) - apply (auto simp add: valid_def mres_def) - done - -subsection "Satisfiability" - -lemma exs_hoare_post_imp: "\\r s. Q r s \ R r s; \P\ a \\Q\\ \ \P\ a \\R\" - apply (simp add: exs_valid_def) - apply safe - apply (erule_tac x=s in allE, simp) - apply blast - done - -lemma use_exs_valid: "\\P\ f \\Q\; P s \ \ \(r, s') \ mres (f s). Q r s'" - by (simp add: exs_valid_def) - -definition "exs_postcondition P f \ (\a b. \(rv, s)\ f a b. P rv s)" - -lemma exs_valid_is_triple: - "exs_valid P f Q = triple_judgement P f (exs_postcondition Q (\s f. mres (f s)))" - by (simp add: triple_judgement_def exs_postcondition_def exs_valid_def) - -lemmas [wp_trip] = exs_valid_is_triple - -lemma exs_valid_weaken_pre [wp_comb]: - "\ \ P' \ f \\ Q \; \s. P s \ P' s \ \ \ P \ f \\ Q \" - apply atomize - apply (clarsimp simp: exs_valid_def) - done + "\ \P. f \P\; (x,s') \ mres (f s) \ \ s' = s" + by (auto simp add: valid_def) blast -lemma exs_valid_chain: - "\ \ P \ f \\ Q \; \s. R s \ P s; \r s. Q r s \ S r s \ \ \ R \ f \\ S \" - by (fastforce simp only: exs_valid_def Bex_def ) -lemma exs_valid_assume_pre: - "\ \s. P s \ \ P \ f \\ Q \ \ \ \ P \ f \\ Q \" - apply (fastforce simp: exs_valid_def) - done - -lemma exs_valid_bind [wp_split]: - "\ \x. \B x\ g x \\C\; \A\ f \\B\ \ \ \ A \ f >>= (\x. g x) \\ C \" - apply atomize - apply (clarsimp simp: exs_valid_def bind_def2 mres_def) - apply (drule spec, drule(1) mp, clarsimp) - apply (drule spec2, drule(1) mp, clarsimp) - apply (simp add: image_def bex_Un) - apply (strengthen subst[where P="\x. x \ f s" for s, mk_strg I _ E], simp) - apply (fastforce elim: rev_bexI) - done - -lemma exs_valid_return [wp]: - "\ Q v \ return v \\ Q \" - by (clarsimp simp: exs_valid_def return_def mres_def) - -lemma exs_valid_select [wp]: - "\ \s. \r \ S. Q r s \ select S \\ Q \" - apply (clarsimp simp: exs_valid_def select_def mres_def) - apply (auto simp add: image_def) - done - -lemma exs_valid_get [wp]: - "\ \s. Q s s \ get \\ Q \" - by (clarsimp simp: exs_valid_def get_def mres_def) - -lemma exs_valid_gets [wp]: - "\ \s. Q (f s) s \ gets f \\ Q \" - by (clarsimp simp: gets_def) wp - -lemma exs_valid_put [wp]: - "\ Q v \ put v \\ Q \" - by (clarsimp simp: put_def exs_valid_def mres_def) - -lemma exs_valid_state_assert [wp]: - "\ \s. Q () s \ G s \ state_assert G \\ Q \" - by (clarsimp simp: state_assert_def exs_valid_def get_def - assert_def bind_def2 return_def mres_def) - -lemmas exs_valid_guard = exs_valid_state_assert - -lemma exs_valid_fail [wp]: - "\ \_. False \ fail \\ Q \" - by (clarsimp simp: fail_def exs_valid_def) - -lemma exs_valid_condition [wp]: - "\ \ P \ L \\ Q \; \ P' \ R \\ Q \ \ \ - \ \s. (C s \ P s) \ (\ C s \ P' s) \ condition C L R \\ Q \" - by (clarsimp simp: condition_def exs_valid_def split: sum.splits) - - -subsection MISC +subsection \Misc\ lemma hoare_return_simp: "\P\ return x \Q\ = (\s. P s \ Q x s)" @@ -978,381 +328,319 @@ lemma hoare_gen_asm: "(P \ \P'\ f \Q\) \ \P' and K P\ f \Q\" by (fastforce simp add: valid_def) -lemma when_wp [wp]: - "\ P \ \Q\ f \R\ \ \ \if P then Q else R ()\ when P f \R\" - by (clarsimp simp: when_def valid_def return_def mres_def) - lemma hoare_conjI: "\ \P\ f \Q\; \P\ f \R\ \ \ \P\ f \\r s. Q r s \ R r s\" unfolding valid_def by blast lemma hoare_disjI1: - "\ \P\ f \Q\ \ \ \P\ f \\r s. Q r s \ R r s \" + "\ \P\ f \Q\ \ \ \P\ f \\rv s. Q rv s \ R rv s \" unfolding valid_def by blast lemma hoare_disjI2: - "\ \P\ f \R\ \ \ \P\ f \\r s. Q r s \ R r s \" + "\ \P\ f \R\ \ \ \P\ f \\rv s. Q rv s \ R rv s \" unfolding valid_def by blast lemma hoare_assume_pre: "(\s. P s \ \P\ f \Q\) \ \P\ f \Q\" by (auto simp: valid_def) -lemma hoare_returnOk_sp: - "\P\ returnOk x \\r s. r = x \ P s\, \Q\" - by (simp add: valid_def validE_def returnOk_def return_def mres_def) - lemma hoare_assume_preE: "(\s. P s \ \P\ f \Q\,\R\) \ \P\ f \Q\,\R\" by (auto simp: valid_def validE_def) lemma hoare_allI: - "(\x. \P\f\Q x\) \ \P\f\\r s. \x. Q x r s\" + "(\x. \P\f\Q x\) \ \P\f\\rv s. \x. Q x rv s\" by (simp add: valid_def) blast lemma validE_allI: - "(\x. \P\ f \\r s. Q x r s\,\E\) \ \P\ f \\r s. \x. Q x r s\,\E\" + "(\x. \P\ f \\r s. Q x r s\,\E\) \ \P\ f \\rv s. \x. Q x rv s\,\E\" by (fastforce simp: valid_def validE_def split: sum.splits) lemma hoare_exI: - "\P\ f \Q x\ \ \P\ f \\r s. \x. Q x r s\" + "\P\ f \Q x\ \ \P\ f \\rv s. \x. Q x rv s\" by (simp add: valid_def) blast lemma hoare_impI: - "(R \ \P\f\Q\) \ \P\f\\r s. R \ Q r s\" + "(R \ \P\ f \Q\) \ \P\ f \\rv s. R \ Q rv s\" by (simp add: valid_def) blast lemma validE_impI: - " \\E. \P\ f \\_ _. True\,\E\; (P' \ \P\ f \Q\,\E\)\ \ - \P\ f \\r s. P' \ Q r s\, \E\" + "\\E. \P\ f \\_ _. True\,\E\; (P' \ \P\ f \Q\,\E\)\ \ + \P\ f \\rv s. P' \ Q rv s\, \E\" by (fastforce simp: validE_def valid_def split: sum.splits) lemma hoare_case_option_wp: - "\ \P\ f None \Q\; - \x. \P' x\ f (Some x) \Q' x\ \ + "\ \P\ f None \Q\; \x. \P' x\ f (Some x) \Q' x\ \ \ \case_option P P' v\ f v \\rv. case v of None \ Q rv | Some x \ Q' x rv\" by (cases v) auto -subsection "Reasoning directly about states" - -lemma in_throwError: - "((v, s') \ mres (throwError e s)) = (v = Inl e \ s' = s)" - by (simp add: throwError_def return_def mres_def) - -lemma in_returnOk: - "((v', s') \ mres (returnOk v s)) = (v' = Inr v \ s' = s)" - by (simp add: returnOk_def return_def mres_def) - -lemma in_bind: - "((r,s') \ mres ((do x \ f; g x od) s)) = - (\s'' x. (x, s'') \ mres (f s) \ (r, s') \ mres (g x s''))" - apply (simp add: bind_def split_def mres_def) - apply (auto split: tmres.splits; force elim: rev_bexI image_eqI[rotated]) - done - -lemma in_bindE_R: - "((Inr r,s') \ mres ((doE x \ f; g x odE) s)) = - (\s'' x. (Inr x, s'') \ mres (f s) \ (Inr r, s') \ mres (g x s''))" - apply (simp add: bindE_def in_bind) - apply (simp add: lift_def split_def) - apply (clarsimp simp: throwError_def return_def lift_def mres_def split: sum.splits) - apply force - done - -lemma in_bindE_L: - "((Inl r, s') \ mres ((doE x \ f; g x odE) s)) \ - (\s'' x. (Inr x, s'') \ mres (f s) \ (Inl r, s') \ mres (g x s'')) \ ((Inl r, s') \ mres (f s))" - apply (simp add: bindE_def in_bind lift_def) - apply safe - apply (simp add: return_def throwError_def lift_def split_def mres_def split: sum.splits if_split_asm) - apply force+ - done +lemma hoare_vcg_prop: + "\\s. P\ f \\rv s. P\" + by (simp add: valid_def) -lemma in_return: - "(r, s') \ mres (return v s) = (r = v \ s' = s)" - by (simp add: return_def mres_def) -lemma in_liftE: - "((v, s') \ mres (liftE f s)) = (\v'. v = Inr v' \ (v', s') \ mres (f s))" - by (auto simp add: liftE_def in_bind in_return) +subsection \@{const valid} and @{const validE}, @{const validE_R}, @{const validE_E}\ -lemma in_whenE: "((v, s') \ mres (whenE P f s)) = ((P \ (v, s') \ mres (f s)) \ - (\P \ v = Inr () \ s' = s))" - by (simp add: whenE_def in_returnOk) +lemma valid_validE: + "\P\ f \\_. Q\ \ \P\ f \\_. Q\, \\_. Q\" + by (rule hoare_post_imp_dc) -lemma inl_whenE: - "((Inl x, s') \ mres (whenE P f s)) = (P \ (Inl x, s') \ mres (f s))" - by (auto simp add: in_whenE) +lemma valid_validE2: + "\ \P\ f \\_. Q'\; \s. Q' s \ Q s; \s. Q' s \ E s \ \ \P\ f \\_. Q\, \\_. E\" + unfolding valid_def validE_def + by (clarsimp split: sum.splits) blast -lemma in_fail: - "r \ mres (fail s) = False" - by (simp add: fail_def mres_def) +lemma validE_valid: + "\P\ f \\_. Q\, \\_. Q\ \ \P\ f \\_. Q\" + unfolding validE_def valid_def + by fastforce -lemma in_assert: - "(r, s') \ mres (assert P s) = (P \ s' = s)" - by (auto simp add: assert_def return_def fail_def mres_def) +lemma valid_validE_R: + "\P\ f \\_. Q\ \ \P\ f \\_. Q\,-" + by (simp add: validE_R_def hoare_post_impErr [OF valid_validE]) -lemma in_assertE: - "(r, s') \ mres (assertE P s) = (P \ r = Inr () \ s' = s)" - by (auto simp add: assertE_def returnOk_def return_def fail_def mres_def) +lemma valid_validE_E: + "\P\ f \\_. Q\ \ \P\ f -,\\_. Q\" + by (simp add: validE_E_def hoare_post_impErr [OF valid_validE]) -lemma in_assert_opt: - "(r, s') \ mres (assert_opt v s) = (v = Some r \ s' = s)" - by (auto simp: assert_opt_def in_fail in_return split: option.splits) +lemma validE_validE_R: + "\P\ f \Q\,\\\\ \ \P\ f \Q\,-" + by (simp add: validE_R_def) -lemma in_get: - "(r, s') \ mres (get s) = (r = s \ s' = s)" - by (simp add: get_def mres_def) +lemma validE_R_validE: + "\P\ f \Q\,- \ \P\ f \Q\,\\\\" + by (simp add: validE_R_def) -lemma in_gets: - "(r, s') \ mres (gets f s) = (r = f s \ s' = s)" - by (simp add: simpler_gets_def mres_def) +lemma validE_validE_E: + "\P\ f \\\\, \E\ \ \P\ f -, \E\" + by (simp add: validE_E_def) -lemma in_put: - "(r, s') \ mres (put x s) = (s' = x \ r = ())" - by (simp add: put_def mres_def) +lemma validE_E_validE: + "\P\ f -, \E\ \ \P\ f \\\\, \E\" + by (simp add: validE_E_def) -lemma in_when: - "(v, s') \ mres (when P f s) = ((P \ (v, s') \ mres (f s)) \ (\P \ v = () \ s' = s))" - by (simp add: when_def in_return) -lemma in_modify: - "(v, s') \ mres (modify f s) = (s'=f s \ v = ())" - by (auto simp add: modify_def bind_def get_def put_def mres_def) +subsection \@{const liftM}\ -lemma gets_the_in_monad: - "((v, s') \ mres (gets_the f s)) = (s' = s \ f s = Some v)" - by (auto simp: gets_the_def in_bind in_gets in_assert_opt split: option.split) +lemma in_image_constant: + "(x \ (\_. v) ` S) = (x = v \ S \ {})" + by (simp add: image_constant_conv) -lemma in_alternative: - "(r,s') \ mres ((f \ g) s) = ((r,s') \ mres (f s) \ (r,s') \ mres (g s))" - by (auto simp add: alternative_def mres_def) +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: valid_def Ball_def mres_def image_Un) + apply (simp add: image_image in_image_constant) + apply force + done -lemmas in_monad = inl_whenE in_whenE in_liftE in_bind in_bindE_L - in_bindE_R in_returnOk in_throwError in_fail - in_assertE in_assert in_return in_assert_opt - in_get in_gets in_put in_when (* unlessE_whenE *) - (* unless_when *) in_modify gets_the_in_monad - in_alternative +lemma hoare_liftME_subst: + "\P\ liftME f m \Q\, \E\ = \P\ m \Q \ f\, \E\" + unfolding validE_def liftME_liftM hoare_liftM_subst o_def + by (fastforce intro!: arg_cong[where f="valid P m"] split: sum.splits) -subsection "Non-Failure" +lemma liftE_validE[simp]: + "\P\ liftE f \Q\, \E\ = \P\ f \Q\" + by (simp add: liftE_liftM validE_def hoare_liftM_subst o_def) -lemma no_failD: - "\ no_fail P m; P s \ \ Failed \ snd ` m s" - by (simp add: no_fail_def) -lemma no_fail_modify [wp,simp]: - "no_fail \ (modify f)" - by (simp add: no_fail_def modify_def get_def put_def bind_def) +subsection \Operator lifting/splitting\ -lemma no_fail_gets_simp[simp]: - "no_fail P (gets f)" - unfolding no_fail_def gets_def get_def return_def bind_def +lemma hoare_vcg_if_split: + "\ P \ \Q\ f \S\; \P \ \R\ g \S\ \ \ \\s. (P \ Q s) \ (\P \ R s)\ if P then f else g \S\" by simp -lemma no_fail_gets: - "no_fail \ (gets f)" +lemma hoare_vcg_if_splitE: + "\ P \ \Q\ f \S\,\E\; \P \ \R\ g \S\,\E\ \ \ + \\s. (P \ Q s) \ (\P \ R s)\ if P then f else g \S\,\E\" by simp -lemma snd_pair_image: - "snd ` Pair x ` S = S" - by (simp add: image_def) - -lemma no_fail_select [simp]: - "no_fail \ (select S)" - by (simp add: no_fail_def select_def image_def) +lemma hoare_vcg_split_case_option: + "\ \x. x = None \ \P x\ f x \R x\; \x y. x = Some y \ \Q x y\ g x y \R x\ \ \ + \\s. (x = None \ P x s) \ (\y. x = Some y \ Q x y s)\ + case x of None \ f x | Some y \ g x y + \R x\" + by (cases x; simp) -lemma no_fail_pre: - "\ no_fail P f; \s. Q s \ P s\ \ no_fail Q f" - by (simp add: no_fail_def) +lemma hoare_vcg_split_case_optionE: + "\ \x. x = None \ \P x\ f x \R x\,\E x\; \x y. x = Some y \ \Q x y\ g x y \R x\,\E x\ \ \ + \\s. (x = None \ P x s) \ (\y. x = Some y \ Q x y s)\ + case x of None \ f x | Some y \ g x y + \R x\, \E x\" + by (cases x; simp) -lemma no_fail_alt [wp]: - "\ no_fail P f; no_fail Q g \ \ no_fail (P and Q) (f \ g)" - by (auto simp add: no_fail_def alternative_def) +lemma hoare_vcg_split_case_sum: + "\ \x a. x = Inl a \ \P x a\ f x a \R x\; \x b. x = Inr b \ \Q x b\ g x b \R x\ \ \ + \\s. (\a. x = Inl a \ P x a s) \ (\b. x = Inr b \ Q x b s) \ + case x of Inl a \ f x a | Inr b \ g x b + \R x\" + by (cases x; simp) -lemma no_fail_return [simp, wp]: - "no_fail \ (return x)" - by (simp add: return_def no_fail_def) +lemmas hoare_vcg_precond_imp = hoare_weaken_pre (* FIXME lib: eliminate *) -lemma no_fail_get [simp, wp]: - "no_fail \ get" - by (simp add: get_def no_fail_def) +lemmas hoare_seq_ext = seq_ext[rotated] +lemmas hoare_vcg_seqE = seqE[rotated] -lemma no_fail_put [simp, wp]: - "no_fail \ (put s)" - by (simp add: put_def no_fail_def) +lemma hoare_seq_ext_nobind: + "\ \B\ g \C\; \A\ f \\_. B\ \ \ \A\ do f; g od \C\" + by (erule seq_ext) (clarsimp simp: valid_def) -lemma no_fail_when [wp]: - "(P \ no_fail Q f) \ no_fail (if P then Q else \) (when P f)" - by (simp add: when_def) +lemma hoare_seq_ext_nobindE: + "\ \B\ g \C\, \E\; \A\ f \\_. B\, \E\ \ \ \A\ doE f; g odE \C\, \E\" + by (erule seqE) (clarsimp simp: validE_def) -lemma no_fail_unless [wp]: - "(\P \ no_fail Q f) \ no_fail (if P then \ else Q) (unless P f)" - by (simp add: unless_def when_def) +lemmas hoare_seq_ext_skip' = hoare_seq_ext[where Q'=Q and Q=Q for Q] -lemma no_fail_fail [simp, wp]: - "no_fail \ fail" - by (simp add: fail_def no_fail_def) +lemma hoare_chain: + "\ \P\ f \Q\; \s. R s \ P s; \rv s. Q rv s \ S rv s \ \ \R\ f \S\" + by (wp_pre, rule hoare_post_imp) -lemmas [wp] = no_fail_gets +lemma validE_weaken: (* FIXME lib: eliminate in favour of hoare_chainE *) + "\ \P'\ A \Q'\,\E'\; \s. P s \ P' s; \rv s. Q' rv s \ Q rv s; \rv s. E' rv s \ E rv s \ + \ \P\ A \Q\,\E\" + by wp_pre (rule hoare_post_impErr) -lemma no_fail_assert [simp, wp]: - "no_fail (\_. P) (assert P)" - by (simp add: assert_def) +lemmas hoare_chainE = validE_weaken -lemma no_fail_assert_opt [simp, wp]: - "no_fail (\_. P \ None) (assert_opt P)" - by (simp add: assert_opt_def split: option.splits) +lemma hoare_vcg_conj_lift: + "\ \P\ f \Q\; \P'\ f \Q'\ \ \ \\s. P s \ P' s\ f \\rv s. Q rv s \ Q' rv s\" + unfolding valid_def + by fastforce -lemma no_fail_case_option [wp]: - assumes f: "no_fail P f" - assumes g: "\x. no_fail (Q x) (g x)" - shows "no_fail (if x = None then P else Q (the x)) (case_option f g x)" - by (clarsimp simp add: f g) +lemma hoare_vcg_conj_liftE1: + "\ \P\ f \Q\,-; \P'\ f \Q'\,\E\ \ \ \P and P'\ f \\rv s. Q rv s \ Q' rv s\,\E\" + unfolding valid_def validE_R_def validE_def + by (fastforce simp: split_def split: sum.splits) -lemma no_fail_if [wp]: - "\ P \ no_fail Q f; \P \ no_fail R g \ \ - no_fail (if P then Q else R) (if P then f else g)" - by simp +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 + by fastforce -lemma no_fail_apply [wp]: - "no_fail P (f (g x)) \ no_fail P (f $ g x)" - by simp +lemma hoare_vcg_const_Ball_lift: + "\ \x. x \ S \ \P x\ f \Q x\ \ \ \\s. \x\S. P x s\ f \\rv s. \x\S. Q x rv s\" + by (fastforce simp: valid_def) -lemma no_fail_undefined [simp, wp]: - "no_fail \ undefined" - by (simp add: no_fail_def) +lemma hoare_vcg_const_Ball_lift_R: + "\ \x. x \ S \ \P x\ f \Q x\,- \ \ \\s. \x \ S. P x s\ f \\rv s. \x \ S. Q x rv s\,-" + unfolding validE_R_def validE_def + by (rule hoare_strengthen_post) + (fastforce intro!: hoare_vcg_const_Ball_lift split: sum.splits)+ -lemma no_fail_returnOK [simp, wp]: - "no_fail \ (returnOk x)" - by (simp add: returnOk_def) +lemma hoare_vcg_all_lift: + "\ \x. \P x\ f \Q x\ \ \ \\s. \x. P x s\ f \\rv s. \x. Q x rv s\" + by (fastforce simp: valid_def) -(* text {* Empty results implies non-failure *} +lemma hoare_vcg_all_lift_R: + "(\x. \P x\ f \Q x\, -) \ \\s. \x. P x s\ f \\rv s. \x. Q x rv s\, -" + by (rule hoare_vcg_const_Ball_lift_R[where S=UNIV, simplified]) -lemma empty_fail_modify [simp]: - "empty_fail (modify f)" - by (simp add: empty_fail_def simpler_modify_def) +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 empty_fail_gets [simp]: - "empty_fail (gets f)" - by (simp add: empty_fail_def simpler_gets_def) +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) -lemma empty_failD: - "\ empty_fail m; fst (m s) = {} \ \ snd (m s)" - by (simp add: empty_fail_def) +lemma hoare_weak_lift_imp: + "\P'\ f \Q\ \ \\s. P \ P' s\ f \\rv s. P \ Q rv s\" + by (auto simp add: valid_def split_def) -lemma empty_fail_select_f [simp]: - assumes ef: "fst S = {} \ snd S" - shows "empty_fail (select_f S)" - by (fastforce simp add: empty_fail_def select_f_def intro: ef) +lemma hoare_vcg_ex_lift: + "\ \x. \P x\ f \Q x\ \ \ \\s. \x. P x s\ f \\rv s. \x. Q x rv s\" + by (clarsimp simp: valid_def, blast) -lemma empty_fail_bind [simp]: - "\ empty_fail a; \x. empty_fail (b x) \ \ empty_fail (a >>= b)" - apply (simp add: bind_def empty_fail_def split_def) - apply clarsimp - apply (case_tac "fst (a s) = {}") - apply blast - apply (clarsimp simp: ex_in_conv [symmetric]) - done +lemma hoare_vcg_ex_lift_R1: + "(\x. \P x\ f \Q\, -) \ \\s. \x. P x s\ f \Q\, -" + by (fastforce simp: valid_def validE_R_def validE_def split: sum.splits) -lemma empty_fail_return [simp]: - "empty_fail (return x)" - by (simp add: empty_fail_def return_def) - -lemma empty_fail_mapM [simp]: - assumes m: "\x. empty_fail (m x)" - shows "empty_fail (mapM m xs)" -proof (induct xs) - case Nil - thus ?case by (simp add: mapM_def sequence_def) -next - case Cons - have P: "\m x xs. mapM m (x # xs) = (do y \ m x; ys \ (mapM m xs); return (y # ys) od)" - by (simp add: mapM_def sequence_def Let_def) - from Cons - show ?case by (simp add: P m) -qed - -lemma empty_fail [simp]: - "empty_fail fail" - by (simp add: fail_def empty_fail_def) - -lemma empty_fail_assert_opt [simp]: - "empty_fail (assert_opt x)" - by (simp add: assert_opt_def split: option.splits) - -lemma empty_fail_mk_ef: - "empty_fail (mk_ef o m)" - by (simp add: empty_fail_def mk_ef_def) - *) -subsection "Failure" +(* for instantiations *) +lemma hoare_triv: "\P\f\Q\ \ \P\f\Q\" . +lemma hoare_trivE: "\P\ f \Q\,\E\ \ \P\ f \Q\,\E\" . +lemma hoare_trivE_R: "\P\ f \Q\,- \ \P\ f \Q\,-" . +lemma hoare_trivR_R: "\P\ f -,\E\ \ \P\ f -,\E\" . -lemma fail_wp: "\\x. True\ fail \Q\" - by (simp add: valid_def fail_def mres_def vimage_def) +lemma hoare_vcg_E_conj: + "\ \P\ f -,\E\; \P'\ f \Q'\,\E'\ \ \ \\s. P s \ P' s\ f \Q'\, \\rv s. E rv s \ E' rv s\" + unfolding validE_def validE_E_def + by (rule hoare_post_imp[OF _ hoare_vcg_conj_lift]; simp split: sum.splits) -lemma failE_wp: "\\x. True\ fail \Q\,\E\" - by (simp add: validE_def fail_wp) +lemma hoare_vcg_E_elim: + "\ \P\ f -,\E\; \P'\ f \Q\,- \ \ \\s. P s \ P' s\ f \Q\,\E\" + by (rule hoare_post_impErr[OF hoare_vcg_E_conj]) (simp add: validE_R_def)+ -lemma fail_update [iff]: - "fail (f s) = fail s" - by (simp add: fail_def) +lemma hoare_vcg_R_conj: + "\ \P\ f \Q\,-; \P'\ f \Q'\,- \ \ \\s. P s \ P' s\ f \\rv s. Q rv s \ Q' rv s\,-" + unfolding validE_R_def validE_def + by (rule hoare_post_imp[OF _ hoare_vcg_conj_lift]; simp split: sum.splits) +lemma hoare_post_imp_R: + "\ \P\ f \Q'\,-; \rv s. Q' rv s \ Q rv s \ \ \P\ f \Q\,-" + unfolding validE_R_def + by (erule hoare_post_impErr) -text \We can prove postconditions using hoare triples\ +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 post_by_hoare: "\ \P\ f \Q\; P s; (r, s') \ mres (f s) \ \ Q r s'" - apply (simp add: valid_def) - apply blast - done -text \Weakest Precondition Rules\ +subsection \Weakest Precondition Rules\ -lemma hoare_vcg_prop: - "\\s. P\ f \\rv s. P\" - by (simp add: valid_def) +lemma fail_wp: + "\\\ fail \Q\" + by (simp add: valid_def fail_def mres_def vimage_def) lemma return_wp: "\P x\ return x \P\" - by(simp add:valid_def return_def mres_def) + by(simp add: valid_def return_def mres_def) + +lemma get_wp: + "\\s. Q s s\ get \Q\" + by (simp add: get_def valid_def mres_def) -(* lemma get_wp: - "\\s. P s s\ get \P\" - by(auto simp add:valid_def split_def get_def mres_def) - *) lemma gets_wp: "\\s. P (f s) s\ gets f \P\" - by(simp add:valid_def split_def gets_def return_def get_def bind_def mres_def) + by(simp add: valid_def split_def gets_def return_def get_def bind_def mres_def) + +lemma put_wp: + "\\_. Q () s\ put s \Q\" + by (simp add: put_def valid_def mres_def) + +lemma modify_wp: + "\\s. Q () (f s)\ modify f \Q\" + unfolding modify_def + by (wp put_wp get_wp) + +lemma failE_wp: + "\\\ fail \Q\, \E\" + by (simp add: validE_def fail_wp) -(* lemma modify_wp: - "\\s. P () (f s)\ modify f \P\" - by(simp add:valid_def split_def modify_def get_def put_def bind_def ) - *) -(* lemma put_wp: - "\\s. P () x\ put x \P\" - by(simp add:valid_def put_def) - *) lemma returnOk_wp: "\P x\ returnOk x \P\,\E\" - by(simp add:validE_def2 returnOk_def return_def mres_def) + by (simp add: validE_def2 returnOk_def return_def mres_def) lemma throwError_wp: "\E e\ throwError e \P\,\E\" - by(simp add:validE_def2 throwError_def return_def mres_def) + by(simp add: validE_def2 throwError_def return_def mres_def) -lemma returnOKE_R_wp : "\P x\ returnOk x \P\, -" +lemma returnOKE_R_wp: + "\P x\ returnOk x \P\, -" by (simp add: validE_R_def validE_def valid_def returnOk_def return_def mres_def) +lemma liftE_wp: + "\P\ f \Q\ \ \P\ liftE f \Q\,\E\" + by simp + lemma catch_wp: - "\ \x. \E x\ handler x \Q\; \P\ f \Q\,\E\ \ \ - \P\ catch f handler \Q\" + "\ \x. \E x\ handler x \Q\; \P\ f \Q\,\E\ \ \ \P\ catch f handler \Q\" apply (unfold catch_def validE_def) apply (erule seq_ext) apply (simp add: return_wp split: sum.splits) done lemma handleE'_wp: - "\ \x. \F x\ handler x \Q\,\E\; \P\ f \Q\,\F\ \ \ - \P\ f handler \Q\,\E\" + "\ \x. \F x\ handler x \Q\,\E\; \P\ f \Q\,\F\ \ \ \P\ f handler \Q\,\E\" apply (unfold handleE'_def validE_def) apply (erule seq_ext) apply (clarsimp split: sum.splits) @@ -1365,171 +653,30 @@ lemma handleE_wp: shows "\P\ f handler \Q\,\E\" by (simp add: handleE_def handleE'_wp [OF x y]) -lemma hoare_vcg_split_if: - "\ P \ \Q\ f \S\; \P \ \R\ g \S\ \ \ - \\s. (P \ Q s) \ (\P \ R s)\ if P then f else g \S\" - by simp - -lemma hoare_vcg_split_ifE: - "\ P \ \Q\ f \S\,\E\; \P \ \R\ g \S\,\E\ \ \ - \\s. (P \ Q s) \ (\P \ R s)\ if P then f else g \S\,\E\" - by simp - -lemma in_image_constant: - "(x \ (\_. v) ` S) = (x = v \ S \ {})" - by (simp add: image_constant_conv) - -lemma hoare_liftM_subst: "\P\ liftM f m \Q\ = \P\ m \Q \ f\" - apply (simp add: liftM_def bind_def2 return_def split_def mres_def) - apply (simp add: valid_def Ball_def mres_def image_Un) - apply (simp add: image_image in_image_constant) - apply (rule_tac f=All in arg_cong) - apply (rule ext) - apply force - done - -lemma liftE_validE[simp]: "\P\ liftE f \Q\,\E\ = \P\ f \Q\" - apply (simp add: liftE_liftM validE_def hoare_liftM_subst o_def) - done - -lemma liftE_wp: - "\P\ f \Q\ \ \P\ liftE f \Q\,\E\" - by simp - -lemma liftM_wp: "\P\ m \Q \ f\ \ \P\ liftM f m \Q\" +lemma liftM_wp: + "\P\ m \Q \ f\ \ \P\ liftM f m \Q\" by (simp add: hoare_liftM_subst) -lemma hoare_liftME_subst: "\P\ liftME f m \Q\,\E\ = \P\ m \Q \ f\,\E\" - apply (simp add: validE_def liftME_liftM hoare_liftM_subst o_def) - apply (rule_tac f="valid P m" in arg_cong) - apply (rule ext)+ - apply (case_tac x, simp_all) - done - -lemma liftME_wp: "\P\ m \Q \ f\,\E\ \ \P\ liftME f m \Q\,\E\" +lemma liftME_wp: + "\P\ m \Q \ f\,\E\ \ \P\ liftME f m \Q\,\E\" by (simp add: hoare_liftME_subst) -(* FIXME: Move *) -lemma o_const_simp[simp]: "(\x. C) \ f = (\x. C)" - by (simp add: o_def) - -lemma hoare_vcg_split_case_option: - "\ \x. x = None \ \P x\ f x \R x\; - \x y. x = Some y \ \Q x y\ g x y \R x\ \ \ - \\s. (x = None \ P x s) \ - (\y. x = Some y \ Q x y s)\ - case x of None \ f x - | Some y \ g x y - \R x\" - apply(simp add:valid_def split_def) - apply(case_tac x, simp_all) -done - -lemma hoare_vcg_split_case_optionE: - assumes none_case: "\x. x = None \ \P x\ f x \R x\,\E x\" - assumes some_case: "\x y. x = Some y \ \Q x y\ g x y \R x\,\E x\" - shows "\\s. (x = None \ P x s) \ - (\y. x = Some y \ Q x y s)\ - case x of None \ f x - | Some y \ g x y - \R x\,\E x\" - apply(case_tac x, simp_all) - apply(rule none_case, simp) - apply(rule some_case, simp) -done - -lemma hoare_vcg_split_case_sum: - "\ \x a. x = Inl a \ \P x a\ f x a \R x\; - \x b. x = Inr b \ \Q x b\ g x b \R x\ \ \ - \\s. (\a. x = Inl a \ P x a s) \ - (\b. x = Inr b \ Q x b s) \ - case x of Inl a \ f x a - | Inr b \ g x b - \R x\" - apply(simp add:valid_def split_def) - apply(case_tac x, simp_all) -done - -lemma hoare_vcg_split_case_sumE: - assumes left_case: "\x a. x = Inl a \ \P x a\ f x a \R x\" - assumes right_case: "\x b. x = Inr b \ \Q x b\ g x b \R x\" - shows "\\s. (\a. x = Inl a \ P x a s) \ - (\b. x = Inr b \ Q x b s) \ - case x of Inl a \ f x a - | Inr b \ g x b - \R x\" - apply(case_tac x, simp_all) - apply(rule left_case, simp) - apply(rule right_case, simp) -done - -lemma hoare_vcg_precond_imp: - "\ \Q\ f \R\; \s. P s \ Q s \ \ \P\ f \R\" - by (fastforce simp add:valid_def) - -lemma hoare_vcg_precond_impE: - "\ \Q\ f \R\,\E\; \s. P s \ Q s \ \ \P\ f \R\,\E\" - by (fastforce simp add:validE_def2) - -lemma hoare_seq_ext: - assumes g_valid: "\x. \B x\ g x \C\" - assumes f_valid: "\A\ f \B\" - shows "\A\ do x \ f; g x od \C\" - apply(insert f_valid g_valid) - apply(blast intro: seq_ext') -done - -lemma hoare_vcg_seqE: - assumes g_valid: "\x. \B x\ g x \C\,\E\" - assumes f_valid: "\A\ f \B\,\E\" - shows "\A\ doE x \ f; g x odE \C\,\E\" - apply(insert f_valid g_valid) - apply(blast intro: seqE') -done - -lemma hoare_seq_ext_nobind: - "\ \B\ g \C\; - \A\ f \\r s. B s\ \ \ - \A\ do f; g od \C\" - apply (erule seq_ext) - apply (clarsimp simp: valid_def) - done - -lemma hoare_seq_ext_nobindE: - "\ \B\ g \C\,\E\; - \A\ f \\r s. B s\,\E\ \ \ - \A\ doE f; g odE \C\,\E\" - apply (erule seqE) - apply (clarsimp simp:validE_def) - done - -lemma hoare_chain: - "\ \P\ f \Q\; - \s. R s \ P s; - \r s. Q r s \ S r s \ \ - \R\ f \S\" - by(fastforce simp add:valid_def split_def) - -lemma validE_weaken: - "\ \P'\ A \Q'\,\E'\; \s. P s \ P' s; \r s. Q' r s \ Q r s; \r s. E' r s \ E r s \ \ \P\ A \Q\,\E\" - by (fastforce simp: validE_def2 split: sum.splits) +lemma assert_wp: + "\\s. P \ Q () s\ assert P \Q\" + unfolding assert_def + by (wpsimp wp: return_wp fail_wp | rule conjI)+ -lemmas hoare_chainE = validE_weaken +lemma list_cases_wp: + assumes a: "\P_A\ a \Q\" + assumes b: "\x xs. ts = x#xs \ \P_B x xs\ b x xs \Q\" + shows "\case_list P_A P_B ts\ case ts of [] \ a | x # xs \ b x xs \Q\" + by (cases ts, auto simp: a b) lemma hoare_vcg_handle_elseE: - "\ \P\ f \Q\,\E\; - \e. \E e\ g e \R\,\F\; - \x. \Q x\ h x \R\,\F\ \ \ + "\ \P\ f \Q\,\E\; \e. \E e\ g e \R\,\F\; \x. \Q x\ h x \R\,\F\ \ \ \P\ f g h \R\,\F\" - apply (simp add: handle_elseE_def validE_def) - apply (rule seq_ext) - apply assumption - apply (simp split: sum.split) - done - -lemma in_mres: - "(tr, Result (rv, s)) \ S \ (rv, s) \ mres S" - by (fastforce simp: mres_def intro: image_eqI[rotated]) + unfolding handle_elseE_def validE_def + by (wpsimp wp: seq_ext | assumption | rule conjI)+ lemma alternative_wp: assumes x: "\P\ f \Q\" @@ -1540,1046 +687,397 @@ lemma alternative_wp: by fastforce lemma alternativeE_wp: - assumes x: "\P\ f \Q\,\E\" and y: "\P'\ f' \Q\,\E\" - shows "\P and P'\ f \ f' \Q\,\E\" - apply (unfold validE_def) - apply (wp add: x y alternative_wp | simp | fold validE_def)+ - done + assumes "\P\ f \Q\,\E\" + assumes "\P'\ f' \Q\,\E\" + shows "\P and P'\ f \ f' \Q\,\E\" + unfolding validE_def + by (wpsimp wp: assms alternative_wp | fold validE_def)+ lemma alternativeE_R_wp: "\ \P\ f \Q\,-; \P'\ f' \Q\,- \ \ \P and P'\ f \ f' \Q\,-" - apply (simp add: validE_R_def) - apply (rule alternativeE_wp) - apply assumption+ - done + unfolding validE_R_def + by (rule alternativeE_wp) -lemma alternative_R_wp: +lemma alternativeE_E_wp: "\ \P\ f -,\Q\; \P'\ g -,\Q\ \ \ \P and P'\ f \ g -, \Q\" - apply (simp add: validE_E_def) - apply (rule alternativeE_wp) - apply assumption+ - done + unfolding validE_E_def + by (rule alternativeE_wp) -lemma state_select_wp [wp]: "\ \s. \t. (s, t) \ f \ P () t \ state_select f \ P \" +lemma select_wp: + "\\s. \x \ S. Q x s\ select S \Q\" + by (simp add: select_def valid_def mres_def image_def) + +lemma state_select_wp: + "\ \s. \t. (s, t) \ f \ P () t \ state_select f \P\" apply (clarsimp simp: state_select_def assert_def) apply (rule hoare_weaken_pre) - apply (wp select_wp hoare_vcg_split_if return_wp fail_wp) + apply (wp put_wp select_wp hoare_vcg_if_split return_wp fail_wp get_wp) apply simp done -lemma condition_wp [wp]: - "\ \ Q \ A \ P \; \ R \ B \ P \ \ \ \ \s. if C s then Q s else R s \ condition C A B \ P \" - apply (clarsimp simp: condition_def) - apply (clarsimp simp: valid_def pred_conj_def pred_neg_def split_def) - done - -lemma conditionE_wp [wp]: - "\ \ P \ A \ Q \,\ R \; \ P' \ B \ Q \,\ R \ \ \ \ \s. if C s then P s else P' s \ condition C A B \Q\,\R\" - apply (clarsimp simp: condition_def) - apply (clarsimp simp: validE_def valid_def) - done - -lemma state_assert_wp [wp]: "\ \s. f s \ P () s \ state_assert f \ P \" - apply (clarsimp simp: state_assert_def get_def - assert_def bind_def valid_def return_def fail_def mres_def) - done - -text \The weakest precondition handler which works on conjunction\ - -lemma hoare_vcg_conj_lift: - 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\" - apply (subst pred_conj_def[symmetric], subst pred_conj_def[symmetric], rule hoare_post_conj) - apply (rule hoare_pre_imp [OF _ x], simp) - apply (rule hoare_pre_imp [OF _ y], simp) - done +lemma condition_wp: + "\ \Q\ A \P\; \R\ B \P\ \ \ \\s. if C s then Q s else R s\ condition C A B \P\" + by (clarsimp simp: condition_def valid_def) -lemma hoare_vcg_conj_liftE1: - "\ \P\ f \Q\,-; \P'\ f \Q'\,\E\ \ \ - \P and P'\ f \\r s. Q r s \ Q' r s\,\E\" - unfolding valid_def validE_R_def validE_def - apply (clarsimp simp: split_def split: sum.splits) - apply (erule allE, erule (1) impE) - apply (erule allE, erule (1) impE) - apply (drule (1) bspec) - apply (drule (1) bspec) - apply clarsimp - done +lemma conditionE_wp: + "\ \P\ A \Q\,\R\; \P'\ B \Q\,\R\ \ \ \\s. if C s then P s else P' s\ condition C A B \Q\,\R\" + by (clarsimp simp: condition_def validE_def valid_def) -lemma hoare_vcg_disj_lift: - 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\" - apply (simp add: valid_def) - apply safe - apply (erule(1) post_by_hoare [OF x]) - apply (erule notE) - apply (erule(1) post_by_hoare [OF y]) - done +lemma state_assert_wp: + "\\s. f s \ P () s\ state_assert f \P\" + unfolding state_assert_def + by (wp seq_ext get_wp assert_wp) -lemma hoare_vcg_const_Ball_lift: - "\ \x. x \ S \ \P x\ f \Q x\ \ \ \\s. \x\S. P x s\ f \\rv s. \x\S. Q x rv s\" - by (fastforce simp: valid_def) - -lemma hoare_vcg_const_Ball_lift_R: - "\ \x. x \ S \ \P x\ f \Q x\,- \ \ - \\s. \x \ S. P x s\ f \\rv s. \x \ S. Q x rv s\,-" - apply (simp add: validE_R_def validE_def) - apply (rule hoare_strengthen_post) - apply (erule hoare_vcg_const_Ball_lift) - apply (simp split: sum.splits) - done - -lemma hoare_vcg_all_lift: - "\ \x. \P x\ f \Q x\ \ \ \\s. \x. P x s\ f \\rv s. \x. Q x rv s\" - by (fastforce simp: valid_def) - -lemma hoare_vcg_all_lift_R: - "(\x. \P x\ f \Q x\, -) \ \\s. \x. P x s\ f \\rv s. \x. Q x rv s\, -" - by (rule hoare_vcg_const_Ball_lift_R[where S=UNIV, simplified]) - -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_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) - -lemma hoare_weak_lift_imp: - "\P'\ f \Q\ \ \\s. P \ P' s\ f \\rv s. P \ Q rv s\" - by (auto simp add: valid_def split_def) - -lemma hoare_vcg_ex_lift: - "\ \x. \P x\ f \Q x\ \ \ \\s. \x. P x s\ f \\rv s. \x. Q x rv s\" - by (clarsimp simp: valid_def, blast) - -lemma hoare_vcg_ex_lift_R1: - "(\x. \P x\ f \Q\, -) \ \\s. \x. P x s\ f \Q\, -" - by (fastforce simp: valid_def validE_R_def validE_def split: sum.splits) - -(* for instantiations *) -lemma hoare_triv: "\P\f\Q\ \ \P\f\Q\" . -lemma hoare_trivE: "\P\ f \Q\,\E\ \ \P\ f \Q\,\E\" . -lemma hoare_trivE_R: "\P\ f \Q\,- \ \P\ f \Q\,-" . -lemma hoare_trivR_R: "\P\ f -,\E\ \ \P\ f -,\E\" . - -lemma hoare_weaken_preE_E: - "\ \P'\ f -,\Q\; \s. P s \ P' s \ \ \P\ f -,\Q\" - by (fastforce simp add: validE_E_def validE_def valid_def) +lemma when_wp[wp_split]: + "\ P \ \Q\ f \R\ \ \ \if P then Q else R ()\ when P f \R\" + by (clarsimp simp: when_def valid_def return_def mres_def) -lemma hoare_vcg_E_conj: - "\ \P\ f -,\E\; \P'\ f \Q'\,\E'\ \ - \ \\s. P s \ P' s\ f \Q'\, \\rv s. E rv s \ E' rv s\" - apply (unfold validE_def validE_E_def) - apply (rule hoare_post_imp [OF _ hoare_vcg_conj_lift], simp_all) - apply (case_tac r, simp_all) - done +lemma unless_wp[wp_split]: + "(\P \ \Q\ f \R\) \ \if P then R () else Q\ unless P f \R\" + unfolding unless_def by wp auto -lemma hoare_vcg_E_elim: - "\ \P\ f -,\E\; \P'\ f \Q\,- \ - \ \\s. P s \ P' s\ f \Q\,\E\" - by (rule hoare_post_impErr [OF hoare_vcg_E_conj], - (simp add: validE_R_def)+) +lemma whenE_wp: + "(P \ \Q\ f \R\, \E\) \ \if P then Q else R ()\ whenE P f \R\, \E\" + unfolding whenE_def by clarsimp (wp returnOk_wp) -lemma hoare_vcg_R_conj: - "\ \P\ f \Q\,-; \P'\ f \Q'\,- \ - \ \\s. P s \ P' s\ f \\rv s. Q rv s \ Q' rv s\,-" - apply (unfold validE_R_def validE_def) - apply (rule hoare_post_imp [OF _ hoare_vcg_conj_lift], simp_all) - apply (case_tac r, simp_all) - done +lemma hoare_K_bind[wp_split]: + "\P\ f \Q\ \ \P\ K_bind f x \Q\" + by simp -lemma valid_validE: - "\P\ f \\rv. Q\ \ \P\ f \\rv. Q\,\\rv. Q\" - apply (simp add: validE_def) - done +lemma hoare_fun_app_wp: + "\P\ f' x \Q'\ \ \P\ f' $ x \Q'\" + "\P\ f x \Q\,\E\ \ \P\ f $ x \Q\,\E\" + "\P\ f x \Q\,- \ \P\ f $ x \Q\,-" + "\P\ f x -,\E\ \ \P\ f $ x -,\E\" + by simp+ -lemma valid_validE2: - "\ \P\ f \\_. Q'\; \s. Q' s \ Q s; \s. Q' s \ E s \ \ \P\ f \\_. Q\,\\_. E\" - unfolding valid_def validE_def - by (clarsimp split: sum.splits) blast +lemma liftE_validE_E: + "\\\ liftE f -, \Q\" + by (clarsimp simp: validE_E_def valid_def) -lemma validE_valid: "\P\ f \\rv. Q\,\\rv. Q\ \ \P\ f \\rv. Q\" - apply (unfold validE_def) - apply (rule hoare_post_imp) - defer - apply assumption - apply (case_tac r, simp_all) - done +lemma returnOk_E: + "\\\ returnOk r -, \Q\" + by (simp add: validE_E_def) (wp returnOk_wp) -lemma valid_validE_R: - "\P\ f \\rv. Q\ \ \P\ f \\rv. Q\,-" - by (simp add: validE_R_def hoare_post_impErr [OF valid_validE]) +lemma case_option_wp: + "\ \x. \P x\ m x \Q\; \P'\ m' \Q\ \ \ + \\s. (x = None \ P' s) \ (x \ None \ P (the x) s)\ case_option m' m x \Q\" + by (cases x; simp) -lemma valid_validE_E: - "\P\ f \\rv. Q\ \ \P\ f -,\\rv. Q\" - by (simp add: validE_E_def hoare_post_impErr [OF valid_validE]) +lemma case_option_wpE: + "\ \x. \P x\ m x \Q\,\E\; \P'\ m' \Q\,\E\ \ \ + \\s. (x = None \ P' s) \ (x \ None \ P (the x) s)\ case_option m' m x \Q\,\E\" + by (cases x; simp) -lemma validE_validE_R: "\P\ f \Q\,\\\\ \ \P\ f \Q\,-" - by (simp add: validE_R_def) +lemmas liftME_E_E_wp[wp_split] = validE_validE_E [OF liftME_wp, simplified, OF validE_E_validE] -lemma validE_R_validE: "\P\ f \Q\,- \ \P\ f \Q\,\\\\" - by (simp add: validE_R_def) +(* FIXME: make wp *) +lemma whenE_throwError_wp: + "\\s. \Q \ P s\ whenE Q (throwError e) \\rv. P\, -" + by (simp add: whenE_def returnOk_def throwError_def return_def validE_R_def validE_def valid_def + mres_def) -lemma hoare_post_imp_R: "\ \P\ f \Q'\,-; \r s. Q' r s \ Q r s \ \ \P\ f \Q\,-" - apply (unfold validE_R_def) - apply (rule hoare_post_impErr, simp+) - done +lemma select_throwError_wp: + "\\s. \x\S. Q x s\ select S >>= throwError -, \Q\" + by (clarsimp simp: bind_def throwError_def return_def select_def validE_E_def + validE_def valid_def mres_def) -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\" - apply (rule hoare_pre_imp) - defer - apply (rule hoare_vcg_conj_lift) - apply assumption+ - apply simp - done -lemma hoare_vcg_precond_impE_R: "\ \P'\ f \Q\,-; \s. P s \ P' s \ \ \P\ f \Q\,-" - by (unfold validE_R_def, rule hoare_vcg_precond_impE, simp+) +subsection \Setting up the @{method wp} method\ -(* lemma valid_is_triple: - "valid P f Q = triple_judgement P f (postcondition Q (\s f. fst (f s)))" +lemma valid_is_triple: + "valid P f Q = triple_judgement P f (postcondition Q (\s f. mres (f s)))" by (simp add: triple_judgement_def valid_def postcondition_def) - *) lemma validE_is_triple: - "validE P f Q E = triple_judgement P f - (postconditions (\s f. (\(r,s') \ {(rv, s'). (Inr rv, s') \ (mres (f s))}. Q r s')) - (\s f. (\(r,s') \ {(rv, s'). (Inl rv, s') \ (mres (f s))}. E r s')))" - apply (simp add: validE_def triple_judgement_def valid_def postcondition_def - postconditions_def split_def split: sum.split) - apply (fastforce elim: image_eqI[rotated]) - done + "validE P f Q E = + triple_judgement P f + (postconditions (postcondition Q (\s f. {(rv, s'). (Inr rv, s') \ mres (f s)})) + (postcondition E (\s f. {(rv, s'). (Inl rv, s') \ mres (f s)})))" + by (fastforce simp: validE_def triple_judgement_def valid_def postcondition_def postconditions_def + split: sum.split) lemma validE_R_is_triple: - "validE_R P f Q = triple_judgement P f - (\s f. (\(r,s') \ {(rv, s'). (Inr rv, s') \ mres (f s)}. Q r s'))" + "validE_R P f Q = + triple_judgement P f (postcondition Q (\s f. {(rv, s'). (Inr rv, s') \ mres (f s)}))" by (simp add: validE_R_def validE_is_triple postconditions_def postcondition_def) lemma validE_E_is_triple: - "validE_E P f E = triple_judgement P f - (\s f. (\(r,s') \ {(rv, s'). (Inl rv, s') \ mres (f s)}. E r s'))" + "validE_E P f E = + triple_judgement P f (postcondition E (\s f. {(rv, s'). (Inl rv, s') \ mres (f s)}))" by (simp add: validE_E_def validE_is_triple postconditions_def postcondition_def) -lemmas hoare_wp_combs = - hoare_post_comb_imp_conj hoare_vcg_precond_imp hoare_vcg_conj_lift +lemmas hoare_wp_combs = hoare_vcg_conj_lift lemmas hoare_wp_combsE = - hoare_vcg_precond_impE - hoare_vcg_precond_impE_R validE_validE_R hoare_vcg_R_conj hoare_vcg_E_elim hoare_vcg_E_conj lemmas hoare_wp_state_combsE = - hoare_vcg_precond_impE[OF valid_validE] - hoare_vcg_precond_impE_R[OF valid_validE_R] valid_validE_R hoare_vcg_R_conj[OF valid_validE_R] hoare_vcg_E_elim[OF valid_validE_E] hoare_vcg_E_conj[OF valid_validE_E] -lemmas hoare_wp_splits [wp_split] = +lemmas hoare_classic_wp_combs = hoare_post_comb_imp_conj hoare_vcg_precond_imp hoare_wp_combs +lemmas hoare_classic_wp_combsE = hoare_vcg_precond_impE hoare_vcg_precond_impE_R hoare_wp_combsE + +lemmas hoare_classic_wp_state_combsE = + hoare_vcg_precond_impE[OF valid_validE] + hoare_vcg_precond_impE_R[OF valid_validE_R] + hoare_wp_state_combsE + +lemmas all_classic_wp_combs = + hoare_classic_wp_state_combsE + hoare_classic_wp_combsE + hoare_classic_wp_combs + +lemmas hoare_wp_splits[wp_split] = hoare_seq_ext hoare_vcg_seqE handleE'_wp handleE_wp validE_validE_R [OF hoare_vcg_seqE [OF validE_R_validE]] validE_validE_R [OF handleE'_wp [OF validE_R_validE]] validE_validE_R [OF handleE_wp [OF validE_R_validE]] - catch_wp hoare_vcg_split_if hoare_vcg_split_ifE - validE_validE_R [OF hoare_vcg_split_ifE [OF validE_R_validE validE_R_validE]] + catch_wp hoare_vcg_if_split hoare_vcg_if_splitE + validE_validE_R [OF hoare_vcg_if_splitE [OF validE_R_validE validE_R_validE]] liftM_wp liftME_wp validE_validE_R [OF liftME_wp [OF validE_R_validE]] validE_valid lemmas [wp_comb] = hoare_wp_state_combsE hoare_wp_combsE hoare_wp_combs +(* rules towards the bottom will be matched first *) lemmas [wp] = hoare_vcg_prop wp_post_taut - return_wp + hoare_fun_app_wp + returnOk_E + liftE_validE_E put_wp get_wp gets_wp modify_wp + return_wp returnOk_wp throwError_wp fail_wp failE_wp + assert_wp + state_assert_wp liftE_wp + alternative_wp + alternativeE_R_wp + alternativeE_E_wp + alternativeE_wp + select_wp + state_select_wp + condition_wp + conditionE_wp lemmas [wp_trip] = valid_is_triple validE_is_triple validE_E_is_triple validE_R_is_triple +lemmas validE_E_combs[wp_comb] = + hoare_vcg_E_conj[where Q'="\\", folded validE_E_def] + valid_validE_E + hoare_vcg_E_conj[where Q'="\\", folded validE_E_def, OF valid_validE_E] + text \Simplifications on conjunction\ -lemma hoare_post_eq: "\ Q = Q'; \P\ f \Q'\ \ \ \P\ f \Q\" +lemma hoare_post_eq: + "\ Q = Q'; \P\ f \Q'\ \ \ \P\ f \Q\" by simp -lemma hoare_post_eqE1: "\ Q = Q'; \P\ f \Q'\,\E\ \ \ \P\ f \Q\,\E\" + +lemma hoare_post_eqE1: + "\ Q = Q'; \P\ f \Q'\,\E\ \ \ \P\ f \Q\,\E\" by simp -lemma hoare_post_eqE2: "\ E = E'; \P\ f \Q\,\E'\ \ \ \P\ f \Q\,\E\" + +lemma hoare_post_eqE2: + "\ E = E'; \P\ f \Q\,\E'\ \ \ \P\ f \Q\,\E\" by simp -lemma hoare_post_eqE_R: "\ Q = Q'; \P\ f \Q'\,- \ \ \P\ f \Q\,-" + +lemma hoare_post_eqE_R: + "\ Q = Q'; \P\ f \Q'\,- \ \ \P\ f \Q\,-" by simp -lemma pred_conj_apply_elim: "(\r. Q r and Q' r) = (\r s. Q r s \ Q' r s)" +lemma pred_conj_apply_elim: + "(\rv. Q rv and Q' rv) = (\rv s. Q rv s \ Q' rv s)" by (simp add: pred_conj_def) -lemma pred_conj_conj_elim: "(\r s. (Q r and Q' r) s \ Q'' r s) = (\r s. Q r s \ Q' r s \ Q'' r s)" + +lemma pred_conj_conj_elim: + "(\rv s. (Q rv and Q' rv) s \ Q'' rv s) = (\rv s. Q rv s \ Q' rv s \ Q'' rv s)" by simp -lemma conj_assoc_apply: "(\r s. (Q r s \ Q' r s) \ Q'' r s) = (\r s. Q r s \ Q' r s \ Q'' r s)" + +lemma conj_assoc_apply: + "(\rv s. (Q rv s \ Q' rv s) \ Q'' rv s) = (\rv s. Q rv s \ Q' rv s \ Q'' rv s)" by simp -lemma all_elim: "(\rv s. \x. P rv s) = P" + +lemma all_elim: + "(\rv s. \x. P rv s) = P" by simp -lemma all_conj_elim: "(\rv s. (\x. P rv s) \ Q rv s) = (\rv s. P rv s \ Q rv s)" + +lemma all_conj_elim: + "(\rv s. (\x. P rv s) \ Q rv s) = (\rv s. P rv s \ Q rv s)" by simp -lemmas vcg_rhs_simps = pred_conj_apply_elim pred_conj_conj_elim - conj_assoc_apply all_elim all_conj_elim +lemmas vcg_rhs_simps = + pred_conj_apply_elim pred_conj_conj_elim conj_assoc_apply all_elim all_conj_elim + +lemma if_apply_reduct: + "\P\ If P' (f x) (g x) \Q\ \ \P\ If P' f g x \Q\" + by (cases P'; simp) -lemma if_apply_reduct: "\P\ If P' (f x) (g x) \Q\ \ \P\ If P' f g x \Q\" - by (cases P', simp_all) -lemma if_apply_reductE: "\P\ If P' (f x) (g x) \Q\,\E\ \ \P\ If P' f g x \Q\,\E\" - by (cases P', simp_all) -lemma if_apply_reductE_R: "\P\ If P' (f x) (g x) \Q\,- \ \P\ If P' f g x \Q\,-" - by (cases P', simp_all) +lemma if_apply_reductE: + "\P\ If P' (f x) (g x) \Q\,\E\ \ \P\ If P' f g x \Q\,\E\" + by (cases P'; simp) + +lemma if_apply_reductE_R: + "\P\ If P' (f x) (g x) \Q\,- \ \P\ If P' f g x \Q\,-" + by (cases P'; simp) lemmas hoare_wp_simps [wp_split] = vcg_rhs_simps [THEN hoare_post_eq] vcg_rhs_simps [THEN hoare_post_eqE1] vcg_rhs_simps [THEN hoare_post_eqE2] vcg_rhs_simps [THEN hoare_post_eqE_R] if_apply_reduct if_apply_reductE if_apply_reductE_R TrueI -schematic_goal if_apply_test: "\?Q\ (if A then returnOk else K fail) x \P\,\E\" +schematic_goal if_apply_test: + "\?Q\ (if A then returnOk else K fail) x \P\,\E\" by wpsimp lemma hoare_elim_pred_conj: - "\P\ f \\r s. Q r s \ Q' r s\ \ \P\ f \\r. Q r and Q' r\" + "\P\ f \\rv s. Q rv s \ Q' rv s\ \ \P\ f \\rv. Q rv and Q' rv\" by (unfold pred_conj_def) lemma hoare_elim_pred_conjE1: - "\P\ f \\r s. Q r s \ Q' r s\,\E\ \ \P\ f \\r. Q r and Q' r\,\E\" + "\P\ f \\rv s. Q rv s \ Q' rv s\,\E\ \ \P\ f \\rv. Q rv and Q' rv\,\E\" by (unfold pred_conj_def) lemma hoare_elim_pred_conjE2: - "\P\ f \Q\, \\x s. E x s \ E' x s\ \ \P\ f \Q\,\\x. E x and E' x\" + "\P\ f \Q\, \\rv s. E rv s \ E' rv s\ \ \P\ f \Q\,\\rv. E rv and E' rv\" by (unfold pred_conj_def) lemma hoare_elim_pred_conjE_R: - "\P\ f \\r s. Q r s \ Q' r s\,- \ \P\ f \\r. Q r and Q' r\,-" + "\P\ f \\rv s. Q rv s \ Q' rv s\,- \ \P\ f \\rv. Q rv and Q' rv\,-" by (unfold pred_conj_def) lemmas hoare_wp_pred_conj_elims = hoare_elim_pred_conj hoare_elim_pred_conjE1 hoare_elim_pred_conjE2 hoare_elim_pred_conjE_R -lemmas hoare_weaken_preE = hoare_vcg_precond_impE - -lemmas hoare_pre [wp_pre] = - hoare_weaken_pre - hoare_weaken_preE - hoare_vcg_precond_impE_R - hoare_weaken_preE_E - -declare no_fail_pre [wp_pre] - -bundle no_pre = hoare_pre [wp_pre del] no_fail_pre [wp_pre del] text \Miscellaneous lemmas on hoare triples\ lemma hoare_vcg_mp: - assumes a: "\P\ f \Q\" - assumes b: "\P\ f \\r s. Q r s \ Q' r s\" - shows "\P\ f \Q'\" - using assms + "\ \P\ f \Q\; \P\ f \\r s. Q r s \ Q' r s\ \ \ \P\ f \Q'\" by (auto simp: valid_def split_def) (* note about this precond stuff: rules get a chance to bind directly before any of their combined forms. As a result, these precondition implication rules are only used when needed. *) - lemma hoare_add_post: - assumes r: "\P'\ f \Q'\" - assumes impP: "\s. P s \ P' s" - assumes impQ: "\P\ f \\rv s. Q' rv s \ Q rv s\" - shows "\P\ f \Q\" - apply (rule hoare_chain) - apply (rule hoare_vcg_conj_lift) - apply (rule r) - apply (rule impQ) - apply simp - apply (erule impP) - apply simp - done - -lemma whenE_wp: - "(P \ \Q\ f \R\, \E\) \ \if P then Q else R ()\ whenE P f \R\, \E\" - unfolding whenE_def by clarsimp wp + "\ \P'\ f \Q'\; \s. P s \ P' s; \P\ f \\rv s. Q' rv s \ Q rv s\ \ \ \P\ f \Q\" + unfolding valid_def + by fastforce lemma hoare_gen_asmE: "(P \ \P'\ f \Q\,-) \ \P' and K P\ f \Q\, -" by (simp add: validE_R_def validE_def valid_def) blast lemma hoare_list_case: - assumes P1: "\P1\ f f1 \Q\" - assumes P2: "\y ys. xs = y#ys \ \P2 y ys\ f (f2 y ys) \Q\" - shows "\case xs of [] \ P1 | y#ys \ P2 y ys\ - f (case xs of [] \ f1 | y#ys \ f2 y ys) - \Q\" - apply (cases xs; simp) - apply (rule P1) - apply (rule P2) - apply simp - done - -lemma unless_wp: - "(\P \ \Q\ f \R\) \ \if P then R () else Q\ unless P f \R\" - unfolding unless_def by wp auto + "\ \P1\ f f1 \Q\; \y ys. xs = y#ys \ \P2 y ys\ f (f2 y ys) \Q\ \ \ + \case xs of [] \ P1 | y#ys \ P2 y ys\ f (case xs of [] \ f1 | y#ys \ f2 y ys) \Q\" + by (cases xs; simp) lemma hoare_use_eq: - assumes x: "\P. \\s. P (f s)\ m \\rv s. P (f s)\" - assumes y: "\f. \\s. P f s\ m \\rv s. Q f s\" - shows "\\s. P (f s) s\ m \\rv s. Q (f s :: 'c :: type) s \" - apply (rule_tac Q="\rv s. \f'. f' = f s \ Q f' s" in hoare_post_imp) - apply simp - apply (wpsimp wp: hoare_vcg_ex_lift x y) + assumes "\P. \\s. P (f s)\ m \\_ s. P (f s)\" + assumes "\f. \\s. P f s\ m \\_ s. Q f s\" + shows "\\s. P (f s) s\ m \\_ s. Q (f s) s \" + apply (rule hoare_post_imp[where Q="\_ s. \y. y = f s \ Q y s"], simp) + apply (wpsimp wp: hoare_vcg_ex_lift assms) done -lemma hoare_return_sp: - "\P\ return x \\r. P and K (r = x)\" - by (simp add: valid_def return_def mres_def) - -lemma hoare_fail_any [simp]: - "\P\ fail \Q\" by wp +lemma hoare_fail_any[simp]: + "\P\ fail \Q\" + by wp -lemma hoare_failE [simp]: "\P\ fail \Q\,\E\" by wp +lemma hoare_failE[simp]: + "\P\ fail \Q\, \E\" + by wp -lemma hoare_FalseE [simp]: - "\\s. False\ f \Q\,\E\" +lemma hoare_FalseE[simp]: + "\\\ f \Q\, \E\" by (simp add: valid_def validE_def) -lemma hoare_K_bind [wp]: - "\P\ f \Q\ \ \P\ K_bind f x \Q\" - by simp - -text \Setting up the precondition case splitter.\ - -lemma wpc_helper_valid: - "\Q\ g \S\ \ wpc_helper (P, P', P'') (Q, Q', Q'') \P\ g \S\" - by (clarsimp simp: wpc_helper_def elim!: hoare_pre) - -lemma wpc_helper_validE: - "\Q\ f \R\,\E\ \ wpc_helper (P, P', P'') (Q, Q', Q'') \P\ f \R\,\E\" - by (clarsimp simp: wpc_helper_def elim!: hoare_pre) - -lemma wpc_helper_validE_R: - "\Q\ f \R\,- \ wpc_helper (P, P', P'') (Q, Q', Q'') \P\ f \R\,-" - by (clarsimp simp: wpc_helper_def elim!: hoare_pre) - -lemma wpc_helper_validR_R: - "\Q\ f -,\E\ \ wpc_helper (P, P', P'') (Q, Q', Q'') \P\ f -,\E\" - by (clarsimp simp: wpc_helper_def elim!: hoare_pre) - -lemma wpc_helper_no_fail_final: - "no_fail Q f \ wpc_helper (P, P', P'') (Q, Q', Q'') (no_fail P f)" - by (clarsimp simp: wpc_helper_def elim!: no_fail_pre) - -lemma wpc_helper_validNF: - "\Q\ g \S\! \ wpc_helper (P, P', P'') (Q, Q', Q'') \P\ g \S\!" - apply (clarsimp simp: wpc_helper_def) - by (metis hoare_wp_combs(2) no_fail_pre validNF_def) - -(* FIXME: this needs adjustment, case_prod Q is unlikely to unify *) -lemma wpc_helper_validI: - "(\Q\,\R\ g \G\,\S\) \ wpc_helper (P, P', P'') (case_prod Q, Q', Q'') (\curry P\,\R\ g \G\,\S\)" - by (clarsimp simp: wpc_helper_def elim!: validI_weaken_pre) - -wpc_setup "\m. \P\ m \Q\" wpc_helper_valid -wpc_setup "\m. \P\ m \Q\,\E\" wpc_helper_validE -wpc_setup "\m. \P\ m \Q\,-" wpc_helper_validE_R -wpc_setup "\m. \P\ m -,\E\" wpc_helper_validR_R -wpc_setup "\m. no_fail P m" wpc_helper_no_fail_final -wpc_setup "\m. \P\ m \Q\!" wpc_helper_validNF -wpc_setup "\m. \P\,\R\ m \G\,\S\" wpc_helper_validI - -lemma in_liftM: - "((r, s') \ mres (liftM t f s)) = (\r'. (r', s') \ mres (f s) \ r = t r')" - by (simp add: liftM_def in_return in_bind) - -lemma hoare_fun_app_wp[wp]: - "\P\ f' x \Q'\ \ \P\ f' $ x \Q'\" - "\P\ f x \Q\,\E\ \ \P\ f $ x \Q\,\E\" - "\P\ f x \Q\,- \ \P\ f $ x \Q\,-" - "\P\ f x -,\E\ \ \P\ f $ x -,\E\" - by simp+ - lemma hoare_validE_pred_conj: - "\ \P\f\Q\,\E\; \P\f\R\,\E\ \ \ \P\f\Q and R\,\E\" - unfolding valid_def validE_def by (simp add: split_def split: sum.splits) + "\ \P\ f \Q\, \E\; \P\ f \R\, \E\ \ \ \P\ f \Q and R\, \E\" + unfolding valid_def validE_def + by (simp add: split_def split: sum.splits) lemma hoare_validE_conj: - "\ \P\f\Q\,\E\; \P\f\R\,\E\ \ \ \P\ f \\r s. Q r s \ R r s\,\E\" - unfolding valid_def validE_def by (simp add: split_def split: sum.splits) - -lemma hoare_valid_validE: - "\P\f\\r. Q\ \ \P\f\\r. Q\,\\r. Q\" - unfolding valid_def validE_def by (simp add: split_def split: sum.splits) + "\ \P\ f \Q\, \E\; \P\ f \R\, \E\ \ \ \P\ f \\rv s. Q rv s \ R rv s\, \E\" + unfolding valid_def validE_def + by (simp add: split_def split: sum.splits) -lemma liftE_validE_E [wp]: - "\\\ liftE f -, \Q\" - by (clarsimp simp: validE_E_def valid_def) +lemmas hoare_valid_validE = valid_validE (* FIXME lib: eliminate one *) -lemma validE_validE_E [wp_comb]: - "\P\ f \\\\, \E\ \ \P\ f -, \E\" - by (simp add: validE_E_def) +declare validE_validE_E[wp_comb] -lemma validE_E_validE: - "\P\ f -, \E\ \ \P\ f \\\\, \E\" - by (simp add: validE_E_def) - -(* - * if_validE_E: - * - * \?P1 \ \?Q1\ ?f1 -, \?E\; \ ?P1 \ \?R1\ ?g1 -, \?E\\ \ \\s. (?P1 \ ?Q1 s) \ (\ ?P1 \ ?R1 s)\ if ?P1 then ?f1 else ?g1 -, \?E\ - *) -lemmas if_validE_E [wp_split] = - validE_validE_E [OF hoare_vcg_split_ifE [OF validE_E_validE validE_E_validE]] - -lemma returnOk_E [wp]: - "\\\ returnOk r -, \Q\" - by (simp add: validE_E_def) wp +lemmas if_validE_E[wp_split] = + validE_validE_E[OF hoare_vcg_if_splitE[OF validE_E_validE validE_E_validE]] lemma hoare_drop_imp: - "\P\ f \Q\ \ \P\ f \\r s. R r s \ Q r s\" + "\P\ f \Q\ \ \P\ f \\rv s. R rv s \ Q rv s\" by (auto simp: valid_def) lemma hoare_drop_impE: - "\\P\ f \\r. Q\, \E\\ \ \P\ f \\r s. R r s \ Q s\, \E\" + "\\P\ f \\r. Q\, \E\\ \ \P\ f \\rv s. R rv s \ Q s\, \E\" by (simp add: validE_weaken) lemma hoare_drop_impE_R: - "\P\ f \Q\,- \ \P\ f \\r s. R r s \ Q r s\, -" + "\P\ f \Q\,- \ \P\ f \\rv s. R rv s \ Q rv s\, -" by (auto simp: validE_R_def validE_def valid_def split_def split: sum.splits) lemma hoare_drop_impE_E: - "\P\ f -,\Q\ \ \P\ f -,\\r s. R r s \ Q r s\" + "\P\ f -,\Q\ \ \P\ f -, \\rv s. R rv s \ Q rv s\" by (auto simp: validE_E_def validE_def valid_def split_def split: sum.splits) lemmas hoare_drop_imps = hoare_drop_imp hoare_drop_impE_R hoare_drop_impE_E -lemma mres_union: - "mres (a \ b) = mres a \ mres b" - by (simp add: mres_def image_Un) - -lemma mres_Failed_empty: - "mres ((\xs. (xs, Failed)) ` X ) = {}" - "mres ((\xs. (xs, Incomplete)) ` X ) = {}" - by (auto simp add: mres_def image_def) - -lemma det_set_option_eq: - "(\a\m. set_option (snd a)) = {(r, s')} \ - (ts, Some (rr, ss)) \ m \ rr = r \ ss = s'" - by (metis UN_I option.set_intros prod.inject singleton_iff snd_conv) - -lemma det_set_option_eq': - "(\a\m. set_option (snd a)) = {(r, s')} \ - Some (r, s') \ snd ` m" - using image_iff by fastforce - -lemma bind_det_exec: - "mres (a s) = {(r,s')} \ mres ((a >>= b) s) = mres (b r s')" - by (simp add: in_bind set_eq_iff) - -lemma in_bind_det_exec: - "mres (a s) = {(r,s')} \ (s'' \ mres ((a >>= b) s)) = (s'' \ mres (b r s'))" - by (cases s'', simp add: in_bind) - -lemma exec_put: - "(put s' >>= m) s = m () s'" - by (auto simp add: bind_def put_def mres_def split_def) - -lemma bind_execI: - "\ (r'',s'') \ mres (f s); \x \ mres (g r'' s''). P x \ \ - \x \ mres ((f >>= g) s). P x" - by (fastforce simp add: Bex_def in_bind) - -lemma True_E_E [wp]: "\\\ f -,\\\\" - by (auto simp: validE_E_def validE_def valid_def split: sum.splits) - -(* - * \\x. \?B1 x\ ?g1 x -, \?E\; \?P\ ?f1 \?B1\, \?E\\ \ \?P\ ?f1 >>=E ?g1 -, \?E\ - *) -lemmas [wp_split] = - validE_validE_E [OF hoare_vcg_seqE [OF validE_E_validE]] - -lemma case_option_wp: - assumes x: "\x. \P x\ m x \Q\" - assumes y: "\P'\ m' \Q\" - shows "\\s. (x = None \ P' s) \ (x \ None \ P (the x) s)\ - case_option m' m x \Q\" - apply (cases x; simp) - apply (rule y) - apply (rule x) - done -lemma case_option_wpE: - assumes x: "\x. \P x\ m x \Q\,\E\" - assumes y: "\P'\ m' \Q\,\E\" - shows "\\s. (x = None \ P' s) \ (x \ None \ P (the x) s)\ - case_option m' m x \Q\,\E\" - apply (cases x; simp) - apply (rule y) - apply (rule x) - done - -lemma in_bindE: - "(rv, s') \ mres ((f >>=E (\rv'. g rv')) s) = - ((\ex. rv = Inl ex \ (Inl ex, s') \ mres (f s)) \ - (\rv' s''. (rv, s') \ mres (g rv' s'') \ (Inr rv', s'') \ mres (f s)))" - apply (clarsimp simp: bindE_def in_bind lift_def in_throwError) - apply (safe del: disjCI; strengthen subst[where P="\x. x \ mres (f s)", mk_strg I _ E]; - auto simp: in_throwError split: sum.splits) - done - -(* - * \?P\ ?m1 -, \?E\ \ \?P\ liftME ?f1 ?m1 -, \?E\ - *) -lemmas [wp_split] = validE_validE_E [OF liftME_wp, simplified, OF validE_E_validE] +lemmas bindE_E_wp[wp_split] = validE_validE_E[OF hoare_vcg_seqE [OF validE_E_validE]] -lemma assert_A_True[simp]: "assert True = return ()" - by (simp add: assert_def) - -lemma assert_wp [wp]: "\\s. P \ Q () s\ assert P \Q\" - by (cases P, (simp add: assert_def | wp)+) - -lemma list_cases_wp: - assumes a: "\P_A\ a \Q\" - assumes b: "\x xs. ts = x#xs \ \P_B x xs\ b x xs \Q\" - shows "\case_list P_A P_B ts\ case ts of [] \ a | x # xs \ b x xs \Q\" - by (cases ts, auto simp: a b) - -(* FIXME: make wp *) -lemma whenE_throwError_wp: - "\\s. \Q \ P s\ whenE Q (throwError e) \\rv. P\, -" - unfolding whenE_def by wp blast - -lemma select_throwError_wp: - "\\s. \x\S. Q x s\ select S >>= throwError -, \Q\" - by (clarsimp simp add: bind_def throwError_def return_def select_def validE_E_def - validE_def valid_def mres_def) - - -section "validNF Rules" - -subsection "Basic validNF theorems" - -lemma validNF [intro?]: - "\ \ P \ f \ Q \; no_fail P f \ \ \ P \ f \ Q \!" - by (clarsimp simp: validNF_def) - -lemma validNF_valid: "\ \ P \ f \ Q \! \ \ \ P \ f \ Q \" - by (clarsimp simp: validNF_def) - -lemma validNF_no_fail: "\ \ P \ f \ Q \! \ \ no_fail P f" - by (clarsimp simp: validNF_def) - -lemma snd_validNF: - "\ \ P \ f \ Q \!; P s \ \ Failed \ snd ` (f s)" - by (clarsimp simp: validNF_def no_fail_def) - -lemma use_validNF: - "\ (r', s') \ mres (f s); \ P \ f \ Q \!; P s \ \ Q r' s'" - by (fastforce simp: validNF_def valid_def) - -subsection "validNF weakest pre-condition rules" - -lemma validNF_return [wp]: - "\ P x \ return x \ P \!" - by (wp validNF)+ - -lemma validNF_get [wp]: - "\ \s. P s s \ get \ P \!" - by (wp validNF)+ - -lemma validNF_put [wp]: - "\ \s. P () x \ put x \ P \!" - by (wp validNF)+ - -lemma validNF_K_bind [wp]: - "\ P \ x \ Q \! \ \ P \ K_bind x f \ Q \!" - by simp - -lemma validNF_fail [wp]: - "\ \s. False \ fail \ Q \!" - by (clarsimp simp: validNF_def fail_def no_fail_def) - -lemma validNF_prop [wp_unsafe]: - "\ no_fail (\s. P) f \ \ \ \s. P \ f \ \rv s. P \!" - by (wp validNF)+ - -lemma validNF_post_conj [intro!]: - "\ \ P \ a \ Q \!; \ P \ a \ R \! \ \ \ P \ a \ Q and R \!" - by (clarsimp simp: validNF_def) - -lemma no_fail_or: - "\no_fail P a; no_fail Q a\ \ no_fail (P or Q) a" - by (clarsimp simp: no_fail_def) - -lemma validNF_pre_disj [intro!]: - "\ \ P \ a \ R \!; \ Q \ a \ R \! \ \ \ P or Q \ a \ R \!" - by (rule validNF) (auto dest: validNF_valid validNF_no_fail intro: no_fail_or) - -(* - * Set up combination rules for WP, which also requires - * a "wp_trip" rule for validNF. - *) - -definition "validNF_property Q s b \ Failed \ snd ` (b s) \ (\(r', s') \ mres (b s). Q r' s')" - -lemma validNF_is_triple [wp_trip]: - "validNF P f Q = triple_judgement P f (validNF_property Q)" - apply (clarsimp simp: validNF_def triple_judgement_def validNF_property_def) - apply (auto simp: no_fail_def valid_def) - done - -lemma validNF_weaken_pre [wp_comb]: - "\\Q\ a \R\!; \s. P s \ Q s\ \ \P\ a \R\!" - by (metis hoare_pre_imp no_fail_pre validNF_def) - -lemma validNF_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 (fastforce simp: validNF_def valid_def) - -lemma validNF_post_comb_conj_L: - "\ \P'\ f \Q\!; \P\ f \Q'\ \ \ \\s. P s \ P' s \ f \\rv s. Q rv s \ Q' rv s\!" - apply (clarsimp simp: validNF_def valid_def no_fail_def) - apply force - done - -lemma validNF_post_comb_conj_R: - "\ \P'\ f \Q\; \P\ f \Q'\! \ \ \\s. P s \ P' s \ f \\rv s. Q rv s \ Q' rv s\!" - apply (clarsimp simp: validNF_def valid_def no_fail_def) - apply force - done - -lemma validNF_post_comb_conj: - "\ \P'\ f \Q\!; \P\ f \Q'\! \ \ \\s. P s \ P' s \ f \\rv s. Q rv s \ Q' rv s\!" - apply (clarsimp simp: validNF_def valid_def no_fail_def) - apply force - done - -lemma validNF_split_if [wp_split]: - "\P \ \Q\ f \S\!; \ P \ \R\ g \S\!\ \ \\s. (P \ Q s) \ (\ P \ R s)\ if P then f else g \S\!" - by simp - -lemma validNF_vcg_conj_lift: - "\ \P\ f \Q\!; \P'\ f \Q'\! \ \ - \\s. P s \ P' s\ f \\rv s. Q rv s \ Q' rv s\!" - apply (subst pred_conj_def[symmetric], subst pred_conj_def[symmetric], rule validNF_post_conj) - apply (erule validNF_weaken_pre, fastforce) - apply (erule validNF_weaken_pre, fastforce) - done - -lemma validNF_vcg_disj_lift: - "\ \P\ f \Q\!; \P'\ f \Q'\! \ \ - \\s. P s \ P' s\ f \\rv s. Q rv s \ Q' rv s\!" - apply (clarsimp simp: validNF_def) - apply safe - apply (auto intro!: hoare_vcg_disj_lift)[1] - apply (clarsimp simp: no_fail_def) - done - -lemma validNF_vcg_all_lift [wp]: - "\ \x. \P x\ f \Q x\! \ \ \\s. \x. P x s\ f \\rv s. \x. Q x rv s\!" - apply atomize - apply (rule validNF) - apply (clarsimp simp: validNF_def) - apply (rule hoare_vcg_all_lift) - apply force - apply (clarsimp simp: no_fail_def validNF_def) - done - -lemma no_fail_bind[wp_split]: - "\ no_fail P f; \x. no_fail (R x) (g x); \Q\ f \R\ \ - \ no_fail (P and Q) (do x \ f; g x od)" - apply (simp add: no_fail_def bind_def2 image_Un image_image - in_image_constant) - apply (intro allI conjI impI) - apply (fastforce simp: image_def) - apply clarsimp - apply (drule(1) post_by_hoare, erule in_mres) - apply (fastforce simp: image_def) - done - -lemma validNF_bind [wp_split]: - "\ \x. \B x\ g x \C\!; \A\ f \B\! \ \ - \A\ do x \ f; g x od \C\!" - apply (rule validNF) - apply (metis validNF_valid hoare_seq_ext) - apply (frule no_fail_bind[OF validNF_no_fail, where g=g]) - apply (rule validNF_no_fail, assumption) - apply (erule validNF_valid) - apply (simp add: no_fail_def) - done - -lemmas validNF_seq_ext = validNF_bind - -subsection "validNF compound rules" -lemma validNF_state_assert [wp]: - "\ \s. P () s \ G s \ state_assert G \ P \!" - apply (rule validNF) - apply wpsimp - apply (clarsimp simp: no_fail_def state_assert_def - bind_def2 assert_def return_def get_def) - done - -lemma validNF_modify [wp]: - "\ \s. P () (f s) \ modify f \ P \!" - apply (clarsimp simp: modify_def) - apply wp - done - -lemma validNF_gets [wp]: - "\\s. P (f s) s\ gets f \P\!" - apply (clarsimp simp: gets_def) - apply wp - done - -lemma validNF_condition [wp]: - "\ \ Q \ A \P\!; \ R \ B \P\!\ \ \\s. if C s then Q s else R s\ condition C A B \P\!" - apply rule - apply (drule validNF_valid)+ - apply (erule (1) condition_wp) - apply (drule validNF_no_fail)+ - apply (clarsimp simp: no_fail_def condition_def) - done - -lemma validNF_alt_def: - "validNF P m Q = (\s. P s \ ((\(r', s') \ mres (m s). Q r' s') \ Failed \ snd ` (m s)))" - by (auto simp: validNF_def valid_def no_fail_def mres_def image_def) - -lemma validNF_assert [wp]: - "\ (\s. P) and (R ()) \ assert P \ R \!" - apply (rule validNF) - apply (clarsimp simp: valid_def in_return) - apply (clarsimp simp: no_fail_def return_def) - done - -lemma validNF_false_pre: - "\ \_. False \ P \ Q \!" - by (clarsimp simp: validNF_def no_fail_def) - -lemma validNF_chain: - "\\P'\ a \R'\!; \s. P s \ P' s; \r s. R' r s \ R r s\ \ \P\ a \R\!" - by (fastforce simp: validNF_def valid_def no_fail_def Ball_def) - -lemma validNF_case_prod [wp]: - "\ \x y. validNF (P x y) (B x y) Q \ \ validNF (case_prod P v) (case_prod (\x y. B x y) v) Q" - by (metis prod.exhaust split_conv) - -lemma validE_NF_case_prod [wp]: - "\ \a b. \P a b\ f a b \Q\, \E\! \ \ - \case x of (a, b) \ P a b\ case x of (a, b) \ f a b \Q\, \E\!" - apply (clarsimp simp: validE_NF_alt_def) - apply (erule validNF_case_prod) - done - -lemma no_fail_is_validNF_True: "no_fail P s = (\ P \ s \ \_ _. True \!)" - by (clarsimp simp: no_fail_def validNF_def valid_def) - -subsection "validNF reasoning in the exception monad" - -lemma validE_NF [intro?]: - "\ \ P \ f \ Q \,\ E \; no_fail P f \ \ \ P \ f \ Q \,\ E \!" - apply (clarsimp simp: validE_NF_def) - done - -lemma validE_NF_valid: - "\ \ P \ f \ Q \,\ E \! \ \ \ P \ f \ Q \,\ E \" - apply (clarsimp simp: validE_NF_def) - done - -lemma validE_NF_no_fail: - "\ \ P \ f \ Q \,\ E \! \ \ no_fail P f" - apply (clarsimp simp: validE_NF_def) - done - -lemma validE_NF_weaken_pre [wp_comb]: - "\\Q\ a \R\,\E\!; \s. P s \ Q s\ \ \P\ a \R\,\E\!" - apply (clarsimp simp: validE_NF_alt_def) - apply (erule validNF_weaken_pre) - apply simp - done - -lemma validE_NF_post_comb_conj_L: - "\ \P\ f \Q\, \ E \!; \P'\ f \Q'\, \ \_ _. True \ \ \ \\s. P s \ P' s \ f \\rv s. Q rv s \ Q' rv s\, \ E \!" - apply (clarsimp simp: validE_NF_alt_def validE_def validNF_def - valid_def no_fail_def split: sum.splits) - apply force - done - -lemma validE_NF_post_comb_conj_R: - "\ \P\ f \Q\, \ \_ _. True \; \P'\ f \Q'\, \ E \! \ \ \\s. P s \ P' s \ f \\rv s. Q rv s \ Q' rv s\, \ E \!" - apply (clarsimp simp: validE_NF_alt_def validE_def validNF_def - valid_def no_fail_def split: sum.splits) - apply force - done - -lemma validE_NF_post_comb_conj: - "\ \P\ f \Q\, \ E \!; \P'\ f \Q'\, \ E \! \ \ \\s. P s \ P' s \ f \\rv s. Q rv s \ Q' rv s\, \ E \!" - apply (clarsimp simp: validE_NF_alt_def validE_def validNF_def - valid_def no_fail_def split: sum.splits) - apply force - done - -lemma validE_NF_chain: - "\\P'\ a \R'\,\E'\!; - \s. P s \ P' s; - \r' s'. R' r' s' \ R r' s'; - \r'' s''. E' r'' s'' \ E r'' s''\ \ - \\s. P s \ a \\r' s'. R r' s'\,\\r'' s''. E r'' s''\!" - by (fastforce simp: validE_NF_def validE_def2 no_fail_def Ball_def split: sum.splits) - -lemma validE_NF_bind_wp [wp]: - "\\x. \B x\ g x \C\, \E\!; \A\ f \B\, \E\!\ \ \A\ f >>=E (\x. g x) \C\, \E\!" - apply (unfold validE_NF_alt_def bindE_def) - apply (rule validNF_bind [rotated]) - apply assumption - apply (clarsimp simp: lift_def throwError_def split: sum.splits) - apply wpsimp - done - -lemma validNF_catch [wp]: - "\\x. \E x\ handler x \Q\!; \P\ f \Q\, \E\!\ \ \P\ f (\x. handler x) \Q\!" - apply (unfold validE_NF_alt_def catch_def) - apply (rule validNF_bind [rotated]) - apply assumption - apply (clarsimp simp: lift_def throwError_def split: sum.splits) - apply wp - done - -lemma validNF_throwError [wp]: - "\E e\ throwError e \P\, \E\!" - by (unfold validE_NF_alt_def throwError_def o_def) wpsimp - -lemma validNF_returnOk [wp]: - "\P e\ returnOk e \P\, \E\!" - by (clarsimp simp: validE_NF_alt_def returnOk_def) wpsimp - -lemma validNF_whenE [wp]: - "(P \ \Q\ f \R\, \E\!) \ \if P then Q else R ()\ whenE P f \R\, \E\!" - unfolding whenE_def by clarsimp wp - -lemma validNF_nobindE [wp]: - "\ \B\ g \C\,\E\!; - \A\ f \\r s. B s\,\E\! \ \ - \A\ doE f; g odE \C\,\E\!" - by clarsimp wp - -(* - * Setup triple rules for validE_NF so that we can use the - * "wp_comb" attribute. - *) - -definition "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')" - -lemma validE_NF_is_triple [wp_trip]: - "validE_NF P f Q E = triple_judgement P f (validE_NF_property Q E)" - apply (clarsimp simp: validE_NF_def validE_def2 no_fail_def triple_judgement_def - validE_NF_property_def split: sum.splits) - apply blast - done - -lemmas [wp_comb] = validE_NF_weaken_pre - -lemma validNF_cong: - "\ \s. P s = P' s; \s. P s \ m s = m' s; - \r' s' s. \ P s; (r', s') \ mres (m s) \ \ Q r' s' = Q' r' s' \ \ - (\ P \ m \ Q \!) = (\ P' \ m' \ Q' \!)" - by (fastforce simp: validNF_alt_def) - -lemma validE_NF_liftE [wp]: - "\P\ f \Q\! \ \P\ liftE f \Q\,\E\!" - by (wpsimp simp: validE_NF_alt_def liftE_def) - -lemma validE_NF_handleE' [wp]: - "\ \x. \F x\ handler x \Q\,\E\!; \P\ f \Q\,\F\! \ \ - \P\ f (\x. handler x) \Q\,\E\!" - apply (unfold validE_NF_alt_def handleE'_def) - apply (rule validNF_bind [rotated]) - apply assumption - apply (clarsimp split: sum.splits) - apply wpsimp - done - -lemma validE_NF_handleE [wp]: - "\ \x. \F x\ handler x \Q\,\E\!; \P\ f \Q\,\F\! \ \ - \P\ f handler \Q\,\E\!" - apply (unfold handleE_def) - apply (metis validE_NF_handleE') - done - -lemma validE_NF_condition [wp]: - "\ \ Q \ A \P\,\ E \!; \ R \ B \P\,\ E \!\ - \ \\s. if C s then Q s else R s\ condition C A B \P\,\ E \!" - apply rule - apply (drule validE_NF_valid)+ - apply wp - apply (drule validE_NF_no_fail)+ - apply (clarsimp simp: no_fail_def condition_def) - done - -lemma validI_name_pre: - "prefix_closed f \ - (\s0 s. P s0 s \ \\s0' s'. s0' = s0 \ s' = s\,\R\ f \G\,\Q\) - \ \P\,\R\ f \G\,\Q\" - unfolding validI_def - by metis - -lemma validI_well_behaved': - "prefix_closed f - \ \P\,\R'\ f \G'\,\Q\ - \ R \ R' - \ G' \ G - \ \P\,\R\ f \G\,\Q\" - apply (subst validI_def, clarsimp) - apply (clarsimp simp add: rely_def) - apply (drule (2) validI_D) - apply (fastforce simp: rely_cond_def guar_cond_def)+ - done +lemma True_E_E[wp]: + "\\\ f -,\\\\" + by (auto simp: validE_E_def validE_def valid_def split: sum.splits) -lemmas validI_well_behaved = validI_well_behaved'[unfolded le_fun_def, simplified] -text \Strengthen setup.\ +subsection \Strongest postcondition rules\ -context strengthen_implementation begin +lemma get_sp: + "\P\ get \\rv s. s = rv \ P s\" + by(simp add:get_def valid_def mres_def) -lemma strengthen_hoare [strg]: - "(\r s. st F (\) (Q r s) (R r s)) - \ st F (\) (\P\ f \Q\) (\P\ f \R\)" - by (cases F, auto elim: hoare_strengthen_post) +lemma put_sp: + "\\\ put a \\_ s. s = a\" + by(simp add:put_def valid_def mres_def) -lemma strengthen_validE_R_cong[strg]: - "(\r s. st F (\) (Q r s) (R r s)) - \ st F (\) (\P\ f \Q\, -) (\P\ f \R\, -)" - by (cases F, auto intro: hoare_post_imp_R) +lemma return_sp: + "\P\ return a \\rv s. rv = a \ P s\" + by(simp add:return_def valid_def mres_def) -lemma strengthen_validE_cong[strg]: - "(\r s. st F (\) (Q r s) (R r s)) - \ (\r s. st F (\) (S r s) (T r s)) - \ st F (\) (\P\ f \Q\, \S\) (\P\ f \R\, \T\)" - by (cases F, auto elim: hoare_post_impErr) +lemma hoare_return_sp: (* FIXME lib: eliminate *) + "\P\ return x \\rv. P and K (rv = x)\" + by (simp add: valid_def return_def mres_def) -lemma strengthen_validE_E_cong[strg]: - "(\r s. st F (\) (S r s) (T r s)) - \ st F (\) (\P\ f -, \S\) (\P\ f -, \T\)" - by (cases F, auto elim: hoare_post_impErr simp: validE_E_def) +lemma assert_sp: + "\P\ assert Q \\_ s. P s \ Q \" + by (simp add: assert_def fail_def return_def valid_def mres_def) -lemma strengthen_validI[strg]: - "(\r s0 s. st F (\) (Q r s0 s) (Q' r s0 s)) - \ st F (\) (\P\,\G\ f \R\,\Q\) (\P\,\G\ f \R\,\Q'\)" - by (cases F, auto elim: validI_strengthen_post) +lemma hoare_gets_sp: + "\P\ gets f \\rv s. rv = f s \ P s\" + by (simp add: valid_def simpler_gets_def mres_def) -end +lemma hoare_returnOk_sp: + "\P\ returnOk x \\rv s. rv = x \ P s\, \Q\" + by (simp add: valid_def validE_def returnOk_def return_def mres_def) end diff --git a/lib/concurrency/Atomicity_Lib.thy b/lib/concurrency/Atomicity_Lib.thy index 728dbdac88..8f50ac0e02 100644 --- a/lib/concurrency/Atomicity_Lib.thy +++ b/lib/concurrency/Atomicity_Lib.thy @@ -5,8 +5,9 @@ *) theory Atomicity_Lib -imports "Prefix_Refinement" - +imports + Prefix_Refinement + Monads.Trace_Det begin text \This library introduces a number of proofs about the question of @@ -186,7 +187,7 @@ lemma repeat_n_nothing: lemma repeat_nothing: "repeat (\_. {}) = return ()" by (simp add: repeat_def bind_def select_def repeat_n_nothing - Sigma_def if_fun_lift UN_If_distrib return_def + Sigma_def if_distribR UN_If_distrib return_def cong del: image_cong_simp) lemma detrace_env_steps: diff --git a/lib/concurrency/Prefix_Refinement.thy b/lib/concurrency/Prefix_Refinement.thy index 774d3360f6..20f0e5bf9b 100644 --- a/lib/concurrency/Prefix_Refinement.thy +++ b/lib/concurrency/Prefix_Refinement.thy @@ -7,8 +7,6 @@ theory Prefix_Refinement imports Triv_Refinement - "Monads.Trace_Lemmas" - begin section \Definition of prefix fragment refinement.\ @@ -1242,7 +1240,7 @@ lemma prefix_refinement_repeat: apply simp apply (rule prefix_refinement_repeat_n, assumption+) apply (rule validI_weaken_pre, assumption, simp) - apply (wp select_wp) + apply wp apply wp apply clarsimp apply clarsimp diff --git a/lib/concurrency/Triv_Refinement.thy b/lib/concurrency/Triv_Refinement.thy index caefd59834..b31995381f 100644 --- a/lib/concurrency/Triv_Refinement.thy +++ b/lib/concurrency/Triv_Refinement.thy @@ -6,8 +6,8 @@ theory Triv_Refinement imports - "Monads.Trace_VCG" - "Monads.Strengthen" + "Monads.Trace_RG" + "Monads.Trace_Strengthen_Setup" begin