theory ADT_IF_Refine

lemma corres_gets_same:
  assumes equiv: "\<And>s s'. \<lbrakk>P s; Q s'; (s, s') \<in> sr\<rbrakk>\<Longrightarrow> f s = g s'"
  and rimp : "\<And>s. P s \<Longrightarrow> R (f s) s"
  and corres: "\<And>r.  corres_underlying sr b c rr (P and (R r) and (\<lambda>s. r = f s)) Q (n r) (m r)"
  shows "corres_underlying sr b c rr P Q (do r \<leftarrow> gets f; n r od) (do r \<leftarrow> gets g; m r od)" apply (rule corres_guard_imp) apply (rule corres_split[where r' = "(=)"]) apply clarsimp apply (rule equiv) apply simp+ apply (rule corres) apply wp+ apply (simp add: rimp) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying sr b c rr P Q (gets f >>= n) (gets g >>= m) proof (prove)
goal (3 subgoals):
 1. corres_underlying sr b c rr ?Q ?Q' (gets f >>= n) (gets g >>= m)
 2. \<And>s. P s \<Longrightarrow> ?Q s
 3. \<And>s. Q s \<Longrightarrow> ?Q' s proof (prove)
goal (6 subgoals):
 1. corres_underlying sr b c (=) ?P4 ?P'4 (gets f) (gets g)
 2. \<And>r ra. r = ra \<Longrightarrow> corres_underlying sr b c rr (?R4 r) (?R'4 ra) (n r) (m ra)
 3. \<lbrace>?Q4\<rbrace> gets f \<lbrace>?R4\<rbrace>
 4. \<lbrace>?Q'4\<rbrace> gets g \<lbrace>?R'4\<rbrace>
 5. \<And>s. P s \<Longrightarrow> (?P4 and ?Q4) s
 6. \<And>s. Q s \<Longrightarrow> (?P'4 and ?Q'4) s proof (prove)
goal (6 subgoals):
 1. \<And>s s'. \<lbrakk>?P4 s; ?P'4 s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> f s = g s'
 2. \<And>r ra. r = ra \<Longrightarrow> corres_underlying sr b c rr (?R4 r) (?R'4 ra) (n r) (m ra)
 3. \<lbrace>?Q4\<rbrace> gets f \<lbrace>?R4\<rbrace>
 4. \<lbrace>?Q'4\<rbrace> gets g \<lbrace>?R'4\<rbrace>
 5. \<And>s. P s \<Longrightarrow> (?P4 and ?Q4) s
 6. \<And>s. Q s \<Longrightarrow> (?P'4 and ?Q'4) s proof (prove)
goal (8 subgoals):
 1. \<And>s s'. \<lbrakk>?P4 s; ?P'4 s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> P s
 2. \<And>s s'. \<lbrakk>?P4 s; ?P'4 s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> Q s'
 3. \<And>s s'. \<lbrakk>?P4 s; ?P'4 s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> (s, s') \<in> sr
 4. \<And>r ra. r = ra \<Longrightarrow> corres_underlying sr b c rr (?R4 r) (?R'4 ra) (n r) (m ra)
 5. \<lbrace>?Q4\<rbrace> gets f \<lbrace>?R4\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> gets g \<lbrace>?R'4\<rbrace>
 7. \<And>s. P s \<Longrightarrow> (?P4 and ?Q4) s
 8. \<And>s. Q s \<Longrightarrow> (?P'4 and ?Q'4) s proof (prove)
goal (5 subgoals):
 1. \<And>r. corres_underlying sr b c rr (?R4 r) (?R'4 r) (n r) (m r)
 2. \<lbrace>?Q4\<rbrace> gets f \<lbrace>?R4\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> gets g \<lbrace>?R'4\<rbrace>
 4. \<And>s. P s \<Longrightarrow> (P and ?Q4) s
 5. \<And>s. Q s \<Longrightarrow> (Q and ?Q'4) s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?Q4\<rbrace> gets f \<lbrace>\<lambda>r. P and R r and (\<lambda>s. r = f s)\<rbrace>
 2. \<lbrace>?Q'4\<rbrace> gets g \<lbrace>\<lambda>r. Q\<rbrace>
 3. \<And>s. P s \<Longrightarrow> (P and ?Q4) s
 4. \<And>s. Q s \<Longrightarrow> (Q and ?Q'4) s proof (prove)
goal (2 subgoals):
 1. \<And>s. P s \<Longrightarrow> (P and (\<lambda>s. (P and R (f s) and (\<lambda>sa. f s = f sa)) s)) s
 2. \<And>s. Q s \<Longrightarrow> (Q and Q) s proof (prove)
goal (1 subgoal):
 1. \<And>s. Q s \<Longrightarrow> (Q and Q) s proof (prove)
goal:
No subgoals!