theory Recycle_C

lemma intvl_2_power_times_decomp:
  "\<forall>y < 2 ^ (n - m). {x + y * 2 ^ m ..+ 2 ^ m} \<times> S \<subseteq> T
    \<Longrightarrow> m \<le> n \<Longrightarrow> n < word_bits
    \<Longrightarrow> {(x :: word32) ..+ 2 ^ n} \<times> S \<subseteq> T" apply (clarsimp simp: intvl_def) apply (drule_tac x="of_nat k >> m" in spec) apply (drule mp) apply (rule shiftr_less_t2n) apply (rule word_of_nat_less) apply (simp add: word_of_nat_less) apply (erule subsetD) apply (clarsimp simp: shiftl_t2n[simplified mult.commute mult.left_commute, symmetric]
                        shiftr_shiftl1) apply (rule_tac x="unat (of_nat k && mask m :: word32)" in exI) apply (simp add: field_simps word_plus_and_or_coroll2) apply (simp add: word_bits_def unat_less_power and_mask_less') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>y<2 ^ (n - m). {x + y * 2 ^ m..+2 ^ m} \<times> S \<subseteq> T; m \<le> n; n < word_bits\<rbrakk> \<Longrightarrow> {x..+2 ^ n} \<times> S \<subseteq> T proof (prove)
goal (1 subgoal):
 1. \<And>b k. \<lbrakk>\<forall>y<2 ^ (n - m). {x + y * 2 ^ m + word_of_nat k |k. k < 2 ^ m} \<times> S \<subseteq> T; m \<le> n; n < word_bits; b \<in> S; k < 2 ^ n\<rbrakk> \<Longrightarrow> (x + word_of_nat k, b) \<in> T proof (prove)
goal (1 subgoal):
 1. \<And>b k. \<lbrakk>m \<le> n; n < word_bits; b \<in> S; k < 2 ^ n; word_of_nat k >> m < 2 ^ (n - m) \<longrightarrow> {x + (word_of_nat k >> m) * 2 ^ m + word_of_nat ka |ka. ka < 2 ^ m} \<times> S \<subseteq> T\<rbrakk> \<Longrightarrow> (x + word_of_nat k, b) \<in> T proof (prove)
goal (2 subgoals):
 1. \<And>b k. \<lbrakk>m \<le> n; n < word_bits; b \<in> S; k < 2 ^ n\<rbrakk> \<Longrightarrow> word_of_nat k >> m < 2 ^ (n - m)
 2. \<And>b k. \<lbrakk>m \<le> n; n < word_bits; b \<in> S; k < 2 ^ n; {x + (word_of_nat k >> m) * 2 ^ m + word_of_nat ka |ka. ka < 2 ^ m} \<times> S \<subseteq> T\<rbrakk> \<Longrightarrow> (x + word_of_nat k, b) \<in> T proof (prove)
goal (2 subgoals):
 1. \<And>b k. \<lbrakk>m \<le> n; n < word_bits; b \<in> S; k < 2 ^ n\<rbrakk> \<Longrightarrow> word_of_nat k < 2 ^ (m + (n - m))
 2. \<And>b k. \<lbrakk>m \<le> n; n < word_bits; b \<in> S; k < 2 ^ n; {x + (word_of_nat k >> m) * 2 ^ m + word_of_nat ka |ka. ka < 2 ^ m} \<times> S \<subseteq> T\<rbrakk> \<Longrightarrow> (x + word_of_nat k, b) \<in> T proof (prove)
goal (2 subgoals):
 1. \<And>b k. \<lbrakk>m \<le> n; n < word_bits; b \<in> S; k < 2 ^ n\<rbrakk> \<Longrightarrow> k < unat (2 ^ (m + (n - m)))
 2. \<And>b k. \<lbrakk>m \<le> n; n < word_bits; b \<in> S; k < 2 ^ n; {x + (word_of_nat k >> m) * 2 ^ m + word_of_nat ka |ka. ka < 2 ^ m} \<times> S \<subseteq> T\<rbrakk> \<Longrightarrow> (x + word_of_nat k, b) \<in> T proof (prove)
goal (1 subgoal):
 1. \<And>b k. \<lbrakk>m \<le> n; n < word_bits; b \<in> S; k < 2 ^ n; {x + (word_of_nat k >> m) * 2 ^ m + word_of_nat ka |ka. ka < 2 ^ m} \<times> S \<subseteq> T\<rbrakk> \<Longrightarrow> (x + word_of_nat k, b) \<in> T proof (prove)
goal (1 subgoal):
 1. \<And>b k. \<lbrakk>m \<le> n; n < word_bits; b \<in> S; k < 2 ^ n\<rbrakk> \<Longrightarrow> (x + word_of_nat k, b) \<in> {x + (word_of_nat k >> m) * 2 ^ m + word_of_nat ka |ka. ka < 2 ^ m} \<times> S proof (prove)
goal (1 subgoal):
 1. \<And>b k. \<lbrakk>m \<le> n; n < word_bits; b \<in> S; k < 2 ^ n\<rbrakk> \<Longrightarrow> \<exists>ka. word_of_nat k = (word_of_nat k && ~~ mask m) + word_of_nat ka \<and> ka < 2 ^ m proof (prove)
goal (1 subgoal):
 1. \<And>b k. \<lbrakk>m \<le> n; n < word_bits; b \<in> S; k < 2 ^ n\<rbrakk> \<Longrightarrow> word_of_nat k = (word_of_nat k && ~~ mask m) + word_of_nat (unat (word_of_nat k && mask m)) \<and> unat (word_of_nat k && mask m) < 2 ^ m proof (prove)
goal (1 subgoal):
 1. \<And>b k. \<lbrakk>m \<le> n; n < word_bits; b \<in> S; k < 2 ^ n\<rbrakk> \<Longrightarrow> unat (word_of_nat k && mask m) < 2 ^ m proof (prove)
goal:
No subgoals!