# HG changeset patch
# User huffman
# Date 1187739755 -7200
# Node ID c1e20c65a3be8e21f0e646b1e919a531be608c4b
# Parent  8df021f79e0b30b42c8eae09de523bbaef3cbd75
move bool list stuff from BinOperations to BinBoolList;
reorganize BinBoolList into subsections

diff -r 8df021f79e0b -r c1e20c65a3be src/HOL/Word/BinBoolList.thy
--- a/src/HOL/Word/BinBoolList.thy	Tue Aug 21 21:50:23 2007 +0200
+++ b/src/HOL/Word/BinBoolList.thy	Wed Aug 22 01:42:35 2007 +0200
@@ -11,32 +11,7 @@
 
 theory BinBoolList imports BinOperations begin
 
-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 *)
-  rbl_succ :: "bool list => bool list"
-  rbl_pred :: "bool list => bool list"
-  rbl_add :: "bool list => bool list => bool list"
-  rbl_mult :: "bool list => bool list => bool list"
-
-primrec 
-  Nil: "rbl_succ Nil = Nil"
-  Cons: "rbl_succ (x # xs) = (if x then False # rbl_succ xs else True # xs)"
-
-primrec 
-  Nil : "rbl_pred Nil = Nil"
-  Cons : "rbl_pred (x # xs) = (if x then False # xs else True # rbl_pred xs)"
-
-primrec (* result is length of first arg, second arg may be longer *)
-  Nil : "rbl_add Nil x = Nil"
-  Cons : "rbl_add (y # ys) x = (let ws = rbl_add ys (tl x) in 
-    (y ~= hd x) # (if hd x & y then rbl_succ ws else ws))"
-
-primrec (* result is length of first arg, second arg may be longer *)
-  Nil : "rbl_mult Nil x = Nil"
-  Cons : "rbl_mult (y # ys) x = (let ws = False # rbl_mult ys x in 
-    if y then rbl_add ws x else ws)"
+subsection "Lemmas about standard list operations"
 
 lemma tl_take: "tl (take n l) = take (n - 1) (tl l)"
   apply (cases n, clarsimp)
@@ -75,6 +50,34 @@
   "(butlast ^ n) bl = take (length bl - n) bl"
   by (induct n) (auto simp: butlast_take)
 
+lemma nth_rev [rule_format] : 
+  "n < length xs --> rev xs ! n = xs ! (length xs - 1 - n)"
+  apply (induct_tac "xs")
+   apply simp
+  apply (clarsimp simp add : nth_append nth.simps split add : nat.split)
+  apply (rule_tac f = "%n. list ! n" in arg_cong) 
+  apply arith
+  done
+
+lemmas nth_rev_alt = nth_rev [where xs = "rev ?ys", simplified]
+
+lemma hd_butlast: "size xs > 1 ==> hd (butlast xs) = hd xs"
+  by (cases xs) auto
+
+subsection "From integers to bool lists"
+
+consts
+  bin_to_bl :: "nat => int => bool list"
+  bin_to_bl_aux :: "nat => int => bool list => bool list"
+
+primrec
+  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 = bit.B1) # bl)"
+
+defs
+  bin_to_bl_def : "bin_to_bl n w == bin_to_bl_aux n w []"
+
 lemma bin_to_bl_aux_Pls_minus_simp:
   "0 < n ==> bin_to_bl_aux n Numeral.Pls bl = 
     bin_to_bl_aux (n - 1) Numeral.Pls (False # bl)"
@@ -94,81 +97,24 @@
   bin_to_bl_aux_Min_minus_simp [simp]
   bin_to_bl_aux_Bit_minus_simp [simp]
 
-(** link between bin and bool list **)
-
-lemma bl_to_bin_aux_append [rule_format] : 
-  "ALL w. bl_to_bin_aux w (bs @ cs) = bl_to_bin_aux (bl_to_bin_aux w bs) cs"
-  by (induct bs) auto
-
 lemma bin_to_bl_aux_append [rule_format] : 
   "ALL w bs. bin_to_bl_aux n w bs @ cs = bin_to_bl_aux n w (bs @ cs)"
   by (induct n) auto
 
-lemma bl_to_bin_append: 
-  "bl_to_bin (bs @ cs) = bl_to_bin_aux (bl_to_bin bs) cs"
-  unfolding bl_to_bin_def by (rule bl_to_bin_aux_append)
-
 lemma bin_to_bl_aux_alt: 
   "bin_to_bl_aux n w bs = bin_to_bl n w @ bs" 
   unfolding bin_to_bl_def by (simp add : bin_to_bl_aux_append)
 
-lemma bin_to_bl_0: "bin_to_bl 0 bs = []"
+lemma bin_to_bl_0 [simp]: "bin_to_bl 0 bs = []"
   unfolding bin_to_bl_def by auto
 
 lemma size_bin_to_bl_aux [rule_format] : 
   "ALL w bs. size (bin_to_bl_aux n w bs) = n + length bs"
   by (induct n) auto
 
-lemma size_bin_to_bl: "size (bin_to_bl n w) = n" 
+lemma size_bin_to_bl [simp]: "size (bin_to_bl n w) = n" 
   unfolding bin_to_bl_def by (simp add : size_bin_to_bl_aux)
 
-lemma bin_bl_bin' [rule_format] : 
-  "ALL w bs. bl_to_bin (bin_to_bl_aux n w bs) = 
-    bl_to_bin_aux (bintrunc n w) bs"
-  by (induct n) (auto simp add : bl_to_bin_def)
-
-lemma bin_bl_bin: "bl_to_bin (bin_to_bl n w) = bintrunc n w"
-  unfolding bin_to_bl_def bin_bl_bin' by auto
-
-lemma bl_bin_bl' [rule_format] :
-  "ALL w n. bin_to_bl (n + length bs) (bl_to_bin_aux w bs) = 
-    bin_to_bl_aux n w bs"
-  apply (induct "bs")
-   apply auto
-    apply (simp_all only : add_Suc [symmetric])
-    apply (auto simp add : bin_to_bl_def)
-  done
-
-lemma bl_bin_bl: "bin_to_bl (length bs) (bl_to_bin bs) = bs"
-  unfolding bl_to_bin_def
-  apply (rule box_equals)
-    apply (rule bl_bin_bl')
-   prefer 2
-   apply (rule bin_to_bl_aux.Z)
-  apply simp
-  done
-  
-declare 
-  bin_to_bl_0 [simp] 
-  size_bin_to_bl [simp] 
-  bin_bl_bin [simp] 
-  bl_bin_bl [simp]
-
-lemma bl_to_bin_inj:
-  "bl_to_bin bs = bl_to_bin cs ==> length bs = length cs ==> bs = cs"
-  apply (rule_tac box_equals)
-    defer
-    apply (rule bl_bin_bl)
-   apply (rule bl_bin_bl)
-  apply simp
-  done
-
-lemma bl_to_bin_False: "bl_to_bin (False # bl) = bl_to_bin bl"
-  unfolding bl_to_bin_def by auto
-  
-lemma bl_to_bin_Nil: "bl_to_bin [] = Numeral.Pls"
-  unfolding bl_to_bin_def by auto
-
 lemma bin_to_bl_Pls_aux [rule_format] : 
   "ALL bl. bin_to_bl_aux n Numeral.Pls bl = replicate n False @ bl"
   by (induct n) (auto simp: replicate_app_Cons_same)
@@ -183,21 +129,6 @@
 lemma bin_to_bl_Min: "bin_to_bl n Numeral.Min = replicate n True"
   unfolding bin_to_bl_def by (simp add : bin_to_bl_Min_aux)
 
-lemma bl_to_bin_rep_F: 
-  "bl_to_bin (replicate n False @ bl) = bl_to_bin bl"
-  apply (simp add: bin_to_bl_Pls_aux [symmetric] bin_bl_bin')
-  apply (simp add: bl_to_bin_def)
-  done
-
-lemma bin_to_bl_trunc:
-  "n <= m ==> bin_to_bl n (bintrunc m w) = bin_to_bl n w"
-  by (auto intro: bl_to_bin_inj)
-
-declare 
-  bin_to_bl_trunc [simp] 
-  bl_to_bin_False [simp] 
-  bl_to_bin_Nil [simp]
-
 lemma bin_to_bl_aux_bintr [rule_format] :
   "ALL m bin bl. bin_to_bl_aux n (bintrunc m bin) bl = 
     replicate (n - m) False @ bin_to_bl_aux (min n m) bin bl"
@@ -214,16 +145,95 @@
 lemmas bin_to_bl_bintr = 
   bin_to_bl_aux_bintr [where bl = "[]", folded bin_to_bl_def]
 
-lemma bl_to_bin_rep_False: "bl_to_bin (replicate n False) = Numeral.Pls"
-  by (induct n) auto
-
 lemma len_bin_to_bl_aux [rule_format] : 
   "ALL w bs. length (bin_to_bl_aux n w bs) = n + length bs"
   by (induct "n") auto
 
 lemma len_bin_to_bl [simp]: "length (bin_to_bl n w) = n"
   unfolding bin_to_bl_def len_bin_to_bl_aux by auto
+
+
+subsection "From bool lists to integers"
+
+consts
+  bl_to_bin :: "bool list => int"
+  bl_to_bin_aux :: "int => bool list => int"
+
+primrec
+  Nil : "bl_to_bin_aux w [] = w"
+  Cons : "bl_to_bin_aux w (b # bs) = 
+      bl_to_bin_aux (w BIT (if b then bit.B1 else bit.B0)) bs"
+
+defs
+  bl_to_bin_def : "bl_to_bin bs == bl_to_bin_aux Numeral.Pls bs"
+
+(** link between bin and bool list **)
+
+lemma bl_to_bin_aux_append [rule_format] : 
+  "ALL w. bl_to_bin_aux w (bs @ cs) = bl_to_bin_aux (bl_to_bin_aux w bs) cs"
+  by (induct bs) auto
+
+lemma bl_to_bin_append: 
+  "bl_to_bin (bs @ cs) = bl_to_bin_aux (bl_to_bin bs) cs"
+  unfolding bl_to_bin_def by (rule bl_to_bin_aux_append)
+
+lemma bl_to_bin_False [simp]: "bl_to_bin (False # bl) = bl_to_bin bl"
+  unfolding bl_to_bin_def by auto
   
+lemma bl_to_bin_Nil [simp]: "bl_to_bin [] = Numeral.Pls"
+  unfolding bl_to_bin_def by auto
+
+lemma bl_to_bin_rep_F: 
+  "bl_to_bin (replicate n False @ bl) = bl_to_bin bl"
+  by (induct n) auto
+
+lemma bl_to_bin_rep_False: "bl_to_bin (replicate n False) = Numeral.Pls"
+  by (induct n) auto
+
+
+subsection "Converting between bool lists and integers"
+
+lemma bin_bl_bin' [rule_format] : 
+  "ALL w bs. bl_to_bin (bin_to_bl_aux n w bs) = 
+    bl_to_bin_aux (bintrunc n w) bs"
+  by (induct n) (auto simp add : bl_to_bin_def)
+
+lemma bin_bl_bin [simp]: "bl_to_bin (bin_to_bl n w) = bintrunc n w"
+  unfolding bin_to_bl_def bin_bl_bin' by auto
+
+lemma bl_bin_bl' [rule_format] :
+  "ALL w n. bin_to_bl (n + length bs) (bl_to_bin_aux w bs) = 
+    bin_to_bl_aux n w bs"
+  apply (induct "bs")
+   apply auto
+    apply (simp_all only : add_Suc [symmetric])
+    apply (auto simp add : bin_to_bl_def)
+  done
+
+lemma bl_bin_bl [simp]: "bin_to_bl (length bs) (bl_to_bin bs) = bs"
+  unfolding bl_to_bin_def
+  apply (rule box_equals)
+    apply (rule bl_bin_bl')
+   prefer 2
+   apply (rule bin_to_bl_aux.Z)
+  apply simp
+  done
+  
+lemma bl_to_bin_inj:
+  "bl_to_bin bs = bl_to_bin cs ==> length bs = length cs ==> bs = cs"
+  apply (rule_tac box_equals)
+    defer
+    apply (rule bl_bin_bl)
+   apply (rule bl_bin_bl)
+  apply simp
+  done
+
+lemma bin_to_bl_trunc [simp]:
+  "n <= m ==> bin_to_bl n (bintrunc m w) = bin_to_bl n w"
+  by (auto intro: bl_to_bin_inj)
+
+subsection "@{term bin_sign} with bool list operations"
+
 lemma sign_bl_bin' [rule_format] : 
   "ALL w. bin_sign (bl_to_bin_aux w bs) = bin_sign w"
   by (induct bs) auto
@@ -245,6 +255,8 @@
   "hd (bin_to_bl (Suc n) w) = (bin_sign (sbintrunc n w) = Numeral.Min)"
   unfolding bin_to_bl_def by (rule bl_sbin_sign_aux)
 
+subsection "@{term bin_nth} with bool list operations"
+
 lemma bin_nth_of_bl_aux [rule_format] : 
   "ALL w. bin_nth (bl_to_bin_aux w bl) n = 
     (n < size bl & rev bl ! n | n >= length bl & bin_nth w (n - size bl))"
@@ -272,17 +284,6 @@
   apply (simp add: bin_to_bl_aux_alt)
   done
 
-lemma nth_rev [rule_format] : 
-  "n < length xs --> rev xs ! n = xs ! (length xs - 1 - n)"
-  apply (induct_tac "xs")
-   apply simp
-  apply (clarsimp simp add : nth_append nth.simps split add : nat.split)
-  apply (rule_tac f = "%n. list ! n" in arg_cong) 
-  apply arith
-  done
-
-lemmas nth_rev_alt = nth_rev [where xs = "rev ?ys", simplified]
-
 lemma nth_bin_to_bl_aux [rule_format] : 
   "ALL w n bl. n < m + length bl --> (bin_to_bl_aux m w bl) ! n = 
     (if n < m then bin_nth w (m - 1 - n) else bl ! (n - m))"
@@ -301,6 +302,8 @@
 lemma nth_bin_to_bl: "n < m ==> (bin_to_bl m w) ! n = bin_nth w (m - Suc n)"
   unfolding bin_to_bl_def by (simp add : nth_bin_to_bl_aux)
 
+subsection "Ordering with bool list operations"
+
 lemma bl_to_bin_lt2p_aux [rule_format] : 
   "ALL w. bl_to_bin_aux w bs < (w + 1) * (2 ^ length bs)"
   apply (induct "bs")
@@ -336,6 +339,8 @@
   apply simp
   done
 
+subsection "@{term butlast} with bool list operations"
+
 lemma butlast_rest_bin: 
   "butlast (bin_to_bl n w) = bin_to_bl (n - 1) (bin_rest w)"
   apply (unfold bin_to_bl_def)
@@ -360,6 +365,8 @@
    apply (auto simp add: butlast_rest_bl2bin_aux)
   done
 
+subsection "Truncation"
+
 lemma trunc_bl2bin_aux [rule_format] : 
   "ALL w. bintrunc m (bl_to_bin_aux w bl) = 
     bl_to_bin_aux (bintrunc (m - length bl) w) (drop (length bl - m) bl)"
@@ -397,6 +404,7 @@
    apply auto
   done
 
+(* TODO: This is not related to bool lists; should be moved *)
 lemma nth_rest_power_bin [rule_format] :
   "ALL n. bin_nth ((bin_rest ^ k) w) n = bin_nth w (n + k)"
   apply (induct k, clarsimp)
@@ -411,8 +419,7 @@
   apply (clarsimp simp add: nth_bin_to_bl nth_rest_power_bin)
   done
 
-lemma hd_butlast: "size xs > 1 ==> hd (butlast xs) = hd xs"
-  by (cases xs) auto
+subsection "@{term last} with bool list operations"
 
 lemma last_bin_last' [rule_format] : 
   "ALL w. size xs > 0 --> last xs = (bin_last (bl_to_bin_aux w xs) = bit.B1)" 
@@ -429,8 +436,14 @@
   apply (auto simp add: bin_to_bl_aux_alt)
   done
 
-(** links between bit-wise operations and operations on bool lists **)
-    
+subsection "Bit-wise operations on bool lists"
+
+consts
+  app2 :: "('a => 'b => 'c) => 'a list => 'b list => 'c list"
+
+defs
+  app2_def : "app2 f as bs == map (split f) (zip as bs)"
+
 lemma app2_Nil [simp]: "app2 f [] ys = []"
   unfolding app2_def by auto
 
@@ -500,6 +513,8 @@
 lemmas bl_xor_bin = bl_xor_aux_bin [where bs="[]" and cs="[]", 
                                     unfolded app2_Nil, folded bin_to_bl_def]
 
+subsection "@{term drop} with bool list operations"
+
 lemma drop_bin2bl_aux [rule_format] : 
   "ALL m bin bs. drop m (bin_to_bl_aux n bin bs) = 
     bin_to_bl_aux (n - m) bin (drop (m - n) bs)"
@@ -534,6 +549,8 @@
   apply simp
   done
 
+subsection "@{term bin_split} with bool list operations"
+
 lemma bin_split_take [rule_format] : 
   "ALL b c. bin_split n c = (a, b) --> 
     bin_to_bl m a = take m (bin_to_bl (m + n) c)"
@@ -549,6 +566,19 @@
     bin_to_bl m a = take m (bin_to_bl k c)"
   by (auto elim: bin_split_take)
   
+subsection "@{term takefill}"
+
+consts
+  takefill :: "'a => nat => 'a list => 'a list"
+
+-- "takefill - like take but if argument list too short,"
+-- "extends result to get requested length"
+primrec
+  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)"
+
 lemma nth_takefill [rule_format] : "ALL m l. m < n --> 
     takefill fill n l ! m = (if m < length l then l ! m else fill)"
   apply (induct n, clarsimp)
@@ -642,6 +672,8 @@
 lemmas takefill_pred_simps [simp] =
   takefill_minus_simps [where n="number_of bin", simplified nobm1, standard]
 
+subsection "@{term bin_cat} with bool list operations"
+
 (* links with function bl_to_bin *)
 
 lemma bl_to_bin_aux_cat: 
@@ -691,7 +723,15 @@
   apply simp
   done
 
-(* function bl_of_nth *)
+subsection "function @{term bl_of_nth}"
+
+consts
+  bl_of_nth :: "nat => (nat => bool) => bool list"
+
+primrec
+  Suc : "bl_of_nth (Suc n) f = f n # bl_of_nth n f"
+  Z : "bl_of_nth 0 f = []"
+
 lemma length_bl_of_nth [simp]: "length (bl_of_nth n f) = n"
   by (induct n)  auto
 
@@ -724,6 +764,33 @@
 
 lemmas bl_of_nth_nth [simp] = order_refl [THEN bl_of_nth_nth_le, simplified]
 
+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 *)
+  rbl_succ :: "bool list => bool list"
+  rbl_pred :: "bool list => bool list"
+  rbl_add :: "bool list => bool list => bool list"
+  rbl_mult :: "bool list => bool list => bool list"
+
+primrec 
+  Nil: "rbl_succ Nil = Nil"
+  Cons: "rbl_succ (x # xs) = (if x then False # rbl_succ xs else True # xs)"
+
+primrec 
+  Nil : "rbl_pred Nil = Nil"
+  Cons : "rbl_pred (x # xs) = (if x then False # xs else True # rbl_pred xs)"
+
+primrec (* result is length of first arg, second arg may be longer *)
+  Nil : "rbl_add Nil x = Nil"
+  Cons : "rbl_add (y # ys) x = (let ws = rbl_add ys (tl x) in 
+    (y ~= hd x) # (if hd x & y then rbl_succ ws else ws))"
+
+primrec (* result is length of first arg, second arg may be longer *)
+  Nil : "rbl_mult Nil x = Nil"
+  Cons : "rbl_mult (y # ys) x = (let ws = False # rbl_mult ys x in 
+    if y then rbl_add ws x else ws)"
+
 lemma size_rbl_pred: "length (rbl_pred bl) = length bl"
   by (induct bl) auto
 
@@ -880,6 +947,8 @@
     (y --> P (rbl_add ws xs)) & (~ y -->  P ws))"
   by (clarsimp simp add : Let_def)
   
+subsection "Miscellaneous lemmas"
+
 lemma and_len: "xs = ys ==> xs = ys & length xs = length ys"
   by auto
 
@@ -1015,8 +1084,6 @@
    in (w1, w2 BIT bin_last w))" 
   by (simp only: nobm1 bin_split_minus_simp)
 
-declare bin_split_pred_simp [simp]
-
 lemma bin_rsplit_aux_simp_alt:
   "bin_rsplit_aux (n, bs, m, c) =
    (if m = 0 \<or> n = 0 
diff -r 8df021f79e0b -r c1e20c65a3be src/HOL/Word/BinOperations.thy
--- a/src/HOL/Word/BinOperations.thy	Tue Aug 21 21:50:23 2007 +0200
+++ b/src/HOL/Word/BinOperations.thy	Wed Aug 22 01:42:35 2007 +0200
@@ -435,49 +435,6 @@
 lemmas bin_sc_Suc_pred [simp] = 
   bin_sc_Suc_minus [of "number_of bin", simplified nobm1, standard]
 
-subsection {* Operations on lists of booleans *}
-
-consts
-  bin_to_bl :: "nat => int => bool list"
-  bin_to_bl_aux :: "nat => int => bool list => bool list"
-  bl_to_bin :: "bool list => int"
-  bl_to_bin_aux :: "int => bool list => int"
-
-  bl_of_nth :: "nat => (nat => bool) => bool list"
-
-primrec
-  Nil : "bl_to_bin_aux w [] = w"
-  Cons : "bl_to_bin_aux w (b # bs) = 
-      bl_to_bin_aux (w BIT (if b then bit.B1 else bit.B0)) bs"
-
-primrec
-  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 = bit.B1) # bl)"
-
-defs
-  bin_to_bl_def : "bin_to_bl n w == bin_to_bl_aux n w []"
-  bl_to_bin_def : "bl_to_bin bs == bl_to_bin_aux Numeral.Pls bs"
-
-primrec
-  Suc : "bl_of_nth (Suc n) f = f n # bl_of_nth n f"
-  Z : "bl_of_nth 0 f = []"
-
-consts
-  takefill :: "'a => nat => 'a list => 'a list"
-  app2 :: "('a => 'b => 'c) => 'a list => 'b list => 'c list"
-
--- "takefill - like take but if argument list too short,"
--- "extends result to get requested length"
-primrec
-  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)"
-
-defs
-  app2_def : "app2 f as bs == map (split f) (zip as bs)"
-
 subsection {* Splitting and concatenation *}
 
 -- "rcat and rsplit"