theory Retype_AI

lemma retype_addrs_range_subset:
  "\<lbrakk>  p \<in> set (retype_addrs ptr ty n us);
     range_cover ptr sz (obj_bits_api ty us) n \<rbrakk>
  \<Longrightarrow> {p .. p + 2 ^ obj_bits_api ty us - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2^sz - 1}" apply (clarsimp simp: retype_addrs_def ptr_add_def
              simp del: atLeastatMost_subset_iff atLeastAtMost_iff) apply (frule_tac x = "of_nat x" in range_cover_cell_subset) apply (erule of_nat_mono_maybe[rotated]) apply (drule range_cover.range_cover_n_less) apply (simp add:word_bits_def) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> set (retype_addrs ptr ty n us); range_cover ptr sz (obj_bits_api ty us) n\<rbrakk> \<Longrightarrow> {p..p + 2 ^ obj_bits_api ty us - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; x < n; p = ptr + word_of_nat x * 2 ^ obj_bits_api ty us; xa \<in> {ptr + word_of_nat x * 2 ^ obj_bits_api ty us..ptr + word_of_nat x * 2 ^ obj_bits_api ty us + 2 ^ obj_bits_api ty us - 1}\<rbrakk> \<Longrightarrow> xa \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; x < n; p = ptr + word_of_nat x * 2 ^ obj_bits_api ty us; xa \<in> {ptr + word_of_nat x * 2 ^ obj_bits_api ty us..ptr + word_of_nat x * 2 ^ obj_bits_api ty us + 2 ^ obj_bits_api ty us - 1}\<rbrakk> \<Longrightarrow> word_of_nat x < word_of_nat n
 2. \<And>x xa. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; x < n; p = ptr + word_of_nat x * 2 ^ obj_bits_api ty us; xa \<in> {ptr + word_of_nat x * 2 ^ obj_bits_api ty us..ptr + word_of_nat x * 2 ^ obj_bits_api ty us + 2 ^ obj_bits_api ty us - 1}; {ptr + word_of_nat x * 2 ^ obj_bits_api ty us..ptr + word_of_nat x * 2 ^ obj_bits_api ty us + 2 ^ obj_bits_api ty us - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> xa \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; p = ptr + word_of_nat x * 2 ^ obj_bits_api ty us; xa \<in> {ptr + word_of_nat x * 2 ^ obj_bits_api ty us..ptr + word_of_nat x * 2 ^ obj_bits_api ty us + 2 ^ obj_bits_api ty us - 1}\<rbrakk> \<Longrightarrow> n < 2 ^ LENGTH(32)
 2. \<And>x xa. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; x < n; p = ptr + word_of_nat x * 2 ^ obj_bits_api ty us; xa \<in> {ptr + word_of_nat x * 2 ^ obj_bits_api ty us..ptr + word_of_nat x * 2 ^ obj_bits_api ty us + 2 ^ obj_bits_api ty us - 1}; {ptr + word_of_nat x * 2 ^ obj_bits_api ty us..ptr + word_of_nat x * 2 ^ obj_bits_api ty us + 2 ^ obj_bits_api ty us - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> xa \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>p = ptr + word_of_nat x * 2 ^ obj_bits_api ty us; xa \<in> {ptr + word_of_nat x * 2 ^ obj_bits_api ty us..ptr + word_of_nat x * 2 ^ obj_bits_api ty us + 2 ^ obj_bits_api ty us - 1}; n < 2 ^ LENGTH(32)\<rbrakk> \<Longrightarrow> n < 2 ^ LENGTH(32)
 2. \<And>x xa. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; x < n; p = ptr + word_of_nat x * 2 ^ obj_bits_api ty us; xa \<in> {ptr + word_of_nat x * 2 ^ obj_bits_api ty us..ptr + word_of_nat x * 2 ^ obj_bits_api ty us + 2 ^ obj_bits_api ty us - 1}; {ptr + word_of_nat x * 2 ^ obj_bits_api ty us..ptr + word_of_nat x * 2 ^ obj_bits_api ty us + 2 ^ obj_bits_api ty us - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> xa \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; x < n; p = ptr + word_of_nat x * 2 ^ obj_bits_api ty us; xa \<in> {ptr + word_of_nat x * 2 ^ obj_bits_api ty us..ptr + word_of_nat x * 2 ^ obj_bits_api ty us + 2 ^ obj_bits_api ty us - 1}; {ptr + word_of_nat x * 2 ^ obj_bits_api ty us..ptr + word_of_nat x * 2 ^ obj_bits_api ty us + 2 ^ obj_bits_api ty us - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> xa \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} proof (prove)
goal:
No subgoals!