theory CNodeInv_R

lemma cteDelete_delete_cases:
  "\<lbrace>\<top>\<rbrace>
     cteDelete slot e
   \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>c. cteCap c = NullCap
                       \<or> \<not> e \<and> isZombie (cteCap c)
                           \<and> capZombiePtr (cteCap c) = slot) slot\<rbrace>, -" apply (simp add: cteDelete_def whenE_def split_def) apply wp apply (rule hoare_strengthen_post [OF emptySlot_deletes]) apply (clarsimp simp: cte_wp_at_ctes_of) apply wp+ apply (rule hoare_post_imp_R, rule finaliseSlot_abort_cases) apply (clarsimp simp: cte_wp_at_ctes_of) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> cteDelete slot e \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap \<or> \<not> e \<and> isZombie (cteCap c) \<and> capZombiePtr (cteCap c) = slot) slot\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> doE p <- finaliseSlot slot e;
if e \<or> fst p then liftE (emptySlot slot (snd p)) else returnOk ()
odE \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap \<or> \<not> e \<and> isZombie (cteCap c) \<and> capZombiePtr (cteCap c) = slot) slot\<rbrace>, - proof (prove)
goal (4 subgoals):
 1. \<And>p. e \<or> fst p \<Longrightarrow> \<lbrace>?Qa2 p\<rbrace> emptySlot slot (snd p) \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap \<or> \<not> e \<and> isZombie (cteCap c) \<and> capZombiePtr (cteCap c) = slot) slot\<rbrace>
 2. \<And>p. \<not> (e \<or> fst p) \<Longrightarrow> \<lbrace>?R2 p\<rbrace> returnOk () \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap \<or> \<not> e \<and> isZombie (cteCap c) \<and> capZombiePtr (cteCap c) = slot) slot\<rbrace>, -
 3. \<lbrace>?P'\<rbrace> finaliseSlot slot e \<lbrace>\<lambda>p s. (e \<or> fst p \<longrightarrow> ?Qa2 p s) \<and> (\<not> (e \<or> fst p) \<longrightarrow> ?R2 p s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>s. True \<Longrightarrow> ?P' s proof (prove)
goal (4 subgoals):
 1. \<And>p rv s. \<lbrakk>e \<or> fst p; cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) slot s\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap \<or> \<not> e \<and> isZombie (cteCap c) \<and> capZombiePtr (cteCap c) = slot) slot s
 2. \<And>p. \<not> (e \<or> fst p) \<Longrightarrow> \<lbrace>?R2 p\<rbrace> returnOk () \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap \<or> \<not> e \<and> isZombie (cteCap c) \<and> capZombiePtr (cteCap c) = slot) slot\<rbrace>, -
 3. \<lbrace>?P'\<rbrace> finaliseSlot slot e \<lbrace>\<lambda>p s. (e \<or> fst p \<longrightarrow> True) \<and> (\<not> (e \<or> fst p) \<longrightarrow> ?R2 p s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>s. True \<Longrightarrow> ?P' s proof (prove)
goal (3 subgoals):
 1. \<And>p. \<not> (e \<or> fst p) \<Longrightarrow> \<lbrace>?R2 p\<rbrace> returnOk () \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap \<or> \<not> e \<and> isZombie (cteCap c) \<and> capZombiePtr (cteCap c) = slot) slot\<rbrace>, -
 2. \<lbrace>?P'\<rbrace> finaliseSlot slot e \<lbrace>\<lambda>p s. (e \<or> fst p \<longrightarrow> True) \<and> (\<not> (e \<or> fst p) \<longrightarrow> ?R2 p s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>s. True \<Longrightarrow> ?P' s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'16\<rbrace> finaliseSlot slot e \<lbrace>\<lambda>p s. (e \<or> fst p \<longrightarrow> True) \<and> (\<not> (e \<or> fst p) \<longrightarrow> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap \<or> \<not> e \<and> isZombie (cteCap c) \<and> capZombiePtr (cteCap c) = slot) slot s)\<rbrace>, -
 2. \<And>s. True \<Longrightarrow> True \<and> ?P'16 s proof (prove)
goal (2 subgoals):
 1. \<And>rv s. fst rv \<or> \<not> e \<and> cte_wp_at' (\<lambda>cte. isZombie (cteCap cte) \<and> capZombiePtr (cteCap cte) = slot) slot s \<Longrightarrow> (e \<or> fst rv \<longrightarrow> True) \<and> (\<not> (e \<or> fst rv) \<longrightarrow> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap \<or> \<not> e \<and> isZombie (cteCap c) \<and> capZombiePtr (cteCap c) = slot) slot s)
 2. \<And>s. True \<Longrightarrow> True \<and> True proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> True \<and> True proof (prove)
goal:
No subgoals!