theory FinalCaps

lemma not_is_final_cap_caps_of_stateE:
  assumes hyp: "\<not> is_final_cap' cap s" "caps_of_state s slot = Some cap" "gen_obj_refs cap \<noteq> {}"
  obtains slot' where "slot' \<noteq> slot" "slot' \<in> slots_holding_overlapping_caps cap s" using hyp apply (simp add: is_final_cap'_def4) apply (subgoal_tac "slot \<in> slots_holding_overlapping_caps cap s") apply (drule_tac x="fst slot" in spec, drule_tac x="snd slot" in spec) apply simp apply fastforce apply (auto simp: slots_holding_overlapping_caps_def' cte_wp_at_caps_of_state) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>slot'. \<lbrakk>slot' \<noteq> slot; slot' \<in> slots_holding_overlapping_caps cap s\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (prove)
using this:
\<not> is_final_cap' cap s
caps_of_state s slot = Some cap
gen_obj_refs cap \<noteq> {}

goal (1 subgoal):
 1. (\<And>slot'. \<lbrakk>slot' \<noteq> slot; slot' \<in> slots_holding_overlapping_caps cap s\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>slot'. \<lbrakk>slot' \<noteq> slot; slot' \<in> slots_holding_overlapping_caps cap s\<rbrakk> \<Longrightarrow> thesis; \<forall>a b. slots_holding_overlapping_caps cap s \<noteq> {(a, b)}; caps_of_state s slot = Some cap; gen_obj_refs cap \<noteq> {}\<rbrakk> \<Longrightarrow> thesis proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>slot'. \<lbrakk>slot' \<noteq> slot; slot' \<in> slots_holding_overlapping_caps cap s\<rbrakk> \<Longrightarrow> thesis; \<forall>a b. slots_holding_overlapping_caps cap s \<noteq> {(a, b)}; caps_of_state s slot = Some cap; gen_obj_refs cap \<noteq> {}; slot \<in> slots_holding_overlapping_caps cap s\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<And>slot'. \<lbrakk>slot' \<noteq> slot; slot' \<in> slots_holding_overlapping_caps cap s\<rbrakk> \<Longrightarrow> thesis; \<forall>a b. slots_holding_overlapping_caps cap s \<noteq> {(a, b)}; caps_of_state s slot = Some cap; gen_obj_refs cap \<noteq> {}\<rbrakk> \<Longrightarrow> slot \<in> slots_holding_overlapping_caps cap s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>slot'. \<lbrakk>slot' \<noteq> slot; slot' \<in> slots_holding_overlapping_caps cap s\<rbrakk> \<Longrightarrow> thesis; caps_of_state s slot = Some cap; gen_obj_refs cap \<noteq> {}; slot \<in> slots_holding_overlapping_caps cap s; slots_holding_overlapping_caps cap s \<noteq> {(fst slot, snd slot)}\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<And>slot'. \<lbrakk>slot' \<noteq> slot; slot' \<in> slots_holding_overlapping_caps cap s\<rbrakk> \<Longrightarrow> thesis; \<forall>a b. slots_holding_overlapping_caps cap s \<noteq> {(a, b)}; caps_of_state s slot = Some cap; gen_obj_refs cap \<noteq> {}\<rbrakk> \<Longrightarrow> slot \<in> slots_holding_overlapping_caps cap s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>slot'. \<lbrakk>slot' \<noteq> slot; slot' \<in> slots_holding_overlapping_caps cap s\<rbrakk> \<Longrightarrow> thesis; caps_of_state s slot = Some cap; gen_obj_refs cap \<noteq> {}; slot \<in> slots_holding_overlapping_caps cap s; slots_holding_overlapping_caps cap s \<noteq> {slot}\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<And>slot'. \<lbrakk>slot' \<noteq> slot; slot' \<in> slots_holding_overlapping_caps cap s\<rbrakk> \<Longrightarrow> thesis; \<forall>a b. slots_holding_overlapping_caps cap s \<noteq> {(a, b)}; caps_of_state s slot = Some cap; gen_obj_refs cap \<noteq> {}\<rbrakk> \<Longrightarrow> slot \<in> slots_holding_overlapping_caps cap s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>slot'. \<lbrakk>slot' \<noteq> slot; slot' \<in> slots_holding_overlapping_caps cap s\<rbrakk> \<Longrightarrow> thesis; \<forall>a b. slots_holding_overlapping_caps cap s \<noteq> {(a, b)}; caps_of_state s slot = Some cap; gen_obj_refs cap \<noteq> {}\<rbrakk> \<Longrightarrow> slot \<in> slots_holding_overlapping_caps cap s proof (prove)
goal:
No subgoals!