theory IsolatedThreadAction

lemma obj_at_partial_overwrite_If:
  "\<lbrakk> \<forall>x. tcb_at' (idx x) s \<rbrakk>
    \<Longrightarrow> obj_at' P p (ksPSpace_update (partial_overwrite idx f) s)
             = (if p \<in> range idx
                then obj_at' (\<lambda>tcb. P (put_tcb_state_regs_tcb (f (inv idx p)) tcb)) p s
                else 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) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>x. tcb_at' (idx x) s \<Longrightarrow> obj_at' P p (ksPSpace_update (partial_overwrite idx f) s) = (if p \<in> range idx then obj_at' (\<lambda>tcb. P (put_tcb_state_regs_tcb (f (inv idx p)) tcb)) p s else obj_at' P p s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x. tcb_at' (idx x) s; dom (partial_overwrite idx f (ksPSpace s)) = dom (ksPSpace s)\<rbrakk> \<Longrightarrow> obj_at' P p (ksPSpace_update (partial_overwrite idx f) s) = (if p \<in> range idx then obj_at' (\<lambda>tcb. P (put_tcb_state_regs_tcb (f (inv idx p)) tcb)) p s else 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) = {}; 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. ko = KOTCB 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. ko = KOTCB obj \<and> P (put_tcb_state_regs_tcb (f (inv idx 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) = {}; 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. ko = KOTCB 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. ko = KOTCB obj \<and> P (put_tcb_state_regs_tcb (f (inv idx (idx x))) 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>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. ko = KOTCB 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. ko = KOTCB obj \<and> P (put_tcb_state_regs_tcb (f (inv idx (idx x))) obj) \<and> ({idx x..idx x + 2 ^ objBitsKO ko - 1} - {idx x}) \<inter> dom (ksPSpace s) = {})) proof (prove)
goal:
No subgoals!