theory KHeap_R

lemma setObject_tcb_strongest:
  "\<lbrace>\<lambda>s. if t = t' then P tcb else obj_at' P t' s\<rbrace>
  setObject t (tcb :: tcb)
  \<lbrace>\<lambda>rv. obj_at' P t'\<rbrace>" apply (cases "t = t'") apply simp apply (rule hoare_weaken_pre) apply (rule obj_at_setObject3) apply simp apply (simp add: objBits_simps') apply simp apply (simp add: setObject_def split_def) apply (clarsimp simp: valid_def obj_at'_def split_def in_monad
                        updateObject_default_def projectKOs
                        ps_clear_upd) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. if t = t' then P tcb else obj_at' P t' s\<rbrace> setObject t tcb \<lbrace>\<lambda>rv. obj_at' P t'\<rbrace> proof (prove)
goal (2 subgoals):
 1. t = t' \<Longrightarrow> \<lbrace>\<lambda>s. if t = t' then P tcb else obj_at' P t' s\<rbrace> setObject t tcb \<lbrace>\<lambda>rv. obj_at' P t'\<rbrace>
 2. t \<noteq> t' \<Longrightarrow> \<lbrace>\<lambda>s. if t = t' then P tcb else obj_at' P t' s\<rbrace> setObject t tcb \<lbrace>\<lambda>rv. obj_at' P t'\<rbrace> proof (prove)
goal (2 subgoals):
 1. t = t' \<Longrightarrow> \<lbrace>\<lambda>s. P tcb\<rbrace> setObject t' tcb \<lbrace>\<lambda>rv. obj_at' P t'\<rbrace>
 2. t \<noteq> t' \<Longrightarrow> \<lbrace>\<lambda>s. if t = t' then P tcb else obj_at' P t' s\<rbrace> setObject t tcb \<lbrace>\<lambda>rv. obj_at' P t'\<rbrace> proof (prove)
goal (3 subgoals):
 1. t = t' \<Longrightarrow> \<lbrace>?Q4\<rbrace> setObject t' tcb \<lbrace>\<lambda>rv. obj_at' P t'\<rbrace>
 2. \<And>s. \<lbrakk>t = t'; P tcb\<rbrakk> \<Longrightarrow> ?Q4 s
 3. t \<noteq> t' \<Longrightarrow> \<lbrace>\<lambda>s. if t = t' then P tcb else obj_at' P t' s\<rbrace> setObject t tcb \<lbrace>\<lambda>rv. obj_at' P t'\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>ko s x y n. t = t' \<Longrightarrow> updateObject tcb ko t' y n s = updateObject_default tcb ko t' y n s
 2. \<And>v. t = t' \<Longrightarrow> 1 < 2 ^ objBits v
 3. \<And>s. \<lbrakk>t = t'; P tcb\<rbrakk> \<Longrightarrow> P tcb
 4. t \<noteq> t' \<Longrightarrow> \<lbrace>\<lambda>s. if t = t' then P tcb else obj_at' P t' s\<rbrace> setObject t tcb \<lbrace>\<lambda>rv. obj_at' P t'\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>v. t = t' \<Longrightarrow> 1 < 2 ^ objBits v
 2. \<And>s. \<lbrakk>t = t'; P tcb\<rbrakk> \<Longrightarrow> P tcb
 3. t \<noteq> t' \<Longrightarrow> \<lbrace>\<lambda>s. if t = t' then P tcb else obj_at' P t' s\<rbrace> setObject t tcb \<lbrace>\<lambda>rv. obj_at' P t'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>t = t'; P tcb\<rbrakk> \<Longrightarrow> P tcb
 2. t \<noteq> t' \<Longrightarrow> \<lbrace>\<lambda>s. if t = t' then P tcb else obj_at' P t' s\<rbrace> setObject t tcb \<lbrace>\<lambda>rv. obj_at' P t'\<rbrace> proof (prove)
goal (1 subgoal):
 1. t \<noteq> t' \<Longrightarrow> \<lbrace>\<lambda>s. if t = t' then P tcb else obj_at' P t' s\<rbrace> setObject t tcb \<lbrace>\<lambda>rv. obj_at' P t'\<rbrace> proof (prove)
goal (1 subgoal):
 1. t \<noteq> t' \<Longrightarrow> \<lbrace>obj_at' P t'\<rbrace> do ps <- gets ksPSpace;
p <- assert_opt (fst (lookupAround2 t ps));
obj' <- updateObject_default tcb (snd p) t (fst p) (snd (lookupAround2 t ps));
modify (ksPSpace_update (\<lambda>_. ps(fst p \<mapsto> obj')))
od \<lbrace>\<lambda>rv. obj_at' P t'\<rbrace> proof (prove)
goal:
No subgoals!