theory Retype_C

lemma range_cover_nca_neg: "\<And>x p (off :: 10 word).
  \<lbrakk>(x::word32) < 4; {p..+2 ^pageBits } \<inter> {ptr..ptr + (of_nat n * 2 ^ (gbits + pageBits) - 1)} = {};
    range_cover ptr sz (gbits + pageBits) n\<rbrakk>
  \<Longrightarrow> p + ucast off * 4 + x \<notin> {ptr..+n * 2 ^ (gbits + pageBits)}" apply (case_tac "n = 0") apply simp apply (subst range_cover_intvl,simp) apply simp apply (subgoal_tac "p + ucast off * 4 + x \<in>  {p..+2 ^ pageBits}") apply blast apply (clarsimp simp: intvl_def) apply (rule_tac x = "unat off * 4 + unat x" in exI) apply (simp add: ucast_nat_def) apply (rule nat_add_offset_less [where n = 2, simplified]) apply (simp add: word_less_nat_alt) apply (rule unat_lt2p) apply (simp add: pageBits_def objBits_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>x p off. \<lbrakk>x < 4; {p..+2 ^ pageBits} \<inter> {ptr..ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)} = {}; range_cover ptr sz (gbits + pageBits) n\<rbrakk> \<Longrightarrow> p + UCAST(10 \<rightarrow> 32) off * 4 + x \<notin> {ptr..+n * 2 ^ (gbits + pageBits)} proof (prove)
goal (2 subgoals):
 1. \<And>x p off. \<lbrakk>x < 4; {p..+2 ^ pageBits} \<inter> {ptr..ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)} = {}; range_cover ptr sz (gbits + pageBits) n; n = 0\<rbrakk> \<Longrightarrow> p + UCAST(10 \<rightarrow> 32) off * 4 + x \<notin> {ptr..+n * 2 ^ (gbits + pageBits)}
 2. \<And>x p off. \<lbrakk>x < 4; {p..+2 ^ pageBits} \<inter> {ptr..ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)} = {}; range_cover ptr sz (gbits + pageBits) n; n \<noteq> 0\<rbrakk> \<Longrightarrow> p + UCAST(10 \<rightarrow> 32) off * 4 + x \<notin> {ptr..+n * 2 ^ (gbits + pageBits)} proof (prove)
goal (1 subgoal):
 1. \<And>x p off. \<lbrakk>x < 4; {p..+2 ^ pageBits} \<inter> {ptr..ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)} = {}; range_cover ptr sz (gbits + pageBits) n; n \<noteq> 0\<rbrakk> \<Longrightarrow> p + UCAST(10 \<rightarrow> 32) off * 4 + x \<notin> {ptr..+n * 2 ^ (gbits + pageBits)} proof (prove)
goal (2 subgoals):
 1. \<And>x p off. \<lbrakk>x < 4; {p..+2 ^ pageBits} \<inter> {ptr..ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)} = {}; range_cover ptr sz (gbits + pageBits) n; n \<noteq> 0\<rbrakk> \<Longrightarrow> n \<noteq> 0
 2. \<And>x p off. \<lbrakk>x < 4; {p..+2 ^ pageBits} \<inter> {ptr..ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)} = {}; range_cover ptr sz (gbits + pageBits) n; n \<noteq> 0\<rbrakk> \<Longrightarrow> p + UCAST(10 \<rightarrow> 32) off * 4 + x \<notin> {ptr..ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)} proof (prove)
goal (1 subgoal):
 1. \<And>x p off. \<lbrakk>x < 4; {p..+2 ^ pageBits} \<inter> {ptr..ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)} = {}; range_cover ptr sz (gbits + pageBits) n; n \<noteq> 0\<rbrakk> \<Longrightarrow> p + UCAST(10 \<rightarrow> 32) off * 4 + x \<notin> {ptr..ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)} proof (prove)
goal (2 subgoals):
 1. \<And>x p off. \<lbrakk>x < 4; {p..+2 ^ pageBits} \<inter> {ptr..ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)} = {}; range_cover ptr sz (gbits + pageBits) n; n \<noteq> 0; p + UCAST(10 \<rightarrow> 32) off * 4 + x \<in> {p..+2 ^ pageBits}\<rbrakk> \<Longrightarrow> p + UCAST(10 \<rightarrow> 32) off * 4 + x \<notin> {ptr..ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)}
 2. \<And>x p off. \<lbrakk>x < 4; {p..+2 ^ pageBits} \<inter> {ptr..ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)} = {}; range_cover ptr sz (gbits + pageBits) n; n \<noteq> 0\<rbrakk> \<Longrightarrow> p + UCAST(10 \<rightarrow> 32) off * 4 + x \<in> {p..+2 ^ pageBits} proof (prove)
goal (1 subgoal):
 1. \<And>x p off. \<lbrakk>x < 4; {p..+2 ^ pageBits} \<inter> {ptr..ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)} = {}; range_cover ptr sz (gbits + pageBits) n; n \<noteq> 0\<rbrakk> \<Longrightarrow> p + UCAST(10 \<rightarrow> 32) off * 4 + x \<in> {p..+2 ^ pageBits} proof (prove)
goal (1 subgoal):
 1. \<And>x p off. \<lbrakk>x < 4; {p + word_of_nat k |k. k < 2 ^ pageBits} \<inter> {ptr..ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)} = {}; range_cover ptr sz (gbits + pageBits) n; 0 < n\<rbrakk> \<Longrightarrow> \<exists>k. UCAST(10 \<rightarrow> 32) off * 4 + x = word_of_nat k \<and> k < 2 ^ pageBits proof (prove)
goal (1 subgoal):
 1. \<And>x p off. \<lbrakk>x < 4; {p + word_of_nat k |k. k < 2 ^ pageBits} \<inter> {ptr..ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)} = {}; range_cover ptr sz (gbits + pageBits) n; 0 < n\<rbrakk> \<Longrightarrow> UCAST(10 \<rightarrow> 32) off * 4 + x = word_of_nat (unat off * 4 + unat x) \<and> unat off * 4 + unat x < 2 ^ pageBits proof (prove)
goal (1 subgoal):
 1. \<And>x p off. \<lbrakk>x < 4; {p + word_of_nat k |k. k < 2 ^ pageBits} \<inter> {ptr..ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)} = {}; range_cover ptr sz (gbits + pageBits) n; 0 < n\<rbrakk> \<Longrightarrow> unat off * 4 + unat x < 2 ^ pageBits proof (prove)
goal (3 subgoals):
 1. \<And>x p off. \<lbrakk>x < 4; {p + word_of_nat k |k. k < 2 ^ pageBits} \<inter> {ptr..ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)} = {}; range_cover ptr sz (gbits + pageBits) n; 0 < n\<rbrakk> \<Longrightarrow> unat x < 4
 2. \<And>x p off. \<lbrakk>x < 4; {p + word_of_nat k |k. k < 2 ^ pageBits} \<inter> {ptr..ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)} = {}; range_cover ptr sz (gbits + pageBits) n; 0 < n\<rbrakk> \<Longrightarrow> unat off < 2 ^ ?m16 x p off
 3. \<And>x p off. \<lbrakk>x < 4; {p + word_of_nat k |k. k < 2 ^ pageBits} \<inter> {ptr..ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)} = {}; range_cover ptr sz (gbits + pageBits) n; 0 < n\<rbrakk> \<Longrightarrow> pageBits = Suc (Suc (?m16 x p off)) proof (prove)
goal (2 subgoals):
 1. \<And>x p off. \<lbrakk>x < 4; {p + word_of_nat k |k. k < 2 ^ pageBits} \<inter> {ptr..ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)} = {}; range_cover ptr sz (gbits + pageBits) n; 0 < n\<rbrakk> \<Longrightarrow> unat off < 2 ^ ?m16 x p off
 2. \<And>x p off. \<lbrakk>x < 4; {p + word_of_nat k |k. k < 2 ^ pageBits} \<inter> {ptr..ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)} = {}; range_cover ptr sz (gbits + pageBits) n; 0 < n\<rbrakk> \<Longrightarrow> pageBits = Suc (Suc (?m16 x p off)) proof (prove)
goal (1 subgoal):
 1. \<And>x p off. \<lbrakk>x < 4; {p + word_of_nat k |k. k < 2 ^ pageBits} \<inter> {ptr..ptr + (word_of_nat n * 2 ^ (gbits + pageBits) - 1)} = {}; range_cover ptr sz (gbits + pageBits) n; 0 < n\<rbrakk> \<Longrightarrow> pageBits = Suc (Suc LENGTH(10)) proof (prove)
goal:
No subgoals!