theory More_Word

lemma mult_pow2_inj:
  assumes ws: "m + n \<le> LENGTH('a)"
  assumes le: "x \<le> mask m" "y \<le> mask m"
  assumes eq: "x * 2 ^ n = y * (2 ^ n::'a::len word)"
  shows "x = y" proof (rule bit_word_eqI) fix q assume \<open>q < LENGTH('a)\<close> from eq have \<open>push_bit n x = push_bit n y\<close> by (simp add: push_bit_eq_mult) moreover from le have \<open>take_bit m x = x\<close> \<open>take_bit m y = y\<close> by (simp_all add: less_eq_mask_iff_take_bit_eq_self) ultimately have \<open>push_bit n (take_bit m x) = push_bit n (take_bit m y)\<close> by simp_all with \<open>q < LENGTH('a)\<close> ws show \<open>bit x q \<longleftrightarrow> bit y q\<close> apply (simp add: push_bit_take_bit) unfolding bit_eq_iff apply (simp add: bit_simps not_le) apply (metis (full_types) \<open>take_bit m x = x\<close> \<open>take_bit m y = y\<close> add.commute add_diff_cancel_right' add_less_cancel_right bit_take_bit_iff le_add2 less_le_trans) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x = y proof (state)
goal (1 subgoal):
 1. \<And>n. n < LENGTH('a) \<Longrightarrow> bit x n = bit y n proof (state)
goal (1 subgoal):
 1. \<And>n. n < LENGTH('a) \<Longrightarrow> bit x n = bit y n proof (state)
this:
q < LENGTH('a)

goal (1 subgoal):
 1. \<And>n. n < LENGTH('a) \<Longrightarrow> bit x n = bit y n proof (chain)
picking this:
x * 2 ^ n = y * 2 ^ n proof (prove)
using this:
x * 2 ^ n = y * 2 ^ n

goal (1 subgoal):
 1. push_bit n x = push_bit n y proof (state)
this:
push_bit n x = push_bit n y

goal (1 subgoal):
 1. \<And>n. n < LENGTH('a) \<Longrightarrow> bit x n = bit y n proof (state)
this:
push_bit n x = push_bit n y

goal (1 subgoal):
 1. \<And>n. n < LENGTH('a) \<Longrightarrow> bit x n = bit y n proof (chain)
picking this:
x \<le> mask m
y \<le> mask m proof (prove)
using this:
x \<le> mask m
y \<le> mask m

goal (1 subgoal):
 1. take_bit m x = x &&& take_bit m y = y proof (state)
this:
take_bit m x = x
take_bit m y = y

goal (1 subgoal):
 1. \<And>n. n < LENGTH('a) \<Longrightarrow> bit x n = bit y n proof (chain)
picking this:
push_bit n x = push_bit n y
take_bit m x = x
take_bit m y = y proof (prove)
using this:
push_bit n x = push_bit n y
take_bit m x = x
take_bit m y = y

goal (1 subgoal):
 1. push_bit n (take_bit m x) = push_bit n (take_bit m y) proof (state)
this:
push_bit n (take_bit m x) = push_bit n (take_bit m y)

goal (1 subgoal):
 1. \<And>n. n < LENGTH('a) \<Longrightarrow> bit x n = bit y n proof (chain)
picking this:
q < LENGTH('a)
m + n \<le> LENGTH('a)
push_bit n (take_bit m x) = push_bit n (take_bit m y) proof (prove)
using this:
q < LENGTH('a)
m + n \<le> LENGTH('a)
push_bit n (take_bit m x) = push_bit n (take_bit m y)

goal (1 subgoal):
 1. bit x q = bit y q proof (prove)
goal (1 subgoal):
 1. \<lbrakk>q < LENGTH('a); m + n \<le> LENGTH('a); take_bit (n + m) (push_bit n x) = take_bit (n + m) (push_bit n y)\<rbrakk> \<Longrightarrow> bit x q = bit y q proof (prove)
goal (1 subgoal):
 1. \<lbrakk>q < LENGTH('a); m + n \<le> LENGTH('a); \<forall>na. possible_bit TYPE('a word) na \<longrightarrow> bit (take_bit (n + m) (push_bit n x)) na = bit (take_bit (n + m) (push_bit n y)) na\<rbrakk> \<Longrightarrow> bit x q = bit y q proof (prove)
goal (1 subgoal):
 1. \<lbrakk>q < LENGTH('a); m + n \<le> LENGTH('a); \<forall>na<LENGTH('a). (na < n + m \<and> n \<le> na \<and> bit x (na - n)) = (na < n + m \<and> n \<le> na \<and> bit y (na - n))\<rbrakk> \<Longrightarrow> bit x q = bit y q proof (prove)
goal:
No subgoals! proof (state)
this:
bit x q = bit y q

goal:
No subgoals!