src/HOL/Word/Word.thy

   "of_bool False = 0"
 | "of_bool True = 1"
 
 (* FIXME: only provide one theorem name *)
 lemmas of_nth_def = word_set_bits_def
+
+subsection {* Theorems about typedefs *}
 
 lemma sint_sbintrunc': 
   "sint (word_of_int bin :: 'a word) = 
     (sbintrunc (len_of TYPE ('a :: len) - 1) bin)"
   unfolding sint_uint 

   unfolding word_size by (rule less_le_trans [OF sint_lt])
 
 lemma sint_below_size:
   "x \<le> - (2 ^ (size (w::'a::len word) - 1)) \<Longrightarrow> x \<le> sint w"
   unfolding word_size by (rule order_trans [OF _ sint_ge])
+
+subsection {* Testing bits *}
 
 lemma test_bit_eq_iff: "(test_bit (u::'a::len0 word) = test_bit v) = (u = v)"
   unfolding word_test_bit_def by (simp add: bin_nth_eq_iff)
 
 lemma test_bit_size [rule_format] : "(w::'a::len0 word) !! n --> n < size w"

   word_rotl_dt [where w="number_of w", unfolded to_bl_no_bin] for w
 
 declare word_roti_def [simp]
 
 
-subsection {* Miscellaneous  *}
+subsection {* Maximum machine word *}
 
 lemma word_int_cases:
   "\<lbrakk>\<And>n. \<lbrakk>(x ::'a::len0 word) = word_of_int n; 0 \<le> n; n < 2^len_of TYPE('a)\<rbrakk> \<Longrightarrow> P\<rbrakk>
    \<Longrightarrow> P"
   by (cases x rule: word_uint.Abs_cases) (simp add: uints_num)

 lemma word_induct2 [induct type]: 
   "\<lbrakk>P 0; \<And>n. \<lbrakk>1 + n \<noteq> 0; P n\<rbrakk> \<Longrightarrow> P (1 + n)\<rbrakk> \<Longrightarrow> P (n::'b::len word)"
   apply (rule word_induct, simp)
   apply (case_tac "1+n = 0", auto)
   done
+
+subsection {* Recursion combinator for words *}
 
 definition word_rec :: "'a \<Rightarrow> ('b::len word \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b word \<Rightarrow> 'a" where
   "word_rec forZero forSuc n = nat_rec forZero (forSuc \<circ> of_nat) (unat n)"
 
 lemma word_rec_0: "word_rec z s 0 = z"