theory Retype_R

lemma class_links_n:
  "class_links n" using class_links_m apply (simp add: class_links_def) apply (elim allEI) apply clarsimp apply (subgoal_tac "p' \<noteq> nullPointer") apply (simp add: n_next split: if_split_asm) apply (case_tac cte, case_tac cte') apply (clarsimp simp add: n_Some_eq split: if_split_asm) apply (drule(1) next_not_P2) apply simp apply (clarsimp simp: no_0_n nullPointer_def) done

(* Proof state trace *)
proof (prove)
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. \<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')) \<Longrightarrow> \<forall>p p' cte. n p = Some cte \<longrightarrow> (\<forall>cte'. n p' = Some cte' \<longrightarrow> n \<turnstile> p \<leadsto> p' \<longrightarrow> capClass (cteCap cte) = capClass (cteCap cte')) proof (prove)
goal (1 subgoal):
 1. \<And>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')) \<Longrightarrow> n p = Some cte \<longrightarrow> (\<forall>cte'. n p' = Some cte' \<longrightarrow> n \<turnstile> p \<leadsto> p' \<longrightarrow> capClass (cteCap cte) = capClass (cteCap cte')) proof (prove)
goal (1 subgoal):
 1. \<And>p p' cte cte'. \<lbrakk>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 (2 subgoals):
 1. \<And>p p' cte cte'. \<lbrakk>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'; p' \<noteq> nullPointer\<rbrakk> \<Longrightarrow> capClass (cteCap cte) = capClass (cteCap cte')
 2. \<And>p p' cte cte'. \<lbrakk>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> p' \<noteq> nullPointer proof (prove)
goal (2 subgoals):
 1. \<And>p p' cte cte'. \<lbrakk>p' \<noteq> nullPointer; m p = Some cte \<longrightarrow> (\<forall>cte'. m p' = Some cte' \<longrightarrow> capClass (cteCap cte) = capClass (cteCap cte')); n p = Some cte; n p' = Some cte'; \<not> P p; m \<turnstile> p \<leadsto> p'\<rbrakk> \<Longrightarrow> capClass (cteCap cte) = capClass (cteCap cte')
 2. \<And>p p' cte cte'. \<lbrakk>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> p' \<noteq> nullPointer proof (prove)
goal (2 subgoals):
 1. \<And>p p' cte cte' x1 x2 x1a x2a. \<lbrakk>p' \<noteq> nullPointer; m p = Some cte \<longrightarrow> (\<forall>cte'. m p' = Some cte' \<longrightarrow> capClass (cteCap cte) = capClass (cteCap cte')); n p = Some cte; n p' = Some cte'; \<not> P p; m \<turnstile> p \<leadsto> p'; cte = CTE x1 x2; cte' = CTE x1a x2a\<rbrakk> \<Longrightarrow> capClass (cteCap cte) = capClass (cteCap cte')
 2. \<And>p p' cte cte'. \<lbrakk>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> p' \<noteq> nullPointer proof (prove)
goal (2 subgoals):
 1. \<And>p p' x1 x2. \<lbrakk>\<not> P p; m \<turnstile> p \<leadsto> p'; p' \<noteq> nullPointer; \<forall>cte'. m p' = Some cte' \<longrightarrow> capClass x1 = capClass (cteCap cte'); m p = Some (CTE x1 x2); P p'\<rbrakk> \<Longrightarrow> capClass x1 = NullClass
 2. \<And>p p' cte cte'. \<lbrakk>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> p' \<noteq> nullPointer proof (prove)
goal (2 subgoals):
 1. \<And>p p' x1 x2. \<lbrakk>\<not> P p; p' \<noteq> nullPointer; \<forall>cte'. m p' = Some cte' \<longrightarrow> capClass x1 = capClass (cteCap cte'); m p = Some (CTE x1 x2); P p'; \<not> P p'\<rbrakk> \<Longrightarrow> capClass x1 = NullClass
 2. \<And>p p' cte cte'. \<lbrakk>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> p' \<noteq> nullPointer proof (prove)
goal (1 subgoal):
 1. \<And>p p' cte cte'. \<lbrakk>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> p' \<noteq> nullPointer proof (prove)
goal:
No subgoals!