theory Reversed_Bit_Lists

lemma horner_sum_of_bool_2_concat:
  \<open>horner_sum of_bool 2 (concat (map (\<lambda>x. map (bit x) [0..<LENGTH('a)]) ws)) = horner_sum uint (2 ^ LENGTH('a)) ws\<close>
  for ws :: \<open>'a::len word list\<close> proof (induction ws) case Nil then show ?case by simp next case (Cons w ws) moreover have \<open>horner_sum of_bool 2 (map (bit w) [0..<LENGTH('a)]) = uint w\<close> proof transfer fix k :: int have \<open>map (\<lambda>n. n < LENGTH('a) \<and> bit k n) [0..<LENGTH('a)]
      = map (bit k) [0..<LENGTH('a)]\<close> by simp then show \<open>horner_sum of_bool 2 (map (\<lambda>n. n < LENGTH('a) \<and> bit k n) [0..<LENGTH('a)])
      = take_bit LENGTH('a) k\<close> by (simp only: horner_sum_bit_eq_take_bit) qed ultimately show ?case by (simp add: horner_sum_append) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. horner_sum of_bool 2 (concat (map (\<lambda>x. map (bit x) [0..<LENGTH('a)]) ws)) = horner_sum uint (2 ^ LENGTH('a)) ws proof (state)
goal (2 subgoals):
 1. horner_sum of_bool 2 (concat (map (\<lambda>x. map (bit x) [0..<LENGTH('a)]) [])) = horner_sum uint (2 ^ LENGTH('a)) []
 2. \<And>a ws. horner_sum of_bool 2 (concat (map (\<lambda>x. map (bit x) [0..<LENGTH('a)]) ws)) = horner_sum uint (2 ^ LENGTH('a)) ws \<Longrightarrow> horner_sum of_bool 2 (concat (map (\<lambda>x. map (bit x) [0..<LENGTH('a)]) (a # ws))) = horner_sum uint (2 ^ LENGTH('a)) (a # ws) proof (state)
this:


goal (2 subgoals):
 1. horner_sum of_bool 2 (concat (map (\<lambda>x. map (bit x) [0..<LENGTH('a)]) [])) = horner_sum uint (2 ^ LENGTH('a)) []
 2. \<And>a ws. horner_sum of_bool 2 (concat (map (\<lambda>x. map (bit x) [0..<LENGTH('a)]) ws)) = horner_sum uint (2 ^ LENGTH('a)) ws \<Longrightarrow> horner_sum of_bool 2 (concat (map (\<lambda>x. map (bit x) [0..<LENGTH('a)]) (a # ws))) = horner_sum uint (2 ^ LENGTH('a)) (a # ws) proof (chain)
picking this:
 proof (prove)
goal (1 subgoal):
 1. horner_sum of_bool 2 (concat (map (\<lambda>x. map (bit x) [0..<LENGTH('a)]) [])) = horner_sum uint (2 ^ LENGTH('a)) [] proof (state)
this:
horner_sum of_bool 2 (concat (map (\<lambda>x. map (bit x) [0..<LENGTH('a)]) [])) = horner_sum uint (2 ^ LENGTH('a)) []

goal (1 subgoal):
 1. \<And>a ws. horner_sum of_bool 2 (concat (map (\<lambda>x. map (bit x) [0..<LENGTH('a)]) ws)) = horner_sum uint (2 ^ LENGTH('a)) ws \<Longrightarrow> horner_sum of_bool 2 (concat (map (\<lambda>x. map (bit x) [0..<LENGTH('a)]) (a # ws))) = horner_sum uint (2 ^ LENGTH('a)) (a # ws) proof (state)
goal (1 subgoal):
 1. \<And>a ws. horner_sum of_bool 2 (concat (map (\<lambda>x. map (bit x) [0..<LENGTH('a)]) ws)) = horner_sum uint (2 ^ LENGTH('a)) ws \<Longrightarrow> horner_sum of_bool 2 (concat (map (\<lambda>x. map (bit x) [0..<LENGTH('a)]) (a # ws))) = horner_sum uint (2 ^ LENGTH('a)) (a # ws) proof (state)
this:
horner_sum of_bool 2 (concat (map (\<lambda>x. map (bit x) [0..<LENGTH('a)]) ws)) = horner_sum uint (2 ^ LENGTH('a)) ws

goal (1 subgoal):
 1. \<And>a ws. horner_sum of_bool 2 (concat (map (\<lambda>x. map (bit x) [0..<LENGTH('a)]) ws)) = horner_sum uint (2 ^ LENGTH('a)) ws \<Longrightarrow> horner_sum of_bool 2 (concat (map (\<lambda>x. map (bit x) [0..<LENGTH('a)]) (a # ws))) = horner_sum uint (2 ^ LENGTH('a)) (a # ws) proof (state)
this:
horner_sum of_bool 2 (concat (map (\<lambda>x. map (bit x) [0..<LENGTH('a)]) ws)) = horner_sum uint (2 ^ LENGTH('a)) ws

goal (1 subgoal):
 1. \<And>a ws. horner_sum of_bool 2 (concat (map (\<lambda>x. map (bit x) [0..<LENGTH('a)]) ws)) = horner_sum uint (2 ^ LENGTH('a)) ws \<Longrightarrow> horner_sum of_bool 2 (concat (map (\<lambda>x. map (bit x) [0..<LENGTH('a)]) (a # ws))) = horner_sum uint (2 ^ LENGTH('a)) (a # ws) proof (prove)
goal (1 subgoal):
 1. horner_sum of_bool 2 (map (bit w) [0..<LENGTH('a)]) = uint w proof (state)
goal (1 subgoal):
 1. \<And>w. horner_sum of_bool 2 (map (\<lambda>n. n < LENGTH('a) \<and> bit w n) [0..<LENGTH('a)]) = take_bit LENGTH('a) w proof (state)
goal (1 subgoal):
 1. \<And>w. horner_sum of_bool 2 (map (\<lambda>n. n < LENGTH('a) \<and> bit w n) [0..<LENGTH('a)]) = take_bit LENGTH('a) w proof (prove)
goal (1 subgoal):
 1. map (\<lambda>n. n < LENGTH('a) \<and> bit k n) [0..<LENGTH('a)] = map (bit k) [0..<LENGTH('a)] proof (state)
this:
map (\<lambda>n. n < LENGTH('a) \<and> bit k n) [0..<LENGTH('a)] = map (bit k) [0..<LENGTH('a)]

goal (1 subgoal):
 1. \<And>w. horner_sum of_bool 2 (map (\<lambda>n. n < LENGTH('a) \<and> bit w n) [0..<LENGTH('a)]) = take_bit LENGTH('a) w proof (chain)
picking this:
map (\<lambda>n. n < LENGTH('a) \<and> bit k n) [0..<LENGTH('a)] = map (bit k) [0..<LENGTH('a)] proof (prove)
using this:
map (\<lambda>n. n < LENGTH('a) \<and> bit k n) [0..<LENGTH('a)] = map (bit k) [0..<LENGTH('a)]

goal (1 subgoal):
 1. horner_sum of_bool 2 (map (\<lambda>n. n < LENGTH('a) \<and> bit k n) [0..<LENGTH('a)]) = take_bit LENGTH('a) k proof (state)
this:
horner_sum of_bool 2 (map (\<lambda>n. n < LENGTH('a) \<and> bit k n) [0..<LENGTH('a)]) = take_bit LENGTH('a) k

goal:
No subgoals! proof (state)
this:
horner_sum of_bool 2 (map (bit w) [0..<LENGTH('a)]) = uint w

goal (1 subgoal):
 1. \<And>a ws. horner_sum of_bool 2 (concat (map (\<lambda>x. map (bit x) [0..<LENGTH('a)]) ws)) = horner_sum uint (2 ^ LENGTH('a)) ws \<Longrightarrow> horner_sum of_bool 2 (concat (map (\<lambda>x. map (bit x) [0..<LENGTH('a)]) (a # ws))) = horner_sum uint (2 ^ LENGTH('a)) (a # ws) proof (chain)
picking this:
horner_sum of_bool 2 (concat (map (\<lambda>x. map (bit x) [0..<LENGTH('a)]) ws)) = horner_sum uint (2 ^ LENGTH('a)) ws
horner_sum of_bool 2 (map (bit w) [0..<LENGTH('a)]) = uint w proof (prove)
using this:
horner_sum of_bool 2 (concat (map (\<lambda>x. map (bit x) [0..<LENGTH('a)]) ws)) = horner_sum uint (2 ^ LENGTH('a)) ws
horner_sum of_bool 2 (map (bit w) [0..<LENGTH('a)]) = uint w

goal (1 subgoal):
 1. horner_sum of_bool 2 (concat (map (\<lambda>x. map (bit x) [0..<LENGTH('a)]) (w # ws))) = horner_sum uint (2 ^ LENGTH('a)) (w # ws) proof (state)
this:
horner_sum of_bool 2 (concat (map (\<lambda>x. map (bit x) [0..<LENGTH('a)]) (w # ws))) = horner_sum uint (2 ^ LENGTH('a)) (w # ws)

goal:
No subgoals!