theory Reversed_Bit_Lists

lemma bin_cat_foldl_lem:
  "foldl (\<lambda>u k. concat_bit n k u) x xs =
    concat_bit (size xs * n) (foldl (\<lambda>u k. concat_bit n k u) y xs) x" apply (induct xs arbitrary: x) apply simp apply (simp (no_asm)) apply (frule asm_rl) apply (drule meta_spec) apply (erule trans) apply (drule_tac x = "concat_bit n a y" in meta_spec) apply (simp add: bin_cat_assoc_sym) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. foldl (\<lambda>u k. concat_bit n k u) x xs = concat_bit (length xs * n) (foldl (\<lambda>u k. concat_bit n k u) y xs) x proof (prove)
goal (2 subgoals):
 1. \<And>x. foldl (\<lambda>u k. concat_bit n k u) x [] = concat_bit (length [] * n) (foldl (\<lambda>u k. concat_bit n k u) y []) x
 2. \<And>a xs x. (\<And>x. foldl (\<lambda>u k. concat_bit n k u) x xs = concat_bit (length xs * n) (foldl (\<lambda>u k. concat_bit n k u) y xs) x) \<Longrightarrow> foldl (\<lambda>u k. concat_bit n k u) x (a # xs) = concat_bit (length (a # xs) * n) (foldl (\<lambda>u k. concat_bit n k u) y (a # xs)) x proof (prove)
goal (1 subgoal):
 1. \<And>a xs x. (\<And>x. foldl (\<lambda>u k. concat_bit n k u) x xs = concat_bit (length xs * n) (foldl (\<lambda>u k. concat_bit n k u) y xs) x) \<Longrightarrow> foldl (\<lambda>u k. concat_bit n k u) x (a # xs) = concat_bit (length (a # xs) * n) (foldl (\<lambda>u k. concat_bit n k u) y (a # xs)) x proof (prove)
goal (1 subgoal):
 1. \<And>a xs x. (\<And>x. foldl (\<lambda>u k. concat_bit n k u) x xs = concat_bit (length xs * n) (foldl (\<lambda>u k. concat_bit n k u) y xs) x) \<Longrightarrow> foldl (\<lambda>u k. concat_bit n k u) (concat_bit n a x) xs = concat_bit (n + length xs * n) (foldl (\<lambda>u k. concat_bit n k u) (concat_bit n a y) xs) x proof (prove)
goal (1 subgoal):
 1. \<And>a xs x. \<lbrakk>\<And>x. foldl (\<lambda>u k. concat_bit n k u) x xs = concat_bit (length xs * n) (foldl (\<lambda>u k. concat_bit n k u) y xs) x; \<And>x. foldl (\<lambda>u k. concat_bit n k u) x xs = concat_bit (length xs * n) (foldl (\<lambda>u k. concat_bit n k u) y xs) x\<rbrakk> \<Longrightarrow> foldl (\<lambda>u k. concat_bit n k u) (concat_bit n a x) xs = concat_bit (n + length xs * n) (foldl (\<lambda>u k. concat_bit n k u) (concat_bit n a y) xs) x proof (prove)
goal (1 subgoal):
 1. \<And>a xs x. \<lbrakk>\<And>x. foldl (\<lambda>u k. concat_bit n k u) x xs = concat_bit (length xs * n) (foldl (\<lambda>u k. concat_bit n k u) y xs) x; foldl (\<lambda>u k. concat_bit n k u) (?x4 a xs x) xs = concat_bit (length xs * n) (foldl (\<lambda>u k. concat_bit n k u) y xs) (?x4 a xs x)\<rbrakk> \<Longrightarrow> foldl (\<lambda>u k. concat_bit n k u) (concat_bit n a x) xs = concat_bit (n + length xs * n) (foldl (\<lambda>u k. concat_bit n k u) (concat_bit n a y) xs) x proof (prove)
goal (1 subgoal):
 1. \<And>a xs x. (\<And>x. foldl (\<lambda>u k. concat_bit n k u) x xs = concat_bit (length xs * n) (foldl (\<lambda>u k. concat_bit n k u) y xs) x) \<Longrightarrow> concat_bit (length xs * n) (foldl (\<lambda>u k. concat_bit n k u) y xs) (concat_bit n a x) = concat_bit (n + length xs * n) (foldl (\<lambda>u k. concat_bit n k u) (concat_bit n a y) xs) x proof (prove)
goal (1 subgoal):
 1. \<And>a xs x. foldl (\<lambda>u k. concat_bit n k u) (concat_bit n a y) xs = concat_bit (length xs * n) (foldl (\<lambda>u k. concat_bit n k u) y xs) (concat_bit n a y) \<Longrightarrow> concat_bit (length xs * n) (foldl (\<lambda>u k. concat_bit n k u) y xs) (concat_bit n a x) = concat_bit (n + length xs * n) (foldl (\<lambda>u k. concat_bit n k u) (concat_bit n a y) xs) x proof (prove)
goal:
No subgoals!