theory KHeap_R

lemma setObject_ko_wp_at:
  fixes v :: "'a :: pspace_storable"
  assumes R: "\<And>ko s x y n. (updateObject v ko p y n s)
                   = (updateObject_default v ko p y n s)"
  assumes n: "\<And>v' :: 'a. objBits v' = n"
  assumes m: "(1 :: word32) < 2 ^ n"
  shows      "\<lbrace>\<lambda>s. obj_at' (\<lambda>x :: 'a. True) p s \<longrightarrow>
                    P (ko_wp_at' (if p = p' then K (P' (injectKO v)) else P')p' s)\<rbrace>
                setObject p v
              \<lbrace>\<lambda>rv s. P (ko_wp_at' P' p' s)\<rbrace>" apply (clarsimp simp: setObject_def valid_def in_monad
                        ko_wp_at'_def split_def
                        R updateObject_default_def
                        projectKOs obj_at'_real_def
             split del: if_split) apply (clarsimp simp: project_inject objBits_def[symmetric] n
                        in_magnitude_check [OF _ m]
                 elim!: rsubst[where P=P]
             split del: if_split) apply (rule iffI) apply (clarsimp simp: n ps_clear_upd objBits_def[symmetric]
                  split: if_split_asm) apply (clarsimp simp: n project_inject objBits_def[symmetric]
                        ps_clear_upd
                 split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. obj_at' (\<lambda>x. True) p s \<longrightarrow> P (ko_wp_at' (if p = p' then K (P' (injectKO v)) else P') p' s)\<rbrace> setObject p v \<lbrace>\<lambda>rv s. P (ko_wp_at' P' p' s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s ba uu_ s''. \<lbrakk>is_aligned p (objBitsKO ba) \<and> ps_clear p (objBitsKO ba) s \<longrightarrow> P (\<exists>ko. ksPSpace s p' = Some ko \<and> is_aligned p' (objBitsKO ko) \<and> (if p = p' then \<lambda>y. P' (injectKO v) else P') ko \<and> ps_clear p' (objBitsKO ko) s); ksPSpace s p = Some ba; projectKO_opt ba = Some uu_; is_aligned p (objBits v); ((), s'') \<in> fst (magnitudeCheck p (snd (lookupAround2 p (ksPSpace s))) (objBits v) s)\<rbrakk> \<Longrightarrow> P (\<exists>ko. (if p' = p then Some (injectKO v) else ksPSpace s p') = Some ko \<and> is_aligned p' (objBitsKO ko) \<and> P' ko \<and> ps_clear p' (objBitsKO ko) (s''\<lparr>ksPSpace := (ksPSpace s)(p \<mapsto> injectKO v)\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s uu_. \<lbrakk>ksPSpace s p = Some (injectKO uu_); is_aligned p n; ps_clear p n s\<rbrakk> \<Longrightarrow> (\<exists>ko. ksPSpace s p' = Some ko \<and> is_aligned p' (objBitsKO ko) \<and> (if p = p' then \<lambda>y. P' (injectKO v) else P') ko \<and> ps_clear p' (objBitsKO ko) s) = (\<exists>ko. (if p' = p then Some (injectKO v) else ksPSpace s p') = Some ko \<and> is_aligned p' (objBitsKO ko) \<and> P' ko \<and> ps_clear p' (objBitsKO ko) (s\<lparr>ksPSpace := (ksPSpace s)(p \<mapsto> injectKO v)\<rparr>)) proof (prove)
goal (2 subgoals):
 1. \<And>s uu_. \<lbrakk>ksPSpace s p = Some (injectKO uu_); is_aligned p n; ps_clear p n s; \<exists>ko. ksPSpace s p' = Some ko \<and> is_aligned p' (objBitsKO ko) \<and> (if p = p' then \<lambda>y. P' (injectKO v) else P') ko \<and> ps_clear p' (objBitsKO ko) s\<rbrakk> \<Longrightarrow> \<exists>ko. (if p' = p then Some (injectKO v) else ksPSpace s p') = Some ko \<and> is_aligned p' (objBitsKO ko) \<and> P' ko \<and> ps_clear p' (objBitsKO ko) (s\<lparr>ksPSpace := (ksPSpace s)(p \<mapsto> injectKO v)\<rparr>)
 2. \<And>s uu_. \<lbrakk>ksPSpace s p = Some (injectKO uu_); is_aligned p n; ps_clear p n s; \<exists>ko. (if p' = p then Some (injectKO v) else ksPSpace s p') = Some ko \<and> is_aligned p' (objBitsKO ko) \<and> P' ko \<and> ps_clear p' (objBitsKO ko) (s\<lparr>ksPSpace := (ksPSpace s)(p \<mapsto> injectKO v)\<rparr>)\<rbrakk> \<Longrightarrow> \<exists>ko. ksPSpace s p' = Some ko \<and> is_aligned p' (objBitsKO ko) \<and> (if p = p' then \<lambda>y. P' (injectKO v) else P') ko \<and> ps_clear p' (objBitsKO ko) s proof (prove)
goal (1 subgoal):
 1. \<And>s uu_. \<lbrakk>ksPSpace s p = Some (injectKO uu_); is_aligned p n; ps_clear p n s; \<exists>ko. (if p' = p then Some (injectKO v) else ksPSpace s p') = Some ko \<and> is_aligned p' (objBitsKO ko) \<and> P' ko \<and> ps_clear p' (objBitsKO ko) (s\<lparr>ksPSpace := (ksPSpace s)(p \<mapsto> injectKO v)\<rparr>)\<rbrakk> \<Longrightarrow> \<exists>ko. ksPSpace s p' = Some ko \<and> is_aligned p' (objBitsKO ko) \<and> (if p = p' then \<lambda>y. P' (injectKO v) else P') ko \<and> ps_clear p' (objBitsKO ko) s proof (prove)
goal:
No subgoals!