theory Bit_Comprehension_Int

lemma set_bits_int_unfold':
  \<open>set_bits f =
    (if \<exists>n. \<forall>n'\<ge>n. \<not> f n' then
      let n = LEAST n. \<forall>n'\<ge>n. \<not> f n'
      in horner_sum of_bool 2 (map f [0..<n])
     else if \<exists>n. \<forall>n'\<ge>n. f n' then
      let n = LEAST n. \<forall>n'\<ge>n. f n'
      in signed_take_bit n (horner_sum of_bool 2 (map f [0..<n] @ [True]))
     else 0 :: int)\<close> proof (cases \<open>\<exists>n. \<forall>m\<ge>n. f m \<longleftrightarrow> f n\<close>) case True then obtain q where q: \<open>\<forall>m\<ge>q. f m \<longleftrightarrow> f q\<close> by blast define n where \<open>n = (LEAST n. \<forall>m\<ge>n. f m \<longleftrightarrow> f n)\<close> have \<open>\<forall>m\<ge>n. f m \<longleftrightarrow> f n\<close> unfolding n_def using q by (rule LeastI [of _ q]) then have n: \<open>\<And>m. n \<le> m \<Longrightarrow> f m \<longleftrightarrow> f n\<close> by blast from n_def have n_eq: \<open>(LEAST q. \<forall>m\<ge>q. f m \<longleftrightarrow> f n) = n\<close> by (smt (verit, best) Least_le \<open>\<forall>m\<ge>n. f m = f n\<close> dual_order.antisym wellorder_Least_lemma(1)) show ?thesis proof (cases \<open>f n\<close>) case False with n have *: \<open>\<exists>n. \<forall>n'\<ge>n. \<not> f n'\<close> by blast have **: \<open>(LEAST n. \<forall>n'\<ge>n. \<not> f n') = n\<close> using False n_eq by simp from * False show ?thesis apply (simp add: set_bits_int_def n_def [symmetric] ** del: upt.upt_Suc) apply (auto simp add: take_bit_horner_sum_bit_eq
      bit_horner_sum_bit_iff take_map
      signed_take_bit_def set_bits_int_def
      horner_sum_bit_eq_take_bit simp del: upt.upt_Suc) done next case True with n have *: \<open>\<exists>n. \<forall>n'\<ge>n. f n'\<close> by blast have ***: \<open>\<not> (\<exists>n. \<forall>n'\<ge>n. \<not> f n')\<close> apply (rule ccontr) using * nat_le_linear by auto have **: \<open>(LEAST n. \<forall>n'\<ge>n. f n') = n\<close> using True n_eq by simp from * *** True show ?thesis apply (simp add: set_bits_int_def n_def [symmetric] ** del: upt.upt_Suc) apply (auto simp add: take_bit_horner_sum_bit_eq
      bit_horner_sum_bit_iff take_map
      signed_take_bit_def set_bits_int_def
      horner_sum_bit_eq_take_bit nth_append simp del: upt.upt_Suc) done qed next case False then show ?thesis by (auto simp add: set_bits_int_def) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. set_bits f = (if \<exists>n. \<forall>n'\<ge>n. \<not> f n' then let n = LEAST n. \<forall>n'\<ge>n. \<not> f n' in horner_sum of_bool 2 (map f [0..<n]) else if \<exists>n. \<forall>n'\<ge>n. f n' then let n = LEAST n. \<forall>n'\<ge>n. f n' in signed_take_bit n (horner_sum of_bool 2 (map f [0..<n] @ [True])) else 0) proof (state)
goal (2 subgoals):
 1. \<exists>n. \<forall>m\<ge>n. f m = f n \<Longrightarrow> set_bits f = (if \<exists>n. \<forall>n'\<ge>n. \<not> f n' then let n = LEAST n. \<forall>n'\<ge>n. \<not> f n' in horner_sum of_bool 2 (map f [0..<n]) else if \<exists>n. \<forall>n'\<ge>n. f n' then let n = LEAST n. \<forall>n'\<ge>n. f n' in signed_take_bit n (horner_sum of_bool 2 (map f [0..<n] @ [True])) else 0)
 2. \<nexists>n. \<forall>m\<ge>n. f m = f n \<Longrightarrow> set_bits f = (if \<exists>n. \<forall>n'\<ge>n. \<not> f n' then let n = LEAST n. \<forall>n'\<ge>n. \<not> f n' in horner_sum of_bool 2 (map f [0..<n]) else if \<exists>n. \<forall>n'\<ge>n. f n' then let n = LEAST n. \<forall>n'\<ge>n. f n' in signed_take_bit n (horner_sum of_bool 2 (map f [0..<n] @ [True])) else 0) proof (state)
this:
\<exists>n. \<forall>m\<ge>n. f m = f n

goal (2 subgoals):
 1. \<exists>n. \<forall>m\<ge>n. f m = f n \<Longrightarrow> set_bits f = (if \<exists>n. \<forall>n'\<ge>n. \<not> f n' then let n = LEAST n. \<forall>n'\<ge>n. \<not> f n' in horner_sum of_bool 2 (map f [0..<n]) else if \<exists>n. \<forall>n'\<ge>n. f n' then let n = LEAST n. \<forall>n'\<ge>n. f n' in signed_take_bit n (horner_sum of_bool 2 (map f [0..<n] @ [True])) else 0)
 2. \<nexists>n. \<forall>m\<ge>n. f m = f n \<Longrightarrow> set_bits f = (if \<exists>n. \<forall>n'\<ge>n. \<not> f n' then let n = LEAST n. \<forall>n'\<ge>n. \<not> f n' in horner_sum of_bool 2 (map f [0..<n]) else if \<exists>n. \<forall>n'\<ge>n. f n' then let n = LEAST n. \<forall>n'\<ge>n. f n' in signed_take_bit n (horner_sum of_bool 2 (map f [0..<n] @ [True])) else 0) proof (chain)
picking this:
\<exists>n. \<forall>m\<ge>n. f m = f n proof (prove)
using this:
\<exists>n. \<forall>m\<ge>n. f m = f n

goal (1 subgoal):
 1. (\<And>q. \<forall>m\<ge>q. f m = f q \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (state)
this:
\<forall>m\<ge>q. f m = f q

goal (2 subgoals):
 1. \<exists>n. \<forall>m\<ge>n. f m = f n \<Longrightarrow> set_bits f = (if \<exists>n. \<forall>n'\<ge>n. \<not> f n' then let n = LEAST n. \<forall>n'\<ge>n. \<not> f n' in horner_sum of_bool 2 (map f [0..<n]) else if \<exists>n. \<forall>n'\<ge>n. f n' then let n = LEAST n. \<forall>n'\<ge>n. f n' in signed_take_bit n (horner_sum of_bool 2 (map f [0..<n] @ [True])) else 0)
 2. \<nexists>n. \<forall>m\<ge>n. f m = f n \<Longrightarrow> set_bits f = (if \<exists>n. \<forall>n'\<ge>n. \<not> f n' then let n = LEAST n. \<forall>n'\<ge>n. \<not> f n' in horner_sum of_bool 2 (map f [0..<n]) else if \<exists>n. \<forall>n'\<ge>n. f n' then let n = LEAST n. \<forall>n'\<ge>n. f n' in signed_take_bit n (horner_sum of_bool 2 (map f [0..<n] @ [True])) else 0) proof (state)
this:
n = (LEAST n. \<forall>m\<ge>n. f m = f n)

goal (2 subgoals):
 1. \<exists>n. \<forall>m\<ge>n. f m = f n \<Longrightarrow> set_bits f = (if \<exists>n. \<forall>n'\<ge>n. \<not> f n' then let n = LEAST n. \<forall>n'\<ge>n. \<not> f n' in horner_sum of_bool 2 (map f [0..<n]) else if \<exists>n. \<forall>n'\<ge>n. f n' then let n = LEAST n. \<forall>n'\<ge>n. f n' in signed_take_bit n (horner_sum of_bool 2 (map f [0..<n] @ [True])) else 0)
 2. \<nexists>n. \<forall>m\<ge>n. f m = f n \<Longrightarrow> set_bits f = (if \<exists>n. \<forall>n'\<ge>n. \<not> f n' then let n = LEAST n. \<forall>n'\<ge>n. \<not> f n' in horner_sum of_bool 2 (map f [0..<n]) else if \<exists>n. \<forall>n'\<ge>n. f n' then let n = LEAST n. \<forall>n'\<ge>n. f n' in signed_take_bit n (horner_sum of_bool 2 (map f [0..<n] @ [True])) else 0) proof (prove)
goal (1 subgoal):
 1. \<forall>m\<ge>n. f m = f n proof (prove)
goal (1 subgoal):
 1. \<forall>m\<ge>LEAST n. \<forall>m\<ge>n. f m = f n. f m = f (LEAST n. \<forall>m\<ge>n. f m = f n) proof (prove)
using this:
\<forall>m\<ge>q. f m = f q

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

goal (2 subgoals):
 1. \<exists>n. \<forall>m\<ge>n. f m = f n \<Longrightarrow> set_bits f = (if \<exists>n. \<forall>n'\<ge>n. \<not> f n' then let n = LEAST n. \<forall>n'\<ge>n. \<not> f n' in horner_sum of_bool 2 (map f [0..<n]) else if \<exists>n. \<forall>n'\<ge>n. f n' then let n = LEAST n. \<forall>n'\<ge>n. f n' in signed_take_bit n (horner_sum of_bool 2 (map f [0..<n] @ [True])) else 0)
 2. \<nexists>n. \<forall>m\<ge>n. f m = f n \<Longrightarrow> set_bits f = (if \<exists>n. \<forall>n'\<ge>n. \<not> f n' then let n = LEAST n. \<forall>n'\<ge>n. \<not> f n' in horner_sum of_bool 2 (map f [0..<n]) else if \<exists>n. \<forall>n'\<ge>n. f n' then let n = LEAST n. \<forall>n'\<ge>n. f n' in signed_take_bit n (horner_sum of_bool 2 (map f [0..<n] @ [True])) else 0) proof (chain)
picking this:
\<forall>m\<ge>n. f m = f n proof (prove)
using this:
\<forall>m\<ge>n. f m = f n

goal (1 subgoal):
 1. \<And>m. n \<le> m \<Longrightarrow> f m = f n proof (state)
this:
n \<le> ?m \<Longrightarrow> f ?m = f n

goal (2 subgoals):
 1. \<exists>n. \<forall>m\<ge>n. f m = f n \<Longrightarrow> set_bits f = (if \<exists>n. \<forall>n'\<ge>n. \<not> f n' then let n = LEAST n. \<forall>n'\<ge>n. \<not> f n' in horner_sum of_bool 2 (map f [0..<n]) else if \<exists>n. \<forall>n'\<ge>n. f n' then let n = LEAST n. \<forall>n'\<ge>n. f n' in signed_take_bit n (horner_sum of_bool 2 (map f [0..<n] @ [True])) else 0)
 2. \<nexists>n. \<forall>m\<ge>n. f m = f n \<Longrightarrow> set_bits f = (if \<exists>n. \<forall>n'\<ge>n. \<not> f n' then let n = LEAST n. \<forall>n'\<ge>n. \<not> f n' in horner_sum of_bool 2 (map f [0..<n]) else if \<exists>n. \<forall>n'\<ge>n. f n' then let n = LEAST n. \<forall>n'\<ge>n. f n' in signed_take_bit n (horner_sum of_bool 2 (map f [0..<n] @ [True])) else 0) proof (chain)
picking this:
n = (LEAST n. \<forall>m\<ge>n. f m = f n) proof (prove)
using this:
n = (LEAST n. \<forall>m\<ge>n. f m = f n)

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

goal (2 subgoals):
 1. \<exists>n. \<forall>m\<ge>n. f m = f n \<Longrightarrow> set_bits f = (if \<exists>n. \<forall>n'\<ge>n. \<not> f n' then let n = LEAST n. \<forall>n'\<ge>n. \<not> f n' in horner_sum of_bool 2 (map f [0..<n]) else if \<exists>n. \<forall>n'\<ge>n. f n' then let n = LEAST n. \<forall>n'\<ge>n. f n' in signed_take_bit n (horner_sum of_bool 2 (map f [0..<n] @ [True])) else 0)
 2. \<nexists>n. \<forall>m\<ge>n. f m = f n \<Longrightarrow> set_bits f = (if \<exists>n. \<forall>n'\<ge>n. \<not> f n' then let n = LEAST n. \<forall>n'\<ge>n. \<not> f n' in horner_sum of_bool 2 (map f [0..<n]) else if \<exists>n. \<forall>n'\<ge>n. f n' then let n = LEAST n. \<forall>n'\<ge>n. f n' in signed_take_bit n (horner_sum of_bool 2 (map f [0..<n] @ [True])) else 0) proof (prove)
goal (1 subgoal):
 1. set_bits f = (if \<exists>n. \<forall>n'\<ge>n. \<not> f n' then let n = LEAST n. \<forall>n'\<ge>n. \<not> f n' in horner_sum of_bool 2 (map f [0..<n]) else if \<exists>n. \<forall>n'\<ge>n. f n' then let n = LEAST n. \<forall>n'\<ge>n. f n' in signed_take_bit n (horner_sum of_bool 2 (map f [0..<n] @ [True])) else 0) proof (state)
goal (2 subgoals):
 1. f n \<Longrightarrow> set_bits f = (if \<exists>n. \<forall>n'\<ge>n. \<not> f n' then let n = LEAST n. \<forall>n'\<ge>n. \<not> f n' in horner_sum of_bool 2 (map f [0..<n]) else if \<exists>n. \<forall>n'\<ge>n. f n' then let n = LEAST n. \<forall>n'\<ge>n. f n' in signed_take_bit n (horner_sum of_bool 2 (map f [0..<n] @ [True])) else 0)
 2. \<not> f n \<Longrightarrow> set_bits f = (if \<exists>n. \<forall>n'\<ge>n. \<not> f n' then let n = LEAST n. \<forall>n'\<ge>n. \<not> f n' in horner_sum of_bool 2 (map f [0..<n]) else if \<exists>n. \<forall>n'\<ge>n. f n' then let n = LEAST n. \<forall>n'\<ge>n. f n' in signed_take_bit n (horner_sum of_bool 2 (map f [0..<n] @ [True])) else 0) proof (state)
this:
\<not> f n

goal (2 subgoals):
 1. f n \<Longrightarrow> set_bits f = (if \<exists>n. \<forall>n'\<ge>n. \<not> f n' then let n = LEAST n. \<forall>n'\<ge>n. \<not> f n' in horner_sum of_bool 2 (map f [0..<n]) else if \<exists>n. \<forall>n'\<ge>n. f n' then let n = LEAST n. \<forall>n'\<ge>n. f n' in signed_take_bit n (horner_sum of_bool 2 (map f [0..<n] @ [True])) else 0)
 2. \<not> f n \<Longrightarrow> set_bits f = (if \<exists>n. \<forall>n'\<ge>n. \<not> f n' then let n = LEAST n. \<forall>n'\<ge>n. \<not> f n' in horner_sum of_bool 2 (map f [0..<n]) else if \<exists>n. \<forall>n'\<ge>n. f n' then let n = LEAST n. \<forall>n'\<ge>n. f n' in signed_take_bit n (horner_sum of_bool 2 (map f [0..<n] @ [True])) else 0) proof (chain)
picking this:
n \<le> ?m \<Longrightarrow> f ?m = f n
\<not> f n proof (prove)
using this:
n \<le> ?m \<Longrightarrow> f ?m = f n
\<not> f n

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

goal (2 subgoals):
 1. f n \<Longrightarrow> set_bits f = (if \<exists>n. \<forall>n'\<ge>n. \<not> f n' then let n = LEAST n. \<forall>n'\<ge>n. \<not> f n' in horner_sum of_bool 2 (map f [0..<n]) else if \<exists>n. \<forall>n'\<ge>n. f n' then let n = LEAST n. \<forall>n'\<ge>n. f n' in signed_take_bit n (horner_sum of_bool 2 (map f [0..<n] @ [True])) else 0)
 2. \<not> f n \<Longrightarrow> set_bits f = (if \<exists>n. \<forall>n'\<ge>n. \<not> f n' then let n = LEAST n. \<forall>n'\<ge>n. \<not> f n' in horner_sum of_bool 2 (map f [0..<n]) else if \<exists>n. \<forall>n'\<ge>n. f n' then let n = LEAST n. \<forall>n'\<ge>n. f n' in signed_take_bit n (horner_sum of_bool 2 (map f [0..<n] @ [True])) else 0) proof (prove)
goal (1 subgoal):
 1. (LEAST n. \<forall>n'\<ge>n. \<not> f n') = n proof (prove)
using this:
\<not> f n
(LEAST q. \<forall>m\<ge>q. f m = f n) = n

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

goal (2 subgoals):
 1. f n \<Longrightarrow> set_bits f = (if \<exists>n. \<forall>n'\<ge>n. \<not> f n' then let n = LEAST n. \<forall>n'\<ge>n. \<not> f n' in horner_sum of_bool 2 (map f [0..<n]) else if \<exists>n. \<forall>n'\<ge>n. f n' then let n = LEAST n. \<forall>n'\<ge>n. f n' in signed_take_bit n (horner_sum of_bool 2 (map f [0..<n] @ [True])) else 0)
 2. \<not> f n \<Longrightarrow> set_bits f = (if \<exists>n. \<forall>n'\<ge>n. \<not> f n' then let n = LEAST n. \<forall>n'\<ge>n. \<not> f n' in horner_sum of_bool 2 (map f [0..<n]) else if \<exists>n. \<forall>n'\<ge>n. f n' then let n = LEAST n. \<forall>n'\<ge>n. f n' in signed_take_bit n (horner_sum of_bool 2 (map f [0..<n] @ [True])) else 0) proof (chain)
picking this:
\<exists>n. \<forall>n'\<ge>n. \<not> f n'
\<not> f n proof (prove)
using this:
\<exists>n. \<forall>n'\<ge>n. \<not> f n'
\<not> f n

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

goal (1 subgoal):
 1. f n \<Longrightarrow> set_bits f = (if \<exists>n. \<forall>n'\<ge>n. \<not> f n' then let n = LEAST n. \<forall>n'\<ge>n. \<not> f n' in horner_sum of_bool 2 (map f [0..<n]) else if \<exists>n. \<forall>n'\<ge>n. f n' then let n = LEAST n. \<forall>n'\<ge>n. f n' in signed_take_bit n (horner_sum of_bool 2 (map f [0..<n] @ [True])) else 0) proof (state)
goal (1 subgoal):
 1. f n \<Longrightarrow> set_bits f = (if \<exists>n. \<forall>n'\<ge>n. \<not> f n' then let n = LEAST n. \<forall>n'\<ge>n. \<not> f n' in horner_sum of_bool 2 (map f [0..<n]) else if \<exists>n. \<forall>n'\<ge>n. f n' then let n = LEAST n. \<forall>n'\<ge>n. f n' in signed_take_bit n (horner_sum of_bool 2 (map f [0..<n] @ [True])) else 0) proof (state)
this:
f n

goal (1 subgoal):
 1. f n \<Longrightarrow> set_bits f = (if \<exists>n. \<forall>n'\<ge>n. \<not> f n' then let n = LEAST n. \<forall>n'\<ge>n. \<not> f n' in horner_sum of_bool 2 (map f [0..<n]) else if \<exists>n. \<forall>n'\<ge>n. f n' then let n = LEAST n. \<forall>n'\<ge>n. f n' in signed_take_bit n (horner_sum of_bool 2 (map f [0..<n] @ [True])) else 0) proof (chain)
picking this:
n \<le> ?m \<Longrightarrow> f ?m = f n
f n proof (prove)
using this:
n \<le> ?m \<Longrightarrow> f ?m = f n
f n

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

goal (1 subgoal):
 1. f n \<Longrightarrow> set_bits f = (if \<exists>n. \<forall>n'\<ge>n. \<not> f n' then let n = LEAST n. \<forall>n'\<ge>n. \<not> f n' in horner_sum of_bool 2 (map f [0..<n]) else if \<exists>n. \<forall>n'\<ge>n. f n' then let n = LEAST n. \<forall>n'\<ge>n. f n' in signed_take_bit n (horner_sum of_bool 2 (map f [0..<n] @ [True])) else 0) proof (prove)
goal (1 subgoal):
 1. \<nexists>n. \<forall>n'\<ge>n. \<not> f n' proof (prove)
goal (1 subgoal):
 1. \<not> (\<nexists>n. \<forall>n'\<ge>n. \<not> f n') \<Longrightarrow> False proof (prove)
using this:
\<exists>n. \<forall>n'\<ge>n. f n'
?m \<le> ?n \<or> ?n \<le> ?m

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

goal (1 subgoal):
 1. f n \<Longrightarrow> set_bits f = (if \<exists>n. \<forall>n'\<ge>n. \<not> f n' then let n = LEAST n. \<forall>n'\<ge>n. \<not> f n' in horner_sum of_bool 2 (map f [0..<n]) else if \<exists>n. \<forall>n'\<ge>n. f n' then let n = LEAST n. \<forall>n'\<ge>n. f n' in signed_take_bit n (horner_sum of_bool 2 (map f [0..<n] @ [True])) else 0) proof (prove)
goal (1 subgoal):
 1. (LEAST n. \<forall>n'\<ge>n. f n') = n proof (prove)
using this:
f n
(LEAST q. \<forall>m\<ge>q. f m = f n) = n

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

goal (1 subgoal):
 1. f n \<Longrightarrow> set_bits f = (if \<exists>n. \<forall>n'\<ge>n. \<not> f n' then let n = LEAST n. \<forall>n'\<ge>n. \<not> f n' in horner_sum of_bool 2 (map f [0..<n]) else if \<exists>n. \<forall>n'\<ge>n. f n' then let n = LEAST n. \<forall>n'\<ge>n. f n' in signed_take_bit n (horner_sum of_bool 2 (map f [0..<n] @ [True])) else 0) proof (chain)
picking this:
\<exists>n. \<forall>n'\<ge>n. f n'
\<nexists>n. \<forall>n'\<ge>n. \<not> f n'
f n proof (prove)
using this:
\<exists>n. \<forall>n'\<ge>n. f n'
\<nexists>n. \<forall>n'\<ge>n. \<not> f n'
f n

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

goal:
No subgoals! proof (state)
this:
set_bits f = (if \<exists>n. \<forall>n'\<ge>n. \<not> f n' then let n = LEAST n. \<forall>n'\<ge>n. \<not> f n' in horner_sum of_bool 2 (map f [0..<n]) else if \<exists>n. \<forall>n'\<ge>n. f n' then let n = LEAST n. \<forall>n'\<ge>n. f n' in signed_take_bit n (horner_sum of_bool 2 (map f [0..<n] @ [True])) else 0)

goal (1 subgoal):
 1. \<nexists>n. \<forall>m\<ge>n. f m = f n \<Longrightarrow> set_bits f = (if \<exists>n. \<forall>n'\<ge>n. \<not> f n' then let n = LEAST n. \<forall>n'\<ge>n. \<not> f n' in horner_sum of_bool 2 (map f [0..<n]) else if \<exists>n. \<forall>n'\<ge>n. f n' then let n = LEAST n. \<forall>n'\<ge>n. f n' in signed_take_bit n (horner_sum of_bool 2 (map f [0..<n] @ [True])) else 0) proof (state)
goal (1 subgoal):
 1. \<nexists>n. \<forall>m\<ge>n. f m = f n \<Longrightarrow> set_bits f = (if \<exists>n. \<forall>n'\<ge>n. \<not> f n' then let n = LEAST n. \<forall>n'\<ge>n. \<not> f n' in horner_sum of_bool 2 (map f [0..<n]) else if \<exists>n. \<forall>n'\<ge>n. f n' then let n = LEAST n. \<forall>n'\<ge>n. f n' in signed_take_bit n (horner_sum of_bool 2 (map f [0..<n] @ [True])) else 0) proof (state)
this:
\<nexists>n. \<forall>m\<ge>n. f m = f n

goal (1 subgoal):
 1. \<nexists>n. \<forall>m\<ge>n. f m = f n \<Longrightarrow> set_bits f = (if \<exists>n. \<forall>n'\<ge>n. \<not> f n' then let n = LEAST n. \<forall>n'\<ge>n. \<not> f n' in horner_sum of_bool 2 (map f [0..<n]) else if \<exists>n. \<forall>n'\<ge>n. f n' then let n = LEAST n. \<forall>n'\<ge>n. f n' in signed_take_bit n (horner_sum of_bool 2 (map f [0..<n] @ [True])) else 0) proof (chain)
picking this:
\<nexists>n. \<forall>m\<ge>n. f m = f n proof (prove)
using this:
\<nexists>n. \<forall>m\<ge>n. f m = f n

goal (1 subgoal):
 1. set_bits f = (if \<exists>n. \<forall>n'\<ge>n. \<not> f n' then let n = LEAST n. \<forall>n'\<ge>n. \<not> f n' in horner_sum of_bool 2 (map f [0..<n]) else if \<exists>n. \<forall>n'\<ge>n. f n' then let n = LEAST n. \<forall>n'\<ge>n. f n' in signed_take_bit n (horner_sum of_bool 2 (map f [0..<n] @ [True])) else 0) proof (state)
this:
set_bits f = (if \<exists>n. \<forall>n'\<ge>n. \<not> f n' then let n = LEAST n. \<forall>n'\<ge>n. \<not> f n' in horner_sum of_bool 2 (map f [0..<n]) else if \<exists>n. \<forall>n'\<ge>n. f n' then let n = LEAST n. \<forall>n'\<ge>n. f n' in signed_take_bit n (horner_sum of_bool 2 (map f [0..<n] @ [True])) else 0)

goal:
No subgoals!