theory CSpaceInv_AI

lemma delete_duplicate_iflive:
  "\<lbrace>\<lambda>s. cte_wp_at (\<lambda>cap. \<not> is_final_cap' cap s) p s
      \<and> if_live_then_nonz_cap s \<and> zombies_final s\<rbrace>
     set_cap cap.NullCap p \<lbrace>\<lambda>rv s. if_live_then_nonz_cap s\<rbrace>" apply (clarsimp simp: if_live_then_nonz_cap_def ex_nonz_cap_to_def) apply (simp only: imp_conv_disj) apply (rule hoare_pre,
         wp hoare_vcg_all_lift hoare_vcg_disj_lift hoare_vcg_ex_lift
            set_cap_cte_wp_at) apply (clarsimp simp: cte_wp_at_def) apply (drule spec, drule(1) mp) apply clarsimp apply (case_tac "(a, b) = p") apply (clarsimp simp: zobj_refs_to_obj_refs) apply (drule(2) not_final_another[OF _ _ obj_ref_is_gen_obj_ref]) apply (simp, elim exEI, clarsimp simp: gen_obj_refs_eq) apply (erule(2) zombies_finalE) apply (simp add: cte_wp_at_def) apply (intro exI, erule conjI, clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cte_wp_at (\<lambda>cap. \<not> is_final_cap' cap s) p s \<and> if_live_then_nonz_cap s \<and> zombies_final s\<rbrace> set_cap NullCap p \<lbrace>\<lambda>rv. if_live_then_nonz_cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cte_wp_at (\<lambda>cap. \<not> is_final_cap' cap s) p s \<and> (\<forall>ptr. obj_at live ptr s \<longrightarrow> (\<exists>a b. cte_wp_at (\<lambda>c. ptr \<in> zobj_refs c) (a, b) s)) \<and> zombies_final s\<rbrace> set_cap NullCap p \<lbrace>\<lambda>rv s. \<forall>ptr. obj_at live ptr s \<longrightarrow> (\<exists>a b. cte_wp_at (\<lambda>c. ptr \<in> zobj_refs c) (a, b) s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cte_wp_at (\<lambda>cap. \<not> is_final_cap' cap s) p s \<and> (\<forall>ptr. \<not> obj_at live ptr s \<or> (\<exists>a b. cte_wp_at (\<lambda>c. ptr \<in> zobj_refs c) (a, b) s)) \<and> zombies_final s\<rbrace> set_cap NullCap p \<lbrace>\<lambda>rv s. \<forall>ptr. \<not> obj_at live ptr s \<or> (\<exists>a b. cte_wp_at (\<lambda>c. ptr \<in> zobj_refs c) (a, b) s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. cte_wp_at (\<lambda>cap. \<not> is_final_cap' cap s) p s \<and> (\<forall>ptr. \<not> obj_at live ptr s \<or> (\<exists>a b. cte_wp_at (\<lambda>c. ptr \<in> zobj_refs c) (a, b) s)) \<and> zombies_final s \<Longrightarrow> \<forall>x. \<not> obj_at live x s \<or> (\<exists>xa xb. ((\<lambda>s. if (xa, xb) = p then x \<in> zobj_refs NullCap else cte_wp_at (\<lambda>c. x \<in> zobj_refs c) (xa, xb) s) and cte_wp_at (\<lambda>_. True) p) s) proof (prove)
goal (1 subgoal):
 1. \<And>s x cap. \<lbrakk>\<forall>ptr. obj_at live ptr s \<longrightarrow> (\<exists>a b cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> ptr \<in> zobj_refs cap); zombies_final s; fst (get_cap p s) = {(cap, s)}; \<not> is_final_cap' cap s; obj_at live x s\<rbrakk> \<Longrightarrow> \<exists>xa xb. (xa, xb) \<noteq> p \<and> ((xa, xb) \<noteq> p \<longrightarrow> (\<exists>cap. fst (get_cap (xa, xb) s) = {(cap, s)} \<and> x \<in> zobj_refs cap)) proof (prove)
goal (1 subgoal):
 1. \<And>s x cap. \<lbrakk>zombies_final s; fst (get_cap p s) = {(cap, s)}; \<not> is_final_cap' cap s; obj_at live x s; \<exists>a b cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> x \<in> zobj_refs cap\<rbrakk> \<Longrightarrow> \<exists>xa xb. (xa, xb) \<noteq> p \<and> ((xa, xb) \<noteq> p \<longrightarrow> (\<exists>cap. fst (get_cap (xa, xb) s) = {(cap, s)} \<and> x \<in> zobj_refs cap)) proof (prove)
goal (1 subgoal):
 1. \<And>s x cap a b capa. \<lbrakk>zombies_final s; fst (get_cap p s) = {(cap, s)}; \<not> is_final_cap' cap s; obj_at live x s; fst (get_cap (a, b) s) = {(capa, s)}; x \<in> zobj_refs capa\<rbrakk> \<Longrightarrow> \<exists>xa xb. (xa, xb) \<noteq> p \<and> ((xa, xb) \<noteq> p \<longrightarrow> (\<exists>cap. fst (get_cap (xa, xb) s) = {(cap, s)} \<and> x \<in> zobj_refs cap)) proof (prove)
goal (2 subgoals):
 1. \<And>s x cap a b capa. \<lbrakk>zombies_final s; fst (get_cap p s) = {(cap, s)}; \<not> is_final_cap' cap s; obj_at live x s; fst (get_cap (a, b) s) = {(capa, s)}; x \<in> zobj_refs capa; (a, b) = p\<rbrakk> \<Longrightarrow> \<exists>xa xb. (xa, xb) \<noteq> p \<and> ((xa, xb) \<noteq> p \<longrightarrow> (\<exists>cap. fst (get_cap (xa, xb) s) = {(cap, s)} \<and> x \<in> zobj_refs cap))
 2. \<And>s x cap a b capa. \<lbrakk>zombies_final s; fst (get_cap p s) = {(cap, s)}; \<not> is_final_cap' cap s; obj_at live x s; fst (get_cap (a, b) s) = {(capa, s)}; x \<in> zobj_refs capa; (a, b) \<noteq> p\<rbrakk> \<Longrightarrow> \<exists>xa xb. (xa, xb) \<noteq> p \<and> ((xa, xb) \<noteq> p \<longrightarrow> (\<exists>cap. fst (get_cap (xa, xb) s) = {(cap, s)} \<and> x \<in> zobj_refs cap)) proof (prove)
goal (2 subgoals):
 1. \<And>s x a b capa. \<lbrakk>zombies_final s; fst (get_cap (a, b) s) = {(capa, s)}; \<not> is_final_cap' capa s; obj_at live x s; p = (a, b); x \<in> obj_refs capa; \<not> is_zombie capa\<rbrakk> \<Longrightarrow> \<exists>xa xb. (xa = a \<longrightarrow> xb \<noteq> b) \<and> ((xa = a \<longrightarrow> xb \<noteq> b) \<longrightarrow> (\<exists>cap. fst (get_cap (xa, xb) s) = {(cap, s)} \<and> x \<in> obj_refs cap \<and> \<not> is_zombie cap))
 2. \<And>s x cap a b capa. \<lbrakk>zombies_final s; fst (get_cap p s) = {(cap, s)}; \<not> is_final_cap' cap s; obj_at live x s; fst (get_cap (a, b) s) = {(capa, s)}; x \<in> zobj_refs capa; (a, b) \<noteq> p\<rbrakk> \<Longrightarrow> \<exists>xa xb. (xa, xb) \<noteq> p \<and> ((xa, xb) \<noteq> p \<longrightarrow> (\<exists>cap. fst (get_cap (xa, xb) s) = {(cap, s)} \<and> x \<in> zobj_refs cap)) proof (prove)
goal (2 subgoals):
 1. \<And>s x a b capa. \<lbrakk>zombies_final s; fst (get_cap (a, b) s) = {(capa, s)}; obj_at live x s; p = (a, b); x \<in> obj_refs capa; \<not> is_zombie capa; \<exists>p' cap'. p' \<noteq> (a, b) \<and> fst (get_cap p' s) = {(cap', s)} \<and> gen_obj_refs cap' = gen_obj_refs capa \<and> \<not> is_final_cap' cap' s\<rbrakk> \<Longrightarrow> \<exists>xa xb. (xa = a \<longrightarrow> xb \<noteq> b) \<and> ((xa = a \<longrightarrow> xb \<noteq> b) \<longrightarrow> (\<exists>cap. fst (get_cap (xa, xb) s) = {(cap, s)} \<and> x \<in> obj_refs cap \<and> \<not> is_zombie cap))
 2. \<And>s x cap a b capa. \<lbrakk>zombies_final s; fst (get_cap p s) = {(cap, s)}; \<not> is_final_cap' cap s; obj_at live x s; fst (get_cap (a, b) s) = {(capa, s)}; x \<in> zobj_refs capa; (a, b) \<noteq> p\<rbrakk> \<Longrightarrow> \<exists>xa xb. (xa, xb) \<noteq> p \<and> ((xa, xb) \<noteq> p \<longrightarrow> (\<exists>cap. fst (get_cap (xa, xb) s) = {(cap, s)} \<and> x \<in> zobj_refs cap)) proof (prove)
goal (2 subgoals):
 1. \<And>s x a b capa xa xb cap'. \<lbrakk>zombies_final s; fst (get_cap (a, b) s) = {(capa, s)}; obj_at live x s; p = (a, b); x \<in> obj_refs capa; \<not> is_zombie capa; xa = a \<longrightarrow> xb \<noteq> b; fst (get_cap (xa, xb) s) = {(cap', s)}; obj_refs cap' = obj_refs capa; cap_irqs cap' = cap_irqs capa; arch_gen_refs cap' = arch_gen_refs capa; \<not> is_final_cap' cap' s; is_zombie cap'\<rbrakk> \<Longrightarrow> False
 2. \<And>s x cap a b capa. \<lbrakk>zombies_final s; fst (get_cap p s) = {(cap, s)}; \<not> is_final_cap' cap s; obj_at live x s; fst (get_cap (a, b) s) = {(capa, s)}; x \<in> zobj_refs capa; (a, b) \<noteq> p\<rbrakk> \<Longrightarrow> \<exists>xa xb. (xa, xb) \<noteq> p \<and> ((xa, xb) \<noteq> p \<longrightarrow> (\<exists>cap. fst (get_cap (xa, xb) s) = {(cap, s)} \<and> x \<in> zobj_refs cap)) proof (prove)
goal (2 subgoals):
 1. \<And>s x a b capa xa xb cap'. \<lbrakk>zombies_final s; fst (get_cap (a, b) s) = {(capa, s)}; obj_at live x s; p = (a, b); x \<in> obj_refs capa; \<not> is_zombie capa; xa = a \<longrightarrow> xb \<noteq> b; fst (get_cap (xa, xb) s) = {(cap', s)}; obj_refs cap' = obj_refs capa; cap_irqs cap' = cap_irqs capa; arch_gen_refs cap' = arch_gen_refs capa; is_zombie cap'\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap') (?p65 s x a b capa xa xb cap') s
 2. \<And>s x cap a b capa. \<lbrakk>zombies_final s; fst (get_cap p s) = {(cap, s)}; \<not> is_final_cap' cap s; obj_at live x s; fst (get_cap (a, b) s) = {(capa, s)}; x \<in> zobj_refs capa; (a, b) \<noteq> p\<rbrakk> \<Longrightarrow> \<exists>xa xb. (xa, xb) \<noteq> p \<and> ((xa, xb) \<noteq> p \<longrightarrow> (\<exists>cap. fst (get_cap (xa, xb) s) = {(cap, s)} \<and> x \<in> zobj_refs cap)) proof (prove)
goal (1 subgoal):
 1. \<And>s x cap a b capa. \<lbrakk>zombies_final s; fst (get_cap p s) = {(cap, s)}; \<not> is_final_cap' cap s; obj_at live x s; fst (get_cap (a, b) s) = {(capa, s)}; x \<in> zobj_refs capa; (a, b) \<noteq> p\<rbrakk> \<Longrightarrow> \<exists>xa xb. (xa, xb) \<noteq> p \<and> ((xa, xb) \<noteq> p \<longrightarrow> (\<exists>cap. fst (get_cap (xa, xb) s) = {(cap, s)} \<and> x \<in> zobj_refs cap)) proof (prove)
goal:
No subgoals!