theory CSpace1_R

lemma descendants_of:
  "descendants_of' p m = descendants_of' p m'" apply (rule set_eqI) apply (clarsimp simp:descendants_of'_def Invariants_H.subtree_def) apply (rule_tac f = "\<lambda>x. lfp x c" for c in arg_cong) apply (rule ext)+ apply (subgoal_tac "\<And>p p'. (m \<turnstile> p \<leadsto> p') = (m' \<turnstile> p \<leadsto> p')") apply clarsimp apply (subgoal_tac "(m \<turnstile> p parentOf xa) = (m' \<turnstile> p parentOf xa)") apply fastforce apply (rule parentOf_preserve[OF dom]) apply (simp add:misc sameRegion mdb_next mdb_next_rel_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. descendants_of' p m = descendants_of' p m' proof (prove)
goal (1 subgoal):
 1. \<And>x. (x \<in> descendants_of' p m) = (x \<in> descendants_of' p m') proof (prove)
goal (1 subgoal):
 1. \<And>x. lfp (\<lambda>pa x. m \<turnstile> p \<leadsto> x \<and> x \<noteq> 0 \<and> m \<turnstile> p parentOf x \<or> (\<exists>c'. pa c' \<and> m \<turnstile> c' \<leadsto> x \<and> x \<noteq> 0 \<and> m \<turnstile> p parentOf x)) x = lfp (\<lambda>pa x. m' \<turnstile> p \<leadsto> x \<and> x \<noteq> 0 \<and> m' \<turnstile> p parentOf x \<or> (\<exists>c'. pa c' \<and> m' \<turnstile> c' \<leadsto> x \<and> x \<noteq> 0 \<and> m' \<turnstile> p parentOf x)) x proof (prove)
goal (1 subgoal):
 1. \<And>x. (\<lambda>pa x. m \<turnstile> p \<leadsto> x \<and> x \<noteq> 0 \<and> m \<turnstile> p parentOf x \<or> (\<exists>c'. pa c' \<and> m \<turnstile> c' \<leadsto> x \<and> x \<noteq> 0 \<and> m \<turnstile> p parentOf x)) = (\<lambda>pa x. m' \<turnstile> p \<leadsto> x \<and> x \<noteq> 0 \<and> m' \<turnstile> p parentOf x \<or> (\<exists>c'. pa c' \<and> m' \<turnstile> c' \<leadsto> x \<and> x \<noteq> 0 \<and> m' \<turnstile> p parentOf x)) proof (prove)
goal (1 subgoal):
 1. \<And>x pa xa. (m \<turnstile> p \<leadsto> xa \<and> xa \<noteq> 0 \<and> m \<turnstile> p parentOf xa \<or> (\<exists>c'. pa c' \<and> m \<turnstile> c' \<leadsto> xa \<and> xa \<noteq> 0 \<and> m \<turnstile> p parentOf xa)) = (m' \<turnstile> p \<leadsto> xa \<and> xa \<noteq> 0 \<and> m' \<turnstile> p parentOf xa \<or> (\<exists>c'. pa c' \<and> m' \<turnstile> c' \<leadsto> xa \<and> xa \<noteq> 0 \<and> m' \<turnstile> p parentOf xa)) proof (prove)
goal (2 subgoals):
 1. \<And>x pa xa. (\<And>p p'. m \<turnstile> p \<leadsto> p' = m' \<turnstile> p \<leadsto> p') \<Longrightarrow> (m \<turnstile> p \<leadsto> xa \<and> xa \<noteq> 0 \<and> m \<turnstile> p parentOf xa \<or> (\<exists>c'. pa c' \<and> m \<turnstile> c' \<leadsto> xa \<and> xa \<noteq> 0 \<and> m \<turnstile> p parentOf xa)) = (m' \<turnstile> p \<leadsto> xa \<and> xa \<noteq> 0 \<and> m' \<turnstile> p parentOf xa \<or> (\<exists>c'. pa c' \<and> m' \<turnstile> c' \<leadsto> xa \<and> xa \<noteq> 0 \<and> m' \<turnstile> p parentOf xa))
 2. \<And>x p xa pa p'. m \<turnstile> pa \<leadsto> p' = m' \<turnstile> pa \<leadsto> p' proof (prove)
goal (2 subgoals):
 1. \<And>pa xa. (\<And>p p'. m \<turnstile> p \<leadsto> p' = m' \<turnstile> p \<leadsto> p') \<Longrightarrow> (m' \<turnstile> p \<leadsto> xa \<and> xa \<noteq> 0 \<and> m \<turnstile> p parentOf xa \<or> (\<exists>c'. pa c' \<and> m' \<turnstile> c' \<leadsto> xa \<and> xa \<noteq> 0 \<and> m \<turnstile> p parentOf xa)) = (m' \<turnstile> p \<leadsto> xa \<and> xa \<noteq> 0 \<and> m' \<turnstile> p parentOf xa \<or> (\<exists>c'. pa c' \<and> m' \<turnstile> c' \<leadsto> xa \<and> xa \<noteq> 0 \<and> m' \<turnstile> p parentOf xa))
 2. \<And>x p xa pa p'. m \<turnstile> pa \<leadsto> p' = m' \<turnstile> pa \<leadsto> p' proof (prove)
goal (3 subgoals):
 1. \<And>pa xa. \<lbrakk>\<And>p p'. m \<turnstile> p \<leadsto> p' = m' \<turnstile> p \<leadsto> p'; m \<turnstile> p parentOf xa = m' \<turnstile> p parentOf xa\<rbrakk> \<Longrightarrow> (m' \<turnstile> p \<leadsto> xa \<and> xa \<noteq> 0 \<and> m \<turnstile> p parentOf xa \<or> (\<exists>c'. pa c' \<and> m' \<turnstile> c' \<leadsto> xa \<and> xa \<noteq> 0 \<and> m \<turnstile> p parentOf xa)) = (m' \<turnstile> p \<leadsto> xa \<and> xa \<noteq> 0 \<and> m' \<turnstile> p parentOf xa \<or> (\<exists>c'. pa c' \<and> m' \<turnstile> c' \<leadsto> xa \<and> xa \<noteq> 0 \<and> m' \<turnstile> p parentOf xa))
 2. \<And>pa xa. (\<And>p p'. m \<turnstile> p \<leadsto> p' = m' \<turnstile> p \<leadsto> p') \<Longrightarrow> m \<turnstile> p parentOf xa = m' \<turnstile> p parentOf xa
 3. \<And>x p xa pa p'. m \<turnstile> pa \<leadsto> p' = m' \<turnstile> pa \<leadsto> p' proof (prove)
goal (2 subgoals):
 1. \<And>pa xa. (\<And>p p'. m \<turnstile> p \<leadsto> p' = m' \<turnstile> p \<leadsto> p') \<Longrightarrow> m \<turnstile> p parentOf xa = m' \<turnstile> p parentOf xa
 2. \<And>x p xa pa p'. m \<turnstile> pa \<leadsto> p' = m' \<turnstile> pa \<leadsto> p' proof (prove)
goal (4 subgoals):
 1. \<And>p xa x cte cte'. \<lbrakk>\<And>p p'. m \<turnstile> p \<leadsto> p' = m' \<turnstile> p \<leadsto> p'; m x = Some cte; m' x = Some cte'\<rbrakk> \<Longrightarrow> global.sameRegionAs (cteCap cte) = global.sameRegionAs (cteCap cte') \<and> (\<lambda>x. global.sameRegionAs x (cteCap cte)) = (\<lambda>x. global.sameRegionAs x (cteCap cte'))
 2. \<And>p xa x cte cte'. \<lbrakk>\<And>p p'. m \<turnstile> p \<leadsto> p' = m' \<turnstile> p \<leadsto> p'; m x = Some cte; m' x = Some cte'\<rbrakk> \<Longrightarrow> isUntypedCap (cteCap cte) = isUntypedCap (cteCap cte') \<and> isNotificationCap (cteCap cte) = isNotificationCap (cteCap cte') \<and> (isNotificationCap (cteCap cte) \<longrightarrow> capNtfnBadge (cteCap cte) = capNtfnBadge (cteCap cte')) \<and> isEndpointCap (cteCap cte) = isEndpointCap (cteCap cte') \<and> (isEndpointCap (cteCap cte) \<longrightarrow> capEPBadge (cteCap cte) = capEPBadge (cteCap cte')) \<and> cteMDBNode cte = cteMDBNode cte'
 3. \<And>p xa pa. (\<And>p p'. m \<turnstile> p \<leadsto> p' = m' \<turnstile> p \<leadsto> p') \<Longrightarrow> mdb_next m pa = mdb_next m' pa
 4. \<And>x p xa pa p'. m \<turnstile> pa \<leadsto> p' = m' \<turnstile> pa \<leadsto> p' proof (prove)
goal:
No subgoals!