theory CSpace1_R

lemma pspace_relation_update_tcbs:
  "\<lbrakk> pspace_relation s s'; s x = Some (TCB otcb); s' x = Some (KOTCB otcb');
        tcb_relation tcb tcb' \<rbrakk>
       \<Longrightarrow> pspace_relation (s(x \<mapsto> TCB tcb)) (s'(x \<mapsto> KOTCB tcb'))" apply (simp add: pspace_relation_def pspace_dom_update
                   dom_fun_upd2
              del: dom_fun_upd) apply (erule conjE) apply (rule ballI, drule(1) bspec) apply (rule conjI, simp add: other_obj_relation_def) apply (clarsimp split: Structures_A.kernel_object.split_asm) apply (drule bspec, fastforce) apply clarsimp apply (erule(1) obj_relation_cutsE, simp_all split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pspace_relation s s'; s x = Some (TCB otcb); s' x = Some (KOTCB otcb'); tcb_relation tcb tcb'\<rbrakk> \<Longrightarrow> pspace_relation (s(x \<mapsto> TCB tcb)) (s'(x \<mapsto> KOTCB tcb')) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pspace_dom s = dom s' \<and> (\<forall>x\<in>dom s. \<forall>xa\<in>obj_relation_cuts (the (s x)) x. case xa of (y, P) \<Rightarrow> P (the (s x)) (the (s' y))); s x = Some (TCB otcb); s' x = Some (KOTCB otcb'); tcb_relation tcb tcb'\<rbrakk> \<Longrightarrow> \<forall>xa\<in>dom s. (xa = x \<longrightarrow> other_obj_relation (TCB tcb) (KOTCB tcb')) \<and> (xa \<noteq> x \<longrightarrow> (\<forall>xb\<in>obj_relation_cuts (the (s xa)) xa. case xb of (y, P) \<Rightarrow> P (the (s xa)) (the (if y = x then Some (KOTCB tcb') else s' y)))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s x = Some (TCB otcb); s' x = Some (KOTCB otcb'); tcb_relation tcb tcb'; pspace_dom s = dom s'; \<forall>x\<in>dom s. \<forall>xa\<in>obj_relation_cuts (the (s x)) x. case xa of (y, P) \<Rightarrow> P (the (s x)) (the (s' y))\<rbrakk> \<Longrightarrow> \<forall>xa\<in>dom s. (xa = x \<longrightarrow> other_obj_relation (TCB tcb) (KOTCB tcb')) \<and> (xa \<noteq> x \<longrightarrow> (\<forall>xb\<in>obj_relation_cuts (the (s xa)) xa. case xb of (y, P) \<Rightarrow> P (the (s xa)) (the (if y = x then Some (KOTCB tcb') else s' y)))) proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>s x = Some (TCB otcb); s' x = Some (KOTCB otcb'); tcb_relation tcb tcb'; pspace_dom s = dom s'; xa \<in> dom s; \<forall>x\<in>obj_relation_cuts (the (s xa)) xa. case x of (y, P) \<Rightarrow> P (the (s xa)) (the (s' y))\<rbrakk> \<Longrightarrow> (xa = x \<longrightarrow> other_obj_relation (TCB tcb) (KOTCB tcb')) \<and> (xa \<noteq> x \<longrightarrow> (\<forall>xb\<in>obj_relation_cuts (the (s xa)) xa. case xb of (y, P) \<Rightarrow> P (the (s xa)) (the (if y = x then Some (KOTCB tcb') else s' y)))) proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>s x = Some (TCB otcb); s' x = Some (KOTCB otcb'); tcb_relation tcb tcb'; pspace_dom s = dom s'; xa \<in> dom s; \<forall>x\<in>obj_relation_cuts (the (s xa)) xa. case x of (y, P) \<Rightarrow> P (the (s xa)) (the (s' y))\<rbrakk> \<Longrightarrow> xa \<noteq> x \<longrightarrow> (\<forall>xb\<in>obj_relation_cuts (the (s xa)) xa. case xb of (y, P) \<Rightarrow> P (the (s xa)) (the (if y = x then Some (KOTCB tcb') else s' y))) proof (prove)
goal (1 subgoal):
 1. \<And>xa y a b. \<lbrakk>s x = Some (TCB otcb); s' x = Some (KOTCB otcb'); tcb_relation tcb tcb'; pspace_dom s = dom s'; \<forall>x\<in>obj_relation_cuts y xa. case x of (ya, P) \<Rightarrow> P y (the (s' ya)); s xa = Some y; xa \<noteq> x; (a, b) \<in> obj_relation_cuts y xa\<rbrakk> \<Longrightarrow> (a = x \<longrightarrow> b y (KOTCB tcb')) \<and> (a \<noteq> x \<longrightarrow> b y (the (s' a))) proof (prove)
goal (1 subgoal):
 1. \<And>xa y a b. \<lbrakk>s x = Some (TCB otcb); s' x = Some (KOTCB otcb'); tcb_relation tcb tcb'; pspace_dom s = dom s'; s xa = Some y; xa \<noteq> x; (a, b) \<in> obj_relation_cuts y xa; case (a, b) of (ya, P) \<Rightarrow> P y (the (s' ya))\<rbrakk> \<Longrightarrow> (a = x \<longrightarrow> b y (KOTCB tcb')) \<and> (a \<noteq> x \<longrightarrow> b y (the (s' a))) proof (prove)
goal (1 subgoal):
 1. \<And>xa y b. \<lbrakk>s x = Some (TCB otcb); s' x = Some (KOTCB otcb'); tcb_relation tcb tcb'; pspace_dom s = dom s'; s xa = Some y; xa \<noteq> x; (x, b) \<in> obj_relation_cuts y xa; b y (KOTCB otcb')\<rbrakk> \<Longrightarrow> b y (KOTCB tcb') proof (prove)
goal:
No subgoals!