theory CNodeInv_R

lemma capSwap_rvk_prog:
  "\<lbrace>\<lambda>s. revoke_progress_ord m (option_map capToRPO \<circ> cteCaps_of s)
           \<and> cte_wp_at' (\<lambda>cte. \<exists>n. (capToRPO (cteCap cte)) = (Some p1, Suc n)) p2 s
           \<and> cte_wp_at' (\<lambda>cte. fst (capToRPO (cteCap cte)) \<noteq> Some p1) p1 s\<rbrace>
     capSwapForDelete p1 p2
   \<lbrace>\<lambda>rv s. revoke_progress_ord m (option_map capToRPO \<circ> cteCaps_of s)\<rbrace>" apply wp apply (clarsimp simp: cte_wp_at_ctes_of cteCaps_of_def) apply (cases "p1 = p2") apply simp apply (erule rpo_trans) apply (rule rpo_delta[where S="{p1, p2}"], simp_all) apply (simp add: Int_insert_left dom_def) apply (case_tac "capToRPO (cteCap ctea)") apply simp apply arith done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. revoke_progress_ord m (map_option capToRPO \<circ> cteCaps_of s) \<and> cte_wp_at' (\<lambda>cte. \<exists>n. capToRPO (cteCap cte) = (Some p1, Suc n)) p2 s \<and> cte_wp_at' (\<lambda>cte. fst (capToRPO (cteCap cte)) \<noteq> Some p1) p1 s\<rbrace> capSwapForDelete p1 p2 \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option capToRPO \<circ> cteCaps_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. revoke_progress_ord m (map_option capToRPO \<circ> cteCaps_of s) \<and> cte_wp_at' (\<lambda>cte. \<exists>n. capToRPO (cteCap cte) = (Some p1, Suc n)) p2 s \<and> cte_wp_at' (\<lambda>cte. fst (capToRPO (cteCap cte)) \<noteq> Some p1) p1 s \<Longrightarrow> revoke_progress_ord m (map_option capToRPO \<circ> (cteCaps_of s \<circ> id(p1 := p2, p2 := p1))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte ctea n. \<lbrakk>revoke_progress_ord m (map_option capToRPO \<circ> (map_option cteCap \<circ> ctes_of s)); ctes_of s p2 = Some cte; capToRPO (cteCap cte) = (Some p1, Suc n); ctes_of s p1 = Some ctea; fst (capToRPO (cteCap ctea)) \<noteq> Some p1\<rbrakk> \<Longrightarrow> revoke_progress_ord m (\<lambda>a. map_option capToRPO (map_option cteCap (ctes_of s (if a = p2 then p1 else if a = p1 then p2 else a)))) proof (prove)
goal (2 subgoals):
 1. \<And>s cte ctea n. \<lbrakk>revoke_progress_ord m (map_option capToRPO \<circ> (map_option cteCap \<circ> ctes_of s)); ctes_of s p2 = Some cte; capToRPO (cteCap cte) = (Some p1, Suc n); ctes_of s p1 = Some ctea; fst (capToRPO (cteCap ctea)) \<noteq> Some p1; p1 = p2\<rbrakk> \<Longrightarrow> revoke_progress_ord m (\<lambda>a. map_option capToRPO (map_option cteCap (ctes_of s (if a = p2 then p1 else if a = p1 then p2 else a))))
 2. \<And>s cte ctea n. \<lbrakk>revoke_progress_ord m (map_option capToRPO \<circ> (map_option cteCap \<circ> ctes_of s)); ctes_of s p2 = Some cte; capToRPO (cteCap cte) = (Some p1, Suc n); ctes_of s p1 = Some ctea; fst (capToRPO (cteCap ctea)) \<noteq> Some p1; p1 \<noteq> p2\<rbrakk> \<Longrightarrow> revoke_progress_ord m (\<lambda>a. map_option capToRPO (map_option cteCap (ctes_of s (if a = p2 then p1 else if a = p1 then p2 else a)))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte ctea n. \<lbrakk>revoke_progress_ord m (map_option capToRPO \<circ> (map_option cteCap \<circ> ctes_of s)); ctes_of s p2 = Some cte; capToRPO (cteCap cte) = (Some p1, Suc n); ctes_of s p1 = Some ctea; fst (capToRPO (cteCap ctea)) \<noteq> Some p1; p1 \<noteq> p2\<rbrakk> \<Longrightarrow> revoke_progress_ord m (\<lambda>a. map_option capToRPO (map_option cteCap (ctes_of s (if a = p2 then p1 else if a = p1 then p2 else a)))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte ctea n. \<lbrakk>ctes_of s p2 = Some cte; capToRPO (cteCap cte) = (Some p1, Suc n); ctes_of s p1 = Some ctea; fst (capToRPO (cteCap ctea)) \<noteq> Some p1; p1 \<noteq> p2\<rbrakk> \<Longrightarrow> revoke_progress_ord (map_option capToRPO \<circ> (map_option cteCap \<circ> ctes_of s)) (\<lambda>a. map_option capToRPO (map_option cteCap (ctes_of s (if a = p2 then p1 else if a = p1 then p2 else a)))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte ctea n. \<lbrakk>ctes_of s p2 = Some cte; capToRPO (cteCap cte) = (Some p1, Suc n); ctes_of s p1 = Some ctea; fst (capToRPO (cteCap ctea)) \<noteq> Some p1; p1 \<noteq> p2\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>{p1, p2} \<inter> dom (\<lambda>a. map_option capToRPO (map_option cteCap (ctes_of s (if a = p2 then p1 else if a = p1 then p2 else a)))). rpo_measure x (map_option capToRPO (map_option cteCap (ctes_of s (if x = p2 then p1 else if x = p1 then p2 else x))))) < (\<Sum>x\<in>{p1, p2} \<inter> dom (ctes_of s). rpo_measure x (map_option capToRPO (map_option cteCap (ctes_of s x)))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte ctea n. \<lbrakk>ctes_of s p2 = Some cte; capToRPO (cteCap cte) = (Some p1, Suc n); ctes_of s p1 = Some ctea; fst (capToRPO (cteCap ctea)) \<noteq> Some p1; p1 \<noteq> p2\<rbrakk> \<Longrightarrow> rpo_measure p2 (Some (capToRPO (cteCap ctea))) < Suc (rpo_measure p1 (Some (capToRPO (cteCap ctea)))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte ctea n a b. \<lbrakk>ctes_of s p2 = Some cte; capToRPO (cteCap cte) = (Some p1, Suc n); ctes_of s p1 = Some ctea; fst (capToRPO (cteCap ctea)) \<noteq> Some p1; p1 \<noteq> p2; capToRPO (cteCap ctea) = (a, b)\<rbrakk> \<Longrightarrow> rpo_measure p2 (Some (capToRPO (cteCap ctea))) < Suc (rpo_measure p1 (Some (capToRPO (cteCap ctea)))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte ctea n a b. \<lbrakk>ctes_of s p2 = Some cte; capToRPO (cteCap cte) = (Some p1, Suc n); ctes_of s p1 = Some ctea; a \<noteq> Some p1; p1 \<noteq> p2; capToRPO (cteCap ctea) = (a, b)\<rbrakk> \<Longrightarrow> a = Some p2 \<longrightarrow> b - Suc 0 < Suc b proof (prove)
goal:
No subgoals!