theory KHeap_R

lemma obj_at_setObject2:
  fixes v :: "'a::pspace_storable"
  fixes P :: "'b::pspace_storable \<Rightarrow> bool"
  assumes R: "\<And>ko s' (v :: 'a) oko x y n s. (ko, s') \<in> fst (updateObject v oko x y n s)
                                  \<Longrightarrow> koTypeOf ko \<noteq> koType TYPE('b)"
  shows
  "\<lbrace> obj_at' P t \<rbrace>
   setObject p (v::'a)
  \<lbrace> \<lambda>rv. obj_at' P t \<rbrace>" apply (simp add: setObject_def split_def) apply (rule hoare_seq_ext [OF _ hoare_gets_sp]) apply (clarsimp simp: valid_def in_monad) apply (frule updateObject_type) apply (drule R) apply (clarsimp simp: obj_at'_def projectKOs) apply (rule conjI) apply (clarsimp simp: lookupAround2_char1) apply (drule iffD1 [OF project_koType, OF exI]) apply simp apply (clarsimp simp: ps_clear_upd lookupAround2_char1) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' P t\<rbrace> setObject p v \<lbrace>\<lambda>rv. obj_at' P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' P t\<rbrace> do ps <- gets ksPSpace;
pa <- assert_opt (fst (lookupAround2 p ps));
obj' <- updateObject v (snd pa) p (fst pa) (snd (lookupAround2 p ps));
modify (ksPSpace_update (\<lambda>_. ps(fst pa \<mapsto> obj')))
od \<lbrace>\<lambda>rv. obj_at' P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ps. \<lbrace>\<lambda>s. ps = ksPSpace s \<and> obj_at' P t s\<rbrace> do pa <- assert_opt (fst (lookupAround2 p ps));
obj' <- updateObject v (snd pa) p (fst pa) (snd (lookupAround2 p ps));
modify (ksPSpace_update (\<lambda>_. ps(fst pa \<mapsto> obj')))
od \<lbrace>\<lambda>rv. obj_at' P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a ba s'' obj'. \<lbrakk>obj_at' P t s; fst (lookupAround2 p (ksPSpace s)) = Some (a, ba); (obj', s'') \<in> fst (updateObject v ba p a (snd (lookupAround2 p (ksPSpace s))) s)\<rbrakk> \<Longrightarrow> obj_at' P t (s''\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> obj')\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s a ba s'' obj'. \<lbrakk>obj_at' P t s; fst (lookupAround2 p (ksPSpace s)) = Some (a, ba); (obj', s'') \<in> fst (updateObject v ba p a (snd (lookupAround2 p (ksPSpace s))) s); koTypeOf obj' = koTypeOf ba\<rbrakk> \<Longrightarrow> obj_at' P t (s''\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> obj')\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s a ba s'' obj'. \<lbrakk>obj_at' P t s; fst (lookupAround2 p (ksPSpace s)) = Some (a, ba); koTypeOf obj' = koTypeOf ba; koTypeOf obj' \<noteq> koType TYPE('b)\<rbrakk> \<Longrightarrow> obj_at' P t (s''\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> obj')\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s a ba s'' obj' ko obj. \<lbrakk>fst (lookupAround2 p (ksPSpace s)) = Some (a, ba); koTypeOf obj' = koTypeOf ba; koTypeOf ba \<noteq> koType TYPE('b); ksPSpace s t = Some ko; is_aligned t (objBitsKO ko); projectKO_opt ko = Some obj; P obj; ps_clear t (objBitsKO ko) s\<rbrakk> \<Longrightarrow> (t = a \<longrightarrow> is_aligned a (objBitsKO obj') \<and> (\<exists>obj. projectKO_opt obj' = Some obj \<and> P obj \<and> ps_clear a (objBitsKO obj') (s''\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> obj')\<rparr>))) \<and> (t \<noteq> a \<longrightarrow> ps_clear t (objBitsKO ko) (s''\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> obj')\<rparr>)) proof (prove)
goal (2 subgoals):
 1. \<And>s a ba s'' obj' ko obj. \<lbrakk>fst (lookupAround2 p (ksPSpace s)) = Some (a, ba); koTypeOf obj' = koTypeOf ba; koTypeOf ba \<noteq> koType TYPE('b); ksPSpace s t = Some ko; is_aligned t (objBitsKO ko); projectKO_opt ko = Some obj; P obj; ps_clear t (objBitsKO ko) s\<rbrakk> \<Longrightarrow> t = a \<longrightarrow> is_aligned a (objBitsKO obj') \<and> (\<exists>obj. projectKO_opt obj' = Some obj \<and> P obj \<and> ps_clear a (objBitsKO obj') (s''\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> obj')\<rparr>))
 2. \<And>s a ba s'' obj' ko obj. \<lbrakk>fst (lookupAround2 p (ksPSpace s)) = Some (a, ba); koTypeOf obj' = koTypeOf ba; koTypeOf ba \<noteq> koType TYPE('b); ksPSpace s t = Some ko; is_aligned t (objBitsKO ko); projectKO_opt ko = Some obj; P obj; ps_clear t (objBitsKO ko) s\<rbrakk> \<Longrightarrow> t \<noteq> a \<longrightarrow> ps_clear t (objBitsKO ko) (s''\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> obj')\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s s'' obj' ko obj. \<lbrakk>koTypeOf obj' = koTypeOf ko; koTypeOf ko \<noteq> koType TYPE('b); is_aligned t (objBitsKO ko); projectKO_opt ko = Some obj; P obj; ps_clear t (objBitsKO ko) s; t \<le> p; ksPSpace s t = Some ko; \<forall>z. t < z \<and> z \<le> p \<longrightarrow> ksPSpace s z = None\<rbrakk> \<Longrightarrow> is_aligned t (objBitsKO obj') \<and> (\<exists>obj. projectKO_opt obj' = Some obj \<and> P obj \<and> ps_clear t (objBitsKO obj') (s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> obj')\<rparr>))
 2. \<And>s a ba s'' obj' ko obj. \<lbrakk>fst (lookupAround2 p (ksPSpace s)) = Some (a, ba); koTypeOf obj' = koTypeOf ba; koTypeOf ba \<noteq> koType TYPE('b); ksPSpace s t = Some ko; is_aligned t (objBitsKO ko); projectKO_opt ko = Some obj; P obj; ps_clear t (objBitsKO ko) s\<rbrakk> \<Longrightarrow> t \<noteq> a \<longrightarrow> ps_clear t (objBitsKO ko) (s''\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> obj')\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s s'' obj' ko obj. \<lbrakk>koTypeOf obj' = koTypeOf ko; koTypeOf ko \<noteq> koType TYPE('b); is_aligned t (objBitsKO ko); P obj; ps_clear t (objBitsKO ko) s; t \<le> p; ksPSpace s t = Some ko; \<forall>z. t < z \<and> z \<le> p \<longrightarrow> ksPSpace s z = None; koTypeOf ko = koType TYPE('b)\<rbrakk> \<Longrightarrow> is_aligned t (objBitsKO obj') \<and> (\<exists>obj. projectKO_opt obj' = Some obj \<and> P obj \<and> ps_clear t (objBitsKO obj') (s''\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> obj')\<rparr>))
 2. \<And>s a ba s'' obj' ko obj. \<lbrakk>fst (lookupAround2 p (ksPSpace s)) = Some (a, ba); koTypeOf obj' = koTypeOf ba; koTypeOf ba \<noteq> koType TYPE('b); ksPSpace s t = Some ko; is_aligned t (objBitsKO ko); projectKO_opt ko = Some obj; P obj; ps_clear t (objBitsKO ko) s\<rbrakk> \<Longrightarrow> t \<noteq> a \<longrightarrow> ps_clear t (objBitsKO ko) (s''\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> obj')\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s a ba s'' obj' ko obj. \<lbrakk>fst (lookupAround2 p (ksPSpace s)) = Some (a, ba); koTypeOf obj' = koTypeOf ba; koTypeOf ba \<noteq> koType TYPE('b); ksPSpace s t = Some ko; is_aligned t (objBitsKO ko); projectKO_opt ko = Some obj; P obj; ps_clear t (objBitsKO ko) s\<rbrakk> \<Longrightarrow> t \<noteq> a \<longrightarrow> ps_clear t (objBitsKO ko) (s''\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> obj')\<rparr>) proof (prove)
goal:
No subgoals!