theory SR_lemmas_C

lemma map_to_ctes_upd_tcb_no_ctes:
  "\<lbrakk>ko_at' tcb thread s ; \<forall>x\<in>ran tcb_cte_cases. (\<lambda>(getF, setF). getF tcb' = getF tcb) x \<rbrakk>
  \<Longrightarrow> map_to_ctes ((ksPSpace s)(thread \<mapsto> KOTCB tcb')) = map_to_ctes (ksPSpace s)" apply (erule obj_atE') apply (simp add: projectKOs objBits_simps) apply (subst map_to_ctes_upd_tcb') apply assumption+ apply (rule ext) apply (clarsimp split: if_split) apply (drule (1) bspec [OF _ ranI]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ko_at' tcb thread s; \<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> getF tcb' = getF tcb\<rbrakk> \<Longrightarrow> map_to_ctes ((ksPSpace s)(thread \<mapsto> KOTCB tcb')) = ctes_of s proof (prove)
goal (1 subgoal):
 1. \<And>ko obj. \<lbrakk>\<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> getF tcb' = getF tcb; ksPSpace s thread = Some ko; is_aligned thread (objBitsKO ko); fst (projectKO ko s) = {(obj, s)}; obj = tcb; ps_clear thread (objBitsKO ko) s\<rbrakk> \<Longrightarrow> map_to_ctes ((ksPSpace s)(thread \<mapsto> KOTCB tcb')) = ctes_of s proof (prove)
goal (1 subgoal):
 1. \<And>ko obj. \<lbrakk>\<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> getF tcb' = getF tcb; ksPSpace s thread = Some (KOTCB tcb); is_aligned thread tcbBlockSizeBits; ko = KOTCB tcb; obj = tcb; ps_clear thread tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> map_to_ctes ((ksPSpace s)(thread \<mapsto> KOTCB tcb')) = ctes_of s proof (prove)
goal (4 subgoals):
 1. \<And>ko obj. \<lbrakk>\<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> getF tcb' = getF tcb; ksPSpace s thread = Some (KOTCB tcb); is_aligned thread tcbBlockSizeBits; ko = KOTCB tcb; obj = tcb; ps_clear thread tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> ksPSpace s thread = Some (KOTCB (?tcb'2 ko obj))
 2. \<And>ko obj. \<lbrakk>\<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> getF tcb' = getF tcb; ksPSpace s thread = Some (KOTCB tcb); is_aligned thread tcbBlockSizeBits; ko = KOTCB tcb; obj = tcb; ps_clear thread tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> is_aligned thread tcbBlockSizeBits
 3. \<And>ko obj. \<lbrakk>\<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> getF tcb' = getF tcb; ksPSpace s thread = Some (KOTCB tcb); is_aligned thread tcbBlockSizeBits; ko = KOTCB tcb; obj = tcb; ps_clear thread tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> ps_clear thread tcbBlockSizeBits s
 4. \<And>ko obj. \<lbrakk>\<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> getF tcb' = getF tcb; ksPSpace s thread = Some (KOTCB tcb); is_aligned thread tcbBlockSizeBits; ko = KOTCB tcb; obj = tcb; ps_clear thread tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> (\<lambda>x. if \<exists>getF setF. tcb_cte_cases (x - thread) = Some (getF, setF) \<and> getF tcb' \<noteq> getF (?tcb'2 ko obj) then case tcb_cte_cases (x - thread) of Some (getF, setF) \<Rightarrow> Some (getF tcb') else ctes_of s x) = ctes_of s proof (prove)
goal (1 subgoal):
 1. \<And>ko obj. \<lbrakk>\<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> getF tcb' = getF tcb; ksPSpace s thread = Some (KOTCB tcb); is_aligned thread tcbBlockSizeBits; ko = KOTCB tcb; obj = tcb; ps_clear thread tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> (\<lambda>x. if \<exists>getF setF. tcb_cte_cases (x - thread) = Some (getF, setF) \<and> getF tcb' \<noteq> getF tcb then case tcb_cte_cases (x - thread) of Some (getF, setF) \<Rightarrow> Some (getF tcb') else ctes_of s x) = ctes_of s proof (prove)
goal (1 subgoal):
 1. \<And>ko obj x. \<lbrakk>\<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> getF tcb' = getF tcb; ksPSpace s thread = Some (KOTCB tcb); is_aligned thread tcbBlockSizeBits; ko = KOTCB tcb; obj = tcb; ps_clear thread tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> (if \<exists>getF setF. tcb_cte_cases (x - thread) = Some (getF, setF) \<and> getF tcb' \<noteq> getF tcb then case tcb_cte_cases (x - thread) of Some (getF, setF) \<Rightarrow> Some (getF tcb') else ctes_of s x) = ctes_of s x proof (prove)
goal (1 subgoal):
 1. \<And>x getF setF. \<lbrakk>\<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> getF tcb' = getF tcb; ksPSpace s thread = Some (KOTCB tcb); is_aligned thread tcbBlockSizeBits; ps_clear thread tcbBlockSizeBits s; getF tcb' \<noteq> getF tcb; tcb_cte_cases (x - thread) = Some (getF, setF)\<rbrakk> \<Longrightarrow> Some (getF tcb') = ctes_of s x proof (prove)
goal (1 subgoal):
 1. \<And>x getF setF. \<lbrakk>ksPSpace s thread = Some (KOTCB tcb); is_aligned thread tcbBlockSizeBits; ps_clear thread tcbBlockSizeBits s; getF tcb' \<noteq> getF tcb; tcb_cte_cases (x - thread) = Some (getF, setF); case (getF, setF) of (getF, setF) \<Rightarrow> getF tcb' = getF tcb\<rbrakk> \<Longrightarrow> Some (getF tcb') = ctes_of s x proof (prove)
goal:
No subgoals!