theory ArchArch_IF

lemma cte_wp_at_pt_exists_cap:
  "\<lbrakk> valid_objs s; cte_wp_at ((=) (ArchObjectCap (PageTableCap word option))) slot s;
     x \<in> set [word , word + 4 .e. word + 2 ^ pt_bits - 1] \<rbrakk>
     \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and>
                   x && ~~ mask pt_bits \<in> obj_refs cap \<and> is_pt_cap cap" apply (case_tac slot) apply (rule_tac x=a in exI) apply (rule_tac x=b in exI) apply (subgoal_tac "is_aligned word pt_bits") apply (frule (1) word_aligned_pt_slots) apply (simp add:pageBits_def cte_wp_at_caps_of_state is_pt_cap_def) apply (frule (1) cte_wp_valid_cap) apply (simp add: valid_cap_def cap_aligned_def pt_bits_def pageBits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs s; cte_wp_at ((=) (ArchObjectCap (PageTableCap word option))) slot s; x \<in> set [word , word + 4 .e. word + 2 ^ pt_bits - 1]\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> x && ~~ mask pt_bits \<in> obj_refs cap \<and> is_pt_cap cap proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>valid_objs s; cte_wp_at ((=) (ArchObjectCap (PageTableCap word option))) slot s; x \<in> set [word , word + 4 .e. word + 2 ^ pt_bits - 1]; slot = (a, b)\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> x && ~~ mask pt_bits \<in> obj_refs cap \<and> is_pt_cap cap proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>valid_objs s; cte_wp_at ((=) (ArchObjectCap (PageTableCap word option))) slot s; x \<in> set [word , word + 4 .e. word + 2 ^ pt_bits - 1]; slot = (a, b)\<rbrakk> \<Longrightarrow> \<exists>b cap. caps_of_state s (a, b) = Some cap \<and> x && ~~ mask pt_bits \<in> obj_refs cap \<and> is_pt_cap cap proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>valid_objs s; cte_wp_at ((=) (ArchObjectCap (PageTableCap word option))) slot s; x \<in> set [word , word + 4 .e. word + 2 ^ pt_bits - 1]; slot = (a, b)\<rbrakk> \<Longrightarrow> \<exists>cap. caps_of_state s (a, b) = Some cap \<and> x && ~~ mask pt_bits \<in> obj_refs cap \<and> is_pt_cap cap proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>valid_objs s; cte_wp_at ((=) (ArchObjectCap (PageTableCap word option))) slot s; x \<in> set [word , word + 4 .e. word + 2 ^ pt_bits - 1]; slot = (a, b); is_aligned word pt_bits\<rbrakk> \<Longrightarrow> \<exists>cap. caps_of_state s (a, b) = Some cap \<and> x && ~~ mask pt_bits \<in> obj_refs cap \<and> is_pt_cap cap
 2. \<And>a b. \<lbrakk>valid_objs s; cte_wp_at ((=) (ArchObjectCap (PageTableCap word option))) slot s; x \<in> set [word , word + 4 .e. word + 2 ^ pt_bits - 1]; slot = (a, b)\<rbrakk> \<Longrightarrow> is_aligned word pt_bits proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>valid_objs s; cte_wp_at ((=) (ArchObjectCap (PageTableCap word option))) slot s; x \<in> set [word , word + 4 .e. word + 2 ^ pt_bits - 1]; slot = (a, b); is_aligned word pt_bits; x && ~~ mask pt_bits = word\<rbrakk> \<Longrightarrow> \<exists>cap. caps_of_state s (a, b) = Some cap \<and> x && ~~ mask pt_bits \<in> obj_refs cap \<and> is_pt_cap cap
 2. \<And>a b. \<lbrakk>valid_objs s; cte_wp_at ((=) (ArchObjectCap (PageTableCap word option))) slot s; x \<in> set [word , word + 4 .e. word + 2 ^ pt_bits - 1]; slot = (a, b)\<rbrakk> \<Longrightarrow> is_aligned word pt_bits proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>valid_objs s; cte_wp_at ((=) (ArchObjectCap (PageTableCap word option))) slot s; x \<in> set [word , word + 4 .e. word + 2 ^ pt_bits - 1]; slot = (a, b)\<rbrakk> \<Longrightarrow> is_aligned word pt_bits proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>valid_objs s; cte_wp_at ((=) (ArchObjectCap (PageTableCap word option))) slot s; x \<in> set [word , word + 4 .e. word + 2 ^ pt_bits - 1]; slot = (a, b); s \<turnstile> ArchObjectCap (PageTableCap word option)\<rbrakk> \<Longrightarrow> is_aligned word pt_bits proof (prove)
goal:
No subgoals!