theory Retype_R

lemma createObjects_cte_wp_at':
  "\<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; n \<noteq> 0\<rbrakk>
  \<Longrightarrow>\<lbrace>\<lambda>s. cte_wp_at' P p s \<and> valid_pspace' s \<and> pspace_no_overlap' ptr sz s\<rbrace>
  createObjects' ptr n val gbits
  \<lbrace>\<lambda>_. cte_wp_at' P p\<rbrace>" apply (clarsimp simp: valid_def cte_wp_at_obj_cases') apply (erule disjE) apply (erule use_valid[OF _ ]) apply (rule createObjects_orig_obj_at') apply fastforce apply clarsimp apply (drule_tac x = na in bspec) apply clarsimp apply clarsimp apply (drule use_valid[OF _ createObjects_orig_obj_at']) apply fastforce apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; n \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. cte_wp_at' P p s \<and> valid_pspace' s \<and> pspace_no_overlap' ptr sz s\<rbrace> createObjects' ptr n val gbits \<lbrace>\<lambda>_. cte_wp_at' P p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; ((), b) \<in> fst (createObjects' ptr n val gbits s); obj_at' P p s \<or> (\<exists>n\<in>dom tcb_cte_cases. obj_at' (P \<circ> fst (the (tcb_cte_cases n))) (p - n) s); valid_pspace' s; pspace_no_overlap' ptr sz s; \<forall>n\<in>dom tcb_cte_cases. \<not> obj_at' (P \<circ> fst (the (tcb_cte_cases n))) (p - n) b\<rbrakk> \<Longrightarrow> obj_at' P p b proof (prove)
goal (2 subgoals):
 1. \<And>s b. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; ((), b) \<in> fst (createObjects' ptr n val gbits s); valid_pspace' s; pspace_no_overlap' ptr sz s; \<forall>n\<in>dom tcb_cte_cases. \<not> obj_at' (P \<circ> fst (the (tcb_cte_cases n))) (p - n) b; obj_at' P p s\<rbrakk> \<Longrightarrow> obj_at' P p b
 2. \<And>s b. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; ((), b) \<in> fst (createObjects' ptr n val gbits s); valid_pspace' s; pspace_no_overlap' ptr sz s; \<forall>n\<in>dom tcb_cte_cases. \<not> obj_at' (P \<circ> fst (the (tcb_cte_cases n))) (p - n) b; \<exists>n\<in>dom tcb_cte_cases. obj_at' (P \<circ> fst (the (tcb_cte_cases n))) (p - n) s\<rbrakk> \<Longrightarrow> obj_at' P p b proof (prove)
goal (3 subgoals):
 1. \<And>s b. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; valid_pspace' s; pspace_no_overlap' ptr sz s; \<forall>n\<in>dom tcb_cte_cases. \<not> obj_at' (P \<circ> fst (the (tcb_cte_cases n))) (p - n) b; obj_at' P p s\<rbrakk> \<Longrightarrow> \<lbrace>?P17 s b\<rbrace> createObjects' ptr n val gbits \<lbrace>\<lambda>a. obj_at' P p\<rbrace>
 2. \<And>s b. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; valid_pspace' s; pspace_no_overlap' ptr sz s; \<forall>n\<in>dom tcb_cte_cases. \<not> obj_at' (P \<circ> fst (the (tcb_cte_cases n))) (p - n) b; obj_at' P p s\<rbrakk> \<Longrightarrow> ?P17 s b s
 3. \<And>s b. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; ((), b) \<in> fst (createObjects' ptr n val gbits s); valid_pspace' s; pspace_no_overlap' ptr sz s; \<forall>n\<in>dom tcb_cte_cases. \<not> obj_at' (P \<circ> fst (the (tcb_cte_cases n))) (p - n) b; \<exists>n\<in>dom tcb_cte_cases. obj_at' (P \<circ> fst (the (tcb_cte_cases n))) (p - n) s\<rbrakk> \<Longrightarrow> obj_at' P p b proof (prove)
goal (2 subgoals):
 1. \<And>s b. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; valid_pspace' s; pspace_no_overlap' ptr sz s; \<forall>n\<in>dom tcb_cte_cases. \<not> obj_at' (P \<circ> fst (the (tcb_cte_cases n))) (p - n) b; obj_at' P p s\<rbrakk> \<Longrightarrow> n \<noteq> 0 \<and> range_cover ptr (?sz21 s b) (objBitsKO val + gbits) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> obj_at' P p s \<and> pspace_no_overlap' ptr (?sz21 s b) s
 2. \<And>s b. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; ((), b) \<in> fst (createObjects' ptr n val gbits s); valid_pspace' s; pspace_no_overlap' ptr sz s; \<forall>n\<in>dom tcb_cte_cases. \<not> obj_at' (P \<circ> fst (the (tcb_cte_cases n))) (p - n) b; \<exists>n\<in>dom tcb_cte_cases. obj_at' (P \<circ> fst (the (tcb_cte_cases n))) (p - n) s\<rbrakk> \<Longrightarrow> obj_at' P p b proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; ((), b) \<in> fst (createObjects' ptr n val gbits s); valid_pspace' s; pspace_no_overlap' ptr sz s; \<forall>n\<in>dom tcb_cte_cases. \<not> obj_at' (P \<circ> fst (the (tcb_cte_cases n))) (p - n) b; \<exists>n\<in>dom tcb_cte_cases. obj_at' (P \<circ> fst (the (tcb_cte_cases n))) (p - n) s\<rbrakk> \<Longrightarrow> obj_at' P p b proof (prove)
goal (1 subgoal):
 1. \<And>s b na a ba. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; ((), b) \<in> fst (createObjects' ptr n val gbits s); valid_pspace' s; pspace_no_overlap' ptr sz s; \<forall>n\<in>dom tcb_cte_cases. \<not> obj_at' (P \<circ> fst (the (tcb_cte_cases n))) (p - n) b; obj_at' (P \<circ> a) (p - na) s; tcb_cte_cases na = Some (a, ba)\<rbrakk> \<Longrightarrow> obj_at' P p b proof (prove)
goal (2 subgoals):
 1. \<And>s b na a ba. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; ((), b) \<in> fst (createObjects' ptr n val gbits s); valid_pspace' s; pspace_no_overlap' ptr sz s; obj_at' (P \<circ> a) (p - na) s; tcb_cte_cases na = Some (a, ba)\<rbrakk> \<Longrightarrow> na \<in> dom tcb_cte_cases
 2. \<And>s b na a ba. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; ((), b) \<in> fst (createObjects' ptr n val gbits s); valid_pspace' s; pspace_no_overlap' ptr sz s; obj_at' (P \<circ> a) (p - na) s; tcb_cte_cases na = Some (a, ba); \<not> obj_at' (P \<circ> fst (the (tcb_cte_cases na))) (p - na) b\<rbrakk> \<Longrightarrow> obj_at' P p b proof (prove)
goal (1 subgoal):
 1. \<And>s b na a ba. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; ((), b) \<in> fst (createObjects' ptr n val gbits s); valid_pspace' s; pspace_no_overlap' ptr sz s; obj_at' (P \<circ> a) (p - na) s; tcb_cte_cases na = Some (a, ba); \<not> obj_at' (P \<circ> fst (the (tcb_cte_cases na))) (p - na) b\<rbrakk> \<Longrightarrow> obj_at' P p b proof (prove)
goal (1 subgoal):
 1. \<And>s b na a ba. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; ((), b) \<in> fst (createObjects' ptr n val gbits s); valid_pspace' s; pspace_no_overlap' ptr sz s; obj_at' (P \<circ> a) (p - na) s; tcb_cte_cases na = Some (a, ba); \<not> obj_at' (P \<circ> a) (p - na) b\<rbrakk> \<Longrightarrow> obj_at' P p b proof (prove)
goal (2 subgoals):
 1. \<And>s b na a ba. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; valid_pspace' s; pspace_no_overlap' ptr sz s; obj_at' (P \<circ> a) (p - na) s; tcb_cte_cases na = Some (a, ba); \<not> obj_at' (P \<circ> a) (p - na) b\<rbrakk> \<Longrightarrow> n \<noteq> 0 \<and> range_cover ptr (?sz42 s b na a ba) (objBitsKO val + gbits) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> obj_at' (?P42 s b na a ba) (?p42 s b na a ba) s \<and> pspace_no_overlap' ptr (?sz42 s b na a ba) s
 2. \<And>s b na a ba. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; valid_pspace' s; pspace_no_overlap' ptr sz s; obj_at' (P \<circ> a) (p - na) s; tcb_cte_cases na = Some (a, ba); \<not> obj_at' (P \<circ> a) (p - na) b; obj_at' (?P42 s b na a ba) (?p42 s b na a ba) b\<rbrakk> \<Longrightarrow> obj_at' P p b proof (prove)
goal (1 subgoal):
 1. \<And>s b na a ba. \<lbrakk>range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; valid_pspace' s; pspace_no_overlap' ptr sz s; obj_at' (P \<circ> a) (p - na) s; tcb_cte_cases na = Some (a, ba); \<not> obj_at' (P \<circ> a) (p - na) b; obj_at' (P \<circ> a) (p - na) b\<rbrakk> \<Longrightarrow> obj_at' P p b proof (prove)
goal:
No subgoals!