theory CNodeInv_AI

lemma rvk_prog_update_strg:
  "revoke_progress_ord m (option_map cap_to_rpo \<circ> caps_of_state s)
        \<and> cte_wp_at (\<lambda>cp. cap_to_rpo cp = cap_to_rpo cap
                         \<or> rpo_measure p (Some (cap_to_rpo cp))
                             > rpo_measure p (Some (cap_to_rpo cap))) p s
      \<longrightarrow> revoke_progress_ord m (option_map cap_to_rpo \<circ> ((caps_of_state s) (p \<mapsto> cap)))" apply (clarsimp simp: cte_wp_at_caps_of_state) apply (erule disjE) apply (erule rsubst[where P="\<lambda>mp. revoke_progress_ord m mp"]) apply (rule ext, simp) apply (erule rpo_trans) apply (rule rpo_delta[where S="{p}"],
         simp_all add: dom_def caps_of_state_set_finite) apply (rule exception_set_finite) apply (rule finite_subset [OF _ caps_of_state_set_finite(2)[where s=s]]) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<and> cte_wp_at (\<lambda>cp. cap_to_rpo cp = cap_to_rpo cap \<or> rpo_measure p (Some (cap_to_rpo cap)) < rpo_measure p (Some (cap_to_rpo cp))) p s \<longrightarrow> revoke_progress_ord m (map_option cap_to_rpo \<circ> (caps_of_state s)(p \<mapsto> cap)) proof (prove)
goal (1 subgoal):
 1. \<And>capa. \<lbrakk>revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s); caps_of_state s p = Some capa; cap_to_rpo capa = cap_to_rpo cap \<or> rpo_measure p (Some (cap_to_rpo cap)) < rpo_measure p (Some (cap_to_rpo capa))\<rbrakk> \<Longrightarrow> revoke_progress_ord m ((map_option cap_to_rpo \<circ> caps_of_state s)(p \<mapsto> cap_to_rpo cap)) proof (prove)
goal (2 subgoals):
 1. \<And>capa. \<lbrakk>revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s); caps_of_state s p = Some capa; cap_to_rpo capa = cap_to_rpo cap\<rbrakk> \<Longrightarrow> revoke_progress_ord m ((map_option cap_to_rpo \<circ> caps_of_state s)(p \<mapsto> cap_to_rpo cap))
 2. \<And>capa. \<lbrakk>revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s); caps_of_state s p = Some capa; rpo_measure p (Some (cap_to_rpo cap)) < rpo_measure p (Some (cap_to_rpo capa))\<rbrakk> \<Longrightarrow> revoke_progress_ord m ((map_option cap_to_rpo \<circ> caps_of_state s)(p \<mapsto> cap_to_rpo cap)) proof (prove)
goal (2 subgoals):
 1. \<And>capa. \<lbrakk>caps_of_state s p = Some capa; cap_to_rpo capa = cap_to_rpo cap\<rbrakk> \<Longrightarrow> map_option cap_to_rpo \<circ> caps_of_state s = (map_option cap_to_rpo \<circ> caps_of_state s)(p \<mapsto> cap_to_rpo cap)
 2. \<And>capa. \<lbrakk>revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s); caps_of_state s p = Some capa; rpo_measure p (Some (cap_to_rpo cap)) < rpo_measure p (Some (cap_to_rpo capa))\<rbrakk> \<Longrightarrow> revoke_progress_ord m ((map_option cap_to_rpo \<circ> caps_of_state s)(p \<mapsto> cap_to_rpo cap)) proof (prove)
goal (1 subgoal):
 1. \<And>capa. \<lbrakk>revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s); caps_of_state s p = Some capa; rpo_measure p (Some (cap_to_rpo cap)) < rpo_measure p (Some (cap_to_rpo capa))\<rbrakk> \<Longrightarrow> revoke_progress_ord m ((map_option cap_to_rpo \<circ> caps_of_state s)(p \<mapsto> cap_to_rpo cap)) proof (prove)
goal (1 subgoal):
 1. \<And>capa. \<lbrakk>caps_of_state s p = Some capa; rpo_measure p (Some (cap_to_rpo cap)) < rpo_measure p (Some (cap_to_rpo capa))\<rbrakk> \<Longrightarrow> revoke_progress_ord (map_option cap_to_rpo \<circ> caps_of_state s) ((map_option cap_to_rpo \<circ> caps_of_state s)(p \<mapsto> cap_to_rpo cap)) proof (prove)
goal (1 subgoal):
 1. \<And>capa. \<lbrakk>caps_of_state s p = Some capa; rpo_measure p (Some (cap_to_rpo cap)) < rpo_measure p (Some (cap_to_rpo capa))\<rbrakk> \<Longrightarrow> finite {a. a \<noteq> p \<longrightarrow> (\<exists>aa b z. caps_of_state s a = Some z \<and> cap_to_rpo z = (aa, b))} proof (prove)
goal (1 subgoal):
 1. \<And>capa. \<lbrakk>caps_of_state s p = Some capa; rpo_measure p (Some (cap_to_rpo cap)) < rpo_measure p (Some (cap_to_rpo capa))\<rbrakk> \<Longrightarrow> finite {a. \<exists>aa b z. caps_of_state s a = Some z \<and> cap_to_rpo z = (aa, b)} proof (prove)
goal (1 subgoal):
 1. \<And>capa. \<lbrakk>caps_of_state s p = Some capa; rpo_measure p (Some (cap_to_rpo cap)) < rpo_measure p (Some (cap_to_rpo capa))\<rbrakk> \<Longrightarrow> {a. \<exists>aa b z. caps_of_state s a = Some z \<and> cap_to_rpo z = (aa, b)} \<subseteq> {p. \<exists>cap. caps_of_state s p = Some cap} proof (prove)
goal:
No subgoals!