theory Corres_UL

lemma corres_noopE:
  assumes P: "\<And>s. P s \<Longrightarrow> \<lbrace>\<lambda>s'. (s, s') \<in> sr \<and> P' s'\<rbrace> f \<lbrace>\<lambda>rv s'. (s, s') \<in> sr \<and> r x rv\<rbrace>,\<lbrace>\<lambda>r s. False\<rbrace>"
  assumes nf': "\<And>s. \<lbrakk> P s; nf' \<rbrakk> \<Longrightarrow> no_fail (\<lambda>s'. (s, s') \<in> sr \<and> P' s') f"
  shows "corres_underlying sr nf nf' (fr \<oplus> r) P P' (returnOk x) f" proof - have Q: "\<And>P f Q E. \<lbrace>P\<rbrace>f\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. case_sum (\<lambda>e. E e s) (\<lambda>r. Q r s) r\<rbrace>" by (simp add: validE_def) thus ?thesis apply (simp add: returnOk_def) apply (rule corres_noop) apply (rule hoare_post_imp) defer apply (rule Q) apply (rule P) apply assumption apply (erule(1) nf') apply (simp split: sum.splits) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' (fr \<oplus> r) P P' (returnOk x) f proof (state)
goal (1 subgoal):
 1. corres_underlying sr nf nf' (fr \<oplus> r) P P' (returnOk x) f proof (prove)
goal (1 subgoal):
 1. \<And>P f Q E. \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. case r of Inl e \<Rightarrow> E e s | Inr r \<Rightarrow> Q r s\<rbrace> proof (state)
this:
\<lbrace>?P\<rbrace> ?f \<lbrace>?Q\<rbrace>, \<lbrace>?E\<rbrace> \<Longrightarrow> \<lbrace>?P\<rbrace> ?f \<lbrace>\<lambda>r s. case r of Inl e \<Rightarrow> ?E e s | Inr r \<Rightarrow> ?Q r s\<rbrace>

goal (1 subgoal):
 1. corres_underlying sr nf nf' (fr \<oplus> r) P P' (returnOk x) f proof (prove)
using this:
\<lbrace>?P\<rbrace> ?f \<lbrace>?Q\<rbrace>, \<lbrace>?E\<rbrace> \<Longrightarrow> \<lbrace>?P\<rbrace> ?f \<lbrace>\<lambda>r s. case r of Inl e \<Rightarrow> ?E e s | Inr r \<Rightarrow> ?Q r s\<rbrace>

goal (1 subgoal):
 1. corres_underlying sr nf nf' (fr \<oplus> r) P P' (returnOk x) f proof (prove)
goal (1 subgoal):
 1. (\<And>P f Q E. \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. case r of Inl e \<Rightarrow> E e s | Inr r \<Rightarrow> Q r s\<rbrace>) \<Longrightarrow> corres_underlying sr nf nf' (fr \<oplus> r) P P' (return (Inr x)) f proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<And>P f Q E. \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. case r of Inl e \<Rightarrow> E e s | Inr r \<Rightarrow> Q r s\<rbrace>; P s\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s'. (s, s') \<in> sr \<and> P' s'\<rbrace> f \<lbrace>\<lambda>rv s'. (s, s') \<in> sr \<and> (fr \<oplus> r) (Inr x) rv\<rbrace>
 2. \<And>s. \<lbrakk>\<And>P f Q E. \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. case r of Inl e \<Rightarrow> E e s | Inr r \<Rightarrow> Q r s\<rbrace>; P s; nf'\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s'. (s, s') \<in> sr \<and> P' s') f proof (prove)
goal (3 subgoals):
 1. \<And>s rv sa. \<lbrakk>\<And>P f Q E. \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. case r of Inl e \<Rightarrow> E e s | Inr r \<Rightarrow> Q r s\<rbrace>; P s; ?Q6 s rv sa\<rbrakk> \<Longrightarrow> (s, sa) \<in> sr \<and> (fr \<oplus> r) (Inr x) rv
 2. \<And>s. \<lbrakk>\<And>P f Q E. \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. case r of Inl e \<Rightarrow> E e s | Inr r \<Rightarrow> Q r s\<rbrace>; P s\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s'. (s, s') \<in> sr \<and> P' s'\<rbrace> f \<lbrace>?Q6 s\<rbrace>
 3. \<And>s. \<lbrakk>\<And>P f Q E. \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. case r of Inl e \<Rightarrow> E e s | Inr r \<Rightarrow> Q r s\<rbrace>; P s; nf'\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s'. (s, s') \<in> sr \<and> P' s') f proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>\<And>P f Q E. \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. case r of Inl e \<Rightarrow> E e s | Inr r \<Rightarrow> Q r s\<rbrace>; P s\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s'. (s, s') \<in> sr \<and> P' s'\<rbrace> f \<lbrace>?Q6 s\<rbrace>
 2. \<And>s. \<lbrakk>\<And>P f Q E. \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. case r of Inl e \<Rightarrow> E e s | Inr r \<Rightarrow> Q r s\<rbrace>; P s; nf'\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s'. (s, s') \<in> sr \<and> P' s') f
 3. \<And>s rv sa. \<lbrakk>\<And>P f Q E. \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. case r of Inl e \<Rightarrow> E e s | Inr r \<Rightarrow> Q r s\<rbrace>; P s; ?Q6 s rv sa\<rbrakk> \<Longrightarrow> (s, sa) \<in> sr \<and> (fr \<oplus> r) (Inr x) rv proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>\<And>P f Q E. \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. case r of Inl e \<Rightarrow> E e s | Inr r \<Rightarrow> Q r s\<rbrace>; P s\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s'. (s, s') \<in> sr \<and> P' s'\<rbrace> f \<lbrace>?Q9 s\<rbrace>, \<lbrace>?E9 s\<rbrace>
 2. \<And>s. \<lbrakk>\<And>P f Q E. \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. case r of Inl e \<Rightarrow> E e s | Inr r \<Rightarrow> Q r s\<rbrace>; P s; nf'\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s'. (s, s') \<in> sr \<and> P' s') f
 3. \<And>s rv sa. \<lbrakk>\<And>P f Q E. \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. case r of Inl e \<Rightarrow> E e s | Inr r \<Rightarrow> Q r s\<rbrace>; P s; case rv of Inl e \<Rightarrow> ?E9 s e sa | Inr r \<Rightarrow> ?Q9 s r sa\<rbrakk> \<Longrightarrow> (s, sa) \<in> sr \<and> (fr \<oplus> r) (Inr x) rv proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>\<And>P f Q E. \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. case r of Inl e \<Rightarrow> E e s | Inr r \<Rightarrow> Q r s\<rbrace>; P s\<rbrakk> \<Longrightarrow> P s
 2. \<And>s. \<lbrakk>\<And>P f Q E. \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. case r of Inl e \<Rightarrow> E e s | Inr r \<Rightarrow> Q r s\<rbrace>; P s; nf'\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s'. (s, s') \<in> sr \<and> P' s') f
 3. \<And>s rv sa. \<lbrakk>\<And>P f Q E. \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. case r of Inl e \<Rightarrow> E e s | Inr r \<Rightarrow> Q r s\<rbrace>; P s; case rv of Inl e \<Rightarrow> False | Inr ra \<Rightarrow> (s, sa) \<in> sr \<and> r x ra\<rbrakk> \<Longrightarrow> (s, sa) \<in> sr \<and> (fr \<oplus> r) (Inr x) rv proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<And>P f Q E. \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. case r of Inl e \<Rightarrow> E e s | Inr r \<Rightarrow> Q r s\<rbrace>; P s; nf'\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s'. (s, s') \<in> sr \<and> P' s') f
 2. \<And>s rv sa. \<lbrakk>\<And>P f Q E. \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. case r of Inl e \<Rightarrow> E e s | Inr r \<Rightarrow> Q r s\<rbrace>; P s; case rv of Inl e \<Rightarrow> False | Inr ra \<Rightarrow> (s, sa) \<in> sr \<and> r x ra\<rbrakk> \<Longrightarrow> (s, sa) \<in> sr \<and> (fr \<oplus> r) (Inr x) rv proof (prove)
goal (1 subgoal):
 1. \<And>s rv sa. \<lbrakk>\<And>P f Q E. \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. case r of Inl e \<Rightarrow> E e s | Inr r \<Rightarrow> Q r s\<rbrace>; P s; case rv of Inl e \<Rightarrow> False | Inr ra \<Rightarrow> (s, sa) \<in> sr \<and> r x ra\<rbrakk> \<Longrightarrow> (s, sa) \<in> sr \<and> (fr \<oplus> r) (Inr x) rv proof (prove)
goal:
No subgoals! proof (state)
this:
corres_underlying sr nf nf' (fr \<oplus> r) P P' (returnOk x) f

goal:
No subgoals!