theory CNodeInv_R

lemma updateCap_not_recursive:
  "\<lbrace>\<lambda>s. card (not_recursive_ctes s) \<le> n
         \<and> cte_wp_at' (\<lambda>cte. isZombie (cteCap cte) \<and> capZombiePtr (cteCap cte) = ptr
                                \<longrightarrow> isZombie cap \<and> capZombiePtr cap = ptr)
               ptr s\<rbrace>
     updateCap ptr cap
   \<lbrace>\<lambda>rv s. card (not_recursive_ctes s) \<le> n\<rbrace>" apply (simp add: not_recursive_ctes_def) apply wp apply clarsimp apply (erule order_trans[rotated]) apply (rule card_mono, simp) apply clarsimp apply (simp add: modify_map_def split: if_split_asm) apply (clarsimp simp: cteCaps_of_def cte_wp_at_ctes_of) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. card (not_recursive_ctes s) \<le> n \<and> cte_wp_at' (\<lambda>cte. isZombie (cteCap cte) \<and> capZombiePtr (cteCap cte) = ptr \<longrightarrow> isZombie cap \<and> capZombiePtr cap = ptr) ptr s\<rbrace> updateCap ptr cap \<lbrace>\<lambda>rv s. card (not_recursive_ctes s) \<le> n\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. card {ptr. \<exists>cap. cteCaps_of s ptr = Some cap \<and> (isZombie cap \<longrightarrow> capZombiePtr cap \<noteq> ptr)} \<le> n \<and> cte_wp_at' (\<lambda>cte. isZombie (cteCap cte) \<and> capZombiePtr (cteCap cte) = ptr \<longrightarrow> isZombie cap \<and> capZombiePtr cap = ptr) ptr s\<rbrace> updateCap ptr cap \<lbrace>\<lambda>rv s. card {ptr. \<exists>cap. cteCaps_of s ptr = Some cap \<and> (isZombie cap \<longrightarrow> capZombiePtr cap \<noteq> ptr)} \<le> n\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. card {ptr. \<exists>cap. cteCaps_of s ptr = Some cap \<and> (isZombie cap \<longrightarrow> capZombiePtr cap \<noteq> ptr)} \<le> n \<and> cte_wp_at' (\<lambda>cte. isZombie (cteCap cte) \<and> capZombiePtr (cteCap cte) = ptr \<longrightarrow> isZombie cap \<and> capZombiePtr cap = ptr) ptr s \<Longrightarrow> card {ptra. \<exists>capa. modify_map (cteCaps_of s) ptr (K cap) ptra = Some capa \<and> (isZombie capa \<longrightarrow> capZombiePtr capa \<noteq> ptra)} \<le> n proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>card {ptr. \<exists>cap. cteCaps_of s ptr = Some cap \<and> (isZombie cap \<longrightarrow> capZombiePtr cap \<noteq> ptr)} \<le> n; cte_wp_at' (\<lambda>cte. isZombie (cteCap cte) \<and> capZombiePtr (cteCap cte) = ptr \<longrightarrow> isZombie cap \<and> capZombiePtr cap = ptr) ptr s\<rbrakk> \<Longrightarrow> card {ptra. \<exists>capa. modify_map (cteCaps_of s) ptr (\<lambda>y. cap) ptra = Some capa \<and> (isZombie capa \<longrightarrow> capZombiePtr capa \<noteq> ptra)} \<le> n proof (prove)
goal (1 subgoal):
 1. \<And>s. cte_wp_at' (\<lambda>cte. isZombie (cteCap cte) \<and> capZombiePtr (cteCap cte) = ptr \<longrightarrow> isZombie cap \<and> capZombiePtr cap = ptr) ptr s \<Longrightarrow> card {ptra. \<exists>capa. modify_map (cteCaps_of s) ptr (\<lambda>y. cap) ptra = Some capa \<and> (isZombie capa \<longrightarrow> capZombiePtr capa \<noteq> ptra)} \<le> card {ptr. \<exists>cap. cteCaps_of s ptr = Some cap \<and> (isZombie cap \<longrightarrow> capZombiePtr cap \<noteq> ptr)} proof (prove)
goal (1 subgoal):
 1. \<And>s. cte_wp_at' (\<lambda>cte. isZombie (cteCap cte) \<and> capZombiePtr (cteCap cte) = ptr \<longrightarrow> isZombie cap \<and> capZombiePtr cap = ptr) ptr s \<Longrightarrow> {ptra. \<exists>capa. modify_map (cteCaps_of s) ptr (\<lambda>y. cap) ptra = Some capa \<and> (isZombie capa \<longrightarrow> capZombiePtr capa \<noteq> ptra)} \<subseteq> {ptr. \<exists>cap. cteCaps_of s ptr = Some cap \<and> (isZombie cap \<longrightarrow> capZombiePtr cap \<noteq> ptr)} proof (prove)
goal (1 subgoal):
 1. \<And>s x capa. \<lbrakk>cte_wp_at' (\<lambda>cte. isZombie (cteCap cte) \<and> capZombiePtr (cteCap cte) = ptr \<longrightarrow> isZombie cap \<and> capZombiePtr cap = ptr) ptr s; modify_map (cteCaps_of s) ptr (\<lambda>y. cap) x = Some capa; isZombie capa \<longrightarrow> capZombiePtr capa \<noteq> x\<rbrakk> \<Longrightarrow> \<exists>cap. cteCaps_of s x = Some cap \<and> (isZombie cap \<longrightarrow> capZombiePtr cap \<noteq> x) proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>isZombie cap \<longrightarrow> capZombiePtr cap \<noteq> ptr; cte_wp_at' (\<lambda>cte. isZombie (cteCap cte) \<and> capZombiePtr (cteCap cte) = ptr \<longrightarrow> isZombie cap \<and> capZombiePtr cap = ptr) ptr s; x = ptr; \<exists>z. cteCaps_of s ptr = Some z\<rbrakk> \<Longrightarrow> \<exists>cap. cteCaps_of s ptr = Some cap \<and> (isZombie cap \<longrightarrow> capZombiePtr cap \<noteq> ptr) proof (prove)
goal:
No subgoals!