theory Retype_AC

lemma delete_objects_descendants_range_in'''':
  "\<lbrace>invs and (\<lambda> s :: det_ext state. \<exists>idx. cte_wp_at ((=) (UntypedCap dev word2 sz idx)) slot s) and
    ct_active and descendants_range_in {word2..word2 + 2 ^ sz - 1} slot and
    K (range_cover word2 sz bits n \<and> n \<noteq> 0)\<rbrace>
   delete_objects word2 sz
   \<lbrace>\<lambda>_. descendants_range_in {word2..word2 + of_nat n * 2 ^ bits - 1} slot\<rbrace>" apply (clarsimp simp: valid_def) apply (rule descendants_range_in_subseteq) apply (erule use_valid) apply (wp delete_objects_descendants_range_in' | clarsimp | blast)+ apply (drule range_cover_subset'', simp) apply (fastforce dest: untyped_cap_aligned) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and (\<lambda>s. \<exists>idx. cte_wp_at ((=) (UntypedCap dev word2 sz idx)) slot s) and ct_active and descendants_range_in {word2..word2 + 2 ^ sz - 1} slot and K (range_cover word2 sz bits n \<and> n \<noteq> 0)\<rbrace> delete_objects word2 sz \<lbrace>\<lambda>_. descendants_range_in {word2..word2 + word_of_nat n * 2 ^ bits - 1} slot\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s b idx. \<lbrakk>((), b) \<in> fst (delete_objects word2 sz s); invs s; cte_wp_at ((=) (UntypedCap dev word2 sz idx)) slot s; ct_active s; descendants_range_in {word2..word2 + 2 ^ sz - 1} slot s; range_cover word2 sz bits n; 0 < n\<rbrakk> \<Longrightarrow> descendants_range_in {word2..word2 + word_of_nat n * 2 ^ bits - 1} slot b proof (prove)
goal (2 subgoals):
 1. \<And>s b idx. \<lbrakk>((), b) \<in> fst (delete_objects word2 sz s); invs s; cte_wp_at ((=) (UntypedCap dev word2 sz idx)) slot s; ct_active s; descendants_range_in {word2..word2 + 2 ^ sz - 1} slot s; range_cover word2 sz bits n; 0 < n\<rbrakk> \<Longrightarrow> descendants_range_in (?A15 s b idx) slot b
 2. \<And>s b idx. \<lbrakk>((), b) \<in> fst (delete_objects word2 sz s); invs s; cte_wp_at ((=) (UntypedCap dev word2 sz idx)) slot s; ct_active s; descendants_range_in {word2..word2 + 2 ^ sz - 1} slot s; range_cover word2 sz bits n; 0 < n\<rbrakk> \<Longrightarrow> {word2..word2 + word_of_nat n * 2 ^ bits - 1} \<subseteq> ?A15 s b idx proof (prove)
goal (3 subgoals):
 1. \<And>s b idx. \<lbrakk>invs s; cte_wp_at ((=) (UntypedCap dev word2 sz idx)) slot s; ct_active s; descendants_range_in {word2..word2 + 2 ^ sz - 1} slot s; range_cover word2 sz bits n; 0 < n\<rbrakk> \<Longrightarrow> \<lbrace>?P18 s b idx\<rbrace> delete_objects word2 sz \<lbrace>\<lambda>a c. descendants_range_in (?A19 s b idx a c) slot c\<rbrace>
 2. \<And>s b idx. \<lbrakk>invs s; cte_wp_at ((=) (UntypedCap dev word2 sz idx)) slot s; ct_active s; descendants_range_in {word2..word2 + 2 ^ sz - 1} slot s; range_cover word2 sz bits n; 0 < n\<rbrakk> \<Longrightarrow> ?P18 s b idx s
 3. \<And>s b idx. \<lbrakk>((), b) \<in> fst (delete_objects word2 sz s); invs s; cte_wp_at ((=) (UntypedCap dev word2 sz idx)) slot s; ct_active s; descendants_range_in {word2..word2 + 2 ^ sz - 1} slot s; range_cover word2 sz bits n; 0 < n\<rbrakk> \<Longrightarrow> {word2..word2 + word_of_nat n * 2 ^ bits - 1} \<subseteq> ?A19 s b idx () b proof (prove)
goal (1 subgoal):
 1. \<And>s b idx. \<lbrakk>((), b) \<in> fst (delete_objects word2 sz s); invs s; cte_wp_at ((=) (UntypedCap dev word2 sz idx)) slot s; ct_active s; descendants_range_in {word2..word2 + 2 ^ sz - 1} slot s; range_cover word2 sz bits n; 0 < n; word2 \<le> word2 + word_of_nat n * 2 ^ bits - 1\<rbrakk> \<Longrightarrow> word2 + word_of_nat n * 2 ^ bits - 1 \<le> word2 + 2 ^ sz - 1 proof (prove)
goal (1 subgoal):
 1. \<And>s b idx. \<lbrakk>((), b) \<in> fst (delete_objects word2 sz s); invs s; cte_wp_at ((=) (UntypedCap dev word2 sz idx)) slot s; ct_active s; descendants_range_in {word2..word2 + 2 ^ sz - 1} slot s; 0 < n; word2 \<le> word2 + word_of_nat n * 2 ^ bits - 1; {word2..word2 + word_of_nat n * 2 ^ bits - 1} \<subseteq> {word2 && ~~ mask sz..(word2 && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> word2 + word_of_nat n * 2 ^ bits - 1 \<le> word2 + 2 ^ sz - 1 proof (prove)
goal:
No subgoals!