theory Prefix_Refinement

lemma prefix_refinement_Await:
  "env_stable AR R sr iosr Q
    \<Longrightarrow> abs_rely_stable AR P
    \<Longrightarrow> \<forall>s t. P s \<longrightarrow> Q t \<longrightarrow> iosr s t \<longrightarrow> G' t \<longrightarrow> G s
    \<Longrightarrow> (\<exists>s. G' s) \<longrightarrow> (\<exists>s. G s)
    \<Longrightarrow> prefix_refinement sr iosr iosr (\<lambda>_ _. True) (\<lambda>s0 s. s0 = s \<and> P s)
                (\<lambda>t0 t. t0 = t \<and> 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="\<lambda>s s'. G s = G' s'"]
             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_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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>env_stable AR R sr iosr Q; abs_rely_stable AR P; \<forall>s t. P s \<longrightarrow> Q t \<longrightarrow> iosr s t \<longrightarrow> G' t \<longrightarrow> G s; (\<exists>s. G' s) \<longrightarrow> (\<exists>s. G s)\<rbrakk> \<Longrightarrow> prefix_refinement sr iosr iosr (\<lambda>_ _. True) (\<lambda>s0 s. s0 = s \<and> P s) (\<lambda>t0 t. t0 = t \<and> Q t) AR R (Await G) (Await G') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>env_stable AR R sr iosr Q; abs_rely_stable AR P; \<forall>s. P s \<longrightarrow> (\<forall>t. Q t \<longrightarrow> iosr s t \<longrightarrow> G' t \<longrightarrow> G s); (\<exists>s. G' s) \<longrightarrow> (\<exists>s. G s)\<rbrakk> \<Longrightarrow> prefix_refinement sr iosr iosr (\<lambda>_ _. True) (\<lambda>s0 s. s0 = s \<and> P s) (\<lambda>t0 t. t0 = t \<and> Q t) AR R (do s1 <- select {s. G s};
y <- env_steps;
s <- get;
select (if G s then {()} else {})
od) (do s1 <- select {s. G' s};
y <- env_steps;
s <- get;
select (if G' s then {()} else {})
od) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>env_stable AR R sr iosr Q; abs_rely_stable AR P; \<forall>s. P s \<longrightarrow> (\<forall>t. Q t \<longrightarrow> iosr s t \<longrightarrow> G' t \<longrightarrow> G s); (\<exists>s. G' s) \<longrightarrow> (\<exists>s. G s)\<rbrakk> \<Longrightarrow> prefix_refinement sr iosr iosr (\<lambda>_ _. True) ?P'3 ?Q'3 AR R (do s1 <- select {s. G s};
y <- env_steps;
s <- get;
select (if G s then {()} else {})
od) (do s1 <- select {s. G' s};
y <- env_steps;
s <- get;
select (if G' s then {()} else {})
od)
 2. \<lbrakk>env_stable AR R sr iosr Q; abs_rely_stable AR P; \<forall>s. P s \<longrightarrow> (\<forall>t. Q t \<longrightarrow> iosr s t \<longrightarrow> G' t \<longrightarrow> G s); (\<exists>s. G' s) \<longrightarrow> (\<exists>s. G s)\<rbrakk> \<Longrightarrow> \<forall>s s0. s0 = s \<and> P s \<longrightarrow> ?P'3 s0 s
 3. \<lbrakk>env_stable AR R sr iosr Q; abs_rely_stable AR P; \<forall>s. P s \<longrightarrow> (\<forall>t. Q t \<longrightarrow> iosr s t \<longrightarrow> G' t \<longrightarrow> G s); (\<exists>s. G' s) \<longrightarrow> (\<exists>s. G s)\<rbrakk> \<Longrightarrow> \<forall>s t s0 t0. iosr s t \<longrightarrow> sr s0 t0 \<longrightarrow> s0 = s \<and> P s \<longrightarrow> t0 = t \<and> Q t \<longrightarrow> ?Q'3 t0 t proof (prove)
goal (2 subgoals):
 1. \<lbrakk>env_stable AR R sr iosr Q; abs_rely_stable AR P; \<forall>s. P s \<longrightarrow> (\<forall>t. Q t \<longrightarrow> iosr s t \<longrightarrow> G' t \<longrightarrow> G s); (\<exists>s. G' s) \<longrightarrow> (\<exists>s. G s)\<rbrakk> \<Longrightarrow> \<forall>s. P s \<longrightarrow> Ex G \<longrightarrow> (\<forall>s'. AR\<^sup>*\<^sup>* s s' \<longrightarrow> P s')
 2. \<lbrakk>env_stable AR R sr iosr Q; abs_rely_stable AR P; \<forall>s. P s \<longrightarrow> (\<forall>t. Q t \<longrightarrow> iosr s t \<longrightarrow> G' t \<longrightarrow> G s); (\<exists>s. G' s) \<longrightarrow> (\<exists>s. G s)\<rbrakk> \<Longrightarrow> \<forall>s t s0 t0. iosr s t \<longrightarrow> sr s0 t0 \<longrightarrow> s0 = s \<and> P s \<longrightarrow> t0 = t \<and> Q t \<longrightarrow> ((\<lambda>_ _. True) and (\<lambda>s0 s. \<forall>x\<in>{s. G' s}. ((\<lambda>t0 t. t0 = t \<and> Q t0) and (\<lambda>a b. (\<forall>s'. R\<^sup>*\<^sup>* a s' \<longrightarrow> Q s') \<and> Q b)) s0 s)) t0 t proof (prove)
goal (2 subgoals):
 1. \<And>s x s'. \<lbrakk>env_stable AR R sr iosr Q; abs_rely_stable AR P; \<forall>s. P s \<longrightarrow> (\<forall>t. Q t \<longrightarrow> iosr s t \<longrightarrow> G' t \<longrightarrow> G s); (\<exists>s. G' s) \<longrightarrow> (\<exists>s. G s); P s; G x; AR\<^sup>*\<^sup>* s s'\<rbrakk> \<Longrightarrow> P s'
 2. \<lbrakk>env_stable AR R sr iosr Q; abs_rely_stable AR P; \<forall>s. P s \<longrightarrow> (\<forall>t. Q t \<longrightarrow> iosr s t \<longrightarrow> G' t \<longrightarrow> G s); (\<exists>s. G' s) \<longrightarrow> (\<exists>s. G s)\<rbrakk> \<Longrightarrow> \<forall>s t s0 t0. iosr s t \<longrightarrow> sr s0 t0 \<longrightarrow> s0 = s \<and> P s \<longrightarrow> t0 = t \<and> Q t \<longrightarrow> ((\<lambda>_ _. True) and (\<lambda>s0 s. \<forall>x\<in>{s. G' s}. ((\<lambda>t0 t. t0 = t \<and> Q t0) and (\<lambda>a b. (\<forall>s'. R\<^sup>*\<^sup>* a s' \<longrightarrow> Q s') \<and> Q b)) s0 s)) t0 t proof (prove)
goal (1 subgoal):
 1. \<lbrakk>env_stable AR R sr iosr Q; abs_rely_stable AR P; \<forall>s. P s \<longrightarrow> (\<forall>t. Q t \<longrightarrow> iosr s t \<longrightarrow> G' t \<longrightarrow> G s); (\<exists>s. G' s) \<longrightarrow> (\<exists>s. G s)\<rbrakk> \<Longrightarrow> \<forall>s t s0 t0. iosr s t \<longrightarrow> sr s0 t0 \<longrightarrow> s0 = s \<and> P s \<longrightarrow> t0 = t \<and> Q t \<longrightarrow> ((\<lambda>_ _. True) and (\<lambda>s0 s. \<forall>x\<in>{s. G' s}. ((\<lambda>t0 t. t0 = t \<and> Q t0) and (\<lambda>a b. (\<forall>s'. R\<^sup>*\<^sup>* a s' \<longrightarrow> Q s') \<and> Q b)) s0 s)) t0 t proof (prove)
goal (1 subgoal):
 1. \<And>s t x s'. \<lbrakk>abs_rely_stable AR P; \<forall>s. P s \<longrightarrow> (\<forall>t. Q t \<longrightarrow> iosr s t \<longrightarrow> G' t \<longrightarrow> G s); (\<exists>s. G' s) \<longrightarrow> (\<exists>s. G s); rely_stable R sr Q; env_rely_stable_iosr AR R sr iosr Q; iosr \<le> sr; iosr s t; sr s t; P s; Q t; G' x; R\<^sup>*\<^sup>* t s'\<rbrakk> \<Longrightarrow> Q s' proof (prove)
goal:
No subgoals!