theory ExtraCorres

lemma corres_whileLoop_abs_ret:
  assumes cond: "\<And>r r' s s'. \<lbrakk>rrel r r'; (s, s') \<in> srel; P r s; P' r' s'\<rbrakk> \<Longrightarrow> C r s = C' r' s'"
  assumes body_corres:
    "\<And>r r'. rrel r r' \<Longrightarrow>
             corres_underlying srel nf nf' rrel (P r and C r) (P' r' and C' r') (B r) (B' r')"
  assumes rrel: "rrel r r'"
  assumes body_inv:
    "\<And>r. \<lbrace>P r and C r\<rbrace> B r \<lbrace>P\<rbrace>"
    "\<And>r'. \<lbrace>P' r' and C' r'\<rbrace> B' r' \<lbrace>P'\<rbrace>"
  assumes abs_termination: "\<And>r s. \<lbrakk>P r s; C r s\<rbrakk> \<Longrightarrow> whileLoop_terminates C B r s"
  assumes nf: "\<And>r. nf \<Longrightarrow> no_fail (P r and C r) (B r)"
  shows "corres_underlying srel nf nf' rrel (P r) (P' r') (whileLoop C B r) (whileLoop C' B' r')" apply (rule corres_underlyingI) apply (frule in_whileLoop_corres[OF body_corres body_inv];
          (fastforce intro: body_corres body_inv rrel dest: nf cond)) apply (rule_tac I="\<lambda>rv' s'. \<exists>rv s. (s, s') \<in> srel \<and> rrel rv rv' \<and> P rv s \<and> P' rv' s'"
              and R="{((r', s'), r, s). C' r s \<and> (r', s') \<in> fst (B' r s)
                                        \<and> whileLoop_terminates C' B' r s}"
               in not_snd_whileLoop) apply (fastforce intro: rrel) apply (rename_tac s s' conc_r new_s) apply (clarsimp simp: validNF_def) apply (rule conjI) apply (intro hoare_vcg_conj_lift_pre_fix; (solves wpsimp)?) apply (rule_tac Q="\<lambda>s'. \<exists>rv s. (s, s') \<in> srel \<and> rrel rv conc_r
                                     \<and> P rv s \<and> (P' conc_r s' \<and> C' conc_r s') \<and> s' = new_s"
                   in hoare_weaken_pre[rotated]) apply clarsimp apply (rule hoare_ex_pre) apply (rename_tac abs_r) apply (rule hoare_weaken_pre) apply (rule_tac G="rrel abs_r conc_r" in hoare_grab_asm) apply (wpsimp wp: wp_from_corres_u[OF body_corres] body_inv) apply (fastforce dest: nf) apply (fastforce dest: cond) apply (fastforce simp: valid_def) apply wpsimp apply (rule whileLoop_terminates_cross[OF body_corres];
           (fastforce dest: nf cond intro: body_inv abs_termination)) apply (rule_tac P="\<lambda>s'. \<exists>rv s. (s, s') \<in> srel \<and> rrel rv conc_r
                                  \<and> P rv s \<and> (P' conc_r s' \<and> C' conc_r s') \<and> s' = new_s"
                in no_fail_pre[rotated]) apply fastforce apply (rule no_fail_ex_lift) apply (rename_tac abs_r) apply (rule no_fail_pre) apply (rule_tac G="rrel abs_r conc_r" in no_fail_grab_asm) apply (fastforce intro: corres_u_nofail dest: body_corres nf) apply (fastforce simp: cond) apply (fastforce intro: wf_subset[OF whileLoop_terminates_wf[where C=C']]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying srel nf nf' rrel (P r) (P' r') (whileLoop C
  B r) (whileLoop C'
  B' r') proof (prove)
goal (2 subgoals):
 1. \<And>s t rv' t'. \<lbrakk>(s, t) \<in> srel; P r s; P' r' t; (rv', t') \<in> fst (whileLoop C'
  B' r' t)\<rbrakk> \<Longrightarrow> \<exists>(rv, s')\<in>fst (whileLoop C
  B r s). (s', t') \<in> srel \<and> rrel rv rv'
 2. \<And>s t. \<lbrakk>(s, t) \<in> srel; P r s; P' r' t; nf'\<rbrakk> \<Longrightarrow> \<not> snd (whileLoop C'
  B' r' t) proof (prove)
goal (1 subgoal):
 1. \<And>s t. \<lbrakk>(s, t) \<in> srel; P r s; P' r' t; nf'\<rbrakk> \<Longrightarrow> \<not> snd (whileLoop C'
  B' r' t) proof (prove)
goal (3 subgoals):
 1. \<And>s t. \<lbrakk>(s, t) \<in> srel; P r s; P' r' t; nf'\<rbrakk> \<Longrightarrow> \<exists>rv s. (s, t) \<in> srel \<and> rrel rv r' \<and> P rv s \<and> P' r' t
 2. \<And>s t ra sa. \<lbrakk>(s, t) \<in> srel; P r s; P' r' t; nf'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s'. (\<exists>rv s. (s, s') \<in> srel \<and> rrel rv ra \<and> P rv s \<and> P' ra s') \<and> C' ra s' \<and> s' = sa\<rbrace> B' ra \<lbrace>\<lambda>r' s'. (\<exists>rv s. (s, s') \<in> srel \<and> rrel rv r' \<and> P rv s \<and> P' r' s') \<and> ((r', s'), ra, sa) \<in> {((r', s'), r, s). C' r s \<and> (r', s') \<in> fst (B' r s) \<and> whileLoop_terminates C' B' r s}\<rbrace>!
 3. \<And>s t. \<lbrakk>(s, t) \<in> srel; P r s; P' r' t; nf'\<rbrakk> \<Longrightarrow> wf {((r', s'), r, s). C' r s \<and> (r', s') \<in> fst (B' r s) \<and> whileLoop_terminates C' B' r s} proof (prove)
goal (2 subgoals):
 1. \<And>s t ra sa. \<lbrakk>(s, t) \<in> srel; P r s; P' r' t; nf'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s'. (\<exists>rv s. (s, s') \<in> srel \<and> rrel rv ra \<and> P rv s \<and> P' ra s') \<and> C' ra s' \<and> s' = sa\<rbrace> B' ra \<lbrace>\<lambda>r' s'. (\<exists>rv s. (s, s') \<in> srel \<and> rrel rv r' \<and> P rv s \<and> P' r' s') \<and> ((r', s'), ra, sa) \<in> {((r', s'), r, s). C' r s \<and> (r', s') \<in> fst (B' r s) \<and> whileLoop_terminates C' B' r s}\<rbrace>!
 2. \<And>s t. \<lbrakk>(s, t) \<in> srel; P r s; P' r' t; nf'\<rbrakk> \<Longrightarrow> wf {((r', s'), r, s). C' r s \<and> (r', s') \<in> fst (B' r s) \<and> whileLoop_terminates C' B' r s} proof (prove)
goal (2 subgoals):
 1. \<And>s s' conc_r new_s. \<lbrakk>(s, s') \<in> srel; P r s; P' r' s'; nf'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s'. (\<exists>rv s. (s, s') \<in> srel \<and> rrel rv conc_r \<and> P rv s \<and> P' conc_r s') \<and> C' conc_r s' \<and> s' = new_s\<rbrace> B' conc_r \<lbrace>\<lambda>r' s'. (\<exists>rv s. (s, s') \<in> srel \<and> rrel rv r' \<and> P rv s \<and> P' r' s') \<and> ((r', s'), conc_r, new_s) \<in> {((r', s'), r, s). C' r s \<and> (r', s') \<in> fst (B' r s) \<and> whileLoop_terminates C' B' r s}\<rbrace>!
 2. \<And>s t. \<lbrakk>(s, t) \<in> srel; P r s; P' r' t; nf'\<rbrakk> \<Longrightarrow> wf {((r', s'), r, s). C' r s \<and> (r', s') \<in> fst (B' r s) \<and> whileLoop_terminates C' B' r s} proof (prove)
goal (2 subgoals):
 1. \<And>s s' conc_r new_s. \<lbrakk>(s, s') \<in> srel; P r s; P' r' s'; nf'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s'. (\<exists>rv s. (s, s') \<in> srel \<and> rrel rv conc_r \<and> P rv s \<and> P' conc_r s') \<and> C' conc_r s' \<and> s' = new_s\<rbrace> B' conc_r \<lbrace>\<lambda>r' s'. (\<exists>rv s. (s, s') \<in> srel \<and> rrel rv r' \<and> P rv s \<and> P' r' s') \<and> C' conc_r new_s \<and> (r', s') \<in> fst (B' conc_r new_s) \<and> whileLoop_terminates C' B' conc_r new_s\<rbrace> \<and> no_fail (\<lambda>s'. (\<exists>rv s. (s, s') \<in> srel \<and> rrel rv conc_r \<and> P rv s \<and> P' conc_r s') \<and> C' conc_r s' \<and> s' = new_s) (B' conc_r)
 2. \<And>s t. \<lbrakk>(s, t) \<in> srel; P r s; P' r' t; nf'\<rbrakk> \<Longrightarrow> wf {((r', s'), r, s). C' r s \<and> (r', s') \<in> fst (B' r s) \<and> whileLoop_terminates C' B' r s} proof (prove)
goal (3 subgoals):
 1. \<And>s s' conc_r new_s. \<lbrakk>(s, s') \<in> srel; P r s; P' r' s'; nf'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s'. (\<exists>rv s. (s, s') \<in> srel \<and> rrel rv conc_r \<and> P rv s \<and> P' conc_r s') \<and> C' conc_r s' \<and> s' = new_s\<rbrace> B' conc_r \<lbrace>\<lambda>r' s'. (\<exists>rv s. (s, s') \<in> srel \<and> rrel rv r' \<and> P rv s \<and> P' r' s') \<and> C' conc_r new_s \<and> (r', s') \<in> fst (B' conc_r new_s) \<and> whileLoop_terminates C' B' conc_r new_s\<rbrace>
 2. \<And>s s' conc_r new_s. \<lbrakk>(s, s') \<in> srel; P r s; P' r' s'; nf'\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s'. (\<exists>rv s. (s, s') \<in> srel \<and> rrel rv conc_r \<and> P rv s \<and> P' conc_r s') \<and> C' conc_r s' \<and> s' = new_s) (B' conc_r)
 3. \<And>s t. \<lbrakk>(s, t) \<in> srel; P r s; P' r' t; nf'\<rbrakk> \<Longrightarrow> wf {((r', s'), r, s). C' r s \<and> (r', s') \<in> fst (B' r s) \<and> whileLoop_terminates C' B' r s} proof (prove)
goal (5 subgoals):
 1. \<And>s s' conc_r new_s. \<lbrakk>(s, s') \<in> srel; P r s; P' r' s'; nf'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (\<exists>rv sa. (sa, s) \<in> srel \<and> rrel rv conc_r \<and> P rv sa \<and> P' conc_r s) \<and> C' conc_r s \<and> s = new_s\<rbrace> B' conc_r \<lbrace>\<lambda>rv s. \<exists>rva sa. (sa, s) \<in> srel \<and> rrel rva rv \<and> P rva sa \<and> P' rv s\<rbrace>
 2. \<And>s s' conc_r new_s. \<lbrakk>(s, s') \<in> srel; P r s; P' r' s'; nf'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (\<exists>rv sa. (sa, s) \<in> srel \<and> rrel rv conc_r \<and> P rv sa \<and> P' conc_r s) \<and> C' conc_r s \<and> s = new_s\<rbrace> B' conc_r \<lbrace>\<lambda>rv s. (rv, s) \<in> fst (B' conc_r new_s)\<rbrace>
 3. \<And>s s' conc_r new_s. \<lbrakk>(s, s') \<in> srel; P r s; P' r' s'; nf'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (\<exists>rv sa. (sa, s) \<in> srel \<and> rrel rv conc_r \<and> P rv sa \<and> P' conc_r s) \<and> C' conc_r s \<and> s = new_s\<rbrace> B' conc_r \<lbrace>\<lambda>rv s. whileLoop_terminates C' B' conc_r new_s\<rbrace>
 4. \<And>s s' conc_r new_s. \<lbrakk>(s, s') \<in> srel; P r s; P' r' s'; nf'\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s'. (\<exists>rv s. (s, s') \<in> srel \<and> rrel rv conc_r \<and> P rv s \<and> P' conc_r s') \<and> C' conc_r s' \<and> s' = new_s) (B' conc_r)
 5. \<And>s t. \<lbrakk>(s, t) \<in> srel; P r s; P' r' t; nf'\<rbrakk> \<Longrightarrow> wf {((r', s'), r, s). C' r s \<and> (r', s') \<in> fst (B' r s) \<and> whileLoop_terminates C' B' r s} proof (prove)
goal (6 subgoals):
 1. \<And>s s' conc_r new_s sa. \<lbrakk>(s, s') \<in> srel; P r s; P' r' s'; nf'; (\<exists>rv s. (s, sa) \<in> srel \<and> rrel rv conc_r \<and> P rv s \<and> P' conc_r sa) \<and> C' conc_r sa \<and> sa = new_s\<rbrakk> \<Longrightarrow> \<exists>rv s. (s, sa) \<in> srel \<and> rrel rv conc_r \<and> P rv s \<and> (P' conc_r sa \<and> C' conc_r sa) \<and> sa = new_s
 2. \<And>s s' conc_r new_s. \<lbrakk>(s, s') \<in> srel; P r s; P' r' s'; nf'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s'. \<exists>rv s. (s, s') \<in> srel \<and> rrel rv conc_r \<and> P rv s \<and> (P' conc_r s' \<and> C' conc_r s') \<and> s' = new_s\<rbrace> B' conc_r \<lbrace>\<lambda>rv s. \<exists>rva sa. (sa, s) \<in> srel \<and> rrel rva rv \<and> P rva sa \<and> P' rv s\<rbrace>
 3. \<And>s s' conc_r new_s. \<lbrakk>(s, s') \<in> srel; P r s; P' r' s'; nf'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (\<exists>rv sa. (sa, s) \<in> srel \<and> rrel rv conc_r \<and> P rv sa \<and> P' conc_r s) \<and> C' conc_r s \<and> s = new_s\<rbrace> B' conc_r \<lbrace>\<lambda>rv s. (rv, s) \<in> fst (B' conc_r new_s)\<rbrace>
 4. \<And>s s' conc_r new_s. \<lbrakk>(s, s') \<in> srel; P r s; P' r' s'; nf'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (\<exists>rv sa. (sa, s) \<in> srel \<and> rrel rv conc_r \<and> P rv sa \<and> P' conc_r s) \<and> C' conc_r s \<and> s = new_s\<rbrace> B' conc_r \<lbrace>\<lambda>rv s. whileLoop_terminates C' B' conc_r new_s\<rbrace>
 5. \<And>s s' conc_r new_s. \<lbrakk>(s, s') \<in> srel; P r s; P' r' s'; nf'\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s'. (\<exists>rv s. (s, s') \<in> srel \<and> rrel rv conc_r \<and> P rv s \<and> P' conc_r s') \<and> C' conc_r s' \<and> s' = new_s) (B' conc_r)
 6. \<And>s t. \<lbrakk>(s, t) \<in> srel; P r s; P' r' t; nf'\<rbrakk> \<Longrightarrow> wf {((r', s'), r, s). C' r s \<and> (r', s') \<in> fst (B' r s) \<and> whileLoop_terminates C' B' r s} proof (prove)
goal (5 subgoals):
 1. \<And>s s' conc_r new_s. \<lbrakk>(s, s') \<in> srel; P r s; P' r' s'; nf'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s'. \<exists>rv s. (s, s') \<in> srel \<and> rrel rv conc_r \<and> P rv s \<and> (P' conc_r s' \<and> C' conc_r s') \<and> s' = new_s\<rbrace> B' conc_r \<lbrace>\<lambda>rv s. \<exists>rva sa. (sa, s) \<in> srel \<and> rrel rva rv \<and> P rva sa \<and> P' rv s\<rbrace>
 2. \<And>s s' conc_r new_s. \<lbrakk>(s, s') \<in> srel; P r s; P' r' s'; nf'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (\<exists>rv sa. (sa, s) \<in> srel \<and> rrel rv conc_r \<and> P rv sa \<and> P' conc_r s) \<and> C' conc_r s \<and> s = new_s\<rbrace> B' conc_r \<lbrace>\<lambda>rv s. (rv, s) \<in> fst (B' conc_r new_s)\<rbrace>
 3. \<And>s s' conc_r new_s. \<lbrakk>(s, s') \<in> srel; P r s; P' r' s'; nf'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (\<exists>rv sa. (sa, s) \<in> srel \<and> rrel rv conc_r \<and> P rv sa \<and> P' conc_r s) \<and> C' conc_r s \<and> s = new_s\<rbrace> B' conc_r \<lbrace>\<lambda>rv s. whileLoop_terminates C' B' conc_r new_s\<rbrace>
 4. \<And>s s' conc_r new_s. \<lbrakk>(s, s') \<in> srel; P r s; P' r' s'; nf'\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s'. (\<exists>rv s. (s, s') \<in> srel \<and> rrel rv conc_r \<and> P rv s \<and> P' conc_r s') \<and> C' conc_r s' \<and> s' = new_s) (B' conc_r)
 5. \<And>s t. \<lbrakk>(s, t) \<in> srel; P r s; P' r' t; nf'\<rbrakk> \<Longrightarrow> wf {((r', s'), r, s). C' r s \<and> (r', s') \<in> fst (B' r s) \<and> whileLoop_terminates C' B' r s} proof (prove)
goal (5 subgoals):
 1. \<And>s s' conc_r new_s rv. \<lbrakk>(s, s') \<in> srel; P r s; P' r' s'; nf'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<exists>sa. (sa, s) \<in> srel \<and> rrel rv conc_r \<and> P rv sa \<and> (P' conc_r s \<and> C' conc_r s) \<and> s = new_s\<rbrace> B' conc_r \<lbrace>\<lambda>rv s. \<exists>rva sa. (sa, s) \<in> srel \<and> rrel rva rv \<and> P rva sa \<and> P' rv s\<rbrace>
 2. \<And>s s' conc_r new_s. \<lbrakk>(s, s') \<in> srel; P r s; P' r' s'; nf'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (\<exists>rv sa. (sa, s) \<in> srel \<and> rrel rv conc_r \<and> P rv sa \<and> P' conc_r s) \<and> C' conc_r s \<and> s = new_s\<rbrace> B' conc_r \<lbrace>\<lambda>rv s. (rv, s) \<in> fst (B' conc_r new_s)\<rbrace>
 3. \<And>s s' conc_r new_s. \<lbrakk>(s, s') \<in> srel; P r s; P' r' s'; nf'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (\<exists>rv sa. (sa, s) \<in> srel \<and> rrel rv conc_r \<and> P rv sa \<and> P' conc_r s) \<and> C' conc_r s \<and> s = new_s\<rbrace> B' conc_r \<lbrace>\<lambda>rv s. whileLoop_terminates C' B' conc_r new_s\<rbrace>
 4. \<And>s s' conc_r new_s. \<lbrakk>(s, s') \<in> srel; P r s; P' r' s'; nf'\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s'. (\<exists>rv s. (s, s') \<in> srel \<and> rrel rv conc_r \<and> P rv s \<and> P' conc_r s') \<and> C' conc_r s' \<and> s' = new_s) (B' conc_r)
 5. \<And>s t. \<lbrakk>(s, t) \<in> srel; P r s; P' r' t; nf'\<rbrakk> \<Longrightarrow> wf {((r', s'), r, s). C' r s \<and> (r', s') \<in> fst (B' r s) \<and> whileLoop_terminates C' B' r s} proof (prove)
goal (5 subgoals):
 1. \<And>s s' conc_r new_s abs_r. \<lbrakk>(s, s') \<in> srel; P r s; P' r' s'; nf'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<exists>sa. (sa, s) \<in> srel \<and> rrel abs_r conc_r \<and> P abs_r sa \<and> (P' conc_r s \<and> C' conc_r s) \<and> s = new_s\<rbrace> B' conc_r \<lbrace>\<lambda>rv s. \<exists>rva sa. (sa, s) \<in> srel \<and> rrel rva rv \<and> P rva sa \<and> P' rv s\<rbrace>
 2. \<And>s s' conc_r new_s. \<lbrakk>(s, s') \<in> srel; P r s; P' r' s'; nf'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (\<exists>rv sa. (sa, s) \<in> srel \<and> rrel rv conc_r \<and> P rv sa \<and> P' conc_r s) \<and> C' conc_r s \<and> s = new_s\<rbrace> B' conc_r \<lbrace>\<lambda>rv s. (rv, s) \<in> fst (B' conc_r new_s)\<rbrace>
 3. \<And>s s' conc_r new_s. \<lbrakk>(s, s') \<in> srel; P r s; P' r' s'; nf'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (\<exists>rv sa. (sa, s) \<in> srel \<and> rrel rv conc_r \<and> P rv sa \<and> P' conc_r s) \<and> C' conc_r s \<and> s = new_s\<rbrace> B' conc_r \<lbrace>\<lambda>rv s. whileLoop_terminates C' B' conc_r new_s\<rbrace>
 4. \<And>s s' conc_r new_s. \<lbrakk>(s, s') \<in> srel; P r s; P' r' s'; nf'\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s'. (\<exists>rv s. (s, s') \<in> srel \<and> rrel rv conc_r \<and> P rv s \<and> P' conc_r s') \<and> C' conc_r s' \<and> s' = new_s) (B' conc_r)
 5. \<And>s t. \<lbrakk>(s, t) \<in> srel; P r s; P' r' t; nf'\<rbrakk> \<Longrightarrow> wf {((r', s'), r, s). C' r s \<and> (r', s') \<in> fst (B' r s) \<and> whileLoop_terminates C' B' r s} proof (prove)
goal (6 subgoals):
 1. \<And>s s' conc_r new_s abs_r. \<lbrakk>(s, s') \<in> srel; P r s; P' r' s'; nf'\<rbrakk> \<Longrightarrow> \<lbrace>?Q142 s s' conc_r new_s abs_r\<rbrace> B' conc_r \<lbrace>\<lambda>rv s. \<exists>rva sa. (sa, s) \<in> srel \<and> rrel rva rv \<and> P rva sa \<and> P' rv s\<rbrace>
 2. \<And>s s' conc_r new_s abs_r sa. \<lbrakk>(s, s') \<in> srel; P r s; P' r' s'; nf'; \<exists>s. (s, sa) \<in> srel \<and> rrel abs_r conc_r \<and> P abs_r s \<and> (P' conc_r sa \<and> C' conc_r sa) \<and> sa = new_s\<rbrakk> \<Longrightarrow> ?Q142 s s' conc_r new_s abs_r sa
 3. \<And>s s' conc_r new_s. \<lbrakk>(s, s') \<in> srel; P r s; P' r' s'; nf'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (\<exists>rv sa. (sa, s) \<in> srel \<and> rrel rv conc_r \<and> P rv sa \<and> P' conc_r s) \<and> C' conc_r s \<and> s = new_s\<rbrace> B' conc_r \<lbrace>\<lambda>rv s. (rv, s) \<in> fst (B' conc_r new_s)\<rbrace>
 4. \<And>s s' conc_r new_s. \<lbrakk>(s, s') \<in> srel; P r s; P' r' s'; nf'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (\<exists>rv sa. (sa, s) \<in> srel \<and> rrel rv conc_r \<and> P rv sa \<and> P' conc_r s) \<and> C' conc_r s \<and> s = new_s\<rbrace> B' conc_r \<lbrace>\<lambda>rv s. whileLoop_terminates C' B' conc_r new_s\<rbrace>
 5. \<And>s s' conc_r new_s. \<lbrakk>(s, s') \<in> srel; P r s; P' r' s'; nf'\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s'. (\<exists>rv s. (s, s') \<in> srel \<and> rrel rv conc_r \<and> P rv s \<and> P' conc_r s') \<and> C' conc_r s' \<and> s' = new_s) (B' conc_r)
 6. \<And>s t. \<lbrakk>(s, t) \<in> srel; P r s; P' r' t; nf'\<rbrakk> \<Longrightarrow> wf {((r', s'), r, s). C' r s \<and> (r', s') \<in> fst (B' r s) \<and> whileLoop_terminates C' B' r s} proof (prove)
goal (6 subgoals):
 1. \<And>s s' conc_r new_s abs_r. \<lbrakk>(s, s') \<in> srel; P r s; P' r' s'; nf'; rrel abs_r conc_r\<rbrakk> \<Longrightarrow> \<lbrace>?P145 s s' conc_r new_s abs_r\<rbrace> B' conc_r \<lbrace>\<lambda>rv s. \<exists>rva sa. (sa, s) \<in> srel \<and> rrel rva rv \<and> P rva sa \<and> P' rv s\<rbrace>
 2. \<And>s s' conc_r new_s abs_r sa. \<lbrakk>(s, s') \<in> srel; P r s; P' r' s'; nf'; \<exists>s. (s, sa) \<in> srel \<and> rrel abs_r conc_r \<and> P abs_r s \<and> (P' conc_r sa \<and> C' conc_r sa) \<and> sa = new_s\<rbrakk> \<Longrightarrow> rrel abs_r conc_r \<and> ?P145 s s' conc_r new_s abs_r sa
 3. \<And>s s' conc_r new_s. \<lbrakk>(s, s') \<in> srel; P r s; P' r' s'; nf'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (\<exists>rv sa. (sa, s) \<in> srel \<and> rrel rv conc_r \<and> P rv sa \<and> P' conc_r s) \<and> C' conc_r s \<and> s = new_s\<rbrace> B' conc_r \<lbrace>\<lambda>rv s. (rv, s) \<in> fst (B' conc_r new_s)\<rbrace>
 4. \<And>s s' conc_r new_s. \<lbrakk>(s, s') \<in> srel; P r s; P' r' s'; nf'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (\<exists>rv sa. (sa, s) \<in> srel \<and> rrel rv conc_r \<and> P rv sa \<and> P' conc_r s) \<and> C' conc_r s \<and> s = new_s\<rbrace> B' conc_r \<lbrace>\<lambda>rv s. whileLoop_terminates C' B' conc_r new_s\<rbrace>
 5. \<And>s s' conc_r new_s. \<lbrakk>(s, s') \<in> srel; P r s; P' r' s'; nf'\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s'. (\<exists>rv s. (s, s') \<in> srel \<and> rrel rv conc_r \<and> P rv s \<and> P' conc_r s') \<and> C' conc_r s' \<and> s' = new_s) (B' conc_r)
 6. \<And>s t. \<lbrakk>(s, t) \<in> srel; P r s; P' r' t; nf'\<rbrakk> \<Longrightarrow> wf {((r', s'), r, s). C' r s \<and> (r', s') \<in> fst (B' r s) \<and> whileLoop_terminates C' B' r s} proof (prove)
goal (6 subgoals):
 1. \<And>s s' conc_r abs_r. \<lbrakk>(s, s') \<in> srel; P r s; P' r' s'; nf'; rrel abs_r conc_r; nf\<rbrakk> \<Longrightarrow> no_fail (P abs_r and C abs_r) (B abs_r)
 2. \<And>s s' conc_r new_s abs_r sa. \<lbrakk>(s, s') \<in> srel; P r s; P' r' s'; nf'; \<exists>s. (s, sa) \<in> srel \<and> rrel abs_r conc_r \<and> P abs_r s \<and> (P' conc_r sa \<and> C' conc_r sa) \<and> sa = new_s\<rbrakk> \<Longrightarrow> rrel abs_r conc_r \<and> (\<exists>s. (s, sa) \<in> srel \<and> (P abs_r and C abs_r) s \<and> (P abs_r and C abs_r) s \<and> (P' conc_r and C' conc_r) sa \<and> (P' conc_r and C' conc_r) sa)
 3. \<And>s s' conc_r new_s. \<lbrakk>(s, s') \<in> srel; P r s; P' r' s'; nf'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (\<exists>rv sa. (sa, s) \<in> srel \<and> rrel rv conc_r \<and> P rv sa \<and> P' conc_r s) \<and> C' conc_r s \<and> s = new_s\<rbrace> B' conc_r \<lbrace>\<lambda>rv s. (rv, s) \<in> fst (B' conc_r new_s)\<rbrace>
 4. \<And>s s' conc_r new_s. \<lbrakk>(s, s') \<in> srel; P r s; P' r' s'; nf'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (\<exists>rv sa. (sa, s) \<in> srel \<and> rrel rv conc_r \<and> P rv sa \<and> P' conc_r s) \<and> C' conc_r s \<and> s = new_s\<rbrace> B' conc_r \<lbrace>\<lambda>rv s. whileLoop_terminates C' B' conc_r new_s\<rbrace>
 5. \<And>s s' conc_r new_s. \<lbrakk>(s, s') \<in> srel; P r s; P' r' s'; nf'\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s'. (\<exists>rv s. (s, s') \<in> srel \<and> rrel rv conc_r \<and> P rv s \<and> P' conc_r s') \<and> C' conc_r s' \<and> s' = new_s) (B' conc_r)
 6. \<And>s t. \<lbrakk>(s, t) \<in> srel; P r s; P' r' t; nf'\<rbrakk> \<Longrightarrow> wf {((r', s'), r, s). C' r s \<and> (r', s') \<in> fst (B' r s) \<and> whileLoop_terminates C' B' r s} proof (prove)
goal (5 subgoals):
 1. \<And>s s' conc_r new_s abs_r sa. \<lbrakk>(s, s') \<in> srel; P r s; P' r' s'; nf'; \<exists>s. (s, sa) \<in> srel \<and> rrel abs_r conc_r \<and> P abs_r s \<and> (P' conc_r sa \<and> C' conc_r sa) \<and> sa = new_s\<rbrakk> \<Longrightarrow> rrel abs_r conc_r \<and> (\<exists>s. (s, sa) \<in> srel \<and> (P abs_r and C abs_r) s \<and> (P abs_r and C abs_r) s \<and> (P' conc_r and C' conc_r) sa \<and> (P' conc_r and C' conc_r) sa)
 2. \<And>s s' conc_r new_s. \<lbrakk>(s, s') \<in> srel; P r s; P' r' s'; nf'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (\<exists>rv sa. (sa, s) \<in> srel \<and> rrel rv conc_r \<and> P rv sa \<and> P' conc_r s) \<and> C' conc_r s \<and> s = new_s\<rbrace> B' conc_r \<lbrace>\<lambda>rv s. (rv, s) \<in> fst (B' conc_r new_s)\<rbrace>
 3. \<And>s s' conc_r new_s. \<lbrakk>(s, s') \<in> srel; P r s; P' r' s'; nf'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (\<exists>rv sa. (sa, s) \<in> srel \<and> rrel rv conc_r \<and> P rv sa \<and> P' conc_r s) \<and> C' conc_r s \<and> s = new_s\<rbrace> B' conc_r \<lbrace>\<lambda>rv s. whileLoop_terminates C' B' conc_r new_s\<rbrace>
 4. \<And>s s' conc_r new_s. \<lbrakk>(s, s') \<in> srel; P r s; P' r' s'; nf'\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s'. (\<exists>rv s. (s, s') \<in> srel \<and> rrel rv conc_r \<and> P rv s \<and> P' conc_r s') \<and> C' conc_r s' \<and> s' = new_s) (B' conc_r)
 5. \<And>s t. \<lbrakk>(s, t) \<in> srel; P r s; P' r' t; nf'\<rbrakk> \<Longrightarrow> wf {((r', s'), r, s). C' r s \<and> (r', s') \<in> fst (B' r s) \<and> whileLoop_terminates C' B' r s} proof (prove)
goal (4 subgoals):
 1. \<And>s s' conc_r new_s. \<lbrakk>(s, s') \<in> srel; P r s; P' r' s'; nf'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (\<exists>rv sa. (sa, s) \<in> srel \<and> rrel rv conc_r \<and> P rv sa \<and> P' conc_r s) \<and> C' conc_r s \<and> s = new_s\<rbrace> B' conc_r \<lbrace>\<lambda>rv s. (rv, s) \<in> fst (B' conc_r new_s)\<rbrace>
 2. \<And>s s' conc_r new_s. \<lbrakk>(s, s') \<in> srel; P r s; P' r' s'; nf'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (\<exists>rv sa. (sa, s) \<in> srel \<and> rrel rv conc_r \<and> P rv sa \<and> P' conc_r s) \<and> C' conc_r s \<and> s = new_s\<rbrace> B' conc_r \<lbrace>\<lambda>rv s. whileLoop_terminates C' B' conc_r new_s\<rbrace>
 3. \<And>s s' conc_r new_s. \<lbrakk>(s, s') \<in> srel; P r s; P' r' s'; nf'\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s'. (\<exists>rv s. (s, s') \<in> srel \<and> rrel rv conc_r \<and> P rv s \<and> P' conc_r s') \<and> C' conc_r s' \<and> s' = new_s) (B' conc_r)
 4. \<And>s t. \<lbrakk>(s, t) \<in> srel; P r s; P' r' t; nf'\<rbrakk> \<Longrightarrow> wf {((r', s'), r, s). C' r s \<and> (r', s') \<in> fst (B' r s) \<and> whileLoop_terminates C' B' r s} proof (prove)
goal (3 subgoals):
 1. \<And>s s' conc_r new_s. \<lbrakk>(s, s') \<in> srel; P r s; P' r' s'; nf'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (\<exists>rv sa. (sa, s) \<in> srel \<and> rrel rv conc_r \<and> P rv sa \<and> P' conc_r s) \<and> C' conc_r s \<and> s = new_s\<rbrace> B' conc_r \<lbrace>\<lambda>rv s. whileLoop_terminates C' B' conc_r new_s\<rbrace>
 2. \<And>s s' conc_r new_s. \<lbrakk>(s, s') \<in> srel; P r s; P' r' s'; nf'\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s'. (\<exists>rv s. (s, s') \<in> srel \<and> rrel rv conc_r \<and> P rv s \<and> P' conc_r s') \<and> C' conc_r s' \<and> s' = new_s) (B' conc_r)
 3. \<And>s t. \<lbrakk>(s, t) \<in> srel; P r s; P' r' t; nf'\<rbrakk> \<Longrightarrow> wf {((r', s'), r, s). C' r s \<and> (r', s') \<in> fst (B' r s) \<and> whileLoop_terminates C' B' r s} proof (prove)
goal (3 subgoals):
 1. \<And>s s' conc_r new_s rv sa. \<lbrakk>(s, s') \<in> srel; P r s; P' r' s'; nf'; C' conc_r new_s; (sa, new_s) \<in> srel; rrel rv conc_r; P rv sa; P' conc_r new_s\<rbrakk> \<Longrightarrow> whileLoop_terminates C' B' conc_r new_s
 2. \<And>s s' conc_r new_s. \<lbrakk>(s, s') \<in> srel; P r s; P' r' s'; nf'\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s'. (\<exists>rv s. (s, s') \<in> srel \<and> rrel rv conc_r \<and> P rv s \<and> P' conc_r s') \<and> C' conc_r s' \<and> s' = new_s) (B' conc_r)
 3. \<And>s t. \<lbrakk>(s, t) \<in> srel; P r s; P' r' t; nf'\<rbrakk> \<Longrightarrow> wf {((r', s'), r, s). C' r s \<and> (r', s') \<in> fst (B' r s) \<and> whileLoop_terminates C' B' r s} proof (prove)
goal (2 subgoals):
 1. \<And>s s' conc_r new_s. \<lbrakk>(s, s') \<in> srel; P r s; P' r' s'; nf'\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s'. (\<exists>rv s. (s, s') \<in> srel \<and> rrel rv conc_r \<and> P rv s \<and> P' conc_r s') \<and> C' conc_r s' \<and> s' = new_s) (B' conc_r)
 2. \<And>s t. \<lbrakk>(s, t) \<in> srel; P r s; P' r' t; nf'\<rbrakk> \<Longrightarrow> wf {((r', s'), r, s). C' r s \<and> (r', s') \<in> fst (B' r s) \<and> whileLoop_terminates C' B' r s} proof (prove)
goal (3 subgoals):
 1. \<And>s s' conc_r new_s sa. \<lbrakk>(s, s') \<in> srel; P r s; P' r' s'; nf'; (\<exists>rv s. (s, sa) \<in> srel \<and> rrel rv conc_r \<and> P rv s \<and> P' conc_r sa) \<and> C' conc_r sa \<and> sa = new_s\<rbrakk> \<Longrightarrow> \<exists>rv s. (s, sa) \<in> srel \<and> rrel rv conc_r \<and> P rv s \<and> (P' conc_r sa \<and> C' conc_r sa) \<and> sa = new_s
 2. \<And>s s' conc_r new_s. \<lbrakk>(s, s') \<in> srel; P r s; P' r' s'; nf'\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s'. \<exists>rv s. (s, s') \<in> srel \<and> rrel rv conc_r \<and> P rv s \<and> (P' conc_r s' \<and> C' conc_r s') \<and> s' = new_s) (B' conc_r)
 3. \<And>s t. \<lbrakk>(s, t) \<in> srel; P r s; P' r' t; nf'\<rbrakk> \<Longrightarrow> wf {((r', s'), r, s). C' r s \<and> (r', s') \<in> fst (B' r s) \<and> whileLoop_terminates C' B' r s} proof (prove)
goal (2 subgoals):
 1. \<And>s s' conc_r new_s. \<lbrakk>(s, s') \<in> srel; P r s; P' r' s'; nf'\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s'. \<exists>rv s. (s, s') \<in> srel \<and> rrel rv conc_r \<and> P rv s \<and> (P' conc_r s' \<and> C' conc_r s') \<and> s' = new_s) (B' conc_r)
 2. \<And>s t. \<lbrakk>(s, t) \<in> srel; P r s; P' r' t; nf'\<rbrakk> \<Longrightarrow> wf {((r', s'), r, s). C' r s \<and> (r', s') \<in> fst (B' r s) \<and> whileLoop_terminates C' B' r s} proof (prove)
goal (2 subgoals):
 1. \<And>s s' conc_r new_s rv. \<lbrakk>(s, s') \<in> srel; P r s; P' r' s'; nf'\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s. \<exists>sa. (sa, s) \<in> srel \<and> rrel rv conc_r \<and> P rv sa \<and> (P' conc_r s \<and> C' conc_r s) \<and> s = new_s) (B' conc_r)
 2. \<And>s t. \<lbrakk>(s, t) \<in> srel; P r s; P' r' t; nf'\<rbrakk> \<Longrightarrow> wf {((r', s'), r, s). C' r s \<and> (r', s') \<in> fst (B' r s) \<and> whileLoop_terminates C' B' r s} proof (prove)
goal (2 subgoals):
 1. \<And>s s' conc_r new_s abs_r. \<lbrakk>(s, s') \<in> srel; P r s; P' r' s'; nf'\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s. \<exists>sa. (sa, s) \<in> srel \<and> rrel abs_r conc_r \<and> P abs_r sa \<and> (P' conc_r s \<and> C' conc_r s) \<and> s = new_s) (B' conc_r)
 2. \<And>s t. \<lbrakk>(s, t) \<in> srel; P r s; P' r' t; nf'\<rbrakk> \<Longrightarrow> wf {((r', s'), r, s). C' r s \<and> (r', s') \<in> fst (B' r s) \<and> whileLoop_terminates C' B' r s} proof (prove)
goal (3 subgoals):
 1. \<And>s s' conc_r new_s abs_r. \<lbrakk>(s, s') \<in> srel; P r s; P' r' s'; nf'\<rbrakk> \<Longrightarrow> no_fail (?P280 s s' conc_r new_s abs_r) (B' conc_r)
 2. \<And>s s' conc_r new_s abs_r sa. \<lbrakk>(s, s') \<in> srel; P r s; P' r' s'; nf'; \<exists>s. (s, sa) \<in> srel \<and> rrel abs_r conc_r \<and> P abs_r s \<and> (P' conc_r sa \<and> C' conc_r sa) \<and> sa = new_s\<rbrakk> \<Longrightarrow> ?P280 s s' conc_r new_s abs_r sa
 3. \<And>s t. \<lbrakk>(s, t) \<in> srel; P r s; P' r' t; nf'\<rbrakk> \<Longrightarrow> wf {((r', s'), r, s). C' r s \<and> (r', s') \<in> fst (B' r s) \<and> whileLoop_terminates C' B' r s} proof (prove)
goal (3 subgoals):
 1. \<And>s s' conc_r new_s abs_r. \<lbrakk>(s, s') \<in> srel; P r s; P' r' s'; nf'; rrel abs_r conc_r\<rbrakk> \<Longrightarrow> no_fail (?P283 s s' conc_r new_s abs_r) (B' conc_r)
 2. \<And>s s' conc_r new_s abs_r sa. \<lbrakk>(s, s') \<in> srel; P r s; P' r' s'; nf'; \<exists>s. (s, sa) \<in> srel \<and> rrel abs_r conc_r \<and> P abs_r s \<and> (P' conc_r sa \<and> C' conc_r sa) \<and> sa = new_s\<rbrakk> \<Longrightarrow> rrel abs_r conc_r \<and> ?P283 s s' conc_r new_s abs_r sa
 3. \<And>s t. \<lbrakk>(s, t) \<in> srel; P r s; P' r' t; nf'\<rbrakk> \<Longrightarrow> wf {((r', s'), r, s). C' r s \<and> (r', s') \<in> fst (B' r s) \<and> whileLoop_terminates C' B' r s} proof (prove)
goal (2 subgoals):
 1. \<And>s s' conc_r new_s abs_r sa. \<lbrakk>(s, s') \<in> srel; P r s; P' r' s'; nf'; \<exists>s. (s, sa) \<in> srel \<and> rrel abs_r conc_r \<and> P abs_r s \<and> (P' conc_r sa \<and> C' conc_r sa) \<and> sa = new_s\<rbrakk> \<Longrightarrow> rrel abs_r conc_r \<and> (P' conc_r and C' conc_r and ex_abs_underlying srel (P abs_r and C abs_r)) sa
 2. \<And>s t. \<lbrakk>(s, t) \<in> srel; P r s; P' r' t; nf'\<rbrakk> \<Longrightarrow> wf {((r', s'), r, s). C' r s \<and> (r', s') \<in> fst (B' r s) \<and> whileLoop_terminates C' B' r s} proof (prove)
goal (1 subgoal):
 1. \<And>s t. \<lbrakk>(s, t) \<in> srel; P r s; P' r' t; nf'\<rbrakk> \<Longrightarrow> wf {((r', s'), r, s). C' r s \<and> (r', s') \<in> fst (B' r s) \<and> whileLoop_terminates C' B' r s} proof (prove)
goal:
No subgoals!