theory FinalCaps

lemma retype_region_cte_wp_at_other':
  "\<lbrace>cte_wp_at P slot and K ((fst slot) \<notin> set (retype_addrs ptr ty n us))\<rbrace>
   retype_region ptr n us ty dev
   \<lbrace>\<lambda>_. cte_wp_at P slot\<rbrace>" apply (rule hoare_gen_asm) apply (clarsimp simp: valid_def) apply (subst cte_wp_at_pspace') prefer 2 apply assumption apply (erule use_valid) apply (simp only: retype_region_def retype_addrs_def
                     foldr_upd_app_if fun_app_def K_bind_def) apply (wp modify_wp | simp)+ apply (clarsimp simp: not_less retype_addrs_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at P slot and K (fst slot \<notin> set (retype_addrs ptr ty n us))\<rbrace> retype_region ptr n us ty dev \<lbrace>\<lambda>_. cte_wp_at P slot\<rbrace> proof (prove)
goal (1 subgoal):
 1. fst slot \<notin> set (retype_addrs ptr ty n us) \<Longrightarrow> \<lbrace>cte_wp_at P slot\<rbrace> retype_region ptr n us ty dev \<lbrace>\<lambda>_. cte_wp_at P slot\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>fst slot \<notin> set (retype_addrs ptr ty n us); cte_wp_at P slot s; (a, b) \<in> fst (retype_region ptr n us ty dev s)\<rbrakk> \<Longrightarrow> cte_wp_at P slot b proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>fst slot \<notin> set (retype_addrs ptr ty n us); cte_wp_at P slot s; (a, b) \<in> fst (retype_region ptr n us ty dev s)\<rbrakk> \<Longrightarrow> kheap b (fst slot) = kheap (?s'9 s a b) (fst slot)
 2. \<And>s a b. \<lbrakk>fst slot \<notin> set (retype_addrs ptr ty n us); cte_wp_at P slot s; (a, b) \<in> fst (retype_region ptr n us ty dev s)\<rbrakk> \<Longrightarrow> cte_wp_at P slot (?s'9 s a b) proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>fst slot \<notin> set (retype_addrs ptr ty n us); cte_wp_at P slot s; (a, b) \<in> fst (retype_region ptr n us ty dev s)\<rbrakk> \<Longrightarrow> cte_wp_at P slot (?s'9 s a b)
 2. \<And>s a b. \<lbrakk>fst slot \<notin> set (retype_addrs ptr ty n us); cte_wp_at P slot s; (a, b) \<in> fst (retype_region ptr n us ty dev s)\<rbrakk> \<Longrightarrow> kheap b (fst slot) = kheap (?s'9 s a b) (fst slot) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>fst slot \<notin> set (retype_addrs ptr ty n us); cte_wp_at P slot s; (a, b) \<in> fst (retype_region ptr n us ty dev s)\<rbrakk> \<Longrightarrow> kheap b (fst slot) = kheap s (fst slot) proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>fst slot \<notin> set (retype_addrs ptr ty n us); cte_wp_at P slot s\<rbrakk> \<Longrightarrow> \<lbrace>?P10 s a b\<rbrace> retype_region ptr n us ty dev \<lbrace>\<lambda>a b. kheap b (fst slot) = kheap s (fst slot)\<rbrace>
 2. \<And>s a b. \<lbrakk>fst slot \<notin> set (retype_addrs ptr ty n us); cte_wp_at P slot s\<rbrakk> \<Longrightarrow> ?P10 s a b s proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>fst slot \<notin> set (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api ty us)) [0..<n]); cte_wp_at P slot s\<rbrakk> \<Longrightarrow> \<lbrace>?P10 s a b\<rbrace> do obj_size <- return (2 ^ obj_bits_api ty us);
ptrs <- return (map (\<lambda>p. ptr_add ptr (p * obj_size)) [0..<n]);
y <- when (ty \<noteq> Untyped) (do kh <- gets kheap;
kh' <- return (\<lambda>x. if x \<in> set ptrs then Some (default_object ty dev us) else kh x);
y <- do_extended_op (retype_region_ext ptrs ty);
modify (kheap_update (K kh'))
od);
return ptrs
od \<lbrace>\<lambda>a b. kheap b (fst slot) = kheap s (fst slot)\<rbrace>
 2. \<And>s a b. \<lbrakk>fst slot \<notin> set (retype_addrs ptr ty n us); cte_wp_at P slot s\<rbrakk> \<Longrightarrow> ?P10 s a b s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>fst slot \<notin> set (retype_addrs ptr ty n us); cte_wp_at P slot s\<rbrakk> \<Longrightarrow> fst slot \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api ty us)) ` {0..<n} \<longrightarrow> ty \<noteq> Untyped \<longrightarrow> Some (default_object ty dev us) = kheap s (fst slot) proof (prove)
goal:
No subgoals!