--- a/src/HOL/Word/Word.thy Tue Dec 27 18:26:15 2011 +0100
+++ b/src/HOL/Word/Word.thy Wed Dec 28 07:58:17 2011 +0100
@@ -456,6 +456,8 @@
(* 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)"
@@ -664,6 +666,8 @@
"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)
@@ -4135,7 +4139,7 @@
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>
@@ -4454,6 +4458,8 @@
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)"