theory SyscallArgs_C

lemma ccorres_nondet_refinement:
  "\<lbrakk> is_nondet_refinement a b;
       ccorres_underlying sr Gamm rvr xf arrel axf G G' hs a c \<rbrakk>
     \<Longrightarrow> ccorres_underlying sr Gamm rvr xf arrel axf G G' hs b c" apply (simp add: ccorres_underlying_def is_nondet_refinement_def
                   split_def) apply (rule ballI, drule(1) bspec) apply (intro impI) apply (drule mp, blast) apply (elim allEI) apply (clarsimp split: xstate.split_asm) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_nondet_refinement a b; ccorres_underlying sr Gamm rvr xf arrel axf G G' hs a c\<rbrakk> \<Longrightarrow> ccorres_underlying sr Gamm rvr xf arrel axf G G' hs b c proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>s. (snd (a s) \<longrightarrow> snd (b s)) \<and> fst (a s) \<subseteq> fst (b s); \<forall>x\<in>sr. G (fst x) \<and> snd x \<in> G' \<and> \<not> snd (a (fst x)) \<longrightarrow> (\<forall>n t. Gamm\<turnstile>\<^sub>h \<langle>c # hs,snd x\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (a (fst x)). (t, s'') \<in> sr \<and> unif_rrel (n = length hs) rvr xf arrel axf r s'' | _ \<Rightarrow> False))\<rbrakk> \<Longrightarrow> \<forall>x\<in>sr. G (fst x) \<and> snd x \<in> G' \<and> \<not> snd (b (fst x)) \<longrightarrow> (\<forall>n t. Gamm\<turnstile>\<^sub>h \<langle>c # hs,snd x\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (b (fst x)). (t, s'') \<in> sr \<and> unif_rrel (n = length hs) rvr xf arrel axf r s'' | _ \<Rightarrow> False)) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>s. (snd (a s) \<longrightarrow> snd (b s)) \<and> fst (a s) \<subseteq> fst (b s); x \<in> sr; G (fst x) \<and> snd x \<in> G' \<and> \<not> snd (a (fst x)) \<longrightarrow> (\<forall>n t. Gamm\<turnstile>\<^sub>h \<langle>c # hs,snd x\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (a (fst x)). (t, s'') \<in> sr \<and> unif_rrel (n = length hs) rvr xf arrel axf r s'' | _ \<Rightarrow> False))\<rbrakk> \<Longrightarrow> G (fst x) \<and> snd x \<in> G' \<and> \<not> snd (b (fst x)) \<longrightarrow> (\<forall>n t. Gamm\<turnstile>\<^sub>h \<langle>c # hs,snd x\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (b (fst x)). (t, s'') \<in> sr \<and> unif_rrel (n = length hs) rvr xf arrel axf r s'' | _ \<Rightarrow> False)) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>s. (snd (a s) \<longrightarrow> snd (b s)) \<and> fst (a s) \<subseteq> fst (b s); x \<in> sr; G (fst x) \<and> snd x \<in> G' \<and> \<not> snd (a (fst x)) \<longrightarrow> (\<forall>n t. Gamm\<turnstile>\<^sub>h \<langle>c # hs,snd x\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (a (fst x)). (t, s'') \<in> sr \<and> unif_rrel (n = length hs) rvr xf arrel axf r s'' | _ \<Rightarrow> False)); G (fst x) \<and> snd x \<in> G' \<and> \<not> snd (b (fst x))\<rbrakk> \<Longrightarrow> \<forall>n t. Gamm\<turnstile>\<^sub>h \<langle>c # hs,snd x\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (b (fst x)). (t, s'') \<in> sr \<and> unif_rrel (n = length hs) rvr xf arrel axf r s'' | _ \<Rightarrow> False) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>s. (snd (a s) \<longrightarrow> snd (b s)) \<and> fst (a s) \<subseteq> fst (b s); x \<in> sr; G (fst x) \<and> snd x \<in> G' \<and> \<not> snd (b (fst x)); \<forall>n t. Gamm\<turnstile>\<^sub>h \<langle>c # hs,snd x\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (a (fst x)). (t, s'') \<in> sr \<and> unif_rrel (n = length hs) rvr xf arrel axf r s'' | _ \<Rightarrow> False)\<rbrakk> \<Longrightarrow> \<forall>n t. Gamm\<turnstile>\<^sub>h \<langle>c # hs,snd x\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (b (fst x)). (t, s'') \<in> sr \<and> unif_rrel (n = length hs) rvr xf arrel axf r s'' | _ \<Rightarrow> False) proof (prove)
goal (1 subgoal):
 1. \<And>x n t. \<lbrakk>\<forall>s. (snd (a s) \<longrightarrow> snd (b s)) \<and> fst (a s) \<subseteq> fst (b s); x \<in> sr; G (fst x) \<and> snd x \<in> G' \<and> \<not> snd (b (fst x)); Gamm\<turnstile>\<^sub>h \<langle>c # hs,snd x\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (a (fst x)). (t, s'') \<in> sr \<and> unif_rrel (n = length hs) rvr xf arrel axf r s'' | _ \<Rightarrow> False)\<rbrakk> \<Longrightarrow> Gamm\<turnstile>\<^sub>h \<langle>c # hs,snd x\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (b (fst x)). (t, s'') \<in> sr \<and> unif_rrel (n = length hs) rvr xf arrel axf r s'' | _ \<Rightarrow> False) proof (prove)
goal (1 subgoal):
 1. \<And>aa ba n x1 aaa baa. \<lbrakk>\<forall>s. (snd (a s) \<longrightarrow> snd (b s)) \<and> fst (a s) \<subseteq> fst (b s); (aa, ba) \<in> sr; G aa; ba \<in> G'; \<not> snd (b aa); Gamm\<turnstile>\<^sub>h \<langle>c # hs,ba\<rangle> \<Rightarrow> (n, Normal x1); (aaa, baa) \<in> fst (a aa); (baa, x1) \<in> sr; unif_rrel (n = length hs) rvr xf arrel axf aaa x1\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (b aa). case x of (r, t) \<Rightarrow> (t, x1) \<in> sr \<and> unif_rrel (n = length hs) rvr xf arrel axf r x1 proof (prove)
goal:
No subgoals!