theory CSpaceInvPre_AI

lemma not_final_another':
  "\<lbrakk> \<not> is_final_cap' cap s; fst (get_cap p s) = {(cap, s)};
       gen_obj_refs cap \<noteq> {} \<rbrakk>
      \<Longrightarrow> \<exists>p' cap'. p' \<noteq> p \<and> fst (get_cap p' s) = {(cap', s)}
                         \<and> gen_obj_refs cap' = gen_obj_refs cap
                         \<and> \<not> is_final_cap' cap' s" apply (simp add: is_final_cap'_def gen_obj_refs_Int_not cong: conj_cong
              del: split_paired_Ex split_paired_All) apply (erule not_singleton_oneE[where p=p]) apply simp apply (rule_tac x=p' in exI) apply clarsimp apply (drule gen_obj_refs_distinct_or_equal) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> is_final_cap' cap s; fst (get_cap p s) = {(cap, s)}; gen_obj_refs cap \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>p' cap'. p' \<noteq> p \<and> fst (get_cap p' s) = {(cap', s)} \<and> gen_obj_refs cap' = gen_obj_refs cap \<and> \<not> is_final_cap' cap' s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>cref. {cref. \<exists>cap'. fst (get_cap cref s) = {(cap', s)} \<and> gen_obj_refs cap \<inter> gen_obj_refs cap' \<noteq> {}} \<noteq> {cref}; fst (get_cap p s) = {(cap, s)}; gen_obj_refs cap \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>p'. p' \<noteq> p \<and> (\<exists>cap'. fst (get_cap p' s) = {(cap', s)} \<and> gen_obj_refs cap' = gen_obj_refs cap) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>fst (get_cap p s) = {(cap, s)}; gen_obj_refs cap \<noteq> {}\<rbrakk> \<Longrightarrow> p \<in> {cref. \<exists>cap'. fst (get_cap cref s) = {(cap', s)} \<and> gen_obj_refs cap \<inter> gen_obj_refs cap' \<noteq> {}}
 2. \<And>p'. \<lbrakk>fst (get_cap p s) = {(cap, s)}; gen_obj_refs cap \<noteq> {}; p \<noteq> p'; p' \<in> {cref. \<exists>cap'. fst (get_cap cref s) = {(cap', s)} \<and> gen_obj_refs cap \<inter> gen_obj_refs cap' \<noteq> {}}\<rbrakk> \<Longrightarrow> \<exists>p'. p' \<noteq> p \<and> (\<exists>cap'. fst (get_cap p' s) = {(cap', s)} \<and> gen_obj_refs cap' = gen_obj_refs cap) proof (prove)
goal (1 subgoal):
 1. \<And>p'. \<lbrakk>fst (get_cap p s) = {(cap, s)}; gen_obj_refs cap \<noteq> {}; p \<noteq> p'; p' \<in> {cref. \<exists>cap'. fst (get_cap cref s) = {(cap', s)} \<and> gen_obj_refs cap \<inter> gen_obj_refs cap' \<noteq> {}}\<rbrakk> \<Longrightarrow> \<exists>p'. p' \<noteq> p \<and> (\<exists>cap'. fst (get_cap p' s) = {(cap', s)} \<and> gen_obj_refs cap' = gen_obj_refs cap) proof (prove)
goal (1 subgoal):
 1. \<And>p'. \<lbrakk>fst (get_cap p s) = {(cap, s)}; gen_obj_refs cap \<noteq> {}; p \<noteq> p'; p' \<in> {cref. \<exists>cap'. fst (get_cap cref s) = {(cap', s)} \<and> gen_obj_refs cap \<inter> gen_obj_refs cap' \<noteq> {}}\<rbrakk> \<Longrightarrow> p' \<noteq> p \<and> (\<exists>cap'. fst (get_cap p' s) = {(cap', s)} \<and> gen_obj_refs cap' = gen_obj_refs cap) proof (prove)
goal (1 subgoal):
 1. \<And>a b cap'. \<lbrakk>fst (get_cap p s) = {(cap, s)}; gen_obj_refs cap \<noteq> {}; p \<noteq> (a, b); fst (get_cap (a, b) s) = {(cap', s)}; gen_obj_refs cap \<inter> gen_obj_refs cap' \<noteq> {}\<rbrakk> \<Longrightarrow> gen_obj_refs cap' = gen_obj_refs cap proof (prove)
goal (1 subgoal):
 1. \<And>a b cap'. \<lbrakk>fst (get_cap p s) = {(cap, s)}; gen_obj_refs cap \<noteq> {}; p \<noteq> (a, b); fst (get_cap (a, b) s) = {(cap', s)}; gen_obj_refs cap = gen_obj_refs cap'\<rbrakk> \<Longrightarrow> gen_obj_refs cap' = gen_obj_refs cap proof (prove)
goal:
No subgoals!