theory CNodeInv_R

lemma reduceZombie_cap_to:
  "\<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> (\<not> exposed \<longrightarrow> ex_cte_cap_to' slot s)
           \<and> cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s\<rbrace>
     reduceZombie cap slot exposed
   \<lbrace>\<lambda>rv s. \<not> exposed \<longrightarrow> ex_cte_cap_to' slot s\<rbrace>, -" apply (rule validE_validE_R, rule hoare_pre,
         rule hoare_post_impErr) apply (rule reduceZombie_invs'[where p=slot]) apply clarsimp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. invs' s \<and> sch_act_simple s \<and> (\<not> exposed \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<and> cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s\<rbrace> reduceZombie cap slot exposed \<lbrace>\<lambda>rv s. \<not> exposed \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s\<rbrace>, - proof (prove)
goal (4 subgoals):
 1. \<lbrace>?Q2\<rbrace> reduceZombie cap slot exposed \<lbrace>?Q5\<rbrace>, \<lbrace>?E5\<rbrace>
 2. \<And>rv s. ?Q5 rv s \<Longrightarrow> \<not> exposed \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s
 3. \<And>e s. ?E5 e s \<Longrightarrow> True
 4. \<And>s. invs' s \<and> sch_act_simple s \<and> (\<not> exposed \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<and> cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s \<Longrightarrow> ?Q2 s proof (prove)
goal (4 subgoals):
 1. \<And>s s'' rv sa. \<lbrakk>\<not> (isZombie cap \<and> capZombieNumber cap = 0); \<not> (isZombie cap \<and> \<not> exposed); isZombie cap \<and> exposed; (Inr rv, s'') \<in> fst ((withoutPreemption $ locateSlotCap cap (fromIntegral (capZombieNumber cap - 1))) s); invs' sa \<and> sch_act_simple sa \<and> cte_wp_at' (\<lambda>cte. isZombie (cteCap cte)) slot sa \<and> ex_cte_cap_wp_to' (\<lambda>_. True) rv sa\<rbrakk> \<Longrightarrow> invs' sa \<and> sch_act_simple sa \<and> (\<not> False \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) rv sa)
 2. \<And>rv s. invs' s \<and> sch_act_simple s \<and> (exposed \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<and> (exposed \<or> slot = slot \<or> cte_wp_at' (\<lambda>cte. (?P9 and isZombie) (cteCap cte) \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie slot zb n \<and> ?P9 cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> slot))) slot s) \<Longrightarrow> \<not> exposed \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s
 3. \<And>e s. invs' s \<and> sch_act_simple s \<Longrightarrow> True
 4. \<And>s. invs' s \<and> sch_act_simple s \<and> (\<not> exposed \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<and> cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s \<Longrightarrow> invs' s \<and> sch_act_simple s \<and> (exposed \<or> ex_cte_cap_wp_to' (\<lambda>_. True) slot s) \<and> cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s \<and> (exposed \<or> slot = slot \<or> cte_wp_at' (\<lambda>cte. (?P9 and isZombie) (cteCap cte) \<or> (\<exists>zb n cp. cteCap cte = capability.Zombie slot zb n \<and> ?P9 cp \<and> (isZombie cp \<longrightarrow> capZombiePtr cp \<noteq> slot))) slot s) proof (prove)
goal:
No subgoals!