theory ExtraCorres

lemma corres_gets_the:
  assumes x: "corres_underlying sr nf nf' (r \<circ> the) P P' (gets f) y"
  shows      "corres_underlying sr nf nf' r (P and (\<lambda>s. f s \<noteq> None)) P' (gets_the f) y" proof - have z: "corres_underlying sr nf nf' (\<lambda>x y. \<exists>x'. x = Some x' \<and> r x' y)
                 (P and (\<lambda>s. f s \<noteq> None)) P' (gets f) y" apply (subst corres_cong [OF refl refl refl refl]) defer apply (rule corres_guard_imp[OF x], simp+) apply (clarsimp simp: simpler_gets_def) done show ?thesis apply (rule corres_guard_imp) apply (unfold gets_the_def) apply (subst bind_return[symmetric], rule corres_split [OF z]) apply (rule corres_trivial, clarsimp simp: assert_opt_def) apply (wp | simp)+ done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' r (P and (\<lambda>s. f s \<noteq> None)) P' (gets_the f) y proof (state)
goal (1 subgoal):
 1. corres_underlying sr nf nf' r (P and (\<lambda>s. f s \<noteq> None)) P' (gets_the f) y proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' (\<lambda>x y. \<exists>x'. x = Some x' \<and> r x' y) (P and (\<lambda>s. f s \<noteq> None)) P' (gets f) y proof (prove)
goal (2 subgoals):
 1. \<And>x ya s t s' t'. \<lbrakk>(P and (\<lambda>s. f s \<noteq> None)) s; P' t; (s', t') \<in> sr; (x, s') \<in> fst (gets f s); (ya, t') \<in> fst (y t)\<rbrakk> \<Longrightarrow> (\<exists>x'. x = Some x' \<and> r x' ya) = ?r' x ya
 2. corres_underlying sr nf nf' ?r' (P and (\<lambda>s. f s \<noteq> None)) P' (gets f) y proof (prove)
goal (2 subgoals):
 1. corres_underlying sr nf nf' ?r' (P and (\<lambda>s. f s \<noteq> None)) P' (gets f) y
 2. \<And>x ya s t s' t'. \<lbrakk>(P and (\<lambda>s. f s \<noteq> None)) s; P' t; (s', t') \<in> sr; (x, s') \<in> fst (gets f s); (ya, t') \<in> fst (y t)\<rbrakk> \<Longrightarrow> (\<exists>x'. x = Some x' \<and> r x' ya) = ?r' x ya proof (prove)
goal (1 subgoal):
 1. \<And>x ya s t s' t'. \<lbrakk>P s \<and> (\<exists>y. f s = Some y); P' t; (s', t') \<in> sr; (x, s') \<in> fst (gets f s); (ya, t') \<in> fst (y t)\<rbrakk> \<Longrightarrow> (\<exists>x'. x = Some x' \<and> r x' ya) = r (the x) ya proof (prove)
goal:
No subgoals! proof (state)
this:
corres_underlying sr nf nf' (\<lambda>x y. \<exists>x'. x = Some x' \<and> r x' y) (P and (\<lambda>s. f s \<noteq> None)) P' (gets f) y

goal (1 subgoal):
 1. corres_underlying sr nf nf' r (P and (\<lambda>s. f s \<noteq> None)) P' (gets_the f) y proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' r (P and (\<lambda>s. f s \<noteq> None)) P' (gets_the f) y proof (prove)
goal (3 subgoals):
 1. corres_underlying sr nf nf' r ?Q ?Q' (gets_the f) y
 2. \<And>s. (P and (\<lambda>s. f s \<noteq> None)) s \<Longrightarrow> ?Q s
 3. \<And>s. P' s \<Longrightarrow> ?Q' s proof (prove)
goal (3 subgoals):
 1. corres_underlying sr nf nf' r ?Q ?Q' (gets f >>= assert_opt) y
 2. \<And>s. (P and (\<lambda>s. f s \<noteq> None)) s \<Longrightarrow> ?Q s
 3. \<And>s. P' s \<Longrightarrow> ?Q' s proof (prove)
goal (5 subgoals):
 1. \<And>rv rv'. \<exists>x'. rv = Some x' \<and> r x' rv' \<Longrightarrow> corres_underlying sr nf nf' r (?R7 rv) (?R'7 rv') (assert_opt rv) (return rv')
 2. \<lbrace>?Q7\<rbrace> gets f \<lbrace>?R7\<rbrace>
 3. \<lbrace>?Q'7\<rbrace> y \<lbrace>?R'7\<rbrace>
 4. \<And>s. (P and (\<lambda>s. f s \<noteq> None)) s \<Longrightarrow> (P and (\<lambda>s. f s \<noteq> None) and ?Q7) s
 5. \<And>s. P' s \<Longrightarrow> (P' and ?Q'7) s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?Q7\<rbrace> gets f \<lbrace>\<lambda>rv _. True\<rbrace>
 2. \<lbrace>?Q'7\<rbrace> y \<lbrace>\<lambda>rv' _. True\<rbrace>
 3. \<And>s. (P and (\<lambda>s. f s \<noteq> None)) s \<Longrightarrow> (P and (\<lambda>s. f s \<noteq> None) and ?Q7) s
 4. \<And>s. P' s \<Longrightarrow> (P' and ?Q'7) s proof (prove)
goal:
No subgoals! proof (state)
this:
corres_underlying sr nf nf' r (P and (\<lambda>s. f s \<noteq> None)) P' (gets_the f) y

goal:
No subgoals!