theory IsolatedThreadAction

lemma obj_at_partial_overwrite_id2:
  "\<lbrakk> \<forall>x. tcb_at' (idx x) s; \<And>v tcb. P v \<or> True \<Longrightarrow> injectKO v \<noteq> KOTCB tcb \<rbrakk>
    \<Longrightarrow> obj_at' P p (ksPSpace_update (partial_overwrite idx f) s)
             = obj_at' P p s" apply (frule dom_partial_overwrite[where tsrs=f]) apply (simp add: obj_at'_def ps_clear_def partial_overwrite_def
                   projectKOs split: if_split) apply clarsimp apply (drule_tac x=x in spec) apply (clarsimp simp: put_tcb_state_regs_def objBits_simps
                        project_inject) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x. tcb_at' (idx x) s; \<And>v tcb. P v \<or> True \<Longrightarrow> injectKOS v \<noteq> KOTCB tcb\<rbrakk> \<Longrightarrow> obj_at' P p (ksPSpace_update (partial_overwrite idx f) s) = obj_at' P p s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x. tcb_at' (idx x) s; \<And>v tcb. P v \<or> True \<Longrightarrow> injectKOS v \<noteq> KOTCB tcb; dom (partial_overwrite idx f (ksPSpace s)) = dom (ksPSpace s)\<rbrakk> \<Longrightarrow> obj_at' P p (ksPSpace_update (partial_overwrite idx f) s) = obj_at' P p s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x. \<exists>ko. ksPSpace s (idx x) = Some ko \<and> is_aligned (idx x) (objBitsKO ko) \<and> (\<exists>obj. ko = KOTCB obj) \<and> ({idx x..idx x + 2 ^ objBitsKO ko - 1} - {idx x}) \<inter> dom (ksPSpace s) = {}; \<And>v tcb. injectKOS v \<noteq> KOTCB tcb; dom (\<lambda>x. if x \<in> range idx then put_tcb_state_regs (f (inv idx x)) (ksPSpace s x) else ksPSpace s x) = dom (ksPSpace s)\<rbrakk> \<Longrightarrow> p \<in> range idx \<longrightarrow> (\<exists>ko. put_tcb_state_regs (f (inv idx p)) (ksPSpace s p) = Some ko \<and> is_aligned p (objBitsKO ko) \<and> (\<exists>obj. projectKO_opt ko = Some obj \<and> P obj \<and> ({p..p + 2 ^ objBitsKO ko - 1} - {p}) \<inter> dom (ksPSpace s) = {})) = (\<exists>ko. ksPSpace s p = Some ko \<and> is_aligned p (objBitsKO ko) \<and> (\<exists>obj. projectKO_opt ko = Some obj \<and> P obj \<and> ({p..p + 2 ^ objBitsKO ko - 1} - {p}) \<inter> dom (ksPSpace s) = {})) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>x. \<exists>ko. ksPSpace s (idx x) = Some ko \<and> is_aligned (idx x) (objBitsKO ko) \<and> (\<exists>obj. ko = KOTCB obj) \<and> ({idx x..idx x + 2 ^ objBitsKO ko - 1} - {idx x}) \<inter> dom (ksPSpace s) = {}; \<And>v tcb. injectKOS v \<noteq> KOTCB tcb; dom (\<lambda>x. if x \<in> range idx then put_tcb_state_regs (f (inv idx x)) (ksPSpace s x) else ksPSpace s x) = dom (ksPSpace s); p = idx x\<rbrakk> \<Longrightarrow> (\<exists>ko. put_tcb_state_regs (f (inv idx (idx x))) (ksPSpace s (idx x)) = Some ko \<and> is_aligned (idx x) (objBitsKO ko) \<and> (\<exists>obj. projectKO_opt ko = Some obj \<and> P obj \<and> ({idx x..idx x + 2 ^ objBitsKO ko - 1} - {idx x}) \<inter> dom (ksPSpace s) = {})) = (\<exists>ko. ksPSpace s (idx x) = Some ko \<and> is_aligned (idx x) (objBitsKO ko) \<and> (\<exists>obj. projectKO_opt ko = Some obj \<and> P obj \<and> ({idx x..idx x + 2 ^ objBitsKO ko - 1} - {idx x}) \<inter> dom (ksPSpace s) = {})) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>v tcb. injectKOS v \<noteq> KOTCB tcb; dom (\<lambda>x. if x \<in> range idx then put_tcb_state_regs (f (inv idx x)) (ksPSpace s x) else ksPSpace s x) = dom (ksPSpace s); p = idx x; \<exists>ko. ksPSpace s (idx x) = Some ko \<and> is_aligned (idx x) (objBitsKO ko) \<and> (\<exists>obj. ko = KOTCB obj) \<and> ({idx x..idx x + 2 ^ objBitsKO ko - 1} - {idx x}) \<inter> dom (ksPSpace s) = {}\<rbrakk> \<Longrightarrow> (\<exists>ko. put_tcb_state_regs (f (inv idx (idx x))) (ksPSpace s (idx x)) = Some ko \<and> is_aligned (idx x) (objBitsKO ko) \<and> (\<exists>obj. projectKO_opt ko = Some obj \<and> P obj \<and> ({idx x..idx x + 2 ^ objBitsKO ko - 1} - {idx x}) \<inter> dom (ksPSpace s) = {})) = (\<exists>ko. ksPSpace s (idx x) = Some ko \<and> is_aligned (idx x) (objBitsKO ko) \<and> (\<exists>obj. projectKO_opt ko = Some obj \<and> P obj \<and> ({idx x..idx x + 2 ^ objBitsKO ko - 1} - {idx x}) \<inter> dom (ksPSpace s) = {})) proof (prove)
goal:
No subgoals!