theory FinalCaps

lemma slots_holding_overlapping_caps_lift:
  assumes a: "\<And>P Q slot. \<lbrace>\<lambda>s. Q (cte_wp_at P slot s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (cte_wp_at P slot s)\<rbrace>"
  shows "\<lbrace>\<lambda>s. P (slots_holding_overlapping_caps cap s)\<rbrace>
         f
         \<lbrace>\<lambda>_ s. P (slots_holding_overlapping_caps cap s)\<rbrace>" apply (clarsimp simp: valid_def) apply (subgoal_tac "slots_holding_overlapping_caps cap b =
                      slots_holding_overlapping_caps cap s", simp) apply (clarsimp simp: slots_holding_overlapping_caps_def2 ctes_wp_at_def) apply (rule Collect_cong) apply (erule use_valid[OF _ a]) apply (rule refl) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (slots_holding_overlapping_caps cap s)\<rbrace> f \<lbrace>\<lambda>_ s. P (slots_holding_overlapping_caps cap s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>P (slots_holding_overlapping_caps cap s); (a, b) \<in> fst (f s)\<rbrakk> \<Longrightarrow> P (slots_holding_overlapping_caps cap b) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>P (slots_holding_overlapping_caps cap s); (a, b) \<in> fst (f s)\<rbrakk> \<Longrightarrow> slots_holding_overlapping_caps cap b = slots_holding_overlapping_caps cap s proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>P {ptr. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) ptr s}; (a, b) \<in> fst (f s)\<rbrakk> \<Longrightarrow> {ptr. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) ptr b} = {ptr. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) ptr s} proof (prove)
goal (1 subgoal):
 1. \<And>s a b ptr. \<lbrakk>P {ptr. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) ptr s}; (a, b) \<in> fst (f s)\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) ptr b = cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) ptr s proof (prove)
goal (1 subgoal):
 1. \<And>s a b ptr. P {ptr. cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) ptr s} \<Longrightarrow> cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) ptr s = cte_wp_at (\<lambda>c. cap_irqs cap \<inter> cap_irqs c = {} \<longrightarrow> obj_refs cap \<inter> obj_refs c = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) ptr s proof (prove)
goal:
No subgoals!