theory Arch_C

lemma flush_range_le:
  assumes assms:"page_base start a = page_base end a"
        "start \<le> end" "w && mask (pageBitsForSize a) = start && mask (pageBitsForSize a)"
  shows "w \<le> w + (end - start)" "unat (end - start) \<le> 2 ^ pageBitsForSize a" proof - have q: "w && mask (pageBitsForSize a) \<le> (w && mask (pageBitsForSize a)) + (end - start)" using assms apply (subst AND_NOT_mask_plus_AND_mask_eq
      [where w = start,symmetric,where n = "pageBitsForSize a"]) apply (simp add: page_base_def) apply (drule word_le_minus_mono_left[where x= "start && ~~ mask (pageBitsForSize a)"]) apply (rule word_and_le2) apply (simp(no_asm_use), simp) done have a: "unat (w && mask (pageBitsForSize a)) + unat (end - start)
    = unat ((w && mask (pageBitsForSize a)) + (end - start))" apply (rule unat_plus_simple[THEN iffD1,symmetric]) apply (rule q) done have b: "end + (start && mask (pageBitsForSize a)) - start
     = end - (start && ~~ mask (pageBitsForSize a))" by (simp add:mask_out_sub_mask) have c: "unat (w && mask (pageBitsForSize a)) + unat (end - start) < 2 ^ pageBitsForSize a" using assms a apply (simp add:field_simps) apply (rule unat_less_helper) apply simp apply (rule_tac P =" \<lambda>x. x < y" for y in ssubst[OF b]) apply (subst AND_NOT_mask_plus_AND_mask_eq
      [where w = "end",symmetric,where n = "pageBitsForSize a"]) apply (simp add:page_base_def) apply (rule and_mask_less') apply simp done show "w \<le> w + (end - start)" using assms apply - apply (rule machine_word_plus_mono_right_split, rule c) apply (simp add:pbfs_less_wb') done show "unat (end - start) \<le> 2 ^ pageBitsForSize a" using q c by (simp add: olen_add_eqv) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. w \<le> w + (end - start) &&& unat (end - start) \<le> 2 ^ pageBitsForSize a proof (state)
goal (2 subgoals):
 1. w \<le> w + (end - start)
 2. unat (end - start) \<le> 2 ^ pageBitsForSize a proof (prove)
goal (1 subgoal):
 1. w && mask (pageBitsForSize a) \<le> (w && mask (pageBitsForSize a)) + (end - start) proof (prove)
using this:
page_base start a = page_base end a
start \<le> end
w && mask (pageBitsForSize a) = start && mask (pageBitsForSize a)

goal (1 subgoal):
 1. w && mask (pageBitsForSize a) \<le> (w && mask (pageBitsForSize a)) + (end - start) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>page_base start a = page_base end a; start \<le> end; w && mask (pageBitsForSize a) = start && mask (pageBitsForSize a)\<rbrakk> \<Longrightarrow> w && mask (pageBitsForSize a) \<le> (w && mask (pageBitsForSize a)) + (end - ((start && ~~ mask (pageBitsForSize a)) + (start && mask (pageBitsForSize a)))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>start && ~~ mask (pageBitsForSize a) = end && ~~ mask (pageBitsForSize a); start \<le> end; w && mask (pageBitsForSize a) = start && mask (pageBitsForSize a)\<rbrakk> \<Longrightarrow> start && mask (pageBitsForSize a) \<le> end && mask (pageBitsForSize a) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>start && ~~ mask (pageBitsForSize a) = end && ~~ mask (pageBitsForSize a); w && mask (pageBitsForSize a) = start && mask (pageBitsForSize a)\<rbrakk> \<Longrightarrow> start && ~~ mask (pageBitsForSize a) \<le> start
 2. \<lbrakk>start && ~~ mask (pageBitsForSize a) = end && ~~ mask (pageBitsForSize a); w && mask (pageBitsForSize a) = start && mask (pageBitsForSize a); start - (start && ~~ mask (pageBitsForSize a)) \<le> end - (start && ~~ mask (pageBitsForSize a))\<rbrakk> \<Longrightarrow> start && mask (pageBitsForSize a) \<le> end && mask (pageBitsForSize a) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>start && ~~ mask (pageBitsForSize a) = end && ~~ mask (pageBitsForSize a); w && mask (pageBitsForSize a) = start && mask (pageBitsForSize a); start - (start && ~~ mask (pageBitsForSize a)) \<le> end - (start && ~~ mask (pageBitsForSize a))\<rbrakk> \<Longrightarrow> start && mask (pageBitsForSize a) \<le> end && mask (pageBitsForSize a) proof (prove)
goal:
No subgoals! proof (state)
this:
w && mask (pageBitsForSize a) \<le> (w && mask (pageBitsForSize a)) + (end - start)

goal (2 subgoals):
 1. w \<le> w + (end - start)
 2. unat (end - start) \<le> 2 ^ pageBitsForSize a proof (prove)
goal (1 subgoal):
 1. unat (w && mask (pageBitsForSize a)) + unat (end - start) = unat ((w && mask (pageBitsForSize a)) + (end - start)) proof (prove)
goal (1 subgoal):
 1. w && mask (pageBitsForSize a) \<le> (w && mask (pageBitsForSize a)) + (end - start) proof (prove)
goal:
No subgoals! proof (state)
this:
unat (w && mask (pageBitsForSize a)) + unat (end - start) = unat ((w && mask (pageBitsForSize a)) + (end - start))

goal (2 subgoals):
 1. w \<le> w + (end - start)
 2. unat (end - start) \<le> 2 ^ pageBitsForSize a proof (prove)
goal (1 subgoal):
 1. end + (start && mask (pageBitsForSize a)) - start = end - (start && ~~ mask (pageBitsForSize a)) proof (state)
this:
end + (start && mask (pageBitsForSize a)) - start = end - (start && ~~ mask (pageBitsForSize a))

goal (2 subgoals):
 1. w \<le> w + (end - start)
 2. unat (end - start) \<le> 2 ^ pageBitsForSize a proof (prove)
goal (1 subgoal):
 1. unat (w && mask (pageBitsForSize a)) + unat (end - start) < 2 ^ pageBitsForSize a proof (prove)
using this:
page_base start a = page_base end a
start \<le> end
w && mask (pageBitsForSize a) = start && mask (pageBitsForSize a)
unat (w && mask (pageBitsForSize a)) + unat (end - start) = unat ((w && mask (pageBitsForSize a)) + (end - start))

goal (1 subgoal):
 1. unat (w && mask (pageBitsForSize a)) + unat (end - start) < 2 ^ pageBitsForSize a proof (prove)
goal (1 subgoal):
 1. \<lbrakk>page_base start a = page_base end a; start \<le> end; w && mask (pageBitsForSize a) = start && mask (pageBitsForSize a); unat (end - start) + unat (start && mask (pageBitsForSize a)) = unat (end + (start && mask (pageBitsForSize a)) - start)\<rbrakk> \<Longrightarrow> unat (end + (start && mask (pageBitsForSize a)) - start) < 2 ^ pageBitsForSize a proof (prove)
goal (1 subgoal):
 1. \<lbrakk>page_base start a = page_base end a; start \<le> end; w && mask (pageBitsForSize a) = start && mask (pageBitsForSize a); unat (end - start) + unat (start && mask (pageBitsForSize a)) = unat (end + (start && mask (pageBitsForSize a)) - start)\<rbrakk> \<Longrightarrow> end + (start && mask (pageBitsForSize a)) - start < word_of_nat (2 ^ pageBitsForSize a) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>page_base start a = page_base end a; start \<le> end; w && mask (pageBitsForSize a) = start && mask (pageBitsForSize a); unat (end - start) + unat (start && mask (pageBitsForSize a)) = unat (end + (start && mask (pageBitsForSize a)) - start)\<rbrakk> \<Longrightarrow> end + (start && mask (pageBitsForSize a)) - start < 2 ^ pageBitsForSize a proof (prove)
goal (1 subgoal):
 1. \<lbrakk>page_base start a = page_base end a; start \<le> end; w && mask (pageBitsForSize a) = start && mask (pageBitsForSize a); unat (end - start) + unat (start && mask (pageBitsForSize a)) = unat (end + (start && mask (pageBitsForSize a)) - start)\<rbrakk> \<Longrightarrow> end - (start && ~~ mask (pageBitsForSize a)) < 2 ^ pageBitsForSize a proof (prove)
goal (1 subgoal):
 1. \<lbrakk>page_base start a = page_base end a; start \<le> end; w && mask (pageBitsForSize a) = start && mask (pageBitsForSize a); unat (end - start) + unat (start && mask (pageBitsForSize a)) = unat (end + (start && mask (pageBitsForSize a)) - start)\<rbrakk> \<Longrightarrow> (end && ~~ mask (pageBitsForSize a)) + (end && mask (pageBitsForSize a)) - (start && ~~ mask (pageBitsForSize a)) < 2 ^ pageBitsForSize a proof (prove)
goal (1 subgoal):
 1. \<lbrakk>start && ~~ mask (pageBitsForSize a) = end && ~~ mask (pageBitsForSize a); start \<le> end; w && mask (pageBitsForSize a) = start && mask (pageBitsForSize a); unat (end - start) + unat (start && mask (pageBitsForSize a)) = unat (end + (start && mask (pageBitsForSize a)) - start)\<rbrakk> \<Longrightarrow> end && mask (pageBitsForSize a) < 2 ^ pageBitsForSize a proof (prove)
goal (1 subgoal):
 1. \<lbrakk>start && ~~ mask (pageBitsForSize a) = end && ~~ mask (pageBitsForSize a); start \<le> end; w && mask (pageBitsForSize a) = start && mask (pageBitsForSize a); unat (end - start) + unat (start && mask (pageBitsForSize a)) = unat (end + (start && mask (pageBitsForSize a)) - start)\<rbrakk> \<Longrightarrow> pageBitsForSize a < LENGTH(32) proof (prove)
goal:
No subgoals! proof (state)
this:
unat (w && mask (pageBitsForSize a)) + unat (end - start) < 2 ^ pageBitsForSize a

goal (2 subgoals):
 1. w \<le> w + (end - start)
 2. unat (end - start) \<le> 2 ^ pageBitsForSize a proof (prove)
goal (1 subgoal):
 1. w \<le> w + (end - start) proof (prove)
using this:
page_base start a = page_base end a
start \<le> end
w && mask (pageBitsForSize a) = start && mask (pageBitsForSize a)

goal (1 subgoal):
 1. w \<le> w + (end - start) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>page_base start a = page_base end a; start \<le> end; w && mask (pageBitsForSize a) = start && mask (pageBitsForSize a)\<rbrakk> \<Longrightarrow> w \<le> w + (end - start) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>page_base start a = page_base end a; start \<le> end; w && mask (pageBitsForSize a) = start && mask (pageBitsForSize a)\<rbrakk> \<Longrightarrow> pageBitsForSize a < word_bits proof (prove)
goal:
No subgoals! proof (state)
this:
w \<le> w + (end - start)

goal (1 subgoal):
 1. unat (end - start) \<le> 2 ^ pageBitsForSize a proof (prove)
goal (1 subgoal):
 1. unat (end - start) \<le> 2 ^ pageBitsForSize a proof (prove)
using this:
w && mask (pageBitsForSize a) \<le> (w && mask (pageBitsForSize a)) + (end - start)
unat (w && mask (pageBitsForSize a)) + unat (end - start) < 2 ^ pageBitsForSize a

goal (1 subgoal):
 1. unat (end - start) \<le> 2 ^ pageBitsForSize a proof (state)
this:
unat (end - start) \<le> 2 ^ pageBitsForSize a

goal:
No subgoals!