theory KHeap_R

lemma setObject_valid_objs':
  assumes x: "\<And>x n ko s ko' s'.
       \<lbrakk> (ko', s') \<in> fst (updateObject val ko ptr x n s); P s;
          valid_obj' ko s; lookupAround2 ptr (ksPSpace s) = (Some (x, ko), n) \<rbrakk>
           \<Longrightarrow> valid_obj' ko' s"
  shows "\<lbrace>valid_objs' and P\<rbrace> setObject ptr val \<lbrace>\<lambda>rv. valid_objs'\<rbrace>" apply (clarsimp simp: valid_def) apply (subgoal_tac "\<forall>ko. valid_obj' ko s \<longrightarrow> valid_obj' ko b") defer apply clarsimp apply (erule(1) use_valid [OF _ setObject_valid_obj]) apply (clarsimp simp: setObject_def split_def in_monad
                        lookupAround2_char1) apply (simp add: valid_objs'_def) apply clarsimp apply (drule spec, erule mp) apply (drule(1) x) apply (simp add: ranI) apply (simp add: prod_eqI lookupAround2_char1) apply (clarsimp elim!: ranE split: if_split_asm simp: ranI) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs' and P\<rbrace> setObject ptr val \<lbrace>\<lambda>rv. valid_objs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<lbrakk>((), b) \<in> fst (setObject ptr val s); valid_objs' s; P s\<rbrakk> \<Longrightarrow> valid_objs' b proof (prove)
goal (2 subgoals):
 1. \<And>s b. \<lbrakk>((), b) \<in> fst (setObject ptr val s); valid_objs' s; P s; \<forall>ko. valid_obj' ko s \<longrightarrow> valid_obj' ko b\<rbrakk> \<Longrightarrow> valid_objs' b
 2. \<And>s b. \<lbrakk>((), b) \<in> fst (setObject ptr val s); valid_objs' s; P s\<rbrakk> \<Longrightarrow> \<forall>ko. valid_obj' ko s \<longrightarrow> valid_obj' ko b proof (prove)
goal (2 subgoals):
 1. \<And>s b. \<lbrakk>((), b) \<in> fst (setObject ptr val s); valid_objs' s; P s\<rbrakk> \<Longrightarrow> \<forall>ko. valid_obj' ko s \<longrightarrow> valid_obj' ko b
 2. \<And>s b. \<lbrakk>((), b) \<in> fst (setObject ptr val s); valid_objs' s; P s; \<forall>ko. valid_obj' ko s \<longrightarrow> valid_obj' ko b\<rbrakk> \<Longrightarrow> valid_objs' b proof (prove)
goal (2 subgoals):
 1. \<And>s b ko. \<lbrakk>((), b) \<in> fst (setObject ptr val s); valid_objs' s; P s; valid_obj' ko s\<rbrakk> \<Longrightarrow> valid_obj' ko b
 2. \<And>s b. \<lbrakk>((), b) \<in> fst (setObject ptr val s); valid_objs' s; P s; \<forall>ko. valid_obj' ko s \<longrightarrow> valid_obj' ko b\<rbrakk> \<Longrightarrow> valid_objs' b proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<lbrakk>((), b) \<in> fst (setObject ptr val s); valid_objs' s; P s; \<forall>ko. valid_obj' ko s \<longrightarrow> valid_obj' ko b\<rbrakk> \<Longrightarrow> valid_objs' b proof (prove)
goal (1 subgoal):
 1. \<And>s a ba s''a obj'. \<lbrakk>valid_objs' s; P s; \<forall>ko. valid_obj' ko s \<longrightarrow> valid_obj' ko (s''a\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> obj')\<rparr>); a \<le> ptr; ksPSpace s a = Some ba; \<forall>z. a < z \<and> z \<le> ptr \<longrightarrow> ksPSpace s z = None; (obj', s''a) \<in> fst (updateObject val ba ptr a (snd (lookupAround2 ptr (ksPSpace s))) s)\<rbrakk> \<Longrightarrow> valid_objs' (s''a\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> obj')\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s a ba s''a obj'. \<lbrakk>\<forall>obj\<in>ran (ksPSpace s). valid_obj' obj s; P s; \<forall>ko. valid_obj' ko s \<longrightarrow> valid_obj' ko (s''a\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> obj')\<rparr>); a \<le> ptr; ksPSpace s a = Some ba; \<forall>z. a < z \<and> z \<le> ptr \<longrightarrow> ksPSpace s z = None; (obj', s''a) \<in> fst (updateObject val ba ptr a (snd (lookupAround2 ptr (ksPSpace s))) s)\<rbrakk> \<Longrightarrow> \<forall>obj\<in>ran ((ksPSpace s)(a \<mapsto> obj')). valid_obj' obj (s''a\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> obj')\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s a ba s''a obj' obj. \<lbrakk>\<forall>obj\<in>ran (ksPSpace s). valid_obj' obj s; P s; \<forall>ko. valid_obj' ko s \<longrightarrow> valid_obj' ko (s''a\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> obj')\<rparr>); a \<le> ptr; ksPSpace s a = Some ba; \<forall>z. a < z \<and> z \<le> ptr \<longrightarrow> ksPSpace s z = None; (obj', s''a) \<in> fst (updateObject val ba ptr a (snd (lookupAround2 ptr (ksPSpace s))) s); obj \<in> ran ((ksPSpace s)(a \<mapsto> obj'))\<rbrakk> \<Longrightarrow> valid_obj' obj (s''a\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> obj')\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s a ba s''a obj' obj. \<lbrakk>\<forall>obj\<in>ran (ksPSpace s). valid_obj' obj s; P s; a \<le> ptr; ksPSpace s a = Some ba; \<forall>z. a < z \<and> z \<le> ptr \<longrightarrow> ksPSpace s z = None; (obj', s''a) \<in> fst (updateObject val ba ptr a (snd (lookupAround2 ptr (ksPSpace s))) s); obj \<in> ran ((ksPSpace s)(a \<mapsto> obj'))\<rbrakk> \<Longrightarrow> valid_obj' obj s proof (prove)
goal (3 subgoals):
 1. \<And>s a ba s''a obj' obj. \<lbrakk>\<forall>obj\<in>ran (ksPSpace s). valid_obj' obj s; P s; a \<le> ptr; ksPSpace s a = Some ba; \<forall>z. a < z \<and> z \<le> ptr \<longrightarrow> ksPSpace s z = None; obj \<in> ran ((ksPSpace s)(a \<mapsto> obj'))\<rbrakk> \<Longrightarrow> valid_obj' ba s
 2. \<And>s a ba s''a obj' obj. \<lbrakk>\<forall>obj\<in>ran (ksPSpace s). valid_obj' obj s; P s; a \<le> ptr; ksPSpace s a = Some ba; \<forall>z. a < z \<and> z \<le> ptr \<longrightarrow> ksPSpace s z = None; obj \<in> ran ((ksPSpace s)(a \<mapsto> obj'))\<rbrakk> \<Longrightarrow> lookupAround2 ptr (ksPSpace s) = (Some (a, ba), snd (lookupAround2 ptr (ksPSpace s)))
 3. \<And>s a ba s''a obj' obj. \<lbrakk>\<forall>obj\<in>ran (ksPSpace s). valid_obj' obj s; P s; a \<le> ptr; ksPSpace s a = Some ba; \<forall>z. a < z \<and> z \<le> ptr \<longrightarrow> ksPSpace s z = None; obj \<in> ran ((ksPSpace s)(a \<mapsto> obj')); valid_obj' obj' s\<rbrakk> \<Longrightarrow> valid_obj' obj s proof (prove)
goal (2 subgoals):
 1. \<And>s a ba s''a obj' obj. \<lbrakk>\<forall>obj\<in>ran (ksPSpace s). valid_obj' obj s; P s; a \<le> ptr; ksPSpace s a = Some ba; \<forall>z. a < z \<and> z \<le> ptr \<longrightarrow> ksPSpace s z = None; obj \<in> ran ((ksPSpace s)(a \<mapsto> obj'))\<rbrakk> \<Longrightarrow> lookupAround2 ptr (ksPSpace s) = (Some (a, ba), snd (lookupAround2 ptr (ksPSpace s)))
 2. \<And>s a ba s''a obj' obj. \<lbrakk>\<forall>obj\<in>ran (ksPSpace s). valid_obj' obj s; P s; a \<le> ptr; ksPSpace s a = Some ba; \<forall>z. a < z \<and> z \<le> ptr \<longrightarrow> ksPSpace s z = None; obj \<in> ran ((ksPSpace s)(a \<mapsto> obj')); valid_obj' obj' s\<rbrakk> \<Longrightarrow> valid_obj' obj s proof (prove)
goal (1 subgoal):
 1. \<And>s a ba s''a obj' obj. \<lbrakk>\<forall>obj\<in>ran (ksPSpace s). valid_obj' obj s; P s; a \<le> ptr; ksPSpace s a = Some ba; \<forall>z. a < z \<and> z \<le> ptr \<longrightarrow> ksPSpace s z = None; obj \<in> ran ((ksPSpace s)(a \<mapsto> obj')); valid_obj' obj' s\<rbrakk> \<Longrightarrow> valid_obj' obj s proof (prove)
goal:
No subgoals!