theory Word_Lemmas_Internal

lemma word_ctz_bound_above:
  fixes x :: "'a::len word"
  shows "x && mask n \<noteq> 0 \<Longrightarrow> word_ctz x < n" apply (cases "n \<le> LENGTH('a)") apply (frule mask_to_bl_exists_True, clarsimp) apply (clarsimp simp: word_ctz_def) apply (subgoal_tac "m < length ((rev (to_bl x)))") apply (subst id_take_nth_drop[where xs="rev (to_bl x)"], assumption) apply (subst takeWhile_tail, simp) apply (rule order.strict_trans1) apply (rule List.length_takeWhile_le) apply simp apply (erule order.strict_trans2, clarsimp) apply (simp add: not_le) apply (erule le_less_trans[OF word_ctz_max, simplified word_size]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x && mask n \<noteq> 0 \<Longrightarrow> word_ctz x < n proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x && mask n \<noteq> 0; n \<le> LENGTH('a)\<rbrakk> \<Longrightarrow> word_ctz x < n
 2. \<lbrakk>x && mask n \<noteq> 0; \<not> n \<le> LENGTH('a)\<rbrakk> \<Longrightarrow> word_ctz x < n proof (prove)
goal (2 subgoals):
 1. \<And>m. \<lbrakk>x && mask n \<noteq> 0; n \<le> LENGTH('a); rev (to_bl x) ! m; m < n\<rbrakk> \<Longrightarrow> word_ctz x < n
 2. \<lbrakk>x && mask n \<noteq> 0; \<not> n \<le> LENGTH('a)\<rbrakk> \<Longrightarrow> word_ctz x < n proof (prove)
goal (2 subgoals):
 1. \<And>m. \<lbrakk>x && mask n \<noteq> 0; n \<le> LENGTH('a); rev (to_bl x) ! m; m < n\<rbrakk> \<Longrightarrow> length (takeWhile Not (rev (to_bl x))) < n
 2. \<lbrakk>x && mask n \<noteq> 0; \<not> n \<le> LENGTH('a)\<rbrakk> \<Longrightarrow> word_ctz x < n proof (prove)
goal (3 subgoals):
 1. \<And>m. \<lbrakk>x && mask n \<noteq> 0; n \<le> LENGTH('a); rev (to_bl x) ! m; m < n; m < length (rev (to_bl x))\<rbrakk> \<Longrightarrow> length (takeWhile Not (rev (to_bl x))) < n
 2. \<And>m. \<lbrakk>x && mask n \<noteq> 0; n \<le> LENGTH('a); rev (to_bl x) ! m; m < n\<rbrakk> \<Longrightarrow> m < length (rev (to_bl x))
 3. \<lbrakk>x && mask n \<noteq> 0; \<not> n \<le> LENGTH('a)\<rbrakk> \<Longrightarrow> word_ctz x < n proof (prove)
goal (3 subgoals):
 1. \<And>m. \<lbrakk>x && mask n \<noteq> 0; n \<le> LENGTH('a); rev (to_bl x) ! m; m < n; m < length (rev (to_bl x))\<rbrakk> \<Longrightarrow> length (takeWhile Not (take m (rev (to_bl x)) @ rev (to_bl x) ! m # drop (Suc m) (rev (to_bl x)))) < n
 2. \<And>m. \<lbrakk>x && mask n \<noteq> 0; n \<le> LENGTH('a); rev (to_bl x) ! m; m < n\<rbrakk> \<Longrightarrow> m < length (rev (to_bl x))
 3. \<lbrakk>x && mask n \<noteq> 0; \<not> n \<le> LENGTH('a)\<rbrakk> \<Longrightarrow> word_ctz x < n proof (prove)
goal (3 subgoals):
 1. \<And>m. \<lbrakk>x && mask n \<noteq> 0; n \<le> LENGTH('a); rev (to_bl x) ! m; m < n; m < length (rev (to_bl x))\<rbrakk> \<Longrightarrow> length (takeWhile Not (take m (rev (to_bl x)))) < n
 2. \<And>m. \<lbrakk>x && mask n \<noteq> 0; n \<le> LENGTH('a); rev (to_bl x) ! m; m < n\<rbrakk> \<Longrightarrow> m < length (rev (to_bl x))
 3. \<lbrakk>x && mask n \<noteq> 0; \<not> n \<le> LENGTH('a)\<rbrakk> \<Longrightarrow> word_ctz x < n proof (prove)
goal (4 subgoals):
 1. \<And>m. \<lbrakk>x && mask n \<noteq> 0; n \<le> LENGTH('a); rev (to_bl x) ! m; m < n; m < length (rev (to_bl x))\<rbrakk> \<Longrightarrow> length (takeWhile Not (take m (rev (to_bl x)))) \<le> ?b16 m
 2. \<And>m. \<lbrakk>x && mask n \<noteq> 0; n \<le> LENGTH('a); rev (to_bl x) ! m; m < n; m < length (rev (to_bl x))\<rbrakk> \<Longrightarrow> ?b16 m < n
 3. \<And>m. \<lbrakk>x && mask n \<noteq> 0; n \<le> LENGTH('a); rev (to_bl x) ! m; m < n\<rbrakk> \<Longrightarrow> m < length (rev (to_bl x))
 4. \<lbrakk>x && mask n \<noteq> 0; \<not> n \<le> LENGTH('a)\<rbrakk> \<Longrightarrow> word_ctz x < n proof (prove)
goal (3 subgoals):
 1. \<And>m. \<lbrakk>x && mask n \<noteq> 0; n \<le> LENGTH('a); rev (to_bl x) ! m; m < n; m < length (rev (to_bl x))\<rbrakk> \<Longrightarrow> length (take m (rev (to_bl x))) < n
 2. \<And>m. \<lbrakk>x && mask n \<noteq> 0; n \<le> LENGTH('a); rev (to_bl x) ! m; m < n\<rbrakk> \<Longrightarrow> m < length (rev (to_bl x))
 3. \<lbrakk>x && mask n \<noteq> 0; \<not> n \<le> LENGTH('a)\<rbrakk> \<Longrightarrow> word_ctz x < n proof (prove)
goal (2 subgoals):
 1. \<And>m. \<lbrakk>x && mask n \<noteq> 0; n \<le> LENGTH('a); rev (to_bl x) ! m; m < n\<rbrakk> \<Longrightarrow> m < length (rev (to_bl x))
 2. \<lbrakk>x && mask n \<noteq> 0; \<not> n \<le> LENGTH('a)\<rbrakk> \<Longrightarrow> word_ctz x < n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x && mask n \<noteq> 0; \<not> n \<le> LENGTH('a)\<rbrakk> \<Longrightarrow> word_ctz x < n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x && mask n \<noteq> 0; LENGTH('a) < n\<rbrakk> \<Longrightarrow> word_ctz x < n proof (prove)
goal:
No subgoals!