theory KHeap_R

lemma setObject_tcb_pre:
  assumes "\<lbrace>P and tcb_at' p\<rbrace> setObject p (t::tcb) \<lbrace>Q\<rbrace>"
  shows "\<lbrace>P\<rbrace> setObject p (t::tcb) \<lbrace>Q\<rbrace>" using assms apply (clarsimp simp: valid_def setObject_def in_monad
                        split_def updateObject_default_def
                        projectKOs in_magnitude_check objBits_simps') apply (drule spec, drule mp, erule conjI) apply (simp add: obj_at'_def projectKOs objBits_simps') apply (simp add: split_paired_Ball) apply (drule spec, erule mp) apply (clarsimp simp: in_monad projectKOs in_magnitude_check) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> setObject p t \<lbrace>Q\<rbrace> proof (prove)
using this:
\<lbrace>P and tcb_at' p\<rbrace> setObject p t \<lbrace>Q\<rbrace>

goal (1 subgoal):
 1. \<lbrace>P\<rbrace> setObject p t \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s uu_. \<lbrakk>\<forall>s. P s \<and> tcb_at' p s \<longrightarrow> (\<forall>x\<in>fst ((do ps <- gets ksPSpace;
pa <- assert_opt (fst (lookupAround2 p ps));
obj' <- do y <- assert (p = fst pa);
_ <- projectKO (snd pa);
y <- alignCheck p 9;
y <- magnitudeCheck p (snd (lookupAround2 p ps)) 9;
return (KOTCB t)
od;
modify (ksPSpace_update (\<lambda>_. ps(fst pa \<mapsto> obj')))
od) s). Q () (snd x)); P s; ksPSpace s p = Some (KOTCB uu_); is_aligned p 9; ps_clear p 9 s\<rbrakk> \<Longrightarrow> Q () (s\<lparr>ksPSpace := (ksPSpace s)(p \<mapsto> KOTCB t)\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s uu_. \<lbrakk>ksPSpace s p = Some (KOTCB uu_); is_aligned p 9; ps_clear p 9 s\<rbrakk> \<Longrightarrow> tcb_at' p s
 2. \<And>s uu_. \<lbrakk>P s; ksPSpace s p = Some (KOTCB uu_); is_aligned p 9; ps_clear p 9 s; \<forall>x\<in>fst ((do ps <- gets ksPSpace;
pa <- assert_opt (fst (lookupAround2 p ps));
obj' <- do y <- assert (p = fst pa);
_ <- projectKO (snd pa);
y <- alignCheck p 9;
y <- magnitudeCheck p (snd (lookupAround2 p ps)) 9;
return (KOTCB t)
od;
modify (ksPSpace_update (\<lambda>_. ps(fst pa \<mapsto> obj')))
od) s). Q () (snd x)\<rbrakk> \<Longrightarrow> Q () (s\<lparr>ksPSpace := (ksPSpace s)(p \<mapsto> KOTCB t)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s uu_. \<lbrakk>P s; ksPSpace s p = Some (KOTCB uu_); is_aligned p 9; ps_clear p 9 s; \<forall>x\<in>fst ((do ps <- gets ksPSpace;
pa <- assert_opt (fst (lookupAround2 p ps));
obj' <- do y <- assert (p = fst pa);
_ <- projectKO (snd pa);
y <- alignCheck p 9;
y <- magnitudeCheck p (snd (lookupAround2 p ps)) 9;
return (KOTCB t)
od;
modify (ksPSpace_update (\<lambda>_. ps(fst pa \<mapsto> obj')))
od) s). Q () (snd x)\<rbrakk> \<Longrightarrow> Q () (s\<lparr>ksPSpace := (ksPSpace s)(p \<mapsto> KOTCB t)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s uu_. \<lbrakk>P s; ksPSpace s p = Some (KOTCB uu_); is_aligned p 9; ps_clear p 9 s; \<forall>y. ((), y) \<in> fst ((do ps <- gets ksPSpace;
pa <- assert_opt (fst (lookupAround2 p ps));
obj' <- do y <- assert (p = fst pa);
_ <- projectKO (snd pa);
y <- alignCheck p 9;
y <- magnitudeCheck p (snd (lookupAround2 p ps)) 9;
return (KOTCB t)
od;
modify (ksPSpace_update (\<lambda>_. ps(fst pa \<mapsto> obj')))
od) s) \<longrightarrow> Q () y\<rbrakk> \<Longrightarrow> Q () (s\<lparr>ksPSpace := (ksPSpace s)(p \<mapsto> KOTCB t)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s uu_. \<lbrakk>P s; ksPSpace s p = Some (KOTCB uu_); is_aligned p 9; ps_clear p 9 s\<rbrakk> \<Longrightarrow> ((), s\<lparr>ksPSpace := (ksPSpace s)(p \<mapsto> KOTCB t)\<rparr>) \<in> fst ((do ps <- gets ksPSpace;
pa <- assert_opt (fst (lookupAround2 p ps));
obj' <- do y <- assert (p = fst pa);
_ <- projectKO (snd pa);
y <- alignCheck p 9;
y <- magnitudeCheck p (snd (lookupAround2 p ps)) 9;
return (KOTCB t)
od;
modify (ksPSpace_update (\<lambda>_. ps(fst pa \<mapsto> obj')))
od) s) proof (prove)
goal:
No subgoals!