# HG changeset patch
# User huffman
# Date 1187626269 -7200
# Node ID 4d74f37c6367813f328f31f107b18a84eddbd5fb
# Parent  0dd8782fb02dc5b9fe9966e12fd6c6036c5126e0
headers for document generation

diff -r 0dd8782fb02d -r 4d74f37c6367 src/HOL/Word/BinBoolList.thy
--- a/src/HOL/Word/BinBoolList.thy	Mon Aug 20 18:10:13 2007 +0200
+++ b/src/HOL/Word/BinBoolList.thy	Mon Aug 20 18:11:09 2007 +0200
@@ -11,7 +11,7 @@
 
 theory BinBoolList imports BinOperations begin
 
-section "Arithmetic in terms of bool lists"
+subsection "Arithmetic in terms of bool lists"
 
 consts (* arithmetic operations in terms of the reversed bool list,
   assuming input list(s) the same length, and don't extend them *)
@@ -930,7 +930,7 @@
 lemmas tl_Cons = tl.simps (2)
 
 
-section "Repeated splitting or concatenation"
+subsection "Repeated splitting or concatenation"
 
 lemma sclem:
   "size (concat (map (bin_to_bl n) xs)) = length xs * n"
diff -r 0dd8782fb02d -r 4d74f37c6367 src/HOL/Word/BinGeneral.thy
--- a/src/HOL/Word/BinGeneral.thy	Mon Aug 20 18:10:13 2007 +0200
+++ b/src/HOL/Word/BinGeneral.thy	Mon Aug 20 18:11:09 2007 +0200
@@ -7,10 +7,14 @@
   in particular, bin_rec and related work
 *) 
 
+header {* Basic Definitions for Binary Integers *}
+
 theory BinGeneral imports TdThs Num_Lemmas
 
 begin
 
+subsection {* Recursion combinator for binary integers *}
+
 lemma brlem: "(bin = Numeral.Min) = (- bin + Numeral.pred 0 = 0)"
   unfolding Min_def pred_def by arith
 
@@ -299,7 +303,7 @@
   by (auto simp: pred_def succ_def split add : split_if_asm)
 
 
-section "Simplifications for (s)bintrunc"
+subsection "Simplifications for (s)bintrunc"
 
 lemma bit_bool:
   "(b = (b' = bit.B1)) = (b' = (if b then bit.B1 else bit.B0))"
diff -r 0dd8782fb02d -r 4d74f37c6367 src/HOL/Word/BinOperations.thy
--- a/src/HOL/Word/BinOperations.thy	Mon Aug 20 18:10:13 2007 +0200
+++ b/src/HOL/Word/BinOperations.thy	Mon Aug 20 18:11:09 2007 +0200
@@ -7,6 +7,8 @@
   and converting them to and from lists of bools
 *) 
 
+header {* Bitwise Operations on Binary Integers *}
+
 theory BinOperations imports BinGeneral
 
 begin
diff -r 0dd8782fb02d -r 4d74f37c6367 src/HOL/Word/Num_Lemmas.thy
--- a/src/HOL/Word/Num_Lemmas.thy	Mon Aug 20 18:10:13 2007 +0200
+++ b/src/HOL/Word/Num_Lemmas.thy	Mon Aug 20 18:11:09 2007 +0200
@@ -1,9 +1,9 @@
 (* 
   ID:      $Id$
   Author:  Jeremy Dawson, NICTA
+*) 
 
-  useful numerical lemmas 
-*) 
+header {* Useful Numerical Lemmas *}
 
 theory Num_Lemmas imports Parity begin
 
diff -r 0dd8782fb02d -r 4d74f37c6367 src/HOL/Word/TdThs.thy
--- a/src/HOL/Word/TdThs.thy	Mon Aug 20 18:10:13 2007 +0200
+++ b/src/HOL/Word/TdThs.thy	Mon Aug 20 18:11:09 2007 +0200
@@ -5,6 +5,9 @@
   consequences of type definition theorems, 
   and of extended type definition theorems
 *)
+
+header {* Type Definition Theorems *}
+
 theory TdThs imports Main begin
 
 lemma
@@ -91,7 +94,7 @@
 declare Nat.exhaust [case_names 0 Suc, cases type]
 
 
-section "Extended of type definition predicate"
+subsection "Extended form of type definition predicate"
 
 lemma td_conds:
   "norm o norm = norm ==> (fr o norm = norm o fr) = 
diff -r 0dd8782fb02d -r 4d74f37c6367 src/HOL/Word/WordArith.thy
--- a/src/HOL/Word/WordArith.thy	Mon Aug 20 18:10:13 2007 +0200
+++ b/src/HOL/Word/WordArith.thy	Mon Aug 20 18:11:09 2007 +0200
@@ -7,6 +7,8 @@
   to linear arithmetic on int or nat
 *) 
 
+header {* Word Arithmetic *}
+
 theory WordArith imports WordDefinition begin
 
 
@@ -217,7 +219,7 @@
 lemmas word_0_alt = word_arith_alts (7)
 lemmas word_1_alt = word_arith_alts (8)
 
-section  "Transferring goals from words to ints"
+subsection  "Transferring goals from words to ints"
 
 lemma word_ths:  
   shows
@@ -307,7 +309,7 @@
 lemmas word_times_ac1 = word_mult_1 word_mult_1_right word_mult_ac
 
 
-section "Order on fixed-length words"
+subsection "Order on fixed-length words"
 
 lemma word_order_trans: "x <= y ==> y <= z ==> x <= (z :: 'a :: len0 word)"
   unfolding word_le_def by auto
@@ -436,7 +438,7 @@
   using uint_ge_0 [of y] uint_lt2p [of x] by arith
 
 
-section "Conditions for the addition (etc) of two words to overflow"
+subsection "Conditions for the addition (etc) of two words to overflow"
 
 lemma uint_add_lem: 
   "(uint x + uint y < 2 ^ len_of TYPE('a)) = 
@@ -464,7 +466,7 @@
   trans [OF uint_word_ariths(2) mod_add_if_z, simplified, standard]
 
 
-section {* Definition of uint\_arith *}
+subsection {* Definition of uint\_arith *}
 
 lemma word_of_int_inverse:
   "word_of_int r = a ==> 0 <= r ==> r < 2 ^ len_of TYPE('a) ==> 
@@ -533,7 +535,7 @@
   "solving word arithmetic via integers and arith"
 
 
-section "More on overflows and monotonicity"
+subsection "More on overflows and monotonicity"
 
 lemma no_plus_overflow_uint_size: 
   "((x :: 'a :: len0 word) <= x + y) = (uint x + uint y < 2 ^ size x)"
@@ -762,7 +764,7 @@
                  word_pred_rbl word_mult_rbl word_add_rbl)
 
 
-section "Arithmetic type class instantiations"
+subsection "Arithmetic type class instantiations"
 
 instance word :: (len0) comm_monoid_add ..
 
@@ -841,7 +843,7 @@
   done
     
 
-section "Word and nat"
+subsection "Word and nat"
 
 lemma td_ext_unat':
   "n = len_of TYPE ('a :: len) ==> 
@@ -1034,7 +1036,7 @@
   unfolding uint_nat by (simp add : unat_mod zmod_int)
 
 
-section {* Definition of unat\_arith tactic *}
+subsection {* Definition of unat\_arith tactic *}
 
 lemma unat_split:
   fixes x::"'a::len word"
@@ -1230,7 +1232,7 @@
   done
 
 
-section "Cardinality, finiteness of set of words"
+subsection "Cardinality, finiteness of set of words"
 
 lemmas card_lessThan' = card_lessThan [unfolded lessThan_def]
 
diff -r 0dd8782fb02d -r 4d74f37c6367 src/HOL/Word/WordBitwise.thy
--- a/src/HOL/Word/WordBitwise.thy	Mon Aug 20 18:10:13 2007 +0200
+++ b/src/HOL/Word/WordBitwise.thy	Mon Aug 20 18:11:09 2007 +0200
@@ -4,6 +4,9 @@
 
   contains theorems to do with bit-wise (logical) operations on words
 *)
+
+header {* Bitwise Operations on Words *}
+
 theory WordBitwise imports WordArith begin
 
 lemmas bin_log_bintrs = bin_trunc_not bin_trunc_xor bin_trunc_and bin_trunc_or
diff -r 0dd8782fb02d -r 4d74f37c6367 src/HOL/Word/WordDefinition.thy
--- a/src/HOL/Word/WordDefinition.thy	Mon Aug 20 18:10:13 2007 +0200
+++ b/src/HOL/Word/WordDefinition.thy	Mon Aug 20 18:11:09 2007 +0200
@@ -6,6 +6,7 @@
   the definition of the word type 
 *) 
 
+header {* Definition of Word Type *}
 
 theory WordDefinition imports Size BitSyntax BinBoolList begin 
 
@@ -26,7 +27,7 @@
 instance word :: (type) bit ..
 
 
-section "Type conversions and casting"
+subsection "Type conversions and casting"
 
 constdefs
   -- {* representation of words using unsigned or signed bins, 
@@ -94,7 +95,7 @@
   "case x of of_int y => b" == "word_int_case (%y. b) x"
 
 
-section  "Arithmetic operations"
+subsection  "Arithmetic operations"
 
 defs (overloaded)
   word_1_wi: "(1 :: ('a :: len0) word) == word_of_int 1"
@@ -135,7 +136,7 @@
   word_mod_def: "a mod b == word_of_int (uint a mod uint b)"
 
 
-section "Bit-wise operations"
+subsection "Bit-wise operations"
 
 defs (overloaded)
   word_and_def: 
@@ -175,7 +176,7 @@
   "clearBit w n == set_bit w n False"
 
 
-section "Shift operations"
+subsection "Shift operations"
 
 constdefs
   shiftl1 :: "'a :: len0 word => 'a word"
@@ -212,7 +213,7 @@
   shiftr_def: "(w::'a::len0 word) >> n == (shiftr1 ^ n) w"
 
 
-section "Rotation"
+subsection "Rotation"
 
 constdefs
   rotater1 :: "'a list => 'a list"
@@ -233,7 +234,7 @@
                     else word_rotl (nat (- i)) w"
 
 
-section "Split and cat operations"
+subsection "Split and cat operations"
 
 constdefs
   word_cat :: "'a :: len0 word => 'b :: len0 word => 'c :: len0 word"
diff -r 0dd8782fb02d -r 4d74f37c6367 src/HOL/Word/WordGenLib.thy
--- a/src/HOL/Word/WordGenLib.thy	Mon Aug 20 18:10:13 2007 +0200
+++ b/src/HOL/Word/WordGenLib.thy	Mon Aug 20 18:11:09 2007 +0200
@@ -6,6 +6,8 @@
    of recursion and induction patterns for words.
 *)
 
+header {* Miscellaneous Library for Words *}
+
 theory WordGenLib imports WordShift Boolean_Algebra
 begin
 
diff -r 0dd8782fb02d -r 4d74f37c6367 src/HOL/Word/WordMain.thy
--- a/src/HOL/Word/WordMain.thy	Mon Aug 20 18:10:13 2007 +0200
+++ b/src/HOL/Word/WordMain.thy	Mon Aug 20 18:11:09 2007 +0200
@@ -5,6 +5,8 @@
   The main interface of the word library to other theories.
 *)
 
+header {* Main Word Library *}
+
 theory WordMain imports WordGenLib
 begin
 
diff -r 0dd8782fb02d -r 4d74f37c6367 src/HOL/Word/WordShift.thy
--- a/src/HOL/Word/WordShift.thy	Mon Aug 20 18:10:13 2007 +0200
+++ b/src/HOL/Word/WordShift.thy	Mon Aug 20 18:11:09 2007 +0200
@@ -5,9 +5,11 @@
   contains theorems to do with shifting, rotating, splitting words
 *)
 
+header {* Shifting, Rotating, and Splitting Words *}
+
 theory WordShift imports WordBitwise begin
 
-section "Bit shifting"
+subsection "Bit shifting"
 
 lemma shiftl1_number [simp] :
   "shiftl1 (number_of w) = number_of (w BIT bit.B0)"
@@ -166,7 +168,7 @@
                    zdiv_zmult2_eq [symmetric])
   done
 
-subsection "shift functions in terms of lists of bools"
+subsubsection "shift functions in terms of lists of bools"
 
 lemmas bshiftr1_no_bin [simp] = 
   bshiftr1_def [where w="number_of ?w", unfolded to_bl_no_bin]
@@ -454,7 +456,7 @@
 
 lemmas aligned_bl_add_size = refl [THEN aligned_bl_add_size']
 
-subsection "Mask"
+subsubsection "Mask"
 
 lemma nth_mask': "m = mask n ==> test_bit m i = (i < n & i < size m)"
   apply (unfold mask_def test_bit_bl)
@@ -590,7 +592,7 @@
   by (clarsimp simp: and_mask_wi word_of_int_power_hom bintr_ariths)
 
 
-subsection "Revcast"
+subsubsection "Revcast"
 
 lemmas revcast_def' = revcast_def [simplified]
 lemmas revcast_def'' = revcast_def' [simplified word_size]
@@ -713,7 +715,7 @@
   rc2 [simplified rev_shiftr revcast_ucast [symmetric]]
 
 
-subsection "Slices"
+subsubsection "Slices"
 
 lemmas slice1_no_bin [simp] =
   slice1_def [where w="number_of ?w", unfolded to_bl_no_bin]
@@ -858,7 +860,7 @@
   done
 
 
-section "Split and cat"
+subsection "Split and cat"
 
 lemmas word_split_bin' = word_split_def [THEN meta_eq_to_obj_eq, standard]
 lemmas word_cat_bin' = word_cat_def [THEN meta_eq_to_obj_eq, standard]
@@ -1025,7 +1027,7 @@
   sym [THEN [2] word_cat_split_alt [symmetric], standard]
 
 
-subsection "Split and slice"
+subsubsection "Split and slice"
 
 lemma split_slices: 
   "word_split w = (u, v) ==> u = slice (size v) w & v = slice 0 w"
@@ -1240,7 +1242,7 @@
 lemmas word_rsplit_rcat_size = refl [THEN word_rsplit_rcat_size']
 
 
-section "Rotation"
+subsection "Rotation"
 
 lemmas rotater_0' [simp] = rotater_def [where n = "0", simplified]
 
@@ -1262,7 +1264,7 @@
   rotate_eq_mod
 
 
-subsection "Rotation of list to right"
+subsubsection "Rotation of list to right"
 
 lemma rotate1_rl': "rotater1 (l @ [a]) = a # l"
   unfolding rotater1_def by (cases l) auto
@@ -1332,7 +1334,7 @@
 lemmas rotater_add = rotater_eqs (2)
 
 
-subsection "map, app2, commuting with rotate(r)"
+subsubsection "map, app2, commuting with rotate(r)"
 
 lemma last_map: "xs ~= [] ==> last (map f xs) = f (last xs)"
   by (induct xs) auto
@@ -1511,7 +1513,7 @@
 lemmas word_roti_conv_mod = word_roti_conv_mod' [unfolded word_size]
 
 
-subsection "Word rotation commutes with bit-wise operations"
+subsubsection "Word rotation commutes with bit-wise operations"
 
 (* using locale to not pollute lemma namespace *)
 locale word_rotate