theory CNodeInv_R

lemma rvk_prog_modify_map:
  "\<lbrakk> \<And>x. Some x = m p \<Longrightarrow>
          capToRPO (f x) = capToRPO x
       \<or> rpo_measure p (Some (capToRPO (f x)))
           < rpo_measure p (Some (capToRPO x)) \<rbrakk>
    \<Longrightarrow> revoke_progress_ord (option_map capToRPO \<circ> m) (option_map capToRPO \<circ> (modify_map m p f))" apply (cases "m p") apply (simp add: modify_map_def fun_upd_idem) apply (simp add: revoke_progress_ord_def) apply simp apply (erule disjE) apply (simp add: modify_map_def fun_upd_idem) apply (simp add: revoke_progress_ord_def) apply (rule rpo_delta[where S="{p}"],
         simp_all add: modify_map_def dom_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x. Some x = m p \<Longrightarrow> capToRPO (f x) = capToRPO x \<or> rpo_measure p (Some (capToRPO (f x))) < rpo_measure p (Some (capToRPO x))) \<Longrightarrow> revoke_progress_ord (map_option capToRPO \<circ> m) (map_option capToRPO \<circ> modify_map m p f) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>x. Some x = m p \<Longrightarrow> capToRPO (f x) = capToRPO x \<or> rpo_measure p (Some (capToRPO (f x))) < rpo_measure p (Some (capToRPO x)); m p = None\<rbrakk> \<Longrightarrow> revoke_progress_ord (map_option capToRPO \<circ> m) (map_option capToRPO \<circ> modify_map m p f)
 2. \<And>a. \<lbrakk>\<And>x. Some x = m p \<Longrightarrow> capToRPO (f x) = capToRPO x \<or> rpo_measure p (Some (capToRPO (f x))) < rpo_measure p (Some (capToRPO x)); m p = Some a\<rbrakk> \<Longrightarrow> revoke_progress_ord (map_option capToRPO \<circ> m) (map_option capToRPO \<circ> modify_map m p f) proof (prove)
goal (2 subgoals):
 1. m p = None \<Longrightarrow> revoke_progress_ord (map_option capToRPO \<circ> m) (map_option capToRPO \<circ> m)
 2. \<And>a. \<lbrakk>\<And>x. Some x = m p \<Longrightarrow> capToRPO (f x) = capToRPO x \<or> rpo_measure p (Some (capToRPO (f x))) < rpo_measure p (Some (capToRPO x)); m p = Some a\<rbrakk> \<Longrightarrow> revoke_progress_ord (map_option capToRPO \<circ> m) (map_option capToRPO \<circ> modify_map m p f) proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>\<And>x. Some x = m p \<Longrightarrow> capToRPO (f x) = capToRPO x \<or> rpo_measure p (Some (capToRPO (f x))) < rpo_measure p (Some (capToRPO x)); m p = Some a\<rbrakk> \<Longrightarrow> revoke_progress_ord (map_option capToRPO \<circ> m) (map_option capToRPO \<circ> modify_map m p f) proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>capToRPO (f a) = capToRPO a \<or> rpo_measure p (Some (capToRPO (f a))) < rpo_measure p (Some (capToRPO a)); m p = Some a\<rbrakk> \<Longrightarrow> revoke_progress_ord (map_option capToRPO \<circ> m) (map_option capToRPO \<circ> modify_map m p f) proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>m p = Some a; capToRPO (f a) = capToRPO a\<rbrakk> \<Longrightarrow> revoke_progress_ord (map_option capToRPO \<circ> m) (map_option capToRPO \<circ> modify_map m p f)
 2. \<And>a. \<lbrakk>m p = Some a; rpo_measure p (Some (capToRPO (f a))) < rpo_measure p (Some (capToRPO a))\<rbrakk> \<Longrightarrow> revoke_progress_ord (map_option capToRPO \<circ> m) (map_option capToRPO \<circ> modify_map m p f) proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>m p = Some a; capToRPO (f a) = capToRPO a\<rbrakk> \<Longrightarrow> revoke_progress_ord (map_option capToRPO \<circ> m) (map_option capToRPO \<circ> m)
 2. \<And>a. \<lbrakk>m p = Some a; rpo_measure p (Some (capToRPO (f a))) < rpo_measure p (Some (capToRPO a))\<rbrakk> \<Longrightarrow> revoke_progress_ord (map_option capToRPO \<circ> m) (map_option capToRPO \<circ> modify_map m p f) proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>m p = Some a; rpo_measure p (Some (capToRPO (f a))) < rpo_measure p (Some (capToRPO a))\<rbrakk> \<Longrightarrow> revoke_progress_ord (map_option capToRPO \<circ> m) (map_option capToRPO \<circ> modify_map m p f) proof (prove)
goal:
No subgoals!