theory Reversed_Bit_Lists

lemma bl_word_roti_dt':
  "n = nat ((- i) mod int (size (w :: 'a::len word))) \<Longrightarrow>
    to_bl (word_roti i w) = drop n (to_bl w) @ take n (to_bl w)" apply (unfold word_roti_eq_word_rotr_word_rotl) apply (simp add: bl_word_rotl_dt bl_word_rotr_dt word_size) apply safe apply (simp add: zmod_zminus1_eq_if) apply safe apply (auto simp add: nat_mult_distrib nat_mod_distrib) using nat_0_le nat_minus_as_int zmod_int apply presburger done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n = nat (- i mod int (size w)) \<Longrightarrow> to_bl (word_roti i w) = drop n (to_bl w) @ take n (to_bl w) proof (prove)
goal (1 subgoal):
 1. n = nat (- i mod int (size w)) \<Longrightarrow> to_bl (if 0 \<le> i then word_rotr (nat i) w else word_rotl (nat (- i)) w) = drop n (to_bl w) @ take n (to_bl w) proof (prove)
goal (1 subgoal):
 1. n = nat (- i mod int LENGTH('a)) \<Longrightarrow> (0 \<le> i \<longrightarrow> drop (LENGTH('a) - nat i mod LENGTH('a)) (to_bl w) @ take (LENGTH('a) - nat i mod LENGTH('a)) (to_bl w) = drop (nat (- i mod int LENGTH('a))) (to_bl w) @ take (nat (- i mod int LENGTH('a))) (to_bl w)) \<and> (\<not> 0 \<le> i \<longrightarrow> drop (nat (- i) mod LENGTH('a)) (to_bl w) @ take (nat (- i) mod LENGTH('a)) (to_bl w) = drop (nat (- i mod int LENGTH('a))) (to_bl w) @ take (nat (- i mod int LENGTH('a))) (to_bl w)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n = nat (- i mod int LENGTH('a)); 0 \<le> i\<rbrakk> \<Longrightarrow> drop (LENGTH('a) - nat i mod LENGTH('a)) (to_bl w) @ take (LENGTH('a) - nat i mod LENGTH('a)) (to_bl w) = drop (nat (- i mod int LENGTH('a))) (to_bl w) @ take (nat (- i mod int LENGTH('a))) (to_bl w)
 2. \<lbrakk>n = nat (- i mod int LENGTH('a)); \<not> 0 \<le> i\<rbrakk> \<Longrightarrow> drop (nat (- i) mod LENGTH('a)) (to_bl w) @ take (nat (- i) mod LENGTH('a)) (to_bl w) = drop (nat (- i mod int LENGTH('a))) (to_bl w) @ take (nat (- i mod int LENGTH('a))) (to_bl w) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n = nat (if i mod int LENGTH('a) = 0 then 0 else int LENGTH('a) - i mod int LENGTH('a)); 0 \<le> i\<rbrakk> \<Longrightarrow> (i mod int LENGTH('a) = 0 \<longrightarrow> drop (LENGTH('a) - nat i mod LENGTH('a)) (to_bl w) @ take (LENGTH('a) - nat i mod LENGTH('a)) (to_bl w) = to_bl w) \<and> (i mod int LENGTH('a) \<noteq> 0 \<longrightarrow> drop (LENGTH('a) - nat i mod LENGTH('a)) (to_bl w) @ take (LENGTH('a) - nat i mod LENGTH('a)) (to_bl w) = drop (nat (int LENGTH('a) - i mod int LENGTH('a))) (to_bl w) @ take (nat (int LENGTH('a) - i mod int LENGTH('a))) (to_bl w))
 2. \<lbrakk>n = nat (- i mod int LENGTH('a)); \<not> 0 \<le> i\<rbrakk> \<Longrightarrow> drop (nat (- i) mod LENGTH('a)) (to_bl w) @ take (nat (- i) mod LENGTH('a)) (to_bl w) = drop (nat (- i mod int LENGTH('a))) (to_bl w) @ take (nat (- i mod int LENGTH('a))) (to_bl w) proof (prove)
goal (3 subgoals):
 1. \<And>q. \<lbrakk>n = nat (if int LENGTH('a) * q mod int LENGTH('a) = 0 then 0 else int LENGTH('a) - int LENGTH('a) * q mod int LENGTH('a)); 0 \<le> int LENGTH('a) * q; i = int LENGTH('a) * q\<rbrakk> \<Longrightarrow> drop (LENGTH('a) - nat (int LENGTH('a) * q) mod LENGTH('a)) (to_bl w) @ take (LENGTH('a) - nat (int LENGTH('a) * q) mod LENGTH('a)) (to_bl w) = to_bl w
 2. \<lbrakk>n = nat (if i mod int LENGTH('a) = 0 then 0 else int LENGTH('a) - i mod int LENGTH('a)); 0 \<le> i; i mod int LENGTH('a) \<noteq> 0\<rbrakk> \<Longrightarrow> drop (LENGTH('a) - nat i mod LENGTH('a)) (to_bl w) @ take (LENGTH('a) - nat i mod LENGTH('a)) (to_bl w) = drop (nat (int LENGTH('a) - i mod int LENGTH('a))) (to_bl w) @ take (nat (int LENGTH('a) - i mod int LENGTH('a))) (to_bl w)
 3. \<lbrakk>n = nat (- i mod int LENGTH('a)); \<not> 0 \<le> i\<rbrakk> \<Longrightarrow> drop (nat (- i) mod LENGTH('a)) (to_bl w) @ take (nat (- i) mod LENGTH('a)) (to_bl w) = drop (nat (- i mod int LENGTH('a))) (to_bl w) @ take (nat (- i mod int LENGTH('a))) (to_bl w) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n = nat (int LENGTH('a) - i mod int LENGTH('a)); 0 \<le> i; i mod int LENGTH('a) \<noteq> 0\<rbrakk> \<Longrightarrow> drop (LENGTH('a) - nat i mod LENGTH('a)) (to_bl w) @ take (LENGTH('a) - nat i mod LENGTH('a)) (to_bl w) = drop (nat (int LENGTH('a) - i mod int LENGTH('a))) (to_bl w) @ take (nat (int LENGTH('a) - i mod int LENGTH('a))) (to_bl w) proof (prove)
using this:
0 \<le> ?z \<Longrightarrow> int (nat ?z) = ?z
(-) = (\<lambda>a b. nat (int a - int b))
int (?m mod ?n) = int ?m mod int ?n

goal (1 subgoal):
 1. \<lbrakk>n = nat (int LENGTH('a) - i mod int LENGTH('a)); 0 \<le> i; i mod int LENGTH('a) \<noteq> 0\<rbrakk> \<Longrightarrow> drop (LENGTH('a) - nat i mod LENGTH('a)) (to_bl w) @ take (LENGTH('a) - nat i mod LENGTH('a)) (to_bl w) = drop (nat (int LENGTH('a) - i mod int LENGTH('a))) (to_bl w) @ take (nat (int LENGTH('a) - i mod int LENGTH('a))) (to_bl w) proof (prove)
goal:
No subgoals!