renamed app2 to map2
authorhaftmann
Fri Apr 04 13:40:25 2008 +0200 (2008-04-04)
changeset 265587fcc10088e72
parent 26557 9e7f95903b24
child 26559 799983936aad
renamed app2 to map2
src/HOL/Word/BinOperations.thy
src/HOL/Word/WordBitwise.thy
src/HOL/Word/WordGenLib.thy
src/HOL/Word/WordShift.thy
     1.1 --- a/src/HOL/Word/BinOperations.thy	Fri Apr 04 13:40:24 2008 +0200
     1.2 +++ b/src/HOL/Word/BinOperations.thy	Fri Apr 04 13:40:25 2008 +0200
     1.3 @@ -9,8 +9,8 @@
     1.4  
     1.5  header {* Bitwise Operations on Binary Integers *}
     1.6  
     1.7 -theory BinOperations imports BinGeneral BitSyntax
     1.8 -
     1.9 +theory BinOperations
    1.10 +imports BinGeneral BitSyntax
    1.11  begin
    1.12  
    1.13  subsection {* Logical operations *}
    1.14 @@ -21,19 +21,19 @@
    1.15  begin
    1.16  
    1.17  definition
    1.18 -  int_not_def: "bitNOT = bin_rec Int.Min Int.Pls 
    1.19 +  int_not_def [code func del]: "bitNOT = bin_rec Int.Min Int.Pls 
    1.20      (\<lambda>w b s. s BIT (NOT b))"
    1.21  
    1.22  definition
    1.23 -  int_and_def: "bitAND = bin_rec (\<lambda>x. Int.Pls) (\<lambda>y. y) 
    1.24 +  int_and_def [code func del]: "bitAND = bin_rec (\<lambda>x. Int.Pls) (\<lambda>y. y) 
    1.25      (\<lambda>w b s y. s (bin_rest y) BIT (b AND bin_last y))"
    1.26  
    1.27  definition
    1.28 -  int_or_def: "bitOR = bin_rec (\<lambda>x. x) (\<lambda>y. Int.Min) 
    1.29 +  int_or_def [code func del]: "bitOR = bin_rec (\<lambda>x. x) (\<lambda>y. Int.Min) 
    1.30      (\<lambda>w b s y. s (bin_rest y) BIT (b OR bin_last y))"
    1.31  
    1.32  definition
    1.33 -  int_xor_def: "bitXOR = bin_rec (\<lambda>x. x) bitNOT 
    1.34 +  int_xor_def [code func del]: "bitXOR = bin_rec (\<lambda>x. x) bitNOT 
    1.35      (\<lambda>w b s y. s (bin_rest y) BIT (b XOR bin_last y))"
    1.36  
    1.37  instance ..
    1.38 @@ -43,16 +43,18 @@
    1.39  lemma int_not_simps [simp]:
    1.40    "NOT Int.Pls = Int.Min"
    1.41    "NOT Int.Min = Int.Pls"
    1.42 -  "NOT (w BIT b) = (NOT w) BIT (NOT b)"
    1.43    "NOT (Int.Bit0 w) = Int.Bit1 (NOT w)"
    1.44    "NOT (Int.Bit1 w) = Int.Bit0 (NOT w)"
    1.45 +  "NOT (w BIT b) = (NOT w) BIT (NOT b)"
    1.46    unfolding int_not_def by (simp_all add: bin_rec_simps)
    1.47  
    1.48 -lemma int_xor_Pls [simp]: 
    1.49 +declare int_not_simps(1-4) [code func]
    1.50 +
    1.51 +lemma int_xor_Pls [simp, code func]: 
    1.52    "Int.Pls XOR x = x"
    1.53    unfolding int_xor_def by (simp add: bin_rec_PM)
    1.54  
    1.55 -lemma int_xor_Min [simp]: 
    1.56 +lemma int_xor_Min [simp, code func]: 
    1.57    "Int.Min XOR x = NOT x"
    1.58    unfolding int_xor_def by (simp add: bin_rec_PM)
    1.59  
    1.60 @@ -67,7 +69,7 @@
    1.61    apply (simp add: int_not_simps [symmetric])
    1.62    done
    1.63  
    1.64 -lemma int_xor_Bits2 [simp]: 
    1.65 +lemma int_xor_Bits2 [simp, code func]: 
    1.66    "(Int.Bit0 x) XOR (Int.Bit0 y) = Int.Bit0 (x XOR y)"
    1.67    "(Int.Bit0 x) XOR (Int.Bit1 y) = Int.Bit1 (x XOR y)"
    1.68    "(Int.Bit1 x) XOR (Int.Bit0 y) = Int.Bit1 (x XOR y)"
    1.69 @@ -83,16 +85,16 @@
    1.70     apply clarsimp+
    1.71    done
    1.72  
    1.73 -lemma int_xor_extra_simps [simp]:
    1.74 +lemma int_xor_extra_simps [simp, code func]:
    1.75    "w XOR Int.Pls = w"
    1.76    "w XOR Int.Min = NOT w"
    1.77    using int_xor_x_simps' by simp_all
    1.78  
    1.79 -lemma int_or_Pls [simp]: 
    1.80 +lemma int_or_Pls [simp, code func]: 
    1.81    "Int.Pls OR x = x"
    1.82    by (unfold int_or_def) (simp add: bin_rec_PM)
    1.83    
    1.84 -lemma int_or_Min [simp]:
    1.85 +lemma int_or_Min [simp, code func]:
    1.86    "Int.Min OR x = Int.Min"
    1.87    by (unfold int_or_def) (simp add: bin_rec_PM)
    1.88  
    1.89 @@ -100,7 +102,7 @@
    1.90    "(x BIT b) OR (y BIT c) = (x OR y) BIT (b OR c)"
    1.91    unfolding int_or_def by (simp add: bin_rec_simps)
    1.92  
    1.93 -lemma int_or_Bits2 [simp]: 
    1.94 +lemma int_or_Bits2 [simp, code func]: 
    1.95    "(Int.Bit0 x) OR (Int.Bit0 y) = Int.Bit0 (x OR y)"
    1.96    "(Int.Bit0 x) OR (Int.Bit1 y) = Int.Bit1 (x OR y)"
    1.97    "(Int.Bit1 x) OR (Int.Bit0 y) = Int.Bit1 (x OR y)"
    1.98 @@ -116,16 +118,16 @@
    1.99     apply clarsimp+
   1.100    done
   1.101  
   1.102 -lemma int_or_extra_simps [simp]:
   1.103 +lemma int_or_extra_simps [simp, code func]:
   1.104    "w OR Int.Pls = w"
   1.105    "w OR Int.Min = Int.Min"
   1.106    using int_or_x_simps' by simp_all
   1.107  
   1.108 -lemma int_and_Pls [simp]:
   1.109 +lemma int_and_Pls [simp, code func]:
   1.110    "Int.Pls AND x = Int.Pls"
   1.111    unfolding int_and_def by (simp add: bin_rec_PM)
   1.112  
   1.113 -lemma int_and_Min [simp]:
   1.114 +lemma int_and_Min [simp, code func]:
   1.115    "Int.Min AND x = x"
   1.116    unfolding int_and_def by (simp add: bin_rec_PM)
   1.117  
   1.118 @@ -133,7 +135,7 @@
   1.119    "(x BIT b) AND (y BIT c) = (x AND y) BIT (b AND c)" 
   1.120    unfolding int_and_def by (simp add: bin_rec_simps)
   1.121  
   1.122 -lemma int_and_Bits2 [simp]: 
   1.123 +lemma int_and_Bits2 [simp, code func]: 
   1.124    "(Int.Bit0 x) AND (Int.Bit0 y) = Int.Bit0 (x AND y)"
   1.125    "(Int.Bit0 x) AND (Int.Bit1 y) = Int.Bit0 (x AND y)"
   1.126    "(Int.Bit1 x) AND (Int.Bit0 y) = Int.Bit0 (x AND y)"
   1.127 @@ -149,7 +151,7 @@
   1.128     apply clarsimp+
   1.129    done
   1.130  
   1.131 -lemma int_and_extra_simps [simp]:
   1.132 +lemma int_and_extra_simps [simp, code func]:
   1.133    "w AND Int.Pls = Int.Pls"
   1.134    "w AND Int.Min = w"
   1.135    using int_and_x_simps' by simp_all
   1.136 @@ -374,13 +376,11 @@
   1.137  
   1.138  subsection {* Setting and clearing bits *}
   1.139  
   1.140 -consts
   1.141 +primrec
   1.142    bin_sc :: "nat => bit => int => int"
   1.143 -
   1.144 -primrec
   1.145 -  Z : "bin_sc 0 b w = bin_rest w BIT b"
   1.146 -  Suc :
   1.147 -    "bin_sc (Suc n) b w = bin_sc n b (bin_rest w) BIT bin_last w"
   1.148 +where
   1.149 +  Z: "bin_sc 0 b w = bin_rest w BIT b"
   1.150 +  | Suc: "bin_sc (Suc n) b w = bin_sc n b (bin_rest w) BIT bin_last w"
   1.151  
   1.152  (** nth bit, set/clear **)
   1.153  
   1.154 @@ -479,76 +479,63 @@
   1.155  
   1.156  subsection {* Operations on lists of booleans *}
   1.157  
   1.158 -consts
   1.159 -  bin_to_bl :: "nat => int => bool list"
   1.160 -  bin_to_bl_aux :: "nat => int => bool list => bool list"
   1.161 -  bl_to_bin :: "bool list => int"
   1.162 -  bl_to_bin_aux :: "int => bool list => int"
   1.163 -
   1.164 -  bl_of_nth :: "nat => (nat => bool) => bool list"
   1.165 +primrec bl_to_bin_aux :: "bool list \<Rightarrow> int \<Rightarrow> int" where
   1.166 +  Nil: "bl_to_bin_aux [] w = w"
   1.167 +  | Cons: "bl_to_bin_aux (b # bs) w = 
   1.168 +      bl_to_bin_aux bs (w BIT (if b then bit.B1 else bit.B0))"
   1.169  
   1.170 -primrec
   1.171 -  Nil : "bl_to_bin_aux w [] = w"
   1.172 -  Cons : "bl_to_bin_aux w (b # bs) = 
   1.173 -      bl_to_bin_aux (w BIT (if b then bit.B1 else bit.B0)) bs"
   1.174 +definition bl_to_bin :: "bool list \<Rightarrow> int" where
   1.175 +  bl_to_bin_def : "bl_to_bin bs = bl_to_bin_aux bs Int.Pls"
   1.176  
   1.177 -primrec
   1.178 -  Z : "bin_to_bl_aux 0 w bl = bl"
   1.179 -  Suc : "bin_to_bl_aux (Suc n) w bl =
   1.180 -    bin_to_bl_aux n (bin_rest w) ((bin_last w = bit.B1) # bl)"
   1.181 +primrec bin_to_bl_aux :: "nat \<Rightarrow> int \<Rightarrow> bool list \<Rightarrow> bool list" where
   1.182 +  Z: "bin_to_bl_aux 0 w bl = bl"
   1.183 +  | Suc: "bin_to_bl_aux (Suc n) w bl =
   1.184 +      bin_to_bl_aux n (bin_rest w) ((bin_last w = bit.B1) # bl)"
   1.185  
   1.186 -defs
   1.187 -  bin_to_bl_def : "bin_to_bl n w == bin_to_bl_aux n w []"
   1.188 -  bl_to_bin_def : "bl_to_bin bs == bl_to_bin_aux Int.Pls bs"
   1.189 +definition bin_to_bl :: "nat \<Rightarrow> int \<Rightarrow> bool list" where
   1.190 +  bin_to_bl_def : "bin_to_bl n w = bin_to_bl_aux n w []"
   1.191  
   1.192 -primrec
   1.193 -  Suc : "bl_of_nth (Suc n) f = f n # bl_of_nth n f"
   1.194 -  Z : "bl_of_nth 0 f = []"
   1.195 +primrec bl_of_nth :: "nat \<Rightarrow> (nat \<Rightarrow> bool) \<Rightarrow> bool list" where
   1.196 +  Suc: "bl_of_nth (Suc n) f = f n # bl_of_nth n f"
   1.197 +  | Z: "bl_of_nth 0 f = []"
   1.198  
   1.199 -consts
   1.200 -  takefill :: "'a => nat => 'a list => 'a list"
   1.201 -  app2 :: "('a => 'b => 'c) => 'a list => 'b list => 'c list"
   1.202 +primrec takefill :: "'a \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   1.203 +  Z: "takefill fill 0 xs = []"
   1.204 +  | Suc: "takefill fill (Suc n) xs = (
   1.205 +      case xs of [] => fill # takefill fill n xs
   1.206 +        | y # ys => y # takefill fill n ys)"
   1.207  
   1.208 --- "takefill - like take but if argument list too short,"
   1.209 --- "extends result to get requested length"
   1.210 -primrec
   1.211 -  Z : "takefill fill 0 xs = []"
   1.212 -  Suc : "takefill fill (Suc n) xs = (
   1.213 -    case xs of [] => fill # takefill fill n xs
   1.214 -      | y # ys => y # takefill fill n ys)"
   1.215 +definition map2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list" where
   1.216 +  "map2 f as bs = map (split f) (zip as bs)"
   1.217  
   1.218 -defs
   1.219 -  app2_def : "app2 f as bs == map (split f) (zip as bs)"
   1.220  
   1.221  subsection {* Splitting and concatenation *}
   1.222  
   1.223 --- "rcat and rsplit"
   1.224 -consts
   1.225 -  bin_rcat :: "nat => int list => int"
   1.226 -  bin_rsplit_aux :: "nat * int list * nat * int => int list"
   1.227 -  bin_rsplit :: "nat => (nat * int) => int list"
   1.228 -  bin_rsplitl_aux :: "nat * int list * nat * int => int list"
   1.229 -  bin_rsplitl :: "nat => (nat * int) => int list"
   1.230 -  
   1.231 -recdef bin_rsplit_aux "measure (fst o snd o snd)"
   1.232 -  "bin_rsplit_aux (n, bs, (m, c)) =
   1.233 +definition bin_rcat :: "nat \<Rightarrow> int list \<Rightarrow> int" where
   1.234 +  "bin_rcat n = foldl (%u v. bin_cat u n v) Int.Pls"
   1.235 +
   1.236 +function bin_rsplit_aux :: "nat \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list" where
   1.237 +  "bin_rsplit_aux n m c bs =
   1.238      (if m = 0 | n = 0 then bs else
   1.239        let (a, b) = bin_split n c 
   1.240 -      in bin_rsplit_aux (n, b # bs, (m - n, a)))"
   1.241 +      in bin_rsplit_aux n (m - n) a (b # bs))"
   1.242 +by pat_completeness auto
   1.243 +termination by (relation "measure (fst o snd)") simp_all
   1.244  
   1.245 -recdef bin_rsplitl_aux "measure (fst o snd o snd)"
   1.246 -  "bin_rsplitl_aux (n, bs, (m, c)) =
   1.247 +definition bin_rsplit :: "nat \<Rightarrow> nat \<times> int \<Rightarrow> int list" where
   1.248 +  "bin_rsplit n w = bin_rsplit_aux n (fst w) (snd w) []"
   1.249 +
   1.250 +function bin_rsplitl_aux :: "nat \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list" where
   1.251 +  "bin_rsplitl_aux n m c bs =
   1.252      (if m = 0 | n = 0 then bs else
   1.253        let (a, b) = bin_split (min m n) c 
   1.254 -      in bin_rsplitl_aux (n, b # bs, (m - n, a)))"
   1.255 +      in bin_rsplitl_aux n (m - n) a (b # bs))"
   1.256 +by pat_completeness auto
   1.257 +termination by (relation "measure (fst o snd)") simp_all
   1.258  
   1.259 -defs
   1.260 -  bin_rcat_def : "bin_rcat n bs == foldl (%u v. bin_cat u n v) Int.Pls bs"
   1.261 -  bin_rsplit_def : "bin_rsplit n w == bin_rsplit_aux (n, [], w)"
   1.262 -  bin_rsplitl_def : "bin_rsplitl n w == bin_rsplitl_aux (n, [], w)"
   1.263 -     
   1.264 - 
   1.265 -(* potential for looping *)
   1.266 +definition bin_rsplitl :: "nat \<Rightarrow> nat \<times> int \<Rightarrow> int list" where
   1.267 +  "bin_rsplitl n w = bin_rsplitl_aux n (fst w) (snd w) []"
   1.268 +
   1.269  declare bin_rsplit_aux.simps [simp del]
   1.270  declare bin_rsplitl_aux.simps [simp del]
   1.271  
     2.1 --- a/src/HOL/Word/WordBitwise.thy	Fri Apr 04 13:40:24 2008 +0200
     2.2 +++ b/src/HOL/Word/WordBitwise.thy	Fri Apr 04 13:40:25 2008 +0200
     2.3 @@ -7,7 +7,9 @@
     2.4  
     2.5  header {* Bitwise Operations on Words *}
     2.6  
     2.7 -theory WordBitwise imports WordArith begin
     2.8 +theory WordBitwise
     2.9 +imports WordArith
    2.10 +begin
    2.11  
    2.12  lemmas bin_log_bintrs = bin_trunc_not bin_trunc_xor bin_trunc_and bin_trunc_or
    2.13    
    2.14 @@ -205,15 +207,15 @@
    2.15    unfolding to_bl_def word_log_defs
    2.16    by (simp add: bl_not_bin number_of_is_id word_no_wi [symmetric])
    2.17  
    2.18 -lemma bl_word_xor: "to_bl (v XOR w) = app2 op ~= (to_bl v) (to_bl w)" 
    2.19 +lemma bl_word_xor: "to_bl (v XOR w) = map2 op ~= (to_bl v) (to_bl w)" 
    2.20    unfolding to_bl_def word_log_defs bl_xor_bin
    2.21    by (simp add: number_of_is_id word_no_wi [symmetric])
    2.22  
    2.23 -lemma bl_word_or: "to_bl (v OR w) = app2 op | (to_bl v) (to_bl w)" 
    2.24 +lemma bl_word_or: "to_bl (v OR w) = map2 op | (to_bl v) (to_bl w)" 
    2.25    unfolding to_bl_def word_log_defs
    2.26    by (simp add: bl_or_bin number_of_is_id word_no_wi [symmetric])
    2.27  
    2.28 -lemma bl_word_and: "to_bl (v AND w) = app2 op & (to_bl v) (to_bl w)" 
    2.29 +lemma bl_word_and: "to_bl (v AND w) = map2 op & (to_bl v) (to_bl w)" 
    2.30    unfolding to_bl_def word_log_defs
    2.31    by (simp add: bl_and_bin number_of_is_id word_no_wi [symmetric])
    2.32  
     3.1 --- a/src/HOL/Word/WordGenLib.thy	Fri Apr 04 13:40:24 2008 +0200
     3.2 +++ b/src/HOL/Word/WordGenLib.thy	Fri Apr 04 13:40:25 2008 +0200
     3.3 @@ -8,7 +8,8 @@
     3.4  
     3.5  header {* Miscellaneous Library for Words *}
     3.6  
     3.7 -theory WordGenLib imports WordShift Boolean_Algebra
     3.8 +theory WordGenLib
     3.9 +imports WordShift Boolean_Algebra
    3.10  begin
    3.11  
    3.12  declare of_nat_2p [simp]
    3.13 @@ -174,14 +175,14 @@
    3.14  proof - 
    3.15    note [simp] = map_replicate_True map_replicate_False
    3.16    have "to_bl (w AND mask n) = 
    3.17 -        app2 op & (to_bl w) (to_bl (mask n::'a::len word))"
    3.18 +        map2 op & (to_bl w) (to_bl (mask n::'a::len word))"
    3.19      by (simp add: bl_word_and)
    3.20    also
    3.21    have "to_bl w = take n' (to_bl w) @ drop n' (to_bl w)" by simp
    3.22    also
    3.23 -  have "app2 op & \<dots> (to_bl (mask n::'a::len word)) = 
    3.24 +  have "map2 op & \<dots> (to_bl (mask n::'a::len word)) = 
    3.25          replicate n' False @ drop n' (to_bl w)"
    3.26 -    unfolding to_bl_mask n'_def app2_def
    3.27 +    unfolding to_bl_mask n'_def map2_def
    3.28      by (subst zip_append) auto
    3.29    finally
    3.30    show ?thesis .
     4.1 --- a/src/HOL/Word/WordShift.thy	Fri Apr 04 13:40:24 2008 +0200
     4.2 +++ b/src/HOL/Word/WordShift.thy	Fri Apr 04 13:40:25 2008 +0200
     4.3 @@ -7,7 +7,9 @@
     4.4  
     4.5  header {* Shifting, Rotating, and Splitting Words *}
     4.6  
     4.7 -theory WordShift imports WordBitwise begin
     4.8 +theory WordShift
     4.9 +imports WordBitwise
    4.10 +begin
    4.11  
    4.12  subsection "Bit shifting"
    4.13  
    4.14 @@ -421,7 +423,7 @@
    4.15  lemma align_lem_or [rule_format] :
    4.16    "ALL x m. length x = n + m --> length y = n + m --> 
    4.17      drop m x = replicate n False --> take m y = replicate m False --> 
    4.18 -    app2 op | x y = take m x @ drop m y"
    4.19 +    map2 op | x y = take m x @ drop m y"
    4.20    apply (induct_tac y)
    4.21     apply force
    4.22    apply clarsimp
    4.23 @@ -435,7 +437,7 @@
    4.24  lemma align_lem_and [rule_format] :
    4.25    "ALL x m. length x = n + m --> length y = n + m --> 
    4.26      drop m x = replicate n False --> take m y = replicate m False --> 
    4.27 -    app2 op & x y = replicate (n + m) False"
    4.28 +    map2 op & x y = replicate (n + m) False"
    4.29    apply (induct_tac y)
    4.30     apply force
    4.31    apply clarsimp
    4.32 @@ -1344,7 +1346,7 @@
    4.33  lemmas rotater_add = rotater_eqs (2)
    4.34  
    4.35  
    4.36 -subsubsection "map, app2, commuting with rotate(r)"
    4.37 +subsubsection "map, map2, commuting with rotate(r)"
    4.38  
    4.39  lemma last_map: "xs ~= [] ==> last (map f xs) = f (last xs)"
    4.40    by (induct xs) auto
    4.41 @@ -1371,13 +1373,13 @@
    4.42       apply ((case_tac ys, auto simp: neq_Nil_conv)[1])+
    4.43    done
    4.44  
    4.45 -lemma but_last_app2 [rule_format] :
    4.46 +lemma but_last_map2 [rule_format] :
    4.47    "ALL ys. length xs = length ys --> xs ~= [] --> 
    4.48 -    last (app2 f xs ys) = f (last xs) (last ys) & 
    4.49 -    butlast (app2 f xs ys) = app2 f (butlast xs) (butlast ys)" 
    4.50 +    last (map2 f xs ys) = f (last xs) (last ys) & 
    4.51 +    butlast (map2 f xs ys) = map2 f (butlast xs) (butlast ys)" 
    4.52    apply (induct "xs")
    4.53    apply auto
    4.54 -     apply (unfold app2_def)
    4.55 +     apply (unfold map2_def)
    4.56       apply ((case_tac ys, auto simp: neq_Nil_conv)[1])+
    4.57    done
    4.58  
    4.59 @@ -1390,35 +1392,35 @@
    4.60     apply ((case_tac ys, auto simp: neq_Nil_conv but_last_zip)[1])+
    4.61    done
    4.62  
    4.63 -lemma rotater1_app2:
    4.64 +lemma rotater1_map2:
    4.65    "length xs = length ys ==> 
    4.66 -    rotater1 (app2 f xs ys) = app2 f (rotater1 xs) (rotater1 ys)" 
    4.67 -  unfolding app2_def by (simp add: rotater1_map rotater1_zip)
    4.68 +    rotater1 (map2 f xs ys) = map2 f (rotater1 xs) (rotater1 ys)" 
    4.69 +  unfolding map2_def by (simp add: rotater1_map rotater1_zip)
    4.70  
    4.71  lemmas lrth = 
    4.72    box_equals [OF asm_rl length_rotater [symmetric] 
    4.73                   length_rotater [symmetric], 
    4.74 -              THEN rotater1_app2]
    4.75 +              THEN rotater1_map2]
    4.76  
    4.77 -lemma rotater_app2: 
    4.78 +lemma rotater_map2: 
    4.79    "length xs = length ys ==> 
    4.80 -    rotater n (app2 f xs ys) = app2 f (rotater n xs) (rotater n ys)" 
    4.81 +    rotater n (map2 f xs ys) = map2 f (rotater n xs) (rotater n ys)" 
    4.82    by (induct n) (auto intro!: lrth)
    4.83  
    4.84 -lemma rotate1_app2:
    4.85 +lemma rotate1_map2:
    4.86    "length xs = length ys ==> 
    4.87 -    rotate1 (app2 f xs ys) = app2 f (rotate1 xs) (rotate1 ys)" 
    4.88 -  apply (unfold app2_def)
    4.89 +    rotate1 (map2 f xs ys) = map2 f (rotate1 xs) (rotate1 ys)" 
    4.90 +  apply (unfold map2_def)
    4.91    apply (cases xs)
    4.92     apply (cases ys, auto simp add : rotate1_def)+
    4.93    done
    4.94  
    4.95  lemmas lth = box_equals [OF asm_rl length_rotate [symmetric] 
    4.96 -  length_rotate [symmetric], THEN rotate1_app2]
    4.97 +  length_rotate [symmetric], THEN rotate1_map2]
    4.98  
    4.99 -lemma rotate_app2: 
   4.100 +lemma rotate_map2: 
   4.101    "length xs = length ys ==> 
   4.102 -    rotate n (app2 f xs ys) = app2 f (rotate n xs) (rotate n ys)" 
   4.103 +    rotate n (map2 f xs ys) = map2 f (rotate n xs) (rotate n ys)" 
   4.104    by (induct n) (auto intro!: lth)
   4.105  
   4.106  
   4.107 @@ -1537,11 +1539,11 @@
   4.108  
   4.109  lemmas lbl_lbl = trans [OF word_bl.Rep' word_bl.Rep' [symmetric]]
   4.110  
   4.111 -lemmas ths_app2 [OF lbl_lbl] = rotate_app2 rotater_app2
   4.112 +lemmas ths_map2 [OF lbl_lbl] = rotate_map2 rotater_map2
   4.113  
   4.114  lemmas ths_map [where xs = "to_bl v"] = rotate_map rotater_map
   4.115  
   4.116 -lemmas th1s [simplified word_rot_defs' [symmetric]] = ths_app2 ths_map
   4.117 +lemmas th1s [simplified word_rot_defs' [symmetric]] = ths_map2 ths_map
   4.118  
   4.119  lemma word_rot_logs:
   4.120    "word_rotl n (NOT v) = NOT word_rotl n v"