theory KHeap_R

lemma obj_at_setObject1:
  assumes R: "\<And>(v::'a::pspace_storable) p q n ko s x s''.
                (x, s'') \<in> fst (updateObject v ko p q n s) \<Longrightarrow> x = injectKO v"
  assumes Q: "\<And>(v::'a::pspace_storable) (v'::'a). objBits v = objBits v'"
  shows
  "\<lbrace> obj_at' (\<lambda>x::'a::pspace_storable. True) t \<rbrace>
   setObject p (v::'a::pspace_storable)
  \<lbrace> \<lambda>rv. obj_at' (\<lambda>x::'a::pspace_storable. True) 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 obj_at'_def
                        projectKOs lookupAround2_char1
                        project_inject
                 dest!: R) apply (subgoal_tac "objBitsKO (injectKO v) = objBitsKO (injectKO obj)") apply (intro conjI impI, simp_all) apply fastforce+ apply (fold objBits_def) apply (rule Q) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (\<lambda>x. True) t\<rbrace> setObject p v \<lbrace>\<lambda>rv. obj_at' (\<lambda>x. True) t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (\<lambda>x. True) 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' (\<lambda>x. True) t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ps. \<lbrace>\<lambda>s. ps = ksPSpace s \<and> obj_at' (\<lambda>x. True) 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' (\<lambda>x. True) t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s obj a ba s''a. \<lbrakk>ksPSpace s t = Some (injectKO obj); is_aligned t (objBitsKO (injectKO obj)); ps_clear t (objBitsKO (injectKO obj)) s; a \<le> p; ksPSpace s a = Some ba; \<forall>z. a < z \<and> z \<le> p \<longrightarrow> ksPSpace s z = None\<rbrakk> \<Longrightarrow> (t = a \<longrightarrow> is_aligned a (objBitsKO (injectKO v)) \<and> (\<exists>obj. injectKO obj = injectKO v) \<and> ps_clear a (objBitsKO (injectKO v)) (s''a\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> injectKO v)\<rparr>)) \<and> (t \<noteq> a \<longrightarrow> (\<exists>obja. injectKO obja = injectKO obj) \<and> ps_clear t (objBitsKO (injectKO obj)) (s''a\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> injectKO v)\<rparr>)) proof (prove)
goal (2 subgoals):
 1. \<And>s obj a ba s''a. \<lbrakk>ksPSpace s t = Some (injectKO obj); is_aligned t (objBitsKO (injectKO obj)); ps_clear t (objBitsKO (injectKO obj)) s; a \<le> p; ksPSpace s a = Some ba; \<forall>z. a < z \<and> z \<le> p \<longrightarrow> ksPSpace s z = None; objBitsKO (injectKO v) = objBitsKO (injectKO obj)\<rbrakk> \<Longrightarrow> (t = a \<longrightarrow> is_aligned a (objBitsKO (injectKO v)) \<and> (\<exists>obj. injectKO obj = injectKO v) \<and> ps_clear a (objBitsKO (injectKO v)) (s''a\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> injectKO v)\<rparr>)) \<and> (t \<noteq> a \<longrightarrow> (\<exists>obja. injectKO obja = injectKO obj) \<and> ps_clear t (objBitsKO (injectKO obj)) (s''a\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> injectKO v)\<rparr>))
 2. \<And>s obj a ba s''a. \<lbrakk>ksPSpace s t = Some (injectKO obj); is_aligned t (objBitsKO (injectKO obj)); ps_clear t (objBitsKO (injectKO obj)) s; a \<le> p; ksPSpace s a = Some ba; \<forall>z. a < z \<and> z \<le> p \<longrightarrow> ksPSpace s z = None\<rbrakk> \<Longrightarrow> objBitsKO (injectKO v) = objBitsKO (injectKO obj) proof (prove)
goal (5 subgoals):
 1. \<And>s obj a. \<lbrakk>is_aligned a (objBitsKO (injectKO obj)); ps_clear a (objBitsKO (injectKO obj)) s; a \<le> p; ksPSpace s a = Some (injectKO obj); \<forall>z. a < z \<and> z \<le> p \<longrightarrow> ksPSpace s z = None; objBitsKO (injectKO v) = objBitsKO (injectKO obj); t = a\<rbrakk> \<Longrightarrow> \<exists>obj. injectKO obj = injectKO v
 2. \<And>s obj a ba s''a. \<lbrakk>ba = injectKO obj; is_aligned a (objBitsKO (injectKO obj)); ps_clear a (objBitsKO (injectKO obj)) s; a \<le> p; ksPSpace s a = Some (injectKO obj); \<forall>z. a < z \<and> z \<le> p \<longrightarrow> ksPSpace s z = None; objBitsKO (injectKO v) = objBitsKO (injectKO obj); t = a\<rbrakk> \<Longrightarrow> ps_clear a (objBitsKO (injectKO obj)) (s''a\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> injectKO v)\<rparr>)
 3. \<And>s obj a ba. \<lbrakk>ksPSpace s t = Some (injectKO obj); is_aligned t (objBitsKO (injectKO obj)); ps_clear t (objBitsKO (injectKO obj)) s; a \<le> p; ksPSpace s a = Some ba; \<forall>z. a < z \<and> z \<le> p \<longrightarrow> ksPSpace s z = None; objBitsKO (injectKO v) = objBitsKO (injectKO obj); t \<noteq> a\<rbrakk> \<Longrightarrow> \<exists>obja. injectKO obja = injectKO obj
 4. \<And>s obj a ba s''a. \<lbrakk>ksPSpace s t = Some (injectKO obj); is_aligned t (objBitsKO (injectKO obj)); ps_clear t (objBitsKO (injectKO obj)) s; a \<le> p; ksPSpace s a = Some ba; \<forall>z. a < z \<and> z \<le> p \<longrightarrow> ksPSpace s z = None; objBitsKO (injectKO v) = objBitsKO (injectKO obj); t \<noteq> a\<rbrakk> \<Longrightarrow> ps_clear t (objBitsKO (injectKO obj)) (s''a\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> injectKO v)\<rparr>)
 5. \<And>s obj a ba. \<lbrakk>ksPSpace s t = Some (injectKO obj); is_aligned t (objBitsKO (injectKO obj)); ps_clear t (objBitsKO (injectKO obj)) s; a \<le> p; ksPSpace s a = Some ba; \<forall>z. a < z \<and> z \<le> p \<longrightarrow> ksPSpace s z = None\<rbrakk> \<Longrightarrow> objBitsKO (injectKO v) = objBitsKO (injectKO obj) proof (prove)
goal (1 subgoal):
 1. \<And>s obj a ba. \<lbrakk>ksPSpace s t = Some (injectKO obj); is_aligned t (objBitsKO (injectKO obj)); ps_clear t (objBitsKO (injectKO obj)) s; a \<le> p; ksPSpace s a = Some ba; \<forall>z. a < z \<and> z \<le> p \<longrightarrow> ksPSpace s z = None\<rbrakk> \<Longrightarrow> objBitsKO (injectKO v) = objBitsKO (injectKO obj) proof (prove)
goal (1 subgoal):
 1. \<And>s obj a ba. \<lbrakk>ksPSpace s t = Some (injectKO obj); is_aligned t (objBits obj); ps_clear t (objBits obj) s; a \<le> p; ksPSpace s a = Some ba; \<forall>z. a < z \<and> z \<le> p \<longrightarrow> ksPSpace s z = None\<rbrakk> \<Longrightarrow> objBits v = objBits obj proof (prove)
goal:
No subgoals!