theory Finalise_DR

lemma page_table_address_eq:
  fixes ptr :: word32
  shows
  "\<lbrakk>is_aligned ptr 6; t \<in> set [0 , 4 .e. 0x3C]\<rbrakk> \<Longrightarrow> ptr && ~~ mask pt_bits = ptr + t && ~~ mask pt_bits" apply (drule large_frame_range_helper) using mask_lower_twice[where m = 10 and n = 6 and x= ptr,symmetric] apply (clarsimp simp:pt_bits_def pageBits_def) using mask_lower_twice[where m = 10 and n = 6 and x= "ptr+t",symmetric] apply (clarsimp simp:pt_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 pt_bits = ptr + t && ~~ mask pt_bits proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 6; t < 0x40\<rbrakk> \<Longrightarrow> ptr && ~~ mask pt_bits = ptr + t && ~~ mask pt_bits proof (prove)
using this:
6 \<le> 10 \<Longrightarrow> ptr && ~~ mask 10 = (ptr && ~~ mask 6) && ~~ mask 10

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

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