theory FinalCaps

lemma set_cap_slots_holding_overlapping_caps_helper:
  "\<lbrakk> x \<in> slots_holding_overlapping_caps cap s; fst x \<noteq> fst slot;
     obj_refs cap = {} \<longrightarrow> cap_irqs cap \<noteq> {};
     ko_at (TCB tcb) (fst slot) s; tcb_cap_cases (snd slot) = Some (getF, setF, blah) \<rbrakk>
     \<Longrightarrow> x \<in> slots_holding_overlapping_caps cap
               (s\<lparr>kheap := (kheap s)(fst slot \<mapsto> TCB (setF (\<lambda>x. capa) tcb))\<rparr>)" apply (clarsimp simp: slots_holding_overlapping_caps_def) apply (rule_tac x=cap' in exI) apply (clarsimp simp: get_cap_cte_wp_at') apply (erule (1) upd_other_cte_wp_at) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> slots_holding_overlapping_caps cap s; fst x \<noteq> fst slot; obj_refs cap = {} \<longrightarrow> cap_irqs cap \<noteq> {}; ko_at (TCB tcb) (fst slot) s; tcb_cap_cases (snd slot) = Some (getF, setF, blah)\<rbrakk> \<Longrightarrow> x \<in> slots_holding_overlapping_caps cap (s\<lparr>kheap := (kheap s)(fst slot \<mapsto> TCB (setF (\<lambda>x. capa) tcb))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>cap'. \<lbrakk>fst x \<noteq> fst slot; obj_refs cap = {} \<longrightarrow> cap_irqs cap \<noteq> {}; ko_at (TCB tcb) (fst slot) s; tcb_cap_cases (snd slot) = Some (getF, setF, blah); fst (get_cap x s) = {(cap', 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'. fst (get_cap x (s\<lparr>kheap := (kheap s)(fst slot \<mapsto> TCB (setF (\<lambda>x. capa) tcb))\<rparr>)) = {(cap', s\<lparr>kheap := (kheap s)(fst slot \<mapsto> TCB (setF (\<lambda>x. capa) tcb))\<rparr>)} \<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>fst x \<noteq> fst slot; obj_refs cap = {} \<longrightarrow> cap_irqs cap \<noteq> {}; ko_at (TCB tcb) (fst slot) s; tcb_cap_cases (snd slot) = Some (getF, setF, blah); fst (get_cap x s) = {(cap', 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> fst (get_cap x (s\<lparr>kheap := (kheap s)(fst slot \<mapsto> TCB (setF (\<lambda>x. capa) tcb))\<rparr>)) = {(cap', s\<lparr>kheap := (kheap s)(fst slot \<mapsto> TCB (setF (\<lambda>x. capa) tcb))\<rparr>)} \<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>fst x \<noteq> fst slot; obj_refs cap = {} \<longrightarrow> cap_irqs cap \<noteq> {}; ko_at (TCB tcb) (fst slot) s; tcb_cap_cases (snd slot) = Some (getF, setF, blah); cte_wp_at ((=) cap') x 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') x (s\<lparr>kheap := (kheap s)(fst slot \<mapsto> TCB (setF (\<lambda>x. capa) tcb))\<rparr>) proof (prove)
goal:
No subgoals!