theory CNodeInv_AI

lemma final_cap_still_at:
  "\<lbrace>\<lambda>s. cte_wp_at (\<lambda>c. gen_obj_refs cap = gen_obj_refs c
                         \<and> P cap (is_final_cap' c s)) ptr s\<rbrace>
     set_cap cap ptr
   \<lbrace>\<lambda>rv s. cte_wp_at (\<lambda>c. P c (is_final_cap' c s)) ptr s\<rbrace>" apply (simp add: is_final_cap'_def2 cte_wp_at_caps_of_state) apply wp apply (clarsimp elim!: rsubst[where P="P cap"]) apply (intro ext arg_cong[where f=Ex] arg_cong[where f=All]) apply (case_tac "(aa, ba) = ptr", simp_all add: gen_obj_refs_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cte_wp_at (\<lambda>c. gen_obj_refs cap = gen_obj_refs c \<and> P cap (is_final_cap' c s)) ptr s\<rbrace> set_cap cap ptr \<lbrace>\<lambda>rv s. cte_wp_at (\<lambda>c. P c (is_final_cap' c s)) ptr s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<exists>capa. caps_of_state s ptr = Some capa \<and> gen_obj_refs cap = gen_obj_refs capa \<and> P cap (\<exists>a b. \<forall>aa ba. (\<exists>cap. caps_of_state s (aa, ba) = Some cap \<and> gen_obj_refs capa \<inter> gen_obj_refs cap \<noteq> {}) = (aa = a \<and> ba = b))\<rbrace> set_cap cap ptr \<lbrace>\<lambda>rv s. \<exists>cap. caps_of_state s ptr = Some cap \<and> P cap (\<exists>a b. \<forall>aa ba. (\<exists>capa. caps_of_state s (aa, ba) = Some capa \<and> gen_obj_refs cap \<inter> gen_obj_refs capa \<noteq> {}) = (aa = a \<and> ba = b))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<exists>capa. caps_of_state s ptr = Some capa \<and> gen_obj_refs cap = gen_obj_refs capa \<and> P cap (\<exists>a b. \<forall>aa ba. (\<exists>cap. caps_of_state s (aa, ba) = Some cap \<and> gen_obj_refs capa \<inter> gen_obj_refs cap \<noteq> {}) = (aa = a \<and> ba = b)) \<Longrightarrow> \<exists>capa. ((caps_of_state s)(ptr \<mapsto> cap)) ptr = Some capa \<and> P capa (\<exists>a b. \<forall>aa ba. (\<exists>capb. ((caps_of_state s)(ptr \<mapsto> cap)) (aa, ba) = Some capb \<and> gen_obj_refs capa \<inter> gen_obj_refs capb \<noteq> {}) = (aa = a \<and> ba = b)) proof (prove)
goal (1 subgoal):
 1. \<And>s capa. \<lbrakk>caps_of_state s ptr = Some capa; gen_obj_refs cap = gen_obj_refs capa\<rbrakk> \<Longrightarrow> (\<exists>a b. \<forall>aa ba. (\<exists>cap. caps_of_state s (aa, ba) = Some cap \<and> gen_obj_refs capa \<inter> gen_obj_refs cap \<noteq> {}) = (aa = a \<and> ba = b)) = (\<exists>a b. \<forall>aa ba. ((aa, ba) = ptr \<longrightarrow> (gen_obj_refs capa \<noteq> {}) = (aa = a \<and> ba = b)) \<and> ((aa, ba) \<noteq> ptr \<longrightarrow> (\<exists>cap. caps_of_state s (aa, ba) = Some cap \<and> gen_obj_refs capa \<inter> gen_obj_refs cap \<noteq> {}) = (aa = a \<and> ba = b))) proof (prove)
goal (1 subgoal):
 1. \<And>s capa a b aa ba. \<lbrakk>caps_of_state s ptr = Some capa; gen_obj_refs cap = gen_obj_refs capa\<rbrakk> \<Longrightarrow> ((\<exists>cap. caps_of_state s (aa, ba) = Some cap \<and> gen_obj_refs capa \<inter> gen_obj_refs cap \<noteq> {}) = (aa = a \<and> ba = b)) = (((aa, ba) = ptr \<longrightarrow> (gen_obj_refs capa \<noteq> {}) = (aa = a \<and> ba = b)) \<and> ((aa, ba) \<noteq> ptr \<longrightarrow> (\<exists>cap. caps_of_state s (aa, ba) = Some cap \<and> gen_obj_refs capa \<inter> gen_obj_refs cap \<noteq> {}) = (aa = a \<and> ba = b))) proof (prove)
goal:
No subgoals!