theory ArchArch_IF

lemma cte_wp_parent_not_global_pd:
  "\<lbrakk> valid_global_refs s; cte_wp_at (parent_for_refs (Inr (a,b))) k s \<rbrakk>
     \<Longrightarrow> \<forall>x \<in> set b. x && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s)" apply (simp only: cte_wp_at_caps_of_state) apply (elim exE conjE) apply (drule valid_global_refsD2,simp) apply (unfold parent_for_refs_def) apply (simp add: image_def global_refs_def cap_range_def) apply clarsimp apply (subgoal_tac "arm_global_pd (arch_state s) \<in> set b") apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_global_refs s; cte_wp_at (parent_for_refs (Inr (a, b))) k s\<rbrakk> \<Longrightarrow> \<forall>x\<in>set b. x && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_global_refs s; \<exists>cap. caps_of_state s k = Some cap \<and> parent_for_refs (Inr (a, b)) cap\<rbrakk> \<Longrightarrow> \<forall>x\<in>set b. x && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) proof (prove)
goal (1 subgoal):
 1. \<And>cap. \<lbrakk>valid_global_refs s; caps_of_state s k = Some cap; parent_for_refs (Inr (a, b)) cap\<rbrakk> \<Longrightarrow> \<forall>x\<in>set b. x && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) proof (prove)
goal (1 subgoal):
 1. \<And>cap. \<lbrakk>valid_global_refs s; parent_for_refs (Inr (a, b)) cap; global_refs s \<inter> cap_range cap = {}\<rbrakk> \<Longrightarrow> \<forall>x\<in>set b. x && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) proof (prove)
goal (1 subgoal):
 1. \<And>cap. \<lbrakk>valid_global_refs s; case Inr (a, b) of Inl (xa, slots) \<Rightarrow> (\<lambda>x. x && ~~ mask pt_bits) ` set slots \<subseteq> obj_refs cap \<and> is_pt_cap cap \<and> cap_asid cap \<noteq> None | Inr (xa, slots) \<Rightarrow> (\<lambda>x. x && ~~ mask pd_bits) ` set slots \<subseteq> obj_refs cap \<and> is_pd_cap cap \<and> cap_asid cap \<noteq> None; global_refs s \<inter> cap_range cap = {}\<rbrakk> \<Longrightarrow> \<forall>x\<in>set b. x && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) proof (prove)
goal (1 subgoal):
 1. \<And>cap. \<lbrakk>valid_global_refs s; {y. \<exists>x\<in>set b. y = x && ~~ mask pd_bits} \<subseteq> obj_refs cap \<and> is_pd_cap cap \<and> (\<exists>y. cap_asid cap = Some y); idle_thread s \<notin> untyped_range cap \<and> idle_thread s \<notin> obj_refs cap \<and> arm_global_pd (arch_state s) \<notin> untyped_range cap \<and> arm_global_pd (arch_state s) \<notin> obj_refs cap \<and> ({y. \<exists>x. y = interrupt_irq_node s x} \<union> set (arm_global_pts (arch_state s))) \<inter> (untyped_range cap \<union> obj_refs cap) = {}\<rbrakk> \<Longrightarrow> \<forall>x\<in>set b. x && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s) proof (prove)
goal (1 subgoal):
 1. \<And>cap x y. \<lbrakk>valid_global_refs s; x \<in> set b; {y. \<exists>x\<in>set b. y = x && ~~ mask pd_bits} \<subseteq> obj_refs cap; idle_thread s \<notin> untyped_range cap; is_pd_cap cap; cap_asid cap = Some y; idle_thread s \<notin> obj_refs cap; arm_global_pd (arch_state s) \<notin> untyped_range cap; arm_global_pd (arch_state s) \<notin> obj_refs cap; ({y. \<exists>x. y = interrupt_irq_node s x} \<union> set (arm_global_pts (arch_state s))) \<inter> (untyped_range cap \<union> obj_refs cap) = {}; x && ~~ mask pd_bits = arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>cap x y. \<lbrakk>valid_global_refs s; x \<in> set b; {y. \<exists>x\<in>set b. y = x && ~~ mask pd_bits} \<subseteq> obj_refs cap; idle_thread s \<notin> untyped_range cap; is_pd_cap cap; cap_asid cap = Some y; idle_thread s \<notin> obj_refs cap; arm_global_pd (arch_state s) \<notin> untyped_range cap; arm_global_pd (arch_state s) \<notin> obj_refs cap; ({y. \<exists>x. y = interrupt_irq_node s x} \<union> set (arm_global_pts (arch_state s))) \<inter> (untyped_range cap \<union> obj_refs cap) = {}; x && ~~ mask pd_bits = arm_global_pd (arch_state s); arm_global_pd (arch_state s) \<in> set b\<rbrakk> \<Longrightarrow> False
 2. \<And>cap x y. \<lbrakk>valid_global_refs s; x \<in> set b; {y. \<exists>x\<in>set b. y = x && ~~ mask pd_bits} \<subseteq> obj_refs cap; idle_thread s \<notin> untyped_range cap; is_pd_cap cap; cap_asid cap = Some y; idle_thread s \<notin> obj_refs cap; arm_global_pd (arch_state s) \<notin> untyped_range cap; arm_global_pd (arch_state s) \<notin> obj_refs cap; ({y. \<exists>x. y = interrupt_irq_node s x} \<union> set (arm_global_pts (arch_state s))) \<inter> (untyped_range cap \<union> obj_refs cap) = {}; x && ~~ mask pd_bits = arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> arm_global_pd (arch_state s) \<in> set b proof (prove)
goal:
No subgoals!