theory Ipc_C

lemma ccorres_case_sum_liftE:
  "ccorres r xf P P' hs H C \<Longrightarrow> ccorres (\<lambda>a c. case_sum (\<lambda>x. r' x c) (\<lambda>y. r y c) a) xf P P' hs (liftE H) C" apply (clarsimp simp: ccorres_underlying_def split: xstate.splits) apply (drule (1) bspec) apply (clarsimp simp: split_def liftE_def bind_def return_def) apply (fastforce simp: unif_rrel_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres r xf P P' hs H C \<Longrightarrow> ccorres (\<lambda>a c. case a of Inl x \<Rightarrow> r' x c | Inr y \<Rightarrow> r y c) xf P P' hs (liftE H) C proof (prove)
goal (1 subgoal):
 1. \<And>a b n t. \<lbrakk>\<forall>x\<in>rf_sr. case x of (s, s') \<Rightarrow> P s \<and> s' \<in> P' \<and> \<not> snd (H s) \<longrightarrow> (\<forall>n t. (\<Gamma>\<turnstile>\<^sub>h \<langle>C # hs,s'\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (\<forall>x1. t = Normal x1 \<longrightarrow> (\<exists>x\<in>fst (H s). case x of (ra, t) \<Rightarrow> (t, x1) \<in> rf_sr \<and> unif_rrel (n = length hs) r xf r xf ra x1))) \<and> ((\<forall>x2. t \<noteq> Abrupt x2) \<or> (s', C # hs, n, t) \<notin> exec_handlers \<Gamma>) \<and> ((\<forall>x3. t \<noteq> Fault x3) \<or> (s', C # hs, n, t) \<notin> exec_handlers \<Gamma>) \<and> (t = Stuck \<longrightarrow> (s', C # hs, n, Stuck) \<notin> exec_handlers \<Gamma>)); (a, b) \<in> rf_sr; P a; b \<in> P'; \<not> snd (liftE H a)\<rbrakk> \<Longrightarrow> (\<forall>x1. t = Normal x1 \<longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>C # hs,b\<rangle> \<Rightarrow> (n, Normal x1) \<longrightarrow> (\<exists>x\<in>fst (liftE H a). case x of (ra, t) \<Rightarrow> (t, x1) \<in> rf_sr \<and> unif_rrel (n = length hs) (\<lambda>a c. case a of Inl x \<Rightarrow> r' x c | Inr y \<Rightarrow> r y c) xf (\<lambda>a c. case a of Inl x \<Rightarrow> r' x c | Inr y \<Rightarrow> r y c) xf ra x1)) \<and> (\<forall>x2. t = Abrupt x2 \<longrightarrow> (b, C # hs, n, Abrupt x2) \<notin> exec_handlers \<Gamma>) \<and> (\<forall>x3. t = Fault x3 \<longrightarrow> (b, C # hs, n, Fault x3) \<notin> exec_handlers \<Gamma>) \<and> (t = Stuck \<longrightarrow> (b, C # hs, n, Stuck) \<notin> exec_handlers \<Gamma>) proof (prove)
goal (1 subgoal):
 1. \<And>a b n t. \<lbrakk>(a, b) \<in> rf_sr; P a; b \<in> P'; \<not> snd (liftE H a); case (a, b) of (s, s') \<Rightarrow> P s \<and> s' \<in> P' \<and> \<not> snd (H s) \<longrightarrow> (\<forall>n t. (\<Gamma>\<turnstile>\<^sub>h \<langle>C # hs,s'\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (\<forall>x1. t = Normal x1 \<longrightarrow> (\<exists>x\<in>fst (H s). case x of (ra, t) \<Rightarrow> (t, x1) \<in> rf_sr \<and> unif_rrel (n = length hs) r xf r xf ra x1))) \<and> ((\<forall>x2. t \<noteq> Abrupt x2) \<or> (s', C # hs, n, t) \<notin> exec_handlers \<Gamma>) \<and> ((\<forall>x3. t \<noteq> Fault x3) \<or> (s', C # hs, n, t) \<notin> exec_handlers \<Gamma>) \<and> (t = Stuck \<longrightarrow> (s', C # hs, n, Stuck) \<notin> exec_handlers \<Gamma>))\<rbrakk> \<Longrightarrow> (\<forall>x1. t = Normal x1 \<longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>C # hs,b\<rangle> \<Rightarrow> (n, Normal x1) \<longrightarrow> (\<exists>x\<in>fst (liftE H a). case x of (ra, t) \<Rightarrow> (t, x1) \<in> rf_sr \<and> unif_rrel (n = length hs) (\<lambda>a c. case a of Inl x \<Rightarrow> r' x c | Inr y \<Rightarrow> r y c) xf (\<lambda>a c. case a of Inl x \<Rightarrow> r' x c | Inr y \<Rightarrow> r y c) xf ra x1)) \<and> (\<forall>x2. t = Abrupt x2 \<longrightarrow> (b, C # hs, n, Abrupt x2) \<notin> exec_handlers \<Gamma>) \<and> (\<forall>x3. t = Fault x3 \<longrightarrow> (b, C # hs, n, Fault x3) \<notin> exec_handlers \<Gamma>) \<and> (t = Stuck \<longrightarrow> (b, C # hs, n, Stuck) \<notin> exec_handlers \<Gamma>) proof (prove)
goal (1 subgoal):
 1. \<And>a b n t. \<lbrakk>(a, b) \<in> rf_sr; P a; b \<in> P'; \<not> snd (H a); \<forall>n t. (\<Gamma>\<turnstile>\<^sub>h \<langle>C # hs,b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (\<forall>x1. t = Normal x1 \<longrightarrow> (\<exists>x\<in>fst (H a). (snd x, x1) \<in> rf_sr \<and> unif_rrel (n = length hs) r xf r xf (fst x) x1))) \<and> ((\<forall>x2. t \<noteq> Abrupt x2) \<or> (b, C # hs, n, t) \<notin> exec_handlers \<Gamma>) \<and> ((\<forall>x3. t \<noteq> Fault x3) \<or> (b, C # hs, n, t) \<notin> exec_handlers \<Gamma>) \<and> (t = Stuck \<longrightarrow> (b, C # hs, n, Stuck) \<notin> exec_handlers \<Gamma>)\<rbrakk> \<Longrightarrow> (\<forall>x1. t = Normal x1 \<longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>C # hs,b\<rangle> \<Rightarrow> (n, Normal x1) \<longrightarrow> (\<exists>y\<in>fst (H a). (snd y, x1) \<in> rf_sr \<and> unif_rrel (n = length hs) (\<lambda>a c. case a of Inl x \<Rightarrow> r' x c | Inr y \<Rightarrow> r y c) xf (\<lambda>a c. case a of Inl x \<Rightarrow> r' x c | Inr y \<Rightarrow> r y c) xf (Inr (fst y)) x1)) \<and> (\<forall>x2. t = Abrupt x2 \<longrightarrow> (b, C # hs, n, Abrupt x2) \<notin> exec_handlers \<Gamma>) \<and> (\<forall>x3. t = Fault x3 \<longrightarrow> (b, C # hs, n, Fault x3) \<notin> exec_handlers \<Gamma>) proof (prove)
goal:
No subgoals!