theory Untyped_R

lemma class_links [simp]: "class_links n'" using class_links_m apply (clarsimp simp add: class_links_def) apply (simp add: n'_direct_eq
            split: if_split_asm) apply (case_tac cte,
           clarsimp dest!: n'_cap simp: site' parent new_site_def phys parent_phys) apply (drule_tac x=parent in spec) apply (drule_tac x=p' in spec) apply (case_tac cte') apply (clarsimp simp: site' new_site_def parent parent_phys phys dest!: n'_cap
                  split: if_split_asm) apply (case_tac cte, case_tac cte') apply (clarsimp dest!: n'_cap split: if_split_asm) apply fastforce 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. \<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 (3 subgoals):
 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' parent = Some cte; n' site = Some cte'; p = parent; p' = site\<rbrakk> \<Longrightarrow> capClass (cteCap cte) = capClass (cteCap cte')
 2. \<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' site = Some cte; n' p' = Some cte'; p = site; m \<turnstile> parent \<leadsto> p'\<rbrakk> \<Longrightarrow> capClass (cteCap cte) = capClass (cteCap cte')
 3. \<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'; p \<noteq> parent; p \<noteq> site; m \<turnstile> p \<leadsto> p'\<rbrakk> \<Longrightarrow> capClass (cteCap cte) = capClass (cteCap cte') proof (prove)
goal (2 subgoals):
 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' site = Some cte; n' p' = Some cte'; p = site; m \<turnstile> parent \<leadsto> p'\<rbrakk> \<Longrightarrow> capClass (cteCap cte) = capClass (cteCap cte')
 2. \<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'; p \<noteq> parent; p \<noteq> site; m \<turnstile> p \<leadsto> p'\<rbrakk> \<Longrightarrow> capClass (cteCap cte) = capClass (cteCap cte') proof (prove)
goal (2 subgoals):
 1. \<And>p p' cte cte'. \<lbrakk>n' site = Some cte; n' p' = Some cte'; p = site; m \<turnstile> parent \<leadsto> p'; \<forall>p' cte. m parent = Some cte \<longrightarrow> (\<forall>cte'. m p' = Some cte' \<longrightarrow> m \<turnstile> parent \<leadsto> p' \<longrightarrow> capClass (cteCap cte) = capClass (cteCap cte'))\<rbrakk> \<Longrightarrow> capClass (cteCap cte) = capClass (cteCap cte')
 2. \<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'; p \<noteq> parent; p \<noteq> site; m \<turnstile> p \<leadsto> p'\<rbrakk> \<Longrightarrow> capClass (cteCap cte) = capClass (cteCap cte') proof (prove)
goal (2 subgoals):
 1. \<And>p p' cte cte'. \<lbrakk>n' site = Some cte; n' p' = Some cte'; p = site; m \<turnstile> parent \<leadsto> p'; \<forall>cte. m parent = Some cte \<longrightarrow> (\<forall>cte'. m p' = Some cte' \<longrightarrow> m \<turnstile> parent \<leadsto> p' \<longrightarrow> capClass (cteCap cte) = capClass (cteCap cte'))\<rbrakk> \<Longrightarrow> capClass (cteCap cte) = capClass (cteCap cte')
 2. \<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'; p \<noteq> parent; p \<noteq> site; m \<turnstile> p \<leadsto> p'\<rbrakk> \<Longrightarrow> capClass (cteCap cte) = capClass (cteCap cte') proof (prove)
goal (2 subgoals):
 1. \<And>p p' cte cte' x1 x2. \<lbrakk>n' site = Some cte; n' p' = Some cte'; p = site; m \<turnstile> parent \<leadsto> p'; \<forall>cte. m parent = Some cte \<longrightarrow> (\<forall>cte'. m p' = Some cte' \<longrightarrow> m \<turnstile> parent \<leadsto> p' \<longrightarrow> capClass (cteCap cte) = capClass (cteCap cte')); cte' = CTE x1 x2\<rbrakk> \<Longrightarrow> capClass (cteCap cte) = capClass (cteCap cte')
 2. \<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'; p \<noteq> parent; p \<noteq> site; 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>\<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'; p \<noteq> parent; p \<noteq> site; 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>\<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'; p \<noteq> parent; p \<noteq> site; 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 x1a node' node'a. \<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')); p \<noteq> parent; p \<noteq> site; m \<turnstile> p \<leadsto> p'; p' \<noteq> site; m p = Some (CTE x1 node'); m p' = Some (CTE x1a node'a)\<rbrakk> \<Longrightarrow> capClass x1 = capClass x1a proof (prove)
goal:
No subgoals!