syntactically tuned
authorhaftmann
Mon Dec 23 14:24:21 2013 +0100 (2013-12-23)
changeset 54848a303daddebbf
parent 54847 d6cf9a5b9be9
child 54849 d325c7c4a4f7
syntactically tuned
src/HOL/Word/Bit_Int.thy
src/HOL/Word/Bit_Representation.thy
src/HOL/Word/Bool_List_Representation.thy
src/HOL/Word/Word.thy
     1.1 --- a/src/HOL/Word/Bit_Int.thy	Mon Dec 23 14:24:20 2013 +0100
     1.2 +++ b/src/HOL/Word/Bit_Int.thy	Mon Dec 23 14:24:21 2013 +0100
     1.3 @@ -482,25 +482,30 @@
     1.4  
     1.5  subsection {* Splitting and concatenation *}
     1.6  
     1.7 -definition bin_rcat :: "nat \<Rightarrow> int list \<Rightarrow> int" where
     1.8 +definition bin_rcat :: "nat \<Rightarrow> int list \<Rightarrow> int"
     1.9 +where
    1.10    "bin_rcat n = foldl (\<lambda>u v. bin_cat u n v) 0"
    1.11  
    1.12 -fun bin_rsplit_aux :: "nat \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list" where
    1.13 +fun bin_rsplit_aux :: "nat \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list"
    1.14 +where
    1.15    "bin_rsplit_aux n m c bs =
    1.16      (if m = 0 | n = 0 then bs else
    1.17        let (a, b) = bin_split n c 
    1.18        in bin_rsplit_aux n (m - n) a (b # bs))"
    1.19  
    1.20 -definition bin_rsplit :: "nat \<Rightarrow> nat \<times> int \<Rightarrow> int list" where
    1.21 +definition bin_rsplit :: "nat \<Rightarrow> nat \<times> int \<Rightarrow> int list"
    1.22 +where
    1.23    "bin_rsplit n w = bin_rsplit_aux n (fst w) (snd w) []"
    1.24  
    1.25 -fun bin_rsplitl_aux :: "nat \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list" where
    1.26 +fun bin_rsplitl_aux :: "nat \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list"
    1.27 +where
    1.28    "bin_rsplitl_aux n m c bs =
    1.29      (if m = 0 | n = 0 then bs else
    1.30        let (a, b) = bin_split (min m n) c 
    1.31        in bin_rsplitl_aux n (m - n) a (b # bs))"
    1.32  
    1.33 -definition bin_rsplitl :: "nat \<Rightarrow> nat \<times> int \<Rightarrow> int list" where
    1.34 +definition bin_rsplitl :: "nat \<Rightarrow> nat \<times> int \<Rightarrow> int list"
    1.35 +where
    1.36    "bin_rsplitl n w = bin_rsplitl_aux n (fst w) (snd w) []"
    1.37  
    1.38  declare bin_rsplit_aux.simps [simp del]
     2.1 --- a/src/HOL/Word/Bit_Representation.thy	Mon Dec 23 14:24:20 2013 +0100
     2.2 +++ b/src/HOL/Word/Bit_Representation.thy	Mon Dec 23 14:24:21 2013 +0100
     2.3 @@ -10,7 +10,8 @@
     2.4  
     2.5  subsection {* Constructors and destructors for binary integers *}
     2.6  
     2.7 -definition Bit :: "int \<Rightarrow> bool \<Rightarrow> int" (infixl "BIT" 90) where
     2.8 +definition Bit :: "int \<Rightarrow> bool \<Rightarrow> int" (infixl "BIT" 90)
     2.9 +where
    2.10    "k BIT b = (if b then 1 else 0) + k + k"
    2.11  
    2.12  lemma Bit_B0:
    2.13 @@ -27,14 +28,16 @@
    2.14  lemma Bit_B1_2t: "k BIT True = 2 * k + 1"
    2.15    by (rule trans, rule Bit_B1) simp
    2.16  
    2.17 -definition bin_last :: "int \<Rightarrow> bool" where
    2.18 +definition bin_last :: "int \<Rightarrow> bool"
    2.19 +where
    2.20    "bin_last w \<longleftrightarrow> w mod 2 = 1"
    2.21  
    2.22  lemma bin_last_odd:
    2.23    "bin_last = odd"
    2.24    by (rule ext) (simp add: bin_last_def even_def)
    2.25  
    2.26 -definition bin_rest :: "int \<Rightarrow> int" where
    2.27 +definition bin_rest :: "int \<Rightarrow> int"
    2.28 +where
    2.29    "bin_rest w = w div 2"
    2.30  
    2.31  lemma bin_rl_simp [simp]:
    2.32 @@ -271,7 +274,8 @@
    2.33  
    2.34  subsection {* Truncating binary integers *}
    2.35  
    2.36 -definition bin_sign :: "int \<Rightarrow> int" where
    2.37 +definition bin_sign :: "int \<Rightarrow> int"
    2.38 +where
    2.39    bin_sign_def: "bin_sign k = (if k \<ge> 0 then 0 else - 1)"
    2.40  
    2.41  lemma bin_sign_simps [simp]:
     3.1 --- a/src/HOL/Word/Bool_List_Representation.thy	Mon Dec 23 14:24:20 2013 +0100
     3.2 +++ b/src/HOL/Word/Bool_List_Representation.thy	Mon Dec 23 14:24:21 2013 +0100
     3.3 @@ -31,27 +31,33 @@
     3.4  
     3.5  subsection {* Operations on lists of booleans *}
     3.6  
     3.7 -primrec bl_to_bin_aux :: "bool list \<Rightarrow> int \<Rightarrow> int" where
     3.8 +primrec bl_to_bin_aux :: "bool list \<Rightarrow> int \<Rightarrow> int"
     3.9 +where
    3.10    Nil: "bl_to_bin_aux [] w = w"
    3.11    | Cons: "bl_to_bin_aux (b # bs) w = 
    3.12        bl_to_bin_aux bs (w BIT b)"
    3.13  
    3.14 -definition bl_to_bin :: "bool list \<Rightarrow> int" where
    3.15 +definition bl_to_bin :: "bool list \<Rightarrow> int"
    3.16 +where
    3.17    bl_to_bin_def: "bl_to_bin bs = bl_to_bin_aux bs 0"
    3.18  
    3.19 -primrec bin_to_bl_aux :: "nat \<Rightarrow> int \<Rightarrow> bool list \<Rightarrow> bool list" where
    3.20 +primrec bin_to_bl_aux :: "nat \<Rightarrow> int \<Rightarrow> bool list \<Rightarrow> bool list"
    3.21 +where
    3.22    Z: "bin_to_bl_aux 0 w bl = bl"
    3.23    | Suc: "bin_to_bl_aux (Suc n) w bl =
    3.24        bin_to_bl_aux n (bin_rest w) ((bin_last w) # bl)"
    3.25  
    3.26 -definition bin_to_bl :: "nat \<Rightarrow> int \<Rightarrow> bool list" where
    3.27 +definition bin_to_bl :: "nat \<Rightarrow> int \<Rightarrow> bool list"
    3.28 +where
    3.29    bin_to_bl_def : "bin_to_bl n w = bin_to_bl_aux n w []"
    3.30  
    3.31 -primrec bl_of_nth :: "nat \<Rightarrow> (nat \<Rightarrow> bool) \<Rightarrow> bool list" where
    3.32 +primrec bl_of_nth :: "nat \<Rightarrow> (nat \<Rightarrow> bool) \<Rightarrow> bool list"
    3.33 +where
    3.34    Suc: "bl_of_nth (Suc n) f = f n # bl_of_nth n f"
    3.35    | Z: "bl_of_nth 0 f = []"
    3.36  
    3.37 -primrec takefill :: "'a \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where
    3.38 +primrec takefill :: "'a \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> 'a list"
    3.39 +where
    3.40    Z: "takefill fill 0 xs = []"
    3.41    | Suc: "takefill fill (Suc n) xs = (
    3.42        case xs of [] => fill # takefill fill n xs
    3.43 @@ -65,21 +71,25 @@
    3.44    assuming input list(s) the same length, and don't extend them. 
    3.45  *}
    3.46  
    3.47 -primrec rbl_succ :: "bool list => bool list" where
    3.48 +primrec rbl_succ :: "bool list => bool list"
    3.49 +where
    3.50    Nil: "rbl_succ Nil = Nil"
    3.51    | Cons: "rbl_succ (x # xs) = (if x then False # rbl_succ xs else True # xs)"
    3.52  
    3.53 -primrec rbl_pred :: "bool list => bool list" where
    3.54 +primrec rbl_pred :: "bool list => bool list"
    3.55 +where
    3.56    Nil: "rbl_pred Nil = Nil"
    3.57    | Cons: "rbl_pred (x # xs) = (if x then False # xs else True # rbl_pred xs)"
    3.58  
    3.59 -primrec rbl_add :: "bool list => bool list => bool list" where
    3.60 +primrec rbl_add :: "bool list => bool list => bool list"
    3.61 +where
    3.62    -- "result is length of first arg, second arg may be longer"
    3.63    Nil: "rbl_add Nil x = Nil"
    3.64    | Cons: "rbl_add (y # ys) x = (let ws = rbl_add ys (tl x) in 
    3.65      (y ~= hd x) # (if hd x & y then rbl_succ ws else ws))"
    3.66  
    3.67 -primrec rbl_mult :: "bool list => bool list => bool list" where
    3.68 +primrec rbl_mult :: "bool list => bool list => bool list"
    3.69 +where
    3.70    -- "result is length of first arg, second arg may be longer"
    3.71    Nil: "rbl_mult Nil x = Nil"
    3.72    | Cons: "rbl_mult (y # ys) x = (let ws = False # rbl_mult ys x in 
     4.1 --- a/src/HOL/Word/Word.thy	Mon Dec 23 14:24:20 2013 +0100
     4.2 +++ b/src/HOL/Word/Word.thy	Mon Dec 23 14:24:21 2013 +0100
     4.3 @@ -35,7 +35,8 @@
     4.4    shows "uint w mod 2 ^ len_of TYPE('a) = uint w"
     4.5    using uint_nonnegative uint_bounded by (rule mod_pos_pos_trivial)
     4.6  
     4.7 -definition word_of_int :: "int \<Rightarrow> 'a\<Colon>len0 word" where
     4.8 +definition word_of_int :: "int \<Rightarrow> 'a\<Colon>len0 word"
     4.9 +where
    4.10    -- {* representation of words using unsigned or signed bins, 
    4.11          only difference in these is the type class *}
    4.12    "word_of_int k = Abs_word (k mod 2 ^ len_of TYPE('a))" 
    4.13 @@ -72,7 +73,8 @@
    4.14  instantiation word :: (len0) equal
    4.15  begin
    4.16  
    4.17 -definition equal_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> bool" where
    4.18 +definition equal_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> bool"
    4.19 +where
    4.20    "equal_word k l \<longleftrightarrow> HOL.equal (uint k) (uint l)"
    4.21  
    4.22  instance proof
    4.23 @@ -101,31 +103,39 @@
    4.24  
    4.25  subsection {* Type conversions and casting *}
    4.26  
    4.27 -definition sint :: "'a :: len word => int" where
    4.28 +definition sint :: "'a :: len word => int"
    4.29 +where
    4.30    -- {* treats the most-significant-bit as a sign bit *}
    4.31    sint_uint: "sint w = sbintrunc (len_of TYPE ('a) - 1) (uint w)"
    4.32  
    4.33 -definition unat :: "'a :: len0 word => nat" where
    4.34 +definition unat :: "'a :: len0 word => nat"
    4.35 +where
    4.36    "unat w = nat (uint w)"
    4.37  
    4.38 -definition uints :: "nat => int set" where
    4.39 +definition uints :: "nat => int set"
    4.40 +where
    4.41    -- "the sets of integers representing the words"
    4.42    "uints n = range (bintrunc n)"
    4.43  
    4.44 -definition sints :: "nat => int set" where
    4.45 +definition sints :: "nat => int set"
    4.46 +where
    4.47    "sints n = range (sbintrunc (n - 1))"
    4.48  
    4.49 -definition unats :: "nat => nat set" where
    4.50 +definition unats :: "nat => nat set"
    4.51 +where
    4.52    "unats n = {i. i < 2 ^ n}"
    4.53  
    4.54 -definition norm_sint :: "nat => int => int" where
    4.55 +definition norm_sint :: "nat => int => int"
    4.56 +where
    4.57    "norm_sint n w = (w + 2 ^ (n - 1)) mod 2 ^ n - 2 ^ (n - 1)"
    4.58  
    4.59 -definition scast :: "'a :: len word => 'b :: len word" where
    4.60 +definition scast :: "'a :: len word => 'b :: len word"
    4.61 +where
    4.62    -- "cast a word to a different length"
    4.63    "scast w = word_of_int (sint w)"
    4.64  
    4.65 -definition ucast :: "'a :: len0 word => 'b :: len0 word" where
    4.66 +definition ucast :: "'a :: len0 word => 'b :: len0 word"
    4.67 +where
    4.68    "ucast w = word_of_int (uint w)"
    4.69  
    4.70  instantiation word :: (len0) size
    4.71 @@ -138,29 +148,37 @@
    4.72  
    4.73  end
    4.74  
    4.75 -definition source_size :: "('a :: len0 word => 'b) => nat" where
    4.76 +definition source_size :: "('a :: len0 word => 'b) => nat"
    4.77 +where
    4.78    -- "whether a cast (or other) function is to a longer or shorter length"
    4.79    "source_size c = (let arb = undefined ; x = c arb in size arb)"  
    4.80  
    4.81 -definition target_size :: "('a => 'b :: len0 word) => nat" where
    4.82 +definition target_size :: "('a => 'b :: len0 word) => nat"
    4.83 +where
    4.84    "target_size c = size (c undefined)"
    4.85  
    4.86 -definition is_up :: "('a :: len0 word => 'b :: len0 word) => bool" where
    4.87 +definition is_up :: "('a :: len0 word => 'b :: len0 word) => bool"
    4.88 +where
    4.89    "is_up c \<longleftrightarrow> source_size c <= target_size c"
    4.90  
    4.91 -definition is_down :: "('a :: len0 word => 'b :: len0 word) => bool" where
    4.92 +definition is_down :: "('a :: len0 word => 'b :: len0 word) => bool"
    4.93 +where
    4.94    "is_down c \<longleftrightarrow> target_size c <= source_size c"
    4.95  
    4.96 -definition of_bl :: "bool list => 'a :: len0 word" where
    4.97 +definition of_bl :: "bool list => 'a :: len0 word"
    4.98 +where
    4.99    "of_bl bl = word_of_int (bl_to_bin bl)"
   4.100  
   4.101 -definition to_bl :: "'a :: len0 word => bool list" where
   4.102 +definition to_bl :: "'a :: len0 word => bool list"
   4.103 +where
   4.104    "to_bl w = bin_to_bl (len_of TYPE ('a)) (uint w)"
   4.105  
   4.106 -definition word_reverse :: "'a :: len0 word => 'a word" where
   4.107 +definition word_reverse :: "'a :: len0 word => 'a word"
   4.108 +where
   4.109    "word_reverse w = of_bl (rev (to_bl w))"
   4.110  
   4.111 -definition word_int_case :: "(int => 'b) => ('a :: len0 word) => 'b" where
   4.112 +definition word_int_case :: "(int => 'b) => ('a :: len0 word) => 'b" 
   4.113 +where
   4.114    "word_int_case f w = f (uint w)"
   4.115  
   4.116  translations
   4.117 @@ -232,7 +250,8 @@
   4.118  subsection {* Correspondence relation for theorem transfer *}
   4.119  
   4.120  definition cr_word :: "int \<Rightarrow> 'a::len0 word \<Rightarrow> bool"
   4.121 -  where "cr_word \<equiv> (\<lambda>x y. word_of_int x = y)"
   4.122 +where
   4.123 +  "cr_word = (\<lambda>x y. word_of_int x = y)"
   4.124  
   4.125  lemma Quotient_word:
   4.126    "Quotient (\<lambda>x y. bintrunc (len_of TYPE('a)) x = bintrunc (len_of TYPE('a)) y)
   4.127 @@ -341,7 +360,8 @@
   4.128    apply (simp add: word_of_nat wi_hom_sub)
   4.129    done
   4.130  
   4.131 -definition udvd :: "'a::len word => 'a::len word => bool" (infixl "udvd" 50) where
   4.132 +definition udvd :: "'a::len word => 'a::len word => bool" (infixl "udvd" 50)
   4.133 +where
   4.134    "a udvd b = (EX n>=0. uint b = n * uint a)"
   4.135  
   4.136  
   4.137 @@ -361,10 +381,12 @@
   4.138  
   4.139  end
   4.140  
   4.141 -definition word_sle :: "'a :: len word => 'a word => bool" ("(_/ <=s _)" [50, 51] 50) where
   4.142 +definition word_sle :: "'a :: len word => 'a word => bool" ("(_/ <=s _)" [50, 51] 50)
   4.143 +where
   4.144    "a <=s b = (sint a <= sint b)"
   4.145  
   4.146 -definition word_sless :: "'a :: len word => 'a word => bool" ("(_/ <s _)" [50, 51] 50) where
   4.147 +definition word_sless :: "'a :: len word => 'a word => bool" ("(_/ <s _)" [50, 51] 50)
   4.148 +where
   4.149    "(x <s y) = (x <=s y & x ~= y)"
   4.150  
   4.151  
   4.152 @@ -398,10 +420,12 @@
   4.153  definition
   4.154    word_lsb_def: "lsb a \<longleftrightarrow> bin_last (uint a)"
   4.155  
   4.156 -definition shiftl1 :: "'a word \<Rightarrow> 'a word" where
   4.157 +definition shiftl1 :: "'a word \<Rightarrow> 'a word"
   4.158 +where
   4.159    "shiftl1 w = word_of_int (uint w BIT False)"
   4.160  
   4.161 -definition shiftr1 :: "'a word \<Rightarrow> 'a word" where
   4.162 +definition shiftr1 :: "'a word \<Rightarrow> 'a word"
   4.163 +where
   4.164    -- "shift right as unsigned or as signed, ie logical or arithmetic"
   4.165    "shiftr1 w = word_of_int (bin_rest (uint w))"
   4.166  
   4.167 @@ -434,76 +458,95 @@
   4.168  
   4.169  end
   4.170  
   4.171 -definition setBit :: "'a :: len0 word => nat => 'a word" where 
   4.172 +definition setBit :: "'a :: len0 word => nat => 'a word"
   4.173 +where 
   4.174    "setBit w n = set_bit w n True"
   4.175  
   4.176 -definition clearBit :: "'a :: len0 word => nat => 'a word" where
   4.177 +definition clearBit :: "'a :: len0 word => nat => 'a word"
   4.178 +where
   4.179    "clearBit w n = set_bit w n False"
   4.180  
   4.181  
   4.182  subsection "Shift operations"
   4.183  
   4.184 -definition sshiftr1 :: "'a :: len word => 'a word" where 
   4.185 +definition sshiftr1 :: "'a :: len word => 'a word"
   4.186 +where 
   4.187    "sshiftr1 w = word_of_int (bin_rest (sint w))"
   4.188  
   4.189 -definition bshiftr1 :: "bool => 'a :: len word => 'a word" where
   4.190 +definition bshiftr1 :: "bool => 'a :: len word => 'a word"
   4.191 +where
   4.192    "bshiftr1 b w = of_bl (b # butlast (to_bl w))"
   4.193  
   4.194 -definition sshiftr :: "'a :: len word => nat => 'a word" (infixl ">>>" 55) where
   4.195 +definition sshiftr :: "'a :: len word => nat => 'a word" (infixl ">>>" 55)
   4.196 +where
   4.197    "w >>> n = (sshiftr1 ^^ n) w"
   4.198  
   4.199 -definition mask :: "nat => 'a::len word" where
   4.200 +definition mask :: "nat => 'a::len word"
   4.201 +where
   4.202    "mask n = (1 << n) - 1"
   4.203  
   4.204 -definition revcast :: "'a :: len0 word => 'b :: len0 word" where
   4.205 +definition revcast :: "'a :: len0 word => 'b :: len0 word"
   4.206 +where
   4.207    "revcast w =  of_bl (takefill False (len_of TYPE('b)) (to_bl w))"
   4.208  
   4.209 -definition slice1 :: "nat => 'a :: len0 word => 'b :: len0 word" where
   4.210 +definition slice1 :: "nat => 'a :: len0 word => 'b :: len0 word"
   4.211 +where
   4.212    "slice1 n w = of_bl (takefill False n (to_bl w))"
   4.213  
   4.214 -definition slice :: "nat => 'a :: len0 word => 'b :: len0 word" where
   4.215 +definition slice :: "nat => 'a :: len0 word => 'b :: len0 word"
   4.216 +where
   4.217    "slice n w = slice1 (size w - n) w"
   4.218  
   4.219  
   4.220  subsection "Rotation"
   4.221  
   4.222 -definition rotater1 :: "'a list => 'a list" where
   4.223 +definition rotater1 :: "'a list => 'a list"
   4.224 +where
   4.225    "rotater1 ys = 
   4.226      (case ys of [] => [] | x # xs => last ys # butlast ys)"
   4.227  
   4.228 -definition rotater :: "nat => 'a list => 'a list" where
   4.229 +definition rotater :: "nat => 'a list => 'a list"
   4.230 +where
   4.231    "rotater n = rotater1 ^^ n"
   4.232  
   4.233 -definition word_rotr :: "nat => 'a :: len0 word => 'a :: len0 word" where
   4.234 +definition word_rotr :: "nat => 'a :: len0 word => 'a :: len0 word"
   4.235 +where
   4.236    "word_rotr n w = of_bl (rotater n (to_bl w))"
   4.237  
   4.238 -definition word_rotl :: "nat => 'a :: len0 word => 'a :: len0 word" where
   4.239 +definition word_rotl :: "nat => 'a :: len0 word => 'a :: len0 word"
   4.240 +where
   4.241    "word_rotl n w = of_bl (rotate n (to_bl w))"
   4.242  
   4.243 -definition word_roti :: "int => 'a :: len0 word => 'a :: len0 word" where
   4.244 +definition word_roti :: "int => 'a :: len0 word => 'a :: len0 word"
   4.245 +where
   4.246    "word_roti i w = (if i >= 0 then word_rotr (nat i) w
   4.247                      else word_rotl (nat (- i)) w)"
   4.248  
   4.249  
   4.250  subsection "Split and cat operations"
   4.251  
   4.252 -definition word_cat :: "'a :: len0 word => 'b :: len0 word => 'c :: len0 word" where
   4.253 +definition word_cat :: "'a :: len0 word => 'b :: len0 word => 'c :: len0 word"
   4.254 +where
   4.255    "word_cat a b = word_of_int (bin_cat (uint a) (len_of TYPE ('b)) (uint b))"
   4.256  
   4.257 -definition word_split :: "'a :: len0 word => ('b :: len0 word) * ('c :: len0 word)" where
   4.258 +definition word_split :: "'a :: len0 word => ('b :: len0 word) * ('c :: len0 word)"
   4.259 +where
   4.260    "word_split a = 
   4.261     (case bin_split (len_of TYPE ('c)) (uint a) of 
   4.262       (u, v) => (word_of_int u, word_of_int v))"
   4.263  
   4.264 -definition word_rcat :: "'a :: len0 word list => 'b :: len0 word" where
   4.265 +definition word_rcat :: "'a :: len0 word list => 'b :: len0 word"
   4.266 +where
   4.267    "word_rcat ws = 
   4.268    word_of_int (bin_rcat (len_of TYPE ('a)) (map uint ws))"
   4.269  
   4.270 -definition word_rsplit :: "'a :: len0 word => 'b :: len word list" where
   4.271 +definition word_rsplit :: "'a :: len0 word => 'b :: len word list"
   4.272 +where
   4.273    "word_rsplit w = 
   4.274    map word_of_int (bin_rsplit (len_of TYPE ('b)) (len_of TYPE ('a), uint w))"
   4.275  
   4.276 -definition max_word :: "'a::len word" -- "Largest representable machine integer." where
   4.277 +definition max_word :: "'a::len word" -- "Largest representable machine integer."
   4.278 +where
   4.279    "max_word = word_of_int (2 ^ len_of TYPE('a) - 1)"
   4.280  
   4.281  (* FIXME: only provide one theorem name *)
   4.282 @@ -4536,7 +4579,8 @@
   4.283  
   4.284  subsection {* Recursion combinator for words *}
   4.285  
   4.286 -definition word_rec :: "'a \<Rightarrow> ('b::len word \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b word \<Rightarrow> 'a" where
   4.287 +definition word_rec :: "'a \<Rightarrow> ('b::len word \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b word \<Rightarrow> 'a"
   4.288 +where
   4.289    "word_rec forZero forSuc n = nat_rec forZero (forSuc \<circ> of_nat) (unat n)"
   4.290  
   4.291  lemma word_rec_0: "word_rec z s 0 = z"