theory Word_Lemmas_Internal

lemma shift_distinct_helper:
  "\<lbrakk> (x :: 'a :: len word) < bnd; y < bnd; x \<noteq> y; x << n = y << n; n < LENGTH('a);
     bnd - 1 \<le> 2 ^ (LENGTH('a) - n) - 1 \<rbrakk>
   \<Longrightarrow> P" apply (cases "n = 0") apply simp apply (drule word_plus_mono_right[where x=1]) apply simp_all apply (subst word_le_sub1) apply (rule power_not_zero) apply simp apply simp apply (drule(1) order_less_le_trans)+ apply (clarsimp simp: bang_eq) apply (drule_tac x="na + n" in spec) apply (simp add: nth_shiftl) apply (case_tac "na + n < LENGTH('a)", simp_all) apply safe apply (drule(1) nth_bounded) apply simp apply simp apply (drule(1) nth_bounded) apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x < bnd; y < bnd; x \<noteq> y; x << n = y << n; n < LENGTH('a); bnd - 1 \<le> 2 ^ (LENGTH('a) - n) - 1\<rbrakk> \<Longrightarrow> P proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x < bnd; y < bnd; x \<noteq> y; x << n = y << n; n < LENGTH('a); bnd - 1 \<le> 2 ^ (LENGTH('a) - n) - 1; n = 0\<rbrakk> \<Longrightarrow> P
 2. \<lbrakk>x < bnd; y < bnd; x \<noteq> y; x << n = y << n; n < LENGTH('a); bnd - 1 \<le> 2 ^ (LENGTH('a) - n) - 1; n \<noteq> 0\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x < bnd; y < bnd; x \<noteq> y; x << n = y << n; n < LENGTH('a); bnd - 1 \<le> 2 ^ (LENGTH('a) - n) - 1; n \<noteq> 0\<rbrakk> \<Longrightarrow> P proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x < bnd; y < bnd; x \<noteq> y; x << n = y << n; n < LENGTH('a); n \<noteq> 0\<rbrakk> \<Longrightarrow> 1 \<le> 1 + (2 ^ (LENGTH('a) - n) - 1)
 2. \<lbrakk>x < bnd; y < bnd; x \<noteq> y; x << n = y << n; n < LENGTH('a); n \<noteq> 0; 1 + (bnd - 1) \<le> 1 + (2 ^ (LENGTH('a) - n) - 1)\<rbrakk> \<Longrightarrow> P proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x < bnd; y < bnd; x \<noteq> y; x << n = y << n; n < LENGTH('a); 0 < n\<rbrakk> \<Longrightarrow> 1 \<le> 2 ^ (LENGTH('a) - n)
 2. \<lbrakk>x < bnd; y < bnd; x \<noteq> y; x << n = y << n; n < LENGTH('a); 0 < n; bnd \<le> 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> P proof (prove)
goal (3 subgoals):
 1. \<lbrakk>x < bnd; y < bnd; x \<noteq> y; x << n = y << n; n < LENGTH('a); 0 < n\<rbrakk> \<Longrightarrow> 2 ^ (LENGTH('a) - n) \<noteq> 0
 2. \<lbrakk>x < bnd; y < bnd; x \<noteq> y; x << n = y << n; n < LENGTH('a); 0 < n\<rbrakk> \<Longrightarrow> 0 \<le> 2 ^ (LENGTH('a) - n) - 1
 3. \<lbrakk>x < bnd; y < bnd; x \<noteq> y; x << n = y << n; n < LENGTH('a); 0 < n; bnd \<le> 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> P proof (prove)
goal (3 subgoals):
 1. \<lbrakk>x < bnd; y < bnd; x \<noteq> y; x << n = y << n; n < LENGTH('a); 0 < n\<rbrakk> \<Longrightarrow> LENGTH('a) - n < LENGTH('a)
 2. \<lbrakk>x < bnd; y < bnd; x \<noteq> y; x << n = y << n; n < LENGTH('a); 0 < n\<rbrakk> \<Longrightarrow> 0 \<le> 2 ^ (LENGTH('a) - n) - 1
 3. \<lbrakk>x < bnd; y < bnd; x \<noteq> y; x << n = y << n; n < LENGTH('a); 0 < n; bnd \<le> 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> P proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x < bnd; y < bnd; x \<noteq> y; x << n = y << n; n < LENGTH('a); 0 < n\<rbrakk> \<Longrightarrow> 0 \<le> 2 ^ (LENGTH('a) - n) - 1
 2. \<lbrakk>x < bnd; y < bnd; x \<noteq> y; x << n = y << n; n < LENGTH('a); 0 < n; bnd \<le> 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x < bnd; y < bnd; x \<noteq> y; x << n = y << n; n < LENGTH('a); 0 < n; bnd \<le> 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<noteq> y; x << n = y << n; n < LENGTH('a); 0 < n; bnd \<le> 2 ^ (LENGTH('a) - n); x < 2 ^ (LENGTH('a) - n); y < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>\<forall>na. (n \<le> na \<and> na < LENGTH('a) \<and> x !! (na - n)) = (n \<le> na \<and> na < LENGTH('a) \<and> y !! (na - n)); n < LENGTH('a); 0 < n; bnd \<le> 2 ^ (LENGTH('a) - n); x < 2 ^ (LENGTH('a) - n); y < 2 ^ (LENGTH('a) - n); x !! na = (\<not> y !! na)\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>n < LENGTH('a); 0 < n; bnd \<le> 2 ^ (LENGTH('a) - n); x < 2 ^ (LENGTH('a) - n); y < 2 ^ (LENGTH('a) - n); x !! na = (\<not> y !! na); (n \<le> na + n \<and> na + n < LENGTH('a) \<and> x !! (na + n - n)) = (n \<le> na + n \<and> na + n < LENGTH('a) \<and> y !! (na + n - n))\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>n < LENGTH('a); 0 < n; bnd \<le> 2 ^ (LENGTH('a) - n); x < 2 ^ (LENGTH('a) - n); y < 2 ^ (LENGTH('a) - n); x !! na = (\<not> y !! na); (na + n < LENGTH('a) \<and> \<not> y !! na) = (na + n < LENGTH('a) \<and> y !! na)\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>n < LENGTH('a); 0 < n; bnd \<le> 2 ^ (LENGTH('a) - n); x < 2 ^ (LENGTH('a) - n); y < 2 ^ (LENGTH('a) - n); x !! na = (\<not> y !! na); \<not> na + n < LENGTH('a)\<rbrakk> \<Longrightarrow> P proof (prove)
goal (2 subgoals):
 1. \<And>na. \<lbrakk>n < LENGTH('a); 0 < n; bnd \<le> 2 ^ (LENGTH('a) - n); x < 2 ^ (LENGTH('a) - n); y < 2 ^ (LENGTH('a) - n); \<not> na + n < LENGTH('a); x !! na; \<not> y !! na\<rbrakk> \<Longrightarrow> P
 2. \<And>na. \<lbrakk>n < LENGTH('a); 0 < n; bnd \<le> 2 ^ (LENGTH('a) - n); x < 2 ^ (LENGTH('a) - n); y < 2 ^ (LENGTH('a) - n); \<not> na + n < LENGTH('a); \<not> x !! na; \<not> P; y !! na\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>na. \<lbrakk>n < LENGTH('a); 0 < n; bnd \<le> 2 ^ (LENGTH('a) - n); x < 2 ^ (LENGTH('a) - n); y < 2 ^ (LENGTH('a) - n); \<not> na + n < LENGTH('a); \<not> y !! na\<rbrakk> \<Longrightarrow> LENGTH('a) - n \<le> LENGTH('a)
 2. \<And>na. \<lbrakk>n < LENGTH('a); 0 < n; bnd \<le> 2 ^ (LENGTH('a) - n); x < 2 ^ (LENGTH('a) - n); y < 2 ^ (LENGTH('a) - n); \<not> na + n < LENGTH('a); \<not> y !! na; na < LENGTH('a) - n\<rbrakk> \<Longrightarrow> P
 3. \<And>na. \<lbrakk>n < LENGTH('a); 0 < n; bnd \<le> 2 ^ (LENGTH('a) - n); x < 2 ^ (LENGTH('a) - n); y < 2 ^ (LENGTH('a) - n); \<not> na + n < LENGTH('a); \<not> x !! na; \<not> P; y !! na\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>na. \<lbrakk>n < LENGTH('a); 0 < n; bnd \<le> 2 ^ (LENGTH('a) - n); x < 2 ^ (LENGTH('a) - n); y < 2 ^ (LENGTH('a) - n); \<not> na + n < LENGTH('a); \<not> y !! na; na < LENGTH('a) - n\<rbrakk> \<Longrightarrow> P
 2. \<And>na. \<lbrakk>n < LENGTH('a); 0 < n; bnd \<le> 2 ^ (LENGTH('a) - n); x < 2 ^ (LENGTH('a) - n); y < 2 ^ (LENGTH('a) - n); \<not> na + n < LENGTH('a); \<not> x !! na; \<not> P; y !! na\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>n < LENGTH('a); 0 < n; bnd \<le> 2 ^ (LENGTH('a) - n); x < 2 ^ (LENGTH('a) - n); y < 2 ^ (LENGTH('a) - n); \<not> na + n < LENGTH('a); \<not> x !! na; \<not> P; y !! na\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>na. \<lbrakk>n < LENGTH('a); 0 < n; bnd \<le> 2 ^ (LENGTH('a) - n); x < 2 ^ (LENGTH('a) - n); y < 2 ^ (LENGTH('a) - n); \<not> na + n < LENGTH('a); \<not> x !! na; \<not> P\<rbrakk> \<Longrightarrow> LENGTH('a) - n \<le> LENGTH('a)
 2. \<And>na. \<lbrakk>n < LENGTH('a); 0 < n; bnd \<le> 2 ^ (LENGTH('a) - n); x < 2 ^ (LENGTH('a) - n); y < 2 ^ (LENGTH('a) - n); \<not> na + n < LENGTH('a); \<not> x !! na; \<not> P; na < LENGTH('a) - n\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>n < LENGTH('a); 0 < n; bnd \<le> 2 ^ (LENGTH('a) - n); x < 2 ^ (LENGTH('a) - n); y < 2 ^ (LENGTH('a) - n); \<not> na + n < LENGTH('a); \<not> x !! na; \<not> P; na < LENGTH('a) - n\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!