theory Bits_R

lemma corres_injection:
  assumes x: "t = injection_handler fn"
  assumes y: "t' = injection_handler fn'"
  assumes z: "\<And>ft ft'. f' ft ft' \<Longrightarrow> f (fn ft) (fn' ft')"
  shows      "corres (f' \<oplus> r) P P' m m'
     \<Longrightarrow> corres (f \<oplus> r) P P' (t m) (t' m')" apply (simp add: injection_handler_def handleE'_def x y) apply (rule corres_guard_imp) apply (rule corres_split) apply assumption apply (case_tac v, (clarsimp simp: z)+) apply (rule wp_post_taut) apply (rule wp_post_taut) apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (f' \<oplus> r) P P' m m' \<Longrightarrow> corres (f \<oplus> r) P P' (t m) (t' m') proof (prove)
goal (1 subgoal):
 1. corres (f' \<oplus> r) P P' m m' \<Longrightarrow> corres (f \<oplus> r) P P' (do v <- m;
case v of Inl e \<Rightarrow> throwError (fn e) | Inr v' \<Rightarrow> return (Inr v')
od) (do v <- m';
case v of Inl e \<Rightarrow> throwError (fn' e) | Inr v' \<Rightarrow> return (Inr v')
od) proof (prove)
goal (3 subgoals):
 1. corres (f' \<oplus> r) P P' m m' \<Longrightarrow> corres (f \<oplus> r) ?Q2 ?Q'2 (do v <- m;
case v of Inl e \<Rightarrow> throwError (fn e) | Inr v' \<Rightarrow> return (Inr v')
od) (do v <- m';
case v of Inl e \<Rightarrow> throwError (fn' e) | Inr v' \<Rightarrow> return (Inr v')
od)
 2. \<And>s. \<lbrakk>corres (f' \<oplus> r) P P' m m'; P s\<rbrakk> \<Longrightarrow> ?Q2 s
 3. \<And>s. \<lbrakk>corres (f' \<oplus> r) P P' m m'; P' s\<rbrakk> \<Longrightarrow> ?Q'2 s proof (prove)
goal (6 subgoals):
 1. corres (f' \<oplus> r) P P' m m' \<Longrightarrow> corres ?r'6 ?P6 ?P'6 m m'
 2. \<And>v va. \<lbrakk>corres (f' \<oplus> r) P P' m m'; ?r'6 v va\<rbrakk> \<Longrightarrow> corres (f \<oplus> r) (?R6 v) (?R'6 va) (case v of Inl e \<Rightarrow> throwError (fn e) | Inr v' \<Rightarrow> return (Inr v')) (case va of Inl e \<Rightarrow> throwError (fn' e) | Inr v' \<Rightarrow> return (Inr v'))
 3. corres (f' \<oplus> r) P P' m m' \<Longrightarrow> \<lbrace>?Q6\<rbrace> m \<lbrace>?R6\<rbrace>
 4. corres (f' \<oplus> r) P P' m m' \<Longrightarrow> \<lbrace>?Q'6\<rbrace> m' \<lbrace>?R'6\<rbrace>
 5. \<And>s. \<lbrakk>corres (f' \<oplus> r) P P' m m'; P s\<rbrakk> \<Longrightarrow> (?P6 and ?Q6) s
 6. \<And>s. \<lbrakk>corres (f' \<oplus> r) P P' m m'; P' s\<rbrakk> \<Longrightarrow> (?P'6 and ?Q'6) s proof (prove)
goal (5 subgoals):
 1. \<And>v va. \<lbrakk>corres (f' \<oplus> r) P P' m m'; (f' \<oplus> r) v va\<rbrakk> \<Longrightarrow> corres (f \<oplus> r) (?R6 v) (?R'6 va) (case v of Inl e \<Rightarrow> throwError (fn e) | Inr v' \<Rightarrow> return (Inr v')) (case va of Inl e \<Rightarrow> throwError (fn' e) | Inr v' \<Rightarrow> return (Inr v'))
 2. corres (f' \<oplus> r) P P' m m' \<Longrightarrow> \<lbrace>?Q6\<rbrace> m \<lbrace>?R6\<rbrace>
 3. corres (f' \<oplus> r) P P' m m' \<Longrightarrow> \<lbrace>?Q'6\<rbrace> m' \<lbrace>?R'6\<rbrace>
 4. \<And>s. \<lbrakk>corres (f' \<oplus> r) P P' m m'; P s\<rbrakk> \<Longrightarrow> (P and ?Q6) s
 5. \<And>s. \<lbrakk>corres (f' \<oplus> r) P P' m m'; P' s\<rbrakk> \<Longrightarrow> (P' and ?Q'6) s proof (prove)
goal (4 subgoals):
 1. corres (f' \<oplus> r) P P' m m' \<Longrightarrow> \<lbrace>?Q6\<rbrace> m \<lbrace>?R6\<rbrace>
 2. corres (f' \<oplus> r) P P' m m' \<Longrightarrow> \<lbrace>?Q'6\<rbrace> m' \<lbrace>?R'6\<rbrace>
 3. \<And>s. \<lbrakk>corres (f' \<oplus> r) P P' m m'; P s\<rbrakk> \<Longrightarrow> (P and ?Q6) s
 4. \<And>s. \<lbrakk>corres (f' \<oplus> r) P P' m m'; P' s\<rbrakk> \<Longrightarrow> (P' and ?Q'6) s proof (prove)
goal (3 subgoals):
 1. corres (f' \<oplus> r) P P' m m' \<Longrightarrow> \<lbrace>?Q'6\<rbrace> m' \<lbrace>?R'6\<rbrace>
 2. \<And>s. \<lbrakk>corres (f' \<oplus> r) P P' m m'; P s\<rbrakk> \<Longrightarrow> (P and (\<lambda>_. True)) s
 3. \<And>s. \<lbrakk>corres (f' \<oplus> r) P P' m m'; P' s\<rbrakk> \<Longrightarrow> (P' and ?Q'6) s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>corres (f' \<oplus> r) P P' m m'; P s\<rbrakk> \<Longrightarrow> (P and (\<lambda>_. True)) s
 2. \<And>s. \<lbrakk>corres (f' \<oplus> r) P P' m m'; P' s\<rbrakk> \<Longrightarrow> (P' and (\<lambda>_. True)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>corres (f' \<oplus> r) P P' m m'; P' s\<rbrakk> \<Longrightarrow> (P' and (\<lambda>_. True)) s proof (prove)
goal:
No subgoals!