theory FinalCaps

lemma overlapping_transfers_across_overlapping_caps:
  "\<lbrakk> slot \<in> slots_holding_overlapping_caps cap s;
     cte_wp_at ((=) cap') slot s;
     lslot \<in> slots_holding_overlapping_caps cap' s \<rbrakk>
     \<Longrightarrow> lslot \<in> slots_holding_overlapping_caps cap s" apply (simp add: slots_holding_overlapping_caps_def get_cap_cte_wp_at') apply (elim exE conjE) apply (drule (1) cte_wp_at_eqD2)+ apply clarsimp apply (rename_tac lcap) apply (rule_tac x=lcap in exI) apply (auto dest: caps_ref_single_objects caps_ref_single_irqs caps_ref_either_an_object_or_irq) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>slot \<in> slots_holding_overlapping_caps cap s; cte_wp_at ((=) cap') slot s; lslot \<in> slots_holding_overlapping_caps cap' s\<rbrakk> \<Longrightarrow> lslot \<in> slots_holding_overlapping_caps cap s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<exists>cap'. cte_wp_at ((=) cap') slot s \<and> (obj_refs cap \<inter> obj_refs cap' = {} \<longrightarrow> cap_irqs cap \<inter> cap_irqs cap' \<noteq> {}); cte_wp_at ((=) cap') slot s; \<exists>cap'a. cte_wp_at ((=) cap'a) lslot s \<and> (obj_refs cap' \<inter> obj_refs cap'a = {} \<longrightarrow> cap_irqs cap' \<inter> cap_irqs cap'a \<noteq> {})\<rbrakk> \<Longrightarrow> \<exists>cap'. cte_wp_at ((=) cap') lslot s \<and> (obj_refs cap \<inter> obj_refs cap' = {} \<longrightarrow> cap_irqs cap \<inter> cap_irqs cap' \<noteq> {}) proof (prove)
goal (1 subgoal):
 1. \<And>cap'a cap'aa. \<lbrakk>cte_wp_at ((=) cap') slot s; cte_wp_at ((=) cap'a) slot s; obj_refs cap \<inter> obj_refs cap'a = {} \<longrightarrow> cap_irqs cap \<inter> cap_irqs cap'a \<noteq> {}; cte_wp_at ((=) cap'aa) lslot s; obj_refs cap' \<inter> obj_refs cap'aa = {} \<longrightarrow> cap_irqs cap' \<inter> cap_irqs cap'aa \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>cap'. cte_wp_at ((=) cap') lslot s \<and> (obj_refs cap \<inter> obj_refs cap' = {} \<longrightarrow> cap_irqs cap \<inter> cap_irqs cap' \<noteq> {}) proof (prove)
goal (1 subgoal):
 1. \<And>cap'a cap'aa. \<lbrakk>cte_wp_at ((=) cap'a) slot s; obj_refs cap \<inter> obj_refs cap'a = {} \<longrightarrow> cap_irqs cap \<inter> cap_irqs cap'a \<noteq> {}; cte_wp_at ((=) cap'aa) lslot s; obj_refs cap' \<inter> obj_refs cap'aa = {} \<longrightarrow> cap_irqs cap' \<inter> cap_irqs cap'aa \<noteq> {}; cap'a = cap'\<rbrakk> \<Longrightarrow> \<exists>cap'. cte_wp_at ((=) cap') lslot s \<and> (obj_refs cap \<inter> obj_refs cap' = {} \<longrightarrow> cap_irqs cap \<inter> cap_irqs cap' \<noteq> {}) proof (prove)
goal (1 subgoal):
 1. \<And>cap'a. \<lbrakk>cte_wp_at ((=) cap') slot s; obj_refs cap \<inter> obj_refs cap' = {} \<longrightarrow> cap_irqs cap \<inter> cap_irqs cap' \<noteq> {}; cte_wp_at ((=) cap'a) lslot s; obj_refs cap' \<inter> obj_refs cap'a = {} \<longrightarrow> cap_irqs cap' \<inter> cap_irqs cap'a \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>cap'. cte_wp_at ((=) cap') lslot s \<and> (obj_refs cap \<inter> obj_refs cap' = {} \<longrightarrow> cap_irqs cap \<inter> cap_irqs cap' \<noteq> {}) proof (prove)
goal (1 subgoal):
 1. \<And>lcap. \<lbrakk>cte_wp_at ((=) cap') slot s; obj_refs cap \<inter> obj_refs cap' = {} \<longrightarrow> cap_irqs cap \<inter> cap_irqs cap' \<noteq> {}; cte_wp_at ((=) lcap) lslot s; obj_refs cap' \<inter> obj_refs lcap = {} \<longrightarrow> cap_irqs cap' \<inter> cap_irqs lcap \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>cap'. cte_wp_at ((=) cap') lslot s \<and> (obj_refs cap \<inter> obj_refs cap' = {} \<longrightarrow> cap_irqs cap \<inter> cap_irqs cap' \<noteq> {}) proof (prove)
goal (1 subgoal):
 1. \<And>lcap. \<lbrakk>cte_wp_at ((=) cap') slot s; obj_refs cap \<inter> obj_refs cap' = {} \<longrightarrow> cap_irqs cap \<inter> cap_irqs cap' \<noteq> {}; cte_wp_at ((=) lcap) lslot s; obj_refs cap' \<inter> obj_refs lcap = {} \<longrightarrow> cap_irqs cap' \<inter> cap_irqs lcap \<noteq> {}\<rbrakk> \<Longrightarrow> cte_wp_at ((=) lcap) lslot s \<and> (obj_refs cap \<inter> obj_refs lcap = {} \<longrightarrow> cap_irqs cap \<inter> cap_irqs lcap \<noteq> {}) proof (prove)
goal:
No subgoals!