theory FinalCaps

lemma silc_inv_preserves_silc_dom_caps:
  "\<lbrakk> silc_inv aag st s; silc_inv aag st s';
     pasObjectAbs aag (fst lslot) = SilcLabel;
     lslot \<in> FinalCaps.slots_holding_overlapping_caps cap s \<rbrakk>
     \<Longrightarrow> lslot \<in> FinalCaps.slots_holding_overlapping_caps cap s'" apply (clarsimp simp: slots_holding_overlapping_caps_def get_cap_cte_wp_at') apply (rule_tac x=cap' in exI) apply simp apply (subst (asm) cte_wp_at_pspace'[where s'=s']) apply (fastforce simp: silc_inv_def silc_dom_equiv_def equiv_for_def) apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>silc_inv aag st s; silc_inv aag st s'; pasObjectAbs aag (fst lslot) = SilcLabel; lslot \<in> slots_holding_overlapping_caps cap s\<rbrakk> \<Longrightarrow> lslot \<in> slots_holding_overlapping_caps cap s' proof (prove)
goal (1 subgoal):
 1. \<And>cap'. \<lbrakk>silc_inv aag st s; silc_inv aag st s'; pasObjectAbs aag (fst lslot) = SilcLabel; cte_wp_at ((=) cap') lslot s; cap_irqs cap \<inter> cap_irqs cap' = {} \<longrightarrow> obj_refs cap \<inter> obj_refs cap' = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs cap' \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>cap'. cte_wp_at ((=) cap') lslot s' \<and> (cap_irqs cap \<inter> cap_irqs cap' = {} \<longrightarrow> obj_refs cap \<inter> obj_refs cap' = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs cap' \<noteq> {}) proof (prove)
goal (1 subgoal):
 1. \<And>cap'. \<lbrakk>silc_inv aag st s; silc_inv aag st s'; pasObjectAbs aag (fst lslot) = SilcLabel; cte_wp_at ((=) cap') lslot s; cap_irqs cap \<inter> cap_irqs cap' = {} \<longrightarrow> obj_refs cap \<inter> obj_refs cap' = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs cap' \<noteq> {}\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap') lslot s' \<and> (cap_irqs cap \<inter> cap_irqs cap' = {} \<longrightarrow> obj_refs cap \<inter> obj_refs cap' = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs cap' \<noteq> {}) proof (prove)
goal (1 subgoal):
 1. \<And>cap'. \<lbrakk>silc_inv aag st s; silc_inv aag st s'; pasObjectAbs aag (fst lslot) = SilcLabel; cte_wp_at ((=) cap') lslot s; cap_irqs cap \<inter> cap_irqs cap' = {} \<longrightarrow> obj_refs cap \<inter> obj_refs cap' = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs cap' \<noteq> {}\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap') lslot s' proof (prove)
goal (2 subgoals):
 1. \<And>cap'. \<lbrakk>cap_irqs cap \<inter> cap_irqs cap' = {} \<longrightarrow> obj_refs cap \<inter> obj_refs cap' = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs cap' \<noteq> {}; silc_inv aag st s; silc_inv aag st s'; pasObjectAbs aag (fst lslot) = SilcLabel\<rbrakk> \<Longrightarrow> kheap s (fst lslot) = kheap s' (fst lslot)
 2. \<And>cap'. \<lbrakk>silc_inv aag st s; silc_inv aag st s'; pasObjectAbs aag (fst lslot) = SilcLabel; cte_wp_at ((=) cap') lslot s'; cap_irqs cap \<inter> cap_irqs cap' = {} \<longrightarrow> obj_refs cap \<inter> obj_refs cap' = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs cap' \<noteq> {}\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap') lslot s' proof (prove)
goal (1 subgoal):
 1. \<And>cap'. \<lbrakk>silc_inv aag st s; silc_inv aag st s'; pasObjectAbs aag (fst lslot) = SilcLabel; cte_wp_at ((=) cap') lslot s'; cap_irqs cap \<inter> cap_irqs cap' = {} \<longrightarrow> obj_refs cap \<inter> obj_refs cap' = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs cap' \<noteq> {}\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap') lslot s' proof (prove)
goal:
No subgoals!