theory CSpace_R

lemma untyped_mdb_prev_update:
  "untyped_mdb' (modify_map m x (cteMDBNode_update (mdbPrev_update f))) = untyped_mdb' m" apply (simp add: untyped_mdb'_def descendants_of_prev_update) apply (rule iffI) apply clarsimp apply (erule_tac x=p in allE) apply (erule_tac x=p' in allE) apply (erule_tac x=c in allE) apply (simp add: modify_map_if split: if_split_asm) apply (erule impE, blast) apply (erule allE, erule impE, blast) apply clarsimp apply clarsimp apply (erule_tac x=p in allE) apply (erule_tac x=p' in allE) apply (erule_tac x=c in allE) apply (simp add: modify_map_if split: if_split_asm) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. untyped_mdb' (modify_map m x (cteMDBNode_update (mdbPrev_update f))) = untyped_mdb' m proof (prove)
goal (1 subgoal):
 1. (\<forall>p p' c. (\<exists>n. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p m)) = (\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p m)) proof (prove)
goal (2 subgoals):
 1. \<forall>p p' c. (\<exists>n. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p m) \<Longrightarrow> \<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p m)
 2. \<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p m) \<Longrightarrow> \<forall>p p' c. (\<exists>n. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p m) proof (prove)
goal (2 subgoals):
 1. \<And>p p' c n c' n'. \<lbrakk>\<forall>p p' c. (\<exists>n. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p m); m p = Some (CTE c n); isUntypedCap c; m p' = Some (CTE c' n'); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}\<rbrakk> \<Longrightarrow> p' \<in> descendants_of' p m
 2. \<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p m) \<Longrightarrow> \<forall>p p' c. (\<exists>n. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p m) proof (prove)
goal (2 subgoals):
 1. \<And>p p' c n c' n'. \<lbrakk>m p = Some (CTE c n); isUntypedCap c; m p' = Some (CTE c' n'); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; \<forall>p' c. (\<exists>n. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p m)\<rbrakk> \<Longrightarrow> p' \<in> descendants_of' p m
 2. \<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p m) \<Longrightarrow> \<forall>p p' c. (\<exists>n. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p m) proof (prove)
goal (2 subgoals):
 1. \<And>p p' c n c' n'. \<lbrakk>m p = Some (CTE c n); isUntypedCap c; m p' = Some (CTE c' n'); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; \<forall>c. (\<exists>n. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p m)\<rbrakk> \<Longrightarrow> p' \<in> descendants_of' p m
 2. \<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p m) \<Longrightarrow> \<forall>p p' c. (\<exists>n. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p m) proof (prove)
goal (2 subgoals):
 1. \<And>p p' c n c' n'. \<lbrakk>m p = Some (CTE c n); isUntypedCap c; m p' = Some (CTE c' n'); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; (\<exists>n. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p m)\<rbrakk> \<Longrightarrow> p' \<in> descendants_of' p m
 2. \<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p m) \<Longrightarrow> \<forall>p p' c. (\<exists>n. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p m) proof (prove)
goal (2 subgoals):
 1. \<And>p p' c n c' n'. \<lbrakk>(\<exists>na. (x = p \<longrightarrow> mdbPrev_update f n = na) \<and> (x = p \<or> na = n)) \<longrightarrow> (\<forall>c'a. (\<exists>n'a. (x = p' \<longrightarrow> c' = c'a \<and> mdbPrev_update f n' = n'a) \<and> (x = p' \<or> c'a = c' \<and> n'a = n')) \<longrightarrow> \<not> isUntypedCap c'a \<longrightarrow> capRange c'a \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p m); m p = Some (CTE c n); isUntypedCap c; m p' = Some (CTE c' n'); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}\<rbrakk> \<Longrightarrow> p' \<in> descendants_of' p m
 2. \<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p m) \<Longrightarrow> \<forall>p p' c. (\<exists>n. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p m) proof (prove)
goal (2 subgoals):
 1. \<And>p p' c n c' n'. \<lbrakk>m p = Some (CTE c n); isUntypedCap c; m p' = Some (CTE c' n'); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; \<forall>c'a. (\<exists>n'a. (x = p' \<longrightarrow> c' = c'a \<and> mdbPrev_update f n' = n'a) \<and> (x = p' \<or> c'a = c' \<and> n'a = n')) \<longrightarrow> \<not> isUntypedCap c'a \<longrightarrow> capRange c'a \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p m\<rbrakk> \<Longrightarrow> p' \<in> descendants_of' p m
 2. \<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p m) \<Longrightarrow> \<forall>p p' c. (\<exists>n. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p m) proof (prove)
goal (2 subgoals):
 1. \<And>p p' c n c' n'. \<lbrakk>m p = Some (CTE c n); isUntypedCap c; m p' = Some (CTE c' n'); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p m\<rbrakk> \<Longrightarrow> p' \<in> descendants_of' p m
 2. \<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p m) \<Longrightarrow> \<forall>p p' c. (\<exists>n. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p m) proof (prove)
goal (1 subgoal):
 1. \<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p m) \<Longrightarrow> \<forall>p p' c. (\<exists>n. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. modify_map m x (cteMDBNode_update (mdbPrev_update f)) p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p m) proof (prove)
goal (1 subgoal):
 1. \<And>p p' c n c' n'. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p m); modify_map m x (cteMDBNode_update (mdbPrev_update f)) p = Some (CTE c n); isUntypedCap c; modify_map m x (cteMDBNode_update (mdbPrev_update f)) p' = Some (CTE c' n'); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}\<rbrakk> \<Longrightarrow> p' \<in> descendants_of' p m proof (prove)
goal (1 subgoal):
 1. \<And>p p' c n c' n'. \<lbrakk>modify_map m x (cteMDBNode_update (mdbPrev_update f)) p = Some (CTE c n); isUntypedCap c; modify_map m x (cteMDBNode_update (mdbPrev_update f)) p' = Some (CTE c' n'); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; \<forall>p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p m)\<rbrakk> \<Longrightarrow> p' \<in> descendants_of' p m proof (prove)
goal (1 subgoal):
 1. \<And>p p' c n c' n'. \<lbrakk>modify_map m x (cteMDBNode_update (mdbPrev_update f)) p = Some (CTE c n); isUntypedCap c; modify_map m x (cteMDBNode_update (mdbPrev_update f)) p' = Some (CTE c' n'); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; \<forall>c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p m)\<rbrakk> \<Longrightarrow> p' \<in> descendants_of' p m proof (prove)
goal (1 subgoal):
 1. \<And>p p' c n c' n'. \<lbrakk>modify_map m x (cteMDBNode_update (mdbPrev_update f)) p = Some (CTE c n); isUntypedCap c; modify_map m x (cteMDBNode_update (mdbPrev_update f)) p' = Some (CTE c' n'); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p m)\<rbrakk> \<Longrightarrow> p' \<in> descendants_of' p m proof (prove)
goal (1 subgoal):
 1. \<And>p p' c n c' n'. \<lbrakk>\<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; \<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p' \<in> descendants_of' p m; p' \<noteq> p; m p = Some (CTE c n); isUntypedCap c; x = p'; \<exists>node. m p' = Some (CTE c' node) \<and> mdbPrev_update f node = n'\<rbrakk> \<Longrightarrow> p' \<in> descendants_of' p m proof (prove)
goal:
No subgoals!