theory Word_Lemmas_Internal

lemma of_nat_shift_distinct_helper:
  "\<lbrakk> x < bnd; y < bnd; x \<noteq> y; (of_nat x :: 'a :: len word) << n = of_nat y << n;
     n < LENGTH('a); bnd \<le> 2 ^ (LENGTH('a) - n) \<rbrakk>
   \<Longrightarrow> P" apply (cases "n = 0") apply (simp add: word_unat.Abs_inject unats_def) apply (subgoal_tac "bnd < 2 ^ LENGTH('a)") apply (erule(1) shift_distinct_helper[rotated, rotated, rotated]) defer apply (erule(1) of_nat_mono_maybe[rotated]) apply (erule(1) of_nat_mono_maybe[rotated]) apply (simp add: word_unat.Abs_inject unats_def) apply (erule order_le_less_trans) apply (rule power_strict_increasing) apply simp apply simp apply (fastforce simp: unat_of_nat_minus_1 word_less_nat_alt) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x < bnd; y < bnd; x \<noteq> y; word_of_nat x << n = word_of_nat y << n; n < LENGTH('a); bnd \<le> 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> P proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x < bnd; y < bnd; x \<noteq> y; word_of_nat x << n = word_of_nat y << n; n < LENGTH('a); bnd \<le> 2 ^ (LENGTH('a) - n); n = 0\<rbrakk> \<Longrightarrow> P
 2. \<lbrakk>x < bnd; y < bnd; x \<noteq> y; word_of_nat x << n = word_of_nat y << n; n < LENGTH('a); bnd \<le> 2 ^ (LENGTH('a) - n); n \<noteq> 0\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x < bnd; y < bnd; x \<noteq> y; word_of_nat x << n = word_of_nat y << n; n < LENGTH('a); bnd \<le> 2 ^ (LENGTH('a) - n); n \<noteq> 0\<rbrakk> \<Longrightarrow> P proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x < bnd; y < bnd; x \<noteq> y; word_of_nat x << n = word_of_nat y << n; n < LENGTH('a); bnd \<le> 2 ^ (LENGTH('a) - n); n \<noteq> 0; bnd < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> P
 2. \<lbrakk>x < bnd; y < bnd; x \<noteq> y; word_of_nat x << n = word_of_nat y << n; n < LENGTH('a); bnd \<le> 2 ^ (LENGTH('a) - n); n \<noteq> 0\<rbrakk> \<Longrightarrow> bnd < 2 ^ LENGTH('a) proof (prove)
goal (5 subgoals):
 1. \<lbrakk>x < bnd; y < bnd; x \<noteq> y; n < LENGTH('a); bnd \<le> 2 ^ (LENGTH('a) - n); n \<noteq> 0; bnd < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> ?bnd12 - 1 \<le> 2 ^ (LENGTH('a) - n) - 1
 2. \<lbrakk>x < bnd; y < bnd; x \<noteq> y; n < LENGTH('a); bnd \<le> 2 ^ (LENGTH('a) - n); n \<noteq> 0; bnd < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> word_of_nat x < ?bnd12
 3. \<lbrakk>x < bnd; y < bnd; x \<noteq> y; n < LENGTH('a); bnd \<le> 2 ^ (LENGTH('a) - n); n \<noteq> 0; bnd < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> word_of_nat y < ?bnd12
 4. \<lbrakk>x < bnd; y < bnd; x \<noteq> y; n < LENGTH('a); bnd \<le> 2 ^ (LENGTH('a) - n); n \<noteq> 0; bnd < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> word_of_nat x \<noteq> word_of_nat y
 5. \<lbrakk>x < bnd; y < bnd; x \<noteq> y; word_of_nat x << n = word_of_nat y << n; n < LENGTH('a); bnd \<le> 2 ^ (LENGTH('a) - n); n \<noteq> 0\<rbrakk> \<Longrightarrow> bnd < 2 ^ LENGTH('a) proof (prove)
goal (5 subgoals):
 1. \<lbrakk>x < bnd; y < bnd; x \<noteq> y; n < LENGTH('a); bnd \<le> 2 ^ (LENGTH('a) - n); n \<noteq> 0; bnd < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> word_of_nat x < ?bnd12
 2. \<lbrakk>x < bnd; y < bnd; x \<noteq> y; n < LENGTH('a); bnd \<le> 2 ^ (LENGTH('a) - n); n \<noteq> 0; bnd < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> word_of_nat y < ?bnd12
 3. \<lbrakk>x < bnd; y < bnd; x \<noteq> y; n < LENGTH('a); bnd \<le> 2 ^ (LENGTH('a) - n); n \<noteq> 0; bnd < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> word_of_nat x \<noteq> word_of_nat y
 4. \<lbrakk>x < bnd; y < bnd; x \<noteq> y; word_of_nat x << n = word_of_nat y << n; n < LENGTH('a); bnd \<le> 2 ^ (LENGTH('a) - n); n \<noteq> 0\<rbrakk> \<Longrightarrow> bnd < 2 ^ LENGTH('a)
 5. \<lbrakk>x < bnd; y < bnd; x \<noteq> y; n < LENGTH('a); bnd \<le> 2 ^ (LENGTH('a) - n); n \<noteq> 0; bnd < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> ?bnd12 - 1 \<le> 2 ^ (LENGTH('a) - n) - 1 proof (prove)
goal (4 subgoals):
 1. \<lbrakk>x < bnd; y < bnd; x \<noteq> y; n < LENGTH('a); bnd \<le> 2 ^ (LENGTH('a) - n); n \<noteq> 0; bnd < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> word_of_nat y < word_of_nat bnd
 2. \<lbrakk>x < bnd; y < bnd; x \<noteq> y; n < LENGTH('a); bnd \<le> 2 ^ (LENGTH('a) - n); n \<noteq> 0; bnd < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> word_of_nat x \<noteq> word_of_nat y
 3. \<lbrakk>x < bnd; y < bnd; x \<noteq> y; word_of_nat x << n = word_of_nat y << n; n < LENGTH('a); bnd \<le> 2 ^ (LENGTH('a) - n); n \<noteq> 0\<rbrakk> \<Longrightarrow> bnd < 2 ^ LENGTH('a)
 4. \<lbrakk>x < bnd; y < bnd; x \<noteq> y; n < LENGTH('a); bnd \<le> 2 ^ (LENGTH('a) - n); n \<noteq> 0; bnd < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> word_of_nat bnd - 1 \<le> 2 ^ (LENGTH('a) - n) - 1 proof (prove)
goal (3 subgoals):
 1. \<lbrakk>x < bnd; y < bnd; x \<noteq> y; n < LENGTH('a); bnd \<le> 2 ^ (LENGTH('a) - n); n \<noteq> 0; bnd < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> word_of_nat x \<noteq> word_of_nat y
 2. \<lbrakk>x < bnd; y < bnd; x \<noteq> y; word_of_nat x << n = word_of_nat y << n; n < LENGTH('a); bnd \<le> 2 ^ (LENGTH('a) - n); n \<noteq> 0\<rbrakk> \<Longrightarrow> bnd < 2 ^ LENGTH('a)
 3. \<lbrakk>x < bnd; y < bnd; x \<noteq> y; n < LENGTH('a); bnd \<le> 2 ^ (LENGTH('a) - n); n \<noteq> 0; bnd < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> word_of_nat bnd - 1 \<le> 2 ^ (LENGTH('a) - n) - 1 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x < bnd; y < bnd; x \<noteq> y; word_of_nat x << n = word_of_nat y << n; n < LENGTH('a); bnd \<le> 2 ^ (LENGTH('a) - n); n \<noteq> 0\<rbrakk> \<Longrightarrow> bnd < 2 ^ LENGTH('a)
 2. \<lbrakk>x < bnd; y < bnd; x \<noteq> y; n < LENGTH('a); bnd \<le> 2 ^ (LENGTH('a) - n); n \<noteq> 0; bnd < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> word_of_nat bnd - 1 \<le> 2 ^ (LENGTH('a) - n) - 1 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x < bnd; y < bnd; x \<noteq> y; word_of_nat x << n = word_of_nat y << n; n < LENGTH('a); n \<noteq> 0\<rbrakk> \<Longrightarrow> 2 ^ (LENGTH('a) - n) < 2 ^ LENGTH('a)
 2. \<lbrakk>x < bnd; y < bnd; x \<noteq> y; n < LENGTH('a); bnd \<le> 2 ^ (LENGTH('a) - n); n \<noteq> 0; bnd < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> word_of_nat bnd - 1 \<le> 2 ^ (LENGTH('a) - n) - 1 proof (prove)
goal (3 subgoals):
 1. \<lbrakk>x < bnd; y < bnd; x \<noteq> y; word_of_nat x << n = word_of_nat y << n; n < LENGTH('a); n \<noteq> 0\<rbrakk> \<Longrightarrow> LENGTH('a) - n < LENGTH('a)
 2. \<lbrakk>x < bnd; y < bnd; x \<noteq> y; word_of_nat x << n = word_of_nat y << n; n < LENGTH('a); n \<noteq> 0\<rbrakk> \<Longrightarrow> 1 < 2
 3. \<lbrakk>x < bnd; y < bnd; x \<noteq> y; n < LENGTH('a); bnd \<le> 2 ^ (LENGTH('a) - n); n \<noteq> 0; bnd < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> word_of_nat bnd - 1 \<le> 2 ^ (LENGTH('a) - n) - 1 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x < bnd; y < bnd; x \<noteq> y; word_of_nat x << n = word_of_nat y << n; n < LENGTH('a); n \<noteq> 0\<rbrakk> \<Longrightarrow> 1 < 2
 2. \<lbrakk>x < bnd; y < bnd; x \<noteq> y; n < LENGTH('a); bnd \<le> 2 ^ (LENGTH('a) - n); n \<noteq> 0; bnd < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> word_of_nat bnd - 1 \<le> 2 ^ (LENGTH('a) - n) - 1 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x < bnd; y < bnd; x \<noteq> y; n < LENGTH('a); bnd \<le> 2 ^ (LENGTH('a) - n); n \<noteq> 0; bnd < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> word_of_nat bnd - 1 \<le> 2 ^ (LENGTH('a) - n) - 1 proof (prove)
goal:
No subgoals!