theory CSpace_R

lemma class_links' [simp]:
  "class_links n'" using src dest apply (clarsimp simp: class_links_def) apply (simp add: n_direct_eq') apply (case_tac cte, case_tac cte') apply clarsimp apply (drule n'_cap)+ apply clarsimp apply (clarsimp split: if_split_asm) apply (drule (2) class_linksD, rule class_links) apply simp apply (drule (2) class_linksD, rule class_links) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. class_links n' proof (prove)
using this:
m src = Some (CTE src_cap src_node)
m dest = Some (CTE dest_cap dest_node)

goal (1 subgoal):
 1. class_links n' proof (prove)
goal (1 subgoal):
 1. \<And>p p' cte cte'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); 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' cte cte'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); n' p = Some cte; n' p' = Some cte'; if p = src then p' = dest else if p = dest then m \<turnstile> src \<leadsto> p' else m \<turnstile> p \<leadsto> p'\<rbrakk> \<Longrightarrow> capClass (cteCap cte) = capClass (cteCap cte') proof (prove)
goal (1 subgoal):
 1. \<And>p p' cte cte' x1 x2 x1a x2a. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); n' p = Some cte; n' p' = Some cte'; if p = src then p' = dest else if p = dest then m \<turnstile> src \<leadsto> p' else m \<turnstile> p \<leadsto> p'; cte = CTE x1 x2; cte' = CTE x1a x2a\<rbrakk> \<Longrightarrow> capClass (cteCap cte) = capClass (cteCap cte') proof (prove)
goal (1 subgoal):
 1. \<And>p p' x1 x2 x1a x2a. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); n' p = Some (CTE x1 x2); n' p' = Some (CTE x1a x2a); if p = src then p' = dest else if p = dest then m \<turnstile> src \<leadsto> p' else m \<turnstile> p \<leadsto> p'\<rbrakk> \<Longrightarrow> capClass x1 = capClass x1a proof (prove)
goal (1 subgoal):
 1. \<And>p p' x1 x2 x1a x2a. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); if p = src then p' = dest else if p = dest then m \<turnstile> src \<leadsto> p' else m \<turnstile> p \<leadsto> p'; \<exists>node'. if p = dest then x1 = c' \<and> m p = Some (CTE dest_cap node') else m p = Some (CTE x1 node'); \<exists>node'. if p' = dest then x1a = c' \<and> m p' = Some (CTE dest_cap node') else m p' = Some (CTE x1a node')\<rbrakk> \<Longrightarrow> capClass x1 = capClass x1a proof (prove)
goal (1 subgoal):
 1. \<And>p p' x1 x1a node' node'a. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); if p = src then p' = dest else if p = dest then m \<turnstile> src \<leadsto> p' else m \<turnstile> p \<leadsto> p'; if p = dest then x1 = c' \<and> dest_node = node' else m p = Some (CTE x1 node'); if p' = dest then x1a = c' \<and> dest_node = node'a else m p' = Some (CTE x1a node'a)\<rbrakk> \<Longrightarrow> capClass x1 = capClass x1a proof (prove)
goal (2 subgoals):
 1. \<And>p' x1a node'a. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); m \<turnstile> src \<leadsto> p'; p' \<noteq> dest; m p' = Some (CTE x1a node'a)\<rbrakk> \<Longrightarrow> capClass src_cap = capClass x1a
 2. \<And>p p' x1 x1a node' node'a. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> src; m \<turnstile> p \<leadsto> p'; p \<noteq> dest; m p = Some (CTE x1 node'); p' \<noteq> dest; m p' = Some (CTE x1a node'a)\<rbrakk> \<Longrightarrow> capClass x1 = capClass x1a proof (prove)
goal (2 subgoals):
 1. \<And>p' x1a node'a. \<lbrakk>m dest = Some (CTE dest_cap dest_node); m \<turnstile> src \<leadsto> p'; p' \<noteq> dest; m p' = Some (CTE x1a node'a); capClass (cteCap (CTE src_cap src_node)) = capClass (cteCap (CTE x1a node'a))\<rbrakk> \<Longrightarrow> capClass src_cap = capClass x1a
 2. \<And>p p' x1 x1a node' node'a. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> src; m \<turnstile> p \<leadsto> p'; p \<noteq> dest; m p = Some (CTE x1 node'); p' \<noteq> dest; m p' = Some (CTE x1a node'a)\<rbrakk> \<Longrightarrow> capClass x1 = capClass x1a proof (prove)
goal (1 subgoal):
 1. \<And>p p' x1 x1a node' node'a. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> src; m \<turnstile> p \<leadsto> p'; p \<noteq> dest; m p = Some (CTE x1 node'); p' \<noteq> dest; m p' = Some (CTE x1a node'a)\<rbrakk> \<Longrightarrow> capClass x1 = capClass x1a proof (prove)
goal (1 subgoal):
 1. \<And>p p' x1 x1a node' node'a. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> src; m \<turnstile> p \<leadsto> p'; p \<noteq> dest; p' \<noteq> dest; m p' = Some (CTE x1a node'a); capClass (cteCap (CTE x1 node')) = capClass (cteCap (CTE x1a node'a))\<rbrakk> \<Longrightarrow> capClass x1 = capClass x1a proof (prove)
goal:
No subgoals!