theory ADT_H

lemma bin_to_bl_of_bl_eq:
  "\<lbrakk>is_aligned (a::'a::len word) n; length b + c \<le> n; length b + c < LENGTH('a)\<rbrakk>
  \<Longrightarrow> bin_to_bl (length b) (uint ((a + of_bl b * 2^c) >> c)) = b" apply (subst word_plus_and_or_coroll) apply (erule is_aligned_get_word_bits) apply (rule is_aligned_AND_less_0) apply (simp add: is_aligned_mask) apply (rule order_less_le_trans) apply (rule of_bl_length2) apply (simp add: word_bits_conv cte_level_bits_def) apply (simp add: two_power_increasing) apply simp apply (rule nth_equalityI) apply (simp only: len_bin_to_bl) apply (clarsimp simp only: len_bin_to_bl nth_bin_to_bl
                             word_test_bit_def[symmetric]) apply (simp add: nth_shiftr nth_shiftl
                   shiftl_t2n[where n=c, simplified mult.commute,
                              simplified, symmetric]) apply (simp add: is_aligned_nth[THEN iffD1, rule_format]
                   test_bit_of_bl nth_rev) apply (case_tac "b ! i", simp_all) apply arith done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned a n; length b + c \<le> n; length b + c < LENGTH('a)\<rbrakk> \<Longrightarrow> bin_to_bl (length b) (uint (a + of_bl b * 2 ^ c >> c)) = b proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned a n; length b + c \<le> n; length b + c < LENGTH('a)\<rbrakk> \<Longrightarrow> a && of_bl b * 2 ^ c = 0
 2. \<lbrakk>is_aligned a n; length b + c \<le> n; length b + c < LENGTH('a)\<rbrakk> \<Longrightarrow> bin_to_bl (length b) (uint (a || of_bl b * 2 ^ c >> c)) = b proof (prove)
goal (3 subgoals):
 1. \<lbrakk>length b + c \<le> n; length b + c < LENGTH('a); is_aligned a n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> a && of_bl b * 2 ^ c = 0
 2. \<lbrakk>length b + c \<le> n; length b + c < LENGTH('a); a = 0; LENGTH('a) \<le> n\<rbrakk> \<Longrightarrow> a && of_bl b * 2 ^ c = 0
 3. \<lbrakk>is_aligned a n; length b + c \<le> n; length b + c < LENGTH('a)\<rbrakk> \<Longrightarrow> bin_to_bl (length b) (uint (a || of_bl b * 2 ^ c >> c)) = b proof (prove)
goal (4 subgoals):
 1. \<lbrakk>length b + c \<le> n; length b + c < LENGTH('a); is_aligned a n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> a && mask ?n3 = 0
 2. \<lbrakk>length b + c \<le> n; length b + c < LENGTH('a); is_aligned a n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> of_bl b * 2 ^ c < 2 ^ ?n3
 3. \<lbrakk>length b + c \<le> n; length b + c < LENGTH('a); a = 0; LENGTH('a) \<le> n\<rbrakk> \<Longrightarrow> a && of_bl b * 2 ^ c = 0
 4. \<lbrakk>is_aligned a n; length b + c \<le> n; length b + c < LENGTH('a)\<rbrakk> \<Longrightarrow> bin_to_bl (length b) (uint (a || of_bl b * 2 ^ c >> c)) = b proof (prove)
goal (3 subgoals):
 1. \<lbrakk>length b + c \<le> n; length b + c < LENGTH('a); is_aligned a n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> of_bl b * 2 ^ c < 2 ^ n
 2. \<lbrakk>length b + c \<le> n; length b + c < LENGTH('a); a = 0; LENGTH('a) \<le> n\<rbrakk> \<Longrightarrow> a && of_bl b * 2 ^ c = 0
 3. \<lbrakk>is_aligned a n; length b + c \<le> n; length b + c < LENGTH('a)\<rbrakk> \<Longrightarrow> bin_to_bl (length b) (uint (a || of_bl b * 2 ^ c >> c)) = b proof (prove)
goal (4 subgoals):
 1. \<lbrakk>length b + c \<le> n; length b + c < LENGTH('a); is_aligned a n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> of_bl b * 2 ^ c < ?y11
 2. \<lbrakk>length b + c \<le> n; length b + c < LENGTH('a); is_aligned a n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> ?y11 \<le> 2 ^ n
 3. \<lbrakk>length b + c \<le> n; length b + c < LENGTH('a); a = 0; LENGTH('a) \<le> n\<rbrakk> \<Longrightarrow> a && of_bl b * 2 ^ c = 0
 4. \<lbrakk>is_aligned a n; length b + c \<le> n; length b + c < LENGTH('a)\<rbrakk> \<Longrightarrow> bin_to_bl (length b) (uint (a || of_bl b * 2 ^ c >> c)) = b proof (prove)
goal (4 subgoals):
 1. \<lbrakk>length b + c \<le> n; length b + c < LENGTH('a); is_aligned a n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> length b + c < LENGTH('a)
 2. \<lbrakk>length b + c \<le> n; length b + c < LENGTH('a); is_aligned a n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> 2 ^ (length b + c) \<le> 2 ^ n
 3. \<lbrakk>length b + c \<le> n; length b + c < LENGTH('a); a = 0; LENGTH('a) \<le> n\<rbrakk> \<Longrightarrow> a && of_bl b * 2 ^ c = 0
 4. \<lbrakk>is_aligned a n; length b + c \<le> n; length b + c < LENGTH('a)\<rbrakk> \<Longrightarrow> bin_to_bl (length b) (uint (a || of_bl b * 2 ^ c >> c)) = b proof (prove)
goal (3 subgoals):
 1. \<lbrakk>length b + c \<le> n; length b + c < LENGTH('a); is_aligned a n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> 2 ^ (length b + c) \<le> 2 ^ n
 2. \<lbrakk>length b + c \<le> n; length b + c < LENGTH('a); a = 0; LENGTH('a) \<le> n\<rbrakk> \<Longrightarrow> a && of_bl b * 2 ^ c = 0
 3. \<lbrakk>is_aligned a n; length b + c \<le> n; length b + c < LENGTH('a)\<rbrakk> \<Longrightarrow> bin_to_bl (length b) (uint (a || of_bl b * 2 ^ c >> c)) = b proof (prove)
goal (2 subgoals):
 1. \<lbrakk>length b + c \<le> n; length b + c < LENGTH('a); a = 0; LENGTH('a) \<le> n\<rbrakk> \<Longrightarrow> a && of_bl b * 2 ^ c = 0
 2. \<lbrakk>is_aligned a n; length b + c \<le> n; length b + c < LENGTH('a)\<rbrakk> \<Longrightarrow> bin_to_bl (length b) (uint (a || of_bl b * 2 ^ c >> c)) = b proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned a n; length b + c \<le> n; length b + c < LENGTH('a)\<rbrakk> \<Longrightarrow> bin_to_bl (length b) (uint (a || of_bl b * 2 ^ c >> c)) = b proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned a n; length b + c \<le> n; length b + c < LENGTH('a)\<rbrakk> \<Longrightarrow> length (bin_to_bl (length b) (uint (a || of_bl b * 2 ^ c >> c))) = length b
 2. \<And>i. \<lbrakk>is_aligned a n; length b + c \<le> n; length b + c < LENGTH('a); i < length (bin_to_bl (length b) (uint (a || of_bl b * 2 ^ c >> c)))\<rbrakk> \<Longrightarrow> bin_to_bl (length b) (uint (a || of_bl b * 2 ^ c >> c)) ! i = b ! i proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>is_aligned a n; length b + c \<le> n; length b + c < LENGTH('a); i < length (bin_to_bl (length b) (uint (a || of_bl b * 2 ^ c >> c)))\<rbrakk> \<Longrightarrow> bin_to_bl (length b) (uint (a || of_bl b * 2 ^ c >> c)) ! i = b ! i proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>is_aligned a n; length b + c \<le> n; length b + c < LENGTH('a); i < length b\<rbrakk> \<Longrightarrow> (a || of_bl b * 2 ^ c >> c) !! (length b - Suc i) = b ! i proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>is_aligned a n; length b + c \<le> n; length b + c < LENGTH('a); i < length b\<rbrakk> \<Longrightarrow> (a !! (c + length b - Suc i) \<or> c \<le> c + length b - Suc i \<and> c + length b - Suc i < LENGTH('a) \<and> rev b ! (length b - Suc i) \<and> length b - Suc i < LENGTH('a) \<and> length b - Suc i < length b) = b ! i proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>is_aligned a n; length b + c \<le> n; length b + c < LENGTH('a); i < length b\<rbrakk> \<Longrightarrow> (c \<le> c + length b - Suc i \<and> c + length b - Suc i < LENGTH('a) \<and> b ! i \<and> length b - Suc i < LENGTH('a) \<and> length b - Suc i < length b) = b ! i proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>is_aligned a n; length b + c \<le> n; length b + c < LENGTH('a); i < length b; b ! i\<rbrakk> \<Longrightarrow> c \<le> c + length b - Suc i \<and> c + length b - Suc i < LENGTH('a) \<and> length b - Suc i < LENGTH('a) \<and> length b - Suc i < length b proof (prove)
goal:
No subgoals!