theory PageTableDuplicates

lemma page_directory_at_pde_atD':
  "\<lbrakk>page_directory_at' p s;is_aligned p' 2; p' && ~~ mask pdBits = p\<rbrakk> \<Longrightarrow> pde_at' p' s" apply (clarsimp simp:page_directory_at'_def) apply (drule_tac x = "p' && mask pdBits >> 2" in spec) apply (erule impE) apply (rule shiftr_less_t2n[where m = 12,simplified]) apply (rule le_less_trans[OF word_and_le1]) apply (simp add:pdBits_def mask_def pageBits_def pdeBits_def) apply (subst (asm) shiftr_shiftl1) apply simp apply simp apply (subst (asm) is_aligned_neg_mask_eq[where n = 2]) apply (simp add: is_aligned_andI1) apply (simp add:mask_out_sub_mask) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>page_directory_at' p s; is_aligned p' 2; p' && ~~ mask pdBits = p\<rbrakk> \<Longrightarrow> pde_at' p' s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p' 2; p = p' && ~~ mask pdBits; \<forall>y<0x1000. pde_at' ((p' && ~~ mask pdBits) + (y << 2)) s\<rbrakk> \<Longrightarrow> pde_at' p' s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p' 2; p = p' && ~~ mask pdBits; p' && mask pdBits >> 2 < 0x1000 \<longrightarrow> pde_at' ((p' && ~~ mask pdBits) + (p' && mask pdBits >> 2 << 2)) s\<rbrakk> \<Longrightarrow> pde_at' p' s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned p' 2; p = p' && ~~ mask pdBits\<rbrakk> \<Longrightarrow> p' && mask pdBits >> 2 < 0x1000
 2. \<lbrakk>is_aligned p' 2; p = p' && ~~ mask pdBits; pde_at' ((p' && ~~ mask pdBits) + (p' && mask pdBits >> 2 << 2)) s\<rbrakk> \<Longrightarrow> pde_at' p' s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned p' 2; p = p' && ~~ mask pdBits\<rbrakk> \<Longrightarrow> p' && mask pdBits < 2 ^ (2 + 12)
 2. \<lbrakk>is_aligned p' 2; p = p' && ~~ mask pdBits; pde_at' ((p' && ~~ mask pdBits) + (p' && mask pdBits >> 2 << 2)) s\<rbrakk> \<Longrightarrow> pde_at' p' s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned p' 2; p = p' && ~~ mask pdBits\<rbrakk> \<Longrightarrow> mask pdBits < 2 ^ (2 + 12)
 2. \<lbrakk>is_aligned p' 2; p = p' && ~~ mask pdBits; pde_at' ((p' && ~~ mask pdBits) + (p' && mask pdBits >> 2 << 2)) s\<rbrakk> \<Longrightarrow> pde_at' p' s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p' 2; p = p' && ~~ mask pdBits; pde_at' ((p' && ~~ mask pdBits) + (p' && mask pdBits >> 2 << 2)) s\<rbrakk> \<Longrightarrow> pde_at' p' s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned p' 2; p = p' && ~~ mask pdBits\<rbrakk> \<Longrightarrow> 2 \<le> 2
 2. \<lbrakk>is_aligned p' 2; p = p' && ~~ mask pdBits; pde_at' ((p' && ~~ mask pdBits) + ((p' && mask pdBits >> 2 - 2) && ~~ mask 2)) s\<rbrakk> \<Longrightarrow> pde_at' p' s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p' 2; p = p' && ~~ mask pdBits; pde_at' ((p' && ~~ mask pdBits) + ((p' && mask pdBits >> 2 - 2) && ~~ mask 2)) s\<rbrakk> \<Longrightarrow> pde_at' p' s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p' 2; p = p' && ~~ mask pdBits; pde_at' ((p' && ~~ mask pdBits) + ((p' && mask pdBits) && ~~ mask 2)) s\<rbrakk> \<Longrightarrow> pde_at' p' s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned p' 2; p = p' && ~~ mask pdBits\<rbrakk> \<Longrightarrow> is_aligned (p' && mask pdBits) 2
 2. \<lbrakk>is_aligned p' 2; p = p' && ~~ mask pdBits; pde_at' ((p' && ~~ mask pdBits) + (p' && mask pdBits)) s\<rbrakk> \<Longrightarrow> pde_at' p' s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p' 2; p = p' && ~~ mask pdBits; pde_at' ((p' && ~~ mask pdBits) + (p' && mask pdBits)) s\<rbrakk> \<Longrightarrow> pde_at' p' s proof (prove)
goal:
No subgoals!