theory ExtraCorres

lemma corres_whileLoop_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 False nf' rrel (P r and C r) (P' r' and C' r') (B r) (B' 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 rel: "rrel r r'"
  assumes nf': "\<And>r'. no_fail (P' r' and C' r') (B' r')"
  assumes termin: "\<And>r' s'. \<lbrakk>P' r' s'; C' r' s'\<rbrakk> \<Longrightarrow> whileLoop_terminates C' B' r' s'"
  shows "corres_underlying srel False nf' rrel (P r) (P' r') (whileLoop C B r) (whileLoop C' B' r')" apply (rule corres_no_failI) apply (simp add: no_fail_def) apply (intro impI allI) apply (erule_tac I="\<lambda>r' s'. P' r' 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 (clarsimp simp: validNF_def) apply (rule conjI) apply (intro hoare_vcg_conj_lift_pre_fix; wpsimp?) using body_inv apply (fastforce simp: valid_def) apply (clarsimp simp: valid_def) apply (insert termin)[1] apply wpsimp apply (fastforce intro: no_fail_pre nf') apply (fastforce intro: wf_subset[OF whileLoop_terminates_wf[where C=C']]) apply clarsimp apply (frule in_whileLoop_corres[OF body_corres body_inv]; (fastforce dest: cond)?) apply (fastforce intro: assms) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying srel False nf' rrel (P r) (P' r') (whileLoop C
  B r) (whileLoop C'
  B' r') proof (prove)
goal (2 subgoals):
 1. nf' \<Longrightarrow> no_fail (P' r') (whileLoop C'
  B' r')
 2. \<forall>(s, s')\<in>srel. P r s \<and> P' r' s' \<longrightarrow> (\<forall>(r', t')\<in>fst (whileLoop C'
  B' r' s'). \<exists>(r, t)\<in>fst (whileLoop C
  B r s). (t, t') \<in> srel \<and> rrel r r') proof (prove)
goal (2 subgoals):
 1. nf' \<Longrightarrow> \<forall>s. P' r' s \<longrightarrow> \<not> snd (whileLoop C'
  B' r' s)
 2. \<forall>(s, s')\<in>srel. P r s \<and> P' r' s' \<longrightarrow> (\<forall>(r', t')\<in>fst (whileLoop C'
  B' r' s'). \<exists>(r, t)\<in>fst (whileLoop C
  B r s). (t, t') \<in> srel \<and> rrel r r') proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>nf'; P' r' s\<rbrakk> \<Longrightarrow> \<not> snd (whileLoop C'
  B' r' s)
 2. \<forall>(s, s')\<in>srel. P r s \<and> P' r' s' \<longrightarrow> (\<forall>(r', t')\<in>fst (whileLoop C'
  B' r' s'). \<exists>(r, t)\<in>fst (whileLoop C
  B r s). (t, t') \<in> srel \<and> rrel r r') proof (prove)
goal (3 subgoals):
 1. \<And>s r sa. nf' \<Longrightarrow> \<lbrace>\<lambda>s'. P' r s' \<and> C' r s' \<and> s' = sa\<rbrace> B' r \<lbrace>\<lambda>r' s'. P' r' s' \<and> ((r', s'), r, 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. nf' \<Longrightarrow> wf {((r', s'), r, s). C' r s \<and> (r', s') \<in> fst (B' r s) \<and> whileLoop_terminates C' B' r s}
 3. \<forall>(s, s')\<in>srel. P r s \<and> P' r' s' \<longrightarrow> (\<forall>(r', t')\<in>fst (whileLoop C'
  B' r' s'). \<exists>(r, t)\<in>fst (whileLoop C
  B r s). (t, t') \<in> srel \<and> rrel r r') proof (prove)
goal (3 subgoals):
 1. \<And>r sa. nf' \<Longrightarrow> \<lbrace>\<lambda>s'. P' r s' \<and> C' r s' \<and> s' = sa\<rbrace> B' r \<lbrace>\<lambda>r' s'. P' r' s' \<and> C' r sa \<and> (r', s') \<in> fst (B' r sa) \<and> whileLoop_terminates C' B' r sa\<rbrace> \<and> no_fail (\<lambda>s'. P' r s' \<and> C' r s' \<and> s' = sa) (B' r)
 2. \<And>s. nf' \<Longrightarrow> wf {((r', s'), r, s). C' r s \<and> (r', s') \<in> fst (B' r s) \<and> whileLoop_terminates C' B' r s}
 3. \<forall>(s, s')\<in>srel. P r s \<and> P' r' s' \<longrightarrow> (\<forall>(r', t')\<in>fst (whileLoop C'
  B' r' s'). \<exists>(r, t)\<in>fst (whileLoop C
  B r s). (t, t') \<in> srel \<and> rrel r r') proof (prove)
goal (4 subgoals):
 1. \<And>r sa. nf' \<Longrightarrow> \<lbrace>\<lambda>s'. P' r s' \<and> C' r s' \<and> s' = sa\<rbrace> B' r \<lbrace>\<lambda>r' s'. P' r' s' \<and> C' r sa \<and> (r', s') \<in> fst (B' r sa) \<and> whileLoop_terminates C' B' r sa\<rbrace>
 2. \<And>r sa. nf' \<Longrightarrow> no_fail (\<lambda>s'. P' r s' \<and> C' r s' \<and> s' = sa) (B' r)
 3. \<And>s. nf' \<Longrightarrow> wf {((r', s'), r, s). C' r s \<and> (r', s') \<in> fst (B' r s) \<and> whileLoop_terminates C' B' r s}
 4. \<forall>(s, s')\<in>srel. P r s \<and> P' r' s' \<longrightarrow> (\<forall>(r', t')\<in>fst (whileLoop C'
  B' r' s'). \<exists>(r, t)\<in>fst (whileLoop C
  B r s). (t, t') \<in> srel \<and> rrel r r') proof (prove)
goal (6 subgoals):
 1. \<And>r sa. nf' \<Longrightarrow> \<lbrace>\<lambda>s. P' r s \<and> C' r s \<and> s = sa\<rbrace> B' r \<lbrace>P'\<rbrace>
 2. \<And>r sa. nf' \<Longrightarrow> \<lbrace>\<lambda>s. P' r s \<and> C' r s \<and> s = sa\<rbrace> B' r \<lbrace>\<lambda>rv s. (rv, s) \<in> fst (B' r sa)\<rbrace>
 3. \<And>r sa. \<lbrakk>nf'; P' r sa; C' r sa\<rbrakk> \<Longrightarrow> whileLoop_terminates C' B' r sa
 4. \<And>r sa. nf' \<Longrightarrow> no_fail (\<lambda>s'. P' r s' \<and> C' r s' \<and> s' = sa) (B' r)
 5. \<And>s. nf' \<Longrightarrow> wf {((r', s'), r, s). C' r s \<and> (r', s') \<in> fst (B' r s) \<and> whileLoop_terminates C' B' r s}
 6. \<forall>(s, s')\<in>srel. P r s \<and> P' r' s' \<longrightarrow> (\<forall>(r', t')\<in>fst (whileLoop C'
  B' r' s'). \<exists>(r, t)\<in>fst (whileLoop C
  B r s). (t, t') \<in> srel \<and> rrel r r') proof (prove)
using this:
\<lbrace>P ?r and C ?r\<rbrace> B ?r \<lbrace>P\<rbrace>
\<lbrace>P' ?r' and C' ?r'\<rbrace> B' ?r' \<lbrace>P'\<rbrace>

goal (6 subgoals):
 1. \<And>r sa. nf' \<Longrightarrow> \<lbrace>\<lambda>s. P' r s \<and> C' r s \<and> s = sa\<rbrace> B' r \<lbrace>P'\<rbrace>
 2. \<And>r sa. nf' \<Longrightarrow> \<lbrace>\<lambda>s. P' r s \<and> C' r s \<and> s = sa\<rbrace> B' r \<lbrace>\<lambda>rv s. (rv, s) \<in> fst (B' r sa)\<rbrace>
 3. \<And>r sa. \<lbrakk>nf'; P' r sa; C' r sa\<rbrakk> \<Longrightarrow> whileLoop_terminates C' B' r sa
 4. \<And>r sa. nf' \<Longrightarrow> no_fail (\<lambda>s'. P' r s' \<and> C' r s' \<and> s' = sa) (B' r)
 5. \<And>s. nf' \<Longrightarrow> wf {((r', s'), r, s). C' r s \<and> (r', s') \<in> fst (B' r s) \<and> whileLoop_terminates C' B' r s}
 6. \<forall>(s, s')\<in>srel. P r s \<and> P' r' s' \<longrightarrow> (\<forall>(r', t')\<in>fst (whileLoop C'
  B' r' s'). \<exists>(r, t)\<in>fst (whileLoop C
  B r s). (t, t') \<in> srel \<and> rrel r r') proof (prove)
goal (5 subgoals):
 1. \<And>r sa. nf' \<Longrightarrow> \<lbrace>\<lambda>s. P' r s \<and> C' r s \<and> s = sa\<rbrace> B' r \<lbrace>\<lambda>rv s. (rv, s) \<in> fst (B' r sa)\<rbrace>
 2. \<And>r sa. \<lbrakk>nf'; P' r sa; C' r sa\<rbrakk> \<Longrightarrow> whileLoop_terminates C' B' r sa
 3. \<And>r sa. nf' \<Longrightarrow> no_fail (\<lambda>s'. P' r s' \<and> C' r s' \<and> s' = sa) (B' r)
 4. \<And>s. nf' \<Longrightarrow> wf {((r', s'), r, s). C' r s \<and> (r', s') \<in> fst (B' r s) \<and> whileLoop_terminates C' B' r s}
 5. \<forall>(s, s')\<in>srel. P r s \<and> P' r' s' \<longrightarrow> (\<forall>(r', t')\<in>fst (whileLoop C'
  B' r' s'). \<exists>(r, t)\<in>fst (whileLoop C
  B r s). (t, t') \<in> srel \<and> rrel r r') proof (prove)
goal (4 subgoals):
 1. \<And>r sa. \<lbrakk>nf'; P' r sa; C' r sa\<rbrakk> \<Longrightarrow> whileLoop_terminates C' B' r sa
 2. \<And>r sa. nf' \<Longrightarrow> no_fail (\<lambda>s'. P' r s' \<and> C' r s' \<and> s' = sa) (B' r)
 3. \<And>s. nf' \<Longrightarrow> wf {((r', s'), r, s). C' r s \<and> (r', s') \<in> fst (B' r s) \<and> whileLoop_terminates C' B' r s}
 4. \<forall>(s, s')\<in>srel. P r s \<and> P' r' s' \<longrightarrow> (\<forall>(r', t')\<in>fst (whileLoop C'
  B' r' s'). \<exists>(r, t)\<in>fst (whileLoop C
  B r s). (t, t') \<in> srel \<and> rrel r r') proof (prove)
goal (4 subgoals):
 1. \<And>r sa. \<lbrakk>nf'; P' r sa; C' r sa; \<And>r' s'. \<lbrakk>P' r' s'; C' r' s'\<rbrakk> \<Longrightarrow> whileLoop_terminates C' B' r' s'\<rbrakk> \<Longrightarrow> whileLoop_terminates C' B' r sa
 2. \<And>r sa. nf' \<Longrightarrow> no_fail (\<lambda>s'. P' r s' \<and> C' r s' \<and> s' = sa) (B' r)
 3. \<And>s. nf' \<Longrightarrow> wf {((r', s'), r, s). C' r s \<and> (r', s') \<in> fst (B' r s) \<and> whileLoop_terminates C' B' r s}
 4. \<forall>(s, s')\<in>srel. P r s \<and> P' r' s' \<longrightarrow> (\<forall>(r', t')\<in>fst (whileLoop C'
  B' r' s'). \<exists>(r, t)\<in>fst (whileLoop C
  B r s). (t, t') \<in> srel \<and> rrel r r') proof (prove)
goal (3 subgoals):
 1. \<And>r sa. nf' \<Longrightarrow> no_fail (\<lambda>s'. P' r s' \<and> C' r s' \<and> s' = sa) (B' r)
 2. \<And>s. nf' \<Longrightarrow> wf {((r', s'), r, s). C' r s \<and> (r', s') \<in> fst (B' r s) \<and> whileLoop_terminates C' B' r s}
 3. \<forall>(s, s')\<in>srel. P r s \<and> P' r' s' \<longrightarrow> (\<forall>(r', t')\<in>fst (whileLoop C'
  B' r' s'). \<exists>(r, t)\<in>fst (whileLoop C
  B r s). (t, t') \<in> srel \<and> rrel r r') proof (prove)
goal (2 subgoals):
 1. \<And>s. nf' \<Longrightarrow> wf {((r', s'), r, s). C' r s \<and> (r', s') \<in> fst (B' r s) \<and> whileLoop_terminates C' B' r s}
 2. \<forall>(s, s')\<in>srel. P r s \<and> P' r' s' \<longrightarrow> (\<forall>(r', t')\<in>fst (whileLoop C'
  B' r' s'). \<exists>(r, t)\<in>fst (whileLoop C
  B r s). (t, t') \<in> srel \<and> rrel r r') proof (prove)
goal (1 subgoal):
 1. \<forall>(s, s')\<in>srel. P r s \<and> P' r' s' \<longrightarrow> (\<forall>(r', t')\<in>fst (whileLoop C'
  B' r' s'). \<exists>(r, t)\<in>fst (whileLoop C
  B r s). (t, t') \<in> srel \<and> rrel r r') proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>(a, b) \<in> srel; (aa, ba) \<in> fst (whileLoop C'
  B' r' b); P r a; P' r' b\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (whileLoop C
  B r a). case x of (r, t) \<Rightarrow> (t, ba) \<in> srel \<and> rrel r aa proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>(a, b) \<in> srel; (aa, ba) \<in> fst (whileLoop C'
  B' r' b); P r a; P' r' b; \<forall>s r. (s, b) \<in> srel \<and> rrel r r' \<and> P r s \<and> P' r' b \<longrightarrow> (\<exists>rv t. (rv, t) \<in> fst (whileLoop C
  B r s) \<and> (t, ba) \<in> srel \<and> rrel rv aa)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (whileLoop C
  B r a). case x of (r, t) \<Rightarrow> (t, ba) \<in> srel \<and> rrel r aa proof (prove)
goal:
No subgoals!