theory Reversed_Bit_Lists

lemma is_aligned_add_conv:
  fixes off::"'a::len word"
  assumes aligned: "is_aligned w n"
  and        offv: "off < 2 ^ n"
  shows    "to_bl (w + off) =
   (take (LENGTH('a) - n) (to_bl w)) @ (drop (LENGTH('a) - n) (to_bl off))" proof cases assume nv: "n \<le> LENGTH('a)" show ?thesis proof (subst aligned_bl_add_size, simp_all only: word_size) show "drop (LENGTH('a) - n) (to_bl w) = replicate n False" by (subst is_aligned_replicate [OF aligned nv]) (simp add: word_size) from offv show "take (LENGTH('a) - n) (to_bl off) =
                    replicate (LENGTH('a) - n) False" by (subst less_is_drop_replicate, assumption) simp qed fact next assume "\<not> n \<le> LENGTH('a)" with offv show ?thesis by (simp add: power_overflow) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. to_bl (w + off) = take (LENGTH('a) - n) (to_bl w) @ drop (LENGTH('a) - n) (to_bl off) proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> to_bl (w + off) = take (LENGTH('a) - n) (to_bl w) @ drop (LENGTH('a) - n) (to_bl off)
 2. \<not> ?P \<Longrightarrow> to_bl (w + off) = take (LENGTH('a) - n) (to_bl w) @ drop (LENGTH('a) - n) (to_bl off) proof (state)
this:
n \<le> LENGTH('a)

goal (2 subgoals):
 1. ?P \<Longrightarrow> to_bl (w + off) = take (LENGTH('a) - n) (to_bl w) @ drop (LENGTH('a) - n) (to_bl off)
 2. \<not> ?P \<Longrightarrow> to_bl (w + off) = take (LENGTH('a) - n) (to_bl w) @ drop (LENGTH('a) - n) (to_bl off) proof (prove)
goal (1 subgoal):
 1. to_bl (w + off) = take (LENGTH('a) - n) (to_bl w) @ drop (LENGTH('a) - n) (to_bl off) proof (state)
goal (3 subgoals):
 1. n \<le> LENGTH('a)
 2. drop (LENGTH('a) - n) (to_bl w) = replicate n False
 3. take (LENGTH('a) - n) (to_bl off) = replicate (LENGTH('a) - n) False proof (prove)
goal (1 subgoal):
 1. drop (LENGTH('a) - n) (to_bl w) = replicate n False proof (state)
this:
drop (LENGTH('a) - n) (to_bl w) = replicate n False

goal (2 subgoals):
 1. n \<le> LENGTH('a)
 2. take (LENGTH('a) - n) (to_bl off) = replicate (LENGTH('a) - n) False proof (chain)
picking this:
off < 2 ^ n proof (prove)
using this:
off < 2 ^ n

goal (1 subgoal):
 1. take (LENGTH('a) - n) (to_bl off) = replicate (LENGTH('a) - n) False proof (state)
this:
take (LENGTH('a) - n) (to_bl off) = replicate (LENGTH('a) - n) False

goal (1 subgoal):
 1. n \<le> LENGTH('a) proof (state)
this:
to_bl (w + off) = take (LENGTH('a) - n) (to_bl w) @ drop (LENGTH('a) - n) (to_bl off)

goal (1 subgoal):
 1. \<not> n \<le> LENGTH('a) \<Longrightarrow> to_bl (w + off) = take (LENGTH('a) - n) (to_bl w) @ drop (LENGTH('a) - n) (to_bl off) proof (state)
goal (1 subgoal):
 1. \<not> n \<le> LENGTH('a) \<Longrightarrow> to_bl (w + off) = take (LENGTH('a) - n) (to_bl w) @ drop (LENGTH('a) - n) (to_bl off) proof (state)
this:
\<not> n \<le> LENGTH('a)

goal (1 subgoal):
 1. \<not> n \<le> LENGTH('a) \<Longrightarrow> to_bl (w + off) = take (LENGTH('a) - n) (to_bl w) @ drop (LENGTH('a) - n) (to_bl off) proof (chain)
picking this:
off < 2 ^ n
\<not> n \<le> LENGTH('a) proof (prove)
using this:
off < 2 ^ n
\<not> n \<le> LENGTH('a)

goal (1 subgoal):
 1. to_bl (w + off) = take (LENGTH('a) - n) (to_bl w) @ drop (LENGTH('a) - n) (to_bl off) proof (state)
this:
to_bl (w + off) = take (LENGTH('a) - n) (to_bl w) @ drop (LENGTH('a) - n) (to_bl off)

goal:
No subgoals!