theory FinalCaps

lemma overlapping_slots_have_labelled_overlapping_caps:
  "\<lbrakk> slot \<in> slots_holding_overlapping_caps cap s; silc_inv aag st s;
     \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot)) \<rbrakk>
     \<Longrightarrow> (\<exists>lslot. lslot \<in> slots_holding_overlapping_caps cap s \<and>
                  pasObjectAbs aag (fst lslot) = SilcLabel)" apply (drule not_cap_points_to_label_transfers_across_overlapping_caps) apply assumption apply (frule slots_holding_overlapping_caps_hold_caps) apply (erule exE, rename_tac cap') apply (drule silc_invD) apply assumption apply assumption apply (blast dest: overlapping_transfers_across_overlapping_caps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>slot \<in> slots_holding_overlapping_caps cap s; silc_inv aag st s; \<not> cap_points_to_label aag cap (pasObjectAbs aag (fst slot))\<rbrakk> \<Longrightarrow> \<exists>lslot. lslot \<in> slots_holding_overlapping_caps cap s \<and> pasObjectAbs aag (fst lslot) = SilcLabel proof (prove)
goal (2 subgoals):
 1. \<lbrakk>slot \<in> slots_holding_overlapping_caps cap s; silc_inv aag st s\<rbrakk> \<Longrightarrow> slot \<in> slots_holding_overlapping_caps cap ?s
 2. \<lbrakk>slot \<in> slots_holding_overlapping_caps cap s; silc_inv aag st s; \<not> intra_label_cap aag slot ?s\<rbrakk> \<Longrightarrow> \<exists>lslot. lslot \<in> slots_holding_overlapping_caps cap s \<and> pasObjectAbs aag (fst lslot) = SilcLabel proof (prove)
goal (1 subgoal):
 1. \<lbrakk>slot \<in> slots_holding_overlapping_caps cap s; silc_inv aag st s; \<not> intra_label_cap aag slot s\<rbrakk> \<Longrightarrow> \<exists>lslot. lslot \<in> slots_holding_overlapping_caps cap s \<and> pasObjectAbs aag (fst lslot) = SilcLabel proof (prove)
goal (1 subgoal):
 1. \<lbrakk>slot \<in> slots_holding_overlapping_caps cap s; silc_inv aag st s; \<not> intra_label_cap aag slot s; \<exists>cap'. cte_wp_at ((=) cap') slot s\<rbrakk> \<Longrightarrow> \<exists>lslot. lslot \<in> slots_holding_overlapping_caps cap s \<and> pasObjectAbs aag (fst lslot) = SilcLabel proof (prove)
goal (1 subgoal):
 1. \<And>cap'. \<lbrakk>slot \<in> slots_holding_overlapping_caps cap s; silc_inv aag st s; \<not> intra_label_cap aag slot s; cte_wp_at ((=) cap') slot s\<rbrakk> \<Longrightarrow> \<exists>lslot. lslot \<in> slots_holding_overlapping_caps cap s \<and> pasObjectAbs aag (fst lslot) = SilcLabel proof (prove)
goal (3 subgoals):
 1. \<And>cap'. \<lbrakk>slot \<in> slots_holding_overlapping_caps cap s; \<not> intra_label_cap aag slot s; cte_wp_at ((=) cap') slot s\<rbrakk> \<Longrightarrow> cte_wp_at ((=) (?cap7 cap')) (?slot7 cap') s
 2. \<And>cap'. \<lbrakk>slot \<in> slots_holding_overlapping_caps cap s; \<not> intra_label_cap aag slot s; cte_wp_at ((=) cap') slot s\<rbrakk> \<Longrightarrow> \<not> intra_label_cap aag (?slot7 cap') s
 3. \<And>cap'. \<lbrakk>slot \<in> slots_holding_overlapping_caps cap s; \<not> intra_label_cap aag slot s; cte_wp_at ((=) cap') slot s; \<exists>lslot. lslot \<in> slots_holding_overlapping_caps (?cap7 cap') s \<and> pasObjectAbs aag (fst lslot) = SilcLabel\<rbrakk> \<Longrightarrow> \<exists>lslot. lslot \<in> slots_holding_overlapping_caps cap s \<and> pasObjectAbs aag (fst lslot) = SilcLabel proof (prove)
goal (2 subgoals):
 1. \<And>cap'. \<lbrakk>slot \<in> slots_holding_overlapping_caps cap s; \<not> intra_label_cap aag slot s; cte_wp_at ((=) cap') slot s\<rbrakk> \<Longrightarrow> \<not> intra_label_cap aag slot s
 2. \<And>cap'. \<lbrakk>slot \<in> slots_holding_overlapping_caps cap s; \<not> intra_label_cap aag slot s; cte_wp_at ((=) cap') slot s; \<exists>lslot. lslot \<in> slots_holding_overlapping_caps cap' s \<and> pasObjectAbs aag (fst lslot) = SilcLabel\<rbrakk> \<Longrightarrow> \<exists>lslot. lslot \<in> slots_holding_overlapping_caps cap s \<and> pasObjectAbs aag (fst lslot) = SilcLabel proof (prove)
goal (1 subgoal):
 1. \<And>cap'. \<lbrakk>slot \<in> slots_holding_overlapping_caps cap s; \<not> intra_label_cap aag slot s; cte_wp_at ((=) cap') slot s; \<exists>lslot. lslot \<in> slots_holding_overlapping_caps cap' s \<and> pasObjectAbs aag (fst lslot) = SilcLabel\<rbrakk> \<Longrightarrow> \<exists>lslot. lslot \<in> slots_holding_overlapping_caps cap s \<and> pasObjectAbs aag (fst lslot) = SilcLabel proof (prove)
goal:
No subgoals!