theory Bisim_UL

lemma bisim_split_handle:
  assumes bm: "bisim (f' \<oplus> r) Pn Pn' m m'"
  and     bc: "\<And>x x'. f' x x' \<Longrightarrow> bisim (f \<oplus> r) (Pf x) (Pf' x') (c x) (c' x')"
  and     v1: "\<lbrace>P\<rbrace> m \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>Pf\<rbrace>"
  and     v2: "\<lbrace>P'\<rbrace> m' \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>Pf'\<rbrace>"
  shows "bisim (f \<oplus> r) (Pn and P) (Pn' and P') (m <handle> c) (m' <handle> c')" unfolding handleE_def handleE'_def apply (rule bisim_split [where Q = "\<lambda>r s. case_sum (\<lambda>l. Pf l s) (\<lambda>_. True) r" and Q' = "\<lambda>r s. case_sum (\<lambda>l. Pf' l s) (\<lambda>_. True) r", OF bm, folded validE_def]) apply (case_tac ra) apply clarsimp apply (erule bc) apply clarsimp apply (rule bisim_return') apply simp apply (rule v1) apply (rule v2) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bisim (f \<oplus> r) (Pn and P) (Pn' and P') (m <handle> c) (m' <handle> c') proof (prove)
goal (1 subgoal):
 1. bisim (f \<oplus> r) (Pn and P) (Pn' and P') (do v <- m;
case v of Inl e \<Rightarrow> c e | Inr v' \<Rightarrow> return (Inr v')
od) (do v <- m';
case v of Inl e \<Rightarrow> c' e | Inr v' \<Rightarrow> return (Inr v')
od) proof (prove)
goal (3 subgoals):
 1. \<And>ra r'. (f' \<oplus> r) ra r' \<Longrightarrow> bisim (f \<oplus> r) (\<lambda>s. case ra of Inl l \<Rightarrow> Pf l s | Inr uu_ \<Rightarrow> True) (\<lambda>s. case r' of Inl l \<Rightarrow> Pf' l s | Inr uu_ \<Rightarrow> True) (case ra of Inl e \<Rightarrow> c e | Inr v' \<Rightarrow> return (Inr v')) (case r' of Inl e \<Rightarrow> c' e | Inr v' \<Rightarrow> return (Inr v'))
 2. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_ s. True\<rbrace>, \<lbrace>Pf\<rbrace>
 3. \<lbrace>P'\<rbrace> m' \<lbrace>\<lambda>_ s. True\<rbrace>, \<lbrace>Pf'\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>ra r' a. \<lbrakk>(f' \<oplus> r) ra r'; ra = Inl a\<rbrakk> \<Longrightarrow> bisim (f \<oplus> r) (\<lambda>s. case ra of Inl l \<Rightarrow> Pf l s | Inr uu_ \<Rightarrow> True) (\<lambda>s. case r' of Inl l \<Rightarrow> Pf' l s | Inr uu_ \<Rightarrow> True) (case ra of Inl e \<Rightarrow> c e | Inr v' \<Rightarrow> return (Inr v')) (case r' of Inl e \<Rightarrow> c' e | Inr v' \<Rightarrow> return (Inr v'))
 2. \<And>ra r' b. \<lbrakk>(f' \<oplus> r) ra r'; ra = Inr b\<rbrakk> \<Longrightarrow> bisim (f \<oplus> r) (\<lambda>s. case ra of Inl l \<Rightarrow> Pf l s | Inr uu_ \<Rightarrow> True) (\<lambda>s. case r' of Inl l \<Rightarrow> Pf' l s | Inr uu_ \<Rightarrow> True) (case ra of Inl e \<Rightarrow> c e | Inr v' \<Rightarrow> return (Inr v')) (case r' of Inl e \<Rightarrow> c' e | Inr v' \<Rightarrow> return (Inr v'))
 3. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_ s. True\<rbrace>, \<lbrace>Pf\<rbrace>
 4. \<lbrace>P'\<rbrace> m' \<lbrace>\<lambda>_ s. True\<rbrace>, \<lbrace>Pf'\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>a y'. f' a y' \<Longrightarrow> bisim (f \<oplus> r) (Pf a) (Pf' y') (c a) (c' y')
 2. \<And>ra r' b. \<lbrakk>(f' \<oplus> r) ra r'; ra = Inr b\<rbrakk> \<Longrightarrow> bisim (f \<oplus> r) (\<lambda>s. case ra of Inl l \<Rightarrow> Pf l s | Inr uu_ \<Rightarrow> True) (\<lambda>s. case r' of Inl l \<Rightarrow> Pf' l s | Inr uu_ \<Rightarrow> True) (case ra of Inl e \<Rightarrow> c e | Inr v' \<Rightarrow> return (Inr v')) (case r' of Inl e \<Rightarrow> c' e | Inr v' \<Rightarrow> return (Inr v'))
 3. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_ s. True\<rbrace>, \<lbrace>Pf\<rbrace>
 4. \<lbrace>P'\<rbrace> m' \<lbrace>\<lambda>_ s. True\<rbrace>, \<lbrace>Pf'\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>ra r' b. \<lbrakk>(f' \<oplus> r) ra r'; ra = Inr b\<rbrakk> \<Longrightarrow> bisim (f \<oplus> r) (\<lambda>s. case ra of Inl l \<Rightarrow> Pf l s | Inr uu_ \<Rightarrow> True) (\<lambda>s. case r' of Inl l \<Rightarrow> Pf' l s | Inr uu_ \<Rightarrow> True) (case ra of Inl e \<Rightarrow> c e | Inr v' \<Rightarrow> return (Inr v')) (case r' of Inl e \<Rightarrow> c' e | Inr v' \<Rightarrow> return (Inr v'))
 2. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_ s. True\<rbrace>, \<lbrace>Pf\<rbrace>
 3. \<lbrace>P'\<rbrace> m' \<lbrace>\<lambda>_ s. True\<rbrace>, \<lbrace>Pf'\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>b y'. r b y' \<Longrightarrow> bisim (f \<oplus> r) (\<lambda>s. True) (\<lambda>s. True) (return (Inr b)) (return (Inr y'))
 2. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_ s. True\<rbrace>, \<lbrace>Pf\<rbrace>
 3. \<lbrace>P'\<rbrace> m' \<lbrace>\<lambda>_ s. True\<rbrace>, \<lbrace>Pf'\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>b y'. r b y' \<Longrightarrow> (f \<oplus> r) (Inr b) (Inr y')
 2. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_ s. True\<rbrace>, \<lbrace>Pf\<rbrace>
 3. \<lbrace>P'\<rbrace> m' \<lbrace>\<lambda>_ s. True\<rbrace>, \<lbrace>Pf'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>_ s. True\<rbrace>, \<lbrace>Pf\<rbrace>
 2. \<lbrace>P'\<rbrace> m' \<lbrace>\<lambda>_ s. True\<rbrace>, \<lbrace>Pf'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P'\<rbrace> m' \<lbrace>\<lambda>_ s. True\<rbrace>, \<lbrace>Pf'\<rbrace> proof (prove)
goal:
No subgoals!