theory CSpace1_R

lemma revokable_relation_next [simp]:
  "revokable_relation revo cs (modify_map m p (cteMDBNode_update (mdbNext_update f))) =
  revokable_relation revo cs m" apply (rule iffI) apply (clarsimp simp add: revokable_relation_def) apply (erule allE, erule allE, erule impE, erule exI) apply (clarsimp simp: modify_map_def split: if_split_asm) apply (clarsimp simp add: revokable_relation_def modify_map_def) apply (erule allE, erule allE, erule impE, erule exI) apply (case_tac z) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. revokable_relation revo cs (modify_map m p (cteMDBNode_update (mdbNext_update f))) = revokable_relation revo cs m proof (prove)
goal (2 subgoals):
 1. revokable_relation revo cs (modify_map m p (cteMDBNode_update (mdbNext_update f))) \<Longrightarrow> revokable_relation revo cs m
 2. revokable_relation revo cs m \<Longrightarrow> revokable_relation revo cs (modify_map m p (cteMDBNode_update (mdbNext_update f))) proof (prove)
goal (2 subgoals):
 1. \<And>a b y cap node. \<lbrakk>\<forall>a b. (\<exists>y. cs (a, b) = Some y) \<longrightarrow> (\<forall>cap node. modify_map m p (cteMDBNode_update (mdbNext_update f)) (cte_map (a, b)) = Some (CTE cap node) \<longrightarrow> revo (a, b) = mdbRevocable node); cs (a, b) = Some y; m (cte_map (a, b)) = Some (CTE cap node)\<rbrakk> \<Longrightarrow> revo (a, b) = mdbRevocable node
 2. revokable_relation revo cs m \<Longrightarrow> revokable_relation revo cs (modify_map m p (cteMDBNode_update (mdbNext_update f))) proof (prove)
goal (2 subgoals):
 1. \<And>a b y cap node. \<lbrakk>cs (a, b) = Some y; m (cte_map (a, b)) = Some (CTE cap node); \<forall>cap node. modify_map m p (cteMDBNode_update (mdbNext_update f)) (cte_map (a, b)) = Some (CTE cap node) \<longrightarrow> revo (a, b) = mdbRevocable node\<rbrakk> \<Longrightarrow> revo (a, b) = mdbRevocable node
 2. revokable_relation revo cs m \<Longrightarrow> revokable_relation revo cs (modify_map m p (cteMDBNode_update (mdbNext_update f))) proof (prove)
goal (1 subgoal):
 1. revokable_relation revo cs m \<Longrightarrow> revokable_relation revo cs (modify_map m p (cteMDBNode_update (mdbNext_update f))) proof (prove)
goal (1 subgoal):
 1. \<And>a b y cap node z. \<lbrakk>\<forall>a b. (\<exists>y. cs (a, b) = Some y) \<longrightarrow> (\<forall>cap node. m (cte_map (a, b)) = Some (CTE cap node) \<longrightarrow> revo (a, b) = mdbRevocable node); p = cte_map (a, b); cs (a, b) = Some y; m (cte_map (a, b)) = Some z; cteMDBNode_update (mdbNext_update f) z = CTE cap node\<rbrakk> \<Longrightarrow> revo (a, b) = mdbRevocable node proof (prove)
goal (1 subgoal):
 1. \<And>a b y cap node z. \<lbrakk>p = cte_map (a, b); cs (a, b) = Some y; m (cte_map (a, b)) = Some z; cteMDBNode_update (mdbNext_update f) z = CTE cap node; \<forall>cap node. m (cte_map (a, b)) = Some (CTE cap node) \<longrightarrow> revo (a, b) = mdbRevocable node\<rbrakk> \<Longrightarrow> revo (a, b) = mdbRevocable node proof (prove)
goal (1 subgoal):
 1. \<And>a b y cap node z x1 x2. \<lbrakk>p = cte_map (a, b); cs (a, b) = Some y; m (cte_map (a, b)) = Some z; cteMDBNode_update (mdbNext_update f) z = CTE cap node; \<forall>cap node. m (cte_map (a, b)) = Some (CTE cap node) \<longrightarrow> revo (a, b) = mdbRevocable node; z = CTE x1 x2\<rbrakk> \<Longrightarrow> revo (a, b) = mdbRevocable node proof (prove)
goal:
No subgoals!