theory Bits_Int

lemma signed_mult_eq_checks_double_size:
  assumes mult_le: "(2 ^ (len_of TYPE ('a) - 1) + 1) ^ 2 \<le> (2 :: int) ^ (len_of TYPE ('b) - 1)"
           and le: "2 ^ (LENGTH('a) - 1) \<le> (2 :: int) ^ (len_of TYPE ('b) - 1)"
  shows "(sint (a :: 'a :: len word) * sint b = sint (a * b))
       = (scast a * scast b = (scast (a * b) :: 'b :: len word))" proof - have P: "(signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (size a - 1) (sint a * sint b) \<in> range ((signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (size a - 1))" by simp have abs: "!! x :: 'a word. abs (sint x) < 2 ^ (size a - 1) + 1" apply (cut_tac x=x in sint_range') apply (simp add: abs_le_iff word_size) done have abs_ab: "abs (sint a * sint b) < 2 ^ (LENGTH('b) - 1)" using abs_mult_less[OF abs[where x=a] abs[where x=b]] mult_le by (simp add: abs_mult power2_eq_square word_size) define r s where \<open>r = LENGTH('a) - 1\<close> \<open>s = LENGTH('b) - 1\<close> then have \<open>LENGTH('a) = Suc r\<close> \<open>LENGTH('b) = Suc s\<close>
    \<open>size a = Suc r\<close> \<open>size b = Suc r\<close> by (simp_all add: word_size) then show ?thesis using P[unfolded range_sbintrunc] abs_ab le apply clarsimp apply (transfer fixing: r s) apply (auto simp add: signed_take_bit_int_eq_self simp flip: signed_take_bit_eq_iff_take_bit_eq) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (sint a * sint b = sint (a * b)) = (scast a * scast b = scast (a * b)) proof (state)
goal (1 subgoal):
 1. (sint a * sint b = sint (a * b)) = (scast a * scast b = scast (a * b)) proof (prove)
goal (1 subgoal):
 1. signed_take_bit (size a - 1) (sint a * sint b) \<in> range (signed_take_bit (size a - 1)) proof (state)
this:
signed_take_bit (size a - 1) (sint a * sint b) \<in> range (signed_take_bit (size a - 1))

goal (1 subgoal):
 1. (sint a * sint b = sint (a * b)) = (scast a * scast b = scast (a * b)) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<bar>sint x\<bar> < 2 ^ (size a - 1) + 1 proof (prove)
goal (1 subgoal):
 1. \<And>x. - (2 ^ (LENGTH('a) - Suc 0)) \<le> sint x \<and> sint x < 2 ^ (LENGTH('a) - Suc 0) \<Longrightarrow> \<bar>sint x\<bar> < 2 ^ (size a - 1) + 1 proof (prove)
goal:
No subgoals! proof (state)
this:
\<bar>sint ?x\<bar> < 2 ^ (size a - 1) + 1

goal (1 subgoal):
 1. (sint a * sint b = sint (a * b)) = (scast a * scast b = scast (a * b)) proof (prove)
goal (1 subgoal):
 1. \<bar>sint a * sint b\<bar> < 2 ^ (LENGTH('b) - 1) proof (prove)
using this:
\<bar>sint a\<bar> * \<bar>sint b\<bar> < (2 ^ (size a - 1) + 1) * (2 ^ (size a - 1) + 1)
(2 ^ (LENGTH('a) - 1) + 1)\<^sup>2 \<le> 2 ^ (LENGTH('b) - 1)

goal (1 subgoal):
 1. \<bar>sint a * sint b\<bar> < 2 ^ (LENGTH('b) - 1) proof (state)
this:
\<bar>sint a * sint b\<bar> < 2 ^ (LENGTH('b) - 1)

goal (1 subgoal):
 1. (sint a * sint b = sint (a * b)) = (scast a * scast b = scast (a * b)) proof (state)
this:
r = LENGTH('a) - 1
s = LENGTH('b) - 1

goal (1 subgoal):
 1. (sint a * sint b = sint (a * b)) = (scast a * scast b = scast (a * b)) proof (chain)
picking this:
r = LENGTH('a) - 1
s = LENGTH('b) - 1 proof (prove)
using this:
r = LENGTH('a) - 1
s = LENGTH('b) - 1

goal (1 subgoal):
 1. (LENGTH('a) = Suc r &&& LENGTH('b) = Suc s) &&& size a = Suc r &&& size b = Suc r proof (state)
this:
LENGTH('a) = Suc r
LENGTH('b) = Suc s
size a = Suc r
size b = Suc r

goal (1 subgoal):
 1. (sint a * sint b = sint (a * b)) = (scast a * scast b = scast (a * b)) proof (chain)
picking this:
LENGTH('a) = Suc r
LENGTH('b) = Suc s
size a = Suc r
size b = Suc r proof (prove)
using this:
LENGTH('a) = Suc r
LENGTH('b) = Suc s
size a = Suc r
size b = Suc r

goal (1 subgoal):
 1. (sint a * sint b = sint (a * b)) = (scast a * scast b = scast (a * b)) proof (prove)
using this:
LENGTH('a) = Suc r
LENGTH('b) = Suc s
size a = Suc r
size b = Suc r
signed_take_bit (size a - 1) (sint a * sint b) \<in> {i. - (2 ^ (size a - 1)) \<le> i \<and> i < 2 ^ (size a - 1)}
\<bar>sint a * sint b\<bar> < 2 ^ (LENGTH('b) - 1)
2 ^ (LENGTH('a) - 1) \<le> 2 ^ (LENGTH('b) - 1)

goal (1 subgoal):
 1. (sint a * sint b = sint (a * b)) = (scast a * scast b = scast (a * b)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>LENGTH('a) = Suc r; LENGTH('b) = Suc s; size a = Suc r; size b = Suc r; \<bar>sint a * sint b\<bar> < 2 ^ s; r \<le> s\<rbrakk> \<Longrightarrow> (sint a * sint b = sint (a * b)) = (scast a * scast b = scast (a * b)) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>LENGTH('a) = Suc r; LENGTH('b) = Suc s; LENGTH('a) = Suc r; LENGTH('a) = Suc r; \<bar>signed_take_bit (LENGTH('a) - Suc 0) a * signed_take_bit (LENGTH('a) - Suc 0) b\<bar> < 2 ^ s; r \<le> s\<rbrakk> \<Longrightarrow> (signed_take_bit (LENGTH('a) - Suc 0) a * signed_take_bit (LENGTH('a) - Suc 0) b = signed_take_bit (LENGTH('a) - Suc 0) (a * b)) = (take_bit LENGTH('b) (signed_take_bit (LENGTH('a) - Suc 0) a * signed_take_bit (LENGTH('a) - Suc 0) b) = take_bit LENGTH('b) (signed_take_bit (LENGTH('a) - Suc 0) (a * b))) proof (prove)
goal:
No subgoals! proof (state)
this:
(sint a * sint b = sint (a * b)) = (scast a * scast b = scast (a * b))

goal:
No subgoals!