factored out bit comprehension

--- a/src/HOL/Library/Bit_Operations.thy	Thu Oct 08 10:33:38 2020 +0200
+++ b/src/HOL/Library/Bit_Operations.thy	Thu Oct 08 07:30:02 2020 +0000
@@ -486,6 +486,74 @@
 
 subsection \<open>Instance \<^typ>\<open>int\<close>\<close>
 
+lemma int_bit_bound:
+  fixes k :: int
+  obtains n where \<open>\<And>m. n \<le> m \<Longrightarrow> bit k m \<longleftrightarrow> bit k n\<close>
+    and \<open>n > 0 \<Longrightarrow> bit k (n - 1) \<noteq> bit k n\<close>
+proof -
+  obtain q where *: \<open>\<And>m. q \<le> m \<Longrightarrow> bit k m \<longleftrightarrow> bit k q\<close>
+  proof (cases \<open>k \<ge> 0\<close>)
+    case True
+    moreover from power_gt_expt [of 2 \<open>nat k\<close>]
+    have \<open>k < 2 ^ nat k\<close> by simp
+    ultimately have *: \<open>k div 2 ^ nat k = 0\<close>
+      by simp
+    show thesis
+    proof (rule that [of \<open>nat k\<close>])
+      fix m
+      assume \<open>nat k \<le> m\<close>
+      then show \<open>bit k m \<longleftrightarrow> bit k (nat k)\<close>
+        by (auto simp add: * bit_iff_odd power_add zdiv_zmult2_eq dest!: le_Suc_ex)
+    qed
+  next
+    case False
+    moreover from power_gt_expt [of 2 \<open>nat (- k)\<close>]
+    have \<open>- k \<le> 2 ^ nat (- k)\<close>
+      by simp
+    ultimately have \<open>- k div - (2 ^ nat (- k)) = - 1\<close>
+      by (subst div_pos_neg_trivial) simp_all
+    then have *: \<open>k div 2 ^ nat (- k) = - 1\<close>
+      by simp
+    show thesis
+    proof (rule that [of \<open>nat (- k)\<close>])
+      fix m
+      assume \<open>nat (- k) \<le> m\<close>
+      then show \<open>bit k m \<longleftrightarrow> bit k (nat (- k))\<close>
+        by (auto simp add: * bit_iff_odd power_add zdiv_zmult2_eq minus_1_div_exp_eq_int dest!: le_Suc_ex)
+    qed
+  qed
+  show thesis
+  proof (cases \<open>\<forall>m. bit k m \<longleftrightarrow> bit k q\<close>)
+    case True
+    then have \<open>bit k 0 \<longleftrightarrow> bit k q\<close>
+      by blast
+    with True that [of 0] show thesis
+      by simp
+  next
+    case False
+    then obtain r where **: \<open>bit k r \<noteq> bit k q\<close>
+      by blast
+    have \<open>r < q\<close>
+      by (rule ccontr) (use * [of r] ** in simp)
+    define N where \<open>N = {n. n < q \<and> bit k n \<noteq> bit k q}\<close>
+    moreover have \<open>finite N\<close> \<open>r \<in> N\<close>
+      using ** N_def \<open>r < q\<close> by auto
+    moreover define n where \<open>n = Suc (Max N)\<close>
+    ultimately have \<open>\<And>m. n \<le> m \<Longrightarrow> bit k m \<longleftrightarrow> bit k n\<close>
+      apply auto
+         apply (metis (full_types, lifting) "*" Max_ge_iff Suc_n_not_le_n \<open>finite N\<close> all_not_in_conv mem_Collect_eq not_le)
+        apply (metis "*" Max_ge Suc_n_not_le_n \<open>finite N\<close> linorder_not_less mem_Collect_eq)
+        apply (metis "*" Max_ge Suc_n_not_le_n \<open>finite N\<close> linorder_not_less mem_Collect_eq)
+      apply (metis (full_types, lifting) "*" Max_ge_iff Suc_n_not_le_n \<open>finite N\<close> all_not_in_conv mem_Collect_eq not_le)
+      done
+    have \<open>bit k (Max N) \<noteq> bit k n\<close>
+      by (metis (mono_tags, lifting) "*" Max_in N_def \<open>\<And>m. n \<le> m \<Longrightarrow> bit k m = bit k n\<close> \<open>finite N\<close> \<open>r \<in> N\<close> empty_iff le_cases mem_Collect_eq)
+    show thesis apply (rule that [of n])
+      using \<open>\<And>m. n \<le> m \<Longrightarrow> bit k m = bit k n\<close> apply blast
+      using \<open>bit k (Max N) \<noteq> bit k n\<close> n_def by auto
+  qed
+qed
+
 instantiation int :: ring_bit_operations
 begin
 

--- a/src/HOL/Word/Bit_Comprehension.thy	Thu Oct 08 10:33:38 2020 +0200
+++ b/src/HOL/Word/Bit_Comprehension.thy	Thu Oct 08 07:30:02 2020 +0000
@@ -5,26 +5,50 @@
 section \<open>Comprehension syntax for bit expressions\<close>
 
 theory Bit_Comprehension
-  imports "HOL-Library.Bit_Operations"
+  imports Word
 begin
 
-class bit_comprehension = semiring_bits +
-  fixes set_bits :: "(nat \<Rightarrow> bool) \<Rightarrow> 'a"  (binder "BITS " 10)
+class bit_comprehension = ring_bit_operations +
+  fixes set_bits :: \<open>(nat \<Rightarrow> bool) \<Rightarrow> 'a\<close>  (binder \<open>BITS \<close> 10)
+  assumes set_bits_bit_eq: \<open>set_bits (bit a) = a\<close>
+begin
+
+lemma set_bits_False_eq [simp]:
+  \<open>(BITS _. False) = 0\<close>
+  using set_bits_bit_eq [of 0] by (simp add: bot_fun_def)
+
+end
 
 instantiation int :: bit_comprehension
 begin
 
 definition
-  "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)"
+  \<open>set_bits f = (
+      if \<exists>n. \<forall>m\<ge>n. f m = f n then
+      let n = LEAST n. \<forall>m\<ge>n. f m = f n
+      in signed_take_bit n (horner_sum of_bool 2 (map f [0..<Suc n]))
+     else 0 :: int)\<close>
 
-instance ..
+instance proof
+  fix k :: int
+  from int_bit_bound [of k] 
+  obtain n where *: \<open>\<And>m. n \<le> m \<Longrightarrow> bit k m \<longleftrightarrow> bit k n\<close>
+    and **: \<open>n > 0 \<Longrightarrow> bit k (n - 1) \<noteq> bit k n\<close>
+    by blast
+  then have ***: \<open>\<exists>n. \<forall>n'\<ge>n. bit k n' \<longleftrightarrow> bit k n\<close>
+    by meson
+  have l: \<open>(LEAST q. \<forall>m\<ge>q. bit k m \<longleftrightarrow> bit k q) = n\<close>
+    apply (rule Least_equality)
+    using * apply blast
+    apply (metis "**" One_nat_def Suc_pred le_cases le0 neq0_conv not_less_eq_eq)
+    done
+  show \<open>set_bits (bit k) = k\<close>
+    apply (simp only: *** set_bits_int_def horner_sum_bit_eq_take_bit l)
+    apply simp
+    apply (rule bit_eqI)
+    apply (simp add: bit_signed_take_bit_iff min_def)
+    using "*" by blast
+qed
 
 end
 
@@ -32,6 +56,192 @@
   by (simp add: set_bits_int_def)
 
 lemma int_set_bits_K_True [simp]: "(BITS _. True) = (-1 :: int)"
-  by (auto simp add: set_bits_int_def)
+  by (simp add: set_bits_int_def)
+
+instantiation word :: (len) bit_comprehension
+begin
+
+definition word_set_bits_def:
+  \<open>(BITS n. P n) = (horner_sum of_bool 2 (map P [0..<LENGTH('a)]) :: 'a word)\<close>
+
+instance by standard
+  (simp add: word_set_bits_def horner_sum_bit_eq_take_bit)
 
 end
+
+lemma bit_set_bits_word_iff:
+  \<open>bit (set_bits P :: 'a::len word) n \<longleftrightarrow> n < LENGTH('a) \<and> P n\<close>
+  by (auto simp add: word_set_bits_def bit_horner_sum_bit_word_iff)
+
+lemma set_bits_K_False [simp]:
+  \<open>set_bits (\<lambda>_. False) = (0 :: 'a :: len word)\<close>
+  by (rule bit_word_eqI) (simp add: bit_set_bits_word_iff)
+
+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 Least_equality Least_le \<open>\<forall>m\<ge>n. f m = f n\<close> dual_order.refl le_refl n order_refl)
+  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
+
+inductive wf_set_bits_int :: "(nat \<Rightarrow> bool) \<Rightarrow> bool" 
+  for f :: "nat \<Rightarrow> bool"
+where
+  zeros: "\<forall>n' \<ge> n. \<not> f n' \<Longrightarrow> wf_set_bits_int f"
+| ones: "\<forall>n' \<ge> n. f n' \<Longrightarrow> wf_set_bits_int f"
+
+lemma wf_set_bits_int_simps: "wf_set_bits_int f \<longleftrightarrow> (\<exists>n. (\<forall>n'\<ge>n. \<not> f n') \<or> (\<forall>n'\<ge>n. f n'))"
+by(auto simp add: wf_set_bits_int.simps)
+
+lemma wf_set_bits_int_const [simp]: "wf_set_bits_int (\<lambda>_. b)"
+by(cases b)(auto intro: wf_set_bits_int.intros)
+
+lemma wf_set_bits_int_fun_upd [simp]: 
+  "wf_set_bits_int (f(n := b)) \<longleftrightarrow> wf_set_bits_int f" (is "?lhs \<longleftrightarrow> ?rhs")
+proof
+  assume ?lhs
+  then obtain n'
+    where "(\<forall>n''\<ge>n'. \<not> (f(n := b)) n'') \<or> (\<forall>n''\<ge>n'. (f(n := b)) n'')"
+    by(auto simp add: wf_set_bits_int_simps)
+  hence "(\<forall>n''\<ge>max (Suc n) n'. \<not> f n'') \<or> (\<forall>n''\<ge>max (Suc n) n'. f n'')" by auto
+  thus ?rhs by(auto simp only: wf_set_bits_int_simps)
+next
+  assume ?rhs
+  then obtain n' where "(\<forall>n''\<ge>n'. \<not> f n'') \<or> (\<forall>n''\<ge>n'. f n'')" (is "?wf f n'")
+    by(auto simp add: wf_set_bits_int_simps)
+  hence "?wf (f(n := b)) (max (Suc n) n')" by auto
+  thus ?lhs by(auto simp only: wf_set_bits_int_simps)
+qed
+
+lemma wf_set_bits_int_Suc [simp]:
+  "wf_set_bits_int (\<lambda>n. f (Suc n)) \<longleftrightarrow> wf_set_bits_int f" (is "?lhs \<longleftrightarrow> ?rhs")
+by(auto simp add: wf_set_bits_int_simps intro: le_SucI dest: Suc_le_D)
+
+context
+  fixes f
+  assumes wff: "wf_set_bits_int f"
+begin
+
+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
+
+lemma bin_last_set_bits [simp]:
+  "bin_last (set_bits f) = f 0"
+  by (subst int_set_bits_unfold_BIT) simp_all
+
+lemma bin_rest_set_bits [simp]:
+  "bin_rest (set_bits f) = set_bits (f \<circ> Suc)"
+  by (subst int_set_bits_unfold_BIT) simp_all
+
+lemma bin_nth_set_bits [simp]:
+  "bin_nth (set_bits f) m = f m"
+using wff proof (induction m arbitrary: f)
+  case 0 
+  then show ?case
+    by (simp add: Bit_Comprehension.bin_last_set_bits)
+next
+  case Suc
+  from Suc.IH [of "f \<circ> Suc"] Suc.prems show ?case
+    by (simp add: Bit_Comprehension.bin_rest_set_bits comp_def bit_Suc)
+qed
+
+end
+
+end

--- a/src/HOL/Word/Misc_Typedef.thy	Thu Oct 08 10:33:38 2020 +0200
+++ b/src/HOL/Word/Misc_Typedef.thy	Thu Oct 08 07:30:02 2020 +0000
@@ -7,7 +7,7 @@
 section \<open>Type Definition Theorems\<close>
 
 theory Misc_Typedef
-  imports Main Word
+  imports Main Word Bit_Comprehension
 begin
 
 subsection "More lemmas about normal type definitions"
@@ -349,8 +349,7 @@
     set_bits
     "{f. \<forall>i. f i \<longrightarrow> i < LENGTH('a::len)}"
     "(\<lambda>h i. h i \<and> i < LENGTH('a::len))"
-  by standard
-    (auto simp add: test_bit_word_eq bit_imp_le_length bit_set_bits_word_iff set_bits_bit_eq)
+  by standard (auto simp add: test_bit_word_eq bit_imp_le_length bit_set_bits_word_iff set_bits_bit_eq)
 
 lemmas td_nth = test_bit.td_thm
 

--- a/src/HOL/Word/More_Word.thy	Thu Oct 08 10:33:38 2020 +0200
+++ b/src/HOL/Word/More_Word.thy	Thu Oct 08 07:30:02 2020 +0000
@@ -9,6 +9,7 @@
   Ancient_Numeral
   Reversed_Bit_Lists
   Bits_Int
+  Bit_Comprehension
   Misc_Auxiliary
   Misc_Arithmetic
   Misc_set_bit

--- a/src/HOL/Word/Word.thy	Thu Oct 08 10:33:38 2020 +0200
+++ b/src/HOL/Word/Word.thy	Thu Oct 08 07:30:02 2020 +0000
@@ -11,7 +11,6 @@
   "HOL-Library.Bit_Operations"
   Bits_Int
   Traditional_Syntax
-  Bit_Comprehension
 begin
 
 subsection \<open>Preliminaries\<close>
@@ -3915,31 +3914,6 @@
   done
 
 
-subsection \<open>Bit comprehension\<close>
-
-instantiation word :: (len) bit_comprehension
-begin
-
-definition word_set_bits_def:
-  \<open>(BITS n. P n) = (horner_sum of_bool 2 (map P [0..<LENGTH('a)]) :: 'a word)\<close>
-
-instance ..
-
-end
-
-lemma bit_set_bits_word_iff:
-  \<open>bit (set_bits P :: 'a::len word) n \<longleftrightarrow> n < LENGTH('a) \<and> P n\<close>
-  by (auto simp add: word_set_bits_def bit_horner_sum_bit_word_iff)
-
-lemma set_bits_bit_eq:
-  \<open>set_bits (bit w) = w\<close> for w :: \<open>'a::len word\<close>
-  by (rule bit_word_eqI) (auto simp add: bit_set_bits_word_iff bit_imp_le_length)
-
-lemma set_bits_K_False [simp]:
-  \<open>set_bits (\<lambda>_. False) = (0 :: 'a :: len word)\<close>
-  by (rule bit_word_eqI) (simp add: bit_set_bits_word_iff)
-
-
 subsection \<open>Shifting, Rotating, and Splitting Words\<close>
 
 lemma shiftl1_wi [simp]: "shiftl1 (word_of_int w) = word_of_int (2 * w)"
@@ -5311,9 +5285,6 @@
 lemma mask_Suc_0: "mask (Suc 0) = 1"
   using mask_1 by simp
 
-lemma mask_numeral: "mask (numeral n) = 2 * mask (pred_numeral n) + (1 :: 'a::len word)"
-  by (simp add: mask_Suc_rec numeral_eq_Suc)
-
 lemma bin_last_bintrunc: "bin_last (take_bit l n) = (l > 0 \<and> bin_last n)"
   by simp