theory CSpaceInv_AI

lemma not_final_another_cte:
  "\<lbrakk> \<not> is_final_cap' cap s; fst (get_cap p s) = {(cap, s)};
       x \<in> cte_refs cap y; valid_objs s; zombies_final s \<rbrakk>
      \<Longrightarrow> \<exists>p' cap'. p' \<noteq> p \<and> fst (get_cap p' s) = {(cap', s)}
                         \<and> (\<forall>y. cte_refs cap' y = cte_refs cap y)
                         \<and> (\<forall>cp. appropriate_cte_cap cp cap'
                                     = appropriate_cte_cap cp cap)
                         \<and> \<not> is_final_cap' cap' s" apply (frule cte_refs_obj_refs_elem) apply (frule(1) not_final_another') subgoal by (auto simp: gen_obj_refs_def cap_irqs_def cap_irq_opt_def) apply (elim exEI, clarsimp) apply (drule(2) not_final_not_zombieD)+ apply (drule(1) get_cap_valid_objs_valid_cap)+ by (auto simp: is_zombie_def valid_cap_def
                        obj_at_def is_obj_defs
                        a_type_def gen_obj_refs_eq
                        option_set_singleton_eq
                        appropriate_cte_cap_irqs
                 dest:  obj_ref_is_arch
                 split: cap.split_asm if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> is_final_cap' cap s; fst (get_cap p s) = {(cap, s)}; x \<in> cte_refs cap y; valid_objs s; zombies_final s\<rbrakk> \<Longrightarrow> \<exists>p' cap'. p' \<noteq> p \<and> fst (get_cap p' s) = {(cap', s)} \<and> (\<forall>y. cte_refs cap' y = cte_refs cap y) \<and> (\<forall>cp. appropriate_cte_cap cp cap' = appropriate_cte_cap cp cap) \<and> \<not> is_final_cap' cap' s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> is_final_cap' cap s; fst (get_cap p s) = {(cap, s)}; x \<in> cte_refs cap y; valid_objs s; zombies_final s; fst x \<in> obj_refs cap \<or> (\<exists>irq. cap = IRQHandlerCap irq)\<rbrakk> \<Longrightarrow> \<exists>p' cap'. p' \<noteq> p \<and> fst (get_cap p' s) = {(cap', s)} \<and> (\<forall>y. cte_refs cap' y = cte_refs cap y) \<and> (\<forall>cp. appropriate_cte_cap cp cap' = appropriate_cte_cap cp cap) \<and> \<not> is_final_cap' cap' s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<not> is_final_cap' cap s; fst (get_cap p s) = {(cap, s)}; x \<in> cte_refs cap y; valid_objs s; zombies_final s; fst x \<in> obj_refs cap \<or> (\<exists>irq. cap = IRQHandlerCap irq)\<rbrakk> \<Longrightarrow> gen_obj_refs cap \<noteq> {}
 2. \<lbrakk>\<not> is_final_cap' cap s; fst (get_cap p s) = {(cap, s)}; x \<in> cte_refs cap y; valid_objs s; zombies_final s; fst x \<in> obj_refs cap \<or> (\<exists>irq. cap = IRQHandlerCap irq); \<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\<rbrakk> \<Longrightarrow> \<exists>p' cap'. p' \<noteq> p \<and> fst (get_cap p' s) = {(cap', s)} \<and> (\<forall>y. cte_refs cap' y = cte_refs cap y) \<and> (\<forall>cp. appropriate_cte_cap cp cap' = appropriate_cte_cap cp cap) \<and> \<not> is_final_cap' cap' s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> is_final_cap' cap s; fst (get_cap p s) = {(cap, s)}; x \<in> cte_refs cap y; valid_objs s; zombies_final s; fst x \<in> obj_refs cap \<or> (\<exists>irq. cap = IRQHandlerCap irq)\<rbrakk> \<Longrightarrow> gen_obj_refs cap \<noteq> {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> is_final_cap' cap s; fst (get_cap p s) = {(cap, s)}; x \<in> cte_refs cap y; valid_objs s; zombies_final s; fst x \<in> obj_refs cap \<or> (\<exists>irq. cap = IRQHandlerCap irq); \<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\<rbrakk> \<Longrightarrow> \<exists>p' cap'. p' \<noteq> p \<and> fst (get_cap p' s) = {(cap', s)} \<and> (\<forall>y. cte_refs cap' y = cte_refs cap y) \<and> (\<forall>cp. appropriate_cte_cap cp cap' = appropriate_cte_cap cp cap) \<and> \<not> is_final_cap' cap' s proof (prove)
goal (1 subgoal):
 1. \<And>a b xa. \<lbrakk>\<not> is_final_cap' cap s; fst (get_cap p s) = {(cap, s)}; x \<in> cte_refs cap y; valid_objs s; zombies_final s; fst x \<in> obj_refs cap \<or> (\<exists>irq. cap = IRQHandlerCap irq); (a, b) \<noteq> p; fst (get_cap (a, b) s) = {(xa, s)}; gen_obj_refs xa = gen_obj_refs cap; \<not> is_final_cap' xa s\<rbrakk> \<Longrightarrow> (\<forall>y. cte_refs xa y = cte_refs cap y) \<and> (\<forall>cp. appropriate_cte_cap cp xa = appropriate_cte_cap cp cap) proof (prove)
goal (1 subgoal):
 1. \<And>a b xa. \<lbrakk>fst (get_cap p s) = {(cap, s)}; x \<in> cte_refs cap y; valid_objs s; zombies_final s; fst x \<in> obj_refs cap \<or> (\<exists>irq. cap = IRQHandlerCap irq); (a, b) \<noteq> p; fst (get_cap (a, b) s) = {(xa, s)}; gen_obj_refs xa = gen_obj_refs cap; \<not> is_zombie cap; \<not> is_zombie xa\<rbrakk> \<Longrightarrow> (\<forall>y. cte_refs xa y = cte_refs cap y) \<and> (\<forall>cp. appropriate_cte_cap cp xa = appropriate_cte_cap cp cap) proof (prove)
goal (1 subgoal):
 1. \<And>a b xa. \<lbrakk>x \<in> cte_refs cap y; valid_objs s; zombies_final s; fst x \<in> obj_refs cap \<or> (\<exists>irq. cap = IRQHandlerCap irq); (a, b) \<noteq> p; gen_obj_refs xa = gen_obj_refs cap; \<not> is_zombie cap; \<not> is_zombie xa; s \<turnstile> cap; s \<turnstile> xa\<rbrakk> \<Longrightarrow> (\<forall>y. cte_refs xa y = cte_refs cap y) \<and> (\<forall>cp. appropriate_cte_cap cp xa = appropriate_cte_cap cp cap)