theory KHeap_DR

lemma dcorres_injection_handler_rhs:
  "dcorres (dc \<oplus> r) P P' f g
     \<Longrightarrow> dcorres (dc \<oplus> r) P P' f (injection_handler h g)" apply (clarsimp simp:injection_handler_def) apply (clarsimp simp:handleE'_def) apply (rule corres_dummy_return_l) apply (rule corres_guard_imp) apply (rule corres_split_forwards'[where Q'="\<lambda>a. \<top>" and Q = "\<lambda>a. \<top>"]) apply assumption apply wp+ apply (clarsimp simp:return_def) apply (case_tac v) apply (clarsimp simp:throwError_def return_def corres_underlying_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres (dc \<oplus> r) P P' f g \<Longrightarrow> dcorres (dc \<oplus> r) P P' f (injection_handler h g) proof (prove)
goal (1 subgoal):
 1. dcorres (dc \<oplus> r) P P' f g \<Longrightarrow> dcorres (dc \<oplus> r) P P' f (g <handle2> (\<lambda>ft. throwError (h ft))) proof (prove)
goal (1 subgoal):
 1. dcorres (dc \<oplus> r) P P' f g \<Longrightarrow> dcorres (dc \<oplus> r) P P' f (do v <- g;
case v of Inl e \<Rightarrow> throwError (h e) | Inr v' \<Rightarrow> return (Inr v')
od) proof (prove)
goal (1 subgoal):
 1. dcorres (dc \<oplus> r) P P' f g \<Longrightarrow> dcorres (dc \<oplus> r) P P' (f >>= return) (do v <- g;
case v of Inl e \<Rightarrow> throwError (h e) | Inr v' \<Rightarrow> return (Inr v')
od) proof (prove)
goal (3 subgoals):
 1. dcorres (dc \<oplus> r) P P' f g \<Longrightarrow> dcorres (dc \<oplus> r) ?Q4 ?Q'4 (f >>= return) (do v <- g;
case v of Inl e \<Rightarrow> throwError (h e) | Inr v' \<Rightarrow> return (Inr v')
od)
 2. \<And>s. \<lbrakk>dcorres (dc \<oplus> r) P P' f g; P s\<rbrakk> \<Longrightarrow> ?Q4 s
 3. \<And>s. \<lbrakk>dcorres (dc \<oplus> r) P P' f g; P' s\<rbrakk> \<Longrightarrow> ?Q'4 s proof (prove)
goal (6 subgoals):
 1. dcorres (dc \<oplus> r) P P' f g \<Longrightarrow> dcorres ?r'8 ?Q4 ?Q'4 f g
 2. dcorres (dc \<oplus> r) P P' f g \<Longrightarrow> \<lbrace>?Q4\<rbrace> f \<lbrace>\<lambda>a _. True\<rbrace>
 3. dcorres (dc \<oplus> r) P P' f g \<Longrightarrow> \<lbrace>?Q'4\<rbrace> g \<lbrace>\<lambda>a _. True\<rbrace>
 4. \<And>x v. \<lbrakk>dcorres (dc \<oplus> r) P P' f g; ?r'8 x v\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> r) (\<lambda>_. True) (\<lambda>_. True) (return x) (case v of Inl e \<Rightarrow> throwError (h e) | Inr v' \<Rightarrow> return (Inr v'))
 5. \<And>s. \<lbrakk>dcorres (dc \<oplus> r) P P' f g; P s\<rbrakk> \<Longrightarrow> ?Q4 s
 6. \<And>s. \<lbrakk>dcorres (dc \<oplus> r) P P' f g; P' s\<rbrakk> \<Longrightarrow> ?Q'4 s proof (prove)
goal (5 subgoals):
 1. dcorres (dc \<oplus> r) P P' f g \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>a _. True\<rbrace>
 2. dcorres (dc \<oplus> r) P P' f g \<Longrightarrow> \<lbrace>P'\<rbrace> g \<lbrace>\<lambda>a _. True\<rbrace>
 3. \<And>x v. \<lbrakk>dcorres (dc \<oplus> r) P P' f g; (dc \<oplus> r) x v\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> r) (\<lambda>_. True) (\<lambda>_. True) (return x) (case v of Inl e \<Rightarrow> throwError (h e) | Inr v' \<Rightarrow> return (Inr v'))
 4. \<And>s. \<lbrakk>dcorres (dc \<oplus> r) P P' f g; P s\<rbrakk> \<Longrightarrow> P s
 5. \<And>s. \<lbrakk>dcorres (dc \<oplus> r) P P' f g; P' s\<rbrakk> \<Longrightarrow> P' s proof (prove)
goal (3 subgoals):
 1. \<And>x v. \<lbrakk>dcorres (dc \<oplus> r) P P' f g; (dc \<oplus> r) x v\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> r) (\<lambda>_. True) (\<lambda>_. True) (return x) (case v of Inl e \<Rightarrow> throwError (h e) | Inr v' \<Rightarrow> return (Inr v'))
 2. \<And>s. \<lbrakk>dcorres (dc \<oplus> r) P P' f g; P s\<rbrakk> \<Longrightarrow> P s
 3. \<And>s. \<lbrakk>dcorres (dc \<oplus> r) P P' f g; P' s\<rbrakk> \<Longrightarrow> P' s proof (prove)
goal (3 subgoals):
 1. \<And>x v. \<lbrakk>dcorres (dc \<oplus> r) P P' f g; (dc \<oplus> r) x v\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> r) (\<lambda>_. True) (\<lambda>_. True) (\<lambda>s. ({(x, s)}, False)) (case v of Inl e \<Rightarrow> throwError (h e) | Inr v' \<Rightarrow> return (Inr v'))
 2. \<And>s. \<lbrakk>dcorres (dc \<oplus> r) P P' f g; P s\<rbrakk> \<Longrightarrow> P s
 3. \<And>s. \<lbrakk>dcorres (dc \<oplus> r) P P' f g; P' s\<rbrakk> \<Longrightarrow> P' s proof (prove)
goal (4 subgoals):
 1. \<And>x v a. \<lbrakk>dcorres (dc \<oplus> r) P P' f g; (dc \<oplus> r) x v; v = Inl a\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> r) (\<lambda>_. True) (\<lambda>_. True) (\<lambda>s. ({(x, s)}, False)) (case v of Inl e \<Rightarrow> throwError (h e) | Inr v' \<Rightarrow> return (Inr v'))
 2. \<And>x v b. \<lbrakk>dcorres (dc \<oplus> r) P P' f g; (dc \<oplus> r) x v; v = Inr b\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> r) (\<lambda>_. True) (\<lambda>_. True) (\<lambda>s. ({(x, s)}, False)) (case v of Inl e \<Rightarrow> throwError (h e) | Inr v' \<Rightarrow> return (Inr v'))
 3. \<And>s. \<lbrakk>dcorres (dc \<oplus> r) P P' f g; P s\<rbrakk> \<Longrightarrow> P s
 4. \<And>s. \<lbrakk>dcorres (dc \<oplus> r) P P' f g; P' s\<rbrakk> \<Longrightarrow> P' s proof (prove)
goal:
No subgoals!