theory Untyped_R

lemma capRange_subset_capBits:
  "capAligned cap \<Longrightarrow> capAligned cap'
    \<Longrightarrow> capRange cap \<subseteq> capRange cap'
    \<Longrightarrow> capRange cap \<noteq> {}
    \<Longrightarrow> capBits cap \<le> capBits cap'" supply
    is_aligned_neg_mask_eq[simp del]
    is_aligned_neg_mask_weaken[simp del] apply (simp add: capRange_def capAligned_def is_aligned_no_overflow
            split: if_split_asm del: atLeastatMost_subset_iff) apply (frule_tac c="capUntypedPtr cap" in subsetD) apply (simp only: mask_in_range[symmetric]) apply (simp add: is_aligned_neg_mask_eq) apply (drule_tac c="(capUntypedPtr cap && ~~ mask (capBits cap))
        || (~~ capUntypedPtr cap' && mask (capBits cap))" in subsetD) apply (simp_all only: mask_in_range[symmetric]) apply (simp add: word_ao_dist is_aligned_neg_mask_eq) apply (simp add: word_ao_dist) apply (cases "capBits cap = 0") apply simp apply (drule_tac f="\<lambda>x. x !! (capBits cap - 1)"
        and x="a || b" for a b in arg_cong) apply (simp add: word_ops_nth_size word_bits_def word_size) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>capAligned cap; capAligned cap'; capRange cap \<subseteq> capRange cap'; capRange cap \<noteq> {}\<rbrakk> \<Longrightarrow> capBits cap \<le> capBits cap' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>capAligned cap; capAligned cap'; capRange cap \<subseteq> capRange cap'; capRange cap \<noteq> {}\<rbrakk> \<Longrightarrow> capBits cap \<le> capBits cap' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned (global.capUntypedPtr cap) (capBits cap); capBits cap < word_bits; is_aligned (global.capUntypedPtr cap') (capBits cap'); capBits cap' < word_bits; capClass cap' = PhysicalClass; {global.capUntypedPtr cap..global.capUntypedPtr cap + 2 ^ capBits cap - 1} \<subseteq> {global.capUntypedPtr cap'..global.capUntypedPtr cap' + 2 ^ capBits cap' - 1}; capClass cap = PhysicalClass\<rbrakk> \<Longrightarrow> capBits cap \<le> capBits cap' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned (global.capUntypedPtr cap) (capBits cap); capBits cap < word_bits; is_aligned (global.capUntypedPtr cap') (capBits cap'); capBits cap' < word_bits; capClass cap' = PhysicalClass; {global.capUntypedPtr cap..global.capUntypedPtr cap + 2 ^ capBits cap - 1} \<subseteq> {global.capUntypedPtr cap'..global.capUntypedPtr cap' + 2 ^ capBits cap' - 1}; capClass cap = PhysicalClass\<rbrakk> \<Longrightarrow> global.capUntypedPtr cap \<in> {global.capUntypedPtr cap..global.capUntypedPtr cap + 2 ^ capBits cap - 1}
 2. \<lbrakk>is_aligned (global.capUntypedPtr cap) (capBits cap); capBits cap < word_bits; is_aligned (global.capUntypedPtr cap') (capBits cap'); capBits cap' < word_bits; capClass cap' = PhysicalClass; {global.capUntypedPtr cap..global.capUntypedPtr cap + 2 ^ capBits cap - 1} \<subseteq> {global.capUntypedPtr cap'..global.capUntypedPtr cap' + 2 ^ capBits cap' - 1}; capClass cap = PhysicalClass; global.capUntypedPtr cap \<in> {global.capUntypedPtr cap'..global.capUntypedPtr cap' + 2 ^ capBits cap' - 1}\<rbrakk> \<Longrightarrow> capBits cap \<le> capBits cap' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned (global.capUntypedPtr cap) (capBits cap); capBits cap < word_bits; is_aligned (global.capUntypedPtr cap') (capBits cap'); capBits cap' < word_bits; capClass cap' = PhysicalClass; {global.capUntypedPtr cap..global.capUntypedPtr cap + 2 ^ capBits cap - 1} \<subseteq> {global.capUntypedPtr cap'..global.capUntypedPtr cap' + 2 ^ capBits cap' - 1}; capClass cap = PhysicalClass\<rbrakk> \<Longrightarrow> global.capUntypedPtr cap && ~~ mask (capBits cap) = global.capUntypedPtr cap
 2. \<lbrakk>is_aligned (global.capUntypedPtr cap) (capBits cap); capBits cap < word_bits; is_aligned (global.capUntypedPtr cap') (capBits cap'); capBits cap' < word_bits; capClass cap' = PhysicalClass; {global.capUntypedPtr cap..global.capUntypedPtr cap + 2 ^ capBits cap - 1} \<subseteq> {global.capUntypedPtr cap'..global.capUntypedPtr cap' + 2 ^ capBits cap' - 1}; capClass cap = PhysicalClass; global.capUntypedPtr cap \<in> {global.capUntypedPtr cap'..global.capUntypedPtr cap' + 2 ^ capBits cap' - 1}\<rbrakk> \<Longrightarrow> capBits cap \<le> capBits cap' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned (global.capUntypedPtr cap) (capBits cap); capBits cap < word_bits; is_aligned (global.capUntypedPtr cap') (capBits cap'); capBits cap' < word_bits; capClass cap' = PhysicalClass; {global.capUntypedPtr cap..global.capUntypedPtr cap + 2 ^ capBits cap - 1} \<subseteq> {global.capUntypedPtr cap'..global.capUntypedPtr cap' + 2 ^ capBits cap' - 1}; capClass cap = PhysicalClass; global.capUntypedPtr cap \<in> {global.capUntypedPtr cap'..global.capUntypedPtr cap' + 2 ^ capBits cap' - 1}\<rbrakk> \<Longrightarrow> capBits cap \<le> capBits cap' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned (global.capUntypedPtr cap) (capBits cap); capBits cap < word_bits; is_aligned (global.capUntypedPtr cap') (capBits cap'); capBits cap' < word_bits; capClass cap' = PhysicalClass; capClass cap = PhysicalClass; global.capUntypedPtr cap \<in> {global.capUntypedPtr cap'..global.capUntypedPtr cap' + 2 ^ capBits cap' - 1}\<rbrakk> \<Longrightarrow> global.capUntypedPtr cap && ~~ mask (capBits cap) || ~~ global.capUntypedPtr cap' && mask (capBits cap) \<in> {global.capUntypedPtr cap..global.capUntypedPtr cap + 2 ^ capBits cap - 1}
 2. \<lbrakk>is_aligned (global.capUntypedPtr cap) (capBits cap); capBits cap < word_bits; is_aligned (global.capUntypedPtr cap') (capBits cap'); capBits cap' < word_bits; capClass cap' = PhysicalClass; capClass cap = PhysicalClass; global.capUntypedPtr cap \<in> {global.capUntypedPtr cap'..global.capUntypedPtr cap' + 2 ^ capBits cap' - 1}; global.capUntypedPtr cap && ~~ mask (capBits cap) || ~~ global.capUntypedPtr cap' && mask (capBits cap) \<in> {global.capUntypedPtr cap'..global.capUntypedPtr cap' + 2 ^ capBits cap' - 1}\<rbrakk> \<Longrightarrow> capBits cap \<le> capBits cap' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned (global.capUntypedPtr cap) (capBits cap); capBits cap < word_bits; is_aligned (global.capUntypedPtr cap') (capBits cap'); capBits cap' < word_bits; capClass cap' = PhysicalClass; capClass cap = PhysicalClass; global.capUntypedPtr cap && ~~ mask (capBits cap') = global.capUntypedPtr cap'\<rbrakk> \<Longrightarrow> (global.capUntypedPtr cap && ~~ mask (capBits cap) || ~~ global.capUntypedPtr cap' && mask (capBits cap)) && ~~ mask (capBits cap) = global.capUntypedPtr cap
 2. \<lbrakk>is_aligned (global.capUntypedPtr cap) (capBits cap); capBits cap < word_bits; is_aligned (global.capUntypedPtr cap') (capBits cap'); capBits cap' < word_bits; capClass cap' = PhysicalClass; capClass cap = PhysicalClass; global.capUntypedPtr cap && ~~ mask (capBits cap') = global.capUntypedPtr cap'; (global.capUntypedPtr cap && ~~ mask (capBits cap) || ~~ global.capUntypedPtr cap' && mask (capBits cap)) && ~~ mask (capBits cap') = global.capUntypedPtr cap'\<rbrakk> \<Longrightarrow> capBits cap \<le> capBits cap' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned (global.capUntypedPtr cap) (capBits cap); capBits cap < word_bits; is_aligned (global.capUntypedPtr cap') (capBits cap'); capBits cap' < word_bits; capClass cap' = PhysicalClass; capClass cap = PhysicalClass; global.capUntypedPtr cap && ~~ mask (capBits cap') = global.capUntypedPtr cap'; (global.capUntypedPtr cap && ~~ mask (capBits cap) || ~~ global.capUntypedPtr cap' && mask (capBits cap)) && ~~ mask (capBits cap') = global.capUntypedPtr cap'\<rbrakk> \<Longrightarrow> capBits cap \<le> capBits cap' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned (global.capUntypedPtr cap) (capBits cap); capBits cap < word_bits; is_aligned (global.capUntypedPtr cap') (capBits cap'); capBits cap' < word_bits; capClass cap' = PhysicalClass; capClass cap = PhysicalClass; global.capUntypedPtr cap && ~~ mask (capBits cap') = global.capUntypedPtr cap'; (global.capUntypedPtr cap && ~~ mask (capBits cap)) && ~~ mask (capBits cap') || (~~ global.capUntypedPtr cap' && mask (capBits cap)) && ~~ mask (capBits cap') = global.capUntypedPtr cap'\<rbrakk> \<Longrightarrow> capBits cap \<le> capBits cap' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned (global.capUntypedPtr cap) (capBits cap); capBits cap < word_bits; is_aligned (global.capUntypedPtr cap') (capBits cap'); capBits cap' < word_bits; capClass cap' = PhysicalClass; capClass cap = PhysicalClass; global.capUntypedPtr cap && ~~ mask (capBits cap') = global.capUntypedPtr cap'; (global.capUntypedPtr cap && ~~ mask (capBits cap)) && ~~ mask (capBits cap') || (~~ global.capUntypedPtr cap' && mask (capBits cap)) && ~~ mask (capBits cap') = global.capUntypedPtr cap'; capBits cap = 0\<rbrakk> \<Longrightarrow> capBits cap \<le> capBits cap'
 2. \<lbrakk>is_aligned (global.capUntypedPtr cap) (capBits cap); capBits cap < word_bits; is_aligned (global.capUntypedPtr cap') (capBits cap'); capBits cap' < word_bits; capClass cap' = PhysicalClass; capClass cap = PhysicalClass; global.capUntypedPtr cap && ~~ mask (capBits cap') = global.capUntypedPtr cap'; (global.capUntypedPtr cap && ~~ mask (capBits cap)) && ~~ mask (capBits cap') || (~~ global.capUntypedPtr cap' && mask (capBits cap)) && ~~ mask (capBits cap') = global.capUntypedPtr cap'; capBits cap \<noteq> 0\<rbrakk> \<Longrightarrow> capBits cap \<le> capBits cap' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned (global.capUntypedPtr cap) (capBits cap); capBits cap < word_bits; is_aligned (global.capUntypedPtr cap') (capBits cap'); capBits cap' < word_bits; capClass cap' = PhysicalClass; capClass cap = PhysicalClass; global.capUntypedPtr cap && ~~ mask (capBits cap') = global.capUntypedPtr cap'; (global.capUntypedPtr cap && ~~ mask (capBits cap)) && ~~ mask (capBits cap') || (~~ global.capUntypedPtr cap' && mask (capBits cap)) && ~~ mask (capBits cap') = global.capUntypedPtr cap'; capBits cap \<noteq> 0\<rbrakk> \<Longrightarrow> capBits cap \<le> capBits cap' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned (global.capUntypedPtr cap) (capBits cap); capBits cap < word_bits; is_aligned (global.capUntypedPtr cap') (capBits cap'); capBits cap' < word_bits; capClass cap' = PhysicalClass; capClass cap = PhysicalClass; global.capUntypedPtr cap && ~~ mask (capBits cap') = global.capUntypedPtr cap'; capBits cap \<noteq> 0; ((global.capUntypedPtr cap && ~~ mask (capBits cap)) && ~~ mask (capBits cap') || (~~ global.capUntypedPtr cap' && mask (capBits cap)) && ~~ mask (capBits cap')) !! (capBits cap - 1) = global.capUntypedPtr cap' !! (capBits cap - 1)\<rbrakk> \<Longrightarrow> capBits cap \<le> capBits cap' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned (global.capUntypedPtr cap) (capBits cap); capBits cap < 32; is_aligned (global.capUntypedPtr cap') (capBits cap'); capBits cap' < 32; capClass cap' = PhysicalClass; capClass cap = PhysicalClass; global.capUntypedPtr cap && ~~ mask (capBits cap') = global.capUntypedPtr cap'; 0 < capBits cap; (capBits cap - Suc 0 < 32 \<and> \<not> global.capUntypedPtr cap' !! (capBits cap - Suc 0) \<and> capBits cap - Suc 0 < 32 \<and> \<not> capBits cap - Suc 0 < capBits cap') = global.capUntypedPtr cap' !! (capBits cap - Suc 0)\<rbrakk> \<Longrightarrow> capBits cap \<le> capBits cap' proof (prove)
goal:
No subgoals!