diff --git a/lib/concurrency/Prefix_Refinement.thy b/lib/concurrency/Prefix_Refinement.thy index 1f35726b64..79a4a77129 100644 --- a/lib/concurrency/Prefix_Refinement.thy +++ b/lib/concurrency/Prefix_Refinement.thy @@ -17,7 +17,7 @@ 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 + 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 @@ -164,15 +164,16 @@ lemma is_matching_fragment_Nil: apply (clarsimp simp: in_fst_snd_image) done -\ \FIXME: it would be good to show this but the last assumption needs to be a lot more complicated - and the nondet equivalent isn't used anywhere. +\ \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'; - no_fail P' f; \t0 t. Q t0 t \ (\s0 s. P s0 s \ sr s0 t0 \ isr s t)\ - \ no_fail Q' f'" - apply (clarsimp simp: prefix_refinement_def no_fail_def) - apply (erule allE, erule (1) impE) + \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\ @@ -592,14 +593,18 @@ lemma prefix_refinement_req: \ prefix_refinement sr isr osr rvr AR R P Q f g" by (auto simp: prefix_refinement_def) -\ \FIXME: is it more usable to have this lemma combined like this or to split it up like Corres_UL's version\ 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" @@ -930,6 +935,9 @@ lemma is_matching_fragment_UNION: apply blast done +\ \ + 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 @@ -1309,8 +1317,6 @@ lemma prefix_refinement_catch: apply clarsimp done -\ \FIXME: an equivalent doesn't seem to exist for corres, do we want it to or does it mean we - shouldn't bother with this?\ 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'); @@ -1403,16 +1409,12 @@ lemma prefix_refinement_whenE: apply simp done -\ \FIXME: an equivalent doesn't seem to exist for corres, do we want it to or does it mean we - shouldn't bother with this?\ 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) -\ \FIXME: an equivalent doesn't seem to exist for corres, do we want it to or does it mean we - shouldn't bother with this?\ 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) @@ -1444,11 +1446,6 @@ lemma prefix_refinement_if_strong: (if G then a else b) (if G' then c else d)" by (fastforce simp: prefix_refinement_def) -\ \FIXME: corres equivalent isn't used, keep or delete?\ -lemmas prefix_refinement_if_strong' = - prefix_refinement_if_strong[where P=P and P'=P and P''=P for P, - where Q=Q and Q'=Q and Q''=Q for Q, simplified] - \ \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. @@ -1722,19 +1719,15 @@ apply (auto simp: is_matching_fragment_def prefix_closed_def self_closed_def env matching_tr_pfx_def matching_tr_def)[1] oops\ -\ \FIXME: not sure why this isn't using \\ (or dc)\ -abbreviation (input) - "dc2 \ (\_ _. True)" - abbreviation - "pfx_refnT sr rvr AR R \ pfx_refn sr rvr AR R dc2 dc2" + "pfx_refnT sr rvr AR R \ pfx_refn sr rvr AR R \\ \\" lemma prefix_refinement_returnTT: - "rvr rv rv' \ prefix_refinement sr iosr iosr rvr AR R dc2 dc2 (return rv) (return rv')" + "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 AR R dc2 dc2 get get" + "prefix_refinement sr iosr iosr iosr AR R \\ \\ get get" by (rule prefix_refinement_get_imp, simp) lemma prefix_refinement_put_imp: @@ -1746,7 +1739,7 @@ lemma prefix_refinement_put_imp: done lemma prefix_refinement_put: - "osr s t \ prefix_refinement sr isr osr dc AR R dc2 dc2 (put s) (put t)" + "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: @@ -1787,16 +1780,16 @@ lemma prefix_refinement_fail: done lemma prefix_refinement_returnOkTT: - "rvr rv rv' \ prefix_refinement sr iosr iosr (rvr' \ rvr) AR R dc2 dc2 (returnOk rv) (returnOk rv')" + "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 dc2 dc2 (throwError e) (throwError e')" + "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 AR R dc2 dc2 (select S) (select T)" + \ 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) @@ -1831,8 +1824,6 @@ lemma prefix_refinement_gets_the: apply wpsimp+ done -\ \FIXME: an equivalent doesn't seem to exist for corres, do we want it to or does it mean we - shouldn't bother with this?\ 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)" @@ -1841,8 +1832,6 @@ lemma prefix_refinement_gets_map: apply simp done -\ \FIXME: an equivalent doesn't seem to exist for corres, do we want it to or does it mean we - shouldn't bother with this?\ 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')" @@ -2033,8 +2022,6 @@ lemma notM_prefix_refinement: apply wpsimp+ done -\ \FIXME: an equivalent doesn't seem to exist for corres, do we want it to or does it mean we - shouldn't bother with this?\ 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\\ @@ -2238,9 +2225,9 @@ lemma prefix_refinement_Await: 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(1), - rule_tac P="Q s'" in prefix_refinement_gen_asm(2)) - | (rule prefix_refinement_select[where rvr=dc2]) + 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 (erule(2) abs_rely_stable_rtranclp)