theory Word_Lemmas

lemma distinct_word_add_ucast_shift_inj:
  \<open>p' = p \<and> off' = off\<close>
  if *: \<open>p + (UCAST('a::len \<rightarrow> 'b::len) off << n) = p' + (ucast off' << n)\<close>
    and \<open>is_aligned p n'\<close> \<open>is_aligned p' n'\<close> \<open>n' = n + LENGTH('a)\<close> \<open>n' < LENGTH('b)\<close> proof - from \<open>n' = n + LENGTH('a)\<close> have [simp]: \<open>n' - n = LENGTH('a)\<close> \<open>n + LENGTH('a) = n'\<close> by simp_all from \<open>is_aligned p n'\<close> obtain q
    where p: \<open>p = push_bit n' (word_of_nat q)\<close> \<open>q < 2 ^ (LENGTH('b) - n')\<close> by (rule is_alignedE') from \<open>is_aligned p' n'\<close> obtain q'
    where p': \<open>p' = push_bit n' (word_of_nat q')\<close> \<open>q' < 2 ^ (LENGTH('b) - n')\<close> by (rule is_alignedE') define m :: nat where \<open>m = unat off\<close> then have off: \<open>off = word_of_nat m\<close> by simp define m' :: nat where \<open>m' = unat off'\<close> then have off': \<open>off' = word_of_nat m'\<close> by simp have \<open>push_bit n' q + take_bit n' (push_bit n m) < 2 ^ LENGTH('b)\<close> by (metis id_apply is_aligned_no_wrap''' of_nat_eq_id of_nat_push_bit p(1) p(2) take_bit_nat_eq_self_iff take_bit_nat_less_exp take_bit_push_bit that(2) that(5) unsigned_of_nat) moreover have \<open>push_bit n' q' + take_bit n' (push_bit n m') < 2 ^ LENGTH('b)\<close> by (metis \<open>n' - n = LENGTH('a)\<close> id_apply is_aligned_no_wrap''' m'_def of_nat_eq_id of_nat_push_bit off' p'(1) p'(2) take_bit_nat_eq_self_iff take_bit_push_bit that(3) that(5) unsigned_of_nat) ultimately have \<open>push_bit n' q + take_bit n' (push_bit n m) = push_bit n' q' + take_bit n' (push_bit n m')\<close> using * by (simp add: p p' off off' push_bit_of_nat push_bit_take_bit word_of_nat_inj unsigned_of_nat shiftl_def flip: of_nat_add) then have \<open>int (push_bit n' q + take_bit n' (push_bit n m))
    = int (push_bit n' q' + take_bit n' (push_bit n m'))\<close> by simp then have \<open>concat_bit n' (int (push_bit n m)) (int q)
    = concat_bit n' (int (push_bit n m')) (int q')\<close> by (simp add: of_nat_push_bit of_nat_take_bit concat_bit_eq) then show ?thesis by (simp add: p p' off off' take_bit_of_nat take_bit_push_bit word_of_nat_eq_iff concat_bit_eq_iff)
      (simp add: push_bit_eq_mult) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. p' = p \<and> off' = off proof (state)
goal (1 subgoal):
 1. p' = p \<and> off' = off proof (chain)
picking this:
n' = n + LENGTH('a) proof (prove)
using this:
n' = n + LENGTH('a)

goal (1 subgoal):
 1. n' - n = LENGTH('a) &&& n + LENGTH('a) = n' proof (state)
this:
n' - n = LENGTH('a)
n + LENGTH('a) = n'

goal (1 subgoal):
 1. p' = p \<and> off' = off proof (chain)
picking this:
is_aligned p n' proof (prove)
using this:
is_aligned p n'

goal (1 subgoal):
 1. (\<And>q. \<lbrakk>p = push_bit n' (word_of_nat q); q < 2 ^ (LENGTH('b) - n')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (state)
this:
p = push_bit n' (word_of_nat q)
q < 2 ^ (LENGTH('b) - n')

goal (1 subgoal):
 1. p' = p \<and> off' = off proof (chain)
picking this:
is_aligned p' n' proof (prove)
using this:
is_aligned p' n'

goal (1 subgoal):
 1. (\<And>q'. \<lbrakk>p' = push_bit n' (word_of_nat q'); q' < 2 ^ (LENGTH('b) - n')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (state)
this:
p' = push_bit n' (word_of_nat q')
q' < 2 ^ (LENGTH('b) - n')

goal (1 subgoal):
 1. p' = p \<and> off' = off proof (state)
this:
m = unat off

goal (1 subgoal):
 1. p' = p \<and> off' = off proof (chain)
picking this:
m = unat off proof (prove)
using this:
m = unat off

goal (1 subgoal):
 1. off = word_of_nat m proof (state)
this:
off = word_of_nat m

goal (1 subgoal):
 1. p' = p \<and> off' = off proof (state)
this:
m' = unat off'

goal (1 subgoal):
 1. p' = p \<and> off' = off proof (chain)
picking this:
m' = unat off' proof (prove)
using this:
m' = unat off'

goal (1 subgoal):
 1. off' = word_of_nat m' proof (state)
this:
off' = word_of_nat m'

goal (1 subgoal):
 1. p' = p \<and> off' = off proof (prove)
goal (1 subgoal):
 1. push_bit n' q + take_bit n' (push_bit n m) < 2 ^ LENGTH('b) proof (state)
this:
push_bit n' q + take_bit n' (push_bit n m) < 2 ^ LENGTH('b)

goal (1 subgoal):
 1. p' = p \<and> off' = off proof (state)
this:
push_bit n' q + take_bit n' (push_bit n m) < 2 ^ LENGTH('b)

goal (1 subgoal):
 1. p' = p \<and> off' = off proof (prove)
goal (1 subgoal):
 1. push_bit n' q' + take_bit n' (push_bit n m') < 2 ^ LENGTH('b) proof (state)
this:
push_bit n' q' + take_bit n' (push_bit n m') < 2 ^ LENGTH('b)

goal (1 subgoal):
 1. p' = p \<and> off' = off proof (chain)
picking this:
push_bit n' q + take_bit n' (push_bit n m) < 2 ^ LENGTH('b)
push_bit n' q' + take_bit n' (push_bit n m') < 2 ^ LENGTH('b) proof (prove)
using this:
push_bit n' q + take_bit n' (push_bit n m) < 2 ^ LENGTH('b)
push_bit n' q' + take_bit n' (push_bit n m') < 2 ^ LENGTH('b)

goal (1 subgoal):
 1. push_bit n' q + take_bit n' (push_bit n m) = push_bit n' q' + take_bit n' (push_bit n m') proof (prove)
using this:
push_bit n' q + take_bit n' (push_bit n m) < 2 ^ LENGTH('b)
push_bit n' q' + take_bit n' (push_bit n m') < 2 ^ LENGTH('b)
p + (UCAST('a \<rightarrow> 'b) off << n) = p' + (UCAST('a \<rightarrow> 'b) off' << n)

goal (1 subgoal):
 1. push_bit n' q + take_bit n' (push_bit n m) = push_bit n' q' + take_bit n' (push_bit n m') proof (state)
this:
push_bit n' q + take_bit n' (push_bit n m) = push_bit n' q' + take_bit n' (push_bit n m')

goal (1 subgoal):
 1. p' = p \<and> off' = off proof (chain)
picking this:
push_bit n' q + take_bit n' (push_bit n m) = push_bit n' q' + take_bit n' (push_bit n m') proof (prove)
using this:
push_bit n' q + take_bit n' (push_bit n m) = push_bit n' q' + take_bit n' (push_bit n m')

goal (1 subgoal):
 1. int (push_bit n' q + take_bit n' (push_bit n m)) = int (push_bit n' q' + take_bit n' (push_bit n m')) proof (state)
this:
int (push_bit n' q + take_bit n' (push_bit n m)) = int (push_bit n' q' + take_bit n' (push_bit n m'))

goal (1 subgoal):
 1. p' = p \<and> off' = off proof (chain)
picking this:
int (push_bit n' q + take_bit n' (push_bit n m)) = int (push_bit n' q' + take_bit n' (push_bit n m')) proof (prove)
using this:
int (push_bit n' q + take_bit n' (push_bit n m)) = int (push_bit n' q' + take_bit n' (push_bit n m'))

goal (1 subgoal):
 1. concat_bit n' (int (push_bit n m)) (int q) = concat_bit n' (int (push_bit n m')) (int q') proof (state)
this:
concat_bit n' (int (push_bit n m)) (int q) = concat_bit n' (int (push_bit n m')) (int q')

goal (1 subgoal):
 1. p' = p \<and> off' = off proof (chain)
picking this:
concat_bit n' (int (push_bit n m)) (int q) = concat_bit n' (int (push_bit n m')) (int q') proof (prove)
using this:
concat_bit n' (int (push_bit n m)) (int q) = concat_bit n' (int (push_bit n m')) (int q')

goal (1 subgoal):
 1. p' = p \<and> off' = off proof (state)
this:
p' = p \<and> off' = off

goal:
No subgoals!