theory CSpace_I

lemma class_links_init:
  "\<lbrakk> class_links m; no_0 m; m p = Some cte;
     no_mdb cte; valid_dlist m \<rbrakk>
   \<Longrightarrow> class_links (m(p \<mapsto> CTE cap initMDBNode))" apply (simp add: class_links_def split del: if_split) apply (erule allEI, erule allEI) apply simp apply (intro conjI impI) apply clarsimp apply (drule no_mdb_not_target[where p=p], simp) apply (simp add: no_mdb_def) apply (erule(2) valid_dlist_init) apply (clarsimp simp add: no_0_def) apply simp apply (clarsimp simp: mdb_next_unfold) apply (clarsimp simp: mdb_next_unfold) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>class_links m; no_0 m; m p = Some cte; no_mdb cte; valid_dlist m\<rbrakk> \<Longrightarrow> class_links (m(p \<mapsto> CTE cap initMDBNode)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>p p' cte. m p = Some cte \<longrightarrow> (\<forall>cte'. m p' = Some cte' \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capClass (cteCap cte) = capClass (cteCap cte')); no_0 m; m p = Some cte; no_mdb cte; valid_dlist m\<rbrakk> \<Longrightarrow> \<forall>pa p' cte. (if pa = p then Some (CTE cap initMDBNode) else m pa) = Some cte \<longrightarrow> (\<forall>cte'. (if p' = p then Some (CTE cap initMDBNode) else m p') = Some cte' \<longrightarrow> m(p \<mapsto> CTE cap initMDBNode) \<turnstile> pa \<leadsto> p' \<longrightarrow> capClass (cteCap cte) = capClass (cteCap cte')) proof (prove)
goal (1 subgoal):
 1. \<And>pa p'. \<lbrakk>no_0 m; m p = Some cte; no_mdb cte; valid_dlist m; \<forall>cte. m pa = Some cte \<longrightarrow> (\<forall>cte'. m p' = Some cte' \<longrightarrow> m \<turnstile> pa \<leadsto> p' \<longrightarrow> capClass (cteCap cte) = capClass (cteCap cte'))\<rbrakk> \<Longrightarrow> \<forall>cte. (if pa = p then Some (CTE cap initMDBNode) else m pa) = Some cte \<longrightarrow> (\<forall>cte'. (if p' = p then Some (CTE cap initMDBNode) else m p') = Some cte' \<longrightarrow> m(p \<mapsto> CTE cap initMDBNode) \<turnstile> pa \<leadsto> p' \<longrightarrow> capClass (cteCap cte) = capClass (cteCap cte')) proof (prove)
goal (1 subgoal):
 1. \<And>pa p'. \<lbrakk>no_0 m; m p = Some cte; no_mdb cte; valid_dlist m; \<forall>cte. m pa = Some cte \<longrightarrow> (\<forall>cte'. m p' = Some cte' \<longrightarrow> m \<turnstile> pa \<leadsto> p' \<longrightarrow> capClass (cteCap cte) = capClass (cteCap cte'))\<rbrakk> \<Longrightarrow> (p' = p \<longrightarrow> pa \<noteq> p \<longrightarrow> (\<forall>cte. m pa = Some cte \<longrightarrow> m(p \<mapsto> CTE cap initMDBNode) \<turnstile> pa \<leadsto> p \<longrightarrow> capClass (cteCap cte) = capClass cap)) \<and> (p' \<noteq> p \<longrightarrow> (pa = p \<longrightarrow> (\<forall>cte'. m p' = Some cte' \<longrightarrow> m(p \<mapsto> CTE cap initMDBNode) \<turnstile> p \<leadsto> p' \<longrightarrow> capClass cap = capClass (cteCap cte'))) \<and> (pa \<noteq> p \<longrightarrow> (\<forall>cte. m pa = Some cte \<longrightarrow> (\<forall>cte'. m p' = Some cte' \<longrightarrow> m(p \<mapsto> CTE cap initMDBNode) \<turnstile> pa \<leadsto> p' \<longrightarrow> capClass (cteCap cte) = capClass (cteCap cte'))))) proof (prove)
goal (3 subgoals):
 1. \<And>pa p'. \<lbrakk>no_0 m; m p = Some cte; no_mdb cte; valid_dlist m; \<forall>cte. m pa = Some cte \<longrightarrow> (\<forall>cte'. m p' = Some cte' \<longrightarrow> m \<turnstile> pa \<leadsto> p' \<longrightarrow> capClass (cteCap cte) = capClass (cteCap cte')); p' = p; pa \<noteq> p\<rbrakk> \<Longrightarrow> \<forall>cte. m pa = Some cte \<longrightarrow> m(p \<mapsto> CTE cap initMDBNode) \<turnstile> pa \<leadsto> p \<longrightarrow> capClass (cteCap cte) = capClass cap
 2. \<And>pa p'. \<lbrakk>no_0 m; m p = Some cte; no_mdb cte; valid_dlist m; \<forall>cte. m pa = Some cte \<longrightarrow> (\<forall>cte'. m p' = Some cte' \<longrightarrow> m \<turnstile> pa \<leadsto> p' \<longrightarrow> capClass (cteCap cte) = capClass (cteCap cte')); p' \<noteq> p; pa = p\<rbrakk> \<Longrightarrow> \<forall>cte'. m p' = Some cte' \<longrightarrow> m(p \<mapsto> CTE cap initMDBNode) \<turnstile> p \<leadsto> p' \<longrightarrow> capClass cap = capClass (cteCap cte')
 3. \<And>pa p'. \<lbrakk>no_0 m; m p = Some cte; no_mdb cte; valid_dlist m; \<forall>cte. m pa = Some cte \<longrightarrow> (\<forall>cte'. m p' = Some cte' \<longrightarrow> m \<turnstile> pa \<leadsto> p' \<longrightarrow> capClass (cteCap cte) = capClass (cteCap cte')); p' \<noteq> p; pa \<noteq> p\<rbrakk> \<Longrightarrow> \<forall>cte. m pa = Some cte \<longrightarrow> (\<forall>cte'. m p' = Some cte' \<longrightarrow> m(p \<mapsto> CTE cap initMDBNode) \<turnstile> pa \<leadsto> p' \<longrightarrow> capClass (cteCap cte) = capClass (cteCap cte')) proof (prove)
goal (3 subgoals):
 1. \<And>pa ctea. \<lbrakk>no_0 m; m p = Some cte; no_mdb cte; valid_dlist m; m \<turnstile> pa \<leadsto> p \<longrightarrow> capClass (cteCap ctea) = capClass (cteCap cte); pa \<noteq> p; m pa = Some ctea; m(p \<mapsto> CTE cap initMDBNode) \<turnstile> pa \<leadsto> p\<rbrakk> \<Longrightarrow> capClass (cteCap ctea) = capClass cap
 2. \<And>pa p'. \<lbrakk>no_0 m; m p = Some cte; no_mdb cte; valid_dlist m; \<forall>cte. m pa = Some cte \<longrightarrow> (\<forall>cte'. m p' = Some cte' \<longrightarrow> m \<turnstile> pa \<leadsto> p' \<longrightarrow> capClass (cteCap cte) = capClass (cteCap cte')); p' \<noteq> p; pa = p\<rbrakk> \<Longrightarrow> \<forall>cte'. m p' = Some cte' \<longrightarrow> m(p \<mapsto> CTE cap initMDBNode) \<turnstile> p \<leadsto> p' \<longrightarrow> capClass cap = capClass (cteCap cte')
 3. \<And>pa p'. \<lbrakk>no_0 m; m p = Some cte; no_mdb cte; valid_dlist m; \<forall>cte. m pa = Some cte \<longrightarrow> (\<forall>cte'. m p' = Some cte' \<longrightarrow> m \<turnstile> pa \<leadsto> p' \<longrightarrow> capClass (cteCap cte) = capClass (cteCap cte')); p' \<noteq> p; pa \<noteq> p\<rbrakk> \<Longrightarrow> \<forall>cte. m pa = Some cte \<longrightarrow> (\<forall>cte'. m p' = Some cte' \<longrightarrow> m(p \<mapsto> CTE cap initMDBNode) \<turnstile> pa \<leadsto> p' \<longrightarrow> capClass (cteCap cte) = capClass (cteCap cte')) proof (prove)
goal (6 subgoals):
 1. \<And>pa ctea. \<lbrakk>no_0 m; m p = Some cte; no_mdb cte; valid_dlist m; m \<turnstile> pa \<leadsto> p \<longrightarrow> capClass (cteCap ctea) = capClass (cteCap cte); pa \<noteq> p; m pa = Some ctea\<rbrakk> \<Longrightarrow> no_mdb (CTE cap initMDBNode)
 2. \<And>pa ctea. \<lbrakk>no_0 m; m p = Some cte; no_mdb cte; valid_dlist m; m \<turnstile> pa \<leadsto> p \<longrightarrow> capClass (cteCap ctea) = capClass (cteCap cte); pa \<noteq> p; m pa = Some ctea\<rbrakk> \<Longrightarrow> valid_dlist (m(p \<mapsto> CTE cap initMDBNode))
 3. \<And>pa ctea. \<lbrakk>no_0 m; m p = Some cte; no_mdb cte; valid_dlist m; m \<turnstile> pa \<leadsto> p \<longrightarrow> capClass (cteCap ctea) = capClass (cteCap cte); pa \<noteq> p; m pa = Some ctea\<rbrakk> \<Longrightarrow> no_0 (m(p \<mapsto> CTE cap initMDBNode))
 4. \<And>pa ctea. \<lbrakk>no_0 m; m p = Some cte; no_mdb cte; valid_dlist m; m \<turnstile> pa \<leadsto> p \<longrightarrow> capClass (cteCap ctea) = capClass (cteCap cte); pa \<noteq> p; m pa = Some ctea; p \<noteq> p\<rbrakk> \<Longrightarrow> capClass (cteCap ctea) = capClass cap
 5. \<And>pa p'. \<lbrakk>no_0 m; m p = Some cte; no_mdb cte; valid_dlist m; \<forall>cte. m pa = Some cte \<longrightarrow> (\<forall>cte'. m p' = Some cte' \<longrightarrow> m \<turnstile> pa \<leadsto> p' \<longrightarrow> capClass (cteCap cte) = capClass (cteCap cte')); p' \<noteq> p; pa = p\<rbrakk> \<Longrightarrow> \<forall>cte'. m p' = Some cte' \<longrightarrow> m(p \<mapsto> CTE cap initMDBNode) \<turnstile> p \<leadsto> p' \<longrightarrow> capClass cap = capClass (cteCap cte')
 6. \<And>pa p'. \<lbrakk>no_0 m; m p = Some cte; no_mdb cte; valid_dlist m; \<forall>cte. m pa = Some cte \<longrightarrow> (\<forall>cte'. m p' = Some cte' \<longrightarrow> m \<turnstile> pa \<leadsto> p' \<longrightarrow> capClass (cteCap cte) = capClass (cteCap cte')); p' \<noteq> p; pa \<noteq> p\<rbrakk> \<Longrightarrow> \<forall>cte. m pa = Some cte \<longrightarrow> (\<forall>cte'. m p' = Some cte' \<longrightarrow> m(p \<mapsto> CTE cap initMDBNode) \<turnstile> pa \<leadsto> p' \<longrightarrow> capClass (cteCap cte) = capClass (cteCap cte')) proof (prove)
goal (5 subgoals):
 1. \<And>pa ctea. \<lbrakk>no_0 m; m p = Some cte; no_mdb cte; valid_dlist m; m \<turnstile> pa \<leadsto> p \<longrightarrow> capClass (cteCap ctea) = capClass (cteCap cte); pa \<noteq> p; m pa = Some ctea\<rbrakk> \<Longrightarrow> valid_dlist (m(p \<mapsto> CTE cap initMDBNode))
 2. \<And>pa ctea. \<lbrakk>no_0 m; m p = Some cte; no_mdb cte; valid_dlist m; m \<turnstile> pa \<leadsto> p \<longrightarrow> capClass (cteCap ctea) = capClass (cteCap cte); pa \<noteq> p; m pa = Some ctea\<rbrakk> \<Longrightarrow> no_0 (m(p \<mapsto> CTE cap initMDBNode))
 3. \<And>pa ctea. \<lbrakk>no_0 m; m p = Some cte; no_mdb cte; valid_dlist m; m \<turnstile> pa \<leadsto> p \<longrightarrow> capClass (cteCap ctea) = capClass (cteCap cte); pa \<noteq> p; m pa = Some ctea; p \<noteq> p\<rbrakk> \<Longrightarrow> capClass (cteCap ctea) = capClass cap
 4. \<And>pa p'. \<lbrakk>no_0 m; m p = Some cte; no_mdb cte; valid_dlist m; \<forall>cte. m pa = Some cte \<longrightarrow> (\<forall>cte'. m p' = Some cte' \<longrightarrow> m \<turnstile> pa \<leadsto> p' \<longrightarrow> capClass (cteCap cte) = capClass (cteCap cte')); p' \<noteq> p; pa = p\<rbrakk> \<Longrightarrow> \<forall>cte'. m p' = Some cte' \<longrightarrow> m(p \<mapsto> CTE cap initMDBNode) \<turnstile> p \<leadsto> p' \<longrightarrow> capClass cap = capClass (cteCap cte')
 5. \<And>pa p'. \<lbrakk>no_0 m; m p = Some cte; no_mdb cte; valid_dlist m; \<forall>cte. m pa = Some cte \<longrightarrow> (\<forall>cte'. m p' = Some cte' \<longrightarrow> m \<turnstile> pa \<leadsto> p' \<longrightarrow> capClass (cteCap cte) = capClass (cteCap cte')); p' \<noteq> p; pa \<noteq> p\<rbrakk> \<Longrightarrow> \<forall>cte. m pa = Some cte \<longrightarrow> (\<forall>cte'. m p' = Some cte' \<longrightarrow> m(p \<mapsto> CTE cap initMDBNode) \<turnstile> pa \<leadsto> p' \<longrightarrow> capClass (cteCap cte) = capClass (cteCap cte')) proof (prove)
goal (4 subgoals):
 1. \<And>pa ctea. \<lbrakk>no_0 m; m p = Some cte; no_mdb cte; valid_dlist m; m \<turnstile> pa \<leadsto> p \<longrightarrow> capClass (cteCap ctea) = capClass (cteCap cte); pa \<noteq> p; m pa = Some ctea\<rbrakk> \<Longrightarrow> no_0 (m(p \<mapsto> CTE cap initMDBNode))
 2. \<And>pa ctea. \<lbrakk>no_0 m; m p = Some cte; no_mdb cte; valid_dlist m; m \<turnstile> pa \<leadsto> p \<longrightarrow> capClass (cteCap ctea) = capClass (cteCap cte); pa \<noteq> p; m pa = Some ctea; p \<noteq> p\<rbrakk> \<Longrightarrow> capClass (cteCap ctea) = capClass cap
 3. \<And>pa p'. \<lbrakk>no_0 m; m p = Some cte; no_mdb cte; valid_dlist m; \<forall>cte. m pa = Some cte \<longrightarrow> (\<forall>cte'. m p' = Some cte' \<longrightarrow> m \<turnstile> pa \<leadsto> p' \<longrightarrow> capClass (cteCap cte) = capClass (cteCap cte')); p' \<noteq> p; pa = p\<rbrakk> \<Longrightarrow> \<forall>cte'. m p' = Some cte' \<longrightarrow> m(p \<mapsto> CTE cap initMDBNode) \<turnstile> p \<leadsto> p' \<longrightarrow> capClass cap = capClass (cteCap cte')
 4. \<And>pa p'. \<lbrakk>no_0 m; m p = Some cte; no_mdb cte; valid_dlist m; \<forall>cte. m pa = Some cte \<longrightarrow> (\<forall>cte'. m p' = Some cte' \<longrightarrow> m \<turnstile> pa \<leadsto> p' \<longrightarrow> capClass (cteCap cte) = capClass (cteCap cte')); p' \<noteq> p; pa \<noteq> p\<rbrakk> \<Longrightarrow> \<forall>cte. m pa = Some cte \<longrightarrow> (\<forall>cte'. m p' = Some cte' \<longrightarrow> m(p \<mapsto> CTE cap initMDBNode) \<turnstile> pa \<leadsto> p' \<longrightarrow> capClass (cteCap cte) = capClass (cteCap cte')) proof (prove)
goal (3 subgoals):
 1. \<And>pa ctea. \<lbrakk>no_0 m; m p = Some cte; no_mdb cte; valid_dlist m; m \<turnstile> pa \<leadsto> p \<longrightarrow> capClass (cteCap ctea) = capClass (cteCap cte); pa \<noteq> p; m pa = Some ctea; p \<noteq> p\<rbrakk> \<Longrightarrow> capClass (cteCap ctea) = capClass cap
 2. \<And>pa p'. \<lbrakk>no_0 m; m p = Some cte; no_mdb cte; valid_dlist m; \<forall>cte. m pa = Some cte \<longrightarrow> (\<forall>cte'. m p' = Some cte' \<longrightarrow> m \<turnstile> pa \<leadsto> p' \<longrightarrow> capClass (cteCap cte) = capClass (cteCap cte')); p' \<noteq> p; pa = p\<rbrakk> \<Longrightarrow> \<forall>cte'. m p' = Some cte' \<longrightarrow> m(p \<mapsto> CTE cap initMDBNode) \<turnstile> p \<leadsto> p' \<longrightarrow> capClass cap = capClass (cteCap cte')
 3. \<And>pa p'. \<lbrakk>no_0 m; m p = Some cte; no_mdb cte; valid_dlist m; \<forall>cte. m pa = Some cte \<longrightarrow> (\<forall>cte'. m p' = Some cte' \<longrightarrow> m \<turnstile> pa \<leadsto> p' \<longrightarrow> capClass (cteCap cte) = capClass (cteCap cte')); p' \<noteq> p; pa \<noteq> p\<rbrakk> \<Longrightarrow> \<forall>cte. m pa = Some cte \<longrightarrow> (\<forall>cte'. m p' = Some cte' \<longrightarrow> m(p \<mapsto> CTE cap initMDBNode) \<turnstile> pa \<leadsto> p' \<longrightarrow> capClass (cteCap cte) = capClass (cteCap cte')) proof (prove)
goal (2 subgoals):
 1. \<And>pa p'. \<lbrakk>no_0 m; m p = Some cte; no_mdb cte; valid_dlist m; \<forall>cte. m pa = Some cte \<longrightarrow> (\<forall>cte'. m p' = Some cte' \<longrightarrow> m \<turnstile> pa \<leadsto> p' \<longrightarrow> capClass (cteCap cte) = capClass (cteCap cte')); p' \<noteq> p; pa = p\<rbrakk> \<Longrightarrow> \<forall>cte'. m p' = Some cte' \<longrightarrow> m(p \<mapsto> CTE cap initMDBNode) \<turnstile> p \<leadsto> p' \<longrightarrow> capClass cap = capClass (cteCap cte')
 2. \<And>pa p'. \<lbrakk>no_0 m; m p = Some cte; no_mdb cte; valid_dlist m; \<forall>cte. m pa = Some cte \<longrightarrow> (\<forall>cte'. m p' = Some cte' \<longrightarrow> m \<turnstile> pa \<leadsto> p' \<longrightarrow> capClass (cteCap cte) = capClass (cteCap cte')); p' \<noteq> p; pa \<noteq> p\<rbrakk> \<Longrightarrow> \<forall>cte. m pa = Some cte \<longrightarrow> (\<forall>cte'. m p' = Some cte' \<longrightarrow> m(p \<mapsto> CTE cap initMDBNode) \<turnstile> pa \<leadsto> p' \<longrightarrow> capClass (cteCap cte) = capClass (cteCap cte')) proof (prove)
goal (1 subgoal):
 1. \<And>pa p'. \<lbrakk>no_0 m; m p = Some cte; no_mdb cte; valid_dlist m; \<forall>cte. m pa = Some cte \<longrightarrow> (\<forall>cte'. m p' = Some cte' \<longrightarrow> m \<turnstile> pa \<leadsto> p' \<longrightarrow> capClass (cteCap cte) = capClass (cteCap cte')); p' \<noteq> p; pa \<noteq> p\<rbrakk> \<Longrightarrow> \<forall>cte. m pa = Some cte \<longrightarrow> (\<forall>cte'. m p' = Some cte' \<longrightarrow> m(p \<mapsto> CTE cap initMDBNode) \<turnstile> pa \<leadsto> p' \<longrightarrow> capClass (cteCap cte) = capClass (cteCap cte')) proof (prove)
goal:
No subgoals!