theory ExtraCorres

lemma whileLoop_terminates_cross:
  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 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_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 ex_abs: "ex_abs_underlying srel (P r) s'"
  assumes rrel: "rrel r r'"
  assumes P': "P' r' s'"
  assumes nf: "\<And>r. nf \<Longrightarrow> no_fail (P r and C r) (B r)"
  shows "whileLoop_terminates C' B' r' s'" proof - have helper: "\<And>s. P r s \<and> C r s \<Longrightarrow> \<forall>r' s'. rrel r r' \<and> (s, s') \<in> srel \<and> P r s \<and> P' r' s'
                                               \<longrightarrow> whileLoop_terminates C' B' r' s'"
       (is "\<And>s. _ \<Longrightarrow> ?I r s") apply (rule_tac P="?I" in whileLoop_terminates.induct) apply (fastforce intro: abs_termination) apply (fastforce simp: whileLoop_terminates.intros dest: cond) apply (subst whileLoop_terminates.simps) apply clarsimp apply (frule (1) corres_underlyingD2[OF body_corres], (fastforce dest: nf simp: no_fail_def)+) apply (fastforce dest: use_valid intro: body_inv) done show ?thesis apply (insert assms helper) apply (cases "C' r' s'") apply (fastforce simp: ex_abs_underlying_def) apply (simp add: whileLoop_terminates.intros(1)) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. whileLoop_terminates C' B' r' s' proof (state)
goal (1 subgoal):
 1. whileLoop_terminates C' B' r' s' proof (prove)
goal (1 subgoal):
 1. \<And>s. P r s \<and> C r s \<Longrightarrow> \<forall>r' s'. rrel r r' \<and> (s, s') \<in> srel \<and> P r s \<and> P' r' s' \<longrightarrow> whileLoop_terminates C' B' r' s' proof (prove)
goal (3 subgoals):
 1. \<And>s. P r s \<and> C r s \<Longrightarrow> whileLoop_terminates (?C s) (?B s) r s
 2. \<And>s ra sa. \<lbrakk>P r s \<and> C r s; \<not> ?C s ra sa\<rbrakk> \<Longrightarrow> \<forall>r' s'. rrel ra r' \<and> (sa, s') \<in> srel \<and> P ra sa \<and> P' r' s' \<longrightarrow> whileLoop_terminates C' B' r' s'
 3. \<And>s ra sa. \<lbrakk>P r s \<and> C r s; ?C s ra sa; \<forall>(r', s')\<in>fst (?B s ra sa). whileLoop_terminates (?C s) (?B s) r' s' \<and> (\<forall>r'a s'a. rrel r' r'a \<and> (s', s'a) \<in> srel \<and> P r' s' \<and> P' r'a s'a \<longrightarrow> whileLoop_terminates C' B' r'a s'a)\<rbrakk> \<Longrightarrow> \<forall>r' s'. rrel ra r' \<and> (sa, s') \<in> srel \<and> P ra sa \<and> P' r' s' \<longrightarrow> whileLoop_terminates C' B' r' s' proof (prove)
goal (2 subgoals):
 1. \<And>s ra sa. \<lbrakk>P r s \<and> C r s; \<not> C ra sa\<rbrakk> \<Longrightarrow> \<forall>r' s'. rrel ra r' \<and> (sa, s') \<in> srel \<and> P ra sa \<and> P' r' s' \<longrightarrow> whileLoop_terminates C' B' r' s'
 2. \<And>s ra sa. \<lbrakk>P r s \<and> C r s; C ra sa; \<forall>(r', s')\<in>fst (B ra sa). whileLoop_terminates C B r' s' \<and> (\<forall>r'a s'a. rrel r' r'a \<and> (s', s'a) \<in> srel \<and> P r' s' \<and> P' r'a s'a \<longrightarrow> whileLoop_terminates C' B' r'a s'a)\<rbrakk> \<Longrightarrow> \<forall>r' s'. rrel ra r' \<and> (sa, s') \<in> srel \<and> P ra sa \<and> P' r' s' \<longrightarrow> whileLoop_terminates C' B' r' s' proof (prove)
goal (1 subgoal):
 1. \<And>s ra sa. \<lbrakk>P r s \<and> C r s; C ra sa; \<forall>(r', s')\<in>fst (B ra sa). whileLoop_terminates C B r' s' \<and> (\<forall>r'a s'a. rrel r' r'a \<and> (s', s'a) \<in> srel \<and> P r' s' \<and> P' r'a s'a \<longrightarrow> whileLoop_terminates C' B' r'a s'a)\<rbrakk> \<Longrightarrow> \<forall>r' s'. rrel ra r' \<and> (sa, s') \<in> srel \<and> P ra sa \<and> P' r' s' \<longrightarrow> whileLoop_terminates C' B' r' s' proof (prove)
goal (1 subgoal):
 1. \<And>s ra sa. \<lbrakk>P r s \<and> C r s; C ra sa; \<forall>(r', s')\<in>fst (B ra sa). whileLoop_terminates C B r' s' \<and> (\<forall>r'a s'a. rrel r' r'a \<and> (s', s'a) \<in> srel \<and> P r' s' \<and> P' r'a s'a \<longrightarrow> whileLoop_terminates C' B' r'a s'a)\<rbrakk> \<Longrightarrow> \<forall>r' s'. rrel ra r' \<and> (sa, s') \<in> srel \<and> P ra sa \<and> P' r' s' \<longrightarrow> (\<exists>r s. r' = r \<and> s' = s \<and> \<not> C' r s) \<or> (\<exists>r s. r' = r \<and> s' = s \<and> C' r s \<and> (\<forall>(x, y)\<in>fst (B' r s). whileLoop_terminates C' B' x y)) proof (prove)
goal (1 subgoal):
 1. \<And>s ra sa r' s' a b. \<lbrakk>C ra sa; \<forall>x\<in>fst (B ra sa). case x of (r', s') \<Rightarrow> whileLoop_terminates C B r' s' \<and> (\<forall>r'a s'a. rrel r' r'a \<and> (s', s'a) \<in> srel \<and> P r' s' \<and> P' r'a s'a \<longrightarrow> whileLoop_terminates C' B' r'a s'a); P r s; C r s; rrel ra r'; (sa, s') \<in> srel; P ra sa; P' r' s'; C' r' s'; (a, b) \<in> fst (B' r' s')\<rbrakk> \<Longrightarrow> whileLoop_terminates C' B' a b proof (prove)
goal (1 subgoal):
 1. \<And>s ra sa r' s' a b. \<lbrakk>C ra sa; \<forall>x\<in>fst (B ra sa). case x of (r', s') \<Rightarrow> whileLoop_terminates C B r' s' \<and> (\<forall>r'a s'a. rrel r' r'a \<and> (s', s'a) \<in> srel \<and> P r' s' \<and> P' r'a s'a \<longrightarrow> whileLoop_terminates C' B' r'a s'a); P r s; C r s; rrel ra r'; (sa, s') \<in> srel; P ra sa; P' r' s'; C' r' s'; (a, b) \<in> fst (B' r' s'); \<exists>(r, t)\<in>fst (B ra sa). (t, b) \<in> srel \<and> rrel r a\<rbrakk> \<Longrightarrow> whileLoop_terminates C' B' a b proof (prove)
goal:
No subgoals! proof (state)
this:
P r ?s \<and> C r ?s \<Longrightarrow> \<forall>r' s'. rrel r r' \<and> (?s, s') \<in> srel \<and> P r ?s \<and> P' r' s' \<longrightarrow> whileLoop_terminates C' B' r' s'

goal (1 subgoal):
 1. whileLoop_terminates C' B' r' s' proof (prove)
goal (1 subgoal):
 1. whileLoop_terminates C' B' r' s' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<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'); \<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'; \<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>; \<And>r s. \<lbrakk>P r s; C r s\<rbrakk> \<Longrightarrow> whileLoop_terminates C B r s; ex_abs_underlying srel (P r) s'; rrel r r'; P' r' s'; \<And>r. nf \<Longrightarrow> no_fail (P r and C r) (B r); \<And>s. P r s \<and> C r s \<Longrightarrow> \<forall>r' s'. rrel r r' \<and> (s, s') \<in> srel \<and> P r s \<and> P' r' s' \<longrightarrow> whileLoop_terminates C' B' r' s'\<rbrakk> \<Longrightarrow> whileLoop_terminates C' B' r' s' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<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'); \<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'; \<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>; \<And>r s. \<lbrakk>P r s; C r s\<rbrakk> \<Longrightarrow> whileLoop_terminates C B r s; ex_abs_underlying srel (P r) s'; rrel r r'; P' r' s'; \<And>r. nf \<Longrightarrow> no_fail (P r and C r) (B r); \<And>s. P r s \<and> C r s \<Longrightarrow> \<forall>r' s'. rrel r r' \<and> (s, s') \<in> srel \<and> P r s \<and> P' r' s' \<longrightarrow> whileLoop_terminates C' B' r' s'; C' r' s'\<rbrakk> \<Longrightarrow> whileLoop_terminates C' B' r' s'
 2. \<lbrakk>\<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'); \<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'; \<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>; \<And>r s. \<lbrakk>P r s; C r s\<rbrakk> \<Longrightarrow> whileLoop_terminates C B r s; ex_abs_underlying srel (P r) s'; rrel r r'; P' r' s'; \<And>r. nf \<Longrightarrow> no_fail (P r and C r) (B r); \<And>s. P r s \<and> C r s \<Longrightarrow> \<forall>r' s'. rrel r r' \<and> (s, s') \<in> srel \<and> P r s \<and> P' r' s' \<longrightarrow> whileLoop_terminates C' B' r' s'; \<not> C' r' s'\<rbrakk> \<Longrightarrow> whileLoop_terminates C' B' r' s' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<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'); \<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'; \<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>; \<And>r s. \<lbrakk>P r s; C r s\<rbrakk> \<Longrightarrow> whileLoop_terminates C B r s; ex_abs_underlying srel (P r) s'; rrel r r'; P' r' s'; \<And>r. nf \<Longrightarrow> no_fail (P r and C r) (B r); \<And>s. P r s \<and> C r s \<Longrightarrow> \<forall>r' s'. rrel r r' \<and> (s, s') \<in> srel \<and> P r s \<and> P' r' s' \<longrightarrow> whileLoop_terminates C' B' r' s'; \<not> C' r' s'\<rbrakk> \<Longrightarrow> whileLoop_terminates C' B' r' s' proof (prove)
goal:
No subgoals! proof (state)
this:
whileLoop_terminates C' B' r' s'

goal:
No subgoals!