theory CNodeInv_AI

lemma cap_swap_fd_final_cap_at_one_case:
  "\<lbrace>\<lambda>s. p \<noteq> p'' \<and> ((p = p') \<longrightarrow> cte_wp_at (\<lambda>c. is_final_cap' c s) p'' s)
     \<and> ((p \<noteq> p') \<longrightarrow> cte_wp_at (\<lambda>c. is_final_cap' c s) p s)\<rbrace>
   cap_swap_for_delete p' p''
  \<lbrace>\<lambda>rv s. cte_wp_at (\<lambda>c. is_final_cap' c s) p s\<rbrace>" apply (simp only: final_cap_at_eq cte_wp_at_conj) apply (simp add: cte_wp_at_caps_of_state) apply wp apply (cases "p = p'") apply (cases p', clarsimp) apply clarsimp apply (cases p', cases p'', clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. p \<noteq> p'' \<and> (p = p' \<longrightarrow> cte_wp_at (\<lambda>c. is_final_cap' c s) p'' s) \<and> (p \<noteq> p' \<longrightarrow> cte_wp_at (\<lambda>c. is_final_cap' c s) p s)\<rbrace> cap_swap_for_delete p' p'' \<lbrace>\<lambda>rv s. cte_wp_at (\<lambda>c. is_final_cap' c s) p s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. p \<noteq> p'' \<and> (p = p' \<longrightarrow> (\<exists>cp. cte_wp_at (\<lambda>c. c = cp) p'' s \<and> gen_obj_refs cp \<noteq> {} \<and> (\<forall>p'. cte_wp_at (\<lambda>_. True) p' s \<and> p' \<noteq> p'' \<longrightarrow> cte_wp_at (\<lambda>c. gen_obj_refs cp \<inter> gen_obj_refs c = {}) p' s))) \<and> (p \<noteq> p' \<longrightarrow> (\<exists>cp. cte_wp_at (\<lambda>c. c = cp) p s \<and> gen_obj_refs cp \<noteq> {} \<and> (\<forall>p'. cte_wp_at (\<lambda>_. True) p' s \<and> p' \<noteq> p \<longrightarrow> cte_wp_at (\<lambda>c. gen_obj_refs cp \<inter> gen_obj_refs c = {}) p' s)))\<rbrace> cap_swap_for_delete p' p'' \<lbrace>\<lambda>rv s. \<exists>cp. cte_wp_at (\<lambda>c. c = cp) p s \<and> gen_obj_refs cp \<noteq> {} \<and> (\<forall>p'. cte_wp_at (\<lambda>_. True) p' s \<and> p' \<noteq> p \<longrightarrow> cte_wp_at (\<lambda>c. gen_obj_refs cp \<inter> gen_obj_refs c = {}) p' s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. p \<noteq> p'' \<and> (p = p' \<longrightarrow> (\<exists>cp. caps_of_state s p'' = Some cp \<and> gen_obj_refs cp \<noteq> {} \<and> (\<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap) \<and> (a, b) \<noteq> p'' \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> gen_obj_refs cp \<inter> gen_obj_refs cap = {})))) \<and> (p \<noteq> p' \<longrightarrow> (\<exists>cp. caps_of_state s p = Some cp \<and> gen_obj_refs cp \<noteq> {} \<and> (\<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap) \<and> (a, b) \<noteq> p \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> gen_obj_refs cp \<inter> gen_obj_refs cap = {}))))\<rbrace> cap_swap_for_delete p' p'' \<lbrace>\<lambda>rv s. \<exists>cp. caps_of_state s p = Some cp \<and> gen_obj_refs cp \<noteq> {} \<and> (\<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap) \<and> (a, b) \<noteq> p \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> gen_obj_refs cp \<inter> gen_obj_refs cap = {}))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. p \<noteq> p'' \<and> (p = p' \<longrightarrow> (\<exists>cp. caps_of_state s p'' = Some cp \<and> gen_obj_refs cp \<noteq> {} \<and> (\<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap) \<and> (a, b) \<noteq> p'' \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> gen_obj_refs cp \<inter> gen_obj_refs cap = {})))) \<and> (p \<noteq> p' \<longrightarrow> (\<exists>cp. caps_of_state s p = Some cp \<and> gen_obj_refs cp \<noteq> {} \<and> (\<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap) \<and> (a, b) \<noteq> p \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> gen_obj_refs cp \<inter> gen_obj_refs cap = {})))) \<Longrightarrow> \<exists>cp. (caps_of_state s \<circ> id(p' := p'', p'' := p')) p = Some cp \<and> gen_obj_refs cp \<noteq> {} \<and> (\<forall>a b. (\<exists>cap. (caps_of_state s \<circ> id(p' := p'', p'' := p')) (a, b) = Some cap) \<and> (a, b) \<noteq> p \<longrightarrow> (\<exists>cap. (caps_of_state s \<circ> id(p' := p'', p'' := p')) (a, b) = Some cap \<and> gen_obj_refs cp \<inter> gen_obj_refs cap = {})) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>p \<noteq> p'' \<and> (p = p' \<longrightarrow> (\<exists>cp. caps_of_state s p'' = Some cp \<and> gen_obj_refs cp \<noteq> {} \<and> (\<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap) \<and> (a, b) \<noteq> p'' \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> gen_obj_refs cp \<inter> gen_obj_refs cap = {})))) \<and> (p \<noteq> p' \<longrightarrow> (\<exists>cp. caps_of_state s p = Some cp \<and> gen_obj_refs cp \<noteq> {} \<and> (\<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap) \<and> (a, b) \<noteq> p \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> gen_obj_refs cp \<inter> gen_obj_refs cap = {})))); p = p'\<rbrakk> \<Longrightarrow> \<exists>cp. (caps_of_state s \<circ> id(p' := p'', p'' := p')) p = Some cp \<and> gen_obj_refs cp \<noteq> {} \<and> (\<forall>a b. (\<exists>cap. (caps_of_state s \<circ> id(p' := p'', p'' := p')) (a, b) = Some cap) \<and> (a, b) \<noteq> p \<longrightarrow> (\<exists>cap. (caps_of_state s \<circ> id(p' := p'', p'' := p')) (a, b) = Some cap \<and> gen_obj_refs cp \<inter> gen_obj_refs cap = {}))
 2. \<And>s. \<lbrakk>p \<noteq> p'' \<and> (p = p' \<longrightarrow> (\<exists>cp. caps_of_state s p'' = Some cp \<and> gen_obj_refs cp \<noteq> {} \<and> (\<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap) \<and> (a, b) \<noteq> p'' \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> gen_obj_refs cp \<inter> gen_obj_refs cap = {})))) \<and> (p \<noteq> p' \<longrightarrow> (\<exists>cp. caps_of_state s p = Some cp \<and> gen_obj_refs cp \<noteq> {} \<and> (\<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap) \<and> (a, b) \<noteq> p \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> gen_obj_refs cp \<inter> gen_obj_refs cap = {})))); p \<noteq> p'\<rbrakk> \<Longrightarrow> \<exists>cp. (caps_of_state s \<circ> id(p' := p'', p'' := p')) p = Some cp \<and> gen_obj_refs cp \<noteq> {} \<and> (\<forall>a b. (\<exists>cap. (caps_of_state s \<circ> id(p' := p'', p'' := p')) (a, b) = Some cap) \<and> (a, b) \<noteq> p \<longrightarrow> (\<exists>cap. (caps_of_state s \<circ> id(p' := p'', p'' := p')) (a, b) = Some cap \<and> gen_obj_refs cp \<inter> gen_obj_refs cap = {})) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>p \<noteq> p'' \<and> (p = p' \<longrightarrow> (\<exists>cp. caps_of_state s p'' = Some cp \<and> gen_obj_refs cp \<noteq> {} \<and> (\<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap) \<and> (a, b) \<noteq> p'' \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> gen_obj_refs cp \<inter> gen_obj_refs cap = {})))) \<and> (p \<noteq> p' \<longrightarrow> (\<exists>cp. caps_of_state s p = Some cp \<and> gen_obj_refs cp \<noteq> {} \<and> (\<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap) \<and> (a, b) \<noteq> p \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> gen_obj_refs cp \<inter> gen_obj_refs cap = {})))); p \<noteq> p'\<rbrakk> \<Longrightarrow> \<exists>cp. (caps_of_state s \<circ> id(p' := p'', p'' := p')) p = Some cp \<and> gen_obj_refs cp \<noteq> {} \<and> (\<forall>a b. (\<exists>cap. (caps_of_state s \<circ> id(p' := p'', p'' := p')) (a, b) = Some cap) \<and> (a, b) \<noteq> p \<longrightarrow> (\<exists>cap. (caps_of_state s \<circ> id(p' := p'', p'' := p')) (a, b) = Some cap \<and> gen_obj_refs cp \<inter> gen_obj_refs cap = {})) proof (prove)
goal (1 subgoal):
 1. \<And>s cp a b. \<lbrakk>p \<noteq> p'; p \<noteq> p''; caps_of_state s p = Some cp; gen_obj_refs cp \<noteq> {}; \<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap) \<and> (a, b) \<noteq> p \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> gen_obj_refs cp \<inter> gen_obj_refs cap = {})\<rbrakk> \<Longrightarrow> ((a, b) = p' \<longrightarrow> (\<exists>cap. caps_of_state s p'' = Some cap) \<longrightarrow> (\<exists>cap. caps_of_state s p'' = Some cap \<and> gen_obj_refs cp \<inter> gen_obj_refs cap = {})) \<and> ((a, b) \<noteq> p' \<longrightarrow> (a, b) = p'' \<longrightarrow> (\<exists>cap. caps_of_state s p' = Some cap) \<longrightarrow> (\<exists>cap. caps_of_state s p' = Some cap \<and> gen_obj_refs cp \<inter> gen_obj_refs cap = {})) proof (prove)
goal:
No subgoals!