theory Detype_AI

lemma range_cover_bound:
  assumes cover:"range_cover ptr sz us n"
  shows "0<n \<Longrightarrow> ptr \<le> ptr + of_nat n * 2^ us - 1" apply (cut_tac range_cover_subset[OF cover,where p = 0]) apply (cut_tac Retype_AI.range_cover_subset_not_empty[OF _ cover , where x = 0]) apply (clarsimp simp del: atLeastatMost_subset_iff) apply (drule_tac c=ptr in subsetD) apply simp apply simp apply (cut_tac range_cover_not_zero[OF _ cover]) apply (simp add:word_gt_0)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> ptr \<le> ptr + word_of_nat n * 2 ^ us - 1 proof (prove)
goal (3 subgoals):
 1. \<lbrakk>0 < n; {ptr + word_of_nat 0 * 2 ^ us..ptr + word_of_nat 0 * 2 ^ us + 2 ^ us - 1} \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ us - 1}\<rbrakk> \<Longrightarrow> ptr \<le> ptr + word_of_nat n * 2 ^ us - 1
 2. 0 < n \<Longrightarrow> 0 < n
 3. 0 < n \<Longrightarrow> n \<noteq> 0 proof (prove)
goal (4 subgoals):
 1. \<lbrakk>0 < n; {ptr + word_of_nat 0 * 2 ^ us..ptr + word_of_nat 0 * 2 ^ us + 2 ^ us - 1} \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ us - 1}; {ptr + 0 * 2 ^ us..ptr + 0 * 2 ^ us + 2 ^ us - 1} \<noteq> {}\<rbrakk> \<Longrightarrow> ptr \<le> ptr + word_of_nat n * 2 ^ us - 1
 2. \<lbrakk>0 < n; {ptr + word_of_nat 0 * 2 ^ us..ptr + word_of_nat 0 * 2 ^ us + 2 ^ us - 1} \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ us - 1}\<rbrakk> \<Longrightarrow> 0 < word_of_nat n
 3. 0 < n \<Longrightarrow> 0 < n
 4. 0 < n \<Longrightarrow> n \<noteq> 0 proof (prove)
goal (4 subgoals):
 1. \<lbrakk>0 < n; {ptr..ptr + 2 ^ us - 1} \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ us - 1}; ptr \<le> ptr + 2 ^ us - 1\<rbrakk> \<Longrightarrow> ptr \<le> ptr + word_of_nat n * 2 ^ us - 1
 2. \<lbrakk>0 < n; {ptr + word_of_nat 0 * 2 ^ us..ptr + word_of_nat 0 * 2 ^ us + 2 ^ us - 1} \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ us - 1}\<rbrakk> \<Longrightarrow> 0 < word_of_nat n
 3. 0 < n \<Longrightarrow> 0 < n
 4. 0 < n \<Longrightarrow> n \<noteq> 0 proof (prove)
goal (5 subgoals):
 1. \<lbrakk>0 < n; ptr \<le> ptr + 2 ^ us - 1\<rbrakk> \<Longrightarrow> ptr \<in> {ptr..ptr + 2 ^ us - 1}
 2. \<lbrakk>0 < n; ptr \<le> ptr + 2 ^ us - 1; ptr \<in> {ptr..ptr + word_of_nat n * 2 ^ us - 1}\<rbrakk> \<Longrightarrow> ptr \<le> ptr + word_of_nat n * 2 ^ us - 1
 3. \<lbrakk>0 < n; {ptr + word_of_nat 0 * 2 ^ us..ptr + word_of_nat 0 * 2 ^ us + 2 ^ us - 1} \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ us - 1}\<rbrakk> \<Longrightarrow> 0 < word_of_nat n
 4. 0 < n \<Longrightarrow> 0 < n
 5. 0 < n \<Longrightarrow> n \<noteq> 0 proof (prove)
goal (4 subgoals):
 1. \<lbrakk>0 < n; ptr \<le> ptr + 2 ^ us - 1; ptr \<in> {ptr..ptr + word_of_nat n * 2 ^ us - 1}\<rbrakk> \<Longrightarrow> ptr \<le> ptr + word_of_nat n * 2 ^ us - 1
 2. \<lbrakk>0 < n; {ptr + word_of_nat 0 * 2 ^ us..ptr + word_of_nat 0 * 2 ^ us + 2 ^ us - 1} \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ us - 1}\<rbrakk> \<Longrightarrow> 0 < word_of_nat n
 3. 0 < n \<Longrightarrow> 0 < n
 4. 0 < n \<Longrightarrow> n \<noteq> 0 proof (prove)
goal (3 subgoals):
 1. \<lbrakk>0 < n; {ptr + word_of_nat 0 * 2 ^ us..ptr + word_of_nat 0 * 2 ^ us + 2 ^ us - 1} \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ us - 1}\<rbrakk> \<Longrightarrow> 0 < word_of_nat n
 2. 0 < n \<Longrightarrow> 0 < n
 3. 0 < n \<Longrightarrow> n \<noteq> 0 proof (prove)
goal (4 subgoals):
 1. \<lbrakk>0 < n; {ptr + word_of_nat 0 * 2 ^ us..ptr + word_of_nat 0 * 2 ^ us + 2 ^ us - 1} \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ us - 1}; word_of_nat n \<noteq> 0\<rbrakk> \<Longrightarrow> 0 < word_of_nat n
 2. \<lbrakk>0 < n; {ptr + word_of_nat 0 * 2 ^ us..ptr + word_of_nat 0 * 2 ^ us + 2 ^ us - 1} \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ us - 1}\<rbrakk> \<Longrightarrow> n \<noteq> 0
 3. 0 < n \<Longrightarrow> 0 < n
 4. 0 < n \<Longrightarrow> n \<noteq> 0 proof (prove)
goal:
No subgoals!