theory Detype_AI

lemma intvl_range_conv':
  "\<lbrakk>is_aligned (ptr::'a :: len word) bits; bits \<le> len_of TYPE('a)\<rbrakk> \<Longrightarrow>
   (\<exists>k. x = ptr + of_nat k \<and> k < 2 ^ bits) \<longleftrightarrow> (ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1)" apply (rule iffI) apply (clarsimp simp: x_power_minus_1 mask_2pm1[symmetric]) apply (frule is_aligned_no_overflow'[simplified mask_2pm1[symmetric]]) apply (rule conjI) apply (rule word_plus_mono_right2, assumption) apply (frule (2) of_nat_le_pow) apply (rule word_plus_mono_right) apply (rule word_of_nat_le) apply (simp add: unat_mask) apply simp apply (subgoal_tac "\<exists>x'. x = ptr + of_nat x' \<and> x' < 2 ^ len_of TYPE('a)") apply clarsimp apply (drule(1) word_le_minus_mono_left [where x=ptr]) apply (simp only: p_assoc_help add_diff_cancel2) apply (rule_tac x="x'" in exI) apply (clarsimp simp: word_le_nat_alt unat_of_nat mask_2pm1[symmetric]) apply (auto simp: unat_mask min_def le_less)[1] apply (rule_tac x="unat (x - ptr)" in exI) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr bits; bits \<le> LENGTH('a)\<rbrakk> \<Longrightarrow> (\<exists>k. x = ptr + word_of_nat k \<and> k < 2 ^ bits) = (ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr bits; bits \<le> LENGTH('a); \<exists>k. x = ptr + word_of_nat k \<and> k < 2 ^ bits\<rbrakk> \<Longrightarrow> ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1
 2. \<lbrakk>is_aligned ptr bits; bits \<le> LENGTH('a); ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> \<exists>k. x = ptr + word_of_nat k \<and> k < 2 ^ bits proof (prove)
goal (2 subgoals):
 1. \<And>k. \<lbrakk>is_aligned ptr bits; bits \<le> LENGTH('a); k < 2 ^ bits; x = ptr + word_of_nat k\<rbrakk> \<Longrightarrow> ptr \<le> ptr + word_of_nat k \<and> ptr + word_of_nat k \<le> ptr + mask bits
 2. \<lbrakk>is_aligned ptr bits; bits \<le> LENGTH('a); ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> \<exists>k. x = ptr + word_of_nat k \<and> k < 2 ^ bits proof (prove)
goal (2 subgoals):
 1. \<And>k. \<lbrakk>is_aligned ptr bits; bits \<le> LENGTH('a); k < 2 ^ bits; x = ptr + word_of_nat k; ptr \<le> ptr + mask bits\<rbrakk> \<Longrightarrow> ptr \<le> ptr + word_of_nat k \<and> ptr + word_of_nat k \<le> ptr + mask bits
 2. \<lbrakk>is_aligned ptr bits; bits \<le> LENGTH('a); ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> \<exists>k. x = ptr + word_of_nat k \<and> k < 2 ^ bits proof (prove)
goal (3 subgoals):
 1. \<And>k. \<lbrakk>is_aligned ptr bits; bits \<le> LENGTH('a); k < 2 ^ bits; x = ptr + word_of_nat k; ptr \<le> ptr + mask bits\<rbrakk> \<Longrightarrow> ptr \<le> ptr + word_of_nat k
 2. \<And>k. \<lbrakk>is_aligned ptr bits; bits \<le> LENGTH('a); k < 2 ^ bits; x = ptr + word_of_nat k; ptr \<le> ptr + mask bits\<rbrakk> \<Longrightarrow> ptr + word_of_nat k \<le> ptr + mask bits
 3. \<lbrakk>is_aligned ptr bits; bits \<le> LENGTH('a); ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> \<exists>k. x = ptr + word_of_nat k \<and> k < 2 ^ bits proof (prove)
goal (3 subgoals):
 1. \<And>k. \<lbrakk>is_aligned ptr bits; bits \<le> LENGTH('a); k < 2 ^ bits; x = ptr + word_of_nat k; ptr \<le> ptr + mask bits\<rbrakk> \<Longrightarrow> word_of_nat k \<le> mask bits
 2. \<And>k. \<lbrakk>is_aligned ptr bits; bits \<le> LENGTH('a); k < 2 ^ bits; x = ptr + word_of_nat k; ptr \<le> ptr + mask bits\<rbrakk> \<Longrightarrow> ptr + word_of_nat k \<le> ptr + mask bits
 3. \<lbrakk>is_aligned ptr bits; bits \<le> LENGTH('a); ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> \<exists>k. x = ptr + word_of_nat k \<and> k < 2 ^ bits proof (prove)
goal (2 subgoals):
 1. \<And>k. \<lbrakk>is_aligned ptr bits; bits \<le> LENGTH('a); k < 2 ^ bits; x = ptr + word_of_nat k; ptr \<le> ptr + mask bits\<rbrakk> \<Longrightarrow> ptr + word_of_nat k \<le> ptr + mask bits
 2. \<lbrakk>is_aligned ptr bits; bits \<le> LENGTH('a); ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> \<exists>k. x = ptr + word_of_nat k \<and> k < 2 ^ bits proof (prove)
goal (3 subgoals):
 1. \<And>k. \<lbrakk>is_aligned ptr bits; bits \<le> LENGTH('a); k < 2 ^ bits; x = ptr + word_of_nat k; ptr \<le> ptr + mask bits\<rbrakk> \<Longrightarrow> word_of_nat k \<le> mask bits
 2. \<And>k. \<lbrakk>is_aligned ptr bits; bits \<le> LENGTH('a); k < 2 ^ bits; x = ptr + word_of_nat k; ptr \<le> ptr + mask bits\<rbrakk> \<Longrightarrow> ptr \<le> ptr + mask bits
 3. \<lbrakk>is_aligned ptr bits; bits \<le> LENGTH('a); ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> \<exists>k. x = ptr + word_of_nat k \<and> k < 2 ^ bits proof (prove)
goal (3 subgoals):
 1. \<And>k. \<lbrakk>is_aligned ptr bits; bits \<le> LENGTH('a); k < 2 ^ bits; x = ptr + word_of_nat k; ptr \<le> ptr + mask bits\<rbrakk> \<Longrightarrow> k \<le> unat (mask bits)
 2. \<And>k. \<lbrakk>is_aligned ptr bits; bits \<le> LENGTH('a); k < 2 ^ bits; x = ptr + word_of_nat k; ptr \<le> ptr + mask bits\<rbrakk> \<Longrightarrow> ptr \<le> ptr + mask bits
 3. \<lbrakk>is_aligned ptr bits; bits \<le> LENGTH('a); ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> \<exists>k. x = ptr + word_of_nat k \<and> k < 2 ^ bits proof (prove)
goal (2 subgoals):
 1. \<And>k. \<lbrakk>is_aligned ptr bits; bits \<le> LENGTH('a); k < 2 ^ bits; x = ptr + word_of_nat k; ptr \<le> ptr + mask bits\<rbrakk> \<Longrightarrow> ptr \<le> ptr + mask bits
 2. \<lbrakk>is_aligned ptr bits; bits \<le> LENGTH('a); ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> \<exists>k. x = ptr + word_of_nat k \<and> k < 2 ^ bits proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr bits; bits \<le> LENGTH('a); ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> \<exists>k. x = ptr + word_of_nat k \<and> k < 2 ^ bits proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr bits; bits \<le> LENGTH('a); ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1; \<exists>x'. x = ptr + word_of_nat x' \<and> x' < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> \<exists>k. x = ptr + word_of_nat k \<and> k < 2 ^ bits
 2. \<lbrakk>is_aligned ptr bits; bits \<le> LENGTH('a); ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> \<exists>x'. x = ptr + word_of_nat x' \<and> x' < 2 ^ LENGTH('a) proof (prove)
goal (2 subgoals):
 1. \<And>x'. \<lbrakk>is_aligned ptr bits; bits \<le> LENGTH('a); ptr \<le> ptr + word_of_nat x'; ptr + word_of_nat x' \<le> ptr + 2 ^ bits - 1; x' < 2 ^ LENGTH('a); x = ptr + word_of_nat x'\<rbrakk> \<Longrightarrow> \<exists>k. word_of_nat x' = word_of_nat k \<and> k < 2 ^ bits
 2. \<lbrakk>is_aligned ptr bits; bits \<le> LENGTH('a); ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> \<exists>x'. x = ptr + word_of_nat x' \<and> x' < 2 ^ LENGTH('a) proof (prove)
goal (2 subgoals):
 1. \<And>x'. \<lbrakk>is_aligned ptr bits; bits \<le> LENGTH('a); ptr \<le> ptr + word_of_nat x'; x' < 2 ^ LENGTH('a); x = ptr + word_of_nat x'; ptr + word_of_nat x' - ptr \<le> ptr + 2 ^ bits - 1 - ptr\<rbrakk> \<Longrightarrow> \<exists>k. word_of_nat x' = word_of_nat k \<and> k < 2 ^ bits
 2. \<lbrakk>is_aligned ptr bits; bits \<le> LENGTH('a); ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> \<exists>x'. x = ptr + word_of_nat x' \<and> x' < 2 ^ LENGTH('a) proof (prove)
goal (2 subgoals):
 1. \<And>x'. \<lbrakk>is_aligned ptr bits; bits \<le> LENGTH('a); ptr \<le> ptr + word_of_nat x'; x' < 2 ^ LENGTH('a); x = ptr + word_of_nat x'; word_of_nat x' \<le> 2 ^ bits - 1\<rbrakk> \<Longrightarrow> \<exists>k. word_of_nat x' = word_of_nat k \<and> k < 2 ^ bits
 2. \<lbrakk>is_aligned ptr bits; bits \<le> LENGTH('a); ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> \<exists>x'. x = ptr + word_of_nat x' \<and> x' < 2 ^ LENGTH('a) proof (prove)
goal (2 subgoals):
 1. \<And>x'. \<lbrakk>is_aligned ptr bits; bits \<le> LENGTH('a); ptr \<le> ptr + word_of_nat x'; x' < 2 ^ LENGTH('a); x = ptr + word_of_nat x'; word_of_nat x' \<le> 2 ^ bits - 1\<rbrakk> \<Longrightarrow> word_of_nat x' = word_of_nat x' \<and> x' < 2 ^ bits
 2. \<lbrakk>is_aligned ptr bits; bits \<le> LENGTH('a); ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> \<exists>x'. x = ptr + word_of_nat x' \<and> x' < 2 ^ LENGTH('a) proof (prove)
goal (2 subgoals):
 1. \<And>x'. \<lbrakk>is_aligned ptr bits; bits \<le> LENGTH('a); unat ptr \<le> unat (ptr + word_of_nat x'); x' < 2 ^ LENGTH('a); x = ptr + word_of_nat x'; x' \<le> unat (mask bits)\<rbrakk> \<Longrightarrow> x' < 2 ^ bits
 2. \<lbrakk>is_aligned ptr bits; bits \<le> LENGTH('a); ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> \<exists>x'. x = ptr + word_of_nat x' \<and> x' < 2 ^ LENGTH('a) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr bits; bits \<le> LENGTH('a); ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> \<exists>x'. x = ptr + word_of_nat x' \<and> x' < 2 ^ LENGTH('a) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr bits; bits \<le> LENGTH('a); ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> x = ptr + word_of_nat (unat (x - ptr)) \<and> unat (x - ptr) < 2 ^ LENGTH('a) proof (prove)
goal:
No subgoals!