theory Finalise_DR

lemma page_directory_address_eq:
  fixes ptr :: word32
  shows
  "\<lbrakk>is_aligned ptr 6; t \<in> set [0 , 4 .e. 0x3C]\<rbrakk> \<Longrightarrow> ptr && ~~ mask pd_bits = ptr + t && ~~ mask pd_bits" apply (drule large_frame_range_helper) using mask_lower_twice[where m = 14 and n = 6 and x= ptr,symmetric] apply (clarsimp simp:pd_bits_def pageBits_def) using mask_lower_twice[where m = 14 and n = 6 and x= "ptr+t",symmetric] apply (clarsimp simp:pd_bits_def pageBits_def) apply (subgoal_tac "(ptr && ~~ mask 6)  = (ptr + t && ~~ mask 6)") apply simp apply (frule is_aligned_neg_mask_eq) apply simp apply (drule_tac q = t in mask_out_add_aligned) apply (subst(asm) less_mask_eq [THEN mask_eq_x_eq_0[THEN iffD1]], erule order_less_le_trans) apply clarsimp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 6; t \<in> set [0 , 4 .e. 0x3C]\<rbrakk> \<Longrightarrow> ptr && ~~ mask pd_bits = ptr + t && ~~ mask pd_bits proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 6; t < 0x40\<rbrakk> \<Longrightarrow> ptr && ~~ mask pd_bits = ptr + t && ~~ mask pd_bits proof (prove)
using this:
6 \<le> 14 \<Longrightarrow> ptr && ~~ mask 14 = (ptr && ~~ mask 6) && ~~ mask 14

goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 6; t < 0x40\<rbrakk> \<Longrightarrow> ptr && ~~ mask pd_bits = ptr + t && ~~ mask pd_bits proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 6; t < 0x40\<rbrakk> \<Longrightarrow> ptr && ~~ mask 14 = ptr + t && ~~ mask 14 proof (prove)
using this:
6 \<le> 14 \<Longrightarrow> ptr + t && ~~ mask 14 = (ptr + t && ~~ mask 6) && ~~ mask 14

goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 6; t < 0x40\<rbrakk> \<Longrightarrow> ptr && ~~ mask 14 = ptr + t && ~~ mask 14 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 6; t < 0x40; ptr + t && ~~ mask 14 = (ptr + t && ~~ mask 6) && ~~ mask 14\<rbrakk> \<Longrightarrow> ptr && ~~ mask 14 = (ptr + t && ~~ mask 6) && ~~ mask 14 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr 6; t < 0x40; ptr + t && ~~ mask 14 = (ptr + t && ~~ mask 6) && ~~ mask 14; ptr && ~~ mask 6 = ptr + t && ~~ mask 6\<rbrakk> \<Longrightarrow> ptr && ~~ mask 14 = (ptr + t && ~~ mask 6) && ~~ mask 14
 2. \<lbrakk>is_aligned ptr 6; t < 0x40; ptr + t && ~~ mask 14 = (ptr + t && ~~ mask 6) && ~~ mask 14\<rbrakk> \<Longrightarrow> ptr && ~~ mask 6 = ptr + t && ~~ mask 6 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 6; t < 0x40; ptr + t && ~~ mask 14 = (ptr + t && ~~ mask 6) && ~~ mask 14\<rbrakk> \<Longrightarrow> ptr && ~~ mask 6 = ptr + t && ~~ mask 6 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 6; t < 0x40; ptr + t && ~~ mask 14 = (ptr + t && ~~ mask 6) && ~~ mask 14; ptr && ~~ mask 6 = ptr\<rbrakk> \<Longrightarrow> ptr && ~~ mask 6 = ptr + t && ~~ mask 6 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 6; t < 0x40; ptr + t && ~~ mask 14 = (ptr + t && ~~ mask 6) && ~~ mask 14\<rbrakk> \<Longrightarrow> ptr = ptr + t && ~~ mask 6 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t < 0x40; ptr + t && ~~ mask 14 = (ptr + t && ~~ mask 6) && ~~ mask 14; ptr + (t && ~~ mask 6) = ptr + t && ~~ mask 6\<rbrakk> \<Longrightarrow> ptr = ptr + t && ~~ mask 6 proof (prove)
goal (2 subgoals):
 1. ptr + t && ~~ mask 14 = (ptr + t && ~~ mask 6) && ~~ mask 14 \<Longrightarrow> 0x40 \<le> 2 ^ 6
 2. \<lbrakk>t < 0x40; ptr + t && ~~ mask 14 = (ptr + t && ~~ mask 6) && ~~ mask 14; ptr + 0 = ptr + t && ~~ mask 6\<rbrakk> \<Longrightarrow> ptr = ptr + t && ~~ mask 6 proof (prove)
goal:
No subgoals!