theory More_Word_Operations

lemma sint_ctz:
  \<open>0 \<le> sint (of_nat (word_ctz (x :: 'a :: len word)) :: 'a signed word)
     \<and> sint (of_nat (word_ctz x) :: 'a signed word) \<le> int (LENGTH('a))\<close> (is \<open>?P \<and> ?Q\<close>)
  if \<open>LENGTH('a) > 2\<close> proof have *: \<open>word_ctz x < 2 ^ (LENGTH('a) - Suc 0)\<close> using word_ctz_le apply (rule le_less_trans) using that small_powers_of_2 [of \<open>LENGTH('a)\<close>] apply simp done have \<open>int (word_ctz x) div 2 ^ (LENGTH('a) - Suc 0) = 0\<close> apply (rule div_pos_pos_trivial) apply (simp_all add: *) done then show ?P by (simp add: signed_of_nat bit_iff_odd) show ?Q apply (auto simp add: signed_of_nat) apply (subst signed_take_bit_int_eq_self) apply (auto simp add: word_ctz_le * minus_le_iff [of _ \<open>int (word_ctz x)\<close>]) apply (rule order.trans [of _ 0]) apply simp_all done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 0 \<le> sint (word_of_nat (word_ctz x)) \<and> sint (word_of_nat (word_ctz x)) \<le> int LENGTH('a) proof (state)
goal (2 subgoals):
 1. 0 \<le> sint (word_of_nat (word_ctz x))
 2. sint (word_of_nat (word_ctz x)) \<le> int LENGTH('a) proof (prove)
goal (1 subgoal):
 1. word_ctz x < 2 ^ (LENGTH('a) - Suc 0) proof (prove)
using this:
word_ctz ?w \<le> LENGTH(?'a)

goal (1 subgoal):
 1. word_ctz x < 2 ^ (LENGTH('a) - Suc 0) proof (prove)
goal (1 subgoal):
 1. LENGTH('a) < 2 ^ (LENGTH('a) - Suc 0) proof (prove)
using this:
2 < LENGTH('a)
3 \<le> LENGTH('a) \<Longrightarrow> LENGTH('a) < 2 ^ (LENGTH('a) - 1)

goal (1 subgoal):
 1. LENGTH('a) < 2 ^ (LENGTH('a) - Suc 0) proof (prove)
goal:
No subgoals! proof (state)
this:
word_ctz x < 2 ^ (LENGTH('a) - Suc 0)

goal (2 subgoals):
 1. 0 \<le> sint (word_of_nat (word_ctz x))
 2. sint (word_of_nat (word_ctz x)) \<le> int LENGTH('a) proof (prove)
goal (1 subgoal):
 1. int (word_ctz x) div 2 ^ (LENGTH('a) - Suc 0) = 0 proof (prove)
goal (2 subgoals):
 1. 0 \<le> int (word_ctz x)
 2. int (word_ctz x) < 2 ^ (LENGTH('a) - Suc 0) proof (prove)
goal:
No subgoals! proof (state)
this:
int (word_ctz x) div 2 ^ (LENGTH('a) - Suc 0) = 0

goal (2 subgoals):
 1. 0 \<le> sint (word_of_nat (word_ctz x))
 2. sint (word_of_nat (word_ctz x)) \<le> int LENGTH('a) proof (chain)
picking this:
int (word_ctz x) div 2 ^ (LENGTH('a) - Suc 0) = 0 proof (prove)
using this:
int (word_ctz x) div 2 ^ (LENGTH('a) - Suc 0) = 0

goal (1 subgoal):
 1. 0 \<le> sint (word_of_nat (word_ctz x)) proof (state)
this:
0 \<le> sint (word_of_nat (word_ctz x))

goal (1 subgoal):
 1. sint (word_of_nat (word_ctz x)) \<le> int LENGTH('a) proof (prove)
goal (1 subgoal):
 1. sint (word_of_nat (word_ctz x)) \<le> int LENGTH('a) proof (prove)
goal (1 subgoal):
 1. signed_take_bit (LENGTH('a) - Suc 0) (int (word_ctz x)) \<le> int LENGTH('a) proof (prove)
goal (3 subgoals):
 1. - (2 ^ (LENGTH('a) - Suc 0)) \<le> int (word_ctz x)
 2. int (word_ctz x) < 2 ^ (LENGTH('a) - Suc 0)
 3. int (word_ctz x) \<le> int LENGTH('a) proof (prove)
goal (1 subgoal):
 1. - int (word_ctz x) \<le> 2 ^ (LENGTH('a) - Suc 0) proof (prove)
goal (2 subgoals):
 1. - int (word_ctz x) \<le> 0
 2. 0 \<le> 2 ^ (LENGTH('a) - Suc 0) proof (prove)
goal:
No subgoals! proof (state)
this:
sint (word_of_nat (word_ctz x)) \<le> int LENGTH('a)

goal:
No subgoals!