From 7b9ca48fe2c33dea2df9aca8e3cc844e0fc14765 Mon Sep 17 00:00:00 2001 From: Corey Lewis Date: Mon, 14 Aug 2023 15:35:46 +1000 Subject: [PATCH] lib/monads: split content out into Trace_RG and Trace_No_Trace Signed-off-by: Corey Lewis --- lib/Monads/trace/Trace_Lemmas_Old.thy | 335 ---------- lib/Monads/trace/Trace_Monad.thy | 82 --- lib/Monads/trace/Trace_Monad_Equations.thy | 203 ++++++ lib/Monads/trace/Trace_No_Trace.thy | 70 ++ lib/Monads/trace/Trace_RG.thy | 691 ++++++++++++++++++++ lib/Monads/trace/Trace_Strengthen_Setup.thy | 2 +- lib/Monads/trace/Trace_VCG.thy | 532 +-------------- 7 files changed, 968 insertions(+), 947 deletions(-) delete mode 100644 lib/Monads/trace/Trace_Lemmas_Old.thy create mode 100644 lib/Monads/trace/Trace_No_Trace.thy create mode 100644 lib/Monads/trace/Trace_RG.thy diff --git a/lib/Monads/trace/Trace_Lemmas_Old.thy b/lib/Monads/trace/Trace_Lemmas_Old.thy deleted file mode 100644 index 2c5bc81e67..0000000000 --- a/lib/Monads/trace/Trace_Lemmas_Old.thy +++ /dev/null @@ -1,335 +0,0 @@ -(* - * Copyright 2023, Proofcraft Pty Ltd - * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) - * - * SPDX-License-Identifier: BSD-2-Clause - *) - -theory Trace_Lemmas_Old - imports - Trace_More_VCG - Trace_Monad_Equations -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) - -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] - -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 diff --git a/lib/Monads/trace/Trace_Monad.thy b/lib/Monads/trace/Trace_Monad.thy index 3de9644457..ede246ed79 100644 --- a/lib/Monads/trace/Trace_Monad.thy +++ b/lib/Monads/trace/Trace_Monad.thy @@ -721,86 +721,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 - -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" - -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 index 4fef376434..a2072db008 100644 --- a/lib/Monads/trace/Trace_Monad_Equations.thy +++ b/lib/Monads/trace/Trace_Monad_Equations.thy @@ -45,4 +45,207 @@ lemma fail_bind[simp]: "fail >>= f = fail" by (simp add: bind_def fail_def) + +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_No_Trace.thy b/lib/Monads/trace/Trace_No_Trace.thy new file mode 100644 index 0000000000..aff4cab62e --- /dev/null +++ b/lib/Monads/trace/Trace_No_Trace.thy @@ -0,0 +1,70 @@ +(* + * 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 + +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_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] = no_trace_is_triple + +(* 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 + +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..6aef80035f --- /dev/null +++ b/lib/Monads/trace/Trace_RG.thy @@ -0,0 +1,691 @@ +(* + * 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 + +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" + +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')))" + +(* +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 _ _ 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)] + +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) + +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 + + + +(* 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 + +lemmas [wp_trip] = validI_is_triple + +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 + +(* 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 + +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_Strengthen_Setup.thy b/lib/Monads/trace/Trace_Strengthen_Setup.thy index bd978d60c1..024d370f8b 100644 --- a/lib/Monads/trace/Trace_Strengthen_Setup.thy +++ b/lib/Monads/trace/Trace_Strengthen_Setup.thy @@ -9,7 +9,7 @@ theory Trace_Strengthen_Setup imports Strengthen Trace_No_Fail - Trace_VCG + Trace_RG begin section \Strengthen setup.\ diff --git a/lib/Monads/trace/Trace_VCG.thy b/lib/Monads/trace/Trace_VCG.thy index 944650d4a7..12e2576aa0 100644 --- a/lib/Monads/trace/Trace_VCG.thy +++ b/lib/Monads/trace/Trace_VCG.thy @@ -32,8 +32,8 @@ text \ 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).\ + 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 @@ -58,27 +58,7 @@ definition validE :: 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 \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.\ @@ -1101,510 +1081,4 @@ 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) - - - -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) - -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 - -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 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] = 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 - -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 - -(* 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 - -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] - end