theory Invariants_AI

lemma typ_at_range:
  "\<lbrakk> typ_at T p s; pspace_aligned s; valid_objs s \<rbrakk> \<Longrightarrow> typ_range p T \<noteq> {}" apply (erule (1) obj_at_valid_objsE) apply (clarsimp simp: pspace_aligned_def) apply (drule bspec) apply blast apply clarsimp apply (case_tac ko) apply (clarsimp simp: a_type_def split: if_split_asm) apply (clarsimp simp: typ_range_def obj_bits_type_def) apply (erule notE) apply (erule is_aligned_no_overflow) apply (clarsimp simp: valid_obj_def valid_cs_def valid_cs_size_def) apply (auto simp: a_type_def typ_range_def  obj_bits_type_def
                        aobj_bits_T
                  dest!: is_aligned_no_overflow
               | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>typ_at T p s; pspace_aligned s; valid_objs s\<rbrakk> \<Longrightarrow> typ_range p T \<noteq> {} proof (prove)
goal (1 subgoal):
 1. \<And>ko. \<lbrakk>pspace_aligned s; valid_objs s; kheap s p = Some ko; a_type ko = T; valid_obj p ko s\<rbrakk> \<Longrightarrow> typ_range p T \<noteq> {} proof (prove)
goal (1 subgoal):
 1. \<And>ko. \<lbrakk>\<forall>x\<in>dom (kheap s). is_aligned x (obj_bits (the (kheap s x))); valid_objs s; kheap s p = Some ko; valid_obj p ko s; T = a_type ko; typ_range p (a_type ko) = {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>ko. \<lbrakk>valid_objs s; kheap s p = Some ko; valid_obj p ko s; T = a_type ko; typ_range p (a_type ko) = {}\<rbrakk> \<Longrightarrow> ?x7 ko \<in> dom (kheap s)
 2. \<And>ko. \<lbrakk>valid_objs s; kheap s p = Some ko; valid_obj p ko s; T = a_type ko; typ_range p (a_type ko) = {}; is_aligned (?x7 ko) (obj_bits (the (kheap s (?x7 ko))))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>ko. \<lbrakk>valid_objs s; kheap s p = Some ko; valid_obj p ko s; T = a_type ko; typ_range p (a_type ko) = {}; is_aligned p (obj_bits (the (kheap s p)))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>ko. \<lbrakk>valid_objs s; kheap s p = Some ko; valid_obj p ko s; T = a_type ko; typ_range p (a_type ko) = {}; is_aligned p (obj_bits ko)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (5 subgoals):
 1. \<And>ko x11 x12. \<lbrakk>valid_objs s; kheap s p = Some ko; valid_obj p ko s; T = a_type ko; typ_range p (a_type ko) = {}; is_aligned p (obj_bits ko); ko = CNode x11 x12\<rbrakk> \<Longrightarrow> False
 2. \<And>ko x2. \<lbrakk>valid_objs s; kheap s p = Some ko; valid_obj p ko s; T = a_type ko; typ_range p (a_type ko) = {}; is_aligned p (obj_bits ko); ko = TCB x2\<rbrakk> \<Longrightarrow> False
 3. \<And>ko x3. \<lbrakk>valid_objs s; kheap s p = Some ko; valid_obj p ko s; T = a_type ko; typ_range p (a_type ko) = {}; is_aligned p (obj_bits ko); ko = Endpoint x3\<rbrakk> \<Longrightarrow> False
 4. \<And>ko x4. \<lbrakk>valid_objs s; kheap s p = Some ko; valid_obj p ko s; T = a_type ko; typ_range p (a_type ko) = {}; is_aligned p (obj_bits ko); ko = Notification x4\<rbrakk> \<Longrightarrow> False
 5. \<And>ko x5. \<lbrakk>valid_objs s; kheap s p = Some ko; valid_obj p ko s; T = a_type ko; typ_range p (a_type ko) = {}; is_aligned p (obj_bits ko); ko = ArchObj x5\<rbrakk> \<Longrightarrow> False proof (prove)
goal (6 subgoals):
 1. \<And>x11 x12. \<lbrakk>typ_range p (ACapTable x11) = {}; is_aligned p (cte_level_bits + x11); valid_objs s; kheap s p = Some (CNode x11 x12); valid_obj p (CNode x11 x12) s; well_formed_cnode_n x11 x12; T = ACapTable x11\<rbrakk> \<Longrightarrow> False
 2. \<And>x11 x12. \<lbrakk>typ_range p (AGarbage (cte_level_bits + x11)) = {}; is_aligned p (cte_level_bits + x11); valid_objs s; kheap s p = Some (CNode x11 x12); valid_obj p (CNode x11 x12) s; \<not> well_formed_cnode_n x11 x12; T = AGarbage (cte_level_bits + x11)\<rbrakk> \<Longrightarrow> False
 3. \<And>ko x2. \<lbrakk>valid_objs s; kheap s p = Some ko; valid_obj p ko s; T = a_type ko; typ_range p (a_type ko) = {}; is_aligned p (obj_bits ko); ko = TCB x2\<rbrakk> \<Longrightarrow> False
 4. \<And>ko x3. \<lbrakk>valid_objs s; kheap s p = Some ko; valid_obj p ko s; T = a_type ko; typ_range p (a_type ko) = {}; is_aligned p (obj_bits ko); ko = Endpoint x3\<rbrakk> \<Longrightarrow> False
 5. \<And>ko x4. \<lbrakk>valid_objs s; kheap s p = Some ko; valid_obj p ko s; T = a_type ko; typ_range p (a_type ko) = {}; is_aligned p (obj_bits ko); ko = Notification x4\<rbrakk> \<Longrightarrow> False
 6. \<And>ko x5. \<lbrakk>valid_objs s; kheap s p = Some ko; valid_obj p ko s; T = a_type ko; typ_range p (a_type ko) = {}; is_aligned p (obj_bits ko); ko = ArchObj x5\<rbrakk> \<Longrightarrow> False proof (prove)
goal (6 subgoals):
 1. \<And>x11 x12. \<lbrakk>\<not> p \<le> p + 2 ^ (cte_level_bits + x11) - 1; is_aligned p (cte_level_bits + x11); valid_objs s; kheap s p = Some (CNode x11 x12); valid_obj p (CNode x11 x12) s; well_formed_cnode_n x11 x12; T = ACapTable x11\<rbrakk> \<Longrightarrow> False
 2. \<And>x11 x12. \<lbrakk>typ_range p (AGarbage (cte_level_bits + x11)) = {}; is_aligned p (cte_level_bits + x11); valid_objs s; kheap s p = Some (CNode x11 x12); valid_obj p (CNode x11 x12) s; \<not> well_formed_cnode_n x11 x12; T = AGarbage (cte_level_bits + x11)\<rbrakk> \<Longrightarrow> False
 3. \<And>ko x2. \<lbrakk>valid_objs s; kheap s p = Some ko; valid_obj p ko s; T = a_type ko; typ_range p (a_type ko) = {}; is_aligned p (obj_bits ko); ko = TCB x2\<rbrakk> \<Longrightarrow> False
 4. \<And>ko x3. \<lbrakk>valid_objs s; kheap s p = Some ko; valid_obj p ko s; T = a_type ko; typ_range p (a_type ko) = {}; is_aligned p (obj_bits ko); ko = Endpoint x3\<rbrakk> \<Longrightarrow> False
 5. \<And>ko x4. \<lbrakk>valid_objs s; kheap s p = Some ko; valid_obj p ko s; T = a_type ko; typ_range p (a_type ko) = {}; is_aligned p (obj_bits ko); ko = Notification x4\<rbrakk> \<Longrightarrow> False
 6. \<And>ko x5. \<lbrakk>valid_objs s; kheap s p = Some ko; valid_obj p ko s; T = a_type ko; typ_range p (a_type ko) = {}; is_aligned p (obj_bits ko); ko = ArchObj x5\<rbrakk> \<Longrightarrow> False proof (prove)
goal (6 subgoals):
 1. \<And>x11 x12. \<lbrakk>is_aligned p (cte_level_bits + x11); valid_objs s; kheap s p = Some (CNode x11 x12); valid_obj p (CNode x11 x12) s; well_formed_cnode_n x11 x12; T = ACapTable x11\<rbrakk> \<Longrightarrow> p \<le> p + 2 ^ (cte_level_bits + x11) - 1
 2. \<And>x11 x12. \<lbrakk>typ_range p (AGarbage (cte_level_bits + x11)) = {}; is_aligned p (cte_level_bits + x11); valid_objs s; kheap s p = Some (CNode x11 x12); valid_obj p (CNode x11 x12) s; \<not> well_formed_cnode_n x11 x12; T = AGarbage (cte_level_bits + x11)\<rbrakk> \<Longrightarrow> False
 3. \<And>ko x2. \<lbrakk>valid_objs s; kheap s p = Some ko; valid_obj p ko s; T = a_type ko; typ_range p (a_type ko) = {}; is_aligned p (obj_bits ko); ko = TCB x2\<rbrakk> \<Longrightarrow> False
 4. \<And>ko x3. \<lbrakk>valid_objs s; kheap s p = Some ko; valid_obj p ko s; T = a_type ko; typ_range p (a_type ko) = {}; is_aligned p (obj_bits ko); ko = Endpoint x3\<rbrakk> \<Longrightarrow> False
 5. \<And>ko x4. \<lbrakk>valid_objs s; kheap s p = Some ko; valid_obj p ko s; T = a_type ko; typ_range p (a_type ko) = {}; is_aligned p (obj_bits ko); ko = Notification x4\<rbrakk> \<Longrightarrow> False
 6. \<And>ko x5. \<lbrakk>valid_objs s; kheap s p = Some ko; valid_obj p ko s; T = a_type ko; typ_range p (a_type ko) = {}; is_aligned p (obj_bits ko); ko = ArchObj x5\<rbrakk> \<Longrightarrow> False proof (prove)
goal (5 subgoals):
 1. \<And>x11 x12. \<lbrakk>typ_range p (AGarbage (cte_level_bits + x11)) = {}; is_aligned p (cte_level_bits + x11); valid_objs s; kheap s p = Some (CNode x11 x12); valid_obj p (CNode x11 x12) s; \<not> well_formed_cnode_n x11 x12; T = AGarbage (cte_level_bits + x11)\<rbrakk> \<Longrightarrow> False
 2. \<And>ko x2. \<lbrakk>valid_objs s; kheap s p = Some ko; valid_obj p ko s; T = a_type ko; typ_range p (a_type ko) = {}; is_aligned p (obj_bits ko); ko = TCB x2\<rbrakk> \<Longrightarrow> False
 3. \<And>ko x3. \<lbrakk>valid_objs s; kheap s p = Some ko; valid_obj p ko s; T = a_type ko; typ_range p (a_type ko) = {}; is_aligned p (obj_bits ko); ko = Endpoint x3\<rbrakk> \<Longrightarrow> False
 4. \<And>ko x4. \<lbrakk>valid_objs s; kheap s p = Some ko; valid_obj p ko s; T = a_type ko; typ_range p (a_type ko) = {}; is_aligned p (obj_bits ko); ko = Notification x4\<rbrakk> \<Longrightarrow> False
 5. \<And>ko x5. \<lbrakk>valid_objs s; kheap s p = Some ko; valid_obj p ko s; T = a_type ko; typ_range p (a_type ko) = {}; is_aligned p (obj_bits ko); ko = ArchObj x5\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>ko x2. \<lbrakk>valid_objs s; kheap s p = Some ko; valid_obj p ko s; T = a_type ko; typ_range p (a_type ko) = {}; is_aligned p (obj_bits ko); ko = TCB x2\<rbrakk> \<Longrightarrow> False
 2. \<And>ko x3. \<lbrakk>valid_objs s; kheap s p = Some ko; valid_obj p ko s; T = a_type ko; typ_range p (a_type ko) = {}; is_aligned p (obj_bits ko); ko = Endpoint x3\<rbrakk> \<Longrightarrow> False
 3. \<And>ko x4. \<lbrakk>valid_objs s; kheap s p = Some ko; valid_obj p ko s; T = a_type ko; typ_range p (a_type ko) = {}; is_aligned p (obj_bits ko); ko = Notification x4\<rbrakk> \<Longrightarrow> False
 4. \<And>ko x5. \<lbrakk>valid_objs s; kheap s p = Some ko; valid_obj p ko s; T = a_type ko; typ_range p (a_type ko) = {}; is_aligned p (obj_bits ko); ko = ArchObj x5\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!