theory CSpace1_R

lemma updateMDB_ekheap_relation:
  assumes "(x, s'') \<in> fst (updateMDB p f s')"
  assumes "ekheap_relation (ekheap s) (ksPSpace s')"
  shows "ekheap_relation (ekheap s) (ksPSpace s'')" using assms apply (clarsimp simp: updateMDB_def Let_def setCTE_def setObject_def in_monad ekheap_relation_def etcb_relation_def split_def split: if_split_asm) apply (drule(1) updateObject_cte_is_tcb_or_cte[OF _ refl, rotated]) apply (drule_tac P="(=) s'" in use_valid [OF _ getCTE_sp], rule refl) apply (drule bspec, erule domI) apply (clarsimp simp: tcb_cte_cases_def lookupAround2_char1 split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ekheap_relation (ekheap s) (ksPSpace s'') proof (prove)
using this:
(x, s'') \<in> fst (updateMDB p f s')
ekheap_relation (ekheap s) (ksPSpace s')

goal (1 subgoal):
 1. ekheap_relation (ekheap s) (ksPSpace s'') proof (prove)
goal (1 subgoal):
 1. \<And>x s''a y cte a b s''aa obj'. \<lbrakk>\<forall>x\<in>dom (ekheap s). \<exists>tcb'. ksPSpace s' x = Some (KOTCB tcb') \<and> tcb_priority (the (ekheap s x)) = tcbPriority tcb' \<and> tcb_time_slice (the (ekheap s x)) = tcbTimeSlice tcb' \<and> tcb_domain (the (ekheap s x)) = tcbDomain tcb'; p \<noteq> 0; ekheap s x = Some y; (cte, s''a) \<in> fst (getCTE p s'); fst (lookupAround2 p (ksPSpace s''a)) = Some (a, b); (obj', s''aa) \<in> fst (updateObject (cteMDBNode_update (\<lambda>_. f (cteMDBNode cte)) cte) b p a (snd (lookupAround2 p (ksPSpace s''a))) s''a); s'' = s''aa\<lparr>ksPSpace := (ksPSpace s''a)(a \<mapsto> obj')\<rparr>\<rbrakk> \<Longrightarrow> (x = a \<longrightarrow> (\<exists>tcb'. obj' = KOTCB tcb' \<and> tcb_priority y = tcbPriority tcb' \<and> tcb_time_slice y = tcbTimeSlice tcb' \<and> tcb_domain y = tcbDomain tcb')) \<and> (x \<noteq> a \<longrightarrow> (\<exists>tcb'. ksPSpace s''a x = Some (KOTCB tcb') \<and> tcb_priority y = tcbPriority tcb' \<and> tcb_time_slice y = tcbTimeSlice tcb' \<and> tcb_domain y = tcbDomain tcb')) proof (prove)
goal (1 subgoal):
 1. \<And>x s''a y cte a b s''aa obj'. \<lbrakk>\<forall>x\<in>dom (ekheap s). \<exists>tcb'. ksPSpace s' x = Some (KOTCB tcb') \<and> tcb_priority (the (ekheap s x)) = tcbPriority tcb' \<and> tcb_time_slice (the (ekheap s x)) = tcbTimeSlice tcb' \<and> tcb_domain (the (ekheap s x)) = tcbDomain tcb'; p \<noteq> 0; ekheap s x = Some y; (cte, s''a) \<in> fst (getCTE p s'); fst (lookupAround2 p (ksPSpace s''a)) = Some (a, b); s'' = s''aa\<lparr>ksPSpace := (ksPSpace s''a)(a \<mapsto> obj')\<rparr>; (\<exists>tcb getF setF. b = KOTCB tcb \<and> s''aa = s''a \<and> tcb_cte_cases (p - a) = Some (getF, setF) \<and> obj' = KOTCB (setF (\<lambda>x. cteMDBNode_update (\<lambda>_. f (cteMDBNode cte)) cte) tcb) \<and> is_aligned a tcbBlockSizeBits \<and> ps_clear a tcbBlockSizeBits s''a) \<or> (\<exists>cte'. b = KOCTE cte' \<and> obj' = KOCTE (cteMDBNode_update (\<lambda>_. f (cteMDBNode cte)) cte) \<and> s''aa = s''a \<and> p = a \<and> is_aligned p cte_level_bits \<and> ps_clear p cte_level_bits s''a)\<rbrakk> \<Longrightarrow> (x = a \<longrightarrow> (\<exists>tcb'. obj' = KOTCB tcb' \<and> tcb_priority y = tcbPriority tcb' \<and> tcb_time_slice y = tcbTimeSlice tcb' \<and> tcb_domain y = tcbDomain tcb')) \<and> (x \<noteq> a \<longrightarrow> (\<exists>tcb'. ksPSpace s''a x = Some (KOTCB tcb') \<and> tcb_priority y = tcbPriority tcb' \<and> tcb_time_slice y = tcbTimeSlice tcb' \<and> tcb_domain y = tcbDomain tcb')) proof (prove)
goal (1 subgoal):
 1. \<And>x s''a y cte a b s''aa obj'. \<lbrakk>\<forall>x\<in>dom (ekheap s). \<exists>tcb'. ksPSpace s' x = Some (KOTCB tcb') \<and> tcb_priority (the (ekheap s x)) = tcbPriority tcb' \<and> tcb_time_slice (the (ekheap s x)) = tcbTimeSlice tcb' \<and> tcb_domain (the (ekheap s x)) = tcbDomain tcb'; p \<noteq> 0; ekheap s x = Some y; fst (lookupAround2 p (ksPSpace s''a)) = Some (a, b); s'' = s''aa\<lparr>ksPSpace := (ksPSpace s''a)(a \<mapsto> obj')\<rparr>; (\<exists>tcb getF setF. b = KOTCB tcb \<and> s''aa = s''a \<and> tcb_cte_cases (p - a) = Some (getF, setF) \<and> obj' = KOTCB (setF (\<lambda>x. cteMDBNode_update (\<lambda>_. f (cteMDBNode cte)) cte) tcb) \<and> is_aligned a tcbBlockSizeBits \<and> ps_clear a tcbBlockSizeBits s''a) \<or> (\<exists>cte'. b = KOCTE cte' \<and> obj' = KOCTE (cteMDBNode_update (\<lambda>_. f (cteMDBNode cte)) cte) \<and> s''aa = s''a \<and> p = a \<and> is_aligned p cte_level_bits \<and> ps_clear p cte_level_bits s''a); (cte_wp_at' (\<lambda>c. c = cte) p and (=) s') s''a\<rbrakk> \<Longrightarrow> (x = a \<longrightarrow> (\<exists>tcb'. obj' = KOTCB tcb' \<and> tcb_priority y = tcbPriority tcb' \<and> tcb_time_slice y = tcbTimeSlice tcb' \<and> tcb_domain y = tcbDomain tcb')) \<and> (x \<noteq> a \<longrightarrow> (\<exists>tcb'. ksPSpace s''a x = Some (KOTCB tcb') \<and> tcb_priority y = tcbPriority tcb' \<and> tcb_time_slice y = tcbTimeSlice tcb' \<and> tcb_domain y = tcbDomain tcb')) proof (prove)
goal (1 subgoal):
 1. \<And>x s''a y cte a b s''aa obj'. \<lbrakk>p \<noteq> 0; ekheap s x = Some y; fst (lookupAround2 p (ksPSpace s''a)) = Some (a, b); s'' = s''aa\<lparr>ksPSpace := (ksPSpace s''a)(a \<mapsto> obj')\<rparr>; (\<exists>tcb getF setF. b = KOTCB tcb \<and> s''aa = s''a \<and> tcb_cte_cases (p - a) = Some (getF, setF) \<and> obj' = KOTCB (setF (\<lambda>x. cteMDBNode_update (\<lambda>_. f (cteMDBNode cte)) cte) tcb) \<and> is_aligned a tcbBlockSizeBits \<and> ps_clear a tcbBlockSizeBits s''a) \<or> (\<exists>cte'. b = KOCTE cte' \<and> obj' = KOCTE (cteMDBNode_update (\<lambda>_. f (cteMDBNode cte)) cte) \<and> s''aa = s''a \<and> p = a \<and> is_aligned p cte_level_bits \<and> ps_clear p cte_level_bits s''a); (cte_wp_at' (\<lambda>c. c = cte) p and (=) s') s''a; \<exists>tcb'. ksPSpace s' x = Some (KOTCB tcb') \<and> tcb_priority (the (ekheap s x)) = tcbPriority tcb' \<and> tcb_time_slice (the (ekheap s x)) = tcbTimeSlice tcb' \<and> tcb_domain (the (ekheap s x)) = tcbDomain tcb'\<rbrakk> \<Longrightarrow> (x = a \<longrightarrow> (\<exists>tcb'. obj' = KOTCB tcb' \<and> tcb_priority y = tcbPriority tcb' \<and> tcb_time_slice y = tcbTimeSlice tcb' \<and> tcb_domain y = tcbDomain tcb')) \<and> (x \<noteq> a \<longrightarrow> (\<exists>tcb'. ksPSpace s''a x = Some (KOTCB tcb') \<and> tcb_priority y = tcbPriority tcb' \<and> tcb_time_slice y = tcbTimeSlice tcb' \<and> tcb_domain y = tcbDomain tcb')) proof (prove)
goal:
No subgoals!