--- 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"
--- 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))"
--- 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
--- 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
--- 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) =
--- 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]
--- 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
--- 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"
--- 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
--- 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
--- 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