theory Syscall_S

lemma bisim_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      "bisim (f' \<oplus> r) P P' m m'
     \<Longrightarrow> bisim (f \<oplus> r) P P' (t m) (t' m')" apply (simp add: injection_handler_def handleE'_def x y) apply (rule bisim_guard_imp) apply (erule bisim_split) apply (case_tac ra, clarsimp+)[1] apply (rule bisim_throwError) apply (simp add: z) apply clarsimp apply (rule bisim_return) apply wpsimp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bisim (f' \<oplus> r) P P' m m' \<Longrightarrow> bisim (f \<oplus> r) P P' (t m) (t' m') proof (prove)
goal (1 subgoal):
 1. bisim (f' \<oplus> r) P P' m m' \<Longrightarrow> bisim (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. bisim (f' \<oplus> r) P P' m m' \<Longrightarrow> bisim (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>bisim (f' \<oplus> r) P P' m m'; P s\<rbrakk> \<Longrightarrow> ?Q2 s
 3. \<And>s. \<lbrakk>bisim (f' \<oplus> r) P P' m m'; P' s\<rbrakk> \<Longrightarrow> ?Q'2 s proof (prove)
goal (5 subgoals):
 1. \<And>ra r'. (f' \<oplus> r) ra r' \<Longrightarrow> bisim (f \<oplus> r) (?Q6 ra) (?Q'6 r') (case ra of Inl e \<Rightarrow> throwError (fn e) | Inr v' \<Rightarrow> return (Inr v')) (case r' of Inl e \<Rightarrow> throwError (fn' e) | Inr v' \<Rightarrow> return (Inr v'))
 2. \<lbrace>?S6\<rbrace> m \<lbrace>?Q6\<rbrace>
 3. \<lbrace>?S'6\<rbrace> m' \<lbrace>?Q'6\<rbrace>
 4. \<And>s. \<lbrakk>bisim (f' \<oplus> r) P P' m m'; P s\<rbrakk> \<Longrightarrow> (P and ?S6) s
 5. \<And>s. \<lbrakk>bisim (f' \<oplus> r) P P' m m'; P' s\<rbrakk> \<Longrightarrow> (P' and ?S'6) s proof (prove)
goal (6 subgoals):
 1. \<And>a y'. f' a y' \<Longrightarrow> bisim (f \<oplus> r) (?Q6 (Inl a)) (?Q'6 (Inl y')) (throwError (fn a)) (throwError (fn' y'))
 2. \<And>ra r' b. \<lbrakk>(f' \<oplus> r) ra r'; ra = Inr b\<rbrakk> \<Longrightarrow> bisim (f \<oplus> r) (?Q6 ra) (?Q'6 r') (case ra of Inl e \<Rightarrow> throwError (fn e) | Inr v' \<Rightarrow> return (Inr v')) (case r' of Inl e \<Rightarrow> throwError (fn' e) | Inr v' \<Rightarrow> return (Inr v'))
 3. \<lbrace>?S6\<rbrace> m \<lbrace>?Q6\<rbrace>
 4. \<lbrace>?S'6\<rbrace> m' \<lbrace>?Q'6\<rbrace>
 5. \<And>s. \<lbrakk>bisim (f' \<oplus> r) P P' m m'; P s\<rbrakk> \<Longrightarrow> (P and ?S6) s
 6. \<And>s. \<lbrakk>bisim (f' \<oplus> r) P P' m m'; P' s\<rbrakk> \<Longrightarrow> (P' and ?S'6) s proof (prove)
goal (6 subgoals):
 1. \<And>a y'. f' a y' \<Longrightarrow> f (fn a) (fn' y')
 2. \<And>ra r' b. \<lbrakk>(f' \<oplus> r) ra r'; ra = Inr b\<rbrakk> \<Longrightarrow> bisim (f \<oplus> r) (\<lambda>a. True) (\<lambda>a. True) (case ra of Inl e \<Rightarrow> throwError (fn e) | Inr v' \<Rightarrow> return (Inr v')) (case r' of Inl e \<Rightarrow> throwError (fn' e) | Inr v' \<Rightarrow> return (Inr v'))
 3. \<lbrace>?S6\<rbrace> m \<lbrace>\<lambda>a b. True\<rbrace>
 4. \<lbrace>?S'6\<rbrace> m' \<lbrace>\<lambda>a b. True\<rbrace>
 5. \<And>s. \<lbrakk>bisim (f' \<oplus> r) P P' m m'; P s\<rbrakk> \<Longrightarrow> (P and ?S6) s
 6. \<And>s. \<lbrakk>bisim (f' \<oplus> r) P P' m m'; P' s\<rbrakk> \<Longrightarrow> (P' and ?S'6) s proof (prove)
goal (5 subgoals):
 1. \<And>ra r' b. \<lbrakk>(f' \<oplus> r) ra r'; ra = Inr b\<rbrakk> \<Longrightarrow> bisim (f \<oplus> r) (\<lambda>a. True) (\<lambda>a. True) (case ra of Inl e \<Rightarrow> throwError (fn e) | Inr v' \<Rightarrow> return (Inr v')) (case r' of Inl e \<Rightarrow> throwError (fn' e) | Inr v' \<Rightarrow> return (Inr v'))
 2. \<lbrace>?S6\<rbrace> m \<lbrace>\<lambda>a b. True\<rbrace>
 3. \<lbrace>?S'6\<rbrace> m' \<lbrace>\<lambda>a b. True\<rbrace>
 4. \<And>s. \<lbrakk>bisim (f' \<oplus> r) P P' m m'; P s\<rbrakk> \<Longrightarrow> (P and ?S6) s
 5. \<And>s. \<lbrakk>bisim (f' \<oplus> r) P P' m m'; P' s\<rbrakk> \<Longrightarrow> (P' and ?S'6) s proof (prove)
goal (5 subgoals):
 1. \<And>b y'. r b y' \<Longrightarrow> bisim (f \<oplus> r) (\<lambda>a. True) (\<lambda>a. True) (return (Inr b)) (return (Inr y'))
 2. \<lbrace>?S6\<rbrace> m \<lbrace>\<lambda>a b. True\<rbrace>
 3. \<lbrace>?S'6\<rbrace> m' \<lbrace>\<lambda>a b. True\<rbrace>
 4. \<And>s. \<lbrakk>bisim (f' \<oplus> r) P P' m m'; P s\<rbrakk> \<Longrightarrow> (P and ?S6) s
 5. \<And>s. \<lbrakk>bisim (f' \<oplus> r) P P' m m'; P' s\<rbrakk> \<Longrightarrow> (P' and ?S'6) s proof (prove)
goal (5 subgoals):
 1. \<And>b y'. r b y' \<Longrightarrow> (f \<oplus> r) (Inr b) (Inr y')
 2. \<lbrace>?S6\<rbrace> m \<lbrace>\<lambda>a b. True\<rbrace>
 3. \<lbrace>?S'6\<rbrace> m' \<lbrace>\<lambda>a b. True\<rbrace>
 4. \<And>s. \<lbrakk>bisim (f' \<oplus> r) P P' m m'; P s\<rbrakk> \<Longrightarrow> (P and ?S6) s
 5. \<And>s. \<lbrakk>bisim (f' \<oplus> r) P P' m m'; P' s\<rbrakk> \<Longrightarrow> (P' and ?S'6) s proof (prove)
goal:
No subgoals!