# HG changeset patch
# User haftmann
# Date 1277908863 -7200
# Node ID 17e1085d07b2aaec218532b9b24cb2cd8a8447d4
# Parent  4f0d6abc4475a23efbf9f0010d984cc4c92c6d9e
moved specific operations here

diff -r 4f0d6abc4475 -r 17e1085d07b2 src/HOL/Word/BinBoolList.thy
--- a/src/HOL/Word/BinBoolList.thy	Wed Jun 30 16:28:29 2010 +0200
+++ b/src/HOL/Word/BinBoolList.thy	Wed Jun 30 16:41:03 2010 +0200
@@ -12,6 +12,48 @@
 imports BinOperations
 begin
 
+subsection {* Operations on lists of booleans *}
+
+primrec bl_to_bin_aux :: "bool list \<Rightarrow> int \<Rightarrow> int" where
+  Nil: "bl_to_bin_aux [] w = w"
+  | Cons: "bl_to_bin_aux (b # bs) w = 
+      bl_to_bin_aux bs (w BIT (if b then 1 else 0))"
+
+definition bl_to_bin :: "bool list \<Rightarrow> int" where
+  bl_to_bin_def : "bl_to_bin bs = bl_to_bin_aux bs Int.Pls"
+
+primrec bin_to_bl_aux :: "nat \<Rightarrow> int \<Rightarrow> bool list \<Rightarrow> bool list" where
+  Z: "bin_to_bl_aux 0 w bl = bl"
+  | Suc: "bin_to_bl_aux (Suc n) w bl =
+      bin_to_bl_aux n (bin_rest w) ((bin_last w = 1) # bl)"
+
+definition bin_to_bl :: "nat \<Rightarrow> int \<Rightarrow> bool list" where
+  bin_to_bl_def : "bin_to_bl n w = bin_to_bl_aux n w []"
+
+primrec bl_of_nth :: "nat \<Rightarrow> (nat \<Rightarrow> bool) \<Rightarrow> bool list" where
+  Suc: "bl_of_nth (Suc n) f = f n # bl_of_nth n f"
+  | Z: "bl_of_nth 0 f = []"
+
+primrec takefill :: "'a \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+  Z: "takefill fill 0 xs = []"
+  | Suc: "takefill fill (Suc n) xs = (
+      case xs of [] => fill # takefill fill n xs
+        | y # ys => y # takefill fill n ys)"
+
+definition map2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list" where
+  "map2 f as bs = map (split f) (zip as bs)"
+
+lemma map2_Nil [simp]: "map2 f [] ys = []"
+  unfolding map2_def by auto
+
+lemma map2_Nil2 [simp]: "map2 f xs [] = []"
+  unfolding map2_def by auto
+
+lemma map2_Cons [simp]:
+  "map2 f (x # xs) (y # ys) = f x y # map2 f xs ys"
+  unfolding map2_def by auto
+
+
 subsection "Arithmetic in terms of bool lists"
 
 (* arithmetic operations in terms of the reversed bool list,
@@ -403,13 +445,6 @@
 
 (** links between bit-wise operations and operations on bool lists **)
     
-lemma map2_Nil [simp]: "map2 f [] ys = []"
-  unfolding map2_def by auto
-
-lemma map2_Cons [simp]:
-  "map2 f (x # xs) (y # ys) = f x y # map2 f xs ys"
-  unfolding map2_def by auto
-
 lemma bl_xor_aux_bin [rule_format] : "ALL v w bs cs. 
     map2 (%x y. x ~= y) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) = 
     bin_to_bl_aux n (v XOR w) (map2 (%x y. x ~= y) bs cs)"
diff -r 4f0d6abc4475 -r 17e1085d07b2 src/HOL/Word/BinOperations.thy
--- a/src/HOL/Word/BinOperations.thy	Wed Jun 30 16:28:29 2010 +0200
+++ b/src/HOL/Word/BinOperations.thy	Wed Jun 30 16:41:03 2010 +0200
@@ -476,37 +476,6 @@
 lemmas bin_sc_Suc_pred [simp] = 
   bin_sc_Suc_minus [of "number_of bin", simplified nobm1, standard]
 
-subsection {* Operations on lists of booleans *}
-
-primrec bl_to_bin_aux :: "bool list \<Rightarrow> int \<Rightarrow> int" where
-  Nil: "bl_to_bin_aux [] w = w"
-  | Cons: "bl_to_bin_aux (b # bs) w = 
-      bl_to_bin_aux bs (w BIT (if b then 1 else 0))"
-
-definition bl_to_bin :: "bool list \<Rightarrow> int" where
-  bl_to_bin_def : "bl_to_bin bs = bl_to_bin_aux bs Int.Pls"
-
-primrec bin_to_bl_aux :: "nat \<Rightarrow> int \<Rightarrow> bool list \<Rightarrow> bool list" where
-  Z: "bin_to_bl_aux 0 w bl = bl"
-  | Suc: "bin_to_bl_aux (Suc n) w bl =
-      bin_to_bl_aux n (bin_rest w) ((bin_last w = 1) # bl)"
-
-definition bin_to_bl :: "nat \<Rightarrow> int \<Rightarrow> bool list" where
-  bin_to_bl_def : "bin_to_bl n w = bin_to_bl_aux n w []"
-
-primrec bl_of_nth :: "nat \<Rightarrow> (nat \<Rightarrow> bool) \<Rightarrow> bool list" where
-  Suc: "bl_of_nth (Suc n) f = f n # bl_of_nth n f"
-  | Z: "bl_of_nth 0 f = []"
-
-primrec takefill :: "'a \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where
-  Z: "takefill fill 0 xs = []"
-  | Suc: "takefill fill (Suc n) xs = (
-      case xs of [] => fill # takefill fill n xs
-        | y # ys => y # takefill fill n ys)"
-
-definition map2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list" where
-  "map2 f as bs = map (split f) (zip as bs)"
-
 
 subsection {* Splitting and concatenation *}