theory Ipc_C

lemma ccorres_add_getRegister:
  "ccorres rv xf P P' hs (asUser t (getRegister r) >>= (\<lambda>_. a)) c
    \<Longrightarrow> ccorres rv xf (P and tcb_at' t) P' hs a c" apply (simp add: asUser_getRegister_discarded) apply (simp add: ccorres_underlying_def) apply (elim ballEI | clarsimp del: allI)+ apply (drule mp) apply (simp add: stateAssert_def bind_assoc exec_get) apply (elim allEI) apply (clarsimp simp: in_monad stateAssert_def split: xstate.split_asm) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres rv xf P P' hs (do _ <- asUser t (getRegister r);
a
od) c \<Longrightarrow> ccorres rv xf (P and tcb_at' t) P' hs a c proof (prove)
goal (1 subgoal):
 1. ccorres rv xf P P' hs (do _ <- stateAssert (tcb_at' t) [];
a
od) c \<Longrightarrow> ccorres rv xf (P and tcb_at' t) P' hs a 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 ((do _ <- stateAssert (tcb_at' t) [];
a
od) s) \<longrightarrow> (\<forall>n ta. \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, ta) \<longrightarrow> (case ta of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst ((do _ <- stateAssert (tcb_at' t) [];
a
od) s). (t, s'') \<in> rf_sr \<and> unif_rrel (n = length hs) rv xf rv xf r s'' | _ \<Rightarrow> False)) \<Longrightarrow> \<forall>x\<in>rf_sr. case x of (s, s') \<Rightarrow> P s \<and> tcb_at' t s \<and> s' \<in> P' \<and> \<not> snd (a 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 (a s). (t, s'') \<in> rf_sr \<and> unif_rrel (n = length hs) rv xf rv xf r s'' | _ \<Rightarrow> False)) proof (prove)
goal (1 subgoal):
 1. \<And>aa b. \<lbrakk>(aa, b) \<in> rf_sr; \<not> snd ((do _ <- stateAssert (tcb_at' t) [];
a
od) aa) \<longrightarrow> (\<forall>n ta. \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,b\<rangle> \<Rightarrow> (n, ta) \<longrightarrow> (case ta of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst ((do _ <- stateAssert (tcb_at' t) [];
a
od) aa). (t, s'') \<in> rf_sr \<and> unif_rrel (n = length hs) rv xf rv xf r s'' | _ \<Rightarrow> False)); P aa; tcb_at' t aa; b \<in> P'; \<not> snd (a aa)\<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 (a aa). (t, s'') \<in> rf_sr \<and> unif_rrel (n = length hs) rv xf rv xf r s'' | _ \<Rightarrow> False) proof (prove)
goal (2 subgoals):
 1. \<And>aa b. \<lbrakk>(aa, b) \<in> rf_sr; P aa; tcb_at' t aa; b \<in> P'; \<not> snd (a aa)\<rbrakk> \<Longrightarrow> \<not> snd ((do _ <- stateAssert (tcb_at' t) [];
a
od) aa)
 2. \<And>aa b. \<lbrakk>(aa, b) \<in> rf_sr; P aa; tcb_at' t aa; b \<in> P'; \<not> snd (a aa); \<forall>n ta. \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,b\<rangle> \<Rightarrow> (n, ta) \<longrightarrow> (case ta of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst ((do _ <- stateAssert (tcb_at' t) [];
a
od) aa). (t, s'') \<in> rf_sr \<and> unif_rrel (n = length hs) rv xf rv xf r s'' | _ \<Rightarrow> False)\<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 (a aa). (t, s'') \<in> rf_sr \<and> unif_rrel (n = length hs) rv xf rv xf r s'' | _ \<Rightarrow> False) proof (prove)
goal (1 subgoal):
 1. \<And>aa b. \<lbrakk>(aa, b) \<in> rf_sr; P aa; tcb_at' t aa; b \<in> P'; \<not> snd (a aa); \<forall>n ta. \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,b\<rangle> \<Rightarrow> (n, ta) \<longrightarrow> (case ta of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst ((do _ <- stateAssert (tcb_at' t) [];
a
od) aa). (t, s'') \<in> rf_sr \<and> unif_rrel (n = length hs) rv xf rv xf r s'' | _ \<Rightarrow> False)\<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 (a aa). (t, s'') \<in> rf_sr \<and> unif_rrel (n = length hs) rv xf rv xf r s'' | _ \<Rightarrow> False) proof (prove)
goal (1 subgoal):
 1. \<And>aa b n ta. \<lbrakk>(aa, b) \<in> rf_sr; P aa; tcb_at' t aa; b \<in> P'; \<not> snd (a aa); \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,b\<rangle> \<Rightarrow> (n, ta) \<longrightarrow> (case ta of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst ((do _ <- stateAssert (tcb_at' t) [];
a
od) aa). (t, s'') \<in> rf_sr \<and> unif_rrel (n = length hs) rv xf rv xf r s'' | _ \<Rightarrow> False)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,b\<rangle> \<Rightarrow> (n, ta) \<longrightarrow> (case ta of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (a aa). (t, s'') \<in> rf_sr \<and> unif_rrel (n = length hs) rv xf rv xf r s'' | _ \<Rightarrow> False) proof (prove)
goal (1 subgoal):
 1. \<And>aa b n x1 aaa ba. \<lbrakk>(aa, b) \<in> rf_sr; P aa; tcb_at' t aa; b \<in> P'; \<not> snd (a aa); \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,b\<rangle> \<Rightarrow> (n, Normal x1); (aaa, ba) \<in> fst (a aa); (ba, x1) \<in> rf_sr; unif_rrel (n = length hs) rv xf rv xf aaa x1\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (a aa). case x of (r, t) \<Rightarrow> (t, x1) \<in> rf_sr \<and> unif_rrel (n = length hs) rv xf rv xf r x1 proof (prove)
goal:
No subgoals!