theory Finalise_DR

lemma zombies_final_ccontr:
  "\<lbrakk>caps_of_state s p = Some cap; r \<in> obj_refs cap; is_zombie cap; zombies_final s;
     caps_of_state s p' = Some cap'\<rbrakk>
    \<Longrightarrow> r\<in> obj_refs cap' \<longrightarrow> is_zombie cap' \<and> p = p'" apply (rule ccontr) apply (case_tac p) apply (clarsimp simp:zombies_final_def) apply (drule_tac x = a in spec,drule_tac x = b in spec) apply (frule caps_of_state_cteD) apply (simp add:cte_wp_at_def) apply (clarsimp simp:IpcCancel_A.is_final_cap'_def) apply (frule_tac a = "(aa,ba)" and b = p' in singleton_set_eq) apply (clarsimp) apply (drule_tac a = "(aa,ba)" and b = p' in singleton_set_eq) apply (clarsimp dest!:caps_of_state_cteD simp:cte_wp_at_def) apply (drule IntI) apply (simp add: gen_obj_refs_Int)+ apply (drule_tac a = "(aa,ba)" and b = "(a,b)" in singleton_set_eq) apply clarsimp apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s p = Some cap; r \<in> obj_refs cap; is_zombie cap; zombies_final s; caps_of_state s p' = Some cap'\<rbrakk> \<Longrightarrow> r \<in> obj_refs cap' \<longrightarrow> is_zombie cap' \<and> p = p' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s p = Some cap; r \<in> obj_refs cap; is_zombie cap; zombies_final s; caps_of_state s p' = Some cap'; \<not> (r \<in> obj_refs cap' \<longrightarrow> is_zombie cap' \<and> p = p')\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>caps_of_state s p = Some cap; r \<in> obj_refs cap; is_zombie cap; zombies_final s; caps_of_state s p' = Some cap'; \<not> (r \<in> obj_refs cap' \<longrightarrow> is_zombie cap' \<and> p = p'); p = (a, b)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>caps_of_state s (a, b) = Some cap; r \<in> obj_refs cap; is_zombie cap; \<forall>a b. cte_wp_at is_zombie (a, b) s \<longrightarrow> cte_wp_at (\<lambda>cap. IpcCancel_A.is_final_cap' cap s) (a, b) s; caps_of_state s p' = Some cap'; p = (a, b); r \<in> obj_refs cap'; is_zombie cap' \<longrightarrow> (a, b) \<noteq> p'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>caps_of_state s (a, b) = Some cap; r \<in> obj_refs cap; is_zombie cap; caps_of_state s p' = Some cap'; p = (a, b); r \<in> obj_refs cap'; is_zombie cap' \<longrightarrow> (a, b) \<noteq> p'; cte_wp_at is_zombie (a, b) s \<longrightarrow> cte_wp_at (\<lambda>cap. IpcCancel_A.is_final_cap' cap s) (a, b) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>caps_of_state s (a, b) = Some cap; r \<in> obj_refs cap; is_zombie cap; caps_of_state s p' = Some cap'; p = (a, b); r \<in> obj_refs cap'; is_zombie cap' \<longrightarrow> (a, b) \<noteq> p'; cte_wp_at is_zombie (a, b) s \<longrightarrow> cte_wp_at (\<lambda>cap. IpcCancel_A.is_final_cap' cap s) (a, b) s; cte_wp_at ((=) cap) (a, b) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>caps_of_state s (a, b) = Some cap; r \<in> obj_refs cap; is_zombie cap; caps_of_state s p' = Some cap'; p = (a, b); r \<in> obj_refs cap'; is_zombie cap' \<longrightarrow> (a, b) \<noteq> p'; IpcCancel_A.is_final_cap' cap s; fst (CSpaceAcc_A.get_cap (a, b) s) = {(cap, s)}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>caps_of_state s (a, b) = Some cap; r \<in> obj_refs cap; is_zombie cap; caps_of_state s p' = Some cap'; p = (a, b); r \<in> obj_refs cap'; is_zombie cap' \<longrightarrow> (a, b) \<noteq> p'; fst (CSpaceAcc_A.get_cap (a, b) s) = {(cap, s)}; {cref. \<exists>cap'. fst (CSpaceAcc_A.get_cap cref s) = {(cap', s)} \<and> gen_obj_refs cap \<inter> gen_obj_refs cap' \<noteq> {}} = {(aa, ba)}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba. \<lbrakk>caps_of_state s (a, b) = Some cap; r \<in> obj_refs cap; is_zombie cap; caps_of_state s p' = Some cap'; p = (a, b); r \<in> obj_refs cap'; is_zombie cap' \<longrightarrow> (a, b) \<noteq> p'; fst (CSpaceAcc_A.get_cap (a, b) s) = {(cap, s)}; {cref. \<exists>cap'. fst (CSpaceAcc_A.get_cap cref s) = {(cap', s)} \<and> gen_obj_refs cap \<inter> gen_obj_refs cap' \<noteq> {}} = {(aa, ba)}\<rbrakk> \<Longrightarrow> p' \<in> {cref. \<exists>cap'. fst (CSpaceAcc_A.get_cap cref s) = {(cap', s)} \<and> gen_obj_refs cap \<inter> gen_obj_refs cap' \<noteq> {}}
 2. \<And>a b aa ba. \<lbrakk>caps_of_state s (a, b) = Some cap; r \<in> obj_refs cap; is_zombie cap; caps_of_state s p' = Some cap'; p = (a, b); r \<in> obj_refs cap'; is_zombie cap' \<longrightarrow> (a, b) \<noteq> p'; fst (CSpaceAcc_A.get_cap (a, b) s) = {(cap, s)}; {cref. \<exists>cap'. fst (CSpaceAcc_A.get_cap cref s) = {(cap', s)} \<and> gen_obj_refs cap \<inter> gen_obj_refs cap' \<noteq> {}} = {(aa, ba)}; p' = (aa, ba)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba. \<lbrakk>caps_of_state s (a, b) = Some cap; r \<in> obj_refs cap; is_zombie cap; caps_of_state s p' = Some cap'; p = (a, b); r \<in> obj_refs cap'; is_zombie cap' \<longrightarrow> (a, b) \<noteq> p'; fst (CSpaceAcc_A.get_cap (a, b) s) = {(cap, s)}; {cref. \<exists>cap'. fst (CSpaceAcc_A.get_cap cref s) = {(cap', s)} \<and> gen_obj_refs cap \<inter> gen_obj_refs cap' \<noteq> {}} = {(aa, ba)}\<rbrakk> \<Longrightarrow> p' = (aa, ba)
 2. \<And>a b aa ba. \<lbrakk>caps_of_state s (a, b) = Some cap; r \<in> obj_refs cap; is_zombie cap; caps_of_state s p' = Some cap'; p = (a, b); r \<in> obj_refs cap'; is_zombie cap' \<longrightarrow> (a, b) \<noteq> p'; fst (CSpaceAcc_A.get_cap (a, b) s) = {(cap, s)}; {cref. \<exists>cap'. fst (CSpaceAcc_A.get_cap cref s) = {(cap', s)} \<and> gen_obj_refs cap \<inter> gen_obj_refs cap' \<noteq> {}} = {(aa, ba)}; p' = (aa, ba)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>a b aa ba. \<lbrakk>caps_of_state s (a, b) = Some cap; r \<in> obj_refs cap; is_zombie cap; caps_of_state s p' = Some cap'; p = (a, b); r \<in> obj_refs cap'; is_zombie cap' \<longrightarrow> (a, b) \<noteq> p'; fst (CSpaceAcc_A.get_cap (a, b) s) = {(cap, s)}\<rbrakk> \<Longrightarrow> p' \<in> {cref. \<exists>cap'. fst (CSpaceAcc_A.get_cap cref s) = {(cap', s)} \<and> gen_obj_refs cap \<inter> gen_obj_refs cap' \<noteq> {}}
 2. \<And>a b aa ba. \<lbrakk>caps_of_state s (a, b) = Some cap; r \<in> obj_refs cap; is_zombie cap; caps_of_state s p' = Some cap'; p = (a, b); r \<in> obj_refs cap'; is_zombie cap' \<longrightarrow> (a, b) \<noteq> p'; fst (CSpaceAcc_A.get_cap (a, b) s) = {(cap, s)}; p' = (aa, ba)\<rbrakk> \<Longrightarrow> p' = (aa, ba)
 3. \<And>a b aa ba. \<lbrakk>caps_of_state s (a, b) = Some cap; r \<in> obj_refs cap; is_zombie cap; caps_of_state s p' = Some cap'; p = (a, b); r \<in> obj_refs cap'; is_zombie cap' \<longrightarrow> (a, b) \<noteq> p'; fst (CSpaceAcc_A.get_cap (a, b) s) = {(cap, s)}; {cref. \<exists>cap'. fst (CSpaceAcc_A.get_cap cref s) = {(cap', s)} \<and> gen_obj_refs cap \<inter> gen_obj_refs cap' \<noteq> {}} = {(aa, ba)}; p' = (aa, ba)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>a b. \<lbrakk>r \<in> obj_refs cap; is_zombie cap; p = (a, b); r \<in> obj_refs cap'; is_zombie cap' \<longrightarrow> (a, b) \<noteq> p'; fst (CSpaceAcc_A.get_cap (a, b) s) = {(cap, s)}; fst (CSpaceAcc_A.get_cap p' s) = {(cap', s)}; gen_obj_refs cap \<inter> gen_obj_refs cap' = {}\<rbrakk> \<Longrightarrow> False
 2. \<And>a b aa ba. \<lbrakk>caps_of_state s (a, b) = Some cap; r \<in> obj_refs cap; is_zombie cap; caps_of_state s p' = Some cap'; p = (a, b); r \<in> obj_refs cap'; is_zombie cap' \<longrightarrow> (a, b) \<noteq> p'; fst (CSpaceAcc_A.get_cap (a, b) s) = {(cap, s)}; p' = (aa, ba)\<rbrakk> \<Longrightarrow> p' = (aa, ba)
 3. \<And>a b aa ba. \<lbrakk>caps_of_state s (a, b) = Some cap; r \<in> obj_refs cap; is_zombie cap; caps_of_state s p' = Some cap'; p = (a, b); r \<in> obj_refs cap'; is_zombie cap' \<longrightarrow> (a, b) \<noteq> p'; fst (CSpaceAcc_A.get_cap (a, b) s) = {(cap, s)}; {cref. \<exists>cap'. fst (CSpaceAcc_A.get_cap cref s) = {(cap', s)} \<and> gen_obj_refs cap \<inter> gen_obj_refs cap' \<noteq> {}} = {(aa, ba)}; p' = (aa, ba)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>a b. \<lbrakk>is_zombie cap; p = (a, b); r \<in> obj_refs cap'; is_zombie cap' \<longrightarrow> (a, b) \<noteq> p'; fst (CSpaceAcc_A.get_cap (a, b) s) = {(cap, s)}; fst (CSpaceAcc_A.get_cap p' s) = {(cap', s)}; gen_obj_refs cap \<inter> gen_obj_refs cap' = {}\<rbrakk> \<Longrightarrow> r \<in> ?B23 a b
 2. \<And>a b. \<lbrakk>is_zombie cap; p = (a, b); r \<in> obj_refs cap'; is_zombie cap' \<longrightarrow> (a, b) \<noteq> p'; fst (CSpaceAcc_A.get_cap (a, b) s) = {(cap, s)}; fst (CSpaceAcc_A.get_cap p' s) = {(cap', s)}; gen_obj_refs cap \<inter> gen_obj_refs cap' = {}; r \<in> obj_refs cap \<inter> ?B23 a b\<rbrakk> \<Longrightarrow> False
 3. \<And>a b aa ba. \<lbrakk>caps_of_state s (a, b) = Some cap; r \<in> obj_refs cap; is_zombie cap; caps_of_state s p' = Some cap'; p = (a, b); r \<in> obj_refs cap'; is_zombie cap' \<longrightarrow> (a, b) \<noteq> p'; fst (CSpaceAcc_A.get_cap (a, b) s) = {(cap, s)}; p' = (aa, ba)\<rbrakk> \<Longrightarrow> p' = (aa, ba)
 4. \<And>a b aa ba. \<lbrakk>caps_of_state s (a, b) = Some cap; r \<in> obj_refs cap; is_zombie cap; caps_of_state s p' = Some cap'; p = (a, b); r \<in> obj_refs cap'; is_zombie cap' \<longrightarrow> (a, b) \<noteq> p'; fst (CSpaceAcc_A.get_cap (a, b) s) = {(cap, s)}; {cref. \<exists>cap'. fst (CSpaceAcc_A.get_cap cref s) = {(cap', s)} \<and> gen_obj_refs cap \<inter> gen_obj_refs cap' \<noteq> {}} = {(aa, ba)}; p' = (aa, ba)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>caps_of_state s (a, b) = Some cap; r \<in> obj_refs cap; is_zombie cap; caps_of_state s (aa, ba) = Some cap'; p = (a, b); r \<in> obj_refs cap'; is_zombie cap' \<longrightarrow> a = aa \<longrightarrow> b \<noteq> ba; fst (CSpaceAcc_A.get_cap (a, b) s) = {(cap, s)}; {cref. \<exists>cap'. fst (CSpaceAcc_A.get_cap cref s) = {(cap', 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> {})} = {(aa, ba)}; p' = (aa, ba)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba. \<lbrakk>caps_of_state s (a, b) = Some cap; r \<in> obj_refs cap; is_zombie cap; caps_of_state s (aa, ba) = Some cap'; p = (a, b); r \<in> obj_refs cap'; is_zombie cap' \<longrightarrow> a = aa \<longrightarrow> b \<noteq> ba; fst (CSpaceAcc_A.get_cap (a, b) s) = {(cap, s)}; p' = (aa, ba)\<rbrakk> \<Longrightarrow> (a, b) \<in> {cref. \<exists>cap'. fst (CSpaceAcc_A.get_cap cref s) = {(cap', 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> {})}
 2. \<And>a b aa ba. \<lbrakk>caps_of_state s (a, b) = Some cap; r \<in> obj_refs cap; is_zombie cap; caps_of_state s (aa, ba) = Some cap'; p = (a, b); r \<in> obj_refs cap'; is_zombie cap' \<longrightarrow> a = aa \<longrightarrow> b \<noteq> ba; fst (CSpaceAcc_A.get_cap (a, b) s) = {(cap, s)}; p' = (aa, ba); (a, b) = (aa, ba)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>caps_of_state s (a, b) = Some cap; r \<in> obj_refs cap; is_zombie cap; caps_of_state s (aa, ba) = Some cap'; p = (a, b); r \<in> obj_refs cap'; is_zombie cap' \<longrightarrow> a = aa \<longrightarrow> b \<noteq> ba; fst (CSpaceAcc_A.get_cap (a, b) s) = {(cap, s)}; p' = (aa, ba); (a, b) = (aa, ba)\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!