theory KHeap_R

lemma setObject_ep_pre:
  assumes "\<lbrace>P and ep_at' p\<rbrace> setObject p (e::endpoint) \<lbrace>Q\<rbrace>"
  shows "\<lbrace>P\<rbrace> setObject p (e::endpoint) \<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 e \<lbrace>Q\<rbrace> proof (prove)
using this:
\<lbrace>P and ep_at' p\<rbrace> setObject p e \<lbrace>Q\<rbrace>

goal (1 subgoal):
 1. \<lbrace>P\<rbrace> setObject p e \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s uu_. \<lbrakk>\<forall>s. P s \<and> ep_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 4;
y <- magnitudeCheck p (snd (lookupAround2 p ps)) 4;
return (KOEndpoint e)
od;
modify (ksPSpace_update (\<lambda>_. ps(fst pa \<mapsto> obj')))
od) s). Q () (snd x)); P s; ksPSpace s p = Some (KOEndpoint uu_); is_aligned p 4; ps_clear p 4 s\<rbrakk> \<Longrightarrow> Q () (s\<lparr>ksPSpace := (ksPSpace s)(p \<mapsto> KOEndpoint e)\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s uu_. \<lbrakk>ksPSpace s p = Some (KOEndpoint uu_); is_aligned p 4; ps_clear p 4 s\<rbrakk> \<Longrightarrow> ep_at' p s
 2. \<And>s uu_. \<lbrakk>P s; ksPSpace s p = Some (KOEndpoint uu_); is_aligned p 4; ps_clear p 4 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 4;
y <- magnitudeCheck p (snd (lookupAround2 p ps)) 4;
return (KOEndpoint e)
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> KOEndpoint e)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s uu_. \<lbrakk>P s; ksPSpace s p = Some (KOEndpoint uu_); is_aligned p 4; ps_clear p 4 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 4;
y <- magnitudeCheck p (snd (lookupAround2 p ps)) 4;
return (KOEndpoint e)
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> KOEndpoint e)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s uu_. \<lbrakk>P s; ksPSpace s p = Some (KOEndpoint uu_); is_aligned p 4; ps_clear p 4 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 4;
y <- magnitudeCheck p (snd (lookupAround2 p ps)) 4;
return (KOEndpoint e)
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> KOEndpoint e)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s uu_. \<lbrakk>P s; ksPSpace s p = Some (KOEndpoint uu_); is_aligned p 4; ps_clear p 4 s\<rbrakk> \<Longrightarrow> ((), s\<lparr>ksPSpace := (ksPSpace s)(p \<mapsto> KOEndpoint e)\<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 4;
y <- magnitudeCheck p (snd (lookupAround2 p ps)) 4;
return (KOEndpoint e)
od;
modify (ksPSpace_update (\<lambda>_. ps(fst pa \<mapsto> obj')))
od) s) proof (prove)
goal:
No subgoals!