squash enlarge prefix_refinement: PR suggestions

Signed-off-by: Corey Lewis <[email protected]>

lib/concurrency/Prefix_Refinement.thy

@@ -17,7 +17,7 @@ section \<open>Definition of prefix fragment refinement\<close>
 
 text \<open>
   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
 
-\<comment> \<open>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.
+\<comment> \<open>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:
   "\<lbrakk>prefix_refinement sr isr osr rvr AR R P Q f f';
-    no_fail P' f; \<forall>t0 t. Q t0 t \<longrightarrow> (\<exists>s0 s. P s0 s \<and> sr s0 t0 \<and> isr s t)\<rbrakk>
-   \<Longrightarrow> no_fail Q' f'"
-  apply (clarsimp simp: prefix_refinement_def no_fail_def)
-  apply (erule allE, erule (1) impE)
+    \<forall>s0. no_fail (P s0) f; \<forall>t0 t. Q t0 t \<longrightarrow> (\<exists>s0 s. P s0 s \<and> sr s0 t0 \<and> isr s t)\<rbrakk>
+   \<Longrightarrow> \<forall>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\<close>
 
@@ -592,14 +593,18 @@ lemma prefix_refinement_req:
    \<Longrightarrow> prefix_refinement sr isr osr rvr AR R P Q f g"
   by (auto simp: prefix_refinement_def)
 
-\<comment> \<open>FIXME: is it more usable to have this lemma combined like this or to split it up like Corres_UL's version\<close>
 lemma prefix_refinement_gen_asm:
   "\<lbrakk>P \<Longrightarrow> prefix_refinement sr isr osr rvr AR R P' Q' f g\<rbrakk>
    \<Longrightarrow> prefix_refinement sr isr osr rvr AR R (P' and (\<lambda>_ _. P)) Q' f g"
+  by (auto simp: prefix_refinement_def)
+
+lemma prefix_refinement_gen_asm2:
   "\<lbrakk>P \<Longrightarrow> prefix_refinement sr isr osr rvr AR R P' Q' f g\<rbrakk>
    \<Longrightarrow> prefix_refinement sr isr osr rvr AR R P' (Q' and (\<lambda>_ _. 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:
   "\<lbrakk>\<And>s s0 t t0. \<lbrakk>isr s t; sr s0 t0; P s0 s; Q t0 t\<rbrakk> \<Longrightarrow> prefix_refinement sr isr osr rvr AR R P Q f g\<rbrakk>
    \<Longrightarrow> prefix_refinement sr isr osr rvr AR R P Q f g"
@@ -930,6 +935,9 @@ lemma is_matching_fragment_UNION:
   apply blast
   done
 
+\<comment> \<open>
+  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}.\<close>
 definition mbind ::
   "('s, 'a) tmonad \<Rightarrow> ('s \<Rightarrow> 'a \<Rightarrow> ('s, 'b) tmonad) \<Rightarrow> 's \<Rightarrow> ('s, 'b) tmonad"
   where
@@ -1309,8 +1317,6 @@ lemma prefix_refinement_catch:
   apply clarsimp
   done
 
-\<comment> \<open>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?\<close>
 lemma prefix_refinement_handle_elseE:
   "\<lbrakk>prefix_refinement sr isr osr (fr' \<oplus> rvr') AR R P Q a c;
     \<And>ft ft'. fr' ft ft' \<Longrightarrow> prefix_refinement sr osr osr (fr \<oplus> rvr) AR R (E ft) (E' ft') (b ft) (d ft');
@@ -1403,16 +1409,12 @@ lemma prefix_refinement_whenE:
   apply simp
   done
 
-\<comment> \<open>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?\<close>
 lemma prefix_refinement_unless:
   "\<lbrakk>G = G'; prefix_refinement sr isr isr rvr AR R P Q a c; rvr () ()\<rbrakk>
    \<Longrightarrow> prefix_refinement sr isr isr rvr AR R (\<lambda>x y. \<not> G \<longrightarrow> P x y) (\<lambda>x y. \<not> G' \<longrightarrow> Q x y)
          (unless G a) (unless G' c)"
   by (simp add: unless_def prefix_refinement_when)
 
-\<comment> \<open>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?\<close>
 lemma prefix_refinement_unlessE:
   "\<lbrakk>G = G'; prefix_refinement sr isr isr (f \<oplus> rvr) AR R P Q a c; rvr () ()\<rbrakk>
    \<Longrightarrow> prefix_refinement sr isr isr (f \<oplus> rvr) AR R (\<lambda>x y. \<not> G \<longrightarrow> P x y) (\<lambda>x y. \<not> G' \<longrightarrow> 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)
 
-\<comment> \<open>FIXME: corres equivalent isn't used, keep or delete?\<close>
-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]
-
 
 \<comment> \<open>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\<close>
 
-\<comment> \<open>FIXME: not sure why this isn't using \<top>\<top> (or dc)\<close>
-abbreviation (input)
-  "dc2 \<equiv> (\<lambda>_ _. True)"
-
 abbreviation
-  "pfx_refnT sr rvr AR R \<equiv> pfx_refn sr rvr AR R dc2 dc2"
+  "pfx_refnT sr rvr AR R \<equiv> pfx_refn sr rvr AR R \<top>\<top> \<top>\<top>"
 
 lemma prefix_refinement_returnTT:
-  "rvr rv rv' \<Longrightarrow> prefix_refinement sr iosr iosr rvr AR R dc2 dc2 (return rv) (return rv')"
+  "rvr rv rv' \<Longrightarrow> prefix_refinement sr iosr iosr rvr AR R \<top>\<top> \<top>\<top> (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 \<top>\<top> \<top>\<top> 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 \<Longrightarrow> prefix_refinement sr isr osr dc AR R dc2 dc2 (put s) (put t)"
+  "osr s t \<Longrightarrow> prefix_refinement sr isr osr dc AR R \<top>\<top> \<top>\<top> (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' \<Longrightarrow> prefix_refinement sr iosr iosr (rvr' \<oplus> rvr) AR R dc2 dc2 (returnOk rv) (returnOk rv')"
+  "rvr rv rv' \<Longrightarrow> prefix_refinement sr iosr iosr (rvr' \<oplus> rvr) AR R \<top>\<top> \<top>\<top> (returnOk rv) (returnOk rv')"
   by (rule prefix_refinement_returnOk_imp, simp)
 
 lemma prefix_refinement_throwErrorTT:
-  "rvr e e' \<Longrightarrow> prefix_refinement sr iosr iosr (rvr \<oplus> rvr') AR R dc2 dc2 (throwError e) (throwError e')"
+  "rvr e e' \<Longrightarrow> prefix_refinement sr iosr iosr (rvr \<oplus> rvr') AR R \<top>\<top> \<top>\<top> (throwError e) (throwError e')"
   by (rule prefix_refinement_throwError_imp, simp)
 
 lemma prefix_refinement_select:
   "\<lbrakk>\<forall>x \<in> T. \<exists>y \<in> S. rvr y x\<rbrakk>
-   \<Longrightarrow> prefix_refinement sr iosr iosr rvr AR R dc2 dc2 (select S) (select T)"
+   \<Longrightarrow> prefix_refinement sr iosr iosr rvr AR R \<top>\<top> \<top>\<top> (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
 
-\<comment> \<open>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?\<close>
 lemma prefix_refinement_gets_map:
   "\<lbrakk>\<And>s t. \<lbrakk>iosr s t; P s; Q t\<rbrakk> \<Longrightarrow> rel_option rvr (f s p) (g t q)\<rbrakk>
    \<Longrightarrow> prefix_refinement sr iosr iosr rvr AR R (\<lambda>_. P) (\<lambda>_. Q) (gets_map f p) (gets_map g q)"
@@ -1841,8 +1832,6 @@ lemma prefix_refinement_gets_map:
   apply simp
   done
 
-\<comment> \<open>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?\<close>
 lemma prefix_refinement_throw_opt:
   "\<lbrakk>\<And>s t. \<lbrakk>iosr s t; P s; Q t\<rbrakk> \<Longrightarrow> rvr ex ex' \<and> rel_option rvr' x x'\<rbrakk>
    \<Longrightarrow> prefix_refinement sr iosr iosr (rvr \<oplus> rvr') AR R (\<lambda>_. P) (\<lambda>_. Q) (throw_opt ex x) (throw_opt ex' x')"
@@ -2033,8 +2022,6 @@ lemma notM_prefix_refinement:
       apply wpsimp+
   done
 
-\<comment> \<open>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?\<close>
 lemma whenM_prefix_refinement:
   "\<lbrakk>prefix_refinement sr isr isr (=) AR R A A' a a'; prefix_refinement sr isr isr dc AR R C C' b b';
     \<lbrace>B\<rbrace>,\<lbrace>AR\<rbrace> a -,\<lbrace>\<lambda>c s0 s. c \<longrightarrow> C s0 s\<rbrace>; \<lbrace>B'\<rbrace>,\<lbrace>R\<rbrace> a' -,\<lbrace>\<lambda>c s0 s. c \<longrightarrow> C' s0 s\<rbrace>\<rbrakk>
@@ -2238,9 +2225,9 @@ lemma prefix_refinement_Await:
                 prefix_refinement_env_steps
            | simp add: if_split[where P="\<lambda>S. x \<in> 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="\<top>\<top>"])
            | wp)+
    apply clarsimp
    apply (erule(2) abs_rely_stable_rtranclp)