theory SyscallArgs_C

lemma ccorres_alternative2:
  "ccorres rvr xf P P' hs g c
     \<Longrightarrow> ccorres rvr xf P P' hs (f \<sqinter> g) c" apply (simp add: ccorres_underlying_def) apply (erule ballEI, clarsimp del: allI) apply (simp add: alternative_def) apply (elim allEI) apply (auto simp: alternative_def split: xstate.split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres rvr xf P P' hs g c \<Longrightarrow> ccorres rvr xf P P' hs (f \<sqinter> g) c proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>rf_sr. case x of (s, s') \<Rightarrow> P s \<and> s' \<in> P' \<and> \<not> snd (g s) \<longrightarrow> (\<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (g s). (t, s'') \<in> rf_sr \<and> unif_rrel (n = length hs) rvr xf rvr xf r s'' | _ \<Rightarrow> False)) \<Longrightarrow> \<forall>x\<in>rf_sr. case x of (s, s') \<Rightarrow> P s \<and> s' \<in> P' \<and> \<not> snd ((f \<sqinter> g) s) \<longrightarrow> (\<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst ((f \<sqinter> g) s). (t, s'') \<in> rf_sr \<and> unif_rrel (n = length hs) rvr xf rvr xf r s'' | _ \<Rightarrow> False)) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>(a, b) \<in> rf_sr; \<not> snd (g a) \<longrightarrow> (\<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (g a). (t, s'') \<in> rf_sr \<and> unif_rrel (n = length hs) rvr xf rvr xf r s'' | _ \<Rightarrow> False)); P a; b \<in> P'; \<not> snd ((f \<sqinter> g) a)\<rbrakk> \<Longrightarrow> \<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst ((f \<sqinter> g) a). (t, s'') \<in> rf_sr \<and> unif_rrel (n = length hs) rvr xf rvr xf r s'' | _ \<Rightarrow> False) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>(a, b) \<in> rf_sr; \<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (g a). (t, s'') \<in> rf_sr \<and> unif_rrel (n = length hs) rvr xf rvr xf r s'' | _ \<Rightarrow> False); P a; b \<in> P'; \<not> snd (f a) \<and> \<not> snd (g a)\<rbrakk> \<Longrightarrow> \<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst ((f \<sqinter> g) a). (t, s'') \<in> rf_sr \<and> unif_rrel (n = length hs) rvr xf rvr xf r s'' | _ \<Rightarrow> False) proof (prove)
goal (1 subgoal):
 1. \<And>a b n t. \<lbrakk>(a, b) \<in> rf_sr; P a; b \<in> P'; \<not> snd (f a) \<and> \<not> snd (g a); \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (g a). (t, s'') \<in> rf_sr \<and> unif_rrel (n = length hs) rvr xf rvr xf r s'' | _ \<Rightarrow> False)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst ((f \<sqinter> g) a). (t, s'') \<in> rf_sr \<and> unif_rrel (n = length hs) rvr xf rvr xf r s'' | _ \<Rightarrow> False) proof (prove)
goal:
No subgoals!