theory Retype_C

lemma offset_intvl_first_chunk_subsets_unat:
  "range_cover (p :: addr) sz bits n
    \<Longrightarrow> unat n' = n
    \<Longrightarrow> i < of_nat n
    \<Longrightarrow> {p + (i << bits) ..+ 2 ^ bits} \<subseteq> {p + (i << bits) ..+ unat (n' - i) * 2 ^ bits}
        \<and> {p + ((i + 1) << bits) ..+ unat (n' - (i + 1)) * 2 ^ bits}
            \<le> {p + (i << bits) ..+ unat (n' - i) * 2 ^ bits}
        \<and> {p + (i << bits) ..+ 2 ^ bits}
            \<inter> {p + ((i + 1) << bits) ..+ unat (n' - (i + 1)) * 2 ^ bits}
            = {}" apply (subgoal_tac "unat (n' - (i + 1)) = unat n' - unat (i + 1)
        \<and> unat (n' - i) = unat n' - unat i") apply (frule(1) offset_intvl_first_chunk_subsets) apply simp apply (intro conjI unat_sub) apply (rule word_minus_one_le_leq, simp) apply (simp add: word_less_nat_alt unat_of_nat) apply (simp add: word_le_nat_alt word_less_nat_alt unat_of_nat) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover p sz bits n; unat n' = n; i < word_of_nat n\<rbrakk> \<Longrightarrow> {p + (i << bits)..+2 ^ bits} \<subseteq> {p + (i << bits)..+unat (n' - i) * 2 ^ bits} \<and> {p + (i + 1 << bits)..+unat (n' - (i + 1)) * 2 ^ bits} \<subseteq> {p + (i << bits)..+unat (n' - i) * 2 ^ bits} \<and> {p + (i << bits)..+2 ^ bits} \<inter> {p + (i + 1 << bits)..+unat (n' - (i + 1)) * 2 ^ bits} = {} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>range_cover p sz bits n; unat n' = n; i < word_of_nat n; unat (n' - (i + 1)) = unat n' - unat (i + 1) \<and> unat (n' - i) = unat n' - unat i\<rbrakk> \<Longrightarrow> {p + (i << bits)..+2 ^ bits} \<subseteq> {p + (i << bits)..+unat (n' - i) * 2 ^ bits} \<and> {p + (i + 1 << bits)..+unat (n' - (i + 1)) * 2 ^ bits} \<subseteq> {p + (i << bits)..+unat (n' - i) * 2 ^ bits} \<and> {p + (i << bits)..+2 ^ bits} \<inter> {p + (i + 1 << bits)..+unat (n' - (i + 1)) * 2 ^ bits} = {}
 2. \<lbrakk>range_cover p sz bits n; unat n' = n; i < word_of_nat n\<rbrakk> \<Longrightarrow> unat (n' - (i + 1)) = unat n' - unat (i + 1) \<and> unat (n' - i) = unat n' - unat i proof (prove)
goal (2 subgoals):
 1. \<lbrakk>range_cover p sz bits n; unat n' = n; i < word_of_nat n; unat (n' - (i + 1)) = unat n' - unat (i + 1) \<and> unat (n' - i) = unat n' - unat i; {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} = {}\<rbrakk> \<Longrightarrow> {p + (i << bits)..+2 ^ bits} \<subseteq> {p + (i << bits)..+unat (n' - i) * 2 ^ bits} \<and> {p + (i + 1 << bits)..+unat (n' - (i + 1)) * 2 ^ bits} \<subseteq> {p + (i << bits)..+unat (n' - i) * 2 ^ bits} \<and> {p + (i << bits)..+2 ^ bits} \<inter> {p + (i + 1 << bits)..+unat (n' - (i + 1)) * 2 ^ bits} = {}
 2. \<lbrakk>range_cover p sz bits n; unat n' = n; i < word_of_nat n\<rbrakk> \<Longrightarrow> unat (n' - (i + 1)) = unat n' - unat (i + 1) \<and> unat (n' - i) = unat n' - unat i proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover p sz bits n; unat n' = n; i < word_of_nat n\<rbrakk> \<Longrightarrow> unat (n' - (i + 1)) = unat n' - unat (i + 1) \<and> unat (n' - i) = unat n' - unat i proof (prove)
goal (2 subgoals):
 1. \<lbrakk>range_cover p sz bits n; unat n' = n; i < word_of_nat n\<rbrakk> \<Longrightarrow> i + 1 \<le> n'
 2. \<lbrakk>range_cover p sz bits n; unat n' = n; i < word_of_nat n\<rbrakk> \<Longrightarrow> i \<le> n' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>range_cover p sz bits n; unat n' = n; i < word_of_nat n\<rbrakk> \<Longrightarrow> i < n'
 2. \<lbrakk>range_cover p sz bits n; unat n' = n; i < word_of_nat n\<rbrakk> \<Longrightarrow> i \<le> n' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover p sz bits n; unat n' = n; i < word_of_nat n\<rbrakk> \<Longrightarrow> i \<le> n' proof (prove)
goal:
No subgoals!