theory Untyped_AI

lemma caps_of_state_no_overlapD:
  "\<lbrakk>caps_of_state s slot = Some cap; valid_objs s; pspace_aligned s;
    pspace_no_overlap S s\<rbrakk>
   \<Longrightarrow> (fst slot) \<notin> S" apply (drule caps_of_state_cteD) apply (clarsimp simp: cte_wp_at_cases obj_at_def
              simp del: atLeastAtMost_iff atLeastatMost_subset_iff
                        atLeastLessThan_iff Int_atLeastAtMost) apply (elim disjE) apply clarify apply (frule(2) p_in_obj_range) apply (erule(1) pspace_no_overlapE) apply (drule(1) IntI) unfolding obj_range_def apply (drule notemptyI)+ apply (simp add: Int_ac p_assoc_help
               del: atLeastAtMost_iff atLeastatMost_subset_iff
                    atLeastLessThan_iff Int_atLeastAtMost) apply clarify apply (frule(2) p_in_obj_range) apply (erule(1) pspace_no_overlapE) apply (drule(1) IntI) unfolding obj_range_def apply (drule notemptyI)+ apply (simp add: Int_ac p_assoc_help add.commute
              del: atLeastAtMost_iff atLeastatMost_subset_iff
         atLeastLessThan_iff Int_atLeastAtMost) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s slot = Some cap; valid_objs s; pspace_aligned s; pspace_no_overlap S s\<rbrakk> \<Longrightarrow> fst slot \<notin> S proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs s; pspace_aligned s; pspace_no_overlap S s; cte_wp_at ((=) cap) slot s\<rbrakk> \<Longrightarrow> fst slot \<notin> S proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs s; pspace_aligned s; pspace_no_overlap S s; (\<exists>sz fun. kheap s (fst slot) = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> fun (snd slot) = Some cap) \<or> (\<exists>tcb. kheap s (fst slot) = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases (snd slot) = Some (get, set, restr)) \<and> cap = get tcb)); fst slot \<in> S\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_objs s; pspace_aligned s; pspace_no_overlap S s; fst slot \<in> S; \<exists>sz fun. kheap s (fst slot) = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> fun (snd slot) = Some cap\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>valid_objs s; pspace_aligned s; pspace_no_overlap S s; fst slot \<in> S; \<exists>tcb. kheap s (fst slot) = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases (snd slot) = Some (get, set, restr)) \<and> cap = get tcb)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>sz fun. \<lbrakk>valid_objs s; pspace_aligned s; pspace_no_overlap S s; fst slot \<in> S; kheap s (fst slot) = Some (CNode sz fun); well_formed_cnode_n sz fun; fun (snd slot) = Some cap\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>valid_objs s; pspace_aligned s; pspace_no_overlap S s; fst slot \<in> S; \<exists>tcb. kheap s (fst slot) = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases (snd slot) = Some (get, set, restr)) \<and> cap = get tcb)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>sz fun. \<lbrakk>valid_objs s; pspace_aligned s; pspace_no_overlap S s; fst slot \<in> S; kheap s (fst slot) = Some (CNode sz fun); well_formed_cnode_n sz fun; fun (snd slot) = Some cap; fst slot \<in> obj_range (fst slot) (CNode sz fun)\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>valid_objs s; pspace_aligned s; pspace_no_overlap S s; fst slot \<in> S; \<exists>tcb. kheap s (fst slot) = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases (snd slot) = Some (get, set, restr)) \<and> cap = get tcb)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>sz fun. \<lbrakk>valid_objs s; pspace_aligned s; fst slot \<in> S; kheap s (fst slot) = Some (CNode sz fun); well_formed_cnode_n sz fun; fun (snd slot) = Some cap; fst slot \<in> obj_range (fst slot) (CNode sz fun); {fst slot..fst slot + (2 ^ obj_bits (CNode sz fun) - 1)} \<inter> S = {}\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>valid_objs s; pspace_aligned s; pspace_no_overlap S s; fst slot \<in> S; \<exists>tcb. kheap s (fst slot) = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases (snd slot) = Some (get, set, restr)) \<and> cap = get tcb)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>sz fun. \<lbrakk>valid_objs s; pspace_aligned s; kheap s (fst slot) = Some (CNode sz fun); well_formed_cnode_n sz fun; fun (snd slot) = Some cap; fst slot \<in> obj_range (fst slot) (CNode sz fun); {fst slot..fst slot + (2 ^ obj_bits (CNode sz fun) - 1)} \<inter> S = {}; fst slot \<in> S \<inter> obj_range (fst slot) (CNode sz fun)\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>valid_objs s; pspace_aligned s; pspace_no_overlap S s; fst slot \<in> S; \<exists>tcb. kheap s (fst slot) = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases (snd slot) = Some (get, set, restr)) \<and> cap = get tcb)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>sz fun. \<lbrakk>valid_objs s; pspace_aligned s; kheap s (fst slot) = Some (CNode sz fun); well_formed_cnode_n sz fun; fun (snd slot) = Some cap; fst slot \<in> {fst slot..fst slot + 2 ^ obj_bits (CNode sz fun) - 1}; {fst slot..fst slot + (2 ^ obj_bits (CNode sz fun) - 1)} \<inter> S = {}; fst slot \<in> S \<inter> {fst slot..fst slot + 2 ^ obj_bits (CNode sz fun) - 1}\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>valid_objs s; pspace_aligned s; pspace_no_overlap S s; fst slot \<in> S; \<exists>tcb. kheap s (fst slot) = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases (snd slot) = Some (get, set, restr)) \<and> cap = get tcb)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>sz fun. \<lbrakk>valid_objs s; pspace_aligned s; kheap s (fst slot) = Some (CNode sz fun); well_formed_cnode_n sz fun; fun (snd slot) = Some cap; {fst slot..fst slot + (2 ^ obj_bits (CNode sz fun) - 1)} \<inter> S = {}; {fst slot..fst slot + 2 ^ obj_bits (CNode sz fun) - 1} \<noteq> {}; S \<inter> {fst slot..fst slot + 2 ^ obj_bits (CNode sz fun) - 1} \<noteq> {}\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>valid_objs s; pspace_aligned s; pspace_no_overlap S s; fst slot \<in> S; \<exists>tcb. kheap s (fst slot) = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases (snd slot) = Some (get, set, restr)) \<and> cap = get tcb)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs s; pspace_aligned s; pspace_no_overlap S s; fst slot \<in> S; \<exists>tcb. kheap s (fst slot) = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases (snd slot) = Some (get, set, restr)) \<and> cap = get tcb)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>tcb get set restr. \<lbrakk>valid_objs s; pspace_aligned s; pspace_no_overlap S s; fst slot \<in> S; kheap s (fst slot) = Some (TCB tcb); cap = get tcb; tcb_cap_cases (snd slot) = Some (get, set, restr)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>tcb get set restr. \<lbrakk>valid_objs s; pspace_aligned s; pspace_no_overlap S s; fst slot \<in> S; kheap s (fst slot) = Some (TCB tcb); cap = get tcb; tcb_cap_cases (snd slot) = Some (get, set, restr); fst slot \<in> obj_range (fst slot) (TCB tcb)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>tcb get set restr. \<lbrakk>valid_objs s; pspace_aligned s; fst slot \<in> S; kheap s (fst slot) = Some (TCB tcb); cap = get tcb; tcb_cap_cases (snd slot) = Some (get, set, restr); fst slot \<in> obj_range (fst slot) (TCB tcb); {fst slot..fst slot + (2 ^ obj_bits (TCB tcb) - 1)} \<inter> S = {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>tcb get set restr. \<lbrakk>valid_objs s; pspace_aligned s; kheap s (fst slot) = Some (TCB tcb); cap = get tcb; tcb_cap_cases (snd slot) = Some (get, set, restr); fst slot \<in> obj_range (fst slot) (TCB tcb); {fst slot..fst slot + (2 ^ obj_bits (TCB tcb) - 1)} \<inter> S = {}; fst slot \<in> S \<inter> obj_range (fst slot) (TCB tcb)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>tcb get set restr. \<lbrakk>valid_objs s; pspace_aligned s; kheap s (fst slot) = Some (TCB tcb); cap = get tcb; tcb_cap_cases (snd slot) = Some (get, set, restr); fst slot \<in> {fst slot..fst slot + 2 ^ obj_bits (TCB tcb) - 1}; {fst slot..fst slot + (2 ^ obj_bits (TCB tcb) - 1)} \<inter> S = {}; fst slot \<in> S \<inter> {fst slot..fst slot + 2 ^ obj_bits (TCB tcb) - 1}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>tcb get set restr. \<lbrakk>valid_objs s; pspace_aligned s; kheap s (fst slot) = Some (TCB tcb); cap = get tcb; tcb_cap_cases (snd slot) = Some (get, set, restr); {fst slot..fst slot + (2 ^ obj_bits (TCB tcb) - 1)} \<inter> S = {}; {fst slot..fst slot + 2 ^ obj_bits (TCB tcb) - 1} \<noteq> {}; S \<inter> {fst slot..fst slot + 2 ^ obj_bits (TCB tcb) - 1} \<noteq> {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!