theory ArchVSpace_AI

lemma no_cap_to_obj_with_diff_ref_map:
  "\<lbrakk> caps_of_state s p = Some cap; is_pt_cap cap \<or> is_pd_cap cap;
     table_cap_ref cap = None;
     unique_table_caps (caps_of_state s);
     valid_objs s; obj_refs cap = obj_refs cap' \<rbrakk>
       \<Longrightarrow> no_cap_to_obj_with_diff_ref cap' {p} s" apply (clarsimp simp: no_cap_to_obj_with_diff_ref_def
                        cte_wp_at_caps_of_state) apply (frule(1) caps_of_state_valid_cap[where p=p]) apply (frule(1) caps_of_state_valid_cap[where p="(a, b)" for a b]) apply (drule(1) valid_cap_obj_ref_pt_pd, simp) apply (drule(1) unique_table_capsD[rotated, where cps="caps_of_state s"]) apply simp apply (simp add: is_pt_pd_cap_asid_None_table_ref) apply fastforce apply assumption apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s p = Some cap; is_pt_cap cap \<or> is_pd_cap cap; table_cap_ref cap = None; unique_table_caps (caps_of_state s); valid_objs s; obj_refs cap = obj_refs cap'\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref cap' {p} s proof (prove)
goal (1 subgoal):
 1. \<And>a b capa. \<lbrakk>caps_of_state s p = Some cap; is_pt_cap cap \<or> is_pd_cap cap; table_cap_ref cap = None; unique_table_caps (caps_of_state s); valid_objs s; obj_refs cap = obj_refs cap'; (a, b) \<noteq> p; obj_refs capa = obj_refs cap'; caps_of_state s (a, b) = Some capa\<rbrakk> \<Longrightarrow> table_cap_ref capa = table_cap_ref cap' proof (prove)
goal (1 subgoal):
 1. \<And>a b capa. \<lbrakk>caps_of_state s p = Some cap; is_pt_cap cap \<or> is_pd_cap cap; table_cap_ref cap = None; unique_table_caps (caps_of_state s); valid_objs s; obj_refs cap = obj_refs cap'; (a, b) \<noteq> p; obj_refs capa = obj_refs cap'; caps_of_state s (a, b) = Some capa; s \<turnstile> cap\<rbrakk> \<Longrightarrow> table_cap_ref capa = table_cap_ref cap' proof (prove)
goal (1 subgoal):
 1. \<And>a b capa. \<lbrakk>caps_of_state s p = Some cap; is_pt_cap cap \<or> is_pd_cap cap; table_cap_ref cap = None; unique_table_caps (caps_of_state s); valid_objs s; obj_refs cap = obj_refs cap'; (a, b) \<noteq> p; obj_refs capa = obj_refs cap'; caps_of_state s (a, b) = Some capa; s \<turnstile> cap; s \<turnstile> capa\<rbrakk> \<Longrightarrow> table_cap_ref capa = table_cap_ref cap' proof (prove)
goal (1 subgoal):
 1. \<And>a b capa. \<lbrakk>caps_of_state s p = Some cap; is_pt_cap cap \<or> is_pd_cap cap; table_cap_ref cap = None; unique_table_caps (caps_of_state s); valid_objs s; obj_refs cap = obj_refs cap'; (a, b) \<noteq> p; obj_refs capa = obj_refs cap'; caps_of_state s (a, b) = Some capa; s \<turnstile> capa; (is_pt_cap cap \<longrightarrow> is_pt_cap capa) \<and> (is_pd_cap cap \<longrightarrow> is_pd_cap capa)\<rbrakk> \<Longrightarrow> table_cap_ref capa = table_cap_ref cap' proof (prove)
goal (5 subgoals):
 1. \<And>a b capa. \<lbrakk>is_pt_cap cap \<or> is_pd_cap cap; table_cap_ref cap = None; unique_table_caps (caps_of_state s); valid_objs s; obj_refs cap = obj_refs cap'; (a, b) \<noteq> p; obj_refs capa = obj_refs cap'; caps_of_state s (a, b) = Some capa; s \<turnstile> capa; (is_pt_cap cap \<longrightarrow> is_pt_cap capa) \<and> (is_pd_cap cap \<longrightarrow> is_pd_cap capa)\<rbrakk> \<Longrightarrow> obj_refs cap = obj_refs capa
 2. \<And>a b capa. \<lbrakk>is_pt_cap cap \<or> is_pd_cap cap; table_cap_ref cap = None; unique_table_caps (caps_of_state s); valid_objs s; obj_refs cap = obj_refs cap'; (a, b) \<noteq> p; obj_refs capa = obj_refs cap'; caps_of_state s (a, b) = Some capa; s \<turnstile> capa; (is_pt_cap cap \<longrightarrow> is_pt_cap capa) \<and> (is_pd_cap cap \<longrightarrow> is_pd_cap capa)\<rbrakk> \<Longrightarrow> cap_asid cap = None \<or> cap_asid capa = None
 3. \<And>a b capa. \<lbrakk>is_pt_cap cap \<or> is_pd_cap cap; table_cap_ref cap = None; unique_table_caps (caps_of_state s); valid_objs s; obj_refs cap = obj_refs cap'; (a, b) \<noteq> p; obj_refs capa = obj_refs cap'; caps_of_state s (a, b) = Some capa; s \<turnstile> capa; (is_pt_cap cap \<longrightarrow> is_pt_cap capa) \<and> (is_pd_cap cap \<longrightarrow> is_pd_cap capa)\<rbrakk> \<Longrightarrow> is_pd_cap cap \<and> is_pd_cap capa \<or> is_pt_cap cap \<and> is_pt_cap capa
 4. \<And>a b capa. \<lbrakk>is_pt_cap cap \<or> is_pd_cap cap; table_cap_ref cap = None; unique_table_caps (caps_of_state s); valid_objs s; obj_refs cap = obj_refs cap'; (a, b) \<noteq> p; obj_refs capa = obj_refs cap'; caps_of_state s (a, b) = Some capa; s \<turnstile> capa; (is_pt_cap cap \<longrightarrow> is_pt_cap capa) \<and> (is_pd_cap cap \<longrightarrow> is_pd_cap capa)\<rbrakk> \<Longrightarrow> unique_table_caps (caps_of_state s)
 5. \<And>a b capa. \<lbrakk>is_pt_cap cap \<or> is_pd_cap cap; table_cap_ref cap = None; unique_table_caps (caps_of_state s); valid_objs s; obj_refs cap = obj_refs cap'; (a, b) \<noteq> p; obj_refs capa = obj_refs cap'; caps_of_state s (a, b) = Some capa; s \<turnstile> capa; (is_pt_cap cap \<longrightarrow> is_pt_cap capa) \<and> (is_pd_cap cap \<longrightarrow> is_pd_cap capa); p = (a, b)\<rbrakk> \<Longrightarrow> table_cap_ref capa = table_cap_ref cap' proof (prove)
goal (4 subgoals):
 1. \<And>a b capa. \<lbrakk>is_pt_cap cap \<or> is_pd_cap cap; table_cap_ref cap = None; unique_table_caps (caps_of_state s); valid_objs s; obj_refs cap = obj_refs cap'; (a, b) \<noteq> p; obj_refs capa = obj_refs cap'; caps_of_state s (a, b) = Some capa; s \<turnstile> capa; (is_pt_cap cap \<longrightarrow> is_pt_cap capa) \<and> (is_pd_cap cap \<longrightarrow> is_pd_cap capa)\<rbrakk> \<Longrightarrow> cap_asid cap = None \<or> cap_asid capa = None
 2. \<And>a b capa. \<lbrakk>is_pt_cap cap \<or> is_pd_cap cap; table_cap_ref cap = None; unique_table_caps (caps_of_state s); valid_objs s; obj_refs cap = obj_refs cap'; (a, b) \<noteq> p; obj_refs capa = obj_refs cap'; caps_of_state s (a, b) = Some capa; s \<turnstile> capa; (is_pt_cap cap \<longrightarrow> is_pt_cap capa) \<and> (is_pd_cap cap \<longrightarrow> is_pd_cap capa)\<rbrakk> \<Longrightarrow> is_pd_cap cap \<and> is_pd_cap capa \<or> is_pt_cap cap \<and> is_pt_cap capa
 3. \<And>a b capa. \<lbrakk>is_pt_cap cap \<or> is_pd_cap cap; table_cap_ref cap = None; unique_table_caps (caps_of_state s); valid_objs s; obj_refs cap = obj_refs cap'; (a, b) \<noteq> p; obj_refs capa = obj_refs cap'; caps_of_state s (a, b) = Some capa; s \<turnstile> capa; (is_pt_cap cap \<longrightarrow> is_pt_cap capa) \<and> (is_pd_cap cap \<longrightarrow> is_pd_cap capa)\<rbrakk> \<Longrightarrow> unique_table_caps (caps_of_state s)
 4. \<And>a b capa. \<lbrakk>is_pt_cap cap \<or> is_pd_cap cap; table_cap_ref cap = None; unique_table_caps (caps_of_state s); valid_objs s; obj_refs cap = obj_refs cap'; (a, b) \<noteq> p; obj_refs capa = obj_refs cap'; caps_of_state s (a, b) = Some capa; s \<turnstile> capa; (is_pt_cap cap \<longrightarrow> is_pt_cap capa) \<and> (is_pd_cap cap \<longrightarrow> is_pd_cap capa); p = (a, b)\<rbrakk> \<Longrightarrow> table_cap_ref capa = table_cap_ref cap' proof (prove)
goal (3 subgoals):
 1. \<And>a b capa. \<lbrakk>is_pt_cap cap \<or> is_pd_cap cap; table_cap_ref cap = None; unique_table_caps (caps_of_state s); valid_objs s; obj_refs cap = obj_refs cap'; (a, b) \<noteq> p; obj_refs capa = obj_refs cap'; caps_of_state s (a, b) = Some capa; s \<turnstile> capa; (is_pt_cap cap \<longrightarrow> is_pt_cap capa) \<and> (is_pd_cap cap \<longrightarrow> is_pd_cap capa)\<rbrakk> \<Longrightarrow> is_pd_cap cap \<and> is_pd_cap capa \<or> is_pt_cap cap \<and> is_pt_cap capa
 2. \<And>a b capa. \<lbrakk>is_pt_cap cap \<or> is_pd_cap cap; table_cap_ref cap = None; unique_table_caps (caps_of_state s); valid_objs s; obj_refs cap = obj_refs cap'; (a, b) \<noteq> p; obj_refs capa = obj_refs cap'; caps_of_state s (a, b) = Some capa; s \<turnstile> capa; (is_pt_cap cap \<longrightarrow> is_pt_cap capa) \<and> (is_pd_cap cap \<longrightarrow> is_pd_cap capa)\<rbrakk> \<Longrightarrow> unique_table_caps (caps_of_state s)
 3. \<And>a b capa. \<lbrakk>is_pt_cap cap \<or> is_pd_cap cap; table_cap_ref cap = None; unique_table_caps (caps_of_state s); valid_objs s; obj_refs cap = obj_refs cap'; (a, b) \<noteq> p; obj_refs capa = obj_refs cap'; caps_of_state s (a, b) = Some capa; s \<turnstile> capa; (is_pt_cap cap \<longrightarrow> is_pt_cap capa) \<and> (is_pd_cap cap \<longrightarrow> is_pd_cap capa); p = (a, b)\<rbrakk> \<Longrightarrow> table_cap_ref capa = table_cap_ref cap' proof (prove)
goal (2 subgoals):
 1. \<And>a b capa. \<lbrakk>is_pt_cap cap \<or> is_pd_cap cap; table_cap_ref cap = None; unique_table_caps (caps_of_state s); valid_objs s; obj_refs cap = obj_refs cap'; (a, b) \<noteq> p; obj_refs capa = obj_refs cap'; caps_of_state s (a, b) = Some capa; s \<turnstile> capa; (is_pt_cap cap \<longrightarrow> is_pt_cap capa) \<and> (is_pd_cap cap \<longrightarrow> is_pd_cap capa)\<rbrakk> \<Longrightarrow> unique_table_caps (caps_of_state s)
 2. \<And>a b capa. \<lbrakk>is_pt_cap cap \<or> is_pd_cap cap; table_cap_ref cap = None; unique_table_caps (caps_of_state s); valid_objs s; obj_refs cap = obj_refs cap'; (a, b) \<noteq> p; obj_refs capa = obj_refs cap'; caps_of_state s (a, b) = Some capa; s \<turnstile> capa; (is_pt_cap cap \<longrightarrow> is_pt_cap capa) \<and> (is_pd_cap cap \<longrightarrow> is_pd_cap capa); p = (a, b)\<rbrakk> \<Longrightarrow> table_cap_ref capa = table_cap_ref cap' proof (prove)
goal (1 subgoal):
 1. \<And>a b capa. \<lbrakk>is_pt_cap cap \<or> is_pd_cap cap; table_cap_ref cap = None; unique_table_caps (caps_of_state s); valid_objs s; obj_refs cap = obj_refs cap'; (a, b) \<noteq> p; obj_refs capa = obj_refs cap'; caps_of_state s (a, b) = Some capa; s \<turnstile> capa; (is_pt_cap cap \<longrightarrow> is_pt_cap capa) \<and> (is_pd_cap cap \<longrightarrow> is_pd_cap capa); p = (a, b)\<rbrakk> \<Longrightarrow> table_cap_ref capa = table_cap_ref cap' proof (prove)
goal:
No subgoals!