theory Retype_C

lemma offset_intvl_first_chunk_subsets:
  "range_cover (p :: addr) sz bits n
    \<Longrightarrow> i < of_nat n
    \<Longrightarrow> {p + (i << bits) ..+ 2 ^ bits} \<subseteq> {p + (i << bits) ..+ (n - unat i) * 2 ^ bits}
        \<and> {p + ((i + 1) << bits) ..+ (n - unat (i + 1)) * 2 ^ bits}
            \<le> {p + (i << bits) ..+ (n - unat i) * 2 ^ bits}
        \<and> {p + (i << bits) ..+ 2 ^ bits}
            \<inter> {p + ((i + 1) << bits) ..+ (n - unat (i + 1)) * 2 ^ bits}
            = {}" apply (strengthen intvl_start_le) apply (strengthen order_trans[OF _
      intvl_sub_offset[where x="2 ^ bits" and y="(n - unat (i + 1)) * 2 ^ bits"]]) apply (frule range_cover_sz') apply (cut_tac n=i in unatSuc) apply unat_arith apply (simp add: word_shiftl_add_distrib field_simps TWO) apply (simp add: mult_Suc[symmetric] del: mult_Suc) apply (frule unat_less_helper) apply (cut_tac p="p + (i << bits)" and k="2 ^ bits"
    and z="(n - unat (i + 1)) * 2 ^ bits" in init_intvl_disj) apply (simp add: field_simps) apply (drule range_cover.strong_times_32, simp) apply (simp add: addr_card_def word_bits_def card_word) apply (erule order_le_less_trans[rotated]) apply (simp add: mult_Suc[symmetric] del: mult_Suc) apply (simp add: Int_commute field_simps) apply unat_arith done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover p sz bits n; i < word_of_nat n\<rbrakk> \<Longrightarrow> {p + (i << bits)..+2 ^ bits} \<subseteq> {p + (i << bits)..+(n - unat i) * 2 ^ bits} \<and> {p + (i + 1 << bits)..+(n - unat (i + 1)) * 2 ^ bits} \<subseteq> {p + (i << bits)..+(n - unat i) * 2 ^ bits} \<and> {p + (i << bits)..+2 ^ bits} \<inter> {p + (i + 1 << bits)..+(n - unat (i + 1)) * 2 ^ bits} = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover p sz bits n; i < word_of_nat n\<rbrakk> \<Longrightarrow> 2 ^ bits \<le> (n - unat i) * 2 ^ bits \<and> {p + (i + 1 << bits)..+(n - unat (i + 1)) * 2 ^ bits} \<subseteq> {p + (i << bits)..+(n - unat i) * 2 ^ bits} \<and> {p + (i << bits)..+2 ^ bits} \<inter> {p + (i + 1 << bits)..+(n - unat (i + 1)) * 2 ^ bits} = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover p sz bits n; i < word_of_nat n\<rbrakk> \<Longrightarrow> 2 ^ bits \<le> (n - unat i) * 2 ^ bits \<and> ({p + (i + 1 << bits)..+(n - unat (i + 1)) * 2 ^ bits} \<subseteq> {p + (i << bits) + 2 ^ bits..+(n - unat (i + 1)) * 2 ^ bits} \<and> unat (2 ^ bits) + (n - unat (i + 1)) * 2 ^ bits \<le> (n - unat i) * 2 ^ bits) \<and> {p + (i << bits)..+2 ^ bits} \<inter> {p + (i + 1 << bits)..+(n - unat (i + 1)) * 2 ^ bits} = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover p sz bits n; i < word_of_nat n; bits < LENGTH(32)\<rbrakk> \<Longrightarrow> 2 ^ bits \<le> (n - unat i) * 2 ^ bits \<and> ({p + (i + 1 << bits)..+(n - unat (i + 1)) * 2 ^ bits} \<subseteq> {p + (i << bits) + 2 ^ bits..+(n - unat (i + 1)) * 2 ^ bits} \<and> unat (2 ^ bits) + (n - unat (i + 1)) * 2 ^ bits \<le> (n - unat i) * 2 ^ bits) \<and> {p + (i << bits)..+2 ^ bits} \<inter> {p + (i + 1 << bits)..+(n - unat (i + 1)) * 2 ^ bits} = {} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>range_cover p sz bits n; i < word_of_nat n; bits < LENGTH(32)\<rbrakk> \<Longrightarrow> 1 + i \<noteq> 0
 2. \<lbrakk>range_cover p sz bits n; i < word_of_nat n; bits < LENGTH(32); unat (1 + i) = Suc (unat i)\<rbrakk> \<Longrightarrow> 2 ^ bits \<le> (n - unat i) * 2 ^ bits \<and> ({p + (i + 1 << bits)..+(n - unat (i + 1)) * 2 ^ bits} \<subseteq> {p + (i << bits) + 2 ^ bits..+(n - unat (i + 1)) * 2 ^ bits} \<and> unat (2 ^ bits) + (n - unat (i + 1)) * 2 ^ bits \<le> (n - unat i) * 2 ^ bits) \<and> {p + (i << bits)..+2 ^ bits} \<inter> {p + (i + 1 << bits)..+(n - unat (i + 1)) * 2 ^ bits} = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover p sz bits n; i < word_of_nat n; bits < LENGTH(32); unat (1 + i) = Suc (unat i)\<rbrakk> \<Longrightarrow> 2 ^ bits \<le> (n - unat i) * 2 ^ bits \<and> ({p + (i + 1 << bits)..+(n - unat (i + 1)) * 2 ^ bits} \<subseteq> {p + (i << bits) + 2 ^ bits..+(n - unat (i + 1)) * 2 ^ bits} \<and> unat (2 ^ bits) + (n - unat (i + 1)) * 2 ^ bits \<le> (n - unat i) * 2 ^ bits) \<and> {p + (i << bits)..+2 ^ bits} \<inter> {p + (i + 1 << bits)..+(n - unat (i + 1)) * 2 ^ bits} = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover p sz bits n; i < word_of_nat n; bits < 32; unat (1 + i) = Suc (unat i)\<rbrakk> \<Longrightarrow> Suc 0 \<le> n - unat i \<and> 2 ^ bits + (n - Suc (unat i)) * 2 ^ bits \<le> (n - unat i) * 2 ^ bits \<and> {p + (i << bits)..+2 ^ bits} \<inter> {p + ((i << bits) + 2 ^ bits)..+(n - Suc (unat i)) * 2 ^ bits} = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover p sz bits n; i < word_of_nat n; bits < 32; unat (1 + i) = Suc (unat i)\<rbrakk> \<Longrightarrow> Suc 0 \<le> n - unat i \<and> Suc (n - Suc (unat i)) \<le> n - unat i \<and> {p + (i << bits)..+2 ^ bits} \<inter> {p + ((i << bits) + 2 ^ bits)..+(n - Suc (unat i)) * 2 ^ bits} = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover p sz bits n; i < word_of_nat n; bits < 32; unat (1 + i) = Suc (unat i); unat i < n\<rbrakk> \<Longrightarrow> Suc 0 \<le> n - unat i \<and> Suc (n - Suc (unat i)) \<le> n - unat i \<and> {p + (i << bits)..+2 ^ bits} \<inter> {p + ((i << bits) + 2 ^ bits)..+(n - Suc (unat i)) * 2 ^ bits} = {} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>range_cover p sz bits n; i < word_of_nat n; bits < 32; unat (1 + i) = Suc (unat i); unat i < n\<rbrakk> \<Longrightarrow> 2 ^ bits + (n - unat (i + 1)) * 2 ^ bits < addr_card
 2. \<lbrakk>range_cover p sz bits n; i < word_of_nat n; bits < 32; unat (1 + i) = Suc (unat i); unat i < n; {p + (i << bits) + word_of_nat (2 ^ bits)..+(n - unat (i + 1)) * 2 ^ bits} \<inter> {p + (i << bits)..+2 ^ bits} = {}\<rbrakk> \<Longrightarrow> Suc 0 \<le> n - unat i \<and> Suc (n - Suc (unat i)) \<le> n - unat i \<and> {p + (i << bits)..+2 ^ bits} \<inter> {p + ((i << bits) + 2 ^ bits)..+(n - Suc (unat i)) * 2 ^ bits} = {} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>range_cover p sz bits n; i < word_of_nat n; bits < 32; unat (1 + i) = Suc (unat i); unat i < n\<rbrakk> \<Longrightarrow> 2 ^ bits + (n - Suc (unat i)) * 2 ^ bits < addr_card
 2. \<lbrakk>range_cover p sz bits n; i < word_of_nat n; bits < 32; unat (1 + i) = Suc (unat i); unat i < n; {p + (i << bits) + word_of_nat (2 ^ bits)..+(n - unat (i + 1)) * 2 ^ bits} \<inter> {p + (i << bits)..+2 ^ bits} = {}\<rbrakk> \<Longrightarrow> Suc 0 \<le> n - unat i \<and> Suc (n - Suc (unat i)) \<le> n - unat i \<and> {p + (i << bits)..+2 ^ bits} \<inter> {p + ((i << bits) + 2 ^ bits)..+(n - Suc (unat i)) * 2 ^ bits} = {} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>i < word_of_nat n; bits < 32; unat (1 + i) = Suc (unat i); unat i < n; n * 2 ^ bits < 2 ^ word_bits\<rbrakk> \<Longrightarrow> 2 ^ bits + (n - Suc (unat i)) * 2 ^ bits < addr_card
 2. \<lbrakk>range_cover p sz bits n; i < word_of_nat n; bits < 32; unat (1 + i) = Suc (unat i); unat i < n; {p + (i << bits) + word_of_nat (2 ^ bits)..+(n - unat (i + 1)) * 2 ^ bits} \<inter> {p + (i << bits)..+2 ^ bits} = {}\<rbrakk> \<Longrightarrow> Suc 0 \<le> n - unat i \<and> Suc (n - Suc (unat i)) \<le> n - unat i \<and> {p + (i << bits)..+2 ^ bits} \<inter> {p + ((i << bits) + 2 ^ bits)..+(n - Suc (unat i)) * 2 ^ bits} = {} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>i < word_of_nat n; bits < 32; unat (1 + i) = Suc (unat i); unat i < n; n * 2 ^ bits < 4294967296\<rbrakk> \<Longrightarrow> 2 ^ bits + (n - Suc (unat i)) * 2 ^ bits < 4294967296
 2. \<lbrakk>range_cover p sz bits n; i < word_of_nat n; bits < 32; unat (1 + i) = Suc (unat i); unat i < n; {p + (i << bits) + word_of_nat (2 ^ bits)..+(n - unat (i + 1)) * 2 ^ bits} \<inter> {p + (i << bits)..+2 ^ bits} = {}\<rbrakk> \<Longrightarrow> Suc 0 \<le> n - unat i \<and> Suc (n - Suc (unat i)) \<le> n - unat i \<and> {p + (i << bits)..+2 ^ bits} \<inter> {p + ((i << bits) + 2 ^ bits)..+(n - Suc (unat i)) * 2 ^ bits} = {} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>i < word_of_nat n; bits < 32; unat (1 + i) = Suc (unat i); unat i < n\<rbrakk> \<Longrightarrow> 2 ^ bits + (n - Suc (unat i)) * 2 ^ bits \<le> n * 2 ^ bits
 2. \<lbrakk>range_cover p sz bits n; i < word_of_nat n; bits < 32; unat (1 + i) = Suc (unat i); unat i < n; {p + (i << bits) + word_of_nat (2 ^ bits)..+(n - unat (i + 1)) * 2 ^ bits} \<inter> {p + (i << bits)..+2 ^ bits} = {}\<rbrakk> \<Longrightarrow> Suc 0 \<le> n - unat i \<and> Suc (n - Suc (unat i)) \<le> n - unat i \<and> {p + (i << bits)..+2 ^ bits} \<inter> {p + ((i << bits) + 2 ^ bits)..+(n - Suc (unat i)) * 2 ^ bits} = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover p sz bits n; i < word_of_nat n; bits < 32; unat (1 + i) = Suc (unat i); unat i < n; {p + (i << bits) + word_of_nat (2 ^ bits)..+(n - unat (i + 1)) * 2 ^ bits} \<inter> {p + (i << bits)..+2 ^ bits} = {}\<rbrakk> \<Longrightarrow> Suc 0 \<le> n - unat i \<and> Suc (n - Suc (unat i)) \<le> n - unat i \<and> {p + (i << bits)..+2 ^ bits} \<inter> {p + ((i << bits) + 2 ^ bits)..+(n - Suc (unat i)) * 2 ^ bits} = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover p sz bits n; i < word_of_nat n; bits < 32; unat (1 + i) = Suc (unat i); unat i < n; {p + (i << bits)..+2 ^ bits} \<inter> {p + ((i << bits) + 2 ^ bits)..+(n - Suc (unat i)) * 2 ^ bits} = {}\<rbrakk> \<Longrightarrow> Suc 0 \<le> n - unat i \<and> Suc (n - Suc (unat i)) \<le> n - unat i proof (prove)
goal:
No subgoals!