theory CSpace1_R

lemma class_links_preserve_oneway:
  assumes dom:"\<And>x. (x \<in> dom m) = (x \<in> dom m')"
  assumes misc:"\<And>x cte cte'. \<lbrakk>m x =Some cte;m' x = Some cte'\<rbrakk> \<Longrightarrow> capClass (cteCap cte) = capClass (cteCap cte')"
  assumes node:"\<And>p. mdb_next m p = mdb_next m' p"
  shows  "class_links m \<Longrightarrow> class_links m'" apply (clarsimp simp:class_links_def Let_def) apply (drule_tac x = p in spec) apply (drule_tac x = p' in spec) apply (frule domI[where m = m'],drule iffD2[OF dom],erule domE) apply (case_tac r) apply clarsimp apply (frule_tac b = cte' in domI[where m = m'],drule iffD2[OF dom],erule domE) apply (elim allE impE) apply simp apply (frule(1) misc) apply (clarsimp simp:mdb_next_rel_def node) apply (drule(1) misc)+ apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. class_links m \<Longrightarrow> class_links m' 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')); m' p = Some cte; m' p' = Some cte'; m' \<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' p = Some cte; m' p' = Some cte'; m' \<turnstile> p \<leadsto> p'; \<forall>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'))\<rbrakk> \<Longrightarrow> capClass (cteCap cte) = capClass (cteCap cte') proof (prove)
goal (1 subgoal):
 1. \<And>p p' cte cte'. \<lbrakk>m' p = Some cte; m' p' = Some cte'; m' \<turnstile> p \<leadsto> p'; \<forall>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'))\<rbrakk> \<Longrightarrow> capClass (cteCap cte) = capClass (cteCap cte') proof (prove)
goal (1 subgoal):
 1. \<And>p p' cte cte' r. \<lbrakk>m' p = Some cte; m' p' = Some cte'; m' \<turnstile> p \<leadsto> p'; \<forall>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')); m p = Some r\<rbrakk> \<Longrightarrow> capClass (cteCap cte) = capClass (cteCap cte') proof (prove)
goal (1 subgoal):
 1. \<And>p p' cte cte' r x1 x2. \<lbrakk>m' p = Some cte; m' p' = Some cte'; m' \<turnstile> p \<leadsto> p'; \<forall>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')); m p = Some r; r = CTE x1 x2\<rbrakk> \<Longrightarrow> capClass (cteCap cte) = capClass (cteCap cte') proof (prove)
goal (1 subgoal):
 1. \<And>p p' cte cte' x1 x2. \<lbrakk>m' p = Some cte; m' p' = Some cte'; m' \<turnstile> p \<leadsto> p'; \<forall>cte'. m p' = Some cte' \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capClass x1 = capClass (cteCap cte'); m p = Some (CTE x1 x2)\<rbrakk> \<Longrightarrow> capClass (cteCap cte) = capClass (cteCap cte') proof (prove)
goal (1 subgoal):
 1. \<And>p p' cte cte' x1 x2 r. \<lbrakk>m' p = Some cte; m' p' = Some cte'; m' \<turnstile> p \<leadsto> p'; \<forall>cte'. m p' = Some cte' \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capClass x1 = capClass (cteCap cte'); m p = Some (CTE x1 x2); m p' = Some r\<rbrakk> \<Longrightarrow> capClass (cteCap cte) = capClass (cteCap cte') proof (prove)
goal (3 subgoals):
 1. \<And>p p' cte cte' x1 x2 r. \<lbrakk>m' p = Some cte; m' p' = Some cte'; m' \<turnstile> p \<leadsto> p'; m p = Some (CTE x1 x2); m p' = Some r\<rbrakk> \<Longrightarrow> m p' = Some (?cte'28 p p' cte cte' x1 x2 r)
 2. \<And>p p' cte cte' x1 x2 r. \<lbrakk>m' p = Some cte; m' p' = Some cte'; m' \<turnstile> p \<leadsto> p'; m p = Some (CTE x1 x2); m p' = Some r\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto> p'
 3. \<And>p p' cte cte' x1 x2 r. \<lbrakk>m' p = Some cte; m' p' = Some cte'; m' \<turnstile> p \<leadsto> p'; m p = Some (CTE x1 x2); m p' = Some r; capClass x1 = capClass (cteCap (?cte'28 p p' cte cte' x1 x2 r))\<rbrakk> \<Longrightarrow> capClass (cteCap cte) = capClass (cteCap cte') proof (prove)
goal (2 subgoals):
 1. \<And>p p' cte cte' x1 x2 r. \<lbrakk>m' p = Some cte; m' p' = Some cte'; m' \<turnstile> p \<leadsto> p'; m p = Some (CTE x1 x2); m p' = Some r\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto> p'
 2. \<And>p p' cte cte' x1 x2 r. \<lbrakk>m' p = Some cte; m' p' = Some cte'; m' \<turnstile> p \<leadsto> p'; m p = Some (CTE x1 x2); m p' = Some r; capClass x1 = capClass (cteCap r)\<rbrakk> \<Longrightarrow> capClass (cteCap cte) = capClass (cteCap cte') proof (prove)
goal (2 subgoals):
 1. \<And>p p' cte cte' x1 x2 r. \<lbrakk>m' p = Some cte; m' p' = Some cte'; m' \<turnstile> p \<leadsto> p'; m p = Some (CTE x1 x2); m p' = Some r; capClass (cteCap (CTE x1 x2)) = capClass (cteCap cte)\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto> p'
 2. \<And>p p' cte cte' x1 x2 r. \<lbrakk>m' p = Some cte; m' p' = Some cte'; m' \<turnstile> p \<leadsto> p'; m p = Some (CTE x1 x2); m p' = Some r; capClass x1 = capClass (cteCap r)\<rbrakk> \<Longrightarrow> capClass (cteCap cte) = capClass (cteCap cte') proof (prove)
goal (1 subgoal):
 1. \<And>p p' cte cte' x1 x2 r. \<lbrakk>m' p = Some cte; m' p' = Some cte'; m' \<turnstile> p \<leadsto> p'; m p = Some (CTE x1 x2); m p' = Some r; capClass x1 = capClass (cteCap r)\<rbrakk> \<Longrightarrow> capClass (cteCap cte) = capClass (cteCap cte') proof (prove)
goal (1 subgoal):
 1. \<And>p p' cte cte' x1 x2 r. \<lbrakk>m' p = Some cte; m' p' = Some cte'; m' \<turnstile> p \<leadsto> p'; capClass x1 = capClass (cteCap r); capClass (cteCap (CTE x1 x2)) = capClass (cteCap cte); capClass (cteCap r) = capClass (cteCap cte')\<rbrakk> \<Longrightarrow> capClass (cteCap cte) = capClass (cteCap cte') proof (prove)
goal:
No subgoals!