theory CNodeInv_R

lemma class_links_n: "class_links n" proof - from valid have "class_links m" by (simp add: valid_mdb_ctes_def) thus ?thesis apply (clarsimp simp: class_links_def) apply (case_tac cte, case_tac cte', clarsimp) apply (drule n_cap)+ apply (simp add: imp_conjL[symmetric]) apply (subst(asm) conj_commute) apply (simp add: imp_conjL) apply (simp add: imp_conjL[symmetric]) apply (subst(asm) conj_commute) apply (simp add: imp_conjL next_m_n2) apply (elim allE, drule(1) mp) apply (auto simp: s_d_swap_def src dest
               split: if_split_asm) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. class_links n proof (state)
goal (1 subgoal):
 1. class_links n proof (chain)
picking this:
valid_mdb_ctes m proof (prove)
using this:
valid_mdb_ctes m

goal (1 subgoal):
 1. class_links m proof (state)
this:
class_links m

goal (1 subgoal):
 1. class_links n proof (prove)
using this:
class_links m

goal (1 subgoal):
 1. class_links n proof (prove)
goal (1 subgoal):
 1. \<And>p p' cte cte'. \<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')); n p = Some cte; n p' = Some cte'; n \<turnstile> p \<leadsto> p'\<rbrakk> \<Longrightarrow> capClass (cteCap cte) = capClass (cteCap cte') proof (prove)
goal (1 subgoal):
 1. \<And>p p' x1 x2 x1a x2a. \<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')); n p = Some (CTE x1 x2); n p' = Some (CTE x1a x2a); n \<turnstile> p \<leadsto> p'\<rbrakk> \<Longrightarrow> capClass x1 = capClass x1a proof (prove)
goal (1 subgoal):
 1. \<And>p p' x1 x2 x1a x2a. \<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')); n \<turnstile> p \<leadsto> p'; if p = src then x1 = dcap else if p = dest then x1 = scap else \<exists>node'. m p = Some (CTE x1 node'); if p' = src then x1a = dcap else if p' = dest then x1a = scap else \<exists>node'. m p' = Some (CTE x1a node')\<rbrakk> \<Longrightarrow> capClass x1 = capClass x1a proof (prove)
goal (1 subgoal):
 1. \<And>p p' x1 x1a. \<lbrakk>\<forall>p p' cte. m p = Some cte \<longrightarrow> (\<forall>cte'. m p' = Some cte' \<and> m \<turnstile> p \<leadsto> p' \<longrightarrow> capClass (cteCap cte) = capClass (cteCap cte')); n \<turnstile> p \<leadsto> p'; if p = src then x1 = dcap else if p = dest then x1 = scap else \<exists>node'. m p = Some (CTE x1 node'); if p' = src then x1a = dcap else if p' = dest then x1a = scap else \<exists>node'. m p' = Some (CTE x1a node')\<rbrakk> \<Longrightarrow> capClass x1 = capClass x1a proof (prove)
goal (1 subgoal):
 1. \<And>p p' x1 x1a. \<lbrakk>\<forall>p p' cte. m p = Some cte \<longrightarrow> (\<forall>cte'. m \<turnstile> p \<leadsto> p' \<and> m p' = Some cte' \<longrightarrow> capClass (cteCap cte) = capClass (cteCap cte')); n \<turnstile> p \<leadsto> p'; if p = src then x1 = dcap else if p = dest then x1 = scap else \<exists>node'. m p = Some (CTE x1 node'); if p' = src then x1a = dcap else if p' = dest then x1a = scap else \<exists>node'. m p' = Some (CTE x1a node')\<rbrakk> \<Longrightarrow> capClass x1 = capClass x1a proof (prove)
goal (1 subgoal):
 1. \<And>p p' x1 x1a. \<lbrakk>\<forall>p p' cte. m p = Some cte \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> (\<forall>cte'. m p' = Some cte' \<longrightarrow> capClass (cteCap cte) = capClass (cteCap cte')); n \<turnstile> p \<leadsto> p'; if p = src then x1 = dcap else if p = dest then x1 = scap else \<exists>node'. m p = Some (CTE x1 node'); if p' = src then x1a = dcap else if p' = dest then x1a = scap else \<exists>node'. m p' = Some (CTE x1a node')\<rbrakk> \<Longrightarrow> capClass x1 = capClass x1a proof (prove)
goal (1 subgoal):
 1. \<And>p p' x1 x1a. \<lbrakk>\<forall>p p' cte. m p = Some cte \<and> m \<turnstile> p \<leadsto> p' \<longrightarrow> (\<forall>cte'. m p' = Some cte' \<longrightarrow> capClass (cteCap cte) = capClass (cteCap cte')); n \<turnstile> p \<leadsto> p'; if p = src then x1 = dcap else if p = dest then x1 = scap else \<exists>node'. m p = Some (CTE x1 node'); if p' = src then x1a = dcap else if p' = dest then x1a = scap else \<exists>node'. m p' = Some (CTE x1a node')\<rbrakk> \<Longrightarrow> capClass x1 = capClass x1a proof (prove)
goal (1 subgoal):
 1. \<And>p p' x1 x1a. \<lbrakk>\<forall>p p' cte. m \<turnstile> p \<leadsto> p' \<and> m p = Some cte \<longrightarrow> (\<forall>cte'. m p' = Some cte' \<longrightarrow> capClass (cteCap cte) = capClass (cteCap cte')); n \<turnstile> p \<leadsto> p'; if p = src then x1 = dcap else if p = dest then x1 = scap else \<exists>node'. m p = Some (CTE x1 node'); if p' = src then x1a = dcap else if p' = dest then x1a = scap else \<exists>node'. m p' = Some (CTE x1a node')\<rbrakk> \<Longrightarrow> capClass x1 = capClass x1a proof (prove)
goal (1 subgoal):
 1. \<And>p p' x1 x1a. \<lbrakk>\<forall>p p'. m \<turnstile> p \<leadsto> p' \<longrightarrow> (\<forall>cte. m p = Some cte \<longrightarrow> (\<forall>cte'. m p' = Some cte' \<longrightarrow> capClass (cteCap cte) = capClass (cteCap cte'))); m \<turnstile> s_d_swap p src dest \<leadsto> s_d_swap p' src dest; if p = src then x1 = dcap else if p = dest then x1 = scap else \<exists>node'. m p = Some (CTE x1 node'); if p' = src then x1a = dcap else if p' = dest then x1a = scap else \<exists>node'. m p' = Some (CTE x1a node')\<rbrakk> \<Longrightarrow> capClass x1 = capClass x1a proof (prove)
goal (1 subgoal):
 1. \<And>p p' x1 x1a. \<lbrakk>m \<turnstile> s_d_swap p src dest \<leadsto> s_d_swap p' src dest; if p = src then x1 = dcap else if p = dest then x1 = scap else \<exists>node'. m p = Some (CTE x1 node'); if p' = src then x1a = dcap else if p' = dest then x1a = scap else \<exists>node'. m p' = Some (CTE x1a node'); \<forall>cte. m (s_d_swap p src dest) = Some cte \<longrightarrow> (\<forall>cte'. m (s_d_swap p' src dest) = Some cte' \<longrightarrow> capClass (cteCap cte) = capClass (cteCap cte'))\<rbrakk> \<Longrightarrow> capClass x1 = capClass x1a proof (prove)
goal:
No subgoals! proof (state)
this:
class_links n

goal:
No subgoals!