theory IpcCancel_R

lemma reply_mdbNext_is_descendantD:
  assumes sr: "(s, s') \<in> state_relation"
  and   invs: "invs' s'"
  and    tcb: "tcb_at t s"
  and    cte: "ctes_of s' (t + 0x20) = Some cte"
  and   desc: "descendants_of (t, tcb_cnode_index 2) (cdt s) = {sl}"
  shows       "mdbNext (cteMDBNode cte) = cte_map sl" proof - from tcb have "cte_at (t, tcb_cnode_index 2) s" by (simp add: tcb_at_cte_at dom_tcb_cap_cases) hence "descendants_of' (t + 2*2^cte_level_bits) (ctes_of s') = {cte_map sl}" using sr desc by (fastforce simp: state_relation_def cdt_relation_def cte_map_def tcb_cnode_index_def) thus ?thesis using cte invs apply (clarsimp simp: descendants_of'_def) apply (frule singleton_eqD, drule CollectD) apply (erule subtree.cases) apply (clarsimp simp: mdb_next_rel_def mdb_next_def cte_level_bits_def) apply (subgoal_tac "c' = cte_map sl") apply (fastforce dest: invs_no_loops no_loops_direct_simp) apply fastforce done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mdbNext (cteMDBNode cte) = cte_map sl proof (state)
goal (1 subgoal):
 1. mdbNext (cteMDBNode cte) = cte_map sl proof (chain)
picking this:
tcb_at t s proof (prove)
using this:
tcb_at t s

goal (1 subgoal):
 1. cte_wp_at (\<lambda>_. True) (t, tcb_cnode_index 2) s proof (state)
this:
cte_wp_at (\<lambda>_. True) (t, tcb_cnode_index 2) s

goal (1 subgoal):
 1. mdbNext (cteMDBNode cte) = cte_map sl proof (prove)
using this:
cte_wp_at (\<lambda>_. True) (t, tcb_cnode_index 2) s

goal (1 subgoal):
 1. descendants_of' (t + 2 * 2 ^ cte_level_bits) (ctes_of s') = {cte_map sl} proof (prove)
using this:
cte_wp_at (\<lambda>_. True) (t, tcb_cnode_index 2) s
(s, s') \<in> state_relation
descendants_of (t, tcb_cnode_index 2) (cdt s) = {sl}

goal (1 subgoal):
 1. descendants_of' (t + 2 * 2 ^ cte_level_bits) (ctes_of s') = {cte_map sl} proof (state)
this:
descendants_of' (t + 2 * 2 ^ cte_level_bits) (ctes_of s') = {cte_map sl}

goal (1 subgoal):
 1. mdbNext (cteMDBNode cte) = cte_map sl proof (prove)
using this:
descendants_of' (t + 2 * 2 ^ cte_level_bits) (ctes_of s') = {cte_map sl}

goal (1 subgoal):
 1. mdbNext (cteMDBNode cte) = cte_map sl proof (prove)
using this:
descendants_of' (t + 2 * 2 ^ cte_level_bits) (ctes_of s') = {cte_map sl}
ctes_of s' (t + 0x20) = Some cte
invs' s'

goal (1 subgoal):
 1. mdbNext (cteMDBNode cte) = cte_map sl proof (prove)
goal (1 subgoal):
 1. \<lbrakk>{c'. ctes_of s' \<turnstile> t + 2 * 2 ^ cte_level_bits \<rightarrow> c'} = {cte_map sl}; ctes_of s' (t + 0x20) = Some cte; invs' s'\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode cte) = cte_map sl proof (prove)
goal (1 subgoal):
 1. \<lbrakk>{c'. ctes_of s' \<turnstile> t + 2 * 2 ^ cte_level_bits \<rightarrow> c'} = {cte_map sl}; ctes_of s' (t + 0x20) = Some cte; invs' s'; ctes_of s' \<turnstile> t + 2 * 2 ^ cte_level_bits \<rightarrow> cte_map sl\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode cte) = cte_map sl proof (prove)
goal (2 subgoals):
 1. \<And>c'. \<lbrakk>{c'. ctes_of s' \<turnstile> t + 2 * 2 ^ cte_level_bits \<rightarrow> c'} = {cte_map sl}; ctes_of s' (t + 0x20) = Some cte; invs' s'; cte_map sl = c'; ctes_of s' \<turnstile> t + 2 * 2 ^ cte_level_bits \<leadsto> c'; c' \<noteq> 0; ctes_of s' \<turnstile> t + 2 * 2 ^ cte_level_bits parentOf c'\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode cte) = cte_map sl
 2. \<And>c' c''. \<lbrakk>{c'. ctes_of s' \<turnstile> t + 2 * 2 ^ cte_level_bits \<rightarrow> c'} = {cte_map sl}; ctes_of s' (t + 0x20) = Some cte; invs' s'; cte_map sl = c''; ctes_of s' \<turnstile> t + 2 * 2 ^ cte_level_bits \<rightarrow> c'; ctes_of s' \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; ctes_of s' \<turnstile> t + 2 * 2 ^ cte_level_bits parentOf c''\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode cte) = cte_map sl proof (prove)
goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>{c'. ctes_of s' \<turnstile> t + 2 * 2 ^ cte_level_bits \<rightarrow> c'} = {cte_map sl}; ctes_of s' (t + 0x20) = Some cte; invs' s'; cte_map sl = c''; ctes_of s' \<turnstile> t + 2 * 2 ^ cte_level_bits \<rightarrow> c'; ctes_of s' \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; ctes_of s' \<turnstile> t + 2 * 2 ^ cte_level_bits parentOf c''\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode cte) = cte_map sl proof (prove)
goal (2 subgoals):
 1. \<And>c' c''. \<lbrakk>{c'. ctes_of s' \<turnstile> t + 2 * 2 ^ cte_level_bits \<rightarrow> c'} = {cte_map sl}; ctes_of s' (t + 0x20) = Some cte; invs' s'; cte_map sl = c''; ctes_of s' \<turnstile> t + 2 * 2 ^ cte_level_bits \<rightarrow> c'; ctes_of s' \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; ctes_of s' \<turnstile> t + 2 * 2 ^ cte_level_bits parentOf c''; c' = cte_map sl\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode cte) = cte_map sl
 2. \<And>c' c''. \<lbrakk>{c'. ctes_of s' \<turnstile> t + 2 * 2 ^ cte_level_bits \<rightarrow> c'} = {cte_map sl}; ctes_of s' (t + 0x20) = Some cte; invs' s'; cte_map sl = c''; ctes_of s' \<turnstile> t + 2 * 2 ^ cte_level_bits \<rightarrow> c'; ctes_of s' \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; ctes_of s' \<turnstile> t + 2 * 2 ^ cte_level_bits parentOf c''\<rbrakk> \<Longrightarrow> c' = cte_map sl proof (prove)
goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>{c'. ctes_of s' \<turnstile> t + 2 * 2 ^ cte_level_bits \<rightarrow> c'} = {cte_map sl}; ctes_of s' (t + 0x20) = Some cte; invs' s'; cte_map sl = c''; ctes_of s' \<turnstile> t + 2 * 2 ^ cte_level_bits \<rightarrow> c'; ctes_of s' \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; ctes_of s' \<turnstile> t + 2 * 2 ^ cte_level_bits parentOf c''\<rbrakk> \<Longrightarrow> c' = cte_map sl proof (prove)
goal:
No subgoals! proof (state)
this:
mdbNext (cteMDBNode cte) = cte_map sl

goal:
No subgoals!