theory ExtraCorres

lemma in_whileLoop_corres:
  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 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 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 result: "(rv', t') \<in> fst (whileLoop C' B' r' s')"
  assumes nf: "\<And>r. nf \<Longrightarrow> no_fail (P r and C r) (B r)"
  shows "\<forall>s r. (s, s') \<in> srel \<and> rrel r r' \<and> P r s \<and> P' r' s'
                \<longrightarrow> (\<exists>rv t. (rv, t) \<in> fst (whileLoop C B r s) \<and> (t, t') \<in> srel \<and> rrel rv rv')" apply (rule in_whileLoop_induct[OF result]) apply (force simp: cond whileLoop_def) apply clarsimp apply (frule (1) corres_underlyingD2[OF body_corres];
         (fastforce dest: nf simp: cond no_fail_def)?) apply clarsimp apply (frule use_valid[OF _ body_inv(1)]) apply (fastforce dest: cond) apply (frule use_valid[OF _ body_inv(2)]) apply fastforce apply (fastforce simp: whileLoop_def intro: whileLoop_results.intros(3) dest: cond) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s r. (s, s') \<in> srel \<and> rrel r r' \<and> P r s \<and> P' r' s' \<longrightarrow> (\<exists>rv t. (rv, t) \<in> fst (whileLoop C
  B r s) \<and> (t, t') \<in> srel \<and> rrel rv rv') proof (prove)
goal (2 subgoals):
 1. \<And>r s. \<not> C' r s \<Longrightarrow> \<forall>sa ra. (sa, s) \<in> srel \<and> rrel ra r \<and> P ra sa \<and> P' r s \<longrightarrow> (\<exists>rv t. (rv, t) \<in> fst (whileLoop C
  B ra sa) \<and> (t, s) \<in> srel \<and> rrel rv r)
 2. \<And>r s r' s' r'' s''. \<lbrakk>C' r s; (r', s') \<in> fst (B' r s); (r'', s'') \<in> fst (whileLoop C'
  B' r' s'); \<forall>s r. (s, s') \<in> srel \<and> rrel r r' \<and> P r s \<and> P' r' s' \<longrightarrow> (\<exists>rv t. (rv, t) \<in> fst (whileLoop C
  B r s) \<and> (t, s'') \<in> srel \<and> rrel rv r'')\<rbrakk> \<Longrightarrow> \<forall>sa ra. (sa, s) \<in> srel \<and> rrel ra r \<and> P ra sa \<and> P' r s \<longrightarrow> (\<exists>rv t. (rv, t) \<in> fst (whileLoop C
  B ra sa) \<and> (t, s'') \<in> srel \<and> rrel rv r'') proof (prove)
goal (1 subgoal):
 1. \<And>r s r' s' r'' s''. \<lbrakk>C' r s; (r', s') \<in> fst (B' r s); (r'', s'') \<in> fst (whileLoop C'
  B' r' s'); \<forall>s r. (s, s') \<in> srel \<and> rrel r r' \<and> P r s \<and> P' r' s' \<longrightarrow> (\<exists>rv t. (rv, t) \<in> fst (whileLoop C
  B r s) \<and> (t, s'') \<in> srel \<and> rrel rv r'')\<rbrakk> \<Longrightarrow> \<forall>sa ra. (sa, s) \<in> srel \<and> rrel ra r \<and> P ra sa \<and> P' r s \<longrightarrow> (\<exists>rv t. (rv, t) \<in> fst (whileLoop C
  B ra sa) \<and> (t, s'') \<in> srel \<and> rrel rv r'') proof (prove)
goal (1 subgoal):
 1. \<And>r s r' s' r'' s'' sa ra. \<lbrakk>C' r s; (r', s') \<in> fst (B' r s); (r'', s'') \<in> fst (whileLoop C'
  B' r' s'); \<forall>s r. (s, s') \<in> srel \<and> rrel r r' \<and> P r s \<and> P' r' s' \<longrightarrow> (\<exists>rv t. (rv, t) \<in> fst (whileLoop C
  B r s) \<and> (t, s'') \<in> srel \<and> rrel rv r''); (sa, s) \<in> srel; rrel ra r; P ra sa; P' r s\<rbrakk> \<Longrightarrow> \<exists>rv t. (rv, t) \<in> fst (whileLoop C
  B ra sa) \<and> (t, s'') \<in> srel \<and> rrel rv r'' proof (prove)
goal (1 subgoal):
 1. \<And>r s r' s' r'' s'' sa ra. \<lbrakk>C' r s; (r', s') \<in> fst (B' r s); (r'', s'') \<in> fst (whileLoop C'
  B' r' s'); \<forall>s r. (s, s') \<in> srel \<and> rrel r r' \<and> P r s \<and> P' r' s' \<longrightarrow> (\<exists>rv t. (rv, t) \<in> fst (whileLoop C
  B r s) \<and> (t, s'') \<in> srel \<and> rrel rv r''); (sa, s) \<in> srel; rrel ra r; P ra sa; P' r s; \<exists>(r, t)\<in>fst (B ra sa). (t, s') \<in> srel \<and> rrel r r'\<rbrakk> \<Longrightarrow> \<exists>rv t. (rv, t) \<in> fst (whileLoop C
  B ra sa) \<and> (t, s'') \<in> srel \<and> rrel rv r'' proof (prove)
goal (1 subgoal):
 1. \<And>r s r' s' r'' s'' sa ra a b. \<lbrakk>C' r s; (r', s') \<in> fst (B' r s); (r'', s'') \<in> fst (whileLoop C'
  B' r' s'); \<forall>s r. (s, s') \<in> srel \<and> rrel r r' \<and> P r s \<and> P' r' s' \<longrightarrow> (\<exists>rv t. (rv, t) \<in> fst (whileLoop C
  B r s) \<and> (t, s'') \<in> srel \<and> rrel rv r''); (sa, s) \<in> srel; rrel ra r; P ra sa; P' r s; (a, b) \<in> fst (B ra sa); (b, s') \<in> srel; rrel a r'\<rbrakk> \<Longrightarrow> \<exists>rv t. (rv, t) \<in> fst (whileLoop C
  B ra sa) \<and> (t, s'') \<in> srel \<and> rrel rv r'' proof (prove)
goal (2 subgoals):
 1. \<And>r s r' s' r'' s'' sa ra a b. \<lbrakk>C' r s; (r', s') \<in> fst (B' r s); (r'', s'') \<in> fst (whileLoop C'
  B' r' s'); \<forall>s r. (s, s') \<in> srel \<and> rrel r r' \<and> P r s \<and> P' r' s' \<longrightarrow> (\<exists>rv t. (rv, t) \<in> fst (whileLoop C
  B r s) \<and> (t, s'') \<in> srel \<and> rrel rv r''); (sa, s) \<in> srel; rrel ra r; P ra sa; P' r s; (a, b) \<in> fst (B ra sa); (b, s') \<in> srel; rrel a r'\<rbrakk> \<Longrightarrow> (P ra and C ra) sa
 2. \<And>r s r' s' r'' s'' sa ra a b. \<lbrakk>C' r s; (r', s') \<in> fst (B' r s); (r'', s'') \<in> fst (whileLoop C'
  B' r' s'); \<forall>s r. (s, s') \<in> srel \<and> rrel r r' \<and> P r s \<and> P' r' s' \<longrightarrow> (\<exists>rv t. (rv, t) \<in> fst (whileLoop C
  B r s) \<and> (t, s'') \<in> srel \<and> rrel rv r''); (sa, s) \<in> srel; rrel ra r; P ra sa; P' r s; (a, b) \<in> fst (B ra sa); (b, s') \<in> srel; rrel a r'; P a b\<rbrakk> \<Longrightarrow> \<exists>rv t. (rv, t) \<in> fst (whileLoop C
  B ra sa) \<and> (t, s'') \<in> srel \<and> rrel rv r'' proof (prove)
goal (1 subgoal):
 1. \<And>r s r' s' r'' s'' sa ra a b. \<lbrakk>C' r s; (r', s') \<in> fst (B' r s); (r'', s'') \<in> fst (whileLoop C'
  B' r' s'); \<forall>s r. (s, s') \<in> srel \<and> rrel r r' \<and> P r s \<and> P' r' s' \<longrightarrow> (\<exists>rv t. (rv, t) \<in> fst (whileLoop C
  B r s) \<and> (t, s'') \<in> srel \<and> rrel rv r''); (sa, s) \<in> srel; rrel ra r; P ra sa; P' r s; (a, b) \<in> fst (B ra sa); (b, s') \<in> srel; rrel a r'; P a b\<rbrakk> \<Longrightarrow> \<exists>rv t. (rv, t) \<in> fst (whileLoop C
  B ra sa) \<and> (t, s'') \<in> srel \<and> rrel rv r'' proof (prove)
goal (2 subgoals):
 1. \<And>r s r' s' r'' s'' sa ra a b. \<lbrakk>C' r s; (r', s') \<in> fst (B' r s); (r'', s'') \<in> fst (whileLoop C'
  B' r' s'); \<forall>s r. (s, s') \<in> srel \<and> rrel r r' \<and> P r s \<and> P' r' s' \<longrightarrow> (\<exists>rv t. (rv, t) \<in> fst (whileLoop C
  B r s) \<and> (t, s'') \<in> srel \<and> rrel rv r''); (sa, s) \<in> srel; rrel ra r; P ra sa; P' r s; (a, b) \<in> fst (B ra sa); (b, s') \<in> srel; rrel a r'; P a b\<rbrakk> \<Longrightarrow> (P' r and C' r) s
 2. \<And>r s r' s' r'' s'' sa ra a b. \<lbrakk>C' r s; (r', s') \<in> fst (B' r s); (r'', s'') \<in> fst (whileLoop C'
  B' r' s'); \<forall>s r. (s, s') \<in> srel \<and> rrel r r' \<and> P r s \<and> P' r' s' \<longrightarrow> (\<exists>rv t. (rv, t) \<in> fst (whileLoop C
  B r s) \<and> (t, s'') \<in> srel \<and> rrel rv r''); (sa, s) \<in> srel; rrel ra r; P ra sa; P' r s; (a, b) \<in> fst (B ra sa); (b, s') \<in> srel; rrel a r'; P a b; P' r' s'\<rbrakk> \<Longrightarrow> \<exists>rv t. (rv, t) \<in> fst (whileLoop C
  B ra sa) \<and> (t, s'') \<in> srel \<and> rrel rv r'' proof (prove)
goal (1 subgoal):
 1. \<And>r s r' s' r'' s'' sa ra a b. \<lbrakk>C' r s; (r', s') \<in> fst (B' r s); (r'', s'') \<in> fst (whileLoop C'
  B' r' s'); \<forall>s r. (s, s') \<in> srel \<and> rrel r r' \<and> P r s \<and> P' r' s' \<longrightarrow> (\<exists>rv t. (rv, t) \<in> fst (whileLoop C
  B r s) \<and> (t, s'') \<in> srel \<and> rrel rv r''); (sa, s) \<in> srel; rrel ra r; P ra sa; P' r s; (a, b) \<in> fst (B ra sa); (b, s') \<in> srel; rrel a r'; P a b; P' r' s'\<rbrakk> \<Longrightarrow> \<exists>rv t. (rv, t) \<in> fst (whileLoop C
  B ra sa) \<and> (t, s'') \<in> srel \<and> rrel rv r'' proof (prove)
goal:
No subgoals!