theory Syscall_S

lemma bisim_split_catch:
  assumes bm: "bisim (f' \<oplus> r) Pn Pn' m m'"
  and     bc: "\<And>x x'. f' x x' \<Longrightarrow> bisim 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 r (Pn and P) (Pn' and P') (m <catch> c) (m' <catch> c')" unfolding catch_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 r (Pn and P) (Pn' and P') (m <catch> c) (m' <catch> c') proof (prove)
goal (1 subgoal):
 1. bisim r (Pn and P) (Pn' and P') (do x <- m;
case x of Inl e \<Rightarrow> c e | Inr b \<Rightarrow> return b
od) (do x <- m';
case x of Inl e \<Rightarrow> c' e | Inr b \<Rightarrow> return b
od) proof (prove)
goal (3 subgoals):
 1. \<And>ra r'. (f' \<oplus> r) ra r' \<Longrightarrow> bisim 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 b \<Rightarrow> return b) (case r' of Inl e \<Rightarrow> c' e | Inr b \<Rightarrow> return b)
 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 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 b \<Rightarrow> return b) (case r' of Inl e \<Rightarrow> c' e | Inr b \<Rightarrow> return b)
 2. \<And>ra r' b. \<lbrakk>(f' \<oplus> r) ra r'; ra = Inr b\<rbrakk> \<Longrightarrow> bisim 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 b \<Rightarrow> return b) (case r' of Inl e \<Rightarrow> c' e | Inr b \<Rightarrow> return b)
 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 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 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 b \<Rightarrow> return b) (case r' of Inl e \<Rightarrow> c' e | Inr b \<Rightarrow> return b)
 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 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 b \<Rightarrow> return b) (case r' of Inl e \<Rightarrow> c' e | Inr b \<Rightarrow> return b)
 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 r (\<lambda>s. True) (\<lambda>s. True) (return b) (return 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> r b 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!