theory Corres_UL

lemma corres_split_handle:
  assumes    "corres_underlying sr nf nf' (f' \<oplus> r) P P' a c"
  assumes y: "\<And>ft ft'. f' ft ft'
              \<Longrightarrow> corres_underlying sr nf nf' (f \<oplus> r) (E ft) (E' ft') (b ft) (d ft')"
  assumes x: "\<lbrace>Q\<rbrace> a \<lbrace>\<top>\<top>\<rbrace>,\<lbrace>E\<rbrace>" "\<lbrace>Q'\<rbrace> c \<lbrace>\<top>\<top>\<rbrace>,\<lbrace>E'\<rbrace>"
  shows      "corres_underlying sr nf nf' (f \<oplus> r) (P and Q) (P' and Q') (a <handle> (\<lambda>ft. b ft)) (c <handle> (\<lambda>ft'. d ft'))" using assms apply (simp add: handleE_def handleE'_def validE_def) apply (erule corres_split) defer apply assumption+ apply (case_tac v, simp_all, safe, simp_all add: y) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' (f \<oplus> r) (P and Q) (P' and Q') (a <handle> b) (c <handle> d) proof (prove)
using this:
corres_underlying sr nf nf' (f' \<oplus> r) P P' a c
f' ?ft ?ft' \<Longrightarrow> corres_underlying sr nf nf' (f \<oplus> r) (E ?ft) (E' ?ft') (b ?ft) (d ?ft')
\<lbrace>Q\<rbrace> a \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>E\<rbrace>
\<lbrace>Q'\<rbrace> c \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>E'\<rbrace>

goal (1 subgoal):
 1. corres_underlying sr nf nf' (f \<oplus> r) (P and Q) (P' and Q') (a <handle> b) (c <handle> d) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>corres_underlying sr nf nf' (f' \<oplus> r) P P' a c; \<And>ft ft'. f' ft ft' \<Longrightarrow> corres_underlying sr nf nf' (f \<oplus> r) (E ft) (E' ft') (b ft) (d ft'); \<lbrace>Q\<rbrace> a \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> E e s | Inr r \<Rightarrow> True\<rbrace>; \<lbrace>Q'\<rbrace> c \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> E' e s | Inr r \<Rightarrow> True\<rbrace>\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' (f \<oplus> r) (P and Q) (P' and Q') (do v <- a;
case v of Inl e \<Rightarrow> b e | Inr v' \<Rightarrow> return (Inr v')
od) (do v <- c;
case v of Inl e \<Rightarrow> d e | Inr v' \<Rightarrow> return (Inr v')
od) proof (prove)
goal (3 subgoals):
 1. \<And>v va. \<lbrakk>\<And>ft ft'. f' ft ft' \<Longrightarrow> corres_underlying sr nf nf' (f \<oplus> r) (E ft) (E' ft') (b ft) (d ft'); \<lbrace>Q\<rbrace> a \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> E e s | Inr r \<Rightarrow> True\<rbrace>; \<lbrace>Q'\<rbrace> c \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> E' e s | Inr r \<Rightarrow> True\<rbrace>; (f' \<oplus> r) v va\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' (f \<oplus> r) (?R5 v) (?R'5 va) (case v of Inl e \<Rightarrow> b e | Inr v' \<Rightarrow> return (Inr v')) (case va of Inl e \<Rightarrow> d e | Inr v' \<Rightarrow> return (Inr v'))
 2. \<lbrakk>\<And>ft ft'. f' ft ft' \<Longrightarrow> corres_underlying sr nf nf' (f \<oplus> r) (E ft) (E' ft') (b ft) (d ft'); \<lbrace>Q\<rbrace> a \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> E e s | Inr r \<Rightarrow> True\<rbrace>; \<lbrace>Q'\<rbrace> c \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> E' e s | Inr r \<Rightarrow> True\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>Q\<rbrace> a \<lbrace>?R5\<rbrace>
 3. \<lbrakk>\<And>ft ft'. f' ft ft' \<Longrightarrow> corres_underlying sr nf nf' (f \<oplus> r) (E ft) (E' ft') (b ft) (d ft'); \<lbrace>Q\<rbrace> a \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> E e s | Inr r \<Rightarrow> True\<rbrace>; \<lbrace>Q'\<rbrace> c \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> E' e s | Inr r \<Rightarrow> True\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>Q'\<rbrace> c \<lbrace>?R'5\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<And>ft ft'. f' ft ft' \<Longrightarrow> corres_underlying sr nf nf' (f \<oplus> r) (E ft) (E' ft') (b ft) (d ft'); \<lbrace>Q\<rbrace> a \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> E e s | Inr r \<Rightarrow> True\<rbrace>; \<lbrace>Q'\<rbrace> c \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> E' e s | Inr r \<Rightarrow> True\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>Q\<rbrace> a \<lbrace>?R5\<rbrace>
 2. \<lbrakk>\<And>ft ft'. f' ft ft' \<Longrightarrow> corres_underlying sr nf nf' (f \<oplus> r) (E ft) (E' ft') (b ft) (d ft'); \<lbrace>Q\<rbrace> a \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> E e s | Inr r \<Rightarrow> True\<rbrace>; \<lbrace>Q'\<rbrace> c \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> E' e s | Inr r \<Rightarrow> True\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>Q'\<rbrace> c \<lbrace>?R'5\<rbrace>
 3. \<And>v va. \<lbrakk>\<And>ft ft'. f' ft ft' \<Longrightarrow> corres_underlying sr nf nf' (f \<oplus> r) (E ft) (E' ft') (b ft) (d ft'); \<lbrace>Q\<rbrace> a \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> E e s | Inr r \<Rightarrow> True\<rbrace>; \<lbrace>Q'\<rbrace> c \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> E' e s | Inr r \<Rightarrow> True\<rbrace>; (f' \<oplus> r) v va\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' (f \<oplus> r) (?R5 v) (?R'5 va) (case v of Inl e \<Rightarrow> b e | Inr v' \<Rightarrow> return (Inr v')) (case va of Inl e \<Rightarrow> d e | Inr v' \<Rightarrow> return (Inr v')) proof (prove)
goal (1 subgoal):
 1. \<And>v va. \<lbrakk>\<And>ft ft'. f' ft ft' \<Longrightarrow> corres_underlying sr nf nf' (f \<oplus> r) (E ft) (E' ft') (b ft) (d ft'); \<lbrace>Q\<rbrace> a \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> E e s | Inr r \<Rightarrow> True\<rbrace>; \<lbrace>Q'\<rbrace> c \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> E' e s | Inr r \<Rightarrow> True\<rbrace>; (f' \<oplus> r) v va\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' (f \<oplus> r) (\<lambda>s. case v of Inl e \<Rightarrow> E e s | Inr r \<Rightarrow> True) (\<lambda>s. case va of Inl e \<Rightarrow> E' e s | Inr r \<Rightarrow> True) (case v of Inl e \<Rightarrow> b e | Inr v' \<Rightarrow> return (Inr v')) (case va of Inl e \<Rightarrow> d e | Inr v' \<Rightarrow> return (Inr v')) proof (prove)
goal:
No subgoals!