theory Retype_R

lemma createObjects_state_refs_of'':
  "\<lbrace>\<lambda>s. n \<noteq> 0
        \<and> range_cover ptr sz (objBitsKO val + gbits) n
        \<and> P (state_refs_of' s) \<and> refs_of' val = {}
        \<and> pspace_aligned' s \<and> pspace_distinct' s
        \<and> pspace_no_overlap' ptr sz s\<rbrace>
     createObjects' ptr n val gbits
   \<lbrace>\<lambda>rv s. P (state_refs_of' s)\<rbrace>" apply (clarsimp simp:valid_def lookupAround2_pspace_no state_refs_ko_wp_at_eq) apply (erule ssubst[where P = P,rotated]) apply (rule ext) apply (rule set_eqI) apply clarsimp apply (intro iffI,rule ccontr) apply (drule_tac P1="\<lambda>x. \<not> x" in use_valid[OF _ createObjects_orig_ko_wp_at2'[where sz = sz]]) apply simp apply (intro conjI) apply simp+ apply (drule_tac P1="\<lambda>x. x" in use_valid[OF _ createObjects_orig_ko_wp_at2'[where sz = sz]]) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. n \<noteq> 0 \<and> range_cover ptr sz (objBitsKO val + gbits) n \<and> P (state_refs_of' s) \<and> refs_of' val = {} \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s\<rbrace> createObjects' ptr n val gbits \<lbrace>\<lambda>rv s. P (state_refs_of' s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<lbrakk>((), b) \<in> fst (createObjects' ptr n val gbits s); 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; P (\<lambda>x. {r. ko_wp_at' (\<lambda>ko. r \<in> refs_of' ko) x s}); refs_of' val = {}; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s\<rbrakk> \<Longrightarrow> P (\<lambda>x. {r. ko_wp_at' (\<lambda>ko. r \<in> refs_of' ko) x b}) proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<lbrakk>((), b) \<in> fst (createObjects' ptr n val gbits s); 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; refs_of' val = {}; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s\<rbrakk> \<Longrightarrow> (\<lambda>x. {r. ko_wp_at' (\<lambda>ko. r \<in> refs_of' ko) x b}) = (\<lambda>x. {r. ko_wp_at' (\<lambda>ko. r \<in> refs_of' ko) x s}) proof (prove)
goal (1 subgoal):
 1. \<And>s b x. \<lbrakk>((), b) \<in> fst (createObjects' ptr n val gbits s); 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; refs_of' val = {}; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s\<rbrakk> \<Longrightarrow> {r. ko_wp_at' (\<lambda>ko. r \<in> refs_of' ko) x b} = {r. ko_wp_at' (\<lambda>ko. r \<in> refs_of' ko) x s} proof (prove)
goal (1 subgoal):
 1. \<And>s b x xa. \<lbrakk>((), b) \<in> fst (createObjects' ptr n val gbits s); 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; refs_of' val = {}; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s\<rbrakk> \<Longrightarrow> (xa \<in> {r. ko_wp_at' (\<lambda>ko. r \<in> refs_of' ko) x b}) = (xa \<in> {r. ko_wp_at' (\<lambda>ko. r \<in> refs_of' ko) x s}) proof (prove)
goal (1 subgoal):
 1. \<And>s b x a ba. \<lbrakk>((), b) \<in> fst (createObjects' ptr n val gbits s); 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; refs_of' val = {}; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s\<rbrakk> \<Longrightarrow> ko_wp_at' (\<lambda>ko. (a, ba) \<in> refs_of' ko) x b = ko_wp_at' (\<lambda>ko. (a, ba) \<in> refs_of' ko) x s proof (prove)
goal (2 subgoals):
 1. \<And>s b x a ba. \<lbrakk>((), b) \<in> fst (createObjects' ptr n val gbits s); 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; refs_of' val = {}; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ko_wp_at' (\<lambda>ko. (a, ba) \<in> refs_of' ko) x b; \<not> ko_wp_at' (\<lambda>ko. (a, ba) \<in> refs_of' ko) x s\<rbrakk> \<Longrightarrow> False
 2. \<And>s b x a ba. \<lbrakk>((), b) \<in> fst (createObjects' ptr n val gbits s); 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; refs_of' val = {}; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ko_wp_at' (\<lambda>ko. (a, ba) \<in> refs_of' ko) x s\<rbrakk> \<Longrightarrow> ko_wp_at' (\<lambda>ko. (a, ba) \<in> refs_of' ko) x b proof (prove)
goal (3 subgoals):
 1. \<And>s b x a ba. \<lbrakk>0 < n; range_cover ptr sz (objBitsKO val + gbits) n; refs_of' val = {}; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ko_wp_at' (\<lambda>ko. (a, ba) \<in> refs_of' ko) x b; \<not> ko_wp_at' (\<lambda>ko. (a, ba) \<in> refs_of' ko) x s\<rbrakk> \<Longrightarrow> range_cover ptr sz (objBitsKO val + gbits) n \<and> n \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> \<not> ko_wp_at' (?P'25 s b x a ba) (?p25 s b x a ba) s \<and> (?P'25 s b x a ba val \<longrightarrow> \<not> True) \<and> pspace_no_overlap' ptr sz s
 2. \<And>s b x a ba. \<lbrakk>0 < n; range_cover ptr sz (objBitsKO val + gbits) n; refs_of' val = {}; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ko_wp_at' (\<lambda>ko. (a, ba) \<in> refs_of' ko) x b; \<not> ko_wp_at' (\<lambda>ko. (a, ba) \<in> refs_of' ko) x s; \<not> ko_wp_at' (?P'25 s b x a ba) (?p25 s b x a ba) b\<rbrakk> \<Longrightarrow> False
 3. \<And>s b x a ba. \<lbrakk>((), b) \<in> fst (createObjects' ptr n val gbits s); 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; refs_of' val = {}; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ko_wp_at' (\<lambda>ko. (a, ba) \<in> refs_of' ko) x s\<rbrakk> \<Longrightarrow> ko_wp_at' (\<lambda>ko. (a, ba) \<in> refs_of' ko) x b proof (prove)
goal (3 subgoals):
 1. \<And>s b x a ba. \<lbrakk>0 < n; range_cover ptr sz (objBitsKO val + gbits) n; refs_of' val = {}; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ko_wp_at' (\<lambda>ko. (a, ba) \<in> refs_of' ko) x b; \<not> ko_wp_at' (\<lambda>ko. (a, ba) \<in> refs_of' ko) x s\<rbrakk> \<Longrightarrow> \<not> ko_wp_at' (?P'25 s b x a ba) (?p25 s b x a ba) s \<and> \<not> ?P'25 s b x a ba val
 2. \<And>s b x a ba. \<lbrakk>0 < n; range_cover ptr sz (objBitsKO val + gbits) n; refs_of' val = {}; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ko_wp_at' (\<lambda>ko. (a, ba) \<in> refs_of' ko) x b; \<not> ko_wp_at' (\<lambda>ko. (a, ba) \<in> refs_of' ko) x s; \<not> ko_wp_at' (?P'25 s b x a ba) (?p25 s b x a ba) b\<rbrakk> \<Longrightarrow> False
 3. \<And>s b x a ba. \<lbrakk>((), b) \<in> fst (createObjects' ptr n val gbits s); 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; refs_of' val = {}; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ko_wp_at' (\<lambda>ko. (a, ba) \<in> refs_of' ko) x s\<rbrakk> \<Longrightarrow> ko_wp_at' (\<lambda>ko. (a, ba) \<in> refs_of' ko) x b proof (prove)
goal (4 subgoals):
 1. \<And>s b x a ba. \<lbrakk>0 < n; range_cover ptr sz (objBitsKO val + gbits) n; refs_of' val = {}; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ko_wp_at' (\<lambda>ko. (a, ba) \<in> refs_of' ko) x b; \<not> ko_wp_at' (\<lambda>ko. (a, ba) \<in> refs_of' ko) x s\<rbrakk> \<Longrightarrow> \<not> ko_wp_at' (?P'25 s b x a ba) (?p25 s b x a ba) s
 2. \<And>s b x a ba. \<lbrakk>0 < n; range_cover ptr sz (objBitsKO val + gbits) n; refs_of' val = {}; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ko_wp_at' (\<lambda>ko. (a, ba) \<in> refs_of' ko) x b; \<not> ko_wp_at' (\<lambda>ko. (a, ba) \<in> refs_of' ko) x s\<rbrakk> \<Longrightarrow> \<not> ?P'25 s b x a ba val
 3. \<And>s b x a ba. \<lbrakk>0 < n; range_cover ptr sz (objBitsKO val + gbits) n; refs_of' val = {}; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ko_wp_at' (\<lambda>ko. (a, ba) \<in> refs_of' ko) x b; \<not> ko_wp_at' (\<lambda>ko. (a, ba) \<in> refs_of' ko) x s; \<not> ko_wp_at' (?P'25 s b x a ba) (?p25 s b x a ba) b\<rbrakk> \<Longrightarrow> False
 4. \<And>s b x a ba. \<lbrakk>((), b) \<in> fst (createObjects' ptr n val gbits s); 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; refs_of' val = {}; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ko_wp_at' (\<lambda>ko. (a, ba) \<in> refs_of' ko) x s\<rbrakk> \<Longrightarrow> ko_wp_at' (\<lambda>ko. (a, ba) \<in> refs_of' ko) x b proof (prove)
goal (1 subgoal):
 1. \<And>s b x a ba. \<lbrakk>((), b) \<in> fst (createObjects' ptr n val gbits s); 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; refs_of' val = {}; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ko_wp_at' (\<lambda>ko. (a, ba) \<in> refs_of' ko) x s\<rbrakk> \<Longrightarrow> ko_wp_at' (\<lambda>ko. (a, ba) \<in> refs_of' ko) x b proof (prove)
goal (2 subgoals):
 1. \<And>s b x a ba. \<lbrakk>0 < n; range_cover ptr sz (objBitsKO val + gbits) n; refs_of' val = {}; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ko_wp_at' (\<lambda>ko. (a, ba) \<in> refs_of' ko) x s\<rbrakk> \<Longrightarrow> range_cover ptr sz (objBitsKO val + gbits) n \<and> n \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> ko_wp_at' (?P'31 s b x a ba) (?p31 s b x a ba) s \<and> (?P'31 s b x a ba val \<longrightarrow> True) \<and> pspace_no_overlap' ptr sz s
 2. \<And>s b x a ba. \<lbrakk>0 < n; range_cover ptr sz (objBitsKO val + gbits) n; refs_of' val = {}; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ko_wp_at' (\<lambda>ko. (a, ba) \<in> refs_of' ko) x s; ko_wp_at' (?P'31 s b x a ba) (?p31 s b x a ba) b\<rbrakk> \<Longrightarrow> ko_wp_at' (\<lambda>ko. (a, ba) \<in> refs_of' ko) x b proof (prove)
goal:
No subgoals!