theory Syscall_S

lemma bisim_split_catch_req:
  assumes bm: "bisim ((=) \<oplus> (=)) Pn Pn' m m'"
  and     bc: "\<And>x. bisim (=) (Pf x) (Pf' x) (c x) (c' x)"
  and     v1: "\<lbrace>P\<rbrace> m \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>r. Pf r and Pf' r\<rbrace>"
  shows "bisim (=) (Pn and P) Pn' (m <catch> c) (m' <catch> c')" unfolding catch_def apply (rule bisim_split_req [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"]) apply (rule bm [simplified rel_sum_comb_eq]) apply (case_tac r) apply clarsimp apply (rule bc) apply clarsimp apply (rule bisim_return') apply simp apply (rule hoare_post_imp [OF _ v1 [unfolded validE_def]]) apply (clarsimp split: sum.split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bisim (=) (Pn and P) Pn' (m <catch> c) (m' <catch> c') proof (prove)
goal (1 subgoal):
 1. bisim (=) (Pn and P) Pn' (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. bisim (=) Pn Pn' m m'
 2. \<And>r. bisim (=) (\<lambda>s. case r 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 r 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>r. (\<lambda>s. case r of Inl l \<Rightarrow> Pf l s | Inr uu_ \<Rightarrow> True) and (\<lambda>s. case r of Inl l \<Rightarrow> Pf' l s | Inr uu_ \<Rightarrow> True)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>r. bisim (=) (\<lambda>s. case r 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 r 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>r. (\<lambda>s. case r of Inl l \<Rightarrow> Pf l s | Inr uu_ \<Rightarrow> True) and (\<lambda>s. case r of Inl l \<Rightarrow> Pf' l s | Inr uu_ \<Rightarrow> True)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>r a. r = Inl a \<Longrightarrow> bisim (=) (\<lambda>s. case r 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 r 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>r b. r = Inr b \<Longrightarrow> bisim (=) (\<lambda>s. case r 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 r 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>r. (\<lambda>s. case r of Inl l \<Rightarrow> Pf l s | Inr uu_ \<Rightarrow> True) and (\<lambda>s. case r of Inl l \<Rightarrow> Pf' l s | Inr uu_ \<Rightarrow> True)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>a. bisim (=) (Pf a) (Pf' a) (c a) (c' a)
 2. \<And>r b. r = Inr b \<Longrightarrow> bisim (=) (\<lambda>s. case r 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 r 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>r. (\<lambda>s. case r of Inl l \<Rightarrow> Pf l s | Inr uu_ \<Rightarrow> True) and (\<lambda>s. case r of Inl l \<Rightarrow> Pf' l s | Inr uu_ \<Rightarrow> True)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>r b. r = Inr b \<Longrightarrow> bisim (=) (\<lambda>s. case r 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 r 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>r. (\<lambda>s. case r of Inl l \<Rightarrow> Pf l s | Inr uu_ \<Rightarrow> True) and (\<lambda>s. case r of Inl l \<Rightarrow> Pf' l s | Inr uu_ \<Rightarrow> True)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>b. bisim (=) (\<lambda>s. True) (\<lambda>s. True) (return b) (return b)
 2. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>r. (\<lambda>s. case r of Inl l \<Rightarrow> Pf l s | Inr uu_ \<Rightarrow> True) and (\<lambda>s. case r of Inl l \<Rightarrow> Pf' l s | Inr uu_ \<Rightarrow> True)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>b. b = b
 2. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>r. (\<lambda>s. case r of Inl l \<Rightarrow> Pf l s | Inr uu_ \<Rightarrow> True) and (\<lambda>s. case r of Inl l \<Rightarrow> Pf' l s | Inr uu_ \<Rightarrow> True)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> m \<lbrace>\<lambda>r. (\<lambda>s. case r of Inl l \<Rightarrow> Pf l s | Inr uu_ \<Rightarrow> True) and (\<lambda>s. case r of Inl l \<Rightarrow> Pf' l s | Inr uu_ \<Rightarrow> True)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>rv s. case rv of Inl e \<Rightarrow> (Pf e and Pf' e) s | Inr r \<Rightarrow> True \<Longrightarrow> ((\<lambda>s. case rv of Inl l \<Rightarrow> Pf l s | Inr uu_ \<Rightarrow> True) and (\<lambda>s. case rv of Inl l \<Rightarrow> Pf' l s | Inr uu_ \<Rightarrow> True)) s proof (prove)
goal:
No subgoals!