theory KHeap_R

lemma setObject_typ_at_not:
  "\<lbrace>\<lambda>s. \<not> (typ_at' T p' s)\<rbrace> setObject p v \<lbrace>\<lambda>r s. \<not> (typ_at' T p' s)\<rbrace>" apply (clarsimp simp: setObject_def valid_def in_monad split_def) apply (erule notE) apply (clarsimp simp: typ_at'_def ko_wp_at'_def lookupAround2_char1
                 split: if_split_asm) apply (drule updateObject_type) apply clarsimp apply (drule objBits_type) apply (clarsimp elim!: ps_clear_domE) apply fastforce apply (clarsimp elim!: ps_clear_domE) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<not> typ_at' T p' s\<rbrace> setObject p v \<lbrace>\<lambda>r s. \<not> typ_at' T p' s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a ba s'' obj'. \<lbrakk>\<not> typ_at' T p' s; typ_at' T p' (s''\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> obj')\<rparr>); 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> False proof (prove)
goal (1 subgoal):
 1. \<And>s a ba s'' obj'. \<lbrakk>typ_at' T p' (s''\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> obj')\<rparr>); 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> typ_at' T p' s proof (prove)
goal (2 subgoals):
 1. \<And>s ba s'' obj'. \<lbrakk>(obj', s'') \<in> fst (updateObject v ba p p' (snd (lookupAround2 p (ksPSpace s))) s); p' \<le> p; ksPSpace s p' = Some ba; \<forall>z. p' < z \<and> z \<le> p \<longrightarrow> ksPSpace s z = None; is_aligned p' (objBitsKO obj'); ps_clear p' (objBitsKO obj') (s''\<lparr>ksPSpace := (ksPSpace s)(p' \<mapsto> obj')\<rparr>); T = koTypeOf obj'\<rbrakk> \<Longrightarrow> is_aligned p' (objBitsKO ba) \<and> koTypeOf ba = koTypeOf obj' \<and> ps_clear p' (objBitsKO ba) s
 2. \<And>s a ba s'' obj' ko. \<lbrakk>(obj', s'') \<in> fst (updateObject v ba p a (snd (lookupAround2 p (ksPSpace s))) s); p' \<noteq> a; a \<le> p; ksPSpace s a = Some ba; \<forall>z. a < z \<and> z \<le> p \<longrightarrow> ksPSpace s z = None; ksPSpace s p' = Some ko; is_aligned p' (objBitsKO ko); ps_clear p' (objBitsKO ko) (s''\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> obj')\<rparr>); T = koTypeOf ko\<rbrakk> \<Longrightarrow> ps_clear p' (objBitsKO ko) s proof (prove)
goal (2 subgoals):
 1. \<And>s ba s'' obj'. \<lbrakk>p' \<le> p; ksPSpace s p' = Some ba; \<forall>z. p' < z \<and> z \<le> p \<longrightarrow> ksPSpace s z = None; is_aligned p' (objBitsKO obj'); ps_clear p' (objBitsKO obj') (s''\<lparr>ksPSpace := (ksPSpace s)(p' \<mapsto> obj')\<rparr>); T = koTypeOf obj'; koTypeOf obj' = koTypeOf ba\<rbrakk> \<Longrightarrow> is_aligned p' (objBitsKO ba) \<and> koTypeOf ba = koTypeOf obj' \<and> ps_clear p' (objBitsKO ba) s
 2. \<And>s a ba s'' obj' ko. \<lbrakk>(obj', s'') \<in> fst (updateObject v ba p a (snd (lookupAround2 p (ksPSpace s))) s); p' \<noteq> a; a \<le> p; ksPSpace s a = Some ba; \<forall>z. a < z \<and> z \<le> p \<longrightarrow> ksPSpace s z = None; ksPSpace s p' = Some ko; is_aligned p' (objBitsKO ko); ps_clear p' (objBitsKO ko) (s''\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> obj')\<rparr>); T = koTypeOf ko\<rbrakk> \<Longrightarrow> ps_clear p' (objBitsKO ko) s proof (prove)
goal (2 subgoals):
 1. \<And>s ba s'' obj'. \<lbrakk>p' \<le> p; ksPSpace s p' = Some ba; \<forall>z. p' < z \<and> z \<le> p \<longrightarrow> ksPSpace s z = None; is_aligned p' (objBitsKO obj'); ps_clear p' (objBitsKO obj') (s''\<lparr>ksPSpace := (ksPSpace s)(p' \<mapsto> obj')\<rparr>); T = koTypeOf ba; koTypeOf obj' = koTypeOf ba\<rbrakk> \<Longrightarrow> is_aligned p' (objBitsKO ba) \<and> ps_clear p' (objBitsKO ba) s
 2. \<And>s a ba s'' obj' ko. \<lbrakk>(obj', s'') \<in> fst (updateObject v ba p a (snd (lookupAround2 p (ksPSpace s))) s); p' \<noteq> a; a \<le> p; ksPSpace s a = Some ba; \<forall>z. a < z \<and> z \<le> p \<longrightarrow> ksPSpace s z = None; ksPSpace s p' = Some ko; is_aligned p' (objBitsKO ko); ps_clear p' (objBitsKO ko) (s''\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> obj')\<rparr>); T = koTypeOf ko\<rbrakk> \<Longrightarrow> ps_clear p' (objBitsKO ko) s proof (prove)
goal (2 subgoals):
 1. \<And>s ba s'' obj'. \<lbrakk>p' \<le> p; ksPSpace s p' = Some ba; \<forall>z. p' < z \<and> z \<le> p \<longrightarrow> ksPSpace s z = None; is_aligned p' (objBitsKO obj'); ps_clear p' (objBitsKO obj') (s''\<lparr>ksPSpace := (ksPSpace s)(p' \<mapsto> obj')\<rparr>); T = koTypeOf ba; objBitsKO obj' = objBitsKO ba\<rbrakk> \<Longrightarrow> is_aligned p' (objBitsKO ba) \<and> ps_clear p' (objBitsKO ba) s
 2. \<And>s a ba s'' obj' ko. \<lbrakk>(obj', s'') \<in> fst (updateObject v ba p a (snd (lookupAround2 p (ksPSpace s))) s); p' \<noteq> a; a \<le> p; ksPSpace s a = Some ba; \<forall>z. a < z \<and> z \<le> p \<longrightarrow> ksPSpace s z = None; ksPSpace s p' = Some ko; is_aligned p' (objBitsKO ko); ps_clear p' (objBitsKO ko) (s''\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> obj')\<rparr>); T = koTypeOf ko\<rbrakk> \<Longrightarrow> ps_clear p' (objBitsKO ko) s proof (prove)
goal (2 subgoals):
 1. \<And>s ba obj'. \<lbrakk>p' \<le> p; ksPSpace s p' = Some ba; \<forall>z. p' < z \<and> z \<le> p \<longrightarrow> ksPSpace s z = None; is_aligned p' (objBitsKO ba); T = koTypeOf ba; objBitsKO obj' = objBitsKO ba\<rbrakk> \<Longrightarrow> insert p' (dom (ksPSpace s)) = dom (ksPSpace s)
 2. \<And>s a ba s'' obj' ko. \<lbrakk>(obj', s'') \<in> fst (updateObject v ba p a (snd (lookupAround2 p (ksPSpace s))) s); p' \<noteq> a; a \<le> p; ksPSpace s a = Some ba; \<forall>z. a < z \<and> z \<le> p \<longrightarrow> ksPSpace s z = None; ksPSpace s p' = Some ko; is_aligned p' (objBitsKO ko); ps_clear p' (objBitsKO ko) (s''\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> obj')\<rparr>); T = koTypeOf ko\<rbrakk> \<Longrightarrow> ps_clear p' (objBitsKO ko) s proof (prove)
goal (1 subgoal):
 1. \<And>s a ba s'' obj' ko. \<lbrakk>(obj', s'') \<in> fst (updateObject v ba p a (snd (lookupAround2 p (ksPSpace s))) s); p' \<noteq> a; a \<le> p; ksPSpace s a = Some ba; \<forall>z. a < z \<and> z \<le> p \<longrightarrow> ksPSpace s z = None; ksPSpace s p' = Some ko; is_aligned p' (objBitsKO ko); ps_clear p' (objBitsKO ko) (s''\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> obj')\<rparr>); T = koTypeOf ko\<rbrakk> \<Longrightarrow> ps_clear p' (objBitsKO ko) s proof (prove)
goal (1 subgoal):
 1. \<And>s a ba s'' obj' ko. \<lbrakk>(obj', s'') \<in> fst (updateObject v ba p a (snd (lookupAround2 p (ksPSpace s))) s); p' \<noteq> a; a \<le> p; ksPSpace s a = Some ba; \<forall>z. a < z \<and> z \<le> p \<longrightarrow> ksPSpace s z = None; ksPSpace s p' = Some ko; is_aligned p' (objBitsKO ko); T = koTypeOf ko\<rbrakk> \<Longrightarrow> insert a (dom (ksPSpace s)) = dom (ksPSpace s) proof (prove)
goal:
No subgoals!