theory Retype_R

lemma foldr_update_ko_wp_at':
  assumes pv: "pspace_aligned' s" "pspace_distinct' s"
     and pv': "pspace_aligned' (ksPSpace_update (\<lambda>x xa. if xa \<in> set addrs then Some obj else ksPSpace s xa) s)"
              "pspace_distinct' (ksPSpace_update (\<lambda>x xa. if xa \<in> set addrs then Some obj else ksPSpace s xa) s)"
      and al: "\<forall>x \<in> set addrs. is_aligned x (objBitsKO obj)"
   shows
  "ko_wp_at' P p (ksPSpace_update (\<lambda>x xa. if xa \<in> set addrs then Some obj else ksPSpace s xa) s)
         = (if p \<in> set addrs then P obj
                         else ko_wp_at' P p s)"
  (is "ko_wp_at' P p ?s' = ?Q") apply (clarsimp simp: ko_wp_at'_def projectKOs al) apply (intro conjI impI) apply safe[1] apply (rule pspace_distinctD' [OF _ pv'(2)]) apply simp apply safe[1] apply (simp add: ps_clear_def dom_if_Some) apply blast apply simp apply (rule pspace_distinctD' [OF _ pv'(2)]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ko_wp_at' P p (s\<lparr>ksPSpace := \<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa\<rparr>) = (if p \<in> set addrs then P obj else ko_wp_at' P p s) proof (prove)
goal (1 subgoal):
 1. (p \<in> set addrs \<longrightarrow> (P obj \<and> ps_clear p (objBitsKO obj) (s\<lparr>ksPSpace := \<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa\<rparr>)) = P obj) \<and> (p \<notin> set addrs \<longrightarrow> (\<exists>ko. ksPSpace s p = Some ko \<and> is_aligned p (objBitsKO ko) \<and> P ko \<and> ps_clear p (objBitsKO ko) (s\<lparr>ksPSpace := \<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa\<rparr>)) = (\<exists>ko. ksPSpace s p = Some ko \<and> is_aligned p (objBitsKO ko) \<and> P ko \<and> ps_clear p (objBitsKO ko) s)) proof (prove)
goal (2 subgoals):
 1. p \<in> set addrs \<Longrightarrow> (P obj \<and> ps_clear p (objBitsKO obj) (s\<lparr>ksPSpace := \<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa\<rparr>)) = P obj
 2. p \<notin> set addrs \<Longrightarrow> (\<exists>ko. ksPSpace s p = Some ko \<and> is_aligned p (objBitsKO ko) \<and> P ko \<and> ps_clear p (objBitsKO ko) (s\<lparr>ksPSpace := \<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa\<rparr>)) = (\<exists>ko. ksPSpace s p = Some ko \<and> is_aligned p (objBitsKO ko) \<and> P ko \<and> ps_clear p (objBitsKO ko) s) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<in> set addrs; P obj\<rbrakk> \<Longrightarrow> ps_clear p (objBitsKO obj) (s\<lparr>ksPSpace := \<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa\<rparr>)
 2. p \<notin> set addrs \<Longrightarrow> (\<exists>ko. ksPSpace s p = Some ko \<and> is_aligned p (objBitsKO ko) \<and> P ko \<and> ps_clear p (objBitsKO ko) (s\<lparr>ksPSpace := \<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa\<rparr>)) = (\<exists>ko. ksPSpace s p = Some ko \<and> is_aligned p (objBitsKO ko) \<and> P ko \<and> ps_clear p (objBitsKO ko) s) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<in> set addrs; P obj\<rbrakk> \<Longrightarrow> ksPSpace (s\<lparr>ksPSpace := \<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa\<rparr>) p = Some obj
 2. p \<notin> set addrs \<Longrightarrow> (\<exists>ko. ksPSpace s p = Some ko \<and> is_aligned p (objBitsKO ko) \<and> P ko \<and> ps_clear p (objBitsKO ko) (s\<lparr>ksPSpace := \<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa\<rparr>)) = (\<exists>ko. ksPSpace s p = Some ko \<and> is_aligned p (objBitsKO ko) \<and> P ko \<and> ps_clear p (objBitsKO ko) s) proof (prove)
goal (1 subgoal):
 1. p \<notin> set addrs \<Longrightarrow> (\<exists>ko. ksPSpace s p = Some ko \<and> is_aligned p (objBitsKO ko) \<and> P ko \<and> ps_clear p (objBitsKO ko) (s\<lparr>ksPSpace := \<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa\<rparr>)) = (\<exists>ko. ksPSpace s p = Some ko \<and> is_aligned p (objBitsKO ko) \<and> P ko \<and> ps_clear p (objBitsKO ko) s) proof (prove)
goal (2 subgoals):
 1. \<And>ko. \<lbrakk>p \<notin> set addrs; ksPSpace s p = Some ko; is_aligned p (objBitsKO ko); P ko; ps_clear p (objBitsKO ko) (s\<lparr>ksPSpace := \<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa\<rparr>)\<rbrakk> \<Longrightarrow> \<exists>ko. ksPSpace s p = Some ko \<and> is_aligned p (objBitsKO ko) \<and> P ko \<and> ps_clear p (objBitsKO ko) s
 2. \<And>ko. \<lbrakk>p \<notin> set addrs; ksPSpace s p = Some ko; is_aligned p (objBitsKO ko); P ko; ps_clear p (objBitsKO ko) s\<rbrakk> \<Longrightarrow> \<exists>ko. ksPSpace s p = Some ko \<and> is_aligned p (objBitsKO ko) \<and> P ko \<and> ps_clear p (objBitsKO ko) (s\<lparr>ksPSpace := \<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>ko. \<lbrakk>p \<notin> set addrs; ksPSpace s p = Some ko; is_aligned p (objBitsKO ko); P ko; ({p..p + 2 ^ objBitsKO ko - 1} - {p}) \<inter> (set addrs \<union> dom (ksPSpace s)) = {}\<rbrakk> \<Longrightarrow> ({p..p + 2 ^ objBitsKO ko - 1} - {p}) \<inter> dom (ksPSpace s) = {}
 2. \<And>ko. \<lbrakk>p \<notin> set addrs; ksPSpace s p = Some ko; is_aligned p (objBitsKO ko); P ko; ps_clear p (objBitsKO ko) s\<rbrakk> \<Longrightarrow> \<exists>ko. ksPSpace s p = Some ko \<and> is_aligned p (objBitsKO ko) \<and> P ko \<and> ps_clear p (objBitsKO ko) (s\<lparr>ksPSpace := \<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>ko. \<lbrakk>p \<notin> set addrs; ksPSpace s p = Some ko; is_aligned p (objBitsKO ko); P ko; ps_clear p (objBitsKO ko) s\<rbrakk> \<Longrightarrow> \<exists>ko. ksPSpace s p = Some ko \<and> is_aligned p (objBitsKO ko) \<and> P ko \<and> ps_clear p (objBitsKO ko) (s\<lparr>ksPSpace := \<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>ko. \<lbrakk>p \<notin> set addrs; ksPSpace s p = Some ko; is_aligned p (objBitsKO ko); P ko; ps_clear p (objBitsKO ko) s\<rbrakk> \<Longrightarrow> ps_clear p (objBitsKO ko) (s\<lparr>ksPSpace := \<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>ko. \<lbrakk>p \<notin> set addrs; ksPSpace s p = Some ko; is_aligned p (objBitsKO ko); P ko; ps_clear p (objBitsKO ko) s\<rbrakk> \<Longrightarrow> ksPSpace (s\<lparr>ksPSpace := \<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa\<rparr>) p = Some ko proof (prove)
goal:
No subgoals!