theory PageTableDuplicates

lemma global_pd_offset:
  "\<lbrakk>is_aligned ptr pdBits ; x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + 2 ^ pdBits - 1}\<rbrakk>
  \<Longrightarrow> ptr  + (x && mask pdBits) = x" apply (rule mask_eqI[where n = pdBits]) apply (simp add:mask_add_aligned mask_twice pdBits_def pageBits_def) apply (subst mask_out_sub_mask) apply (simp add:mask_add_aligned mask_twice pdBits_def pageBits_def pdeBits_def) apply clarsimp apply (drule neg_mask_mono_le[where n = 14]) apply (drule neg_mask_mono_le[where n = 14]) apply (simp add:field_simps) apply (frule_tac d1 = "0x3FFF" and p1="ptr" in is_aligned_add_helper[THEN conjunct2]) apply simp apply (frule_tac d1 = "pptrBase >> 20 << 2" and p1 = "ptr"
    in is_aligned_add_helper[THEN conjunct2]) apply (simp add: pptrBase_def) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr pdBits; x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + 2 ^ pdBits - 1}\<rbrakk> \<Longrightarrow> ptr + (x && mask pdBits) = x proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr pdBits; x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + 2 ^ pdBits - 1}\<rbrakk> \<Longrightarrow> ptr + (x && mask pdBits) && mask pdBits = x && mask pdBits
 2. \<lbrakk>is_aligned ptr pdBits; x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + 2 ^ pdBits - 1}\<rbrakk> \<Longrightarrow> ptr + (x && mask pdBits) && ~~ mask pdBits = x && ~~ mask pdBits proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr pdBits; x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + 2 ^ pdBits - 1}\<rbrakk> \<Longrightarrow> ptr + (x && mask pdBits) && ~~ mask pdBits = x && ~~ mask pdBits proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr pdBits; x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + 2 ^ pdBits - 1}\<rbrakk> \<Longrightarrow> ptr + (x && mask pdBits) - (ptr + (x && mask pdBits) && mask pdBits) = x && ~~ mask pdBits proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 14; ptr + (pptrBase >> 20 << 2) \<le> x \<and> x \<le> 0x3FFF + ptr\<rbrakk> \<Longrightarrow> ptr = x && ~~ mask 14 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 14; ptr + (pptrBase >> 20 << 2) \<le> x; x \<le> 0x3FFF + ptr\<rbrakk> \<Longrightarrow> ptr = x && ~~ mask 14 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 14; x \<le> 0x3FFF + ptr; ptr + (pptrBase >> 20 << 2) && ~~ mask 14 \<le> x && ~~ mask 14\<rbrakk> \<Longrightarrow> ptr = x && ~~ mask 14 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 14; ptr + (pptrBase >> 20 << 2) && ~~ mask 14 \<le> x && ~~ mask 14; x && ~~ mask 14 \<le> 0x3FFF + ptr && ~~ mask 14\<rbrakk> \<Longrightarrow> ptr = x && ~~ mask 14 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 14; ptr + (pptrBase >> 20 << 2) && ~~ mask 14 \<le> x && ~~ mask 14; x && ~~ mask 14 \<le> ptr + 0x3FFF && ~~ mask 14\<rbrakk> \<Longrightarrow> ptr = x && ~~ mask 14 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr 14; ptr + (pptrBase >> 20 << 2) && ~~ mask 14 \<le> x && ~~ mask 14; x && ~~ mask 14 \<le> ptr + 0x3FFF && ~~ mask 14\<rbrakk> \<Longrightarrow> 0x3FFF < 2 ^ 14
 2. \<lbrakk>is_aligned ptr 14; ptr + (pptrBase >> 20 << 2) && ~~ mask 14 \<le> x && ~~ mask 14; x && ~~ mask 14 \<le> ptr + 0x3FFF && ~~ mask 14; ptr + 0x3FFF && ~~ mask 14 = ptr\<rbrakk> \<Longrightarrow> ptr = x && ~~ mask 14 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 14; ptr + (pptrBase >> 20 << 2) && ~~ mask 14 \<le> x && ~~ mask 14; x && ~~ mask 14 \<le> ptr + 0x3FFF && ~~ mask 14; ptr + 0x3FFF && ~~ mask 14 = ptr\<rbrakk> \<Longrightarrow> ptr = x && ~~ mask 14 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr 14; ptr + (pptrBase >> 20 << 2) && ~~ mask 14 \<le> x && ~~ mask 14; x && ~~ mask 14 \<le> ptr + 0x3FFF && ~~ mask 14; ptr + 0x3FFF && ~~ mask 14 = ptr\<rbrakk> \<Longrightarrow> pptrBase >> 20 << 2 < 2 ^ 14
 2. \<lbrakk>is_aligned ptr 14; ptr + (pptrBase >> 20 << 2) && ~~ mask 14 \<le> x && ~~ mask 14; x && ~~ mask 14 \<le> ptr + 0x3FFF && ~~ mask 14; ptr + 0x3FFF && ~~ mask 14 = ptr; ptr + (pptrBase >> 20 << 2) && ~~ mask 14 = ptr\<rbrakk> \<Longrightarrow> ptr = x && ~~ mask 14 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 14; ptr + (pptrBase >> 20 << 2) && ~~ mask 14 \<le> x && ~~ mask 14; x && ~~ mask 14 \<le> ptr + 0x3FFF && ~~ mask 14; ptr + 0x3FFF && ~~ mask 14 = ptr; ptr + (pptrBase >> 20 << 2) && ~~ mask 14 = ptr\<rbrakk> \<Longrightarrow> ptr = x && ~~ mask 14 proof (prove)
goal:
No subgoals!