theory CSpace1_R

lemma same_master_descendants:
  assumes slot: "m slot = Some cte"
  assumes master: "capMasterCap (cteCap cte) = capMasterCap cap'"
  assumes c': "\<not>isReplyCap cap'" "\<not>isEndpointCap cap'" "\<not>isNotificationCap cap'"
  defines "m' \<equiv> m(slot \<mapsto> cteCap_update (\<lambda>_. cap') cte)"
  shows "descendants_of' p m' = descendants_of' p m" proof (rule set_eqI, simp add: descendants_of'_def) obtain cap n where cte: "cte = CTE cap n" by (cases cte) then interpret masterCap cap cap' using master by (simp add: masterCap_def) from c' have c: "\<not>isReplyCap cap"
          "\<not>isEndpointCap cap"
          "\<not>isNotificationCap cap" by auto note parent [simp] = isMDBParentOf [OF c] { fix a b from slot have "m' \<turnstile> a \<leadsto> b = m \<turnstile> a \<leadsto> b" by (simp add: m'_def mdb_next_unfold) } note this [simp] { fix a b from slot cte have "m' \<turnstile> a parentOf b = m \<turnstile> a parentOf b" by (simp add: m'_def parentOf_def) } note this [simp] fix x { assume "m \<turnstile> p \<rightarrow> x" hence "m' \<turnstile> p \<rightarrow> x" proof induct case (direct_parent c') thus ?case by (auto intro: subtree.direct_parent) next case trans_parent thus ?case by (auto elim: subtree.trans_parent) qed } moreover { assume "m' \<turnstile> p \<rightarrow> x" hence "m \<turnstile> p \<rightarrow> x" proof induct case (direct_parent c') thus ?case by (auto intro: subtree.direct_parent) next case trans_parent thus ?case by (auto elim: subtree.trans_parent) qed } ultimately show "m' \<turnstile> p \<rightarrow> x = m \<turnstile> p \<rightarrow> x" by blast qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. descendants_of' p m' = descendants_of' p m proof (state)
goal (1 subgoal):
 1. \<And>x. m' \<turnstile> p \<rightarrow> x = m \<turnstile> p \<rightarrow> x proof (prove)
goal (1 subgoal):
 1. (\<And>cap n. cte = CTE cap n \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (state)
this:
cte = CTE cap n

goal (1 subgoal):
 1. \<And>x. m' \<turnstile> p \<rightarrow> x = m \<turnstile> p \<rightarrow> x proof (chain)
picking this:
cte = CTE cap n proof (prove)
using this:
cte = CTE cap n

goal (1 subgoal):
 1. masterCap cap cap' proof (prove)
using this:
cte = CTE cap n
capMasterCap (cteCap cte) = capMasterCap cap'

goal (1 subgoal):
 1. masterCap cap cap' proof (state)
goal (1 subgoal):
 1. \<And>x. m' \<turnstile> p \<rightarrow> x = m \<turnstile> p \<rightarrow> x proof (chain)
picking this:
\<not> isReplyCap cap'
\<not> isEndpointCap cap'
\<not> isNotificationCap cap' proof (prove)
using this:
\<not> isReplyCap cap'
\<not> isEndpointCap cap'
\<not> isNotificationCap cap'

goal (1 subgoal):
 1. \<not> isReplyCap cap &&& \<not> isEndpointCap cap &&& \<not> isNotificationCap cap proof (state)
this:
\<not> isReplyCap cap
\<not> isEndpointCap cap
\<not> isNotificationCap cap

goal (1 subgoal):
 1. \<And>x. m' \<turnstile> p \<rightarrow> x = m \<turnstile> p \<rightarrow> x proof (state)
this:
isMDBParentOf ?c (CTE cap' ?m) = isMDBParentOf ?c (CTE cap ?m)
isMDBParentOf (CTE cap' ?m) ?c = isMDBParentOf (CTE cap ?m) ?c

goal (1 subgoal):
 1. \<And>x. m' \<turnstile> p \<rightarrow> x = m \<turnstile> p \<rightarrow> x proof (state)
this:
isMDBParentOf ?c (CTE cap' ?m) = isMDBParentOf ?c (CTE cap ?m)
isMDBParentOf (CTE cap' ?m) ?c = isMDBParentOf (CTE cap ?m) ?c

goal (1 subgoal):
 1. \<And>x. m' \<turnstile> p \<rightarrow> x = m \<turnstile> p \<rightarrow> x proof (state)
goal (1 subgoal):
 1. \<And>x. m' \<turnstile> p \<rightarrow> x = m \<turnstile> p \<rightarrow> x proof (chain)
picking this:
m slot = Some cte proof (prove)
using this:
m slot = Some cte

goal (1 subgoal):
 1. m' \<turnstile> a \<leadsto> b = m \<turnstile> a \<leadsto> b proof (state)
this:
m' \<turnstile> a \<leadsto> b = m \<turnstile> a \<leadsto> b

goal (1 subgoal):
 1. \<And>x. m' \<turnstile> p \<rightarrow> x = m \<turnstile> p \<rightarrow> x proof (state)
this:
m' \<turnstile> ?a2 \<leadsto> ?b2 = m \<turnstile> ?a2 \<leadsto> ?b2

goal (1 subgoal):
 1. \<And>x. m' \<turnstile> p \<rightarrow> x = m \<turnstile> p \<rightarrow> x proof (state)
this:
m' \<turnstile> ?a2 \<leadsto> ?b2 = m \<turnstile> ?a2 \<leadsto> ?b2

goal (1 subgoal):
 1. \<And>x. m' \<turnstile> p \<rightarrow> x = m \<turnstile> p \<rightarrow> x proof (state)
this:
m' \<turnstile> ?a2 \<leadsto> ?b2 = m \<turnstile> ?a2 \<leadsto> ?b2

goal (1 subgoal):
 1. \<And>x. m' \<turnstile> p \<rightarrow> x = m \<turnstile> p \<rightarrow> x proof (state)
goal (1 subgoal):
 1. \<And>x. m' \<turnstile> p \<rightarrow> x = m \<turnstile> p \<rightarrow> x proof (chain)
picking this:
m slot = Some cte
cte = CTE cap n proof (prove)
using this:
m slot = Some cte
cte = CTE cap n

goal (1 subgoal):
 1. m' \<turnstile> a parentOf b = m \<turnstile> a parentOf b proof (state)
this:
m' \<turnstile> a parentOf b = m \<turnstile> a parentOf b

goal (1 subgoal):
 1. \<And>x. m' \<turnstile> p \<rightarrow> x = m \<turnstile> p \<rightarrow> x proof (state)
this:
m' \<turnstile> ?a2 parentOf ?b2 = m \<turnstile> ?a2 parentOf ?b2

goal (1 subgoal):
 1. \<And>x. m' \<turnstile> p \<rightarrow> x = m \<turnstile> p \<rightarrow> x proof (state)
this:
m' \<turnstile> ?a2 parentOf ?b2 = m \<turnstile> ?a2 parentOf ?b2

goal (1 subgoal):
 1. \<And>x. m' \<turnstile> p \<rightarrow> x = m \<turnstile> p \<rightarrow> x proof (state)
goal (1 subgoal):
 1. \<And>x. m' \<turnstile> p \<rightarrow> x = m \<turnstile> p \<rightarrow> x proof (state)
goal (1 subgoal):
 1. \<And>x. m' \<turnstile> p \<rightarrow> x = m \<turnstile> p \<rightarrow> x proof (state)
this:
m \<turnstile> p \<rightarrow> x

goal (1 subgoal):
 1. \<And>x. m' \<turnstile> p \<rightarrow> x = m \<turnstile> p \<rightarrow> x proof (prove)
using this:
m \<turnstile> p \<rightarrow> x

goal (1 subgoal):
 1. m' \<turnstile> p \<rightarrow> x proof (state)
goal (2 subgoals):
 1. \<And>c'. \<lbrakk>m \<turnstile> p \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'\<rbrakk> \<Longrightarrow> m' \<turnstile> p \<rightarrow> c'
 2. \<And>c' c''. \<lbrakk>m \<turnstile> p \<rightarrow> c'; m' \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> m' \<turnstile> p \<rightarrow> c'' proof (state)
this:
m \<turnstile> p \<leadsto> c'
c' \<noteq> 0
m \<turnstile> p parentOf c'

goal (2 subgoals):
 1. \<And>c'. \<lbrakk>m \<turnstile> p \<leadsto> c'; c' \<noteq> 0; m \<turnstile> p parentOf c'\<rbrakk> \<Longrightarrow> m' \<turnstile> p \<rightarrow> c'
 2. \<And>c' c''. \<lbrakk>m \<turnstile> p \<rightarrow> c'; m' \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> m' \<turnstile> p \<rightarrow> c'' proof (prove)
using this:
m \<turnstile> p \<leadsto> c'
c' \<noteq> 0
m \<turnstile> p parentOf c'

goal (1 subgoal):
 1. m' \<turnstile> p \<rightarrow> c' proof (state)
this:
m' \<turnstile> p \<rightarrow> c'

goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>m \<turnstile> p \<rightarrow> c'; m' \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> m' \<turnstile> p \<rightarrow> c'' proof (state)
goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>m \<turnstile> p \<rightarrow> c'; m' \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> m' \<turnstile> p \<rightarrow> c'' proof (state)
this:
m \<turnstile> p \<rightarrow> c'_
m' \<turnstile> p \<rightarrow> c'_
m \<turnstile> c'_ \<leadsto> c''_
c''_ \<noteq> 0
m \<turnstile> p parentOf c''_

goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>m \<turnstile> p \<rightarrow> c'; m' \<turnstile> p \<rightarrow> c'; m \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> m' \<turnstile> p \<rightarrow> c'' proof (prove)
using this:
m \<turnstile> p \<rightarrow> c'_
m' \<turnstile> p \<rightarrow> c'_
m \<turnstile> c'_ \<leadsto> c''_
c''_ \<noteq> 0
m \<turnstile> p parentOf c''_

goal (1 subgoal):
 1. m' \<turnstile> p \<rightarrow> c''_ proof (state)
this:
m' \<turnstile> p \<rightarrow> c''_

goal:
No subgoals! proof (state)
this:
m' \<turnstile> p \<rightarrow> x

goal (1 subgoal):
 1. \<And>x. m' \<turnstile> p \<rightarrow> x = m \<turnstile> p \<rightarrow> x proof (state)
this:
m \<turnstile> p \<rightarrow> x \<Longrightarrow> m' \<turnstile> p \<rightarrow> x

goal (1 subgoal):
 1. \<And>x. m' \<turnstile> p \<rightarrow> x = m \<turnstile> p \<rightarrow> x proof (state)
this:
m \<turnstile> p \<rightarrow> x \<Longrightarrow> m' \<turnstile> p \<rightarrow> x

goal (1 subgoal):
 1. \<And>x. m' \<turnstile> p \<rightarrow> x = m \<turnstile> p \<rightarrow> x proof (state)
this:
m \<turnstile> p \<rightarrow> x \<Longrightarrow> m' \<turnstile> p \<rightarrow> x

goal (1 subgoal):
 1. \<And>x. m' \<turnstile> p \<rightarrow> x = m \<turnstile> p \<rightarrow> x proof (state)
this:
m' \<turnstile> p \<rightarrow> x

goal (1 subgoal):
 1. \<And>x. m' \<turnstile> p \<rightarrow> x = m \<turnstile> p \<rightarrow> x proof (prove)
using this:
m' \<turnstile> p \<rightarrow> x

goal (1 subgoal):
 1. m \<turnstile> p \<rightarrow> x proof (state)
goal (2 subgoals):
 1. \<And>c'. \<lbrakk>m' \<turnstile> p \<leadsto> c'; c' \<noteq> 0; m' \<turnstile> p parentOf c'\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> c'
 2. \<And>c' c''. \<lbrakk>m' \<turnstile> p \<rightarrow> c'; m \<turnstile> p \<rightarrow> c'; m' \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m' \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> c'' proof (state)
this:
m' \<turnstile> p \<leadsto> c'
c' \<noteq> 0
m' \<turnstile> p parentOf c'

goal (2 subgoals):
 1. \<And>c'. \<lbrakk>m' \<turnstile> p \<leadsto> c'; c' \<noteq> 0; m' \<turnstile> p parentOf c'\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> c'
 2. \<And>c' c''. \<lbrakk>m' \<turnstile> p \<rightarrow> c'; m \<turnstile> p \<rightarrow> c'; m' \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m' \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> c'' proof (prove)
using this:
m' \<turnstile> p \<leadsto> c'
c' \<noteq> 0
m' \<turnstile> p parentOf c'

goal (1 subgoal):
 1. m \<turnstile> p \<rightarrow> c' proof (state)
this:
m \<turnstile> p \<rightarrow> c'

goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>m' \<turnstile> p \<rightarrow> c'; m \<turnstile> p \<rightarrow> c'; m' \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m' \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> c'' proof (state)
goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>m' \<turnstile> p \<rightarrow> c'; m \<turnstile> p \<rightarrow> c'; m' \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m' \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> c'' proof (state)
this:
m' \<turnstile> p \<rightarrow> c'_
m \<turnstile> p \<rightarrow> c'_
m' \<turnstile> c'_ \<leadsto> c''_
c''_ \<noteq> 0
m' \<turnstile> p parentOf c''_

goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>m' \<turnstile> p \<rightarrow> c'; m \<turnstile> p \<rightarrow> c'; m' \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; m' \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> c'' proof (prove)
using this:
m' \<turnstile> p \<rightarrow> c'_
m \<turnstile> p \<rightarrow> c'_
m' \<turnstile> c'_ \<leadsto> c''_
c''_ \<noteq> 0
m' \<turnstile> p parentOf c''_

goal (1 subgoal):
 1. m \<turnstile> p \<rightarrow> c''_ proof (state)
this:
m \<turnstile> p \<rightarrow> c''_

goal:
No subgoals! proof (state)
this:
m \<turnstile> p \<rightarrow> x

goal (1 subgoal):
 1. \<And>x. m' \<turnstile> p \<rightarrow> x = m \<turnstile> p \<rightarrow> x proof (state)
this:
m' \<turnstile> p \<rightarrow> x \<Longrightarrow> m \<turnstile> p \<rightarrow> x

goal (1 subgoal):
 1. \<And>x. m' \<turnstile> p \<rightarrow> x = m \<turnstile> p \<rightarrow> x proof (chain)
picking this:
m \<turnstile> p \<rightarrow> x \<Longrightarrow> m' \<turnstile> p \<rightarrow> x
m' \<turnstile> p \<rightarrow> x \<Longrightarrow> m \<turnstile> p \<rightarrow> x proof (prove)
using this:
m \<turnstile> p \<rightarrow> x \<Longrightarrow> m' \<turnstile> p \<rightarrow> x
m' \<turnstile> p \<rightarrow> x \<Longrightarrow> m \<turnstile> p \<rightarrow> x

goal (1 subgoal):
 1. m' \<turnstile> p \<rightarrow> x = m \<turnstile> p \<rightarrow> x proof (state)
this:
m' \<turnstile> p \<rightarrow> x = m \<turnstile> p \<rightarrow> x

goal:
No subgoals!