theory Bit_Comprehension_Int

lemma int_set_bits_unfold_BIT:
  "set_bits f = of_bool (f 0) + (2 :: int) * set_bits (f \<circ> Suc)" using wff proof cases case (zeros n) show ?thesis proof(cases "\<forall>n. \<not> f n") case True hence "f = (\<lambda>_. False)" by auto thus ?thesis using True by(simp add: o_def) next case False then obtain n' where "f n'" by blast with zeros have "(LEAST n. \<forall>n'\<ge>n. \<not> f n') = Suc (LEAST n. \<forall>n'\<ge>Suc n. \<not> f n')" by(auto intro: Least_Suc) also have "(\<lambda>n. \<forall>n'\<ge>Suc n. \<not> f n') = (\<lambda>n. \<forall>n'\<ge>n. \<not> f (Suc n'))" by(auto dest: Suc_le_D) also from zeros have "\<forall>n'\<ge>n. \<not> f (Suc n')" by auto ultimately show ?thesis using zeros apply (simp (no_asm_simp) add: set_bits_int_unfold' exI
        del: upt.upt_Suc flip: map_map split del: if_split) apply (simp only: map_Suc_upt upt_conv_Cons) apply simp done qed next case (ones n) show ?thesis proof(cases "\<forall>n. f n") case True hence "f = (\<lambda>_. True)" by auto thus ?thesis using True by(simp add: o_def) next case False then obtain n' where "\<not> f n'" by blast with ones have "(LEAST n. \<forall>n'\<ge>n. f n') = Suc (LEAST n. \<forall>n'\<ge>Suc n. f n')" by(auto intro: Least_Suc) also have "(\<lambda>n. \<forall>n'\<ge>Suc n. f n') = (\<lambda>n. \<forall>n'\<ge>n. f (Suc n'))" by(auto dest: Suc_le_D) also from ones have "\<forall>n'\<ge>n. f (Suc n')" by auto moreover from ones have "(\<exists>n. \<forall>n'\<ge>n. \<not> f n') = False" by(auto intro!: exI[where x="max n m" for n m] simp add: max_def split: if_split_asm) moreover hence "(\<exists>n. \<forall>n'\<ge>n. \<not> f (Suc n')) = False" by(auto elim: allE[where x="Suc n" for n] dest: Suc_le_D) ultimately show ?thesis using ones apply (simp (no_asm_simp) add: set_bits_int_unfold' exI split del: if_split) apply (auto simp add: Let_def hd_map map_tl[symmetric] map_map[symmetric] map_Suc_upt upt_conv_Cons signed_take_bit_Suc
        not_le simp del: map_map) done qed qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. set_bits f = of_bool (f 0) + 2 * set_bits (f \<circ> Suc) proof (prove)
using this:
wf_set_bits_int f

goal (1 subgoal):
 1. set_bits f = of_bool (f 0) + 2 * set_bits (f \<circ> Suc) proof (state)
goal (2 subgoals):
 1. \<And>n. \<forall>n'\<ge>n. \<not> f n' \<Longrightarrow> set_bits f = of_bool (f 0) + 2 * set_bits (f \<circ> Suc)
 2. \<And>n. \<forall>n'\<ge>n. f n' \<Longrightarrow> set_bits f = of_bool (f 0) + 2 * set_bits (f \<circ> Suc) proof (state)
this:
\<forall>n'\<ge>n. \<not> f n'

goal (2 subgoals):
 1. \<And>n. \<forall>n'\<ge>n. \<not> f n' \<Longrightarrow> set_bits f = of_bool (f 0) + 2 * set_bits (f \<circ> Suc)
 2. \<And>n. \<forall>n'\<ge>n. f n' \<Longrightarrow> set_bits f = of_bool (f 0) + 2 * set_bits (f \<circ> Suc) proof (prove)
goal (1 subgoal):
 1. set_bits f = of_bool (f 0) + 2 * set_bits (f \<circ> Suc) proof (state)
goal (2 subgoals):
 1. \<forall>n. \<not> f n \<Longrightarrow> set_bits f = of_bool (f 0) + 2 * set_bits (f \<circ> Suc)
 2. \<not> (\<forall>n. \<not> f n) \<Longrightarrow> set_bits f = of_bool (f 0) + 2 * set_bits (f \<circ> Suc) proof (state)
this:
\<forall>n. \<not> f n

goal (2 subgoals):
 1. \<forall>n. \<not> f n \<Longrightarrow> set_bits f = of_bool (f 0) + 2 * set_bits (f \<circ> Suc)
 2. \<not> (\<forall>n. \<not> f n) \<Longrightarrow> set_bits f = of_bool (f 0) + 2 * set_bits (f \<circ> Suc) proof (prove)
using this:
\<forall>n. \<not> f n

goal (1 subgoal):
 1. f = (\<lambda>_. False) proof (state)
this:
f = (\<lambda>_. False)

goal (2 subgoals):
 1. \<forall>n. \<not> f n \<Longrightarrow> set_bits f = of_bool (f 0) + 2 * set_bits (f \<circ> Suc)
 2. \<not> (\<forall>n. \<not> f n) \<Longrightarrow> set_bits f = of_bool (f 0) + 2 * set_bits (f \<circ> Suc) proof (prove)
using this:
f = (\<lambda>_. False)

goal (1 subgoal):
 1. set_bits f = of_bool (f 0) + 2 * set_bits (f \<circ> Suc) proof (prove)
using this:
f = (\<lambda>_. False)
\<forall>n. \<not> f n

goal (1 subgoal):
 1. set_bits f = of_bool (f 0) + 2 * set_bits (f \<circ> Suc) proof (state)
this:
set_bits f = of_bool (f 0) + 2 * set_bits (f \<circ> Suc)

goal (1 subgoal):
 1. \<not> (\<forall>n. \<not> f n) \<Longrightarrow> set_bits f = of_bool (f 0) + 2 * set_bits (f \<circ> Suc) proof (state)
goal (1 subgoal):
 1. \<not> (\<forall>n. \<not> f n) \<Longrightarrow> set_bits f = of_bool (f 0) + 2 * set_bits (f \<circ> Suc) proof (state)
this:
\<not> (\<forall>n. \<not> f n)

goal (1 subgoal):
 1. \<not> (\<forall>n. \<not> f n) \<Longrightarrow> set_bits f = of_bool (f 0) + 2 * set_bits (f \<circ> Suc) proof (chain)
picking this:
\<not> (\<forall>n. \<not> f n) proof (prove)
using this:
\<not> (\<forall>n. \<not> f n)

goal (1 subgoal):
 1. (\<And>n'. f n' \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (state)
this:
f n'

goal (1 subgoal):
 1. \<not> (\<forall>n. \<not> f n) \<Longrightarrow> set_bits f = of_bool (f 0) + 2 * set_bits (f \<circ> Suc) proof (chain)
picking this:
\<forall>n'\<ge>n. \<not> f n'
f n' proof (prove)
using this:
\<forall>n'\<ge>n. \<not> f n'
f n'

goal (1 subgoal):
 1. (LEAST n. \<forall>n'\<ge>n. \<not> f n') = Suc (LEAST n. \<forall>n'\<ge>Suc n. \<not> f n') proof (state)
this:
(LEAST n. \<forall>n'\<ge>n. \<not> f n') = Suc (LEAST n. \<forall>n'\<ge>Suc n. \<not> f n')

goal (1 subgoal):
 1. \<not> (\<forall>n. \<not> f n) \<Longrightarrow> set_bits f = of_bool (f 0) + 2 * set_bits (f \<circ> Suc) proof (state)
this:
(LEAST n. \<forall>n'\<ge>n. \<not> f n') = Suc (LEAST n. \<forall>n'\<ge>Suc n. \<not> f n')

goal (1 subgoal):
 1. \<not> (\<forall>n. \<not> f n) \<Longrightarrow> set_bits f = of_bool (f 0) + 2 * set_bits (f \<circ> Suc) proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. \<forall>n'\<ge>Suc n. \<not> f n') = (\<lambda>n. \<forall>n'\<ge>n. \<not> f (Suc n')) proof (state)
this:
(\<lambda>n. \<forall>n'\<ge>Suc n. \<not> f n') = (\<lambda>n. \<forall>n'\<ge>n. \<not> f (Suc n'))

goal (1 subgoal):
 1. \<not> (\<forall>n. \<not> f n) \<Longrightarrow> set_bits f = of_bool (f 0) + 2 * set_bits (f \<circ> Suc) proof (state)
this:
(\<lambda>n. \<forall>n'\<ge>Suc n. \<not> f n') = (\<lambda>n. \<forall>n'\<ge>n. \<not> f (Suc n'))

goal (1 subgoal):
 1. \<not> (\<forall>n. \<not> f n) \<Longrightarrow> set_bits f = of_bool (f 0) + 2 * set_bits (f \<circ> Suc) proof (chain)
picking this:
\<forall>n'\<ge>n. \<not> f n' proof (prove)
using this:
\<forall>n'\<ge>n. \<not> f n'

goal (1 subgoal):
 1. \<forall>n'\<ge>n. \<not> f (Suc n') proof (state)
this:
\<forall>n'\<ge>n. \<not> f (Suc n')

goal (1 subgoal):
 1. \<not> (\<forall>n. \<not> f n) \<Longrightarrow> set_bits f = of_bool (f 0) + 2 * set_bits (f \<circ> Suc) proof (chain)
picking this:
(LEAST n. \<forall>n'\<ge>n. \<not> f n') = Suc (LEAST n. \<forall>n'\<ge>n. \<not> f (Suc n'))
\<forall>n'\<ge>n. \<not> f (Suc n') proof (prove)
using this:
(LEAST n. \<forall>n'\<ge>n. \<not> f n') = Suc (LEAST n. \<forall>n'\<ge>n. \<not> f (Suc n'))
\<forall>n'\<ge>n. \<not> f (Suc n')

goal (1 subgoal):
 1. set_bits f = of_bool (f 0) + 2 * set_bits (f \<circ> Suc) proof (prove)
using this:
(LEAST n. \<forall>n'\<ge>n. \<not> f n') = Suc (LEAST n. \<forall>n'\<ge>n. \<not> f (Suc n'))
\<forall>n'\<ge>n. \<not> f (Suc n')
\<forall>n'\<ge>n. \<not> f n'

goal (1 subgoal):
 1. set_bits f = of_bool (f 0) + 2 * set_bits (f \<circ> Suc) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(LEAST n. \<forall>n'\<ge>n. \<not> f n') = Suc (LEAST n. \<forall>n'\<ge>n. \<not> f (Suc n')); \<forall>n'\<ge>n. \<not> f (Suc n'); \<forall>n'\<ge>n. \<not> f n'\<rbrakk> \<Longrightarrow> (f 0 \<longrightarrow> horner_sum of_bool 2 (map f [0..<Suc (LEAST n. \<forall>n'\<ge>n. \<not> f (Suc n'))]) = 1 + 2 * horner_sum of_bool 2 (map f (map Suc [0..<LEAST n. \<forall>n'\<ge>n. \<not> f (Suc n')]))) \<and> (\<not> f 0 \<longrightarrow> horner_sum of_bool 2 (map f [0..<Suc (LEAST n. \<forall>n'\<ge>n. \<not> f (Suc n'))]) = 2 * horner_sum of_bool 2 (map f (map Suc [0..<LEAST n. \<forall>n'\<ge>n. \<not> f (Suc n')]))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(LEAST n. \<forall>n'\<ge>n. \<not> f n') = Suc (LEAST n. \<forall>n'\<ge>n. \<not> f (Suc n')); \<forall>n'\<ge>n. \<not> f (Suc n'); \<forall>n'\<ge>n. \<not> f n'\<rbrakk> \<Longrightarrow> (f 0 \<longrightarrow> horner_sum of_bool 2 (map f (0 # [Suc 0..<Suc (LEAST n. \<forall>n'\<ge>n. \<not> f (Suc n'))])) = 1 + 2 * horner_sum of_bool 2 (map f [Suc 0..<Suc (LEAST n. \<forall>n'\<ge>n. \<not> f (Suc n'))])) \<and> (\<not> f 0 \<longrightarrow> horner_sum of_bool 2 (map f (0 # [Suc 0..<Suc (LEAST n. \<forall>n'\<ge>n. \<not> f (Suc n'))])) = 2 * horner_sum of_bool 2 (map f [Suc 0..<Suc (LEAST n. \<forall>n'\<ge>n. \<not> f (Suc n'))])) proof (prove)
goal:
No subgoals! proof (state)
this:
set_bits f = of_bool (f 0) + 2 * set_bits (f \<circ> Suc)

goal:
No subgoals! proof (state)
this:
set_bits f = of_bool (f 0) + 2 * set_bits (f \<circ> Suc)

goal (1 subgoal):
 1. \<And>n. \<forall>n'\<ge>n. f n' \<Longrightarrow> set_bits f = of_bool (f 0) + 2 * set_bits (f \<circ> Suc) proof (state)
goal (1 subgoal):
 1. \<And>n. \<forall>n'\<ge>n. f n' \<Longrightarrow> set_bits f = of_bool (f 0) + 2 * set_bits (f \<circ> Suc) proof (state)
this:
\<forall>n'\<ge>n. f n'

goal (1 subgoal):
 1. \<And>n. \<forall>n'\<ge>n. f n' \<Longrightarrow> set_bits f = of_bool (f 0) + 2 * set_bits (f \<circ> Suc) proof (prove)
goal (1 subgoal):
 1. set_bits f = of_bool (f 0) + 2 * set_bits (f \<circ> Suc) proof (state)
goal (2 subgoals):
 1. \<forall>n. f n \<Longrightarrow> set_bits f = of_bool (f 0) + 2 * set_bits (f \<circ> Suc)
 2. \<not> (\<forall>n. f n) \<Longrightarrow> set_bits f = of_bool (f 0) + 2 * set_bits (f \<circ> Suc) proof (state)
this:
\<forall>n. f n

goal (2 subgoals):
 1. \<forall>n. f n \<Longrightarrow> set_bits f = of_bool (f 0) + 2 * set_bits (f \<circ> Suc)
 2. \<not> (\<forall>n. f n) \<Longrightarrow> set_bits f = of_bool (f 0) + 2 * set_bits (f \<circ> Suc) proof (prove)
using this:
\<forall>n. f n

goal (1 subgoal):
 1. f = (\<lambda>_. True) proof (state)
this:
f = (\<lambda>_. True)

goal (2 subgoals):
 1. \<forall>n. f n \<Longrightarrow> set_bits f = of_bool (f 0) + 2 * set_bits (f \<circ> Suc)
 2. \<not> (\<forall>n. f n) \<Longrightarrow> set_bits f = of_bool (f 0) + 2 * set_bits (f \<circ> Suc) proof (prove)
using this:
f = (\<lambda>_. True)

goal (1 subgoal):
 1. set_bits f = of_bool (f 0) + 2 * set_bits (f \<circ> Suc) proof (prove)
using this:
f = (\<lambda>_. True)
\<forall>n. f n

goal (1 subgoal):
 1. set_bits f = of_bool (f 0) + 2 * set_bits (f \<circ> Suc) proof (state)
this:
set_bits f = of_bool (f 0) + 2 * set_bits (f \<circ> Suc)

goal (1 subgoal):
 1. \<not> (\<forall>n. f n) \<Longrightarrow> set_bits f = of_bool (f 0) + 2 * set_bits (f \<circ> Suc) proof (state)
goal (1 subgoal):
 1. \<not> (\<forall>n. f n) \<Longrightarrow> set_bits f = of_bool (f 0) + 2 * set_bits (f \<circ> Suc) proof (state)
this:
\<not> (\<forall>n. f n)

goal (1 subgoal):
 1. \<not> (\<forall>n. f n) \<Longrightarrow> set_bits f = of_bool (f 0) + 2 * set_bits (f \<circ> Suc) proof (chain)
picking this:
\<not> (\<forall>n. f n) proof (prove)
using this:
\<not> (\<forall>n. f n)

goal (1 subgoal):
 1. (\<And>n'. \<not> f n' \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (state)
this:
\<not> f n'

goal (1 subgoal):
 1. \<not> (\<forall>n. f n) \<Longrightarrow> set_bits f = of_bool (f 0) + 2 * set_bits (f \<circ> Suc) proof (chain)
picking this:
\<forall>n'\<ge>n. f n'
\<not> f n' proof (prove)
using this:
\<forall>n'\<ge>n. f n'
\<not> f n'

goal (1 subgoal):
 1. (LEAST n. \<forall>n'\<ge>n. f n') = Suc (LEAST n. \<forall>n'\<ge>Suc n. f n') proof (state)
this:
(LEAST n. \<forall>n'\<ge>n. f n') = Suc (LEAST n. \<forall>n'\<ge>Suc n. f n')

goal (1 subgoal):
 1. \<not> (\<forall>n. f n) \<Longrightarrow> set_bits f = of_bool (f 0) + 2 * set_bits (f \<circ> Suc) proof (state)
this:
(LEAST n. \<forall>n'\<ge>n. f n') = Suc (LEAST n. \<forall>n'\<ge>Suc n. f n')

goal (1 subgoal):
 1. \<not> (\<forall>n. f n) \<Longrightarrow> set_bits f = of_bool (f 0) + 2 * set_bits (f \<circ> Suc) proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. \<forall>n'\<ge>Suc n. f n') = (\<lambda>n. \<forall>n'\<ge>n. f (Suc n')) proof (state)
this:
(\<lambda>n. \<forall>n'\<ge>Suc n. f n') = (\<lambda>n. \<forall>n'\<ge>n. f (Suc n'))

goal (1 subgoal):
 1. \<not> (\<forall>n. f n) \<Longrightarrow> set_bits f = of_bool (f 0) + 2 * set_bits (f \<circ> Suc) proof (state)
this:
(\<lambda>n. \<forall>n'\<ge>Suc n. f n') = (\<lambda>n. \<forall>n'\<ge>n. f (Suc n'))

goal (1 subgoal):
 1. \<not> (\<forall>n. f n) \<Longrightarrow> set_bits f = of_bool (f 0) + 2 * set_bits (f \<circ> Suc) proof (chain)
picking this:
\<forall>n'\<ge>n. f n' proof (prove)
using this:
\<forall>n'\<ge>n. f n'

goal (1 subgoal):
 1. \<forall>n'\<ge>n. f (Suc n') proof (state)
this:
\<forall>n'\<ge>n. f (Suc n')

goal (1 subgoal):
 1. \<not> (\<forall>n. f n) \<Longrightarrow> set_bits f = of_bool (f 0) + 2 * set_bits (f \<circ> Suc) proof (state)
this:
\<forall>n'\<ge>n. f (Suc n')

goal (1 subgoal):
 1. \<not> (\<forall>n. f n) \<Longrightarrow> set_bits f = of_bool (f 0) + 2 * set_bits (f \<circ> Suc) proof (chain)
picking this:
\<forall>n'\<ge>n. f n' proof (prove)
using this:
\<forall>n'\<ge>n. f n'

goal (1 subgoal):
 1. (\<exists>n. \<forall>n'\<ge>n. \<not> f n') = False proof (state)
this:
(\<exists>n. \<forall>n'\<ge>n. \<not> f n') = False

goal (1 subgoal):
 1. \<not> (\<forall>n. f n) \<Longrightarrow> set_bits f = of_bool (f 0) + 2 * set_bits (f \<circ> Suc) proof (state)
this:
(\<exists>n. \<forall>n'\<ge>n. \<not> f n') = False

goal (1 subgoal):
 1. \<not> (\<forall>n. f n) \<Longrightarrow> set_bits f = of_bool (f 0) + 2 * set_bits (f \<circ> Suc) proof (prove)
using this:
(\<exists>n. \<forall>n'\<ge>n. \<not> f n') = False

goal (1 subgoal):
 1. (\<exists>n. \<forall>n'\<ge>n. \<not> f (Suc n')) = False proof (state)
this:
(\<exists>n. \<forall>n'\<ge>n. \<not> f (Suc n')) = False

goal (1 subgoal):
 1. \<not> (\<forall>n. f n) \<Longrightarrow> set_bits f = of_bool (f 0) + 2 * set_bits (f \<circ> Suc) proof (chain)
picking this:
(LEAST n. \<forall>n'\<ge>n. f n') = Suc (LEAST n. \<forall>n'\<ge>n. f (Suc n'))
\<forall>n'\<ge>n. f (Suc n')
(\<exists>n. \<forall>n'\<ge>n. \<not> f n') = False
(\<exists>n. \<forall>n'\<ge>n. \<not> f (Suc n')) = False proof (prove)
using this:
(LEAST n. \<forall>n'\<ge>n. f n') = Suc (LEAST n. \<forall>n'\<ge>n. f (Suc n'))
\<forall>n'\<ge>n. f (Suc n')
(\<exists>n. \<forall>n'\<ge>n. \<not> f n') = False
(\<exists>n. \<forall>n'\<ge>n. \<not> f (Suc n')) = False

goal (1 subgoal):
 1. set_bits f = of_bool (f 0) + 2 * set_bits (f \<circ> Suc) proof (prove)
using this:
(LEAST n. \<forall>n'\<ge>n. f n') = Suc (LEAST n. \<forall>n'\<ge>n. f (Suc n'))
\<forall>n'\<ge>n. f (Suc n')
(\<exists>n. \<forall>n'\<ge>n. \<not> f n') = False
(\<exists>n. \<forall>n'\<ge>n. \<not> f (Suc n')) = False
\<forall>n'\<ge>n. f n'

goal (1 subgoal):
 1. set_bits f = of_bool (f 0) + 2 * set_bits (f \<circ> Suc) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(LEAST n. \<forall>n'\<ge>n. f n') = Suc (LEAST n. \<forall>n'\<ge>n. f (Suc n')); \<forall>n'\<ge>n. f (Suc n'); (\<exists>n. \<forall>n'\<ge>n. \<not> f n') = False; (\<exists>n. \<forall>n'\<ge>n. \<not> f (Suc n')) = False; \<forall>n'\<ge>n. f n'\<rbrakk> \<Longrightarrow> (f 0 \<longrightarrow> signed_take_bit (Suc (LEAST n. \<forall>n'\<ge>n. f (Suc n'))) (horner_sum of_bool 2 (map f [0..<LEAST n. \<forall>n'\<ge>n. f (Suc n')] @ [f (LEAST n. \<forall>n'\<ge>n. f (Suc n')), True])) = 1 + 2 * (let n = LEAST n. \<forall>n'\<ge>n. f (Suc n') in signed_take_bit n (horner_sum of_bool 2 (map (f \<circ> Suc) [0..<n] @ [True])))) \<and> (\<not> f 0 \<longrightarrow> signed_take_bit (Suc (LEAST n. \<forall>n'\<ge>n. f (Suc n'))) (horner_sum of_bool 2 (map f [0..<LEAST n. \<forall>n'\<ge>n. f (Suc n')] @ [f (LEAST n. \<forall>n'\<ge>n. f (Suc n')), True])) = 2 * (let n = LEAST n. \<forall>n'\<ge>n. f (Suc n') in signed_take_bit n (horner_sum of_bool 2 (map (f \<circ> Suc) [0..<n] @ [True])))) proof (prove)
goal:
No subgoals! proof (state)
this:
set_bits f = of_bool (f 0) + 2 * set_bits (f \<circ> Suc)

goal:
No subgoals! proof (state)
this:
set_bits f = of_bool (f 0) + 2 * set_bits (f \<circ> Suc)

goal:
No subgoals!