diff --git a/lib/Monads/trace/Trace_Empty_Fail.thy b/lib/Monads/trace/Trace_Empty_Fail.thy index b2b531768f..7227712ff5 100644 --- a/lib/Monads/trace/Trace_Empty_Fail.thy +++ b/lib/Monads/trace/Trace_Empty_Fail.thy @@ -55,6 +55,10 @@ lemma empty_failD3: "\ empty_fail f; \ failed (f s) \ \ mres (f s) \ {}" by (drule(1) empty_failD2, clarsimp) +lemma empty_fail_not_empty: + "empty_fail f \ \s. f s \ {}" + by (auto simp: empty_fail_def mres_def) + lemma empty_fail_bindD1: "empty_fail (a >>= b) \ empty_fail a" unfolding empty_fail_def bind_def diff --git a/lib/Monads/trace/Trace_Monad.thy b/lib/Monads/trace/Trace_Monad.thy index 98b378a629..dc1c29b794 100644 --- a/lib/Monads/trace/Trace_Monad.thy +++ b/lib/Monads/trace/Trace_Monad.thy @@ -805,6 +805,12 @@ definition Await :: "('s \ bool) \ ('s,unit) tmonad" whe section "Parallel combinator" +text \ + Programs combined with @{text parallel} should begin with an + @{const env_steps} and end with @{const interference} to be wellformed. + This ensures that there are at least enough enough environment steps in + each program for their traces to be able to be matched up; without it + the composed program would be trivially empty.\ 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 diff --git a/lib/Monads/trace/Trace_Monad_Equations.thy b/lib/Monads/trace/Trace_Monad_Equations.thy index 5887fb7169..21c22b6188 100644 --- a/lib/Monads/trace/Trace_Monad_Equations.thy +++ b/lib/Monads/trace/Trace_Monad_Equations.thy @@ -10,7 +10,9 @@ theory Trace_Monad_Equations imports + Trace_Empty_Fail Trace_No_Fail + Trace_No_Trace begin lemmas assertE_assert = assertE_liftE @@ -214,7 +216,7 @@ lemma bind_return_unit: by simp lemma modify_id_return: - "modify id = return ()" + "modify id = return ()" by (simp add: simpler_modify_def return_def) lemma liftE_bind_return_bindE_returnOk: @@ -245,6 +247,38 @@ lemma zipWithM_x_modify: apply (simp add: simpler_modify_def bind_def split_def) done +lemma bind_return_subst: + assumes r: "\r. \\s. P x = r\ f x \\rv s. Q rv = r\" + shows + "do a \ f x; + g (Q a) + od = + do _ \ f x; + g (P x) + od" +proof - + have "do a \ f x; + return (Q a) + od = + do _ \ f x; + return (P x) + od" + using r + apply (subst fun_eq_iff) + apply (auto simp: bind_def valid_def return_def mres_def vimage_def split: tmres.splits; + fastforce simp: image_def intro: rev_bexI) + done + hence "do a \ f x; + return (Q a) + od >>= g = + do _ \ f x; + return (P x) + od >>= g" + by (rule bind_cong, simp) + thus ?thesis + by simp +qed + lemma assert2: "(do v1 \ assert P; v2 \ assert Q; c od) = (do v \ assert (P \ Q); c od)" @@ -306,6 +340,28 @@ lemma if_bind: lemma bind_liftE_distrib: "(liftE (A >>= (\x. B x))) = (liftE A >>=E (\x. liftE (\s. B x s)))" by (clarsimp simp: liftE_def bindE_def lift_def bind_assoc) +(*FIXME: the following lemmas were originally solved by monad_eq, which doesn't yet exist for the + trace monad due to traces making equality more complicated.*) +lemma condition_apply_cong: + "\ c s = c' s'; s = s'; \s. c' s \ l s = l' s ; \s. \ c' s \ r s = r' s \ \ condition c l r s = condition c' l' r' s'" + by (simp add: condition_def) + +lemma condition_cong [cong, fundef_cong]: + "\ c = c'; \s. c' s \ l s = l' s; \s. \ c' s \ r s = r' s \ \ condition c l r = condition c' l' r'" + by (simp add: condition_def fun_eq_iff) + +lemma lift_Inr [simp]: "(lift X (Inr r)) = (X r)" + by (simp add: lift_def) + +lemma lift_Inl [simp]: "lift C (Inl a) = throwError a" + by (simp add: lift_def) + +lemma returnOk_def2: "returnOk a = return (Inr a)" + by (simp add: returnOk_def) + +lemma liftE_fail[simp]: "liftE fail = fail" + by (simp add: liftE_def) + lemma if_catch_distrib: "((if P then f else g) h) = (if P then f h else g h)" by (simp split: if_split) @@ -328,10 +384,115 @@ lemma catch_is_if: lemma liftE_K_bind: "liftE ((K_bind (\s. A s)) x) = K_bind (liftE (\s. A s)) x" by clarsimp +lemma monad_eq_split: + assumes "\r s. Q r s \ f r s = f' r s" + "\P\ g \\r s. Q r s\" + "P s" + shows "(g >>= f) s = (g >>= f') s" +proof - + have pre: "\rv s'. \(rv, s') \ mres (g s)\ \ f rv s' = f' rv s'" + using assms unfolding valid_def apply - + by (erule allE[where x=s]) (fastforce simp: mres_def image_def) + show ?thesis + by (fastforce intro!: bind_apply_cong simp: pre) +qed + +lemma monad_eq_split2: + assumes eq: " g' s = g s" + assumes tail:"\r s. Q r s \ f r s = f' r s" + and hoare: "\P\ g \\r s. Q r s\" "P s" + shows "(g >>= f) s = (g' >>= f') s" + apply (rule trans) + apply (rule monad_eq_split[OF tail hoare], assumption) + apply (clarsimp simp: bind_def eq) + done + lemma monad_eq_split_tail: "\f = g; a s = b s\ \ (a >>= f) s = ((b >>= g) s)" by (simp add:bind_def) +lemma double_gets_drop_regets: + "(do x \ gets f; + y \ gets f; + m y x + od) = + (do x \ gets f; + m x x + od)" + by (simp add: simpler_gets_def bind_def) + +lemma state_assert_false[simp]: + "state_assert (\_. False) = fail" + by (simp add: state_assert_def get_def bind_def) + +lemma condition_fail_rhs: + "condition C X fail = (state_assert C >>= (\_. X))" + by (auto simp: condition_def state_assert_def assert_def fail_def return_def get_def bind_def + fun_eq_iff) + +lemma condition_swap: + "condition C A B = condition (\s. \ C s) B A" + by (simp add: condition_def fun_eq_iff) + +lemma condition_fail_lhs: + "condition C fail X = (state_assert (\s. \ C s) >>= (\_. X))" + by (metis condition_fail_rhs condition_swap) + +lemma condition_bind_fail[simp]: + "(condition C A B >>= (\_. fail)) = condition C (A >>= (\_. fail)) (B >>= (\_. fail))" + by (auto simp: condition_def assert_def fail_def bind_def fun_eq_iff) + +lemma bind_fail_propagates: + "\no_trace A; empty_fail A\ \ A >>= (\_. fail) = fail" + by (fastforce simp: no_trace_def fail_def bind_def case_prod_unfold + dest!: empty_fail_not_empty split: tmres.splits) + +lemma simple_bind_fail [simp]: + "(state_assert X >>= (\_. fail)) = fail" + "(modify M >>= (\_. fail)) = fail" + "(return X >>= (\_. fail)) = fail" + "(gets X >>= (\_. fail)) = fail" + by (auto intro!: bind_fail_propagates) + +lemma bind_inv_inv_comm: + "\ \P. \P\ f \\_. P\; \P. \P\ g \\_. P\; + empty_fail f; empty_fail g; no_trace f; no_trace g \ \ + do x \ f; y \ g; n x y od = do y \ g; x \ f; n x y od" + apply (rule ext) + apply (rule trans[where s="(do (x, y) \ do x \ f; y \ (\_. g s) ; (\_. return (x, y) s) od; + n x y od) s" for s]) + apply (simp add: bind_assoc) + apply (intro bind_apply_cong, simp_all)[1] + apply (metis in_inv_by_hoareD) + apply (simp add: return_def bind_def) + apply (metis in_inv_by_hoareD) + apply (rule trans[where s="(do (x, y) \ do y \ g; x \ (\_. f s) ; (\_. return (x, y) s) od; + n x y od) s" for s, rotated]) + apply (simp add: bind_assoc) + apply (intro bind_apply_cong, simp_all)[1] + apply (metis in_inv_by_hoareD) + apply (simp add: return_def bind_def) + apply (metis in_inv_by_hoareD) + apply (rule bind_apply_cong, simp_all) + apply (clarsimp simp: bind_def split_def return_def) + apply (rule subset_antisym; + clarsimp simp: no_trace_def case_prod_unfold + split: tmres.splits dest!: empty_fail_not_empty) + apply ((drule_tac x=x in spec)+, fastforce)+ + done + +lemma bind_known_operation_eq: + "\ no_fail P f; \Q\ f \\rv s. rv = x \ s = t\; P s; Q s; empty_fail f; no_trace f \ + \ (f >>= g) s = g x t" + apply (drule(1) no_failD) + apply (subgoal_tac "f s = {([], Result (x, t))}") + apply (clarsimp simp: bind_def) + apply (rule subset_antisym; + clarsimp simp: valid_def empty_fail_def no_trace_def mres_def image_def failed_def) + apply (metis eq_snd_iff tmres.exhaust) + apply fastforce + done + lemma assert_opt_If: "assert_opt v = If (v = None) fail (return (the v))" by (simp add: assert_opt_def split: option.split) @@ -384,6 +545,25 @@ lemma mapM_x_Cons: "mapM_x f [] = return ()" by (simp_all add: mapM_x_def sequence_x_def) +lemma mapME_Cons: + "mapME f (x # xs) = doE + y \ f x; + ys \ mapME f xs; + returnOk (y # ys) + odE" + and mapME_Nil: + "mapME f [] = returnOk []" + by (simp_all add: mapME_def sequenceE_def) + +lemma mapME_x_Cons: + "mapME_x f (x # xs) = doE + y \ f x; + mapME_x f xs + odE" + and mapME_x_Nil: + "mapME_x f [] = returnOk ()" + by (simp_all add: mapME_x_def sequenceE_x_def) + lemma mapM_append: "mapM f (xs @ ys) = (do fxs \ mapM f xs; @@ -399,6 +579,21 @@ lemma mapM_x_append: od)" by (induct xs, simp_all add: mapM_x_Cons mapM_x_Nil bind_assoc) +lemma mapME_append: + "mapME f (xs @ ys) = (doE + fxs \ mapME f xs; + fys \ mapME f ys; + returnOk (fxs @ fys) + odE)" + by (induct xs, simp_all add: mapME_Cons mapME_Nil bindE_assoc) + +lemma mapME_x_append: + "mapME_x f (xs @ ys) = (doE + fxs \ mapME_x f xs; + mapME_x f ys + odE)" + by (induct xs, simp_all add: mapME_x_Cons mapME_x_Nil bindE_assoc) + lemma mapM_map: "mapM f (map g xs) = mapM (f o g) xs" by (induct xs; simp add: mapM_Nil mapM_Cons) @@ -407,6 +602,14 @@ 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) +lemma mapME_map: + "mapME f (map g xs) = mapME (f o g) xs" + by (induct xs; simp add: mapME_Nil mapME_Cons) + +lemma mapME_x_map: + "mapME_x f (map g xs) = mapME_x (f o g) xs" + by (induct xs; simp add: mapME_x_Nil mapME_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" diff --git a/lib/concurrency/Atomicity_Lib.thy b/lib/concurrency/Atomicity_Lib.thy index a895fbb607..7801d68bfe 100644 --- a/lib/concurrency/Atomicity_Lib.thy +++ b/lib/concurrency/Atomicity_Lib.thy @@ -4,18 +4,17 @@ * SPDX-License-Identifier: BSD-2-Clause *) theory Atomicity_Lib - -imports - Prefix_Refinement - Monads.Trace_Det + imports + Prefix_Refinement + Monads.Trace_Det begin -text \This library introduces a number of proofs about the question of -atomicity refinement, particularly in combination with the existing -prefix refinement notion. It introduces an additional notion of refinement -which left-composes with prefix refinement and can be used to rearrange -operations around interference points. -\ +text \ + This library introduces a number of proofs about the question of + atomicity refinement, particularly in combination with the existing + prefix refinement notion. It introduces an additional notion of refinement + which left-composes with prefix refinement and can be used to rearrange + operations around interference points.\ abbreviation "interferences \ repeat interference" @@ -27,28 +26,25 @@ lemma triv_refinement_Await_env_steps: apply simp done -lemmas prefix_refinement_env_steps_Await - = prefix_refinement_triv_refinement_conc[OF - prefix_refinement_env_steps triv_refinement_Await_env_steps] +lemmas prefix_refinement_env_steps_Await = + prefix_refinement_triv_refinement_conc[OF prefix_refinement_env_steps triv_refinement_Await_env_steps] lemma pfx_refn_interferences: - " env_stable AR R sr iosr (\t. True) - \ prefix_refinement sr iosr iosr (\\) (\\) (\\) AR R interferences interferences" + "env_stable AR R sr iosr (\_. True) + \ prefix_refinement sr iosr iosr dc AR R \\ \\ interferences interferences" apply (rule prefix_refinement_repeat) apply (erule prefix_refinement_interference) apply wp+ done lemma repeat_n_validI: - "\I\,\R\ f \G\,\\_. I\ - \ \I\,\R\ repeat_n n f \G\,\\_. I\" + "\I\,\R\ f \G\,\\_. I\ \ \I\,\R\ repeat_n n f \G\,\\_. I\" apply (induct n) apply wpsimp+ done lemma repeat_validI: - "\I\,\R\ f \G\,\\_. I\ - \ \I\,\R\ repeat f \G\,\\_. I\" + "\I\,\R\ f \G\,\\_. I\ \ \I\,\R\ repeat f \G\,\\_. I\" apply (simp add: repeat_def) apply (wpsimp wp: repeat_n_validI) done @@ -68,29 +64,27 @@ lemma repeat_pre_triv_refinement[simplified]: apply (simp add: repeat_def select_early) apply (rule triv_refinement_select_concrete_All; clarsimp) apply (rule_tac x="Suc x" in triv_refinement_select_abstract_x; simp) - apply (rule triv_refinement_refl) done lemma repeat_none_triv_refinement: "triv_refinement (repeat f) (return ())" apply (simp add: repeat_def) apply (rule_tac x="0" in triv_refinement_select_abstract_x; simp) - apply (rule triv_refinement_refl) done -lemmas repeat_triv_refinement_consume_1 - = triv_refinement_trans[OF triv_refinement_mono_bind(1), - OF repeat_pre_triv_refinement, simplified bind_assoc, - OF triv_refinement_mono_bind(2), simplified] +lemmas repeat_triv_refinement_consume_1 = + triv_refinement_trans[OF triv_refinement_mono_bind(1), + OF repeat_pre_triv_refinement, simplified bind_assoc, + OF triv_refinement_mono_bind(2), simplified] -lemmas repeat_one_triv_refinement - = repeat_triv_refinement_consume_1[where b=return and d=return, - simplified, OF repeat_none_triv_refinement] +lemmas repeat_one_triv_refinement = + repeat_triv_refinement_consume_1[where b=return and d=return, simplified, + OF repeat_none_triv_refinement] schematic_goal prefix_refinement_interferences_split: - "prefix_refinement sr isr osr rvr P Q AR R ?aprog cprog - \ prefix_refinement sr isr osr rvr P Q AR R - (do y <- interferences; aprog od) cprog" + "prefix_refinement sr isr osr rvr AR R P Q ?aprog cprog + \ prefix_refinement sr isr osr rvr AR R P Q + (do y <- interferences; aprog od) cprog" apply (rule prefix_refinement_triv_refinement_abs) apply (rule triv_refinement_mono_bind) apply (rule triv_refinement_trans) @@ -99,21 +93,18 @@ schematic_goal prefix_refinement_interferences_split: apply (simp add: bind_assoc) done -text \Suppressing interference points. The constant below discards -the self actions within a trace and filters out traces in which the -environment acts. This reduces both env_steps and interference to -noops. -\ +text \ + Suppressing interference points. The constant below discards + the self actions within a trace and filters out traces in which the + environment acts. This reduces both env_steps and interference to + noops.\ -definition - detrace :: "('s, 'a) tmonad \ ('s, 'a) tmonad" -where - "detrace f = (\s. (\(tr, res). ([], res)) - ` (f s \ ({tr. Env \ fst ` set tr} \ {res. res \ Incomplete})))" +definition detrace :: "('s, 'a) tmonad \ ('s, 'a) tmonad" where + "detrace f = + (\s. (\(tr, res). ([], res)) ` (f s \ ({tr. Env \ fst ` set tr} \ {res. res \ Incomplete})))" lemma detrace_UN: - "detrace (\s. \x \ S s. f x s) - = (\s. \x \ S s. detrace (f x) s)" + "detrace (\s. \x \ S s. f x s) = (\s. \x \ S s. detrace (f x) s)" apply (simp add: detrace_def) apply (rule ext; fastforce) done @@ -151,13 +142,13 @@ lemma detrace_select[simp]: by (rule ext, auto simp add: select_def detrace_def image_image) lemma detrace_put_trace_elem: - "detrace (put_trace_elem (tmid, s)) = (if tmid = Env - then (\_. {}) else return ())" + "detrace (put_trace_elem (tmid, s)) = + (if tmid = Env then (\_. {}) else return ())" by (simp add: put_trace_elem_def detrace_def return_def) lemma detrace_put_trace: - "detrace (put_trace xs) = (if Env \ fst ` set xs - then (\_. {}) else return ())" + "detrace (put_trace xs) = + (if Env \ fst ` set xs then (\_. {}) else return ())" apply (induct xs; simp) apply (clarsimp simp: detrace_bind detrace_put_trace_elem) apply (simp add: bind_def) @@ -198,21 +189,18 @@ lemma detrace_interference: apply (simp add: bind_def get_def) done -text \Decomposition of environment and program actions by strict -separation, possibly relevant for ``recovering'' atomicity.\ +text \ + Decomposition of environment and program actions by strict separation, possibly relevant for + ``recovering'' atomicity.\ lemma equivp_compare_f: "equivp (\x y. f x = f y)" by (simp add: equivp_def fun_eq_iff, metis) -definition - fst_split_eq :: "('s \ ('e \ 'p)) \ ('s \ 's \ bool)" -where +definition fst_split_eq :: "('s \ ('e \ 'p)) \ ('s \ 's \ bool)" where "fst_split_eq f = (\s s'. fst (f s) = fst (f s'))" -definition - snd_split_eq :: "('s \ ('e \ 'p)) \ ('s \ 's \ bool)" -where +definition snd_split_eq :: "('s \ ('e \ 'p)) \ ('s \ 's \ bool)" where "snd_split_eq f = (\s s'. snd (f s) = snd (f s'))" lemma equivp_split_eqs: @@ -220,18 +208,17 @@ lemma equivp_split_eqs: "equivp (snd_split_eq f)" by (simp_all add: fst_split_eq_def snd_split_eq_def equivp_compare_f) -text \One way of defining the "diamond" pattern in which two state -changes commute. Depends on a way of splitting the state into domains, -in which state changes can be observed to impact only certain domains. -This can define a unique way of reordering operations that impact -disjoint sets of domains.\ +text \ + One way of defining the "diamond" pattern in which two state + changes commute. Depends on a way of splitting the state into domains, + in which state changes can be observed to impact only certain domains. + This can define a unique way of reordering operations that impact + disjoint sets of domains.\ type_synonym ('s, 'd) domain_split = "'s \ 'd \ 's" -definition - dom_s_match :: "('s, 'd) domain_split \ 'd set \ 's \ 's \ bool" -where +definition dom_s_match :: "('s, 'd) domain_split \ 'd set \ 's \ 's \ bool" where "dom_s_match ds D s s' = (\d \ D. ds s' d = ds s d)" lemma dom_s_match_refl: @@ -246,15 +233,12 @@ lemma dom_s_match_equivp: done lemma dom_s_match_mono: - "dom_s_match ds D s s' \ D' \ D - \ dom_s_match ds D' s s'" + "\dom_s_match ds D s s'; D' \ D\ \ dom_s_match ds D' s s'" by (auto simp add: dom_s_match_def) -definition - diamond :: "('s, 'd) domain_split \ 's \ 's \ 's \ 's \ bool" -where - "diamond ds s sa sb sab = (\d. (ds sab d = ds sa d \ ds sb d = ds s d) - \ (ds sab d = ds sb d \ ds sa d = ds s d))" +definition diamond :: "('s, 'd) domain_split \ 's \ 's \ 's \ 's \ bool" where + "diamond ds s sa sb sab = + (\d. (ds sab d = ds sa d \ ds sb d = ds s d) \ (ds sab d = ds sb d \ ds sa d = ds s d))" lemma diamond_flips: "diamond ds s sa sb sab \ diamond ds sb sab s sa" @@ -265,35 +249,28 @@ lemma diamond_diag_flip: "diamond ds s sa sb sab \ diamond ds s sb sa sab" by (simp add: diamond_def, metis) -definition - domains_complete :: "('s, 'd) domain_split \ bool" -where +definition domains_complete :: "('s, 'd) domain_split \ bool" where "domains_complete ds = (\s s'. (\d. ds s d = ds s' d) \ s = s')" lemmas domains_completeD = domains_complete_def[THEN iffD1, rule_format] lemma diamond_unique: - "domains_complete ds \ diamond ds s sa sb sab - \ diamond ds s sa sb sab' \ sab = sab'" + "\domains_complete ds; diamond ds s sa sb sab; diamond ds s sa sb sab'\ \ sab = sab'" apply (erule domains_completeD) apply (simp add: diamond_def) apply metis done lemma diamond_uniques_other: - "domains_complete ds \ diamond ds s sa sb sab - \ diamond ds s sa sb' sab \ sb = sb'" - "domains_complete ds \ diamond ds s sa sb sab - \ diamond ds s sa' sb sab \ sa = sa'" - "domains_complete ds \ diamond ds s sa sb sab - \ diamond ds s' sa sb sab \ s = s'" + "\domains_complete ds; diamond ds s sa sb sab; diamond ds s sa sb' sab\ \ sb = sb'" + "\domains_complete ds; diamond ds s sa sb sab; diamond ds s sa' sb sab\ \ sa = sa'" + "\domains_complete ds; diamond ds s sa sb sab; diamond ds s' sa sb sab\ \ s = s'" by (metis diamond_unique diamond_flips)+ lemmas diamond_uniques = diamond_unique diamond_uniques_other lemma dom_s_match_diamond: - "dom_s_match ds D s sa \ diamond ds s sa sb sab - \ dom_s_match ds D sb sab" + "\dom_s_match ds D s sa; diamond ds s sa sb sab\ \ dom_s_match ds D sb sab" apply (simp add: dom_s_match_def diamond_def) apply metis done @@ -307,28 +284,26 @@ lemma diamond_trans_eq: by (simp add: fun_eq_iff, metis diamond_trans diamond_flips) text \ -A notion of refinement by traces related under a state relation. Simpler -than @{term prefix_refinement}, and left-composes with -@{term prefix_refinement}. - -We'll use this notion to show how the concrete side of a @{term prefix_refinement} -hypothesis can be reordered to better match its specification, in particular -how interference points can be moved. -\ - -definition - rel_tr_refinement :: "('s \ 's \ bool) \ ('s \ bool) \ 's rg_pred - \ bool \ ('s, 'a) tmonad \ ('s, 'a) tmonad \ bool" -where - "rel_tr_refinement sr P R commit f g = (\tr res s s0. P s - \ (tr, res) \ f s \ rely_cond R s0 tr \ (commit \ s0 = s) - \ (\tr'. (tr', res) \ g s \ rely_cond R s0 tr' - \ list_all2 (rel_prod (=) sr) tr tr'))" + A notion of refinement by traces related under a state relation. Simpler + than @{term prefix_refinement}, and left-composes with + @{term prefix_refinement}. + + We'll use this notion to show how the concrete side of a @{term prefix_refinement} + hypothesis can be reordered to better match its specification, in particular + how interference points can be moved.\ + +definition rel_tr_refinement :: + "('s \ 's \ bool) \ ('s \ bool) \ 's rg_pred \ bool \ ('s, 'a) tmonad \ ('s, 'a) tmonad \ bool" + where + "rel_tr_refinement sr P R commit f g = + (\tr res s s0. P s + \ (tr, res) \ f s \ rely_cond R s0 tr \ (commit \ s0 = s) + \ (\tr'. (tr', res) \ g s \ rely_cond R s0 tr' + \ list_all2 (rel_prod (=) sr) tr tr'))" lemma rely_cond_equiv_s: - "rely_cond R s0 tr - \ (\s. tr \ [] \ last tr = (Env, s) \ R s0 s \ R s0' s) - \ rely_cond R s0' tr" + "\rely_cond R s0 tr; \s. tr \ [] \ last tr = (Env, s) \ R s0 s \ R s0' s\ + \ rely_cond R s0' tr" apply (cases tr rule: rev_cases) apply simp apply (clarsimp simp: rely_cond_append rely_cond_def[where tr="Cons x xs" for x xs]) @@ -337,23 +312,19 @@ lemma rely_cond_equiv_s: lemmas rel_tr_refinementD = rel_tr_refinement_def[THEN iffD1, rule_format] lemma rel_tr_refinement_refl: - "reflp sr - \ rel_tr_refinement sr P R C f f" + "reflp sr \ rel_tr_refinement sr P R C f f" apply (clarsimp simp: rel_tr_refinement_def) apply (intro exI, rule conjI, assumption) apply (simp add: list_all2_same rel_prod_sel reflpD) done lemma rel_tr_refinement_drop_C: - "rel_tr_refinement sr P R False f g - \ rel_tr_refinement sr P R C f g" + "rel_tr_refinement sr P R False f g \ rel_tr_refinement sr P R C f g" by (clarsimp simp: rel_tr_refinement_def) lemma rel_tr_refinement_trans: - "transp sr - \ rel_tr_refinement sr P R C f g - \ rel_tr_refinement sr P R C g h - \ rel_tr_refinement sr P R C f h" + "\transp sr; rel_tr_refinement sr P R C f g; rel_tr_refinement sr P R C g h\ + \ rel_tr_refinement sr P R C f h" apply (subst rel_tr_refinement_def, clarsimp) apply (drule(3) rel_tr_refinementD, clarsimp+) apply (drule(3) rel_tr_refinementD, clarsimp+) @@ -365,7 +336,7 @@ lemma rel_tr_refinement_trans: lemma list_all2_matching_tr_pfx: "list_all2 (rel_prod (=) (\cs cs'. \as. sr as cs = sr as cs')) tr tr' - \ matching_tr_pfx sr atr tr = matching_tr_pfx sr atr tr'" + \ matching_tr_pfx sr atr tr = matching_tr_pfx sr atr tr'" apply (simp add: matching_tr_pfx_def list_all2_lengthD matching_tr_def) apply (intro conj_cong; simp?) apply (clarsimp simp: list_all2_conv_all_nth rel_prod_sel split_def) @@ -373,19 +344,19 @@ lemma list_all2_matching_tr_pfx: done lemma is_matching_fragment_list_all2: - "is_matching_fragment sr osr rvr tr' res s0 R s f - \ list_all2 (rel_prod (=) (\cs cs'. \as. sr as cs = sr as cs')) tr tr' - \ is_matching_fragment sr osr rvr tr res s0 R s f" + "\is_matching_fragment sr osr rvr tr' res s0 R s f; + list_all2 (rel_prod (=) (\cs cs'. \as. sr as cs = sr as cs')) tr tr'\ + \ is_matching_fragment sr osr rvr tr res s0 R s f" apply (clarsimp simp: is_matching_fragment_def) apply (subst(asm) list_all2_is_me[symmetric], assumption, simp) apply (simp add: list_all2_matching_tr_pfx list_all2_lengthD) done lemma pfx_refinement_use_rel_tr_refinement: - "rel_tr_refinement tr_r Q R False g g' - \ \s t t'. tr_r t t' \ sr s t = sr s t' - \ prefix_refinement sr isr osr rvr P Q' AR R f g' - \ prefix_refinement sr isr osr rvr P (\s0. Q and Q' s0) AR R f g" + "\rel_tr_refinement tr_r Q R False g g'; + \s t t'. tr_r t t' \ sr s t = sr s t'; + prefix_refinement sr isr osr rvr AR R P Q' f g'\ + \ prefix_refinement sr isr osr rvr AR R P (\s0. Q and Q' s0) f g" apply (subst prefix_refinement_def, clarsimp) apply (drule(3) rel_tr_refinementD, simp) apply clarsimp @@ -398,25 +369,21 @@ lemma pfx_refinement_use_rel_tr_refinement: done lemma pfx_refinement_use_rel_tr_refinement_equivp: - "rel_tr_refinement sr Q R False g g' - \ equivp sr - \ prefix_refinement sr isr osr rvr P Q' AR R f g' - \ prefix_refinement sr isr osr rvr P (\s0. Q and Q' s0) AR R f g" + "\rel_tr_refinement sr Q R False g g'; equivp sr; + prefix_refinement sr isr osr rvr AR R P Q' f g'\ + \ prefix_refinement sr isr osr rvr AR R P (\s0. Q and Q' s0) f g" apply (erule pfx_refinement_use_rel_tr_refinement, simp_all) apply (metis equivpE sympD transpD) done -definition - not_env_steps_first :: "('s, 'a) tmonad \ bool" -where +definition not_env_steps_first :: "('s, 'a) tmonad \ bool" where "not_env_steps_first f = (\tr res s. (tr, res) \ f s \ tr \ [] \ fst (last tr) = Me)" lemmas not_env_steps_firstD = not_env_steps_first_def[THEN iffD1, rule_format] lemma not_env_steps_first_bind: - "not_env_steps_first f - \ \x. not_env_steps_first (g x) - \ not_env_steps_first (do x \ f; g x od)" + "\not_env_steps_first f; \x. not_env_steps_first (g x)\ + \ not_env_steps_first (do x \ f; g x od)" apply (subst not_env_steps_first_def, clarsimp) apply (erule elem_bindE) apply (simp add: not_env_steps_firstD) @@ -426,7 +393,7 @@ lemma not_env_steps_first_bind: lemma not_env_steps_first_no_trace: "no_trace f \ not_env_steps_first f" - by (fastforce simp add: not_env_steps_first_def dest: no_trace_emp) + by (fastforce simp: not_env_steps_first_def dest: no_trace_emp) lemma not_env_steps_first_interference: "not_env_steps_first interference" @@ -443,18 +410,17 @@ lemma not_env_steps_first_repeat_n: lemma not_env_steps_first_repeat: "not_env_steps_first f \ not_env_steps_first (repeat f)" - by (simp add: repeat_def not_env_steps_first_bind - not_env_steps_first_repeat_n not_env_steps_first_simple) + by (simp add: repeat_def not_env_steps_first_bind not_env_steps_first_repeat_n + not_env_steps_first_simple) -lemmas not_env_steps_first_all = not_env_steps_first_interference - not_env_steps_first_bind[rule_format] not_env_steps_first_repeat_n - not_env_steps_first_repeat not_env_steps_first_simple +lemmas not_env_steps_first_all = + not_env_steps_first_interference not_env_steps_first_bind[rule_format] + not_env_steps_first_repeat_n not_env_steps_first_repeat not_env_steps_first_simple lemma rel_tr_refinement_bind_left_general: - "reflp sr - \ (\x. not_env_steps_first (h x)) \ (\s s' t. sr s s' \ R s t = R s' t) - \ rel_tr_refinement sr P R C f g - \ rel_tr_refinement sr P R C (f >>= (\x. h x)) (g >>= h)" + "\reflp sr; (\x. not_env_steps_first (h x)) \ (\s s' t. sr s s' \ R s t = R s' t); + rel_tr_refinement sr P R C f g\ + \ rel_tr_refinement sr P R C (f >>= (\x. h x)) (g >>= h)" apply (subst rel_tr_refinement_def, clarsimp) apply (erule elem_bindE) apply (drule(3) rel_tr_refinementD, simp) @@ -467,8 +433,7 @@ lemma rel_tr_refinement_bind_left_general: apply (simp add: image_def) apply (strengthen bexI[mk_strg I _ E] | simp)+ apply (simp add: list_all2_append rely_cond_append - list_all2_same reflpD[where R=sr] rel_prod_sel - split del: if_split) + list_all2_same reflpD[where R=sr] rel_prod_sel) apply (erule rely_cond_equiv_s) apply (erule disjE) apply (drule spec, drule(2) not_env_steps_firstD) @@ -477,15 +442,12 @@ lemma rel_tr_refinement_bind_left_general: split: if_split_asm) done -lemmas rel_tr_refinement_bind_left - = rel_tr_refinement_bind_left_general[OF _ disjI1] +lemmas rel_tr_refinement_bind_left = rel_tr_refinement_bind_left_general[OF _ disjI1] lemma rel_tr_refinement_bind_right_general: - "reflp sr - \ \x. rel_tr_refinement sr Q R C' (g x) (h x) - \ \\s0 s. (C \ s0 = s) \ P s\,\R\ f - \\_ _. True\,\\_ s0 s. (C' \ s0 = s) \ Q s\ - \ rel_tr_refinement sr P R C (f >>= (\x. g x)) (f >>= h)" + "\reflp sr; \x. rel_tr_refinement sr Q R C' (g x) (h x); + \\s0 s. (C \ s0 = s) \ P s\,\R\ f \\_ _. True\,\\_ s0 s. (C' \ s0 = s) \ Q s\\ + \ rel_tr_refinement sr P R C (f >>= (\x. g x)) (f >>= h)" apply (subst rel_tr_refinement_def, clarsimp) apply (erule elem_bindE) apply (clarsimp simp: bind_def) @@ -494,28 +456,25 @@ lemma rel_tr_refinement_bind_right_general: apply (clarsimp simp: rely_cond_append) apply (drule validI_D, erule(1) conjI, assumption+, clarsimp) apply (drule spec, drule(3) rel_tr_refinementD, - simp add: hd_append hd_map split: if_split_asm) + simp add: hd_append hd_map split: if_split_asm) apply (clarsimp simp: bind_def) apply (simp add: image_def) apply (strengthen bexI[mk_strg I _ E] | simp)+ apply (simp add: list_all2_append list_all2_lengthD) - apply (simp add: rely_cond_append list_all2_same reflpD[where R=sr] rel_prod_sel - split del: if_split) + apply (simp add: rely_cond_append list_all2_same reflpD[where R=sr] rel_prod_sel) done -lemmas validI_triv' = rg_weaken_pre[OF validI_triv, simplified] -lemmas rel_tr_refinement_bind_right - = rel_tr_refinement_bind_right_general[where C'=False, simplified] +lemmas rel_tr_refinement_bind_right = + rel_tr_refinement_bind_right_general[where C'=False, simplified] lemma rel_tr_refinement_comm_repeat_n[simplified K_bind_def]: - "equivp sr - \ rel_tr_refinement sr P R C (do f; g od) (do x \ g; f; return x od) - \ not_env_steps_first f \ (\s s' t. sr s s' \ R s t = R s' t) - \ \\s0 s. (C \ s0 = s) \ P s\,\R\ f - \\_ _. True\,\\_ s0 s. (C \ s0 = s) \ P s\ - \ rel_tr_refinement sr P R C - (do repeat_n n f; g od) - (do x \ g; repeat_n n f; return x od)" + "\equivp sr; + rel_tr_refinement sr P R C (do f; g od) (do x \ g; f; return x od); + not_env_steps_first f \ (\s s' t. sr s s' \ R s t = R s' t); + \\s0 s. (C \ s0 = s) \ P s\,\R\ f \\_ _. True\,\\_ s0 s. (C \ s0 = s) \ P s\\ + \ rel_tr_refinement sr P R C + (do repeat_n n f; g od) + (do x \ g; repeat_n n f; return x od)" apply (induct n) apply simp apply (rule rel_tr_refinement_refl) @@ -528,21 +487,20 @@ lemma rel_tr_refinement_comm_repeat_n[simplified K_bind_def]: apply assumption apply (wpsimp wp: repeat_n_validI) apply (drule_tac h="\x. do f; return x od" - in rel_tr_refinement_bind_left_general[rotated 2]) + in rel_tr_refinement_bind_left_general[rotated 2]) apply (metis equivpE) apply (auto intro!: not_env_steps_first_all)[1] apply (simp add: bind_assoc) done lemma rel_tr_refinement_comm_repeat[simplified K_bind_def]: - "equivp sr - \ rel_tr_refinement sr P R C (do f; g od) (do x \ g; f; return x od) - \ not_env_steps_first f \ (\s s' t. sr s s' \ R s t = R s' t) - \ \\s0 s. (C \ s0 = s) \ P s\,\R\ f - \\_ _. True\,\\_ s0 s. (C \ s0 = s) \ P s\ - \ rel_tr_refinement sr P R C - (do repeat f; g od) - (do x \ g; repeat f; return x od)" + "\equivp sr; + rel_tr_refinement sr P R C (do f; g od) (do x \ g; f; return x od); + not_env_steps_first f \ (\s s' t. sr s s' \ R s t = R s' t); + \\s0 s. (C \ s0 = s) \ P s\,\R\ f \\_ _. True\,\\_ s0 s. (C \ s0 = s) \ P s\\ + \ rel_tr_refinement sr P R C + (do repeat f; g od) + (do x \ g; repeat f; return x od)" apply (simp add: repeat_def select_early bind_assoc) apply (rule rel_tr_refinement_bind_right_general[rule_format]) apply (metis equivpE) @@ -551,14 +509,13 @@ lemma rel_tr_refinement_comm_repeat[simplified K_bind_def]: done lemma rel_tr_refinement_rev_comm_repeat_n[simplified K_bind_def]: - "equivp sr - \ rel_tr_refinement sr P R C (do x \ g; f; return x od) (do f; g od) - \ not_env_steps_first f \ (\s s' t. sr s s' \ R s t = R s' t) - \ \\s0 s. (C \ s0 = s) \ P s\,\R\ f - \\_ _. True\,\\_ s0 s. (C \ s0 = s) \ P s\ - \ rel_tr_refinement sr P R C - (do x \ g; repeat_n n f; return x od) - (do repeat_n n f; g od)" + "\equivp sr; + rel_tr_refinement sr P R C (do x \ g; f; return x od) (do f; g od); + not_env_steps_first f \ (\s s' t. sr s s' \ R s t = R s' t); + \\s0 s. (C \ s0 = s) \ P s\,\R\ f \\_ _. True\,\\_ s0 s. (C \ s0 = s) \ P s\\ + \ rel_tr_refinement sr P R C + (do x \ g; repeat_n n f; return x od) + (do repeat_n n f; g od)" apply (induct n) apply simp apply (rule rel_tr_refinement_refl) @@ -572,21 +529,20 @@ lemma rel_tr_refinement_rev_comm_repeat_n[simplified K_bind_def]: apply assumption apply (wpsimp wp: repeat_n_validI) apply (drule_tac h="\x. do f; return x od" - in rel_tr_refinement_bind_left_general[rotated 2]) + in rel_tr_refinement_bind_left_general[rotated 2]) apply (metis equivpE) apply (auto intro!: not_env_steps_first_all)[1] apply (simp add: bind_assoc) done lemma rel_tr_refinement_rev_comm_repeat[simplified K_bind_def]: - "equivp sr - \ rel_tr_refinement sr P R C (do x \ g; f; return x od) (do f; g od) - \ not_env_steps_first f \ (\s s' t. sr s s' \ R s t = R s' t) - \ \\s0 s. (C \ s0 = s) \ P s\,\R\ f - \\_ _. True\,\\_ s0 s. (C \ s0 = s) \ P s\ - \ rel_tr_refinement sr P R C - (do x \ g; repeat f; return x od) - (do repeat f; g od)" + "\equivp sr; + rel_tr_refinement sr P R C (do x \ g; f; return x od) (do f; g od); + not_env_steps_first f \ (\s s' t. sr s s' \ R s t = R s' t); + \\s0 s. (C \ s0 = s) \ P s\,\R\ f \\_ _. True\,\\_ s0 s. (C \ s0 = s) \ P s\\ + \ rel_tr_refinement sr P R C + (do x \ g; repeat f; return x od) + (do repeat f; g od)" apply (simp add: repeat_def select_early bind_assoc) apply (rule rel_tr_refinement_bind_right_general[rule_format]) apply (metis equivpE) @@ -599,16 +555,18 @@ lemma alternative_distrib_lhs_bind: by (simp add: bind_def alternative_def) lemma shuttle_modify_commit_step[simplified K_bind_def]: - "\s. sr s (f s) \ rel_tr_refinement sr P R C - (do x \ commit_step; modify f od) (do x \ modify f; commit_step od)" + "\s. sr s (f s) + \ rel_tr_refinement sr P R C + (do x \ commit_step; modify f od) (do x \ modify f; commit_step od)" apply (simp add: rel_tr_refinement_def commit_step_def put_trace_elem_def bind_def get_def return_def modify_def put_def) apply (simp add: rely_cond_def) done lemma shuttle_gets_commit_step[simplified K_bind_def]: - "reflp sr \ rel_tr_refinement sr P R C - (do x \ commit_step; gets f od) (do x \ gets f; commit_step; return x od)" + "reflp sr + \ rel_tr_refinement sr P R C + (do x \ commit_step; gets f od) (do x \ gets f; commit_step; return x od)" apply (simp add: rel_tr_refinement_def commit_step_def put_trace_elem_def bind_def get_def return_def gets_def) apply (simp add: rely_cond_def reflpD) @@ -619,9 +577,9 @@ lemma shuttle_modify_interference[simplified K_bind_def]: and P_stable: "\s t. P s \ R s t \ P t" and R: "\s0 s. P s0 \ R s0 s \ R (f s0) (f s)" shows - "rel_tr_refinement sr P R C - (do interference; modify f od) - (do modify f; interference od)" + "rel_tr_refinement sr P R C + (do interference; modify f od) + (do modify f; interference od)" proof - have list_all2_map: "\xs. list_all2 (rel_prod (=) sr) xs (map (apsnd f) xs)" @@ -642,8 +600,7 @@ proof - apply (clarsimp simp: rel_tr_refinement_def) apply (clarsimp simp: bind_def commit_step_def get_def return_def put_trace_elem_def modify_def put_def - interference_def env_steps_def select_def - ) + interference_def env_steps_def select_def) apply (erule disjE; clarsimp) apply (simp add: put_trace_eq_drop) apply (clarsimp; split if_split_asm) @@ -676,24 +633,23 @@ lemma rshuttle_modify_interference[simplified K_bind_def]: and P_stable: "\s t. P s \ R s t \ P t" and R: "\s0 s. R (f s0) s \ P s0 \ (\s_pre. s = f s_pre \ R s0 s_pre)" shows - "rel_tr_refinement sr P R C - (do modify f; interference od) - (do interference; modify f od)" + "rel_tr_refinement sr P R C + (do modify f; interference od) + (do interference; modify f od)" proof - - have last_st_tr: "\s ss. last_st_tr (map (Pair Env \ f) ss) (f s) - = f (last_st_tr (map (Pair Env) ss) s)" + have last_st_tr: + "\s ss. last_st_tr (map (Pair Env \ f) ss) (f s) = f (last_st_tr (map (Pair Env) ss) s)" by (simp add: last_st_tr_def hd_append hd_map) { fix s ss s' - have rely_cond_P_stable[rule_format]: - "P s \ rely_cond R s (map (Pair Env) ss) - \ s' \ set (ss @ [s]) \ P s'" - apply (induct ss arbitrary: s' rule: list.induct) - apply simp - apply clarsimp - apply (clarsimp simp: rely_cond_Cons_eq P_stable) - apply (erule P_stable[rule_format, rotated]) - apply (case_tac x2; simp add: last_st_tr_in_set) - done + have rely_cond_P_stable[rule_format]: + "P s \ rely_cond R s (map (Pair Env) ss) \ s' \ set (ss @ [s]) \ P s'" + apply (induct ss arbitrary: s' rule: list.induct) + apply simp + apply clarsimp + apply (clarsimp simp: rely_cond_Cons_eq P_stable) + apply (erule P_stable[rule_format, rotated]) + apply (case_tac x2; simp add: last_st_tr_in_set) + done } note rely_cond_P_stable = this have rely_cond_ex: "\s ss. rely_cond R (f s) (map (Pair Env) ss) \ P s @@ -710,8 +666,7 @@ proof - apply (clarsimp simp: rel_tr_refinement_def) apply (clarsimp simp: bind_def commit_step_def get_def return_def put_trace_elem_def modify_def put_def - interference_def env_steps_def select_def - ) + interference_def env_steps_def select_def) apply (erule disjE; clarsimp) apply (clarsimp simp: put_trace_eq_drop) apply (split if_split_asm) @@ -739,9 +694,9 @@ proof - qed lemma shuttle_gets_env_step[simplified K_bind_def]: - "reflp sr \ \s t. P s \ R s t \ f s = f t - \ rel_tr_refinement sr P R True - (do x \ env_step; gets f od) (do x \ gets f; env_step; return x od)" + "\reflp sr; \s t. P s \ R s t \ f s = f t\ + \ rel_tr_refinement sr P R True + (do x \ env_step; gets f od) (do x \ gets f; env_step; return x od)" apply (simp add: rel_tr_refinement_def env_step_def select_def put_trace_elem_def bind_def get_def return_def gets_def put_def) apply (clarsimp simp: rely_cond_def reflpD) @@ -755,11 +710,10 @@ lemma env_step_twp[wp]: done lemma shuttle_modify_interferences[simplified K_bind_def]: - "equivp sr \ \s. sr s (f s) \ \s t. P s \ R s t \ R (f s) (f t) - \ not_env_steps_first g - \ \s t. P s \ R\<^sup>*\<^sup>* s t \ P t - \ rel_tr_refinement sr P R C - (do x \ interferences; modify f; g od) (do x \ modify f; interferences; g od)" + "\equivp sr; \s. sr s (f s); \s t. P s \ R s t \ R (f s) (f t); + not_env_steps_first g; \s t. P s \ R\<^sup>*\<^sup>* s t \ P t\ + \ rel_tr_refinement sr P R C + (do x \ interferences; modify f; g od) (do x \ modify f; interferences; g od)" apply (simp only: bind_assoc[symmetric]) apply (rule rel_tr_refinement_bind_left_general) apply (metis equivpE) @@ -772,17 +726,16 @@ lemma shuttle_modify_interferences[simplified K_bind_def]: apply wpsimp done -lemmas shuttle_modify_interferences_flat - = shuttle_modify_interferences[where g="return ()", simplified] +lemmas shuttle_modify_interferences_flat = + shuttle_modify_interferences[where g="return ()", simplified] lemma rshuttle_modify_interferences[simplified K_bind_def]: - "equivp sr \ \s. sr (f s) s - \ \s0 s. R (f s0) s \ P s0 \ (\s_pre. s = f s_pre \ R s0 s_pre) - \ not_env_steps_first g - \ \s t. P s \ R\<^sup>*\<^sup>* s t \ P t - \ rel_tr_refinement sr P R C - (do x \ modify f; interferences; g od) - (do x \ interferences; modify f; g od)" + "\equivp sr; \s. sr (f s) s; + \s0 s. R (f s0) s \ P s0 \ (\s_pre. s = f s_pre \ R s0 s_pre); + not_env_steps_first g; \s t. P s \ R\<^sup>*\<^sup>* s t \ P t\ + \ rel_tr_refinement sr P R C + (do x \ modify f; interferences; g od) + (do x \ interferences; modify f; g od)" apply (simp only: bind_assoc[symmetric]) apply (rule rel_tr_refinement_bind_left_general) apply (metis equivpE) @@ -796,11 +749,10 @@ lemma rshuttle_modify_interferences[simplified K_bind_def]: done lemma shuttle_gets_interference[simplified K_bind_def]: - "equivp sr \ \s t. P s \ R s t \ f s = f t - \ (\s s' t. sr s s' \ R s t = R s' t) - \ \s t. P s \ R\<^sup>*\<^sup>* s t \ P t - \ rel_tr_refinement sr P R C - (do x \ interference; gets f od) (do x \ gets f; interference; return x od)" + "\equivp sr; \s t. P s \ R s t \ f s = f t; + \s s' t. sr s s' \ R s t = R s' t; \s t. P s \ R\<^sup>*\<^sup>* s t \ P t\ + \ rel_tr_refinement sr P R C + (do x \ interference; gets f od) (do x \ gets f; interference; return x od)" apply (simp add: interference_def bind_assoc env_steps_repeat) apply (rule rel_tr_refinement_trans) apply (metis equivpE) @@ -816,19 +768,18 @@ lemma shuttle_gets_interference[simplified K_bind_def]: apply (clarsimp simp: r_into_rtranclp) apply (simp add: commit_step_def, wp put_trace_elem_twp) apply (simp add: drop_Cons' guar_cond_def) - apply (rule shuttle_gets_commit_step[THEN - rel_tr_refinement_bind_left_general[rotated -1], simplified bind_assoc return_bind]) + apply (rule shuttle_gets_commit_step[THEN rel_tr_refinement_bind_left_general[rotated -1], + simplified bind_assoc return_bind]) apply (metis equivpE) apply (metis equivpE) apply simp done lemma shuttle_gets_interferences[simplified K_bind_def]: - "equivp sr \ \s t. P s \ R s t \ f s = f t - \ (\s s' t. sr s s' \ R s t = R s' t) - \ \s t. P s \ R\<^sup>*\<^sup>* s t \ P t - \ rel_tr_refinement sr P R C - (do interferences; x \ gets f; g x od) (do x \ gets f; interferences; g x od)" + "\equivp sr; \s t. P s \ R s t \ f s = f t; + \s s' t. sr s s' \ R s t = R s' t; \s t. P s \ R\<^sup>*\<^sup>* s t \ P t\ + \ rel_tr_refinement sr P R C + (do interferences; x \ gets f; g x od) (do x \ gets f; interferences; g x od)" apply (rule rel_tr_refinement_trans) apply (metis equivpE) apply (simp only: bind_assoc[symmetric] K_bind_def) @@ -844,32 +795,24 @@ lemma shuttle_gets_interferences[simplified K_bind_def]: apply (metis equivpE) done -lemmas shuttle_gets_interferences_flat - = shuttle_gets_interferences[where g = return, simplified] +lemmas shuttle_gets_interferences_flat = shuttle_gets_interferences[where g = return, simplified] -definition - adjust_tr_relation :: "('t \ 't \ bool) \ ('s \ 't \ bool) \ bool" -where +definition adjust_tr_relation :: "('t \ 't \ bool) \ ('s \ 't \ bool) \ bool" where "adjust_tr_relation tr_r sr = (equivp tr_r \ (\s t t'. tr_r t t' \ sr s t = sr s t'))" lemma adjust_tr_relation_equivp: - "equivp sr - \ adjust_tr_relation sr sr" + "equivp sr \ adjust_tr_relation sr sr" apply (simp add: adjust_tr_relation_def) apply (metis equivpE sympD transpD) done lemma prefix_refinement_i_modify_split: - "adjust_tr_relation tr_r sr - \ \s t. isr s t \ P s \ Q t \ intsr (f s) (g t) - \ \s. tr_r s (g s) - \ \s t. R s t \ R (g s) (g t) - \ not_env_steps_first b - \ prefix_refinement sr intsr osr rvr' P' Q' AR R - d (do x \ interferences; b od) - \ prefix_refinement sr isr osr rvr' (\s0 s. P s \ P' s0 (f s)) (\s0 s. Q s \ Q' s0 (g s)) AR R - (do z \ modify f; d od) - (do x \ interferences; y \ modify g; b od)" + "\adjust_tr_relation tr_r sr; \s t. \isr s t; P s; Q t\ \ intsr (f s) (g t); + \s. tr_r s (g s); \s t. R s t \ R (g s) (g t); not_env_steps_first b; + prefix_refinement sr intsr osr rvr' AR R P' Q' d (do x \ interferences; b od)\ + \ prefix_refinement sr isr osr rvr' AR R (\s0 s. P s \ P' s0 (f s)) (\s0 s. Q s \ Q' s0 (g s)) + (do z \ modify f; d od) + (do x \ interferences; y \ modify g; b od)" apply (clarsimp simp: adjust_tr_relation_def) apply (rule prefix_refinement_weaken_pre) apply (rule pfx_refinement_use_rel_tr_refinement[where tr_r=tr_r and Q=\]) diff --git a/lib/concurrency/Prefix_Refinement.thy b/lib/concurrency/Prefix_Refinement.thy index 3fe4adbd07..79a4a77129 100644 --- a/lib/concurrency/Prefix_Refinement.thy +++ b/lib/concurrency/Prefix_Refinement.thy @@ -1,4 +1,5 @@ (* + * Copyright 2024, Proofcraft Pty Ltd * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) * * SPDX-License-Identifier: BSD-2-Clause @@ -6,96 +7,84 @@ theory Prefix_Refinement imports + Monads.Trace_Empty_Fail Triv_Refinement + Monads.Trace_Reader_Option + Monads.Trace_Sat begin -section \Definition of prefix fragment refinement.\ +section \Definition of prefix fragment refinement\ text \ -This is a notion of refinement/simulation making use of prefix closure. -For a concrete program to refine an abstract program, then for every -trace of the concrete program there must exist a well-formed fragment -of the abstract program that matches (according to the simulation -relation) but which leaves enough decisions available to the abstract -environment to permit parallel composition. -\ + This is a notion of refinement/simulation making use of prefix closure. + For a concrete program to refine an abstract program, for every + trace of the concrete program there must exist a well-formed fragment + of the abstract program that matches (according to the simulation + relation) but which leaves enough decisions available to the abstract + environment to permit parallel composition.\ text \ -Fragments must be self-closed, or enabled. Certain incomplete traces -must be possible to extend by a program step. -\ -definition - self_closed :: "((tmid \ 's) list \ bool) \ 's \ ('s, 'a) tmonad \ bool" -where - "self_closed cond s f = (\xs. (xs, Incomplete) \ f s - \ cond xs \ (\s'. (Me, s') # xs \ fst ` f s))" + Fragments must be self-closed, or enabled. Certain incomplete traces + must be possible to extend by a program step.\ +definition self_closed :: "((tmid \ 's) list \ bool) \ 's \ ('s, 'a) tmonad \ bool" where + "self_closed cond s f = + (\xs. (xs, Incomplete) \ f s \ cond xs \ (\s'. (Me, s') # xs \ fst ` f s))" lemmas self_closedD = self_closed_def[THEN iffD1, rule_format] text \ -Fragments must be environment-closed. Certain incomplete traces -must be possible to extend by any environment step that is -compatible with some condition. -\ -definition - env_closed :: "((tmid \ 's) list \ 's \ bool) \ 's \ ('s, 'a) tmonad \ bool" -where - "env_closed cond s f = (\xs s'. (xs, Incomplete) \ f s - \ cond xs s' \ ((Env, s') # xs) \ fst ` f s)" + Fragments must be environment-closed. Certain incomplete traces + must be possible to extend by any environment step that is + compatible with some condition.\ +definition env_closed :: "((tmid \ 's) list \ 's \ bool) \ 's \ ('s, 'a) tmonad \ bool" where + "env_closed cond s f = + (\xs s'. (xs, Incomplete) \ f s \ cond xs s' \ ((Env, s') # xs) \ fst ` f s)" lemmas env_closedD = env_closed_def[THEN iffD1, rule_format] lemma env_closed_strengthen_cond: - "env_closed P s f - \ (\xs s. Q xs s \ P xs s) - \ env_closed Q s f" + "\env_closed P s f; \xs s. Q xs s \ P xs s\ \ env_closed Q s f" by (simp add: env_closed_def) -text \ -Two traces match according to some state relation if they match at every step. -\ -definition - matching_tr :: "('s \ 't \ bool) \ (tmid \ 's) list \ (tmid \ 't) list \ bool" -where +text \Two traces match according to some state relation if they match at every step.\ +definition matching_tr :: "('s \ 't \ bool) \ (tmid \ 's) list \ (tmid \ 't) list \ bool" where "matching_tr sr = list_all2 (\(aid, as) (cid, cs). aid = cid \ sr as cs)" -definition - matching_tr_pfx :: "('s \ 't \ bool) \ (tmid \ 's) list \ (tmid \ 't) list \ bool" -where - "matching_tr_pfx sr atr ctr = (length atr \ length ctr - \ matching_tr sr (rev atr) (take (length atr) (rev ctr)))" +definition matching_tr_pfx :: + "('s \ 't \ bool) \ (tmid \ 's) list \ (tmid \ 't) list \ bool" + where + "matching_tr_pfx sr atr ctr = + (length atr \ length ctr \ matching_tr sr (rev atr) (take (length atr) (rev ctr)))" abbreviation "matching_tr_tmids_pfx \ matching_tr_pfx (\_ _. True)" -abbreviation(input) +abbreviation (input) "matching_self_cond ctr \ (\xs. length xs < length ctr \ fst (rev ctr ! length xs) = Me)" -abbreviation(input) - "matching_env_cond sr ctr s0 R \ (\xs s. matching_tr_pfx sr ((Env, s) # xs) ctr - \ rely_cond R s0 ((Env, s) # xs))" +abbreviation (input) + "matching_env_cond sr ctr s0 R \ + (\xs s. matching_tr_pfx sr ((Env, s) # xs) ctr \ rely_cond R s0 ((Env, s) # xs))" text \ -The collection of properties a fragment must have to match some concrete -trace. It must be prefix, self and environment closed, nonempty, and all -outcomes must be matching. The outcomes (trace and result) must match -the rely condition, the concrete trace (or a prefix), and must either be -a matching result or @{term Incomplete} if a prefix. -\ -definition - is_matching_fragment :: "('s \ 't \ bool) \ ('s \ 't \ bool) - \ ('a \ 'b \ bool) \ (tmid \ 't) list \ ('t, 'b) tmres - \ 's \ ('s \ 's \ bool) \ 's \ ('s, 'a) tmonad \ bool" -where + The collection of properties a fragment must have to match some concrete + trace. It must be prefix, self and environment closed, nonempty, and all + outcomes must be matching. The outcomes (trace and result) must match + the rely condition, the concrete trace (or a prefix), and must either be + a matching result or @{term Incomplete} if a prefix.\ +definition is_matching_fragment :: + "('s \ 't \ bool) \ ('s \ 't \ bool) \ ('a \ 'b \ bool) \ (tmid \ 't) list \ + ('t, 'b) tmres \ 's \ ('s \ 's \ bool) \ 's \ ('s, 'a) tmonad \ bool" + where "is_matching_fragment sr osr rvr ctr cres s0 R s f - = ((prefix_closed f - \ self_closed (matching_self_cond ctr) s f - \ env_closed (matching_env_cond sr ctr s0 R) s f) - \ (f s \ {}) + = ((prefix_closed f + \ self_closed (matching_self_cond ctr) s f + \ env_closed (matching_env_cond sr ctr s0 R) s f) + \ f s \ {} \ (\(tr, res) \ f s. rely_cond R s0 tr - \ matching_tr_pfx sr tr ctr - \ (length tr < length ctr \ res = Incomplete) - \ (length tr = length ctr \ rel_tmres osr rvr res cres)))" + \ matching_tr_pfx sr tr ctr + \ (length tr < length ctr \ res = Incomplete) + \ (length tr = length ctr \ rel_tmres osr rvr res cres)))" lemmas is_matching_fragmentD = is_matching_fragment_def[THEN iffD1, rule_format] @@ -106,38 +95,50 @@ lemmas is_matching_fragment_env_closed = is_matching_fragment_wf[THEN conjunct2, lemmas is_matching_fragment_defD = is_matching_fragmentD[THEN conjunct2, THEN conjunct1, rule_format] lemmas is_matching_fragment_trD - = is_matching_fragmentD[THEN conjunct2, THEN conjunct2, - rule_format, where x="(tr, res)" for tr res, simplified, rule_format] + = is_matching_fragmentD[THEN conjunct2, THEN conjunct2, rule_format, + where x="(tr, res)" for tr res, simplified, rule_format] text \ -Prefix fragment refinement. Given the initial conditions, every concrete outcome -(trace and result) must have a matching fragment which is a simple refinement of -the abstract program. -\ -definition - prefix_refinement :: "('s \ 't \ bool) \ ('s \ 't \ bool) \ ('s \ 't \ bool) - \ ('a \ 'b \ bool) \ ('s \ 's \ bool) \ ('t \ 't \ bool) - \ ('s \ 's \ bool) \ ('t \ 't \ bool) - \ ('s, 'a) tmonad \ ('t, 'b) tmonad \ bool" -where - "prefix_refinement sr isr osr rvr P Q AR R aprog cprog + Prefix fragment refinement. Given the initial conditions, every concrete outcome + (trace and result) must have a matching fragment which is a simple refinement of + the abstract program.\ +\ \FIXME: do we want to be able to assume non-failure of the abstract program.\ +\ \FIXME: should we have an option for showing non-failure of the concrete program.\ +\ \FIXME: corres uses a set for the state relation, this uses a predicate. Do we care?\ +definition prefix_refinement :: + "('s \ 't \ bool) \ ('s \ 't \ bool) \ ('s \ 't \ bool) \ ('a \ 'b \ bool) \ + ('s \ 's \ bool) \ ('t \ 't \ bool) \ ('s \ 's \ bool) \ ('t \ 't \ bool) \ + ('s, 'a) tmonad \ ('t, 'b) tmonad \ bool" + where + "prefix_refinement sr isr osr rvr AR R P Q aprog cprog = (\s s0 t0 t. isr s t \ P s0 s \ sr s0 t0 \ Q t0 t - \ (\(ctr, cres) \ cprog t. - rely_cond R t0 ctr \ (\f. is_matching_fragment sr osr rvr ctr cres s0 AR s f - \ triv_refinement aprog f)))" + \ (\(ctr, cres) \ cprog t. + rely_cond R t0 ctr \ + (\f. is_matching_fragment sr osr rvr ctr cres s0 AR s f + \ triv_refinement aprog f)))" abbreviation - "pfx_refn sr rvr P \ prefix_refinement sr sr sr rvr P" + "pfx_refn sr \ prefix_refinement sr sr sr" + +section \Base case facts about refinement\ lemmas prefix_refinementD = prefix_refinement_def[THEN iffD1, rule_format] lemmas split_iffD1 = Product_Type.split[THEN iffD1] lemmas pfx_refnD = prefix_refinementD lemmas pfx_refnD2 = pfx_refnD[THEN split_iffD1[where a=tr and b=res for tr res], rule_format] +lemma prefix_refinement_False: + "prefix_refinement sr isr osr rvr AR R P \\ f g" + by (clarsimp simp: prefix_refinement_def) + +lemma prefix_refinement_False': + "prefix_refinement sr isr osr rvr AR R \\ Q f g" + by (clarsimp simp: prefix_refinement_def) + lemma matching_tr_pfx_aCons: "matching_tr_pfx sr ((tmid, s) # atr) ctr = (\s'. length atr < length ctr \ rev ctr ! length atr = (tmid, s') - \ sr s s' \ matching_tr_pfx sr atr ctr)" + \ sr s s' \ matching_tr_pfx sr atr ctr)" apply (simp add: matching_tr_pfx_def matching_tr_def Suc_le_eq list_all2_conv_all_nth less_Suc_eq all_conj_distrib) apply (simp add: nth_append prod_eq_iff) @@ -145,35 +146,168 @@ lemma matching_tr_pfx_aCons: done lemma rely_cond_hd: - "rely_cond R s0 xs \ xs \ [] - \ fst (hd xs) = Env \ R (last_st_tr (tl xs) s0) (snd (hd xs))" + "\rely_cond R s0 xs; xs \ []\ + \ fst (hd xs) = Env \ R (last_st_tr (tl xs) s0) (snd (hd xs))" by (clarsimp simp: rely_cond_def neq_Nil_conv trace_steps_append split: if_split_asm) -lemma diff_Suc_eq_if: - "(Suc n - m) = (if m \ n then Suc (n - m) else 0)" - by auto - lemma rely_cond_nth: - "rely_cond R s0 tr \ n < length tr - \ fst (rev tr ! n) = Env \ R ((if n = 0 then s0 else snd (rev tr ! (n - 1)))) (snd (rev tr ! n))" + "\rely_cond R s0 tr; n < length tr\ + \ fst (rev tr ! n) = Env \ R ((if n = 0 then s0 else snd (rev tr ! (n - 1)))) (snd (rev tr ! n))" by (simp add: rely_cond_def trace_steps_rev_drop_nth[where n=0, simplified]) lemma is_matching_fragment_Nil: - "is_matching_fragment sr osr rvr ctr cres s0 R s f - \ [] \ fst ` f s" + "is_matching_fragment sr osr rvr ctr cres s0 R s f \ [] \ fst ` f s" apply (clarsimp simp: is_matching_fragment_def) apply (clarsimp simp only: set_eq_iff empty_iff simp_thms not_all) apply (drule(1) prefix_closed_drop[where tr=tr and n="length tr" for tr]) - apply (clarsimp simp add: in_fst_snd_image) + apply (clarsimp simp: in_fst_snd_image) + done + +\ \FIXME: it would be good to show this but it needs more thought to determine how best to handle + the case where the concrete function has failing traces that do not satisy the rely. +lemma prefix_refinement_propagate_no_fail: + "\prefix_refinement sr isr osr rvr AR R P Q f f'; + \s0. no_fail (P s0) f; \t0 t. Q t0 t \ (\s0 s. P s0 s \ sr s0 t0 \ isr s t)\ + \ \t0. no_fail (Q t0) f'" + apply (clarsimp simp: prefix_refinement_def no_fail_def failed_def) + apply (erule allE, erule allE, erule (1) impE) + apply clarsimp + apply ((drule spec)+, (drule (1) mp)+) + apply (drule (1) bspec, clarsimp) + oops\ + +\ \FIXME: this needs some sort of assumption saying that the rely R does not lead to an empty set + of results. +lemma prefix_refinement_serial: + "\prefix_refinement sr isr osr rvr AR R P Q f f'; empty_fail f'; no_fail Q' f'; + \t0 t. Q t0 t \ Q' t\ + \ \s0 s. (\t0 t. isr s t \ P s0 s \ sr s0 t0 \ Q t0 t) \ mres (f s) \ {}" + apply (clarsimp simp: prefix_refinement_def empty_fail_def) + apply (drule no_failD, fastforce) + apply (drule_tac x=t in spec, drule mp; simp?) + apply ((drule spec)+, (drule (1) mp)+) + apply (clarsimp simp: mres_def vimage_def) + apply (drule (1) bspec) + apply clarsimp + oops\ + +lemma is_matching_fragment_no_trace: + "is_matching_fragment sr osr rvr [] cres s0 R s (\s. {([], ares s)}) + = rel_tmres osr rvr (ares s) cres" + by (simp add: is_matching_fragment_def prefix_closed_def self_closed_def env_closed_def + matching_tr_pfx_def matching_tr_def) + +\ \Singleton trace monads must have an empty trace to be prefix_closed\ +lemma prefix_refinement_singleton: + "prefix_refinement sr isr osr rvr AR R P Q (\s. {([], res s)}) (\s. {([], cres s)}) + = (\s0 s t0 t. isr s t \ P s0 s \ sr s0 t0 \ Q t0 t + \ rel_tmres osr rvr (res s) (cres t))" + (is "prefix_refinement _ _ _ _ _ _ _ _ ?f _ = _") + apply (rule iffI; clarsimp simp: prefix_refinement_def) + apply ((drule spec)+, (drule (1) mp)+) + apply clarsimp + apply (subgoal_tac "f s = ?f s") + prefer 2 + apply (clarsimp simp: triv_refinement_def fun_eq_iff) + apply (drule_tac x=s in spec, drule subset_singletonD) + apply (clarsimp simp: is_matching_fragment_def) + apply (drule_tac tr="[]" and res="res s" in is_matching_fragment_trD) + apply clarsimp + apply clarsimp + apply ((drule spec)+, (drule (1) mp)+) + apply (rule_tac x="?f" in exI) + apply (clarsimp simp: is_matching_fragment_no_trace) + done + +lemma prefix_refinement_no_trace: + "no_trace g + \ prefix_refinement sr isr osr rvr AR R P Q f g + = (\s0 s t0 t. isr s t \ P s0 s \ sr s0 t0 \ Q t0 t + \ (\cres \ snd ` (g t). \(tr, res) \ (f s). tr = [] \ rel_tmres osr rvr res cres))" + apply (rule iffI; clarsimp simp: prefix_refinement_def; drule (1) no_traceD; clarsimp) + apply ((drule spec)+, (drule (1) mp)+) + apply (drule (1) bspec, clarsimp) + apply (frule_tac s=s in is_matching_fragment_defD) + apply (clarsimp simp: ex_in_conv[symmetric]) + apply (drule (1) is_matching_fragment_trD) + apply (clarsimp simp: matching_tr_pfx_def matching_tr_def) + apply (drule (1) triv_refinement_elemD) + apply (rule_tac x= "([], ba)" in bexI; clarsimp) + apply ((drule spec)+, (drule (1) mp)+) + apply (drule (1) bspec, clarsimp) + apply (rename_tac gres fres) + apply (rule_tac x="\s'. if s'=s then {([],fres)} else {}" in exI) + apply (auto simp: is_matching_fragment_def prefix_closed_def self_closed_def env_closed_def + matching_tr_pfx_def matching_tr_def triv_refinement_def) + done + +lemma prefix_refinement_no_trace': + "\no_trace g; + \s0 s t0 t. \isr s t; P s0 s; sr s0 t0; Q t0 t\ + \ (\cres \ snd ` (g t). \(tr, res) \ (f s). tr = [] \ rel_tmres osr rvr res cres)\ + \ prefix_refinement sr isr osr rvr AR R P Q f g" + by (simp add: prefix_refinement_no_trace) + +section \Building blocks\ +text \Prefix refinement rules for basic constructs.\ + +lemma default_prefix_refinement_ex: + "is_matching_fragment sr osr rvr ctr cres s0 R s + (\s. aprog s \ ({tr'. length tr' \ length ctr} \ UNIV)) + \ \f. is_matching_fragment sr osr rvr ctr cres s0 R s f \ triv_refinement aprog f" + apply (intro exI conjI, assumption) + apply (simp add: triv_refinement_def) + done + +lemma default_prefix_refinement_ex_match_iosr_R: + "is_matching_fragment sr osr rvr ctr cres s0 R s + (rely (\s. aprog s \ ({tr'. matching_tr_pfx iosr tr' ctr} \ UNIV)) R s0) + \ \f. is_matching_fragment sr osr rvr ctr cres s0 R s f \ triv_refinement aprog f" + apply (intro exI conjI, assumption) + apply (clarsimp simp: triv_refinement_def rely_def) + done + +lemma prefix_refinement_return_imp: + "\\s0 s t0 t. \P s0 s; Q t0 t; isr s t\ \ rvr rv rv' \ osr s t\ + \ prefix_refinement sr isr osr rvr AR R P Q (return rv) (return rv')" + apply (clarsimp simp: prefix_refinement_def) + apply (rule default_prefix_refinement_ex) + apply (clarsimp simp: return_def is_matching_fragment_no_trace) + done + +lemma prefix_refinement_get_imp: + "\\s0 s t0 t. \P s0 s; Q t0 t; isr s t\ \ rvr s t \ osr s t\ + \ prefix_refinement sr isr osr rvr AR R P Q get get" + apply (clarsimp simp: prefix_refinement_def) + apply (rule default_prefix_refinement_ex) + apply (clarsimp simp: get_def is_matching_fragment_no_trace) + done + +lemma prefix_refinement_gets_imp: + "\\s0 s t0 t. \P s0 s; Q t0 t; isr s t\ \ rvr (f s) (g t) \ osr s t\ + \ prefix_refinement sr isr osr rvr AR R P Q (gets f) (gets g)" + apply (clarsimp simp: prefix_refinement_def) + apply (rule default_prefix_refinement_ex) + apply (clarsimp simp: simpler_gets_def is_matching_fragment_no_trace) done +lemma prefix_refinement_returnOk_imp: + "\\s0 s t0 t. \P s0 s; Q t0 t; isr s t\ \ rvr (Inr rv) (Inr rv') \ osr s t\ + \ prefix_refinement sr isr osr rvr AR R P Q (returnOk rv) (returnOk rv')" + by (simp add: returnOk_def prefix_refinement_return_imp) + +lemma prefix_refinement_throwError_imp: + "\\s0 s t0 t. \P s0 s; Q t0 t; isr s t\ \ rvr (Inl e) (Inl e') \ osr s t\ + \ prefix_refinement sr isr osr rvr AR R P Q (throwError e) (throwError e')" + by (simp add: throwError_def prefix_refinement_return_imp) + + section \Implications\ text \ -The notions of matching fragment and prefix refinement we have defined -allow us to prove the existence of a matching trace in the abstract -program. -\ + The notions of matching fragment and prefix refinement we have defined + allow us to prove the existence of a matching trace in the abstract + program.\ theorem matching_fragment_matching_tr: assumes match: "is_matching_fragment sr osr rvr ctr cres s0 R' s f" and rely: "rely_cond R t0 ctr" @@ -256,23 +390,21 @@ corollary matching_fragment_matching_tr_trivR: assumes match: "is_matching_fragment sr osr rvr ctr cres s0 R s f" and sr: "(\s t t'. sr s t \ (\s'. sr s' t' \ R s s'))" and srx: "sr s0 t0" - shows "\(atr, ares) \ f s. matching_tr sr atr ctr - \ rel_tmres osr rvr ares cres" - using matching_fragment_matching_tr[where R="\_ _. True", - OF match _ srx] - by (auto simp add: rely_cond_def sr) + shows "\(atr, ares) \ f s. matching_tr sr atr ctr \ rel_tmres osr rvr ares cres" + using matching_fragment_matching_tr[where R="\_ _. True", OF match _ srx] + by (auto simp: rely_cond_def sr) theorem prefix_refinement_rely_cond_trD: - assumes preds: "prefix_refinement sr isr osr rvr P Q R' R aprog cprog" + assumes preds: "prefix_refinement sr isr osr rvr AR R P Q aprog cprog" "isr s t" "P s0 s" "Q t0 t" "(ctr, cres) \ cprog t" "rely_cond R t0 ctr" "sr s0 t0" - and sr: "(\s t t'. sr s t \ R t t' \ (\s'. sr s' t' \ R' s s'))" + and sr: "(\s t t'. sr s t \ R t t' \ (\s'. sr s' t' \ AR s s'))" shows "\(atr, ares) \ aprog s. matching_tr sr atr ctr \ rel_tmres osr rvr ares cres - \ rely_cond R' s0 atr" + \ rely_cond AR s0 atr" proof - obtain f where subs: "f s \ aprog s" - and match: "is_matching_fragment sr osr rvr ctr cres s0 R' s f" + and match: "is_matching_fragment sr osr rvr ctr cres s0 AR s f" using prefix_refinementD[OF preds(1-3) _ preds(4-5)] preds(6-) by (auto simp add: triv_refinement_def) show ?thesis @@ -280,55 +412,249 @@ proof - by blast qed -lemma rely_cond_True: - "rely_cond (\_ _. True) = (\_ _. True)" - by (simp add: rely_cond_def fun_eq_iff) +section \Using prefix refinement\ +text \ + Using prefix refinement to map the validI Hoare quadruple + (precond/rely/guarantee/postcond). Proofs of quadruples for + abstract programs imply related quadruples for concrete + programs.\ + +lemma list_all2_all_trace_steps: + assumes P: "\x\trace_steps (rev tr) s0. P x" + and lR': "list_all2 (\(aid, as) (cid, cs). aid = cid \ R' as cs) tr tr'" + and R': "R' s0 s0'" + and Q: "\idn as1 as2 cs1 cs2. R' as1 cs1 \ R' as2 cs2 + \ P (idn, as1, as2) \ Q (idn, cs1, cs2)" + shows "\x\trace_steps (rev tr') s0'. Q x" +proof - + note lR'' = lR'[simplified trans[OF list_all2_rev[symmetric] list_all2_conv_all_nth], + simplified split_def, THEN conjunct2, rule_format] + note len[simp] = lR'[THEN list_all2_lengthD] + show ?thesis + using P R' + apply (clarsimp simp: trace_steps_nth) + apply (drule_tac x=x in bspec, simp) + apply (frule lR''[simplified]) + apply (cut_tac i="x - 1" in lR'', simp) + apply (auto simp: Q) + done +qed + +theorem prefix_refinement_validI: + "\prefix_refinement sr isr osr rvr AR R prP' prP f g; + \P'\,\AR\ f \G'\,\Q'\; + \t0 t. P t0 t \ (\s0 s. P' s0 s \ prP' s0 s \ prP t0 t \ isr s t \ sr s0 t0); + \s0 t0 t. \sr s0 t0; R t0 t\ \ (\s. AR s0 s \ sr s t); + \s0 t0 s t. \G' s0 s; sr s0 t0; sr s t\ \ G t0 t; + \rv rv' s0 t0 s t. \Q' rv s0 s; sr s0 t0; osr s t; rvr rv rv'\ \ Q rv' t0 t; prefix_closed g\ + \ \P\,\R\ g \G\,\Q\" + apply (subst validI_def, clarsimp simp: rely_def) + apply (drule meta_spec2, drule(1) meta_mp, clarsimp) + apply (drule(6) prefix_refinement_rely_cond_trD[where AR=AR, simplified]) + apply blast + apply clarsimp + apply (rule conjI) + apply (frule(3) validI_GD) + apply (simp add: guar_cond_def matching_tr_def) + apply (erule_tac R'="\s cs. sr s cs" in list_all2_all_trace_steps) + apply (clarsimp simp: list_all2_conv_all_nth split_def) + apply simp + apply clarsimp + apply clarsimp + apply (erule tmres.rel_cases; clarsimp) + apply (drule(1) validI_rvD, simp add: rely_def) + apply simp + apply (case_tac tr; clarsimp simp: list_all2_Cons2 matching_tr_def) + done + +section \Weakening rules\ + +named_theorems pfx_refn_pre +(* Introduce schematic prefix_refinement guards; fail if already schematic *) +method pfx_refn_pre0 = WP_Pre.pre_tac pfx_refn_pre +(* Optionally introduce schematic prefix_refinement guards *) +method pfx_refn_pre = pfx_refn_pre0? + +lemma stronger_prefix_refinement_weaken_pre[pfx_refn_pre]: + "\prefix_refinement sr isr osr rvr AR R P' Q' f g; + \s t s0 t0. \isr s t; sr s0 t0; P s0 s; Q t0 t\ \ P' s0 s; + \s t s0 t0. \isr s t; sr s0 t0; P s0 s; Q t0 t\ \ Q' t0 t\ + \ prefix_refinement sr isr osr rvr AR R P Q f g" + by (fastforce simp: prefix_refinement_def) + +lemma prefix_refinement_weaken_pre: + "\prefix_refinement sr isr osr rvr AR R P' Q' f g; + \s s0. P s0 s \ P' s0 s; \t t0. Q t0 t \ Q' t0 t\ + \ prefix_refinement sr isr osr rvr AR R P Q f g" + by pfx_refn_pre + +lemma prefix_refinement_weaken_pre1: + "\prefix_refinement sr isr osr rvr AR R P' Q f g; \s s0. P s0 s \ P' s0 s\ + \ prefix_refinement sr isr osr rvr AR R P Q f g" + by pfx_refn_pre + +lemma prefix_refinement_weaken_pre2: + "\prefix_refinement sr isr osr rvr AR R P Q' f g; \t t0. Q t0 t \ Q' t0 t\ + \ prefix_refinement sr isr osr rvr AR R P Q f g" + by pfx_refn_pre + +lemma prefix_refinement_weaken_srs: + "\prefix_refinement sr isr osr r AR R P Q f g; isr' \ isr; osr \ osr'; sr \ sr\ + \ prefix_refinement sr isr' osr' r AR R P Q f g" + apply (subst prefix_refinement_def, clarsimp) + apply (drule(1) predicate2D) + apply (drule(5) prefix_refinementD) + apply clarsimp + apply (rule exI, rule conjI[rotated], assumption) + apply (clarsimp simp: is_matching_fragment_def) + apply (drule(1) bspec, clarsimp) + apply (erule tmres.rel_cases; clarsimp) + apply (erule(1) predicate2D) + done + +named_theorems pfx_refn_rvr_pre +(* Introduce schematic return value relation, fail if already schematic *) +method pfx_refn_rvr_pre = WP_Pre.pre_tac pfx_refn_rvr_pre + +lemma prefix_refinement_weaken_rvr[pfx_refn_rvr_pre]: + "\prefix_refinement sr isr osr rvr AR R P Q f g; \rv rv'. rvr rv rv' \ rvr' rv rv'\ + \ prefix_refinement sr isr osr rvr' AR R P Q f g" + apply (subst prefix_refinement_def, clarsimp) + apply (drule(5) prefix_refinementD, clarsimp) + apply (rule exI, rule conjI[rotated], assumption) + apply (clarsimp simp: is_matching_fragment_def) + apply (drule(1) bspec, clarsimp) + apply (erule tmres.rel_cases; clarsimp) + done + +lemma prefix_closed_rely: + "prefix_closed f \ prefix_closed (rely f R s0)" + apply (subst prefix_closed_def, clarsimp simp: rely_def rely_cond_Cons_eq) + apply (erule(1) prefix_closedD) + done + +lemma rely_self_closed: + "self_closed P s f \ self_closed P s (rely f R s0)" + apply (subst self_closed_def, clarsimp simp: rely_def rely_cond_Cons_eq) + apply (drule(2) self_closedD) + apply (fastforce simp: rely_cond_Cons_eq) + done + +lemma rely_env_closed: + "\env_closed P s f; + \xs s. \P' xs s; rely_cond R s0 xs\ \ P xs s \ R (last_st_tr xs s0) s\ + \ env_closed P' s (rely f R s0)" + apply (subst env_closed_def, clarsimp simp: rely_def) + apply (drule_tac s'=s' in env_closedD, assumption) + apply simp + apply (clarsimp simp: image_def) + apply (fastforce intro: rely_cond_Cons rev_bexI) + done + +lemma rely_cond_mono: + "R \ R' \ rely_cond R \ rely_cond R'" + by (simp add: le_fun_def rely_cond_def split_def) + +lemma is_matching_fragment_add_rely: + "\is_matching_fragment sr osr r ctr cres s0 AR s f; AR' \ AR\ + \ is_matching_fragment sr osr r ctr cres s0 AR' s (rely f AR' s0)" + apply (frule is_matching_fragment_Nil) + apply (clarsimp simp: is_matching_fragment_def prefix_closed_rely + rely_self_closed) + apply (intro conjI) + apply (erule rely_env_closed) + apply (frule rely_cond_mono) + apply (simp add: le_fun_def rely_cond_Cons_eq) + apply (fastforce simp: rely_def) + apply (auto simp: rely_def)[1] + done + +named_theorems pfx_refn_rely_pre +(* Introduce schematic rely relations, fail if already schematic *) +method pfx_refn_rely_pre = WP_Pre.pre_tac pfx_refn_rely_pre + +lemma prefix_refinement_weaken_rely[pfx_refn_rely_pre]: + "\prefix_refinement sr isr osr r AR R P Q f g; R' \ R; AR' \ AR\ + \ prefix_refinement sr isr osr r AR' R' P Q f g" + apply (subst prefix_refinement_def, clarsimp) + apply (drule(3) prefix_refinementD, assumption+) + apply (clarsimp simp: rely_cond_def split_def le_fun_def) + apply (rule exI, rule conjI, erule is_matching_fragment_add_rely) + apply (simp add: le_fun_def) + apply (auto simp add: triv_refinement_def rely_def) + done + + +section \Inserting assumptions to be proved later\ + +lemma prefix_refinement_req: + "\\s0 s t0 t. \sr s0 t0; isr s t; P s0 s; Q t0 t\ \ F; + F \ prefix_refinement sr isr osr rvr AR R P Q f g\ + \ prefix_refinement sr isr osr rvr AR R P Q f g" + by (auto simp: prefix_refinement_def) + +lemma prefix_refinement_gen_asm: + "\P \ prefix_refinement sr isr osr rvr AR R P' Q' f g\ + \ prefix_refinement sr isr osr rvr AR R (P' and (\_ _. P)) Q' f g" + by (auto simp: prefix_refinement_def) + +lemma prefix_refinement_gen_asm2: + "\P \ prefix_refinement sr isr osr rvr AR R P' Q' f g\ + \ prefix_refinement sr isr osr rvr AR R P' (Q' and (\_ _. P)) f g" + by (auto simp: prefix_refinement_def) + +lemmas prefix_refinement_gen_asms = prefix_refinement_gen_asm prefix_refinement_gen_asm2 + +lemma prefix_refinement_assume_pre: + "\\s s0 t t0. \isr s t; sr s0 t0; P s0 s; Q t0 t\ \ prefix_refinement sr isr osr rvr AR R P Q f g\ + \ prefix_refinement sr isr osr rvr AR R P Q f g" + by (fastforce simp: prefix_refinement_def) + +lemma prefix_refinement_name_pre: + "\\s s0 t t0. + \isr s t; sr s0 t0; P s0 s; Q t0 t\ + \ prefix_refinement sr isr osr rvr AR R + (\s0' s'. s0' = s0 \ s' = s) (\t0' t'. t0' = t0 \ t' = t) f g\ + \ prefix_refinement sr isr osr rvr AR R P Q f g" + by (fastforce simp: prefix_refinement_def) + -section \Compositionality.\ -text \The crucial rules for proving prefix refinement -of parallel and sequential compositions.\ +section \Compositionality\ +text \The crucial rules for proving prefix refinement of parallel and sequential compositions.\ lemma ball_set_zip_conv_nth: - "(\x \ set (zip ys zs). P x) - = (\n. n < length ys \ n < length zs \ P (ys ! n, zs ! n))" - by (auto simp add: Ball_def in_set_zip) + "(\x \ set (zip ys zs). P x) = (\n. n < length ys \ n < length zs \ P (ys ! n, zs ! n))" + by (auto simp: Ball_def in_set_zip) -definition - par_tr_fin_principle :: "('s, unit) tmonad \ bool" -where +definition par_tr_fin_principle :: "('s, unit) tmonad \ bool" where "par_tr_fin_principle f = (\s tr s'. (tr, Result ((), s')) \ f s \ s' = last_st_tr tr s \ tr \ [])" lemmas par_tr_fin_principleD = par_tr_fin_principle_def[THEN iffD1, rule_format] lemma tr_in_parallel: "(tr, res) \ parallel f g s - \ \f_tr g_tr. (f_tr, res) \ f s \ (g_tr, res) \ g s - \ (tr, res) \ parallel (K {(f_tr, res)}) (K {(g_tr, res)}) s" + \ \f_tr g_tr. (f_tr, res) \ f s \ (g_tr, res) \ g s + \ (tr, res) \ parallel (K {(f_tr, res)}) (K {(g_tr, res)}) s" apply (clarsimp simp: parallel_def) apply fastforce done lemma matching_env_closedD: - "(tr, res) \ f s - \ is_matching_fragment sr osr rvr ctr cres s0 R s f - \ length tr < length ctr - \ fst (rev ctr ! length tr) = Env - \ sr s' (snd (rev ctr ! length tr)) - \ R (last_st_tr tr s0) s' - \ (Env, s') # tr \ fst ` f s" + "\(tr, res) \ f s; is_matching_fragment sr osr rvr ctr cres s0 R s f; + length tr < length ctr; fst (rev ctr ! length tr) = Env; + sr s' (snd (rev ctr ! length tr)); R (last_st_tr tr s0) s'\ + \ (Env, s') # tr \ fst ` f s" apply (frule(1) is_matching_fragment_trD, clarsimp) apply (erule(1) env_closedD[OF is_matching_fragment_env_closed]) apply (clarsimp simp: matching_tr_pfx_aCons rely_cond_Cons_eq prod_eq_iff) done lemma par_tr_fin_fragment: - "par_tr_fin_principle f - \ (tr, res) \ f s - \ is_matching_fragment sr osr rvr ctr cres s0 R s f - \ res = (case (length ctr - length tr, cres) - of (0, Failed) \ Failed - | (0, Result _) \ Result ((), last_st_tr tr s) - | _ \ Incomplete)" + "\par_tr_fin_principle f; (tr, res) \ f s; is_matching_fragment sr osr rvr ctr cres s0 R s f\ + \ res = (case (length ctr - length tr, cres) of + (0, Failed) \ Failed + | (0, Result _) \ Result ((), last_st_tr tr s) + | _ \ Incomplete)" apply (frule(1) is_matching_fragment_trD) apply (cases "length tr < length ctr") apply (clarsimp split: nat.split) @@ -339,15 +665,14 @@ lemma par_tr_fin_fragment: done lemma par_tr_fragment_in_parallel: - "par_tr_fin_principle f - \ par_tr_fin_principle g - \ is_matching_fragment sr osr rvr ctr1 cres s0 R s f - \ is_matching_fragment sr osr' rvr ctr2 cres s0 R' s g - \ length ctr1 = length ctr2 - \ \f_steps res'. length f_steps = length tr - \ (map (\(f_step, (id, s)). (if f_step then id else Env, s)) (zip f_steps tr), res) \ f s - \ (map (\(f_step, (id, s)). (if f_step then Env else id, s)) (zip f_steps tr), res') \ g s - \ (tr, res) \ parallel f g s" + "\par_tr_fin_principle f; par_tr_fin_principle g; + is_matching_fragment sr osr rvr ctr1 cres s0 R s f; + is_matching_fragment sr osr' rvr ctr2 cres s0 R' s g; + length ctr1 = length ctr2; + \f_steps res'. length f_steps = length tr + \ (map (\(f_step, (id, s)). (if f_step then id else Env, s)) (zip f_steps tr), res) \ f s + \ (map (\(f_step, (id, s)). (if f_step then Env else id, s)) (zip f_steps tr), res') \ g s\ + \ (tr, res) \ parallel f g s" apply (clarsimp simp: parallel_def) apply (rule_tac x=f_steps in exI, clarsimp) apply (drule(2) par_tr_fin_fragment)+ @@ -357,75 +682,64 @@ lemma par_tr_fragment_in_parallel: done lemma par_tr_fragment_parallel_def: - "par_tr_fin_principle f - \ par_tr_fin_principle g - \ is_matching_fragment sr osr rvr ctr1 cres s0 R s f - \ is_matching_fragment sr osr' rvr ctr2 cres s0 R' s g - \ length ctr1 = length ctr2 - \ parallel f g s = {(tr, res). \f_steps res'. length f_steps = length tr - \ (map (\(f_step, (id, s)). (if f_step then id else Env, s)) (zip f_steps tr), res) \ f s - \ (map (\(f_step, (id, s)). (if f_step then Env else id, s)) (zip f_steps tr), res') \ g s}" + "\par_tr_fin_principle f; par_tr_fin_principle g; + is_matching_fragment sr osr rvr ctr1 cres s0 R s f; + is_matching_fragment sr osr' rvr ctr2 cres s0 R' s g; + length ctr1 = length ctr2\ + \ parallel f g s = {(tr, res). \f_steps res'. length f_steps = length tr + \ (map (\(f_step, (id, s)). (if f_step then id else Env, s)) (zip f_steps tr), res) \ f s + \ (map (\(f_step, (id, s)). (if f_step then Env else id, s)) (zip f_steps tr), res') \ g s}" apply (rule equalityI; clarsimp) apply (auto simp: parallel_def)[1] apply (erule(4) par_tr_fragment_in_parallel) apply blast done -lemmas list_all2_rev_nthD - = list_all2_nthD[OF list_all2_rev[THEN iffD2], simplified] +lemmas list_all2_rev_nthD = list_all2_nthD[OF list_all2_rev[THEN iffD2], simplified] -definition - forward_enabled :: "'s rg_pred \ bool" -where +definition forward_enabled :: "'s rg_pred \ bool" where "forward_enabled P = (\s_pre. \s. P s_pre s)" lemmas forward_enabledD = forward_enabled_def[THEN iffD1, rule_format] lemma forward_enabled_mono: - "P \ Q \ forward_enabled P \ forward_enabled Q" + "\P \ Q; forward_enabled P\ \ forward_enabled Q" by (fastforce simp: forward_enabled_def le_fun_def) lemma forward_enabled_reflp: "reflp P \ forward_enabled P" - by (auto simp add: reflp_def forward_enabled_def) + by (auto simp: reflp_def forward_enabled_def) lemma par_tr_fin_principle_triv_refinement: - "par_tr_fin_principle aprog - \ triv_refinement aprog cprog - \ par_tr_fin_principle cprog" + "\par_tr_fin_principle aprog; triv_refinement aprog cprog\ + \ par_tr_fin_principle cprog" by (fastforce simp: par_tr_fin_principle_def triv_refinement_def) lemma matching_tr_pfx_parallel_zip: - "matching_tr_pfx sr a_pfx a_tr - \ matching_tr_pfx sr b_pfx b_tr - \ length a_pfx = length b_pfx - \ list_all2 (\y z. (fst y = Env \ fst z = Env) \ snd y = snd z) a_tr b_tr - \ matching_tr_pfx sr (map parallel_mrg (zip a_pfx b_pfx)) (map parallel_mrg (zip a_tr b_tr))" + "\matching_tr_pfx sr a_pfx a_tr; matching_tr_pfx sr b_pfx b_tr; + length a_pfx = length b_pfx; + list_all2 (\y z. (fst y = Env \ fst z = Env) \ snd y = snd z) a_tr b_tr\ + \ matching_tr_pfx sr (map parallel_mrg (zip a_pfx b_pfx)) (map parallel_mrg (zip a_tr b_tr))" apply (clarsimp simp: matching_tr_pfx_def matching_tr_def list_all2_lengthD) apply (clarsimp simp: list_all2_conv_all_nth) apply (clarsimp simp: rev_map split_def zip_rev[symmetric]) done lemma drop_sub_Suc_is_Cons: - "n = length xs \ m < length xs \ drop (n - Suc m) xs = (rev xs ! m) # drop (n - m) xs" + "\n = length xs; m < length xs\ \ drop (n - Suc m) xs = (rev xs ! m) # drop (n - m) xs" apply (rule nth_equalityI; clarsimp) - apply (clarsimp simp add: nth_Cons' rev_nth) + apply (clarsimp simp: nth_Cons' rev_nth) done -lemma le_sub_eq_0: - "((x :: nat) \ x - y) = (x = 0 \ y = 0)" - by arith - -lemmas rely_cond_append_split - = rely_cond_append[where xs="take n xs" and ys="drop n xs" for n xs, simplified] -lemmas guar_cond_append_split - = guar_cond_append[where xs="take n xs" and ys="drop n xs" for n xs, simplified] +lemmas rely_cond_append_split = + rely_cond_append[where xs="take n xs" and ys="drop n xs" for n xs, simplified] +lemmas guar_cond_append_split = + guar_cond_append[where xs="take n xs" and ys="drop n xs" for n xs, simplified] lemma validI_drop_next_G: - "\ \P\, \R\ f \G\, \Q\; P s0 s; (tr, res) \ f s; - rely_cond R s0 (drop (n - m) tr); n = length tr; m < length tr \ - \ fst (rev tr ! m) \ Env - \ G (last_st_tr (rev (take m (rev tr))) s0) (snd (rev tr ! m))" + "\\P\, \R\ f \G\, \Q\; P s0 s; (tr, res) \ f s; rely_cond R s0 (drop (n - m) tr); + n = length tr; m < length tr\ + \ fst (rev tr ! m) \ Env \ G (last_st_tr (rev (take m (rev tr))) s0) (snd (rev tr ! m))" apply clarify apply (drule(2) validI_GD_drop[where n="n - Suc m"]) apply (simp add: drop_sub_Suc_is_Cons) @@ -446,18 +760,17 @@ lemma tr_in_parallel_validI: by (clarsimp simp: rel trs predicate2I) lemma env_closed_parallel_fragment: - "is_matching_fragment sr osr rvr ctr1 cres1 s0 (E or Gg) s f - \ is_matching_fragment sr osr' rvr ctr2 cres2 s0 (E or Gf) s g - \ par_tr_fin_principle f - \ par_tr_fin_principle g - \ cres1 = cres2 \ length ctr1 = length ctr2 - \ \s xs. Q xs s \ (sr s (snd (rev ctr1 ! length xs))) - \ (sr s (snd (rev ctr2 ! length xs))) - \ length xs < length ctr2 - \ fst (rev ctr1 ! length xs) = Env - \ fst (rev ctr2 ! length xs) = Env - \ E (last_st_tr xs s0) s - \ env_closed Q s (parallel f g)" + "\is_matching_fragment sr osr rvr ctr1 cres1 s0 (E or Gg) s f; + is_matching_fragment sr osr' rvr ctr2 cres2 s0 (E or Gf) s g; + par_tr_fin_principle f; par_tr_fin_principle g; + cres1 = cres2; length ctr1 = length ctr2; + \s xs. Q xs s \ (sr s (snd (rev ctr1 ! length xs))) + \ (sr s (snd (rev ctr2 ! length xs))) + \ length xs < length ctr2 + \ fst (rev ctr1 ! length xs) = Env + \ fst (rev ctr2 ! length xs) = Env + \ E (last_st_tr xs s0) s\ + \ env_closed Q s (parallel f g)" apply (subst env_closed_def, clarsimp) apply (frule is_matching_fragment_prefix_closed[where f=f]) apply (frule is_matching_fragment_prefix_closed[where f=g]) @@ -472,10 +785,10 @@ lemma env_closed_parallel_fragment: apply (drule spec2, drule(1) mp[where P="Q xs s" for xs s]) apply clarsimp apply (drule_tac s'=s' in env_closedD[where f=f, OF is_matching_fragment_env_closed, rotated]; - simp?) + simp?) apply (simp add: matching_tr_pfx_aCons rely_cond_Cons_eq last_st_tr_map_zip prod_eq_iff) apply (drule_tac s'=s' in env_closedD[where f=g, OF is_matching_fragment_env_closed, rotated]; - simp?) + simp?) apply (simp add: matching_tr_pfx_aCons rely_cond_Cons_eq last_st_tr_map_zip prod_eq_iff) apply clarsimp apply blast @@ -484,18 +797,15 @@ lemma env_closed_parallel_fragment: lemma self_closed_parallel_fragment: notes if_split[split del] shows - "is_matching_fragment sr osr rvr ctr1 cres1 s0 (E or Gg) s f - \ is_matching_fragment sr osr' rvr ctr2 cres2 s0 (E or Gf) s g - \ par_tr_fin_principle f - \ par_tr_fin_principle g - \ list_all2 (\y z. (fst y = Env \ fst z = Env) \ snd y = snd z) ctr1 ctr2 - \ \P\,\E or Gg\ f \Gf\,\\_ _ _. True\ - \ \P\,\E or Gf\ g \Gg\,\\_ _ _. True\ - \ P s0 s - \ cres1 = cres2 - \ Q = (\xs. length xs < length ctr1 \ (fst (rev ctr1 ! length xs) \ Env - \ fst (rev ctr2 ! length xs) \ Env)) - \ self_closed Q s (parallel f g)" + "\is_matching_fragment sr osr rvr ctr1 cres1 s0 (E or Gg) s f; + is_matching_fragment sr osr' rvr ctr2 cres2 s0 (E or Gf) s g; + par_tr_fin_principle f; par_tr_fin_principle g; + list_all2 (\y z. (fst y = Env \ fst z = Env) \ snd y = snd z) ctr1 ctr2; + \P\,\E or Gg\ f \Gf\,\\_ _ _. True\; \P\,\E or Gf\ g \Gg\,\\_ _ _. True\; + P s0 s; cres1 = cres2; + Q = (\xs. length xs < length ctr1 \ (fst (rev ctr1 ! length xs) \ Env + \ fst (rev ctr2 ! length xs) \ Env))\ + \ self_closed Q s (parallel f g)" apply (subst self_closed_def, clarsimp) apply (subst(asm) parallel_def, clarsimp) apply (frule list_all2_lengthD[symmetric]) @@ -506,7 +816,7 @@ lemma self_closed_parallel_fragment: apply (frule(1) list_all2_rev_nthD, clarsimp) apply (case_tac "fst (rev ctr1 ! length xs) = Env"; simp) apply (frule is_matching_fragment_self_closed[where f=g], - drule(1) self_closedD, simp add: eq_Me_neq_Env) + drule(1) self_closedD, simp add: eq_Me_neq_Env) apply (thin_tac "v \ g s" for v s) apply clarsimp apply (frule(1) is_matching_fragment_trD[where f=g]) @@ -519,7 +829,7 @@ lemma self_closed_parallel_fragment: apply (blast intro: in_fst_snd_image) (* pretty much identical proof for symmetric case. sad. *) apply (frule is_matching_fragment_self_closed[where f=f], - drule(1) self_closedD, simp add: eq_Me_neq_Env) + drule(1) self_closedD, simp add: eq_Me_neq_Env) apply (thin_tac "v \ f s" for v s) apply clarsimp apply (frule(1) is_matching_fragment_trD[where f=f]) @@ -533,51 +843,23 @@ lemma self_closed_parallel_fragment: done lemma is_matching_fragment_validI_disj: - "is_matching_fragment sr osr rvr b_tr bd_res s0 R s f - \ triv_refinement g f - \ G = \\ \ \P\,\R\ g \G\,\\_ _ _. True\ - \ \P\,\R\ f \G\,\\_ _ _. True\" + "\is_matching_fragment sr osr rvr b_tr bd_res s0 R s f; triv_refinement g f; + G = \\ \ \P\,\R\ g \G\,\\_ _ _. True\\ + \ \P\,\R\ f \G\,\\_ _ _. True\" apply (frule is_matching_fragment_prefix_closed) apply (erule disjE) - apply (simp add: validI_def guar_cond_def) + apply wpsimp apply (erule(2) validI_triv_refinement) done -lemma prefix_closed_rely: - "prefix_closed f \ prefix_closed (rely f R s0)" - apply (subst prefix_closed_def, clarsimp simp: rely_def rely_cond_Cons_eq) - apply (erule(1) prefix_closedD) - done - -lemma rely_self_closed: - "self_closed P s f \ self_closed P s (rely f R s0)" - apply (subst self_closed_def, clarsimp simp: rely_def rely_cond_Cons_eq) - apply (drule(2) self_closedD) - apply (fastforce simp: rely_cond_Cons_eq) - done - -lemma rely_env_closed: - "env_closed P s f - \ (\xs s. P' xs s \ rely_cond R s0 xs \ P xs s \ R (last_st_tr xs s0) s) - \ env_closed P' s (rely f R s0)" - apply (subst env_closed_def, clarsimp simp: rely_def) - apply (drule_tac s'=s' in env_closedD, assumption) - apply simp - apply (clarsimp simp: image_def) - apply (fastforce intro: rely_cond_Cons rev_bexI) - done - theorem prefix_refinement_parallel: - "prefix_refinement sr isr osr rvr P Q (AE or Gc) (E or Gd) a b - \ prefix_refinement sr isr osr rvr P Q (AE or Ga) (E or Gb) c d - \ par_tr_fin_principle a - \ par_tr_fin_principle c - \ \Q\,\E or Gd\ b \Gb\,\\_ _ _. True\ - \ \Q\,\E or Gb\ d \Gd\,\\_ _ _. True\ - \ (Ga = \\ \ Gc = \\) - \ (\P\,\AE or Gc\ a \Ga\,\\_ _ _. True\ - \ \P\,\AE or Ga\ c \Gc\,\\_ _ _. True\) - \ prefix_refinement sr isr osr rvr P Q AE E (parallel a c) (parallel b d)" + "\prefix_refinement sr isr osr rvr (AE or Gc) (E or Gd) P Q a b; + prefix_refinement sr isr osr rvr (AE or Ga) (E or Gb) P Q c d; + par_tr_fin_principle a; par_tr_fin_principle c; + \Q\,\E or Gd\ b \Gb\,\\_ _ _. True\; \Q\,\E or Gb\ d \Gd\,\\_ _ _. True\; + (Ga = \\ \ Gc = \\) + \ (\P\,\AE or Gc\ a \Ga\,\\_ _ _. True\ \ \P\,\AE or Ga\ c \Gc\,\\_ _ _. True\)\ + \ prefix_refinement sr isr osr rvr AE E P Q (parallel a c) (parallel b d)" apply (subst prefix_refinement_def, clarsimp) apply (drule tr_in_parallel, clarify) apply (frule(6) tr_in_parallel_validI) @@ -594,9 +876,9 @@ theorem prefix_refinement_parallel: apply (frule(1) is_matching_fragment_validI_disj[where g=a and G=Ga], blast) apply (frule(1) is_matching_fragment_validI_disj[where g=c and G=Gc], blast) apply (intro conjI prefix_closed_parallel prefix_closed_rely rely_self_closed, - simp_all add: is_matching_fragment_prefix_closed) + simp_all add: is_matching_fragment_prefix_closed) apply (rule self_closed_parallel_fragment, - (assumption | erule par_tr_fin_principle_triv_refinement[rotated])+) + (assumption | erule par_tr_fin_principle_triv_refinement[rotated])+) apply simp apply (frule list_all2_lengthD) apply (simp add: list_all2_lengthD eq_Me_neq_Env rev_nth split_def fun_eq_iff @@ -604,7 +886,7 @@ theorem prefix_refinement_parallel: apply (rule rely_env_closed[where P=P and P'=P for P, rotated]) apply (simp add: rely_cond_Cons_eq) apply (rule env_closed_parallel_fragment, - (assumption | erule par_tr_fin_principle_triv_refinement[rotated])+) + (assumption | erule par_tr_fin_principle_triv_refinement[rotated])+) apply simp apply (simp add: list_all2_lengthD) apply (clarsimp simp: matching_tr_pfx_aCons rev_map split_def @@ -624,35 +906,27 @@ theorem prefix_refinement_parallel: apply (simp add: list_all2_lengthD) done -lemma validI_triv': - "prefix_closed f \ \P\,\R\ f \\_ _. True\,\\_ _ _. True\" - by (simp add: validI_def guar_cond_def) -lemmas validI_triv = validI_triv'[where P="\\"] - lemmas prefix_refinement_parallel_ART - = prefix_refinement_parallel[OF _ _ _ _ _ _ disjI1[OF conjI, OF refl refl]] + = prefix_refinement_parallel[OF _ _ _ _ _ _ disjI1[OF conjI, OF refl refl]] lemmas prefix_refinement_parallel_triv - = prefix_refinement_parallel_ART[OF _ _ _ _ validI_triv' validI_triv'] + = prefix_refinement_parallel_ART[where Gb="\\" and Gd="\\", simplified] lemmas prefix_refinement_parallel' - = prefix_refinement_parallel[OF _ _ _ _ _ _ disjI2[OF conjI]] + = prefix_refinement_parallel[OF _ _ _ _ _ _ disjI2[OF conjI]] lemma pfx_trace_set_allD: - "\n. \v\set (take n xs). P n v \ v \ set (take n xs) - \ P n v" + "\\n. \v\set (take n xs). P n v; v \ set (take n xs)\ \ P n v" by simp lemma prefix_closed_UNION: - "(\s' x. x \ S s' \ prefix_closed (f x)) - \ prefix_closed (\s. \x \ S s. f x s)" + "\\s' x. x \ S s' \ prefix_closed (f x)\ \ prefix_closed (\s. \x \ S s. f x s)" apply (simp add: prefix_closed_def) apply (blast intro: in_fst_snd_image) done lemma is_matching_fragment_UNION: - "(\x. x \ S s \ is_matching_fragment sr osr rvr ctr cres s0 R s (f x)) - \ (\s' x. x \ S s' \ prefix_closed (f x)) - \ S s \ {} - \ is_matching_fragment sr osr rvr ctr cres s0 R s (\s. \x \ S s. f x s)" + "\\x. x \ S s \ is_matching_fragment sr osr rvr ctr cres s0 R s (f x); + \s' x. x \ S s' \ prefix_closed (f x); S s \ {}\ + \ is_matching_fragment sr osr rvr ctr cres s0 R s (\s. \x \ S s. f x s)" apply (clarsimp simp: is_matching_fragment_def prefix_closed_UNION) apply (intro conjI impI) apply (clarsimp simp: self_closed_def split_def in_fst_snd_image_eq) @@ -661,22 +935,26 @@ lemma is_matching_fragment_UNION: apply blast done -definition - mbind :: "('s, 'a) tmonad \ ('s \ 'a \ ('s, 'b) tmonad) \ - 's \ ('s, 'b) tmonad" +\ \ + This is a variant of @{term Trace_Monad.bind}, that is used to build up the fragment required + for proving @{text prefix_refinement_bind_general}.\ +definition mbind :: + "('s, 'a) tmonad \ ('s \ 'a \ ('s, 'b) tmonad) \ 's \ ('s, 'b) tmonad" where - "mbind f g s0 \ \s. \(xs, r) \ (f s). case r of Failed \ {(xs, Failed)} - | Incomplete \ {(xs, Incomplete)} - | Result (rv, s) \ fst_upd (\ys. ys @ xs) ` g (last_st_tr xs s0) rv s" + "mbind f g s0 \ \s. \(xs, r) \ (f s). + case r of + Failed \ {(xs, Failed)} + | Incomplete \ {(xs, Incomplete)} + | Result (rv, s) \ fst_upd (\ys. ys @ xs) ` g (last_st_tr xs s0) rv s" lemma self_closed_mbind: - "is_matching_fragment sr osr rvr ctr cres s0 R s f - \ (\tr x s'. (tr, Result (x, s')) \ f s - \ self_closed (\xs. length xs < length ctr' \ fst (rev ctr' ! length xs) = Me) s' - (g (last_st_tr tr s0) x) \ [] \ fst ` g (last_st_tr tr s0) x s') - \ Q = matching_self_cond (ctr' @ ctr) - \ cres = Incomplete \ ctr' = [] - \ self_closed Q s (mbind f g s0)" + "\is_matching_fragment sr osr rvr ctr cres s0 R s f; + \tr x s'. (tr, Result (x, s')) \ f s + \ self_closed (\xs. length xs < length ctr' \ fst (rev ctr' ! length xs) = Me) s' + (g (last_st_tr tr s0) x) + \ [] \ fst ` g (last_st_tr tr s0) x s'; + Q = matching_self_cond (ctr' @ ctr); cres = Incomplete \ ctr' = []\ + \ self_closed Q s (mbind f g s0)" apply (frule is_matching_fragment_self_closed) apply (subst self_closed_def, clarsimp simp: mbind_def) apply (rename_tac tr res) @@ -706,14 +984,12 @@ lemma matching_tr_pfx_rhs_is_extend: fixes ys ys' defines "N == length ys' - length ys" shows - "matching_tr_pfx sr xs ys - \ length xs \ length ys \ drop N ys' = ys - \ matching_tr_pfx sr xs ys'" + "\matching_tr_pfx sr xs ys; length xs \ length ys \ drop N ys' = ys\ + \ matching_tr_pfx sr xs ys'" apply (clarsimp simp: matching_tr_pfx_def) apply (rule context_conjI) apply simp - apply (simp add: matching_tr_def list_all2_conv_all_nth - min_def) + apply (simp add: matching_tr_def list_all2_conv_all_nth min_def) apply (clarsimp simp: rev_nth) done @@ -721,24 +997,21 @@ lemma matching_tr_pfx_rhs_is_drop: fixes ys ys' defines "N == length ys - length ys'" shows - "matching_tr_pfx sr xs ys - \ drop N ys = ys' - \ length xs \ length ys' - \ matching_tr_pfx sr xs ys'" + "\matching_tr_pfx sr xs ys; drop N ys = ys'; length xs \ length ys'\ + \ matching_tr_pfx sr xs ys'" apply (clarsimp simp: matching_tr_pfx_def) - apply (simp add: matching_tr_def list_all2_conv_all_nth - min_def) + apply (simp add: matching_tr_def list_all2_conv_all_nth min_def) apply (clarsimp simp: rev_nth) done lemma env_closed_mbind: - "is_matching_fragment sr osr rvr ctr' cres s0 R s f - \ \tr x s'. (tr, Result (x, s')) \ f s - \ env_closed (matching_env_cond sr ctr'' (last_st_tr tr s0) R) s' (g (last_st_tr tr s0) x) - \ [] \ fst ` g (last_st_tr tr s0) x s' - \ (if cres \ {Incomplete, Failed} then ctr = ctr' else ctr = ctr'' @ ctr') - \ Q = matching_env_cond sr ctr s0 R - \ env_closed Q s (mbind f g s0)" + "\is_matching_fragment sr osr rvr ctr' cres s0 R s f; + \tr x s'. (tr, Result (x, s')) \ f s + \ env_closed (matching_env_cond sr ctr'' (last_st_tr tr s0) R) s' (g (last_st_tr tr s0) x) + \ [] \ fst ` g (last_st_tr tr s0) x s'; + if cres \ {Incomplete, Failed} then ctr = ctr' else ctr = ctr'' @ ctr'; + Q = matching_env_cond sr ctr s0 R\ + \ env_closed Q s (mbind f g s0)" apply (simp add: if_bool_eq_conj) apply (subst env_closed_def, clarsimp simp: mbind_def) apply (strengthen in_fst_snd_image, simp) @@ -773,12 +1046,11 @@ lemma env_closed_mbind: done lemma prefix_closed_mbind: - "prefix_closed f - \ \tr x s' s. (tr, Result (x, s')) \ f s \ prefix_closed (g (last_st_tr tr s0) x) + "\prefix_closed f; \tr x s' s. (tr, Result (x, s')) \ f s \ prefix_closed (g (last_st_tr tr s0) x)\ \ prefix_closed (mbind f g s0)" apply (subst prefix_closed_def, clarsimp simp: mbind_def) apply (split tmres.split_asm; clarsimp; - (drule(1) prefix_closedD, fastforce elim: rev_bexI)?) + (drule(1) prefix_closedD, fastforce elim: rev_bexI)?) apply (simp add: Cons_eq_append_conv, safe) apply (drule(1) prefix_closedD) apply (fastforce elim: rev_bexI) @@ -789,26 +1061,25 @@ lemma prefix_closed_mbind: done lemma is_matching_fragment_mbind: - "is_matching_fragment sr intsr rvr ctr cres s0 R s f_a - \ \tr x s'. (tr, Result (x, s')) \ f_a s - \ is_matching_fragment sr osr rvr' ctr' cres' (last_st_tr tr s0) R s' (f_b (last_st_tr tr s0) x) - \ \s0' x. prefix_closed (f_b s0' x) - \ ctr'' = ctr' @ ctr - \ cres'' = (case cres of Failed \ Failed | Incomplete \ Incomplete | _ \ cres') - \ (cres = Incomplete \ cres = Failed) \ ctr' = [] - \ is_matching_fragment sr osr rvr' ctr'' cres'' s0 R s - (mbind f_a f_b s0)" + "\is_matching_fragment sr intsr rvr ctr cres s0 R s f_a; + \tr x s'. (tr, Result (x, s')) \ f_a s + \ is_matching_fragment sr osr rvr' ctr' cres' (last_st_tr tr s0) R s' (f_b (last_st_tr tr s0) x); + \s0' x. prefix_closed (f_b s0' x); + ctr'' = ctr' @ ctr; + cres'' = (case cres of Failed \ Failed | Incomplete \ Incomplete | _ \ cres'); + (cres = Incomplete \ cres = Failed) \ ctr' = []\ + \ is_matching_fragment sr osr rvr' ctr'' cres'' s0 R s (mbind f_a f_b s0)" apply (subst is_matching_fragment_def, clarsimp) apply (strengthen env_closed_mbind[where ctr''=ctr', mk_strg I E] prefix_closed_mbind self_closed_mbind[where ctr'="ctr'", mk_strg I E]) apply (simp add: conj_comms if_bool_eq_conj mres_def split del: if_split) apply (intro conjI allI impI; clarsimp?; - (blast intro: is_matching_fragment_prefix_closed - is_matching_fragment_env_closed - is_matching_fragment_Nil - is_matching_fragment_self_closed - dest: post_by_hoare)?) + (blast intro: is_matching_fragment_prefix_closed + is_matching_fragment_env_closed + is_matching_fragment_Nil + is_matching_fragment_self_closed + dest: post_by_hoare)?) apply (clarsimp simp: mbind_def) apply (frule_tac s=s in is_matching_fragment_defD) apply (drule ex_in_conv[THEN iffD2], clarsimp) @@ -826,16 +1097,18 @@ lemma is_matching_fragment_mbind: done lemma is_matching_fragment_mbind_union: - "is_matching_fragment sr intsr rvr ctr cres s0 R s f_a - \ ctr'' = ctr' @ ctr - \ cres'' = (case cres of Failed \ Failed | Incomplete \ Incomplete | _ \ cres') - \ cres = Incomplete \ cres = Failed \ ctr' = [] - \ \tr x s'. (tr, Result (x, s')) \ f_a s + "\is_matching_fragment sr intsr rvr ctr cres s0 R s f_a; + ctr'' = ctr' @ ctr; + cres'' = (case cres of Failed \ Failed | Incomplete \ Incomplete | _ \ cres'); + cres = Incomplete \ cres = Failed \ ctr' = []; + \tr x s'. (tr, Result (x, s')) \ f_a s \ (\f. is_matching_fragment sr osr rvr' ctr' cres' (last_st_tr tr s0) R s' f - \ triv_refinement (aprog x) f) - \ is_matching_fragment sr osr rvr' ctr'' cres'' s0 R s - (mbind f_a (\s0' rv s. \f \ {f. is_matching_fragment sr osr rvr' ctr' cres' s0' R s f - \ triv_refinement (aprog rv) f}. f s) s0)" + \ triv_refinement (aprog x) f)\ + \ is_matching_fragment sr osr rvr' ctr'' cres'' s0 R s + (mbind f_a + (\s0' rv s. \f \ {f. is_matching_fragment sr osr rvr' ctr' cres' s0' R s f + \ triv_refinement (aprog rv) f}. f s) + s0)" apply (rule is_matching_fragment_mbind; assumption?) apply clarsimp apply (rule is_matching_fragment_UNION) @@ -848,9 +1121,8 @@ lemma is_matching_fragment_mbind_union: done lemma is_matching_fragment_mresD: - "is_matching_fragment sr osr rvr ctr cres s0 R s f - \ (x, s') \ mres (f s) - \ \y s''. cres = Result (y, s'') \ osr s' s'' \ rvr x y" + "\is_matching_fragment sr osr rvr ctr cres s0 R s f; (x, s') \ mres (f s)\ + \ \y s''. cres = Result (y, s'') \ osr s' s'' \ rvr x y" apply (clarsimp simp: mres_def) apply (frule(1) is_matching_fragment_trD) apply (clarsimp simp: matching_tr_pfx_def) @@ -858,40 +1130,26 @@ lemma is_matching_fragment_mresD: done lemma matching_tr_pfx_sr_hd_append: - "matching_tr_pfx sr tr tr' - \ sr s0 t0 - \ length tr \ length tr' - \ sr (hd (map snd tr @ [s0])) (hd (map snd tr' @ [t0]))" + "\matching_tr_pfx sr tr tr'; sr s0 t0; length tr \ length tr'\ + \ sr (hd (map snd tr @ [s0])) (hd (map snd tr' @ [t0]))" apply (clarsimp simp: matching_tr_pfx_def matching_tr_def) apply (erule list.rel_cases; clarsimp) done lemma matching_tr_pfx_last_st_tr: - "matching_tr_pfx sr tr tr' - \ sr s0 t0 - \ length tr \ length tr' - \ sr (last_st_tr tr s0) (last_st_tr tr' t0)" + "\matching_tr_pfx sr tr tr'; sr s0 t0; length tr \ length tr'\ + \ sr (last_st_tr tr s0) (last_st_tr tr' t0)" apply (clarsimp simp: matching_tr_pfx_def matching_tr_def) apply (erule list.rel_cases; clarsimp) done -lemma validI_relyT_mresD: - "\P'\,\\\\ f \G\,\P''\ - \ (rv, s') \ mres (f s) - \ P' s0 s - \ \s0'. P'' rv s0' s'" - apply (clarsimp simp: mres_def) - apply (drule(2) validI_rvD) - apply (simp add: rely_cond_def) - apply blast - done - -theorem prefix_refinement_bind_general[rule_format]: - "prefix_refinement sr isr intsr rvr P Q AR R a c - \ (\x y. rvr x y \ prefix_refinement sr intsr osr rvr' (P'' x) (Q'' y) AR R (b x) (d y)) - \ \P'\,\AR\ a \\\\,\P''\ \ \\s. \s0. P' s0 s\ a \\rv s. \s0. P'' rv s0 s\ - \ \Q'\,\R\ c \\\\,\Q''\ - \ prefix_refinement sr isr osr rvr' (P and P') (Q and Q') AR R (a >>= b) (c >>= d)" +\ \FIXME: do we want to follow the corres naming pattern and use split instead of bind?\ +theorem prefix_refinement_bind_general: + "\prefix_refinement sr isr intsr rvr' AR R P Q a c; + \rv rv'. rvr' rv rv' \ prefix_refinement sr intsr osr rvr AR R (P'' rv) (Q'' rv') (b rv) (d rv'); + \P'\,\AR\ a \\\\,\P''\ \ \\s. \s0. P' s0 s\ a \\rv s. \s0. P'' rv s0 s\; + \Q'\,\R\ c \\\\,\Q''\\ + \ prefix_refinement sr isr osr rvr AR R (P and P') (Q and Q') (a >>= (\rv. b rv)) (c >>= (\rv'. d rv'))" apply (subst prefix_refinement_def, clarsimp simp: bind_def) apply (rename_tac c_tr c_res cd_tr cd_res) apply (drule(5) prefix_refinementD, simp) @@ -902,7 +1160,8 @@ theorem prefix_refinement_bind_general[rule_format]: apply (case_tac "c_res = Incomplete \ c_res = Failed") apply (intro exI conjI) apply (rule_tac ctr'=Nil and cres'=Failed and f_b="\_ _ _. {}" - in is_matching_fragment_mbind, assumption, simp_all add: prefix_closed_def)[1] + in is_matching_fragment_mbind, + assumption, simp_all add: prefix_closed_def)[1] apply clarsimp apply (frule is_matching_fragment_mresD, erule in_mres) apply clarsimp @@ -915,20 +1174,20 @@ theorem prefix_refinement_bind_general[rule_format]: apply (frule(2) validI_rvD, simp add: rely_cond_append) apply (intro exI conjI) apply (rule is_matching_fragment_mbind_union[where aprog="b"], - assumption, simp_all)[1] + assumption, simp_all)[1] apply clarsimp apply (frule is_matching_fragment_mresD, erule in_mres) apply (clarsimp simp: mres_def) apply (frule(1) is_matching_fragment_trD) apply clarsimp apply (rule prefix_refinementD[where x="(a, b)" for a b, simplified, rule_format], - blast, simp_all)[1] + blast, simp_all)[1] prefer 2 apply (erule(1) matching_tr_pfx_last_st_tr) apply simp apply (erule disjE) apply (drule(1) validI_rvD[OF validI_triv_refinement], - erule is_matching_fragment_prefix_closed, assumption+) + erule is_matching_fragment_prefix_closed, assumption+) apply (drule(2) use_valid[OF in_mres valid_triv_refinement], blast, simp) apply (clarsimp simp: rely_cond_append hd_append hd_map cong: if_cong) apply (clarsimp simp: triv_refinement_def mbind_def) @@ -938,163 +1197,599 @@ theorem prefix_refinement_bind_general[rule_format]: apply blast done -section \Using prefix refinement.\ -text \ -Using prefix refinement to map the validI Hoare quadruple -(precond/rely/guarantee/postcond). Proofs of quadruples for -abstract programs imply related quadruples for concrete -programs. -\ - -lemma list_all2_all_trace_steps: - assumes P: "\x\trace_steps (rev tr) s0. P x" - and lR': "list_all2 (\(aid, as) (cid, cs). aid = cid \ R' as cs) tr' tr" - and R': "R' s0' s0" - and Q: "\idn as1 as2 cs1 cs2. R' as1 cs1 \ R' as2 cs2 - \ P (idn, cs1, cs2) \ Q (idn, as1, as2)" - shows "\x\trace_steps (rev tr') s0'. Q x" -proof - - note lR'' = lR'[simplified trans[OF list_all2_rev[symmetric] list_all2_conv_all_nth], - simplified split_def, THEN conjunct2, rule_format] - note len[simp] = lR'[THEN list_all2_lengthD] - show ?thesis - using P R' - apply (clarsimp simp: trace_steps_nth) - apply (drule_tac x=x in bspec, simp) - apply (frule lR''[simplified]) - apply (cut_tac i="x - 1" in lR'', simp) - apply (auto simp: Q) - done -qed +section \Derivative splitting rules\ -theorem prefix_refinement_validI: - "prefix_refinement sr isr osr rvr prP' prP R' R f g - \ \P'\,\R'\ - f \\s0 s. \cs0 cs. sr s0 cs0 \ sr s cs \ G cs0 cs\,\\rv - s0 s. \rv' cs0 cs. sr s0 cs0 \ osr s cs \ rvr rv rv' \ Q rv' cs0 cs\ - \ \t0 t. P t0 t \ (\s0 s. P' s0 s \ prP' s0 s \ prP t0 t \ isr s t \ sr s0 t0) - \ \s0 t0 t. sr s0 t0 \ R t0 t \ (\s. R' s0 s \ sr s t) - \ prefix_closed g - \ \P\,\R\ g \G\,\Q\" - apply (subst validI_def, clarsimp simp: rely_def) - apply (drule spec2, drule(1) mp, clarsimp) - apply (drule(6) prefix_refinement_rely_cond_trD[where R'=R', simplified]) - apply blast - apply clarsimp - apply (rule conjI) - apply (frule(3) validI_GD) - apply (simp add: guar_cond_def matching_tr_def) - apply (erule_tac R'="\cs s. sr s cs" in list_all2_all_trace_steps) - apply (clarsimp simp: list_all2_conv_all_nth split_def) - apply simp +lemma prefix_refinement_bind_v: + "\prefix_refinement sr isr intsr rvr' AR R P Q a c; + \rv rv'. rvr' rv rv' \ prefix_refinement sr intsr osr rvr AR R (\_. P'' rv) (Q'' rv') (b rv) (d rv'); + \P'\ a \P''\; \Q'\,\R\ c \\\\,\Q''\\ + \ prefix_refinement sr isr osr rvr AR R (\s0. P s0 and P') (Q and Q') (a >>= (\rv. b rv)) (c >>= (\rv'. d rv'))" + apply (rule prefix_refinement_weaken_pre, + rule prefix_refinement_bind_general[where P'="\_. P'"]) + apply assumption + apply (elim meta_allE, erule(1) meta_mp) + apply (rule disjI2) + apply simp + apply assumption apply clarsimp apply clarsimp - apply (erule tmres.rel_cases; clarsimp) - apply (drule(1) validI_rvD, simp add: rely_def) - apply simp - apply (case_tac tr; clarsimp simp: list_all2_Cons2 matching_tr_def) done -lemmas prefix_refinement_validI' = prefix_refinement_validI[OF _ rg_strengthen_guar, OF _ rg_strengthen_post] +lemmas prefix_refinement_bind = prefix_refinement_bind_general[OF _ _ disjI1] -section \Building blocks.\ -text \ -Prefix refinement rules for various basic constructs. -\ +lemmas prefix_refinement_bind_sr = prefix_refinement_bind[where sr=sr and intsr=sr for sr] +lemmas prefix_refinement_bind_isr = prefix_refinement_bind[where isr=isr and intsr=isr for isr] +lemmas pfx_refn_bind = + prefix_refinement_bind_v[where sr=sr and isr=sr and osr=sr and intsr=sr for sr] +lemmas pfx_refn_bindT = + pfx_refn_bind[where P'="\" and Q'="\_ _. True", OF _ _ hoare_post_taut twp_post_taut, + simplified pred_conj_def, simplified] -lemma prefix_refinement_weaken_pre: - "prefix_refinement sr isr osr rvr P' Q' AR R f g - \ \s s0. P s0 s \ P' s0 s - \ (\s t s0 t0. isr s t \ sr s0 t0 \ P s0 s \ Q t0 t \ Q' t0 t) - \ prefix_refinement sr isr osr rvr P Q AR R f g" - by (fastforce simp: prefix_refinement_def) - -lemma prefix_refinement_name_pre: - "(\s s0 t t0. isr s t \ sr s0 t0 \ P s0 s \ Q t0 t - \ prefix_refinement sr isr osr rvr (\s0' s'. s0' = s0 \ s' = s) (\t0' t'. t0' = t0 \ t' = t) AR R f g) - \ prefix_refinement sr isr osr rvr P Q AR R f g" - by (fastforce simp: prefix_refinement_def) +\ \FIXME: these are copied from Corres_UL.thy, move somewhere that they can be shared\ +primrec rel_sum_comb :: + "('a \ 'b \ bool) \ ('c \ 'd \ bool) \ ('a + 'c \ 'b + 'd \ bool)" (infixl "\" 95) + where + "(f \ g) (Inr x) y = (\y'. y = Inr y' \ (g x y'))" + | "(f \ g) (Inl x) y = (\y'. y = Inl y' \ (f x y'))" + +lemma rel_sum_comb_r2[simp]: + "(f \ g) x (Inr y) = (\x'. x = Inr x' \ g x' y)" + apply (case_tac x, simp_all) + done + +lemma rel_sum_comb_l2[simp]: + "(f \ g) x (Inl y) = (\x'. x = Inl x' \ f x' y)" + apply (case_tac x, simp_all) + done + +lemma prefix_refinement_bindE_general: + "\prefix_refinement sr isr intsr (f \ rvr') AR R P Q a c; + \rv rv'. rvr' rv rv' \ prefix_refinement sr intsr osr (f \ rvr) AR R (P'' rv) (Q'' rv') (b rv) (d rv'); + \P'\,\AR\ a \\\\,\P''\,\E\ \ \\s. \s0. P' s0 s\ a \\rv s. \s0. P'' rv s0 s\,\\rv s. \s0. E rv s0 s\; + \Q'\,\R\ c \\\\,\Q''\,\E'\; + \rv s0 s rv' t0 t. \E rv s0 s; E' rv' t0 t; intsr s t\ \ osr s t\ + \ prefix_refinement sr isr osr (f \ rvr) AR R (P and P') (Q and Q') (a >>=E (\rv. b rv)) (c >>=E (\rv'. d rv'))" + apply (unfold bindE_def validIE_def validE_def) + apply (erule prefix_refinement_bind_general) + defer + apply (erule disj_forward; assumption?) + apply (fastforce simp: valid_def split_def split: sum.splits) + apply assumption + apply (case_tac rv; clarsimp simp: lift_def) + apply (rule prefix_refinement_throwError_imp) + apply clarsimp + done -lemma prefix_refinement_bind_v[rule_format]: - "prefix_refinement sr isr intsr rvr P Q AR R a c - \ (\x y. rvr x y \ prefix_refinement sr intsr osr rvr' (\s0. P'' x) (Q'' y) AR R (b x) (d y)) - \ \P'\ a \P''\ \ \Q'\,\R\ c \\\\,\Q''\ - \ prefix_refinement sr isr osr rvr' (\s0. P s0 and P') (Q and Q') AR R (a >>= b) (c >>= d)" +lemma prefix_refinement_bindE_v: + "\prefix_refinement sr isr intsr (f \ rvr') AR R P Q a c; + \rv rv'. rvr' rv rv' \ prefix_refinement sr intsr osr (f \ rvr) AR R (\_. P'' rv) (Q'' rv') (b rv) (d rv'); + \P'\ a \P''\,\E\; \Q'\,\R\ c \\\\,\Q''\,\E'\; + \rv s rv' t0 t. \E rv s; E' rv' t0 t; intsr s t\ \ osr s t\ + \ prefix_refinement sr isr osr (f \ rvr) AR R (\s0. P s0 and P') (Q and Q') (a >>=E (\rv. b rv)) (c >>=E (\rv'. d rv'))" apply (rule prefix_refinement_weaken_pre, - rule prefix_refinement_bind_general[where P'="\_. P'"]) - apply assumption - apply (elim allE, erule(1) mp) - apply (rule disjI2) - apply simp - apply assumption + rule prefix_refinement_bindE_general[where P'="\_. P'"and E="\rv _. E rv"]) + apply assumption + apply (elim meta_allE, erule(1) meta_mp) + apply (rule disjI2) + apply simp + apply assumption + apply clarsimp apply clarsimp apply clarsimp done -lemmas prefix_refinement_bind - = prefix_refinement_bind_general[OF _ _ disjI1] +lemmas prefix_refinement_bindE = prefix_refinement_bindE_general[OF _ _ disjI1] + +lemmas prefix_refinement_bindE_sr = prefix_refinement_bindE[where sr=sr and intsr=sr for sr] +lemmas prefix_refinement_bindE_isr = prefix_refinement_bindE[where isr=isr and intsr=isr for isr] +lemmas pfx_refn_bindE = + prefix_refinement_bindE_v[where sr=sr and isr=sr and osr=sr and intsr=sr for sr, where E="\\" and E'="\\\", + atomized, simplified, rule_format] (*this sequence of attributes removes a trivial assumption*) +lemmas pfx_refn_bindET = + pfx_refn_bindE[where P'="\" and Q'="\_ _. True", OF _ _ hoareE_TrueI twp_post_tautE, + simplified pred_conj_def, simplified] + +lemma prefix_refinement_handle: + "\prefix_refinement sr isr osr (rvr'' \ rvr) AR R P Q a c; + \ft ft'. rvr'' ft ft' \ prefix_refinement sr osr osr (rvr' \ rvr) AR R (E ft) (E' ft') (b ft) (d ft'); + \P'\,\AR\ a -,-,\E\; \Q'\,\R\ c -, -,\E'\\ + \ prefix_refinement sr isr osr (rvr' \ rvr) AR R (P and P') (Q and Q') (a (\ft. b ft)) (c (\ft'. d ft'))" + apply (simp add: handleE_def handleE'_def validIE_def) + apply (erule prefix_refinement_bind) + defer + apply assumption+ + apply (case_tac v; clarsimp) + apply (rule prefix_refinement_return_imp) + apply clarsimp + done -lemma default_prefix_refinement_ex: - "is_matching_fragment sr osr rvr ctr cres s0 R s - (\s. aprog s \ ({tr'. length tr' \ length ctr} \ UNIV)) - \ \f. is_matching_fragment sr osr rvr ctr cres s0 R s f - \ triv_refinement aprog f" - apply (intro exI conjI, assumption) - apply (simp add: triv_refinement_def) +lemma prefix_refinement_catch: + "\prefix_refinement sr isr osr (rvr' \ rvr) AR R P Q a c; + \ft ft'. rvr' ft ft' \ prefix_refinement sr osr osr rvr AR R (E ft) (E' ft') (b ft) (d ft'); + \P'\,\AR\ a -,-,\E\; \Q'\,\R\ c -, -,\E'\\ + \ prefix_refinement sr isr osr rvr AR R (P and P') (Q and Q') (a (\ft. b ft)) (c (\ft'. d ft'))" + apply (simp add: catch_def validIE_def) + apply (erule prefix_refinement_bind) + defer + apply assumption+ + apply (case_tac x; clarsimp) + apply (rule prefix_refinement_return_imp) + apply clarsimp done -lemma default_prefix_refinement_ex_match_iosr_R: - "is_matching_fragment sr osr rvr ctr cres s0 R s - (rely (\s. aprog s \ ({tr'. matching_tr_pfx iosr tr' ctr} \ UNIV)) R s0) - \ \f. is_matching_fragment sr osr rvr ctr cres s0 R s f - \ triv_refinement aprog f" - apply (intro exI conjI, assumption) - apply (clarsimp simp add: triv_refinement_def rely_def) +lemma prefix_refinement_handle_elseE: + "\prefix_refinement sr isr osr (fr' \ rvr') AR R P Q a c; + \ft ft'. fr' ft ft' \ prefix_refinement sr osr osr (fr \ rvr) AR R (E ft) (E' ft') (b ft) (d ft'); + \rv rv'. rvr' rv rv' \ prefix_refinement sr osr osr (fr \ rvr) AR R (P'' rv) (Q'' rv') (f rv) (g rv'); + \P'\,\AR\ a -,\P''\,\E\; \Q'\,\R\ c -, \Q''\,\E'\\ + \ prefix_refinement sr isr osr (fr \ rvr) AR R (P and P') (Q and Q') + (a (\ft. b ft) (\rv. f rv)) (c (\ft'. d ft') (\rv. g rv))" + apply (simp add: handle_elseE_def validIE_def) + apply (erule prefix_refinement_bind) + defer + apply assumption+ + apply (case_tac v; clarsimp) done -lemma is_matching_fragment_no_trace: - "is_matching_fragment sr osr rvr [] cres s0 R s (\s. {([], ares s)}) - = rel_tmres osr rvr (ares s) cres" - by (simp add: is_matching_fragment_def prefix_closed_def - self_closed_def env_closed_def - matching_tr_pfx_def matching_tr_def) +lemmas prefix_refinement_bind_eqr = prefix_refinement_bind[where rvr'="(=)", simplified] +lemmas prefix_refinement_bind_eqrE = prefix_refinement_bindE[where rvr'="(=)", simplified] -lemma prefix_refinement_return_imp: - "(\s s0 t0 t. P s0 s \ Q t0 t \ isr s t \ rvr rv rv' \ osr s t) - \ prefix_refinement sr isr osr rvr P Q AR R (return rv) (return rv')" - apply (clarsimp simp: prefix_refinement_def) - apply (rule default_prefix_refinement_ex) - apply (auto simp add: return_def is_matching_fragment_no_trace) +\ \FIXME: these are copied from Corres_UL.thy, move somewhere that they can be shared\ +definition + "dc \ \rv rv'. True" + +lemma dc_simp[simp]: "dc a b" + by (simp add: dc_def) + +lemma dc_o_simp1[simp]: "dc \ f = dc" + by (simp add: dc_def o_def) + +lemma dc_o_simp2[simp]: "dc x \ f = dc x" + by (simp add: dc_def o_def) + +lemma unit_dc_is_eq: + "(dc::unit\_\_) = (=)" + by (fastforce simp: dc_def) + +lemma prefix_refinement_bind_nor: + "\prefix_refinement sr isr intsr dc AR R P Q a c; + prefix_refinement sr intsr osr rvr AR R P'' Q'' b d; + \P'\, \AR\ a -, \\_. P''\; \Q'\, \R\ c -, \\_. Q''\\ + \ prefix_refinement sr isr osr rvr AR R (P and P') (Q and Q') (a >>= (\_. b)) (c >>= (\_. d))" + by (rule prefix_refinement_bind; assumption) + +lemma prefix_refinement_bind_norE: + "\prefix_refinement sr isr intsr (f \ dc) AR R P Q a c; + prefix_refinement sr intsr osr (f \ rvr) AR R P'' Q'' b d; + \P'\, \AR\ a -, \\_. P''\, \E\; \Q'\, \R\ c -, \\_. Q''\, \E'\; + \rv s0 s rv' t0 t. \E rv s0 s; E' rv' t0 t; intsr s t\ \ osr s t\ + \ prefix_refinement sr isr osr (f \ rvr) AR R (P and P') (Q and Q') (a >>=E (\_. b)) (c >>=E (\_. d))" + by (rule prefix_refinement_bindE; assumption) + +lemmas prefix_refinement_bind_mapr = prefix_refinement_bind[where rvr'="(=) \ g" for g, simplified] +lemmas prefix_refinement_bind_maprE = prefix_refinement_bindE[where rvr'="(=) \ g" for g, simplified] + + +section \Rules for walking prefix refinement into basic constructs\ + +lemma prefix_refinement_if: + "\G = G'; prefix_refinement sr isr osr rvr AR R P Q a c; + prefix_refinement sr isr osr rvr AR R P' Q' b d \ + \ prefix_refinement sr isr osr rvr AR R + (if G then P else P') (if G' then Q else Q') + (if G then a else b) (if G' then c else d)" + by simp + +\ \FIXME: copied from Word_Lib.Many_More, where would be a good spot to put it?\ +lemma if_apply_def2: + "(if P then F else G) = (\x y. (P \ F x y) \ (\ P \ G x y))" + by simp + +\ \FIXME: this could have slightly better bound variable names if written out, should we just do + that and avoid the previous FIXME?\ +lemmas prefix_refinement_if2 = prefix_refinement_if[unfolded if_apply_def2] + +lemma prefix_refinement_when: + "\G = G'; prefix_refinement sr isr isr rvr AR R P Q a c; rvr () ()\ + \ prefix_refinement sr isr isr rvr AR R (\x y. G \ P x y) (\x y. G' \ Q x y) + (when G a) (when G' c)" + unfolding when_def + apply clarsimp + apply (rule prefix_refinement_return_imp) + apply simp done -abbreviation(input) - "dc2 \ (\_ _. True)" +lemma prefix_refinement_whenE: + "\G = G'; prefix_refinement sr isr isr (f \ rvr) AR R P Q a c; rvr () ()\ + \ prefix_refinement sr isr isr (f \ rvr) AR R (\x y. G \ P x y) (\x y. G' \ Q x y) + (whenE G a) (whenE G' c)" + unfolding whenE_def returnOk_def + apply clarsimp + apply (rule prefix_refinement_return_imp) + apply simp + done + +lemma prefix_refinement_unless: + "\G = G'; prefix_refinement sr isr isr rvr AR R P Q a c; rvr () ()\ + \ prefix_refinement sr isr isr rvr AR R (\x y. \ G \ P x y) (\x y. \ G' \ Q x y) + (unless G a) (unless G' c)" + by (simp add: unless_def prefix_refinement_when) + +lemma prefix_refinement_unlessE: + "\G = G'; prefix_refinement sr isr isr (f \ rvr) AR R P Q a c; rvr () ()\ + \ prefix_refinement sr isr isr (f \ rvr) AR R (\x y. \ G \ P x y) (\x y. \ G' \ Q x y) + (unlessE G a) (unlessE G' c)" + by (simp add: unlessE_whenE prefix_refinement_whenE) + +lemma prefix_refinement_if_r: + "\G' \ prefix_refinement sr isr osr rvr AR R P Q a c; + \G' \ prefix_refinement sr isr osr rvr AR R P Q' a d \ + \ prefix_refinement sr isr osr rvr AR R + P (if G' then Q else Q') + a (if G' then c else d)" + by simp + +lemma prefix_refinement_if3: + "\G = G'; G' \ prefix_refinement sr isr osr rvr AR R P Q a c; + \G' \ prefix_refinement sr isr osr rvr AR R P' Q' b d \ + \ prefix_refinement sr isr osr rvr AR R + (if G then P else P') (if G' then Q else Q') + (if G then a else b) (if G' then c else d)" + by simp + +lemma prefix_refinement_if_strong: + "\\s0 s t0 t. \sr s0 t0; isr s t; P'' s0 s; Q'' t0 t\ \ G = G'; + \G; G'\ \ prefix_refinement sr isr osr rvr AR R P Q a c; + \\G; \G'\ \ prefix_refinement sr isr osr rvr AR R P' Q' b d \ + \ prefix_refinement sr isr osr rvr AR R + (P'' and (if G then P else P')) (Q'' and (if G' then Q else Q')) + (if G then a else b) (if G' then c else d)" + by (fastforce simp: prefix_refinement_def) + + +\ \FIXME: Put more thought into whether we want this section, and if not what alternative rules + would we want. The comment copied from Corres_UL suggests we might not want them. + They would be a fair bit more complicated to prove for prefix_refinement.\ +section \Some equivalences about liftM and other useful simps\ + +(* These rules are declared [simp], which in hindsight was not a good decision, because they + change the return relation which often is schematic when these rules apply in the goal. + In those circumstances it is usually safer to unfold liftM_def and proceed with the resulting + substituted term. + + (We leave the [simp] attribute here, because too many proofs now depend on it) +*) +(* +lemma prefix_refinement_liftM_simp[simp]: + "prefix_refinement sr isr osr rvr AR R P P' (liftM t f) g = + prefix_refinement sr isr osr (rvr \ t) AR R P P' f g" + by (auto simp: prefix_refinement_def triv_refinement_def in_liftM) + +lemma prefix_refinement_liftM2_simp[simp]: + "prefix_refinement sr isr osr rvr AR R P P' f (liftM t g) = + prefix_refinement sr isr osr (\x. rvr x \ t) AR R P P' f g" + by (fastforce simp: prefix_refinement_def in_liftM) + +lemma prefix_refinement_liftE_rel_sum[simp]: + "prefix_refinement sr isr osr (f \ rvr) AR R P P' (liftE m) (liftE m') = + prefix_refinement sr isr osr rvr AR R P P' m m'" + by (simp add: liftE_liftM o_def) + +lemmas corres_liftE_lift = corres_liftE_rel_sum[THEN iffD2]*) + + +section \Support for proving correspondence to noop with hoare triples\ + +lemma prefix_refinement_noop: + assumes P: "\s0 s. P s0 s \ \\t. isr s t \ Q t\ f \\rv t. osr s t \ rvr x rv\" + assumes nt: "no_trace f" + assumes nf: "\s0 s. P s0 s \ no_fail (\t. isr s t \ Q t) f" + shows "prefix_refinement sr isr osr rvr AR R P (\_. Q) (return x) f" + apply (subst prefix_refinement_no_trace) + apply (rule nt) + apply clarsimp + apply (frule P) + apply (insert nf) + apply (insert nt) + apply (clarsimp simp: valid_def no_fail_def no_trace_def return_def mres_def failed_def image_def) + apply (case_tac b; fastforce) + done + +lemma prefix_refinement_noopE: + assumes P: "\s0 s. P s0 s \ \\t. isr s t \ Q t\ f \\rv t. osr s t \ rvr x rv\,\\\\" + assumes nt: "no_trace f" + assumes nf: "\s0 s. P s0 s \ no_fail (\t. isr s t \ Q t) f" + shows "prefix_refinement sr isr osr (frvr \ rvr) AR R P (\_. Q) (returnOk x) f" +proof - + have Q: "\P f Q E. \P\f\Q\,\E\ \ \P\ f \\r s. case_sum (\e. E e s) (\r. Q r s) r\" + by (simp add: validE_def) + thus ?thesis + apply (simp add: returnOk_def) + apply (rule prefix_refinement_noop) + apply (rule hoare_strengthen_post) + apply (rule Q) + apply (rule P) + apply assumption + apply (simp split: sum.splits) + apply (rule nt) + apply (erule nf) + done +qed + +lemma prefix_refinement_noop2: + assumes f: "\s. P s \ \(=) s\ f \\\_. (=) s\" + assumes g: "\t. Q t \ \(=) t\ g \\_. (=) t\" + assumes nt: "no_trace f" "no_trace g" + assumes nf: "no_fail P f" "no_fail Q g" + shows "prefix_refinement sr iosr iosr dc AR R (\_. P) (\_. Q) f g" + apply (subst prefix_refinement_no_trace) + apply (rule nt) + apply clarsimp + apply (insert nt) + apply (insert nf) + apply (clarsimp simp: no_trace_def no_fail_def failed_def image_def) + apply (subgoal_tac "\(r, s')\mres (f s). rel_tmres iosr dc (Result (r, s')) b") + apply (case_tac b; fastforce simp: mres_def intro: rev_bexI) + apply (rule use_exs_valid) + apply (rule exs_hoare_post_imp[rotated]) + apply (erule f) + apply (case_tac b; clarsimp) + apply fastforce + apply fastforce + apply (subgoal_tac "ba = t") + apply simp + apply (rule sym) + apply (rule use_valid[OF _ g], erule in_mres) + apply simp+ + done + + +section \Support for dividing correspondence along logical boundaries\ + +lemma prefix_refinement_disj_division: + "\S \ T; S \ prefix_refinement sr isr osr rvr AR R P Q x y; + T \ prefix_refinement sr isr osr rvr AR R P' Q' x y\ + \ prefix_refinement sr isr osr rvr AR R + (\s0 s. (S \ P s0 s) \ (T \ P' s0 s)) (\s0 s. (S \ Q s0 s) \ (T \ Q' s0 s)) x y" + by (safe; pfx_refn_pre, simp+) + +lemma prefix_refinement_weaker_disj_division: + "\S \ T; S \ prefix_refinement sr isr osr rvr AR R P Q x y; + T \ prefix_refinement sr isr osr rvr AR R P' Q' x y\ + \ prefix_refinement sr isr osr rvr AR R (P and P') (Q and Q') x y" + by (pfx_refn_pre, rule prefix_refinement_disj_division, simp+) + +lemma prefix_refinement_symmetric_bool_cases: + "\S = T; \S; T\ \ prefix_refinement sr isr osr rvr AR R P Q f g; + \\S; \T\ \ prefix_refinement sr isr osr rvr AR R P' Q' f g\ + \ prefix_refinement sr isr osr rvr AR R (\s0 s. (S \ P s0 s) \ (\S \ P' s0 s)) + (\s0 s. (T \ Q s0 s) \ (\T \ Q' s0 s)) + f g" + by (cases S, simp_all) + +text \Support for symbolically executing into the guards and manipulating them\ + +lemma prefix_refinement_symb_exec_l: + assumes z: "\rv. prefix_refinement sr isr osr rvr AR R (\_. P' rv) Q (x rv) y" + assumes x: "\s. P s \ \(=) s\ m \\\r. (=) s\" + assumes y: "\P\ m \\rv s. P' rv s\" + assumes nf: "no_fail P m" + assumes nt: "no_trace m" + shows "prefix_refinement sr isr osr rvr AR R (\_. P) Q (m >>= (\rv. x rv)) y" + apply pfx_refn_pre + apply (subst gets_bind_ign[symmetric], rule prefix_refinement_bind[OF _ z]) + apply (rule prefix_refinement_noop2) + apply (erule x) + apply (rule gets_wp) + apply (rule nt) + apply (rule no_trace_gets) + apply (rule nf) + apply (rule no_fail_gets) + apply (rule valid_validI_wp[OF nt y]) + apply wp + apply simp+ + done + +lemma prefix_refinement_symb_exec_r: + assumes z: "\rv. prefix_refinement sr isr osr rvr AR R P (\_. Q' rv) x (y rv)" + assumes y: "\Q\ m \Q'\" + assumes x: "\s. Q s \ \(=) s\ m \\r. (=) s\" + assumes nf: "no_fail Q m" + assumes nt: "no_trace m" + shows "prefix_refinement sr isr osr rvr AR R P (\_. Q) x (m >>= (\rv. y rv))" + apply pfx_refn_pre + apply (subst gets_bind_ign[symmetric], rule prefix_refinement_bind[OF _ z]) + apply (rule prefix_refinement_noop2) + apply (clarsimp simp: simpler_gets_def exs_valid_def mres_def vimage_def) + apply (erule x) + apply (rule no_trace_gets) + apply (rule nt) + apply (rule no_fail_gets) + apply (rule nf) + apply wp + apply (rule valid_validI_wp[OF nt y]) + apply simp+ + done + +lemma prefix_refinement_symb_exec_r_conj: + assumes z: "\rv. prefix_refinement sr isr osr rvr AR R P (\_. Q' rv) x (y rv)" + assumes y: "\Q\ m \Q'\" + assumes x: "\s. \\s'. isr s s' \ S s'\ m \\rv s'. isr s s'\" + assumes nf: "\s. no_fail (\t. isr s t \ S t) m" + assumes nt: "no_trace m" + shows "prefix_refinement sr isr osr rvr AR R P (\_. S and Q) x (m >>= (\rv. y rv))" +proof - + have P: "prefix_refinement sr isr isr dc AR R \\ (\_. S) (return undefined) m" + apply (rule prefix_refinement_noop) + apply (simp add: x nt nf)+ + done + show ?thesis + apply pfx_refn_pre + apply (subst return_bind[symmetric], rule prefix_refinement_bind[OF P]) + apply (rule z) + apply wp + apply (rule valid_validI_wp[OF nt y]) + apply simp+ + done +qed + +\ \FIXME: improve automation of this proof\ +lemma prefix_refinement_bind_return_r: + "prefix_refinement sr isr osr (\x y. rvr x (h y)) AR R P Q f g \ + prefix_refinement sr isr osr rvr AR R P Q f (do x \ g; return (h x) od)" + apply (clarsimp simp: prefix_refinement_def bind_def return_def) + apply ((drule spec)+, (drule (1) mp)+) + apply (drule (1) bspec, clarsimp) + apply (subgoal_tac "aa=a") + prefer 2 + apply (fastforce split: tmres.splits) + apply clarsimp + apply (rule_tac x=fa in exI) + apply (clarsimp simp: is_matching_fragment_def split: tmres.splits) + apply (case_tac b; fastforce) + apply (case_tac b; fastforce) + apply (case_tac bc; fastforce) + done + +lemma prefix_refinement_symb_exec_l': + "\prefix_refinement sr isr isr dc AR R P P' f (return ()); + \rv. prefix_refinement sr isr osr rvr AR R (Q rv) P' (g rv) h; + \s0. \P s0\ f \\rv. Q rv s0\; no_trace f\ + \ prefix_refinement sr isr osr rvr AR R P P' (f >>= g) h" + apply (drule prefix_refinement_bind) + apply assumption + apply (erule valid_validI_wp) + apply assumption + apply wp + apply clarsimp + done + + +section \Building blocks\ + +lemma prefix_refinement_triv_pre: + "prefix_refinement sr isr osr rvr AR R \\ \\ f g + \ prefix_refinement sr isr osr rvr AR R \\ \\ f g" + by assumption + +\ \FIXME: Need to work out the best fragment to provide for prefix_refinement_trivial. + Defining and using prefix_close like this is one option but might be more work than needed.\ +\ \definition prefix_close_set :: + "((tmid \ 's) list \ ('s, 'a) tmres) set \ ((tmid \ 's) list \ ('s, 'a) tmres) set" + where + "prefix_close_set f = {(xs, Incomplete). (\xs' \ fst ` f. \n\length xs'. drop n xs' = xs)} \ f" + +definition prefix_close :: "('a, 'b) tmonad \ ('a, 'b) tmonad" where + "prefix_close f \ \s. prefix_close_set (f s)" + +lemma drop_Suc_eq: + "drop n xs = y # ys \ drop (Suc n) xs = ys" + by (auto simp: drop_Suc drop_tl) + +lemma prefix_close_set_closed: + "x # xs \ fst ` prefix_close_set (f s) \ (xs, Incomplete) \ prefix_close_set (f s)" + unfolding prefix_close_set_def + apply safe + apply (rule_tac x=aa in bexI) + apply (rule_tac x="Suc n" in exI) + apply (fastforce intro!: Suc_leI le_neq_trans elim!: drop_Suc_eq[OF sym]) + apply (auto simp: image_def intro!: bexI)[1] + apply (rule_tac x=a in bexI) + apply (rule_tac x="Suc 0" in exI) + apply fastforce + apply (auto simp: image_def intro!: bexI)[1] + done + +lemma prefix_close_closed: + "prefix_closed (prefix_close f)" + unfolding prefix_closed_def prefix_close_def + by (auto simp: prefix_close_set_closed) + +lemma triv_refinement_prefix_close: + "\prefix_closed f; triv_refinement f g\ \ triv_refinement f (prefix_close g)" + apply (clarsimp simp: triv_refinement_def) + oops + +lemma prefix_refinement_trivial: + "prefix_closed f \ pfx_refn (=) (=) R R \\ \\ f f" + apply (clarsimp simp: prefix_refinement_def) + apply (rule_tac x="prefix_close (\s'. if s'=s then {(a,b)} else {})" in exI) + apply (clarsimp simp: triv_refinement_def) +apply (auto simp: is_matching_fragment_def prefix_closed_def self_closed_def env_closed_def + matching_tr_pfx_def matching_tr_def)[1] +oops\ abbreviation - "pfx_refnT sr rvr \ pfx_refn sr rvr (\_ _. True) dc2" + "pfx_refnT sr rvr AR R \ pfx_refn sr rvr AR R \\ \\" -lemma pfx_refn_return: - "rvr rv rv' - \ pfx_refnT sr rvr AR R (return rv) (return rv')" +lemma prefix_refinement_returnTT: + "rvr rv rv' \ prefix_refinement sr iosr iosr rvr AR R \\ \\ (return rv) (return rv')" by (rule prefix_refinement_return_imp, simp) lemma prefix_refinement_get: - "prefix_refinement sr iosr iosr iosr dc2 dc2 AR R get get" - apply (clarsimp simp: prefix_refinement_def get_def) + "prefix_refinement sr iosr iosr iosr AR R \\ \\ get get" + by (rule prefix_refinement_get_imp, simp) + +lemma prefix_refinement_put_imp: + "\\s0 s t0 t. \sr s0 t0; isr s t; P s0 s; Q t0 t\ \ osr s' t'\ + \ prefix_refinement sr isr osr dc AR R P Q (put s') (put t')" + apply (clarsimp simp: prefix_refinement_def) apply (rule default_prefix_refinement_ex) - apply (simp add: is_matching_fragment_no_trace) + apply (clarsimp simp: put_def is_matching_fragment_no_trace) done lemma prefix_refinement_put: - "osr s t \ prefix_refinement sr isr osr dc2 dc2 dc2 AR R (put s) (put t)" - apply (clarsimp simp: prefix_refinement_def put_def) + "osr s t \ prefix_refinement sr isr osr dc AR R \\ \\ (put s) (put t)" + by (rule prefix_refinement_put_imp, simp) + +lemma prefix_refinement_modify: + "\\s0 s t0 t. \sr s0 t0; isr s t; P s0 s; Q t0 t\ \ osr (f s) (g t)\ + \ prefix_refinement sr isr osr dc AR R P Q (modify f) (modify g)" + apply (simp add: modify_def) + apply (rule prefix_refinement_weaken_pre) + apply (rule prefix_refinement_bind[where intsr=isr, OF prefix_refinement_get]) + apply (rule_tac P="\s0 _. P s0 s" and Q="\s0 _. Q s0 sa" in prefix_refinement_put_imp) + apply wpsimp+ + done + +lemmas prefix_refinement_modifyT = + prefix_refinement_modify[where P="\\" and Q="\\", simplified] + +lemmas pfx_refn_modifyT = + prefix_refinement_modifyT[where sr=sr and isr=sr and osr=sr for sr] + +lemmas prefix_refinement_get_pre = + prefix_refinement_bind[OF prefix_refinement_get _ valid_validI_wp[OF _ get_sp] + valid_validI_wp[OF _ get_sp], + simplified pred_conj_def, simplified] + +lemma prefix_refinement_gets: + "\\s t. \iosr s t; P s; Q t\ \ rvr (f s) (f' t)\ + \ prefix_refinement sr iosr iosr rvr AR R (\_. P) (\_. Q) (gets f) (gets f')" + apply (simp add: gets_def) + apply (rule prefix_refinement_get_pre) + apply (rule prefix_refinement_return_imp) + apply simp + done + +lemma prefix_refinement_fail: + "prefix_refinement sr isr osr rvr AR R \\ \\ fail fail" + apply (clarsimp simp: prefix_refinement_def fail_def) apply (rule default_prefix_refinement_ex) apply (simp add: is_matching_fragment_no_trace) done +lemma prefix_refinement_returnOkTT: + "rvr rv rv' \ prefix_refinement sr iosr iosr (rvr' \ rvr) AR R \\ \\ (returnOk rv) (returnOk rv')" + by (rule prefix_refinement_returnOk_imp, simp) + +lemma prefix_refinement_throwErrorTT: + "rvr e e' \ prefix_refinement sr iosr iosr (rvr \ rvr') AR R \\ \\ (throwError e) (throwError e')" + by (rule prefix_refinement_throwError_imp, simp) + lemma prefix_refinement_select: - "(\x \ T. \y \ S. rvr y x) - \ prefix_refinement sr iosr iosr rvr dc2 dc2 AR R (select S) (select T)" + "\\x \ T. \y \ S. rvr y x\ + \ prefix_refinement sr iosr iosr rvr AR R \\ \\ (select S) (select T)" apply (clarsimp simp: prefix_refinement_def select_def) apply (drule(1) bspec, clarsimp) apply (rule_tac x="return y" in exI) @@ -1103,36 +1798,267 @@ lemma prefix_refinement_select: apply (auto simp add: triv_refinement_def return_def image_def) done +lemma prefix_refinement_assert: + "P = P' \ prefix_refinement sr iosr iosr dc AR R \\ \\ (assert P) (assert P')" + by (simp add: assert_def prefix_refinement_fail prefix_refinement_return_imp) + +lemma prefix_refinement_assert_opt: + "\rel_option rvr v v'\ + \ prefix_refinement sr iosr iosr rvr AR R \\ \\ (assert_opt v) (assert_opt v')" + by (auto simp: assert_opt_def prefix_refinement_fail prefix_refinement_return_imp + split: option.splits) + +lemma prefix_refinement_assertE: + "P = P' \ prefix_refinement sr iosr iosr dc AR R \\ \\ (assertE P) (assertE P')" + by (simp add: assertE_def prefix_refinement_fail prefix_refinement_returnOk_imp) + +lemma prefix_refinement_gets_the: + "\\s t. \iosr s t; P s; Q t\ \ rel_option rvr (f s) (g t)\ + \ prefix_refinement sr iosr iosr rvr AR R (\_. P) (\_. Q) (gets_the f) (gets_the g)" + apply (simp add: gets_the_def) + apply (rule prefix_refinement_weaken_pre) + apply (rule prefix_refinement_bind[where rvr'="rel_option rvr"]) + apply (rule prefix_refinement_gets[where P=P and Q=Q]) + apply simp + apply (erule prefix_refinement_assert_opt) + apply wpsimp+ + done + +lemma prefix_refinement_gets_map: + "\\s t. \iosr s t; P s; Q t\ \ rel_option rvr (f s p) (g t q)\ + \ prefix_refinement sr iosr iosr rvr AR R (\_. P) (\_. Q) (gets_map f p) (gets_map g q)" + apply (subst gets_the_oapply_comp[symmetric])+ + apply (rule prefix_refinement_gets_the) + apply simp + done + +lemma prefix_refinement_throw_opt: + "\\s t. \iosr s t; P s; Q t\ \ rvr ex ex' \ rel_option rvr' x x'\ + \ prefix_refinement sr iosr iosr (rvr \ rvr') AR R (\_. P) (\_. Q) (throw_opt ex x) (throw_opt ex' x')" + apply (simp add: throw_opt_def) + apply (cases x; cases x') + apply (clarsimp simp: prefix_refinement_throwError_imp) + apply (fastforce simp: prefix_refinement_def) + apply (fastforce simp: prefix_refinement_def) + apply (clarsimp simp: prefix_refinement_returnOk_imp) + done + +lemma prefix_refinement_alternate1: + "prefix_refinement sr iosr iosr rvr AR R P Q a c \ prefix_refinement sr iosr iosr rvr AR R P Q (a \ b) c" + apply (subst prefix_refinement_def, clarsimp) + apply (drule(6) pfx_refnD2, clarsimp) + apply (fastforce intro: triv_refinement_trans[rotated] triv_refinement_alternative1) + done + +lemma prefix_refinement_alternate2: + "prefix_refinement sr iosr iosr rvr AR R P Q b c \ prefix_refinement sr iosr iosr rvr AR R P Q (a \ b) c" + apply (subst prefix_refinement_def, clarsimp) + apply (drule(6) pfx_refnD2, clarsimp) + apply (fastforce intro: triv_refinement_trans[rotated] triv_refinement_alternative2) + done + +lemma prefix_refinement_either_alternate1: + "\prefix_refinement sr iosr iosr rvr AR R P Q a c; prefix_refinement sr iosr iosr rvr AR R P' Q b c\ + \ prefix_refinement sr iosr iosr rvr AR R (P or P') Q (a \ b) c" + apply (subst prefix_refinement_def, clarsimp simp del: imp_disjL) + apply (erule disjE) + apply (drule(6) pfx_refnD2, clarsimp) + apply (fastforce intro: triv_refinement_trans[rotated] triv_refinement_alternative1) + apply (drule(6) pfx_refnD2, clarsimp) + apply (fastforce intro: triv_refinement_trans[rotated] triv_refinement_alternative2) + done + +lemma prefix_refinement_either_alternate2: + "\prefix_refinement sr iosr iosr rvr AR R P Q a c; prefix_refinement sr iosr iosr rvr AR R P Q' b c\ + \ prefix_refinement sr iosr iosr rvr AR R P (Q or Q') (a \ b) c" + apply (subst prefix_refinement_def, clarsimp simp del: imp_disjL) + apply (erule disjE) + apply (drule(6) pfx_refnD2, clarsimp) + apply (fastforce intro: triv_refinement_trans[rotated] triv_refinement_alternative1) + apply (drule(6) pfx_refnD2, clarsimp) + apply (fastforce intro: triv_refinement_trans[rotated] triv_refinement_alternative2) + done + +lemma is_matching_fragment_restrict: + "is_matching_fragment sr osr rvr ctr cres s0 R s f + \ is_matching_fragment sr osr rvr ctr cres s0 R s (\s'. if s'=s then f s else {})" + by (simp add: is_matching_fragment_def prefix_closed_def self_closed_def env_closed_def + matching_tr_pfx_def matching_tr_def) + +lemma triv_refinement_restrict: + "triv_refinement f (\s'. if s'=s then f s else {})" + by (clarsimp simp: triv_refinement_def) + +\ \FIXME: corres rules for condition don't exist, so maybe we don't bother with this. It feels + like it shouldn't be this hard to prove, but providing correct fragments is frustrating. + It might make it easier to instantiate if the exists was wrapped in a new definition.\ +lemma prefix_refinement_condition_strong: + "\\s0 s t0 t. \sr s0 t0; isr s t; P'' s0 s; Q'' t0 t\ \ C s = C' t; + prefix_refinement sr isr osr rvr AR R P Q a c; + prefix_refinement sr isr osr rvr AR R P' Q' b d \ + \ prefix_refinement sr isr osr rvr AR R + (P'' and (\s0 s. if C s then P s0 s else P' s0 s)) + (Q'' and (\s0 s. if C' s then Q s0 s else Q' s0 s)) + (condition C a b) (condition C' c d)" + apply (clarsimp simp: condition_def) + apply (auto simp: prefix_refinement_def simp del: not_ex ) + apply (erule notE) + apply (drule spec | drule (1) mp | drule (1) bspec)+ + apply clarsimp + apply (rule_tac x="\s'. if s'=s then f s else {}" in exI) + apply (clarsimp simp: triv_refinement_def is_matching_fragment_restrict) + apply (drule spec | drule (1) mp | drule (1) bspec)+ + apply clarsimp + apply (rule_tac x="\s'. if s'=s then f s else {}" in exI) + apply (clarsimp simp: triv_refinement_def is_matching_fragment_restrict) + apply (drule spec | drule (1) mp | drule (1) bspec)+ + apply clarsimp + apply (rule_tac x="\s'. if s'=s then f s else {}" in exI) + apply (clarsimp simp: triv_refinement_def is_matching_fragment_restrict) + apply (drule spec | drule (1) mp | drule (1) bspec)+ + apply clarsimp + apply (rule_tac x="\s'. if s'=s then f s else {}" in exI) + apply (clarsimp simp: triv_refinement_def is_matching_fragment_restrict) + done + +lemma prefix_refinement_mapM[rule_format]: + "\list_all2 xyr xs ys; + \x y. x \ set xs \ y \ set ys \ xyr x y + \ prefix_refinement sr intsr intsr rvr AR R P Q (f x) (g y); + \x. x \ set xs \ \P\,\AR\ f x \\_ _. True\,\\_. P\; + \y. y \ set ys \ \Q\,\R\ g y \\_ _. True\,\\_. Q\\ + \ prefix_refinement sr intsr intsr (list_all2 rvr) AR R P Q (mapM f xs) (mapM g ys)" + apply (induct xs ys rule: list_all2_induct) + apply (simp add: mapM_def sequence_def prefix_refinement_return_imp) + apply (clarsimp simp: mapM_Cons all_conj_distrib imp_conjR) + apply (rule prefix_refinement_weaken_pre) + apply (rule prefix_refinement_bind, assumption) + apply (rule prefix_refinement_bind, assumption) + apply (rule prefix_refinement_triv_pre, rule prefix_refinement_return_imp, simp) + apply wp + apply fastforce + apply (simp | wp | blast dest: validI_prefix_closed)+ + done + +lemma prefix_refinement_mapME[rule_format]: + "\list_all2 xyr xs ys; + \x y. x \ set xs \ y \ set ys \ xyr x y + \ prefix_refinement sr intsr intsr (F \ rvr) AR R P Q (f x) (g y); + \x. x \ set xs \ \P\,\AR\ f x \\_ _. True\,\\_. P\; + \y. y \ set ys \ \Q\,\R\ g y \\_ _. True\,\\_. Q\\ + \ prefix_refinement sr intsr intsr (F \ list_all2 rvr) AR R P Q (mapME f xs) (mapME g ys)" + apply (induct xs ys rule: list_all2_induct) + apply (simp add: mapME_def sequenceE_def prefix_refinement_returnOk_imp) + apply (clarsimp simp add: mapME_Cons all_conj_distrib imp_conjR) + apply (rule prefix_refinement_weaken_pre) + apply (unfold bindE_def validE_def) + apply (rule prefix_refinement_bind, assumption) + apply (case_tac rv) + apply (clarsimp simp: prefix_refinement_throwError_imp) + apply clarsimp + apply (rule prefix_refinement_bind, assumption) + apply (rule prefix_refinement_triv_pre) + apply (case_tac rv) + apply (clarsimp simp: prefix_refinement_throwError_imp) + apply (clarsimp simp: prefix_refinement_returnOk_imp) + apply (simp | wp | blast dest: validI_prefix_closed)+ + done + + +section \Some prefix_refinement rules for monadic combinators\ + +\ \FIXME: naming of these lemmas\ +lemma ifM_prefix_refinement: + assumes test: "prefix_refinement sr isr isr (=) AR R A A' test test'" + and l: "prefix_refinement sr isr osr rvr AR R P P' a a'" + and r: "prefix_refinement sr isr osr rvr AR R Q Q' b b'" + and abs_valid: "\B\,\AR\ test -,\\c s0 s. c \ P s0 s\" + "\C\,\AR\ test -,\\c s0 s. \ c \ Q s0 s\" + and conc_valid: "\B'\,\R\ test' -,\\c s0 s. c \ P' s0 s\" + "\C'\,\R\ test' -,\\c s0 s. \ c \ Q' s0 s\" + shows "prefix_refinement sr isr osr rvr AR R (A and B and C) (A' and B' and C') + (ifM test a b) (ifM test' a' b')" + unfolding ifM_def + apply pfx_refn_pre + apply (rule prefix_refinement_bind[OF test]) + apply (erule prefix_refinement_if[OF _ l r]) + apply (wpsimp wp: abs_valid conc_valid rg_vcg_if_lift2)+ + done + +lemmas ifM_prefix_refinement' = + ifM_prefix_refinement[where A=A and B=A and C=A for A, + where A'=A' and B'=A' and C'=A' for A', simplified] + +lemma orM_prefix_refinement: + "\prefix_refinement sr isr isr (=) AR R A A' a a'; prefix_refinement sr isr isr (=) AR R C C' b b'; + \B\,\AR\ a -,\\c s0 s. \ c \ C s0 s\; \B'\,\R\ a' -,\\c s0 s. \ c \ C' s0 s\\ + \ prefix_refinement sr isr isr (=) AR R (A and B) (A' and B') (orM a b) (orM a' b')" + unfolding orM_def + apply pfx_refn_pre + apply (rule ifM_prefix_refinement[where P="\\" and P'="\\"]) + apply (wpsimp | fastforce simp: prefix_refinement_return_imp)+ + done + +lemmas orM_prefix_refinement' = + orM_prefix_refinement[where A=A and B=A for A, simplified, where A'=A' and B'=A' for A', simplified] + +lemma andM_prefix_refinement: + "\prefix_refinement sr isr isr (=) AR R A A' a a'; prefix_refinement sr isr isr (=) AR R C C' b b'; + \B\,\AR\ a -,\\c s0 s. c \ C s0 s\; \B'\,\R\ a' -,\\c s0 s. c \ C' s0 s\\ + \ prefix_refinement sr isr isr (=) AR R (A and B) (A' and B') (andM a b) (andM a' b')" + unfolding andM_def + apply pfx_refn_pre + apply (rule ifM_prefix_refinement[where Q="\\" and Q'="\\"]) + apply (wpsimp | fastforce simp: prefix_refinement_return_imp)+ + done + +lemma notM_prefix_refinement: + "\prefix_refinement sr isr isr (=) AR R G G' a a'; prefix_closed a; prefix_closed a'\ + \ prefix_refinement sr isr isr (=) AR R G G' (notM a) (notM a')" + unfolding notM_def + apply pfx_refn_pre + apply (erule prefix_refinement_bind) + apply (rule prefix_refinement_returnTT) + apply wpsimp+ + done + +lemma whenM_prefix_refinement: + "\prefix_refinement sr isr isr (=) AR R A A' a a'; prefix_refinement sr isr isr dc AR R C C' b b'; + \B\,\AR\ a -,\\c s0 s. c \ C s0 s\; \B'\,\R\ a' -,\\c s0 s. c \ C' s0 s\\ + \ prefix_refinement sr isr isr dc AR R (A and B) (A' and B') (whenM a b) (whenM a' b')" + unfolding whenM_def + apply pfx_refn_pre + apply (rule ifM_prefix_refinement[where Q="\\" and Q'="\\"]) + apply (wpsimp | fastforce simp: prefix_refinement_return_imp)+ + done + + +section \prefix_refinement rules for env_step, commit_step, interference and Await\ +\ \FIXME: better name for section\ + lemma Int_insert_left2: "(insert a B \ C) = ((if a \ C then {a} else {}) \ (B \ C))" by auto -definition - rely_stable :: "('t \ 't \ bool) \ ('s \ 't \ bool) \ ('t \ bool) \ bool" -where +definition rely_stable :: "('t \ 't \ bool) \ ('s \ 't \ bool) \ ('t \ bool) \ bool" where "rely_stable R sr Q = (\s t t'. Q t \ sr s t \ R t t' \ Q t' \ (\s'. sr s' t'))" lemmas rely_stableD = rely_stable_def[THEN iffD1, simplified imp_conjL, rule_format] -definition - env_rely_stable_iosr :: "'s rg_pred \ 't rg_pred - \ ('s \ 't \ bool) \ ('s \ 't \ bool) \ ('t \ bool) \ bool" -where - "env_rely_stable_iosr AR R sr iosr Q - = (\s0 t0 s t. Q t0 \ iosr s0 t0 \ R t0 t \ AR s0 s \ sr s t \ iosr s t)" +definition env_rely_stable_iosr :: + "'s rg_pred \ 't rg_pred \ ('s \ 't \ bool) \ ('s \ 't \ bool) \ ('t \ bool) \ bool" + where + "env_rely_stable_iosr AR R sr iosr Q = + (\s0 t0 s t. Q t0 \ iosr s0 t0 \ R t0 t \ AR s0 s \ sr s t \ iosr s t)" lemmas env_rely_stable_iosrD = env_rely_stable_iosr_def[THEN iffD1, rule_format] -definition - env_stable :: "'s rg_pred \ 't rg_pred - \ ('s \ 't \ bool) \ ('s \ 't \ bool) \ ('t \ bool) \ bool" -where - "env_stable AR R sr iosr Q = (rely_stable R sr Q - \ env_rely_stable_iosr AR R sr iosr Q \ iosr \ sr)" +definition env_stable :: + "'s rg_pred \ 't rg_pred \ ('s \ 't \ bool) \ ('s \ 't \ bool) \ ('t \ bool) \ bool" + where + "env_stable AR R sr iosr Q = (rely_stable R sr Q \ env_rely_stable_iosr AR R sr iosr Q \ iosr \ sr)" -definition - abs_rely_stable :: "('s \ 's \ bool) \ ('s \ bool) \ bool" -where +definition abs_rely_stable :: "('s \ 's \ bool) \ ('s \ bool) \ bool" where "abs_rely_stable R P = (\s s'. P s \ R s s' \ P s')" lemmas abs_rely_stableD = abs_rely_stable_def[THEN iffD1, simplified imp_conjL, rule_format] @@ -1142,10 +2068,7 @@ lemma abs_rely_stableT: by (simp add: abs_rely_stable_def) lemma rely_stable_rtranclp: - "rely_stable R sr Q - \ sr s t \ Q t - \ rtranclp R t t' - \ Q t'" + "\rely_stable R sr Q; sr s t; Q t; rtranclp R t t'\ \ Q t'" apply (rotate_tac 3, induct arbitrary: s rule: converse_rtranclp_induct) apply simp apply (clarsimp simp: rely_stable_def) @@ -1153,9 +2076,7 @@ lemma rely_stable_rtranclp: done lemma abs_rely_stable_rtranclp: - "abs_rely_stable R P - \ P s \ rtranclp R s s' - \ P s'" + "\abs_rely_stable R P; P s; rtranclp R s s'\ \ P s'" apply (rotate_tac 2, induct rule: converse_rtranclp_induct) apply simp apply (clarsimp simp: abs_rely_stable_def) @@ -1163,8 +2084,8 @@ lemma abs_rely_stable_rtranclp: lemma prefix_refinement_env_step: assumes env_stable: "env_stable AR R sr iosr Q" - shows "prefix_refinement sr iosr iosr dc2 (\s0 s. s0 = s) (\t0 t. t0 = t \ Q t0) - AR R env_step env_step" + shows "prefix_refinement sr iosr iosr dc AR R (\s0 s. s0 = s) (\t0 t. t0 = t \ Q t0) + env_step env_step" proof - have P: "\S. {xs. length xs = Suc 0} = (\x. [x]) ` UNIV" apply (safe, simp_all) @@ -1186,9 +2107,9 @@ proof - apply (simp only: UN_extend_simps Int_insert_left2) apply (simp add: is_matching_fragment_def UN_If_distrib) apply (intro conjI allI impI; - simp add: prefix_closed_def in_fst_snd_image_eq self_closed_def - matching_tr_pfx_def matching_tr_def - env_closed_def) + simp add: prefix_closed_def in_fst_snd_image_eq self_closed_def + matching_tr_pfx_def matching_tr_def + env_closed_def) apply (metis env_rely_stable_iosrD[OF est]) apply clarsimp apply (auto dest: rely_stableD[OF st] predicate2D[OF sr])[1] @@ -1196,23 +2117,22 @@ proof - qed lemma prefix_refinement_repeat_n: - "prefix_refinement sr iosr iosr (\_ _. True) P Q AR R f g - \ \P\,\AR\ f \\\\,\\_. P\ - \ \\t0 t. Q t0 t \ (\s0 s. sr s0 t0 \ iosr s t)\,\R\ g \\\\,\\_. Q\ - \ prefix_refinement sr iosr iosr (\_ _. True) P Q AR R (repeat_n n f) (repeat_n n g)" + "\prefix_refinement sr iosr iosr dc AR R P Q f g; \P\,\AR\ f \\\\,\\_. P\; + \\t0 t. Q t0 t \ (\s0 s. sr s0 t0 \ iosr s t)\,\R\ g \\\\,\\_. Q\\ + \ prefix_refinement sr iosr iosr dc AR R P Q (repeat_n n f) (repeat_n n g)" apply (induct n) apply (simp add: prefix_refinement_return_imp) - apply (rule prefix_refinement_weaken_pre) + apply pfx_refn_pre apply simp - apply (rule prefix_refinement_bind, assumption+) + apply (rule prefix_refinement_bind, assumption+) apply simp apply auto done lemma prefix_refinement_env_n_steps: assumes env_stable: "env_stable AR R sr iosr Q" - shows "prefix_refinement sr iosr iosr (\_ _. True) - (=) (\t0 t. t0 = t \ Q t0) AR R (env_n_steps n) (env_n_steps n)" + shows "prefix_refinement sr iosr iosr dc AR R + (=) (\t0 t. t0 = t \ Q t0) (env_n_steps n) (env_n_steps n)" apply (rule prefix_refinement_repeat_n) apply (rule prefix_refinement_env_step[OF env_stable]) apply (simp add: env_step_def) @@ -1229,10 +2149,9 @@ lemma prefix_refinement_env_n_steps: done lemma prefix_refinement_repeat: - "prefix_refinement sr iosr iosr (\_ _. True) P Q AR R f g - \ \P\,\AR\ f \\\\,\\_. P\ - \ \\t0 t. Q t0 t \ (\s0 s. sr s0 t0 \ iosr s t)\,\R\ g \\\\,\\_. Q\ - \ prefix_refinement sr iosr iosr (\_ _. True) P Q AR R (repeat f) (repeat g)" + "\prefix_refinement sr iosr iosr dc AR R P Q f g; \P\,\AR\ f \\\\,\\_. P\; + \\t0 t. Q t0 t \ (\s0 s. sr s0 t0 \ iosr s t)\,\R\ g \\\\,\\_. Q\\ + \ prefix_refinement sr iosr iosr dc AR R P Q (repeat f) (repeat g)" apply (simp add: repeat_def) apply (rule prefix_refinement_weaken_pre) apply (rule prefix_refinement_bind, rule prefix_refinement_select[where rvr="(=)"]) @@ -1248,8 +2167,7 @@ lemma prefix_refinement_repeat: lemma prefix_refinement_env_steps: "env_stable AR R sr iosr Q - \ prefix_refinement sr iosr iosr (\_ _. True) - (=) (\t0 t. t0 = t \ Q t0) AR R env_steps env_steps" + \ prefix_refinement sr iosr iosr dc AR R (=) (\t0 t. t0 = t \ Q t0) env_steps env_steps" apply (simp add: env_steps_repeat) apply (rule prefix_refinement_repeat) apply (erule prefix_refinement_env_step) @@ -1266,7 +2184,7 @@ lemma prefix_refinement_env_steps: lemma prefix_refinement_commit_step: "\s t. isr s t \ sr s t \ osr s t - \ prefix_refinement sr isr osr (\_ _. True) (\\) (\\) AR R commit_step commit_step" + \ prefix_refinement sr isr osr dc AR R (\\) (\\) commit_step commit_step" apply (clarsimp simp: prefix_refinement_def) apply (rule default_prefix_refinement_ex) apply (simp add: commit_step_def bind_def get_def return_def put_trace_elem_def) @@ -1277,24 +2195,9 @@ lemma prefix_refinement_commit_step: apply (simp add: matching_tr_pfx_def matching_tr_def rely_cond_def) done -lemma prefix_refinement_weaken_srs: - "prefix_refinement sr isr osr r P Q AR R f g - \ isr' \ isr \ osr \ osr' \ sr \ sr - \ prefix_refinement sr isr' osr' r P Q AR R f g" - apply (subst prefix_refinement_def, clarsimp) - apply (drule(1) predicate2D) - apply (drule(5) prefix_refinementD) - apply clarsimp - apply (rule exI, rule conjI[rotated], assumption) - apply (clarsimp simp: is_matching_fragment_def) - apply (drule(1) bspec, clarsimp) - apply (erule tmres.rel_cases; clarsimp) - apply (erule(1) predicate2D) - done - lemma prefix_refinement_interference: "env_stable AR R sr iosr Q - \ prefix_refinement sr iosr iosr (\_ _. True) \\ (\t0 t. Q t) AR R interference interference" + \ prefix_refinement sr iosr iosr dc AR R \\ (\t0 t. Q t) interference interference" apply (simp add: interference_def) apply (rule prefix_refinement_weaken_pre) apply (rule prefix_refinement_bind[where intsr=iosr]) @@ -1309,67 +2212,31 @@ lemma prefix_refinement_interference: apply (clarsimp simp: guar_cond_def) done -lemma mapM_x_Cons: - "mapM_x f (x # xs) = do f x; mapM_x f xs od" - by (simp add: mapM_x_def sequence_x_def) - -lemmas prefix_refinement_bind_sr = prefix_refinement_bind[where sr=sr - and intsr=sr for sr] -lemmas prefix_refinement_bind_isr = prefix_refinement_bind[where isr=isr - and intsr=isr for isr] -lemmas pfx_refn_bind = prefix_refinement_bind_v[where sr=sr - and isr=sr and osr=sr and intsr=sr for sr] -lemmas pfx_refn_bindT - = pfx_refn_bind[where P'="\" and Q'="\_ _. True", OF _ _ hoare_post_taut validI_triv, - simplified pred_conj_def, simplified] - -lemma prefix_refinement_assume_pre: - "(P \ prefix_refinement sr isr osr rvr P' Q' AR R f g) - \ prefix_refinement sr isr osr rvr (P' and (\_ _. P)) Q' AR R f g" - "(P \ prefix_refinement sr isr osr rvr P' Q' AR R f g) - \ prefix_refinement sr isr osr rvr P' (Q' and (\_ _. P)) AR R f g" - by (auto simp: prefix_refinement_def) - -lemma prefix_refinement_modify: - "\s t. isr s t \ P s \ Q t \ osr (f s) (g t) - \ prefix_refinement sr isr osr (\_ _. True) (\_. P) (\_. Q) AR R (modify f) (modify g)" - apply (simp add: modify_def) - apply (rule prefix_refinement_weaken_pre) - apply (rule prefix_refinement_bind[where intsr=isr, OF prefix_refinement_get]) - apply (rule_tac P="P x" in prefix_refinement_assume_pre(1)) - apply (rule_tac P="Q y" in prefix_refinement_assume_pre(2)) - apply (rule prefix_refinement_put, simp) - apply wp+ +lemma prefix_refinement_Await: + "\env_stable AR R sr iosr Q; abs_rely_stable AR P; + \s t. P s \ Q t \ iosr s t \ G' t \ G s; + (\s. G' s) \ (\s. G s)\ + \ prefix_refinement sr iosr iosr (\_ _. True) AR R (\s0 s. s0 = s \ P s) (\t0 t. t0 = t \ Q t) + (Await G) (Await G')" + apply (simp add: Await_redef) + apply pfx_refn_pre + apply (rule prefix_refinement_bind[where intsr=iosr] + prefix_refinement_select[where rvr="\s s'. G s = G' s'"] + prefix_refinement_env_steps + | simp add: if_split[where P="\S. x \ S" for x] split del: if_split + | (rule prefix_refinement_get, rename_tac s s', + rule_tac P="P s" in prefix_refinement_gen_asm, + rule_tac P="Q s'" in prefix_refinement_gen_asm2) + | (rule prefix_refinement_select[where rvr="\\"]) + | wp)+ apply clarsimp - apply clarsimp - done - -lemmas pfx_refn_modifyT = prefix_refinement_modify[where P="\" and Q="\"] - -lemmas prefix_refinement_get_pre = - prefix_refinement_bind[OF prefix_refinement_get _ valid_validI_wp[OF _ get_sp] - valid_validI_wp[OF _ get_sp], - simplified pred_conj_def, simplified] - -lemma prefix_refinement_gets: - "\s t. iosr s t \ P s \ Q t \ rvr (f s) (f' t) - \ prefix_refinement sr iosr iosr rvr (\_. P) (\_. Q) AR R (gets f) (gets f')" - apply (simp add: gets_def) - apply (rule prefix_refinement_get_pre) - apply (rule prefix_refinement_return_imp) - apply simp + apply (erule(2) abs_rely_stable_rtranclp) + apply (clarsimp simp: env_stable_def) + apply (erule(3) rely_stable_rtranclp) done -lemma prefix_refinement_fail: - "prefix_refinement sr isr osr rvr \\ \\ AR R fail fail" - apply (clarsimp simp: prefix_refinement_def fail_def) - apply (rule default_prefix_refinement_ex) - apply (simp add: is_matching_fragment_no_trace) - done -lemma prefix_refinement_assert: - "P = P' \ prefix_refinement sr iosr iosr \\ \\ \\ AR R (assert P) (assert P')" - by (simp add: assert_def prefix_refinement_fail prefix_refinement_return_imp) +section \FIXME: name for this section\ lemma par_tr_fin_bind: "(\x. par_tr_fin_principle (g x)) \ par_tr_fin_principle (f >>= g)" @@ -1379,8 +2246,7 @@ lemma par_tr_fin_bind: done lemma par_tr_fin_add_env_n_steps: - "par_tr_fin_principle f - \ par_tr_fin_principle (do x \ f; env_n_steps n od)" + "par_tr_fin_principle f \ par_tr_fin_principle (do x \ f; env_n_steps n od)" proof (induct n) case 0 then show ?case by simp @@ -1416,93 +2282,24 @@ lemma par_tr_fin_interference: done lemma prefix_refinement_triv_refinement_abs: - "triv_refinement f f' - \ prefix_refinement sr isr osr rvr P Q AR R f' g - \ prefix_refinement sr isr osr rvr P Q AR R f g" + "\triv_refinement f f'; prefix_refinement sr isr osr rvr AR R P Q f' g\ + \ prefix_refinement sr isr osr rvr AR R P Q f g" apply (clarsimp simp: prefix_refinement_def) apply (strengthen triv_refinement_trans[mk_strg I E]) apply fastforce done lemma prefix_refinement_triv_refinement_conc: - "prefix_refinement sr isr osr rvr P Q AR R f g' - \ triv_refinement g' g - \ prefix_refinement sr isr osr rvr P Q AR R f g" + "\prefix_refinement sr isr osr rvr AR R P Q f g'; triv_refinement g' g\ + \ prefix_refinement sr isr osr rvr AR R P Q f g" apply (clarsimp simp: prefix_refinement_def triv_refinement_def) apply blast done -lemmas prefix_refinement_triv_pre - = Pure.asm_rl[where psi="prefix_refinement sr isr osr rvr - (\_ _. True) (\_ _. True) AR R f g"] for sr isr osr rvr AR R f g - -lemma prefix_refinement_mapM: - "list_all2 xyr xs ys - \ (\x y. x \ set xs \ y \ set ys \ xyr x y - \ prefix_refinement sr intsr intsr rvr P Q AR R (f x) (g y)) - \ (\x. x \ set xs \ \P\,\AR\ f x \\_ _. True\,\\_. P\) - \ (\y. y \ set ys \ \Q\,\R\ g y \\_ _. True\,\\_. Q\) - \ prefix_refinement sr intsr intsr (list_all2 rvr) P Q AR R (mapM f xs) (mapM g ys)" - apply (induct xs ys rule: list_all2_induct) - apply (simp add: mapM_def sequence_def prefix_refinement_return_imp) - apply (clarsimp simp add: mapM_Cons all_conj_distrib imp_conjR) - apply (rule prefix_refinement_weaken_pre) - apply (rule prefix_refinement_bind, assumption) - apply (rule prefix_refinement_bind, assumption) - apply (rule prefix_refinement_triv_pre, rule prefix_refinement_return_imp, simp) - apply (wp validI_triv)+ - apply (blast intro: validI_prefix_closed) - apply (wp validI_triv | simp add: pred_conj_def - | blast dest: validI_prefix_closed)+ - done - -lemma prefix_refinement_weaken_rel: - "prefix_refinement sr isr osr r P Q AR R f g - \ \rv rv'. r rv rv' \ r' rv rv' - \ prefix_refinement sr isr osr r' P Q AR R f g" - apply (subst prefix_refinement_def, clarsimp) - apply (drule(5) prefix_refinementD, clarsimp) - apply (rule exI, rule conjI[rotated], assumption) - apply (clarsimp simp: is_matching_fragment_def) - apply (drule(1) bspec, clarsimp) - apply (erule tmres.rel_cases; clarsimp) - done - -lemma rely_cond_mono: - "R \ R' \ rely_cond R \ rely_cond R'" - by (simp add: le_fun_def rely_cond_def split_def) -lemma is_matching_fragment_add_rely: - "is_matching_fragment sr osr r ctr cres s0 AR s f - \ AR' \ AR - \ is_matching_fragment sr osr r ctr cres s0 AR' s (rely f AR' s0)" - apply (frule is_matching_fragment_Nil) - apply (clarsimp simp: is_matching_fragment_def prefix_closed_rely - rely_self_closed) - apply (intro conjI) - apply (erule rely_env_closed) - apply (frule rely_cond_mono) - apply (simp add: le_fun_def rely_cond_Cons_eq) - apply (fastforce simp: rely_def) - apply (auto simp: rely_def)[1] - done - -lemma prefix_refinement_weaken_rely: - "prefix_refinement sr isr osr r P Q AR R f g - \ R' \ R \ AR' \ AR - \ prefix_refinement sr isr osr r P Q AR' R' f g" - apply (subst prefix_refinement_def, clarsimp) - apply (drule(3) prefix_refinementD, assumption+) - apply (clarsimp simp: rely_cond_def split_def le_fun_def) - apply (rule exI, rule conjI, erule is_matching_fragment_add_rely) - apply (simp add: le_fun_def) - apply (auto simp add: triv_refinement_def rely_def) - done - -text \Using prefix refinement as an in-place calculus, permitting -multiple applications at the same level.\ - -lemmas trivial = imp_refl[rule_format] +section \ + Using prefix refinement as an in-place calculus, permitting multiple applications at the + same level\ lemma matching_tr_transp: "transp sr \ transp (matching_tr sr)" @@ -1520,10 +2317,8 @@ lemma matching_tr_symp: done lemma list_all2_is_me: - "list_all2 P tr tr' - \ \x y. P x y \ fst x = fst y - \ (n < length tr \ fst (rev tr ! n) = Me) - = (n < length tr' \ fst (rev tr' ! n) = Me)" + "\list_all2 P tr tr'; \x y. P x y \ fst x = fst y\ + \ (n < length tr \ fst (rev tr ! n) = Me) = (n < length tr' \ fst (rev tr' ! n) = Me)" apply (rule conj_cong, simp add: list_all2_lengthD) apply (frule list_all2_rev_nthD, simp add: list_all2_lengthD) apply (cases "rev tr ! n", cases "rev tr' ! n", auto) @@ -1550,11 +2345,9 @@ proof - apply (simp add: matching_tr_pfx_def assms) apply (rule conj_cong; simp?) apply (strengthen iffI) - apply (metis matching_tr transpD[OF matching_tr_transp] - sympD[OF matching_tr_symp]) + apply (metis matching_tr transpD[OF matching_tr_transp] sympD[OF matching_tr_symp]) done - note is_me = matching_tr1[unfolded matching_tr_def, simplified, - THEN list_all2_is_me, symmetric] + note is_me = matching_tr1[unfolded matching_tr_def, simplified, THEN list_all2_is_me, symmetric] show ?thesis using assms apply (clarsimp simp: is_matching_fragment_def matching is_me) apply (drule(1) bspec)+ @@ -1566,10 +2359,8 @@ proof - qed lemma matching_tr_rely_cond: - "matching_tr sr (rev tr) (rev tr') - \ rely_cond R s0 tr - \ sr s0 t0 - \ rely_cond (\t0 t. \s0 s. sr s0 t0 \ sr s t \ R s0 s) t0 tr'" + "\matching_tr sr (rev tr) (rev tr'); rely_cond R s0 tr; sr s0 t0\ + \ rely_cond (\t0 t. \s0 s. sr s0 t0 \ sr s t \ R s0 s) t0 tr'" apply (simp add: matching_tr_def) apply (induct arbitrary: s0 t0 rule: list_all2_induct) apply simp @@ -1581,21 +2372,23 @@ lemma matching_tr_rely_cond: done lemma prefix_refinement_in_place_trans: - "prefix_refinement sr isr osr (=) P (\_ _. True) AR (\t0 t. \s0 s. sr s0 t0 \ sr s t \ R s0 s) f g - \ prefix_refinement sr isr osr (=) (\_ _. True) Q AR R g h - \ equivp sr \ equivp osr \ equivp isr - \ (\s t t'. sr s t \ R t t' \ (\s'. sr s' t' \ AR s s')) - \ prefix_refinement sr isr osr (=) P Q AR R f h" + "\prefix_refinement sr isr osr (=) AR (\t0 t. \s0 s. sr s0 t0 \ sr s t \ R s0 s) P (\_ _. True) f g; + prefix_refinement sr isr osr (=) AR R (\_ _. True) Q g h; + equivp sr; equivp osr; equivp isr; + \s t t'. sr s t \ R t t' \ (\s'. sr s' t' \ AR s s')\ + \ prefix_refinement sr isr osr (=) AR R P Q f h" apply (subst prefix_refinement_def, clarsimp) apply (drule_tac s=t and t=t and ?t0.0=t0 and cprog=h in pfx_refnD; - assumption?) + assumption?) apply (metis equivp_reflp_symp_transp reflpD) apply metis apply clarsimp apply (rename_tac h_tr h_res frag_g) apply (rule_tac x="\s. \(tr, res) \ frag_g t \ ({tr. length tr = length h_tr} \ UNIV). - \frag_f \ {frag_f. is_matching_fragment sr osr (=) tr res s0 AR s frag_f - \ triv_refinement f frag_f}. frag_f s" in exI) + \frag_f \ {frag_f. is_matching_fragment sr osr (=) tr res s0 AR s frag_f + \ triv_refinement f frag_f}. + frag_f s" + in exI) apply (rule conjI) apply (rule is_matching_fragment_UNION) apply clarsimp @@ -1622,29 +2415,4 @@ lemma prefix_refinement_in_place_trans: apply blast done -lemma prefix_refinement_Await: - "env_stable AR R sr iosr Q - \ abs_rely_stable AR P - \ \s t. P s \ Q t \ iosr s t \ G' t \ G s - \ (\s. G' s) \ (\s. G s) - \ prefix_refinement sr iosr iosr (\_ _. True) (\s0 s. s0 = s \ P s) - (\t0 t. t0 = t \ Q t) AR R - (Await G) (Await G')" - apply (simp add: Await_redef) - apply (rule prefix_refinement_weaken_pre) - apply (rule prefix_refinement_bind[where intsr=iosr] - prefix_refinement_select[where rvr="\s s'. G s = G' s'"] - prefix_refinement_env_steps - | simp add: if_split[where P="\S. x \ S" for x] split del: if_split - | (rule prefix_refinement_get, rename_tac s s', - rule_tac P="P s" in prefix_refinement_assume_pre(1), - rule_tac P="Q s'" in prefix_refinement_assume_pre(2)) - | (rule prefix_refinement_select[where rvr=dc2]) - | wp)+ - apply clarsimp - apply (erule(2) abs_rely_stable_rtranclp) - apply (clarsimp simp: env_stable_def) - apply (erule(3) rely_stable_rtranclp) - done - end diff --git a/lib/concurrency/Triv_Refinement.thy b/lib/concurrency/Triv_Refinement.thy index 1000f0efae..465d09f278 100644 --- a/lib/concurrency/Triv_Refinement.thy +++ b/lib/concurrency/Triv_Refinement.thy @@ -1,26 +1,30 @@ (* + * Copyright 2024, Proofcraft Pty Ltd * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) * * SPDX-License-Identifier: BSD-2-Clause *) theory Triv_Refinement - -imports - "Monads.Trace_More_RG" - "Monads.Trace_Strengthen_Setup" - + imports + "Monads.Trace_More_RG" + "Monads.Trace_Strengthen_Setup" begin -text \This is a simple (almost trivial) definition of refinement, -which simply resolves nondeterminism to a smaller set of options.\ -definition - triv_refinement :: "('s,'a) tmonad \ ('s,'a) tmonad \ bool" -where +text \ + This is a simple (almost trivial) definition of refinement, which simply resolves nondeterminism + to a smaller set of options.\ +definition triv_refinement :: "('s,'a) tmonad \ ('s,'a) tmonad \ bool" where "triv_refinement aprog cprog = (\s. cprog s \ aprog s)" +lemmas triv_refinement_elemD = triv_refinement_def[THEN iffD1, rule_format, THEN subsetD] + +lemma triv_refinement_trans: + "\triv_refinement f g; triv_refinement g h\ \ triv_refinement f h" + by (auto simp add: triv_refinement_def) + lemma triv_refinement_mono_bind: "triv_refinement a c \ triv_refinement (a >>= b) (c >>= b)" - "(\x. triv_refinement (b x) (d x)) \ triv_refinement (a >>= b) (a >>= d)" + "\\x. triv_refinement (b x) (d x)\ \ triv_refinement (a >>= b) (a >>= d)" apply (simp add: triv_refinement_def bind_def) apply (intro allI UN_mono; simp) apply (simp only: triv_refinement_def bind_def' split_def) @@ -28,15 +32,9 @@ lemma triv_refinement_mono_bind: apply simp done -lemma triv_refinement_trans: - "triv_refinement f g \ triv_refinement g h - \ triv_refinement f h" - by (auto simp add: triv_refinement_def) - lemma triv_refinement_bind: - "triv_refinement a c - \ (\x. triv_refinement (b x) (d x)) - \ triv_refinement (bind a b) (bind c d)" + "\triv_refinement a c; \x. triv_refinement (b x) (d x)\ + \ triv_refinement (bind a b) (bind c d)" by (metis triv_refinement_mono_bind triv_refinement_trans) lemma triv_refinement_mono_parallel: @@ -52,11 +50,10 @@ lemma triv_refinement_mono_parallel': done lemma triv_refinement_parallel: - "triv_refinement a b - \ triv_refinement c d - \ triv_refinement (parallel a c) (parallel b d)" + "\triv_refinement a b; triv_refinement c d\ + \ triv_refinement (parallel a c) (parallel b d)" by (metis triv_refinement_mono_parallel triv_refinement_mono_parallel' - triv_refinement_trans) + triv_refinement_trans) lemma select_subset: "(select S s \ select S' s') = (S \ S' \ (S \ {} \ s = s'))" @@ -71,52 +68,49 @@ lemma triv_refinement_select_eq: by (simp add: triv_refinement_def select_subset) lemma triv_refinement_rely: - "(\s0 s. R' s0 s \ R s0 s) \ - triv_refinement (rely f R s0) (rely f R' s0)" + "\\s0 s. R' s0 s \ R s0 s\ + \ triv_refinement (rely f R s0) (rely f R' s0)" unfolding rely_def triv_refinement_def rely_cond_def by auto lemma triv_refinement_rely2: - "triv_refinement f g \ - triv_refinement (rely f R s0) (rely g R s0)" + "triv_refinement f g \ triv_refinement (rely f R s0) (rely g R s0)" unfolding rely_def triv_refinement_def rely_cond_def by auto lemma rely_rely_triv_refinement: - "(\s0 s. R s0 s \ R' s0 s) \ - triv_refinement (rely f R' s0) (rely (rely f R s0) R' s0)" + "\\s0 s. R s0 s \ R' s0 s\ \ triv_refinement (rely f R' s0) (rely (rely f R s0) R' s0)" by (clarsimp simp: triv_refinement_def rely_def parallel_def) -lemma validI_triv_refinement: - "triv_refinement f g - \ \P\,\R\ f \G\,\Q\ - \ prefix_closed g - \ \P\,\R\ g \G\,\Q\" - unfolding rely_def triv_refinement_def validI_def - by fastforce - -lemma valid_triv_refinement: - "triv_refinement f g - \ \P\ f \Q\ - \ \P\ g \Q\" - unfolding rely_def triv_refinement_def valid_def mres_def - by (fastforce elim: image_eqI[rotated]) - -lemma triv_refinement_refl: +lemma triv_refinement_refl[simp]: "triv_refinement f f" by (simp add: triv_refinement_def) lemma triv_refinement_select_concrete_All: - "\x \ S. triv_refinement aprog (cprog x) - \ triv_refinement aprog (select S >>= cprog)" - by (auto simp add: triv_refinement_def bind_def select_def) + "\x \ S. triv_refinement aprog (cprog x) \ triv_refinement aprog (select S >>= cprog)" + by (auto simp: triv_refinement_def bind_def select_def) lemma triv_refinement_select_abstract_x: - "x \ S \ triv_refinement (aprog x) cprog - \ triv_refinement (select S >>= aprog) cprog" - by (auto simp add: triv_refinement_def bind_def select_def) + "\x \ S; triv_refinement (aprog x) cprog\ \ triv_refinement (select S >>= aprog) cprog" + by (auto simp: triv_refinement_def bind_def select_def) + +lemma triv_refinement_alternative1: + "triv_refinement (a \ b) a" + by (clarsimp simp: triv_refinement_def alternative_def) -lemmas triv_refinement_elemD - = triv_refinement_def[THEN iffD1, rule_format, THEN subsetD] +lemma triv_refinement_alternative2: + "triv_refinement (a \ b) b" + by (clarsimp simp: triv_refinement_def alternative_def) + + +lemma validI_triv_refinement: + "\triv_refinement f g; \P\,\R\ f \G\,\Q\; prefix_closed g\ \ \P\,\R\ g \G\,\Q\" + unfolding rely_def triv_refinement_def validI_def + by fastforce + +lemma valid_triv_refinement: + "\triv_refinement f g; \P\ f \Q\\ \ \P\ g \Q\" + unfolding rely_def triv_refinement_def valid_def mres_def + by (fastforce elim: image_eqI[rotated]) end diff --git a/lib/concurrency/examples/Peterson_Atomicity.thy b/lib/concurrency/examples/Peterson_Atomicity.thy index caf2483a69..04907808bb 100644 --- a/lib/concurrency/examples/Peterson_Atomicity.thy +++ b/lib/concurrency/examples/Peterson_Atomicity.thy @@ -15,8 +15,7 @@ text \ datatype ident = A | B -primrec other_ident -where +primrec other_ident where "other_ident A = B" | "other_ident B = A" @@ -34,7 +33,7 @@ lemma neq_A_B[simp]: lemma forall_ident_eq: "(\ident. P ident) = (P A \ P B)" using ident.nchotomy - by metis + by (metis (full_types)) lemma other_other_ident_simps[simp]: "other_ident (other_ident x) = x" @@ -43,14 +42,13 @@ lemma other_other_ident_simps[simp]: by (simp_all split: other_ident_split add: eq_commute) text \ -The state of the algorithm. The variables A/B are condensed into -an ab_v variable, so we can parametrise by thread A/B. The priority -variable is t_v, and the critical section cs has two variable to -operate on, cs1_v and cs2_v. + The state of the algorithm. The variables A/B are condensed into + an ab_v variable, so we can parametrise by thread A/B. The priority + variable is t_v, and the critical section cs has two variable to + operate on, cs1_v and cs2_v. -Labels are needed to track where we're up to for the preconditions, -relies and guarantees. -\ + Labels are needed to track where we're up to for the preconditions, + relies and guarantees.\ datatype label = Awaiting | Critical | Exited @@ -67,136 +65,107 @@ locale mx_locale = and csI :: "'b \ bool" begin -definition - set_ab :: "ident \ bool \ ('a, 'b) p_state \ ('a, 'b) p_state" -where +definition set_ab :: "ident \ bool \ ('a, 'b) p_state \ ('a, 'b) p_state" where "set_ab ident trying s = (s \ ab_v := (ab_v s) (ident := trying) \)" -definition - set_label :: "ident \ label \ ('a, 'b) p_state \ ('a, 'b) p_state" -where +definition set_label :: "ident \ label \ ('a, 'b) p_state \ ('a, 'b) p_state" where "set_label ident label s = (s \ ab_label := (ab_label s) (ident := label) \)" -definition - locked :: "ident \ ('a, 'b) p_state \ bool" -where +definition locked :: "ident \ ('a, 'b) p_state \ bool" where "locked ident s = (ab_v s (other_ident ident) \ t_v s = ident)" -definition - acquire_lock :: "ident \ (('a, 'b) p_state, unit) tmonad" -where +definition acquire_lock :: "ident \ (('a, 'b) p_state, unit) tmonad" where "acquire_lock ident = do - interference; - modify (set_ab ident True); - modify (\s. s \ t_v := other_ident ident \); - modify (set_label ident Awaiting); - interference; - Await (locked ident); - modify (set_label ident Critical) + interference; + modify (set_ab ident True); + modify (\s. s \ t_v := other_ident ident \); + modify (set_label ident Awaiting); + interference; + Await (locked ident); + modify (set_label ident Critical) od" -definition - release_lock :: "ident \ (('a, 'b) p_state, unit) tmonad" -where +definition release_lock :: "ident \ (('a, 'b) p_state, unit) tmonad" where "release_lock ident = do - modify (set_ab ident False); - modify (set_label ident Exited); - interference; - return () + modify (set_ab ident False); + modify (set_label ident Exited); + interference; + return () od" -definition - abs_critical_section :: "(('a, 'b) p_state, unit) tmonad" -where +definition abs_critical_section :: "(('a, 'b) p_state, unit) tmonad" where "abs_critical_section = do - interferences; - modify (\s. s \ cs1_v := cs1 (cs2_v s) \); - cs2; - interference - od" + interferences; + modify (\s. s \ cs1_v := cs1 (cs2_v s) \); + cs2; + interference + od" -definition - abs_peterson_proc :: - "ident \ (('a, 'b) p_state, unit) tmonad" -where +definition abs_peterson_proc :: "ident \ (('a, 'b) p_state, unit) tmonad" where "abs_peterson_proc ident = do - acquire_lock ident; - abs_critical_section; - release_lock ident - od" + acquire_lock ident; + abs_critical_section; + release_lock ident + od" -definition - critical_section :: "(('a, 'b) p_state, unit) tmonad" -where +definition critical_section :: "(('a, 'b) p_state, unit) tmonad" where "critical_section = do - interference; - modify (\s. s \ cs1_v := cs1 (cs2_v s) \); - interference; - cs2; - interference - od" + interference; + modify (\s. s \ cs1_v := cs1 (cs2_v s) \); + interference; + cs2; + interference + od" -definition - peterson_proc :: "ident \ (('a, 'b) p_state, unit) tmonad" -where +definition peterson_proc :: "ident \ (('a, 'b) p_state, unit) tmonad" where "peterson_proc ident = do - acquire_lock ident; - critical_section; - release_lock ident - od" + acquire_lock ident; + critical_section; + release_lock ident + od" abbreviation "critical label \ label = Critical" -text \The required invariant. We can't both be in the critical section. -Whenever neither of us is in the critical section, its invariant holds.\ -definition - req_peterson_inv :: "('a, 'b) p_state \ bool" -where - "req_peterson_inv s = (\ (critical (ab_label s A) \ critical (ab_label s B)) - \ (critical (ab_label s A) \ critical (ab_label s B) \ csI (cs2_v s)))" +text \ + The required invariant. We can't both be in the critical section. + Whenever neither of us is in the critical section, its invariant holds.\ +definition req_peterson_inv :: "('a, 'b) p_state \ bool" where + "req_peterson_inv s = + (\ (critical (ab_label s A) \ critical (ab_label s B)) + \ (critical (ab_label s A) \ critical (ab_label s B) \ csI (cs2_v s)))" -text \The key invariant. We can't both be enabled, where that means -either we're in the critical section or waiting to enter with priority. -\ -abbreviation(input) - enabled :: "ident \ ('a, 'b) p_state \ bool" -where - "enabled ident s \ (critical (ab_label s ident) - \ (ab_label s ident = Awaiting \ t_v s = ident))" +text \ + The key invariant. We can't both be enabled, where that means + either we're in the critical section or waiting to enter with priority.\ +abbreviation (input) enabled :: "ident \ ('a, 'b) p_state \ bool" where + "enabled ident s \ + critical (ab_label s ident) \ ab_label s ident = Awaiting \ t_v s = ident" -definition - key_peterson_inv :: "('a, 'b) p_state \ bool" -where +definition key_peterson_inv :: "('a, 'b) p_state \ bool" where "key_peterson_inv s = (\ (enabled A s \ enabled B s))" text \Some trivia about labels and variables.\ -definition - local_peterson_inv :: "('a, 'b) p_state \ bool" -where - "local_peterson_inv s - = (\ident. ab_label s ident \ Exited \ ab_v s ident)" +definition local_peterson_inv :: "('a, 'b) p_state \ bool" where + "local_peterson_inv s = (\ident. ab_label s ident \ Exited \ ab_v s ident)" definition - "invs s = (req_peterson_inv s - \ key_peterson_inv s \ local_peterson_inv s)" + "invs s = (req_peterson_inv s \ key_peterson_inv s \ local_peterson_inv s)" lemmas invs_defs = req_peterson_inv_def key_peterson_inv_def local_peterson_inv_def -definition - peterson_rel :: "ident \ ('a, 'b) p_state \ ('a, 'b) p_state \ bool" -where - "peterson_rel ident s_prior s = (\ \assume invs\ invs s_prior \ +definition peterson_rel :: "ident \ ('a, 'b) p_state \ ('a, 'b) p_state \ bool" where + "peterson_rel ident s_prior s = + (\ \assume invs\ invs s_prior \ \ \invariants are preserved\ (invs s \ \I won't adjust your variables\ - \ (ab_v s (other_ident ident) = ab_v s_prior (other_ident ident)) - \ (ab_label s (other_ident ident) = ab_label s_prior (other_ident ident)) + \ (ab_v s (other_ident ident) = ab_v s_prior (other_ident ident)) + \ (ab_label s (other_ident ident) = ab_label s_prior (other_ident ident)) \ \I will only ever give you priority\ - \ (t_v s_prior = other_ident ident \ t_v s = other_ident ident) + \ (t_v s_prior = other_ident ident \ t_v s = other_ident ident) \ \If you're in the critical section, I won't change cs2_v and cs1_v\ - \ (critical (ab_label s_prior (other_ident ident)) - \ cs2_v s = cs2_v s_prior \ cs1_v s = cs1_v s_prior) - ))" + \ (critical (ab_label s_prior (other_ident ident)) + \ cs2_v s = cs2_v s_prior \ cs1_v s = cs1_v s_prior)))" lemma peterson_rel_rtranclp[simp]: "rtranclp (peterson_rel ident) = (peterson_rel ident)" @@ -213,57 +182,56 @@ lemma reflp_peterson_rel[simp]: declare reflp_peterson_rel[THEN reflpD, simp] lemma peterson_rel_imp_assume_invs: - "invs x \ (peterson_rel ident x y \ invs x \ invs y \ P x y) - \ (peterson_rel ident x y \ P x y)" + "\invs x; peterson_rel ident x y \ invs x \ invs y \ P x y\ + \ peterson_rel ident x y \ P x y" by (simp add: peterson_rel_def) end text \ -We assume validity for the underspecified critical section code represented by -@{text cs2}. + We assume validity for the underspecified critical section code represented by + @{text cs2}. -We also assume some basic sanity properties about the structure of @{text cs2}. -\ + We also assume some basic sanity properties about the structure of @{text cs2}.\ locale mx_locale_wp = mx_locale cs1 cs2 csI for cs1 :: "'b \ 'a" and cs2 and csI + assumes cs_wp: "\s c. I s \ lockf s \ I s \ lockf (s \ cs2_v := c \) \ - \ \s0' s'. csI (cs2_v s') \ s0' = s0 \ s' = s \ I s \ lockf s - \ cs1_v s' = cs1 (cs2_v s') \, - \ \s0 s. I s0 \ lockf s0 \ cs2_v s = cs2_v s0 \ I s \ lockf s - \ cs1_v s = cs1_v s0 \ - cs2 - \ \s0 s. I s0 \ (\c. s = s0 \ cs2_v := c \) \ I s \ lockf s \, - \ \_ s0' s'. \c. csI c \ s' = s \ cs2_v := c \ - \ (\c'. s0' = s0 \ s0' = s \ cs2_v := c' \) - \ I s' \ lockf s' \" + \\s0' s'. csI (cs2_v s') \ s0' = s0 \ s' = s \ I s \ lockf s + \ cs1_v s' = cs1 (cs2_v s')\, + \\s0 s. I s0 \ lockf s0 \ cs2_v s = cs2_v s0 \ I s \ lockf s \ cs1_v s = cs1_v s0\ + cs2 + \\s0 s. I s0 \ (\c. s = s0 \ cs2_v := c \) \ I s \ lockf s\, + \\_ s0' s'. \c. csI c \ s' = s \ cs2_v := c \ + \ (\c'. s0' = s0 \ s0' = s \ cs2_v := c' \) + \ I s' \ lockf s'\" and cs_closed: "prefix_closed cs2" and cs_not_env_steps_first: "not_env_steps_first cs2" begin -method_setup rev_drule = \ - Attrib.thms >> curry (fn (thms, ctxt) - => SIMPLE_METHOD (dresolve_tac ctxt thms 1 #> Seq.list_of #> rev #> Seq.of_list)) -\ +method_setup rev_drule = + \Attrib.thms >> + curry (fn (thms, ctxt) => + SIMPLE_METHOD (dresolve_tac ctxt thms 1 #> Seq.list_of #> rev #> Seq.of_list))\ lemma cs2_wp_apply_peterson[wp]: - "\ (\s0 s. csI (cs2_v s) - \ invs s0 \ invs s \ critical (ab_label s ident) - \ cs1_v s = cs1 (cs2_v s) - \ (\s0' c' c. csI c \ (\c'. s0' = s0 \ s0' = s \ cs2_v := c' \) - \ Q () s0' (s \ cs2_v := c\))) \, - \ peterson_rel (other_ident ident) \ - cs2 - \ peterson_rel ident \, - \ Q \" + "\\s0 s. csI (cs2_v s) + \ invs s0 \ invs s \ critical (ab_label s ident) + \ cs1_v s = cs1 (cs2_v s) + \ (\s0' c' c. csI c \ (\c'. s0' = s0 \ s0' = s \ cs2_v := c' \) + \ Q () s0' (s \ cs2_v := c\))\, + \peterson_rel (other_ident ident)\ + cs2 + \peterson_rel ident\, + \Q\" apply (rule validI_name_pre[OF cs_closed], clarsimp simp del: imp_disjL) apply (rule rg_weaken_pre) apply (rule validI_well_behaved[OF cs_closed]) apply (rule rg_strengthen_post) apply (rule_tac s=s and ?s0.0=s0 - and lockf="\s. critical (ab_label s ident)" - and I="invs" in cs_wp) + and lockf="\s. critical (ab_label s ident)" + and I="invs" + in cs_wp) apply (clarsimp simp: invs_defs invs_def) apply (clarsimp simp del: imp_disjL) apply (simp only: imp_conjL[symmetric]) @@ -276,101 +244,85 @@ lemma cs2_wp_apply_peterson[wp]: done lemma release_lock_mutual_excl: - "\ \s0 s. peterson_rel ident s0 s \ invs s - \ ab_label s ident = Critical \ csI (cs2_v s) \, - \ peterson_rel (other_ident ident) \ - release_lock ident - \ peterson_rel ident \, - \ \rv s0 s. peterson_rel ident s0 s \ invs s - \ ab_label s ident = Exited \" + "\\s0 s. peterson_rel ident s0 s \ invs s \ ab_label s ident = Critical \ csI (cs2_v s)\, + \peterson_rel (other_ident ident)\ + release_lock ident + \peterson_rel ident\, + \\rv s0 s. peterson_rel ident s0 s \ invs s \ ab_label s ident = Exited\" apply (simp add: release_lock_def) apply wpsimp apply (strengthen peterson_rel_imp_assume_invs | simp)+ apply (cases ident) - apply (safe, simp_all) - by ((clarsimp simp: peterson_rel_def set_label_def - set_ab_def invs_defs - | rule invs_def[THEN iffD2] conjI - | rev_drule invs_def[THEN iffD1])+) + apply (safe, simp_all) + by (clarsimp simp: peterson_rel_def set_label_def set_ab_def invs_defs + | rule invs_def[THEN iffD2] conjI + | rev_drule invs_def[THEN iffD1])+ lemma abs_critical_section_mutual_excl: - "\ \s0 s. peterson_rel ident s0 s \ invs s \ invs s0 - \ ab_label s ident = Critical \ csI (cs2_v s) \, - \ peterson_rel (other_ident ident) \ - abs_critical_section - \ peterson_rel ident \, - \ \rv s0 s. peterson_rel ident s0 s \ invs s - \ ab_label s ident = Critical \ csI (cs2_v s) \" + "\\s0 s. peterson_rel ident s0 s \ invs s \ invs s0 \ ab_label s ident = Critical \ csI (cs2_v s)\, + \peterson_rel (other_ident ident)\ + abs_critical_section + \peterson_rel ident\, + \\rv s0 s. peterson_rel ident s0 s \ invs s \ ab_label s ident = Critical \ csI (cs2_v s)\" apply (simp add: abs_critical_section_def) apply wpsimp apply (strengthen peterson_rel_imp_assume_invs | simp)+ apply (cases ident) - apply (safe, simp_all) - by ((clarsimp simp: peterson_rel_def invs_defs - | rule invs_def[THEN iffD2] conjI - | rev_drule invs_def[THEN iffD1])+) + apply (safe, simp_all) + by (clarsimp simp: peterson_rel_def invs_defs + | rule invs_def[THEN iffD2] conjI + | rev_drule invs_def[THEN iffD1])+ lemma acquire_lock_mutual_excl: - "\ \s0 s. peterson_rel ident s0 s \ invs s - \ ab_label s ident = Exited \, - \ peterson_rel (other_ident ident) \ - acquire_lock ident - \ peterson_rel ident \, - \ \rv s0 s. peterson_rel ident s0 s \ invs s \ invs s0 - \ ab_label s ident = Critical \ csI (cs2_v s) \" + "\\s0 s. peterson_rel ident s0 s \ invs s \ ab_label s ident = Exited\, + \peterson_rel (other_ident ident)\ + acquire_lock ident + \peterson_rel ident\, + \\rv s0 s. peterson_rel ident s0 s \ invs s \ invs s0 + \ ab_label s ident = Critical \ csI (cs2_v s)\" apply (simp add: acquire_lock_def) apply (wpsimp wp: Await_sync_twp) apply (strengthen peterson_rel_imp_assume_invs | simp)+ apply (cases ident) - apply (safe, simp_all) - by ((clarsimp simp: peterson_rel_def set_label_def set_ab_def - locked_def invs_defs - | rule invs_def[THEN iffD2] conjI - | rev_drule invs_def[THEN iffD1])+) + apply (safe, simp_all) + by (clarsimp simp: peterson_rel_def set_label_def set_ab_def locked_def invs_defs + | rule invs_def[THEN iffD2] conjI + | rev_drule invs_def[THEN iffD1])+ theorem abs_peterson_proc_mutual_excl: - "\ \s0 s. peterson_rel ident s0 s \ invs s - \ ab_label s ident = Exited \, - \ peterson_rel (other_ident ident) \ - abs_peterson_proc ident - \ peterson_rel ident \, - \ \rv s0 s. peterson_rel ident s0 s \ invs s - \ ab_label s ident = Exited \" + "\\s0 s. peterson_rel ident s0 s \ invs s \ ab_label s ident = Exited\, + \peterson_rel (other_ident ident)\ + abs_peterson_proc ident + \peterson_rel ident\, + \\rv s0 s. peterson_rel ident s0 s \ invs s \ ab_label s ident = Exited\" apply (simp add: abs_peterson_proc_def bind_assoc) apply (wpsimp wp: release_lock_mutual_excl acquire_lock_mutual_excl abs_critical_section_mutual_excl) done -definition - peterson_sr :: "(('a, 'b) p_state \ ('a, 'b) p_state \ bool)" -where +definition peterson_sr :: "(('a, 'b) p_state \ ('a, 'b) p_state \ bool)" where "peterson_sr sa sc \ - t_v sa = t_v sc \ ab_v sa = ab_v sc - \ ab_label sa = ab_label sc \ cs2_v sa = cs2_v sc" + t_v sa = t_v sc \ ab_v sa = ab_v sc \ ab_label sa = ab_label sc \ cs2_v sa = cs2_v sc" -definition - peterson_sr' :: "(('a, 'b) p_state \ ('a, 'b) p_state \ bool)" -where +definition peterson_sr' :: "(('a, 'b) p_state \ ('a, 'b) p_state \ bool)" where "peterson_sr' sa sc \ sa = sc \ cs1_v := cs1_v sa \" -definition - peterson_sr_cs1 :: "(('a, 'b) p_state \ ('a, 'b) p_state \ bool)" -where +definition peterson_sr_cs1 :: "(('a, 'b) p_state \ ('a, 'b) p_state \ bool)" where "peterson_sr_cs1 sa sc \ peterson_sr sa sc \ cs1_v sa = cs1_v sc" end + text \ -Finally we assume that we can prove refinement for @{text cs2}, although this -may depend on being in a state where @{term cs1_v} has been correctly -initialised. -\ + Finally we assume that we can prove refinement for @{text cs2}, although this + may depend on being in a state where @{term cs1_v} has been correctly + initialised.\ locale mx_locale_refine = mx_locale_wp cs1 cs2 csI for cs1 :: "'b \ 'a" and cs2 and csI + assumes cs_refine: - "prefix_refinement peterson_sr peterson_sr_cs1 peterson_sr \\ - (\_ s. cs1_v s = cs1 (cs2_v s)) \\ - (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) - cs2 cs2" + "prefix_refinement peterson_sr peterson_sr_cs1 peterson_sr \\ + (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) + (\_ s. cs1_v s = cs1 (cs2_v s)) \\ + cs2 cs2" begin lemma @@ -378,7 +330,7 @@ lemma by (auto simp: p_state.splits peterson_sr_def peterson_sr'_def intro!: ext) lemma peterson_sr_set_ab[simp]: - "peterson_sr s t \ peterson_sr (set_ab ident v s) (set_ab ident v t)" + "peterson_sr s t \ peterson_sr (set_ab ident v s) (set_ab ident v t)" by (simp add: peterson_sr_def set_ab_def) lemma env_stable_peterson_sr: @@ -396,10 +348,11 @@ lemma peterson_sr_equivp[simp]: "equivp peterson_sr" by (auto simp: peterson_sr_def intro!: sympI equivpI transpI) -lemma peterson_sr_cs1_invs: "peterson_sr_cs1 s t \ invs s = invs t" - apply (auto simp: peterson_sr_def peterson_sr_cs1_def invs_def - req_peterson_inv_def key_peterson_inv_def - local_peterson_inv_def)[1] +lemma peterson_sr_cs1_invs: + "peterson_sr_cs1 s t \ invs s = invs t" + apply (auto simp: peterson_sr_def peterson_sr_cs1_def invs_def + req_peterson_inv_def key_peterson_inv_def + local_peterson_inv_def)[1] done lemma env_stable_peterson_sr_cs1: @@ -420,30 +373,30 @@ lemmas prefix_refinement_interference_peterson_cs1 = prefix_refinement_interference[OF env_stable_peterson_sr_cs1] lemmas prefix_refinement_bind_2left_2right - = prefix_refinement_bind[where a="bind a a'" and c="bind c c'" for a a' c c', simplified bind_assoc] + = prefix_refinement_bind[where a="Trace_Monad.bind a a'" and c="Trace_Monad.bind c c'" for a a' c c', simplified bind_assoc] lemmas rel_tr_refinement_bind_left_general_2left_2right - = rel_tr_refinement_bind_left_general[where f="bind f f'" and g="bind g g'" for f f' g g', simplified bind_assoc] + = rel_tr_refinement_bind_left_general[where f="Trace_Monad.bind f f'" and g="Trace_Monad.bind g g'" for f f' g g', + simplified bind_assoc] lemma peterson_rel_imp_invs: - "peterson_rel ident x y \ invs x \ invs y" + "\peterson_rel ident x y; invs x\ \ invs y" by (simp add: peterson_rel_def) lemma peterson_rel_imp_label: - "peterson_rel (other_ident ident) x y \ invs x + "\peterson_rel (other_ident ident) x y; invs x\ \ ab_label x ident = ab_label y ident" by (simp add: peterson_rel_def) lemma peterson_rel_set_label: - "peterson_rel (other_ident ident) (set_label ident label s) s' - \ invs (set_label ident label s) + "\peterson_rel (other_ident ident) (set_label ident label s) s'; invs (set_label ident label s)\ \ ab_label s' ident = label" by (simp add: peterson_rel_def set_label_def) lemma acquire_lock_refinement: - "prefix_refinement peterson_sr peterson_sr peterson_sr \\ - \\ \\ - (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) - (acquire_lock ident) (acquire_lock ident)" + "prefix_refinement peterson_sr peterson_sr peterson_sr dc + (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) + \\ \\ + (acquire_lock ident) (acquire_lock ident)" apply (unfold acquire_lock_def) apply (rule prefix_refinement_weaken_pre) apply (rule prefix_refinement_bind_sr) @@ -464,11 +417,11 @@ lemma acquire_lock_refinement: done lemma peterson_sr_invs[simp]: - "peterson_sr as cs \ invs as \ invs cs" + "\peterson_sr as cs; invs as\ \ invs cs" by (simp add: peterson_sr_def invs_def invs_defs) lemma peterson_sr_invs_sym: - "peterson_sr as cs \ invs cs \ invs as" + "\peterson_sr as cs; invs cs\ \ invs as" by (simp add: peterson_sr_def invs_def invs_defs) lemma peterson_sr_ab_label: @@ -476,12 +429,12 @@ lemma peterson_sr_ab_label: by (simp add: peterson_sr_def) lemma critical_section_refinement: - "prefix_refinement peterson_sr peterson_sr peterson_sr \\ - (\_ s. invs s \ ab_label s ident = Critical) \\ - (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) - abs_critical_section critical_section" + "prefix_refinement peterson_sr peterson_sr peterson_sr dc + (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) + (\_ s. invs s \ ab_label s ident = Critical) \\ + abs_critical_section critical_section" apply (simp add: abs_critical_section_def critical_section_def) - apply (rule prefix_refinement_weaken_pre) + apply pfx_refn_pre apply (rule prefix_refinement_interferences_split) apply (rule prefix_refinement_bind_sr) apply (rule prefix_refinement_interference_peterson) @@ -504,23 +457,23 @@ lemma critical_section_refinement: apply (rule prefix_refinement_bind_sr) apply (rule prefix_refinement_interference_peterson) apply (rule prefix_refinement_bind[where intsr=peterson_sr_cs1]) - apply (rule pfx_refn_modifyT) + apply (rule prefix_refinement_modifyT) apply (clarsimp simp add: peterson_sr_def peterson_sr_cs1_def) apply (rule prefix_refinement_bind_sr) apply (rule cs_refine) apply (rule prefix_refinement_interference_peterson) - apply (wpsimp wp: validI_triv[OF cs_closed])+ + apply (wpsimp wp: cs_closed)+ apply (subst peterson_rel_imp_label[symmetric], assumption, simp) apply (drule peterson_rel_imp_invs, simp) apply (simp add: peterson_sr_ab_label) done lemma release_lock_refinement: - "prefix_refinement peterson_sr peterson_sr peterson_sr \\ - \\ \\ - (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) - (release_lock ident) (release_lock ident)" + "prefix_refinement peterson_sr peterson_sr peterson_sr dc + (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) + \\ \\ + (release_lock ident) (release_lock ident)" apply (unfold release_lock_def) apply (rule prefix_refinement_weaken_pre) apply (simp add: modify_modify_bind) @@ -542,21 +495,21 @@ lemma abs_critical_section_prefix_closed[simp]: simp: cs_closed abs_critical_section_def) lemma peterson_rel_trans: - "peterson_rel ident x y \ peterson_rel ident y z \ - peterson_rel ident x z" - by (clarsimp simp: peterson_rel_def) + "\peterson_rel ident x y; peterson_rel ident y z\ + \ peterson_rel ident x z" + by (clarsimp simp: peterson_rel_def) lemma invs_set_label_Critical: - "invs s \ locked ident s \ ab_label s ident = Awaiting + "\invs s; locked ident s; ab_label s ident = Awaiting\ \ invs (set_label ident Critical s)" by (auto simp: invs_def invs_defs set_label_def locked_def) lemma acquire_lock_wp: - "\ \s0 s. invs s \ ab_label s ident = Exited \, - \ peterson_rel (other_ident ident) \ - acquire_lock ident - \ \\ \, - \ \rv s0 s. invs s \ ab_label s ident = Critical \" + "\\s0 s. invs s \ ab_label s ident = Exited\, + \peterson_rel (other_ident ident)\ + acquire_lock ident + \\\\, + \\rv s0 s. invs s \ ab_label s ident = Critical\" apply (simp add: acquire_lock_def) apply (wpsimp wp: Await_sync_twp) apply (subst (asm) peterson_rel_imp_label, assumption+) @@ -579,45 +532,42 @@ lemma acquire_lock_prefix_closed[simp]: simp: cs_closed acquire_lock_def) theorem peterson_proc_refinement: - "prefix_refinement peterson_sr peterson_sr peterson_sr \\ - (\_ s. invs s \ ab_label s ident = Exited) - (\_ s. invs s \ ab_label s ident = Exited) - (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) - (abs_peterson_proc ident) - (peterson_proc ident)" - apply (simp add: abs_peterson_proc_def peterson_proc_def) - apply (rule prefix_refinement_weaken_pre) - apply (rule prefix_refinement_bind_sr) + "prefix_refinement peterson_sr peterson_sr peterson_sr dc + (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) + (\_ s. invs s \ ab_label s ident = Exited) + (\_ s. invs s \ ab_label s ident = Exited) + (abs_peterson_proc ident) + (peterson_proc ident)" + apply (simp add: abs_peterson_proc_def peterson_proc_def) + apply (rule prefix_refinement_weaken_pre) + apply (rule prefix_refinement_bind_sr) apply (rule acquire_lock_refinement) apply (rule prefix_refinement_bind_sr) apply (rule critical_section_refinement) apply (rule release_lock_refinement) - apply (wpsimp wp: validI_triv acquire_lock_wp + apply (wpsimp wp: acquire_lock_wp simp: pred_conj_def)+ done -definition - peterson_rel2 :: "ident \ ('a, 'b) p_state \ ('a, 'b) p_state \ bool" -where - "peterson_rel2 ident s_prior s = (\ \assume invs\ invs s_prior \ - \ \If you're in the critical section, I won't change cs1_v\ - (critical (ab_label s_prior (other_ident ident)) - \ cs1_v s = cs1_v s_prior))" +definition peterson_rel2 :: "ident \ ('a, 'b) p_state \ ('a, 'b) p_state \ bool" where + "peterson_rel2 ident s_prior s = + (\ \assume invs\ invs s_prior \ + \ \If you're in the critical section, I won't change cs1_v\ + (critical (ab_label s_prior (other_ident ident)) \ cs1_v s = cs1_v s_prior))" -definition - peterson_rel3 :: "ident \ ('a, 'b) p_state \ ('a, 'b) p_state \ bool" -where - "peterson_rel3 ident s_prior s = (\ \assume invs\ invs s_prior \ - \ \invariants are preserved\ +definition peterson_rel3 :: "ident \ ('a, 'b) p_state \ ('a, 'b) p_state \ bool" where + "peterson_rel3 ident s_prior s = + (\ \assume invs\ invs s_prior \ + \ \invariants are preserved\ (invs s \ \I won't adjust your variables\ - \ (ab_v s (other_ident ident) = ab_v s_prior (other_ident ident)) - \ (ab_label s (other_ident ident) = ab_label s_prior (other_ident ident)) + \ (ab_v s (other_ident ident) = ab_v s_prior (other_ident ident)) + \ (ab_label s (other_ident ident) = ab_label s_prior (other_ident ident)) \ \I will only ever give you priority\ - \ (t_v s_prior = other_ident ident \ t_v s = other_ident ident) + \ (t_v s_prior = other_ident ident \ t_v s = other_ident ident) \ \If you're in the critical section, I won't change cs2_v\ - \ (critical (ab_label s_prior (other_ident ident)) - \ cs2_v s = cs2_v s_prior)))" + \ (critical (ab_label s_prior (other_ident ident)) + \ cs2_v s = cs2_v s_prior)))" lemma peterson_rel_helpers: "peterson_rel2 ident s0 s \ peterson_rel3 ident s0 s @@ -629,8 +579,8 @@ lemma peterson_rel_peterson_rel2: by (clarsimp simp: peterson_rel_def peterson_rel2_def) lemma peterson_sr_peterson_rel3: - "peterson_sr as0 cs0 \ peterson_sr as cs - \ peterson_rel ident as0 as \ peterson_rel3 ident cs0 cs" + "\peterson_sr as0 cs0; peterson_sr as cs; peterson_rel ident as0 as\ + \ peterson_rel3 ident cs0 cs" apply (clarsimp simp: peterson_rel_def peterson_rel3_def invs_def invs_defs peterson_sr_ab_label) apply (clarsimp simp: peterson_sr_def) @@ -642,36 +592,31 @@ lemma peterson_proc_prefix_closed[simp]: simp: cs_closed peterson_proc_def acquire_lock_def release_lock_def) lemma peterson_proc_mutual_excl_helper: - "\ \s0 s. peterson_rel ident s0 s \ invs s - \ ab_label s ident = Exited \, - \ peterson_rel (other_ident ident) \ - peterson_proc ident - \ peterson_rel3 ident \, - \ \rv s0 s. peterson_rel3 ident s0 s \ invs s - \ ab_label s ident = Exited \" - apply (rule prefix_refinement_validI') + "\\s0 s. peterson_rel ident s0 s \ invs s \ ab_label s ident = Exited\, + \peterson_rel (other_ident ident)\ + peterson_proc ident + \peterson_rel3 ident\, + \\rv s0 s. peterson_rel3 ident s0 s \ invs s \ ab_label s ident = Exited\" + apply (rule prefix_refinement_validI) apply (rule peterson_proc_refinement) apply (rule abs_peterson_proc_mutual_excl) - apply (clarsimp simp: peterson_sr_peterson_rel3 peterson_sr_ab_label) - apply (clarsimp simp: peterson_sr_peterson_rel3) - apply clarsimp - apply (rule_tac x=t0 in exI) - apply (rule_tac x="t \cs1_v := cs1_v t0\" in exI) - apply (clarsimp simp: peterson_rel_def peterson_sr_def) - apply clarsimp - apply (rule_tac x="t \cs1_v := cs1_v s0\" in exI) - apply (clarsimp simp: peterson_rel_def peterson_sr_def invs_def invs_defs) + apply clarsimp + apply (rule_tac x=t0 in exI) + apply (rule_tac x="t \cs1_v := cs1_v t0\" in exI) + apply (clarsimp simp: peterson_rel_def peterson_sr_def) + apply (rule_tac x="t \cs1_v := cs1_v s0\" in exI) + apply (clarsimp simp: peterson_rel_def peterson_sr_def invs_def invs_defs) + apply (clarsimp simp: peterson_sr_peterson_rel3) + apply (clarsimp simp: peterson_sr_peterson_rel3 peterson_sr_ab_label) apply clarsimp done lemma peterson_proc_mutual_excl_helper': - "\ \s0 s. peterson_rel ident s0 s \ invs s - \ ab_label s ident = Exited \, - \ peterson_rel (other_ident ident) \ - peterson_proc ident - \ peterson_rel2 ident \, - \ \rv s0 s. peterson_rel2 ident s0 s \ invs s - \ ab_label s ident = Exited \" + "\\s0 s. peterson_rel ident s0 s \ invs s \ ab_label s ident = Exited\, + \peterson_rel (other_ident ident)\ + peterson_proc ident + \peterson_rel2 ident\, + \\rv s0 s. peterson_rel2 ident s0 s \ invs s \ ab_label s ident = Exited\" apply (simp add: peterson_proc_def acquire_lock_def release_lock_def critical_section_def) apply (wp Await_sync_twp | simp add: split_def @@ -679,34 +624,32 @@ lemma peterson_proc_mutual_excl_helper': apply (clarsimp simp: imp_conjL) apply (strengthen peterson_rel_imp_assume_invs | simp)+ apply (cases ident) - apply (safe, simp_all) - by ((clarsimp simp: peterson_rel_def peterson_rel2_def forall_ident_eq - set_label_def set_ab_def locked_def invs_defs cs_closed - | rule invs_def[THEN iffD2] conjI - | rev_drule invs_def[THEN iffD1])+) + apply (safe, simp_all) + by (clarsimp simp: peterson_rel_def peterson_rel2_def forall_ident_eq + set_label_def set_ab_def locked_def invs_defs cs_closed + | rule invs_def[THEN iffD2] conjI + | rev_drule invs_def[THEN iffD1])+ lemma peterson_proc_mutual_excl: - "\ \s0 s. peterson_rel ident s0 s \ invs s - \ ab_label s ident = Exited \, - \ peterson_rel (other_ident ident) \ - peterson_proc ident - \ peterson_rel ident \, - \ \rv s0 s. peterson_rel ident s0 s \ invs s - \ ab_label s ident = Exited \" + "\\s0 s. peterson_rel ident s0 s \ invs s \ ab_label s ident = Exited\, + \peterson_rel (other_ident ident)\ + peterson_proc ident + \peterson_rel ident\, + \\rv s0 s. peterson_rel ident s0 s \ invs s \ ab_label s ident = Exited\" apply (rule rg_strengthen_guar, rule rg_strengthen_post, rule validI_guar_post_conj_lift) apply (rule peterson_proc_mutual_excl_helper) apply (rule peterson_proc_mutual_excl_helper') apply (clarsimp simp: peterson_rel_helpers)+ done -definition "abs_peterson_proc_system \ +definition + "abs_peterson_proc_system \ parallel (do repeat (abs_peterson_proc A); interference od) (do repeat (abs_peterson_proc B); interference od)" lemma validI_repeat_interference: - "\P\, \R\ f \G\, \\_. P\ - \ \s0 s. P s0 s \ (\s'. R\<^sup>*\<^sup>* s s' \ Q () s' s') \ G s0 s - \ \P\, \R\ do repeat f; interference od \G\, \Q\" + "\\P\,\R\ f \G\,\\_. P\; \s0 s. P s0 s \ (\s'. R\<^sup>*\<^sup>* s s' \ Q () s' s') \ G s0 s\ + \ \P\,\R\ do repeat f; interference od \G\,\Q\" apply (rule bind_twp) apply simp apply (rule interference_twp) @@ -716,11 +659,11 @@ lemma validI_repeat_interference: done lemma abs_peterson_proc_system_mutual_excl: - "\ \s0 s. s0 = s \ invs s \ ab_label s = (\_. Exited) \, - \ \s0 s. s0 = s \ - abs_peterson_proc_system - \ \s0 s. invs s0 \ invs s \, - \ \rv s0 s. invs s \" + "\\s0 s. s0 = s \ invs s \ ab_label s = (\_. Exited)\, + \\s0 s. s0 = s\ + abs_peterson_proc_system + \\s0 s. invs s0 \ invs s\, + \\rv s0 s. invs s\" apply (rule rg_weaken_pre, rule rg_strengthen_post) apply (unfold abs_peterson_proc_system_def) apply (rule rg_validI[where Qf="\_ _. invs" and Qg="\_ _. invs"]) @@ -729,10 +672,11 @@ lemma abs_peterson_proc_system_mutual_excl: apply (rule validI_repeat_interference[OF abs_peterson_proc_mutual_excl]) apply (clarsimp simp: peterson_rel_imp_invs) apply (simp add: reflp_ge_eq)+ - apply (clarsimp simp: peterson_rel_def)+ + apply (clarsimp simp: peterson_rel_def)+ done -definition "peterson_proc_system \ +definition + "peterson_proc_system \ parallel (do repeat (peterson_proc A); interference od) (do repeat (peterson_proc B); interference od)" @@ -742,16 +686,16 @@ lemma abs_peterson_proc_prefix_closed[simp]: simp: cs_closed abs_peterson_proc_def acquire_lock_def release_lock_def) lemma peterson_repeat_refinement: - "prefix_refinement peterson_sr peterson_sr peterson_sr \\ - (\s0 s. peterson_rel ident s0 s \ invs s \ ab_label s ident = Exited) - (\s0 s. peterson_rel ident s0 s \ invs s \ ab_label s ident = Exited) - (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) - (do repeat (abs_peterson_proc ident); - interference - od) - (do repeat (peterson_proc ident); - interference - od)" + "prefix_refinement peterson_sr peterson_sr peterson_sr dc + (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident)) + (\s0 s. peterson_rel ident s0 s \ invs s \ ab_label s ident = Exited) + (\s0 s. peterson_rel ident s0 s \ invs s \ ab_label s ident = Exited) + (do repeat (abs_peterson_proc ident); + interference + od) + (do repeat (peterson_proc ident); + interference + od)" apply (rule prefix_refinement_weaken_pre) apply (rule prefix_refinement_bind_sr) apply (rule prefix_refinement_repeat[rotated]) @@ -762,15 +706,15 @@ lemma peterson_repeat_refinement: apply (rule peterson_proc_refinement[THEN prefix_refinement_weaken_pre]) apply simp+ apply (rule prefix_refinement_interference_peterson) - apply (wpsimp wp: validI_triv)+ + apply wpsimp+ done theorem peterson_proc_system_refinement: - "prefix_refinement peterson_sr peterson_sr peterson_sr \\ - (\s0 s. s0 = s \ invs s \ ab_label s = (\_. Exited)) - (\t0 t. t0 = t \ invs t \ ab_label t = (\_. Exited)) - (\s0 s. s0 = s) (\t0 t. t0 = t) - abs_peterson_proc_system peterson_proc_system" + "prefix_refinement peterson_sr peterson_sr peterson_sr dc + (\s0 s. s0 = s) (\t0 t. t0 = t) + (\s0 s. s0 = s \ invs s \ ab_label s = (\_. Exited)) + (\t0 t. t0 = t \ invs t \ ab_label t = (\_. Exited)) + abs_peterson_proc_system peterson_proc_system" apply (unfold abs_peterson_proc_system_def peterson_proc_system_def) apply (rule prefix_refinement_parallel') apply (rule prefix_refinement_weaken_rely, rule prefix_refinement_weaken_pre) @@ -795,7 +739,7 @@ theorem peterson_proc_system_refinement: apply (rule validI_repeat_interference; simp) apply (rule peterson_proc_mutual_excl) apply (simp+)[3] - apply (rule rg_weaken_pre, rule rg_weaken_rely) + apply (rule rg_weaken_pre, rule rg_weaken_rely) apply (rule validI_repeat_interference; simp) apply (rule abs_peterson_proc_mutual_excl) apply (simp+)[3] @@ -811,17 +755,17 @@ lemma peterson_proc_system_prefix_closed[simp]: simp: cs_closed peterson_proc_system_def) theorem peterson_proc_system_mutual_excl: - "\ \s0 s. s0 = s \ invs s \ ab_label s = (\_. Exited) \, - \ \s0 s. s0 = s \ - peterson_proc_system - \ \s0 s. invs s0 \ invs s \, - \ \rv s0 s. invs s \" - apply (rule prefix_refinement_validI') + "\\s0 s. s0 = s \ invs s \ ab_label s = (\_. Exited)\, + \\s0 s. s0 = s\ + peterson_proc_system + \\s0 s. invs s0 \ invs s\, + \\rv s0 s. invs s\" + apply (rule prefix_refinement_validI) apply (rule peterson_proc_system_refinement) apply (rule abs_peterson_proc_system_mutual_excl) - apply clarsimp - apply (clarsimp simp: peterson_sr_invs_sym ) - apply (fastforce simp: peterson_rel_def peterson_sr_def) + apply (fastforce simp: peterson_rel_def peterson_sr_def) + apply clarsimp + apply (clarsimp simp: peterson_sr_invs_sym ) apply clarsimp apply (fastforce simp: peterson_sr_def) done diff --git a/lib/concurrency/examples/Plus2_Prefix.thy b/lib/concurrency/examples/Plus2_Prefix.thy index 87e37b76cc..aba52c3b8a 100644 --- a/lib/concurrency/examples/Plus2_Prefix.thy +++ b/lib/concurrency/examples/Plus2_Prefix.thy @@ -12,44 +12,52 @@ begin section \The plus2 example.\ text \ -This example presents an application of prefix refinement -to solve the plus2 verification problem. - -The function below can be proven to do two increments per -instance when grouped in parallel. But RG-reasoning doesn't -work well for this proof, since the state change (+1) performed -by the counterparts must be allowed by the rely, which must be -transitively closed, allowing any number of (+1) operations, -which is far too general. - -We address the issue with a ghost variable which records the number -of increments by each thread. We use prefix refinement to relate the -program with ghost variable to the initial program. -\ + This example presents an application of prefix refinement + to solve the plus2 verification problem. + + The function below can be proven to do two increments per + instance when grouped in parallel. But RG-reasoning doesn't + work well for this proof, since the state change (+1) performed + by the counterparts must be allowed by the rely, which must be + transitively closed, allowing any number of (+1) operations, + which is far too general. + + We address the issue with a ghost variable which records the number + of increments by each thread. We use prefix refinement to relate the + program with ghost variable to the initial program. + + Note that the programs defined here begin with an @{const env_steps} + and ends with @{const interference}. This is required so that they + can be combined with @{const parallel}; without these steps the + traces would not be able to be matched up and the composed program + would be trivially empty.\ definition - "plus2 \ do env_steps; modify ((+) (1 :: nat)); - interference; modify ((+) 1); interference od" + "plus2 \ do + env_steps; + modify ((+) (1 :: nat)); + interference; + modify ((+) 1); + interference + od" section \The ghost-extended program.\ -record - plus2_xstate = - mainv :: nat - threadv :: "nat \ nat" +record plus2_xstate = + mainv :: nat + threadv :: "nat \ nat" -definition - point_update :: "'a \ ('b \ 'b) \ (('a \ 'b) \ ('a \ 'b))" -where +definition point_update :: "'a \ ('b \ 'b) \ (('a \ 'b) \ ('a \ 'b))" where "point_update x fup f = f (x := fup (f x))" definition - "plus2_x tid \ do env_steps; - modify (mainv_update ((+) 1) o threadv_update (point_update tid ((+) 1))); - interference; - modify (mainv_update ((+) 1) o threadv_update (point_update tid ((+) 1))); - interference - od" + "plus2_x tid \ do + env_steps; + modify (mainv_update ((+) 1) o threadv_update (point_update tid ((+) 1))); + interference; + modify (mainv_update ((+) 1) o threadv_update (point_update tid ((+) 1))); + interference + od" section \Verifying the extended @{term plus2}.\ text \The RG-reasoning needed to verify the @{term plus2_x} program.\ @@ -57,8 +65,8 @@ definition "plus2_inv tids s = (mainv s = sum (threadv s) tids)" definition - "plus2_rel tids fix_tids s0 s - = ((plus2_inv tids s0 \ plus2_inv tids s) \ (\tid \ fix_tids. threadv s tid = threadv s0 tid))" + "plus2_rel tids fix_tids s0 s = + ((plus2_inv tids s0 \ plus2_inv tids s) \ (\tid \ fix_tids. threadv s tid = threadv s0 tid))" lemma plus2_rel_trans[simp]: "rtranclp (plus2_rel tids ftids) = plus2_rel tids ftids" @@ -68,16 +76,17 @@ lemma plus2_rel_trans[simp]: done lemma plus2_inv_Suc[simp]: - "tid \ tids \ finite tids - \ plus2_inv tids (mainv_update Suc (threadv_update (point_update tid Suc) s)) - = plus2_inv tids s" + "\tid \ tids; finite tids\ + \ plus2_inv tids (mainv_update Suc (threadv_update (point_update tid Suc) s)) + = plus2_inv tids s" apply (simp add: plus2_inv_def point_update_def) apply (simp add: sum.If_cases[where h=f and g=f and P="(=) tid" and A="tids" for f x, simplified]) done theorem plus2_x_property: "\\s0 s. plus2_inv tids s \ threadv s tid = 0 \ s = s0 \ tid \ tids \ finite tids\,\plus2_rel tids {tid}\ - plus2_x tid \plus2_rel tids (- {tid})\,\\_ _ s. plus2_inv tids s \ threadv s tid = 2\" + plus2_x tid + \plus2_rel tids (- {tid})\,\\_ _ s. plus2_inv tids s \ threadv s tid = 2\" apply (simp add: plus2_x_def) apply wpsimp apply (clarsimp simp: plus2_rel_def point_update_def) @@ -85,7 +94,8 @@ theorem plus2_x_property: corollary plus2_x_parallel: "\\s0 s. mainv s = 0 \ (\tid \ {1, 2}. threadv s tid = 0) \ s = s0\,\\a b. a = b\ - parallel (plus2_x 1) (plus2_x 2) \\s0 s. True\,\\_ s0 s. mainv s = 4\" + parallel (plus2_x 1) (plus2_x 2) + \\s0 s. True\,\\_ s0 s. mainv s = 4\" apply (rule rg_weaken_pre) apply (rule rg_strengthen_post) apply ((rule rg_validI plus2_x_property[where tids="{1, 2}"])+; simp add: plus2_rel_def le_fun_def) @@ -94,8 +104,7 @@ corollary plus2_x_parallel: done section \Mapping across prefix refinement.\ -text \Proving prefix refinement of @{term plus2} and @{term plus2_x} and -deriving the final result.\ +text \Proving prefix refinement of @{term plus2} and @{term plus2_x} and deriving the final result.\ lemma env_stable: "env_stable AR R (\s t. t = mainv s) (\s t. t = mainv s) \" @@ -103,14 +112,14 @@ lemma env_stable: apply (simp add: plus2_xstate.splits) done -abbreviation(input) - "p_refn rvr P Q AR R \ prefix_refinement (\s t. t = mainv s) (\s t. t = mainv s) - (\s t. t = mainv s) rvr P Q AR R" +abbreviation (input) + "p_refn rvr AR R P Q \ + prefix_refinement (\s t. t = mainv s) (\s t. t = mainv s) (\s t. t = mainv s) rvr AR R P Q" theorem pfx_refn_plus2_x: - "p_refn (\\) (=) (\\) AR R (plus2_x tid) plus2" + "p_refn dc AR R (=) (\\) (plus2_x tid) plus2" apply (simp add: plus2_x_def plus2_def) - apply (rule prefix_refinement_weaken_pre) + apply pfx_refn_pre apply (rule pfx_refn_bind prefix_refinement_interference prefix_refinement_env_steps pfx_refn_modifyT env_stable | wpsimp)+ @@ -128,32 +137,32 @@ lemma prefix_closed_plus2: theorem plus2_parallel: "\\s0 s. s = 0 \ s = s0\,\\a b. a = b\ - parallel plus2 plus2 \\s0 s. True\,\\_ s0 s. s = 4\" + parallel plus2 plus2 + \\s0 s. True\,\\_ s0 s. s = 4\" apply (rule_tac sr="\s t. t = mainv s" in prefix_refinement_validI) - apply (rule prefix_refinement_parallel_triv; - ((rule par_tr_fin_plus2_x prefix_closed_plus2)?)) - apply (rule pfx_refn_plus2_x[where tid=1]) - apply (rule pfx_refn_plus2_x[where tid=2]) - apply clarsimp - apply (rule rg_strengthen_post) - apply (rule plus2_x_parallel[simplified]) + apply (rule prefix_refinement_parallel_triv; + ((rule par_tr_fin_plus2_x prefix_closed_plus2 twp_post_taut)+)?) + apply (rule pfx_refn_plus2_x[where tid=1]) + apply (rule pfx_refn_plus2_x[where tid=2]) + apply (rule plus2_x_parallel) + apply clarsimp + apply (clarsimp simp: plus2_xstate.splits) + apply (strengthen exI[where x="f(1 := x, 2 := y)" for f x y]) + apply simp apply clarsimp - apply (clarsimp simp: plus2_xstate.splits) - apply (strengthen exI[where x="f(1 := x, 2 := y)" for f x y]) - apply simp + apply clarsimp apply clarsimp apply (intro prefix_closed_parallel prefix_closed_plus2) done section \Generalising\ -text \Just for fun, generalise to arbitrarily many -copies of the @{term plus2} program.\ +text \Just for fun, generalise to arbitrarily many copies of the @{term plus2} program.\ lemma plus2_x_n_parallel_induct: - "n > 0 \ n \ N \ - \\s0 s. plus2_inv {..< N} s \ (\i < N. threadv s i = 0) \ s = s0\,\plus2_rel {..< N} {..< n}\ - fold parallel (map plus2_x [1 ..< n]) (plus2_x 0) \plus2_rel {..< N} ( - {..< n})\,\\_ _ s. - plus2_inv {..< N} s \ (\i < n. threadv s i = 2)\" + "\n > 0; n \ N\ \ + \\s0 s. plus2_inv {..< N} s \ (\i < N. threadv s i = 0) \ s = s0\,\plus2_rel {..< N} {..< n}\ + fold parallel (map plus2_x [1 ..< n]) (plus2_x 0) + \plus2_rel {..< N} ( - {..< n})\,\\_ _ s. plus2_inv {..< N} s \ (\i < n. threadv s i = 2)\" apply (induct n) apply simp apply (case_tac n) @@ -163,18 +172,19 @@ lemma plus2_x_n_parallel_induct: apply clarsimp apply (clarsimp split del: if_split) apply (rule rg_weaken_pre, rule rg_strengthen_post, - rule rg_validI, rule plus2_x_property[where tids="{..< N}"], - assumption, (clarsimp simp: plus2_rel_def)+) + rule rg_validI, rule plus2_x_property[where tids="{..< N}"], assumption, + (clarsimp simp: plus2_rel_def)+) apply (auto dest: less_Suc_eq[THEN iffD1])[1] apply clarsimp done theorem plus2_x_n_parallel: "n > 0 \ - \\s0 s. mainv s = 0 \ (\i < n. threadv s i = 0) \ s = s0\,\plus2_rel {..< n} {..< n}\ - fold parallel (map plus2_x [1 ..< n]) (plus2_x 0) \\s0 s. True\,\\_ _ s. mainv s = (n * 2)\" + \\s0 s. mainv s = 0 \ (\i < n. threadv s i = 0) \ s = s0\,\plus2_rel {..< n} {..< n}\ + fold parallel (map plus2_x [1 ..< n]) (plus2_x 0) + \\s0 s. True\,\\_ _ s. mainv s = (n * 2)\" apply (rule rg_weaken_pre, rule rg_strengthen_post, - rule rg_strengthen_guar, erule plus2_x_n_parallel_induct) + rule rg_strengthen_guar, erule plus2_x_n_parallel_induct) apply simp apply simp apply (clarsimp simp: plus2_inv_def) @@ -182,8 +192,8 @@ theorem plus2_x_n_parallel: done lemma par_tr_fin_principle_parallel: - "par_tr_fin_principle f \ par_tr_fin_principle g - \ par_tr_fin_principle (parallel f g)" + "\par_tr_fin_principle f; par_tr_fin_principle g\ + \ par_tr_fin_principle (parallel f g)" apply (subst par_tr_fin_principle_def, clarsimp simp: parallel_def3) apply (drule(1) par_tr_fin_principleD)+ apply (clarsimp simp: neq_Nil_conv) @@ -191,12 +201,12 @@ lemma par_tr_fin_principle_parallel: lemma fold_parallel_par_tr_fin_principle[where xs="rev xs" for xs, simplified]: "\x \ insert x (set xs). par_tr_fin_principle x - \ par_tr_fin_principle (fold parallel (rev xs) x)" + \ par_tr_fin_principle (fold parallel (rev xs) x)" by (induct xs, simp_all add: par_tr_fin_principle_parallel) lemma fold_parallel_prefix_closed[where xs="rev xs" for xs, simplified]: "\x \ insert x (set xs). prefix_closed x - \ prefix_closed (fold parallel (rev xs) x)" + \ prefix_closed (fold parallel (rev xs) x)" by (induct xs, simp_all add: prefix_closed_parallel) lemma bipred_disj_top_eq: @@ -205,42 +215,44 @@ lemma bipred_disj_top_eq: by auto lemma fold_parallel_pfx_refn_induct: - "list_all2 (prefix_refinement sr sr sr (\_ _. True) P Q (\\) (\\)) xs ys - \ prefix_refinement sr sr sr (\_ _. True) P Q (\\) (\\) x y - \ \x \ set (x # xs). par_tr_fin_principle x - \ \y \ set (y # ys). prefix_closed y - \ prefix_refinement sr sr sr (\_ _. True) P Q (\\) (\\) - (fold parallel (rev xs) x) (fold parallel (rev ys) y)" + "\list_all2 (prefix_refinement sr sr sr dc (\\) (\\) P Q) xs ys; + prefix_refinement sr sr sr dc (\\) (\\) P Q x y; + \x \ set (x # xs). par_tr_fin_principle x; + \y \ set (y # ys). prefix_closed y\ + \ prefix_refinement sr sr sr dc(\\) (\\) P Q + (fold parallel (rev xs) x) (fold parallel (rev ys) y)" apply (induct rule: list_all2_induct; simp) apply (rule prefix_refinement_parallel_triv[simplified bipred_disj_top_eq]; simp?) apply (clarsimp simp: fold_parallel_par_tr_fin_principle - fold_parallel_prefix_closed)+ + fold_parallel_prefix_closed rg_TrueI)+ done -lemmas fold_parallel_pfx_refn - = fold_parallel_pfx_refn_induct[where xs="rev xs" and ys="rev ys" for xs ys, simplified] +lemmas fold_parallel_pfx_refn = + fold_parallel_pfx_refn_induct[where xs="rev xs" and ys="rev ys" for xs ys, simplified] theorem plus2_n_parallel: - "n > 0 - \ \\s0 s. s = 0 \ s = s0\,\\a b. a = b\ - fold parallel (replicate (n - 1) plus2) plus2 \\s0 s. True\,\\_ s0 s. s = n * 2\" + "n > 0 \ + \\s0 s. s = 0 \ s = s0\,\\a b. a = b\ + fold parallel (replicate (n - 1) plus2) plus2 + \\s0 s. True\,\\_ s0 s. s = n * 2\" apply (rule_tac sr="\s t. t = mainv s" in prefix_refinement_validI) - apply (rule prefix_refinement_weaken_rely, - rule_tac xs="map plus2_x [1 ..< n]" in fold_parallel_pfx_refn) - apply (clarsimp simp: list_all2_conv_all_nth) - apply (rule pfx_refn_plus2_x) - apply (rule pfx_refn_plus2_x[where tid=0]) - apply (simp add: par_tr_fin_plus2_x) - apply (simp add: prefix_closed_plus2) - apply (simp add: le_fun_def) - apply (simp add: le_fun_def) - apply simp - apply (rule rg_strengthen_post, rule plus2_x_n_parallel[simplified], simp) + apply (rule prefix_refinement_weaken_rely, + rule_tac xs="map plus2_x [1 ..< n]" in fold_parallel_pfx_refn) + apply (clarsimp simp: list_all2_conv_all_nth) + apply (rule pfx_refn_plus2_x) + apply (rule pfx_refn_plus2_x[where tid=0]) + apply (simp add: par_tr_fin_plus2_x) + apply (simp add: prefix_closed_plus2) + apply (simp add: le_fun_def) + apply (simp add: le_fun_def) + apply (rule plus2_x_n_parallel, simp) + apply clarsimp + apply (clarsimp simp: plus2_xstate.splits exI[where x="\_. 0"]) apply clarsimp - apply (clarsimp simp: plus2_xstate.splits exI[where x="\_. 0"]) + apply (rule exI, strengthen refl) + apply (clarsimp simp: plus2_rel_def plus2_inv_def) + apply clarsimp apply clarsimp - apply (rule exI, strengthen refl) - apply (clarsimp simp: plus2_rel_def plus2_inv_def) apply (rule fold_parallel_prefix_closed) apply (simp add: prefix_closed_plus2) done