# HG changeset patch
# User haftmann
# Date 1207309224 -7200
# Node ID 9e7f95903b245d4e335c1f299f8e1b54983362e4
# Parent  90b02960c8ce78d6d0a4caedf8c8f76a0f9e9caa
more new primrec

diff -r 90b02960c8ce -r 9e7f95903b24 src/HOL/Word/BinBoolList.thy
--- a/src/HOL/Word/BinBoolList.thy	Fri Apr 04 13:40:23 2008 +0200
+++ b/src/HOL/Word/BinBoolList.thy	Fri Apr 04 13:40:24 2008 +0200
@@ -9,33 +9,33 @@
 
 header "Bool lists and integers"
 
-theory BinBoolList imports BinOperations begin
+theory BinBoolList
+imports BinOperations
+begin
 
 subsection "Arithmetic in terms of bool lists"
 
-consts (* arithmetic operations in terms of the reversed bool list,
+(* 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 
+primrec rbl_succ :: "bool list => bool list" where
   Nil: "rbl_succ Nil = Nil"
-  Cons: "rbl_succ (x # xs) = (if x then False # rbl_succ xs else True # xs)"
+  | 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 rbl_pred :: "bool list => bool list" where
+  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 
+primrec rbl_add :: "bool list => bool list => bool list" where
+    (* 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 
+primrec rbl_mult :: "bool list => bool list => bool list" where
+    (* 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 tl_take: "tl (take n l) = take (n - 1) (tl l)"
@@ -102,16 +102,16 @@
 
 (** 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_aux_append: 
+  "bl_to_bin_aux (bs @ cs) w = bl_to_bin_aux cs (bl_to_bin_aux bs w)"
+  by (induct bs arbitrary: w) 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 bin_to_bl_aux_append: 
+  "bin_to_bl_aux n w bs @ cs = bin_to_bl_aux n w (bs @ cs)"
+  by (induct n arbitrary: w bs) auto
 
 lemma bl_to_bin_append: 
-  "bl_to_bin (bs @ cs) = bl_to_bin_aux (bl_to_bin bs) cs"
+  "bl_to_bin (bs @ cs) = bl_to_bin_aux cs (bl_to_bin bs)"
   unfolding bl_to_bin_def by (rule bl_to_bin_aux_append)
 
 lemma bin_to_bl_aux_alt: 
@@ -121,25 +121,25 @@
 lemma bin_to_bl_0: "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_aux: 
+  "size (bin_to_bl_aux n w bs) = n + length bs"
+  by (induct n arbitrary: w bs) auto
 
 lemma size_bin_to_bl: "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_aux n w bs) = 
+    bl_to_bin_aux bs (bintrunc n w)"
+  by (induct n arbitrary: w bs) (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) = 
+lemma bl_bin_bl':
+  "bin_to_bl (n + length bs) (bl_to_bin_aux bs w) = 
     bin_to_bl_aux n w bs"
-  apply (induct "bs")
+  apply (induct bs arbitrary: w n)
    apply auto
     apply (simp_all only : add_Suc [symmetric])
     apply (auto simp add : bin_to_bl_def)
@@ -175,9 +175,9 @@
 lemma bl_to_bin_Nil: "bl_to_bin [] = Int.Pls"
   unfolding bl_to_bin_def by auto
 
-lemma bin_to_bl_Pls_aux [rule_format] : 
-  "ALL bl. bin_to_bl_aux n Int.Pls bl = replicate n False @ bl"
-  by (induct n) (auto simp: replicate_app_Cons_same)
+lemma bin_to_bl_Pls_aux: 
+  "bin_to_bl_aux n Int.Pls bl = replicate n False @ bl"
+  by (induct n arbitrary: bl) (auto simp: replicate_app_Cons_same)
 
 lemma bin_to_bl_Pls: "bin_to_bl n Int.Pls = replicate n False"
   unfolding bin_to_bl_def by (simp add : bin_to_bl_Pls_aux)
@@ -223,26 +223,26 @@
 lemma bl_to_bin_rep_False: "bl_to_bin (replicate n False) = Int.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_aux: 
+  "length (bin_to_bl_aux n w bs) = n + length bs"
+  by (induct n arbitrary: w bs) 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
   
-lemma sign_bl_bin' [rule_format] : 
-  "ALL w. bin_sign (bl_to_bin_aux w bs) = bin_sign w"
-  by (induct bs) auto
+lemma sign_bl_bin': 
+  "bin_sign (bl_to_bin_aux bs w) = bin_sign w"
+  by (induct bs arbitrary: w) auto
   
 lemma sign_bl_bin: "bin_sign (bl_to_bin bs) = Int.Pls"
   unfolding bl_to_bin_def by (simp add : sign_bl_bin')
   
-lemma bl_sbin_sign_aux [rule_format] : 
-  "ALL w bs. hd (bin_to_bl_aux (Suc n) w bs) = 
+lemma bl_sbin_sign_aux: 
+  "hd (bin_to_bl_aux (Suc n) w bs) = 
     (bin_sign (sbintrunc n w) = Int.Min)"
-  apply (induct "n")
+  apply (induct n arbitrary: w bs)
    apply clarsimp
-   apply (case_tac w rule: bin_exhaust)
+   apply (cases w rule: bin_exhaust)
    apply (simp split add : bit.split)
   apply clarsimp
   done
@@ -251,15 +251,15 @@
   "hd (bin_to_bl (Suc n) w) = (bin_sign (sbintrunc n w) = Int.Min)"
   unfolding bin_to_bl_def by (rule bl_sbin_sign_aux)
 
-lemma bin_nth_of_bl_aux [rule_format] : 
-  "ALL w. bin_nth (bl_to_bin_aux w bl) n = 
+lemma bin_nth_of_bl_aux [rule_format]: 
+  "\<forall>w. bin_nth (bl_to_bin_aux bl w) n = 
     (n < size bl & rev bl ! n | n >= length bl & bin_nth w (n - size bl))"
   apply (induct_tac bl)
    apply clarsimp
   apply clarsimp
   apply (cut_tac x=n and y="size list" in linorder_less_linear)
   apply (erule disjE, simp add: nth_append)+
-  apply (simp add: nth_append)
+  apply auto
   done
 
 lemma bin_nth_of_bl: "bin_nth (bl_to_bin bl) n = (n < length bl & rev bl ! n)";
@@ -307,14 +307,14 @@
 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)
 
-lemma bl_to_bin_lt2p_aux [rule_format] : 
-  "ALL w. bl_to_bin_aux w bs < (w + 1) * (2 ^ length bs)"
-  apply (induct "bs")
+lemma bl_to_bin_lt2p_aux [rule_format]: 
+  "\<forall>w. bl_to_bin_aux bs w < (w + 1) * (2 ^ length bs)"
+  apply (induct bs)
    apply clarsimp
   apply clarsimp
   apply safe
-   apply (erule allE, erule xtr8 [rotated],
-          simp add: numeral_simps ring_simps cong add : number_of_False_cong)+
+  apply (erule allE, erule xtr8 [rotated],
+         simp add: numeral_simps ring_simps cong add : number_of_False_cong)+
   done
 
 lemma bl_to_bin_lt2p: "bl_to_bin bs < (2 ^ length bs)"
@@ -326,7 +326,7 @@
   done
 
 lemma bl_to_bin_ge2p_aux [rule_format] : 
-  "ALL w. bl_to_bin_aux w bs >= w * (2 ^ length bs)"
+  "\<forall>w. bl_to_bin_aux bs w >= w * (2 ^ length bs)"
   apply (induct bs)
    apply clarsimp
   apply clarsimp
@@ -354,10 +354,10 @@
 lemmas butlast_bin_rest = butlast_rest_bin
   [where w="bl_to_bin bl" and n="length bl", simplified, standard]
 
-lemma butlast_rest_bl2bin_aux [rule_format] :
-  "ALL w. bl ~= [] --> 
-    bl_to_bin_aux w (butlast bl) = bin_rest (bl_to_bin_aux w bl)"
-  by (induct bl) auto
+lemma butlast_rest_bl2bin_aux:
+  "bl ~= [] \<Longrightarrow>
+    bl_to_bin_aux (butlast bl) w = bin_rest (bl_to_bin_aux bl w)"
+  by (induct bl arbitrary: w) auto
   
 lemma butlast_rest_bl2bin: 
   "bl_to_bin (butlast bl) = bin_rest (bl_to_bin bl)"
@@ -366,9 +366,9 @@
    apply (auto simp add: butlast_rest_bl2bin_aux)
   done
 
-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)"
+lemma trunc_bl2bin_aux [rule_format]: 
+  "ALL w. bintrunc m (bl_to_bin_aux bl w) = 
+    bl_to_bin_aux (drop (length bl - m) bl) (bintrunc (m - length bl) w)"
   apply (induct_tac bl)
    apply clarsimp
   apply clarsimp
@@ -376,13 +376,13 @@
    apply (case_tac "m - size list")
     apply (simp add : diff_is_0_eq [THEN iffD1, THEN Suc_diff_le])
    apply simp
-   apply (rule_tac f = "%nat. bl_to_bin_aux (Int.Bit1 (bintrunc nat w)) list" 
+   apply (rule_tac f = "%nat. bl_to_bin_aux list (Int.Bit1 (bintrunc nat w))" 
                    in arg_cong) 
    apply simp
   apply (case_tac "m - size list")
    apply (simp add: diff_is_0_eq [THEN iffD1, THEN Suc_diff_le])
   apply simp
-  apply (rule_tac f = "%nat. bl_to_bin_aux (Int.Bit0 (bintrunc nat w)) list" 
+  apply (rule_tac f = "%nat. bl_to_bin_aux list (Int.Bit0 (bintrunc nat w))" 
                   in arg_cong) 
   apply simp
   done
@@ -420,9 +420,9 @@
 lemma hd_butlast: "size xs > 1 ==> hd (butlast xs) = hd xs"
   by (cases xs) auto
 
-lemma last_bin_last' [rule_format] : 
-  "ALL w. size xs > 0 --> last xs = (bin_last (bl_to_bin_aux w xs) = bit.B1)" 
-  by (induct xs) auto
+lemma last_bin_last': 
+  "size xs > 0 \<Longrightarrow> last xs = (bin_last (bl_to_bin_aux xs w) = bit.B1)" 
+  by (induct xs arbitrary: w) auto
 
 lemma last_bin_last: 
   "size xs > 0 ==> last xs = (bin_last (bl_to_bin xs) = bit.B1)" 
@@ -437,16 +437,16 @@
 
 (** links between bit-wise operations and operations on bool lists **)
     
-lemma app2_Nil [simp]: "app2 f [] ys = []"
-  unfolding app2_def by auto
+lemma map2_Nil [simp]: "map2 f [] ys = []"
+  unfolding map2_def by auto
 
-lemma app2_Cons [simp]:
-  "app2 f (x # xs) (y # ys) = f x y # app2 f xs ys"
-  unfolding app2_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. 
-    app2 (%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) (app2 (%x y. x ~= y) 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)"
   apply (induct_tac n)
    apply safe
    apply simp
@@ -458,8 +458,8 @@
   done
     
 lemma bl_or_aux_bin [rule_format] : "ALL v w bs cs. 
-    app2 (op | ) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) = 
-    bin_to_bl_aux n (v OR w) (app2 (op | ) bs cs)" 
+    map2 (op | ) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) = 
+    bin_to_bl_aux n (v OR w) (map2 (op | ) bs cs)" 
   apply (induct_tac n)
    apply safe
    apply simp
@@ -471,8 +471,8 @@
   done
     
 lemma bl_and_aux_bin [rule_format] : "ALL v w bs cs. 
-    app2 (op & ) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) = 
-    bin_to_bl_aux n (v AND w) (app2 (op & ) bs cs)" 
+    map2 (op & ) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) = 
+    bin_to_bl_aux n (v AND w) (map2 (op & ) bs cs)" 
   apply (induct_tac n)
    apply safe
    apply simp
@@ -498,13 +498,13 @@
   [where cs = "[]", unfolded bin_to_bl_def [symmetric] map.simps]
 
 lemmas bl_and_bin = bl_and_aux_bin [where bs="[]" and cs="[]", 
-                                    unfolded app2_Nil, folded bin_to_bl_def]
+                                    unfolded map2_Nil, folded bin_to_bl_def]
 
 lemmas bl_or_bin = bl_or_aux_bin [where bs="[]" and cs="[]", 
-                                  unfolded app2_Nil, folded bin_to_bl_def]
+                                  unfolded map2_Nil, folded bin_to_bl_def]
 
 lemmas bl_xor_bin = bl_xor_aux_bin [where bs="[]" and cs="[]", 
-                                    unfolded app2_Nil, folded bin_to_bl_def]
+                                    unfolded map2_Nil, folded bin_to_bl_def]
 
 lemma drop_bin2bl_aux [rule_format] : 
   "ALL m bin bs. drop m (bin_to_bl_aux n bin bs) = 
@@ -651,8 +651,8 @@
 (* links with function bl_to_bin *)
 
 lemma bl_to_bin_aux_cat: 
-  "!!nv v. bl_to_bin_aux (bin_cat w nv v) bs = 
-    bin_cat w (nv + length bs) (bl_to_bin_aux v bs)"
+  "!!nv v. bl_to_bin_aux bs (bin_cat w nv v) = 
+    bin_cat w (nv + length bs) (bl_to_bin_aux bs v)"
   apply (induct bs)
    apply simp
   apply (simp add: bin_cat_Suc_Bit [symmetric] del: bin_cat.simps)
@@ -985,19 +985,21 @@
   rsplit_aux_simp1s [OF disjI1] rsplit_aux_simp1s [OF disjI2]
 
 lemma bin_rsplit_aux_append:
-  "bin_rsplit_aux (n, bs @ cs, m, c) = bin_rsplit_aux (n, bs, m, c) @ cs"
-  apply (rule_tac u=n and v=bs and w=m and x=c in bin_rsplit_aux.induct)
+  "bin_rsplit_aux n m c (bs @ cs) = bin_rsplit_aux n m c bs @ cs"
+  apply (induct n m c bs rule: bin_rsplit_aux.induct)
   apply (subst bin_rsplit_aux.simps)
   apply (subst bin_rsplit_aux.simps)
   apply (clarsimp split: ls_splits)
+  apply auto
   done
 
 lemma bin_rsplitl_aux_append:
-  "bin_rsplitl_aux (n, bs @ cs, m, c) = bin_rsplitl_aux (n, bs, m, c) @ cs"
-  apply (rule_tac u=n and v=bs and w=m and x=c in bin_rsplitl_aux.induct)
+  "bin_rsplitl_aux n m c (bs @ cs) = bin_rsplitl_aux n m c bs @ cs"
+  apply (induct n m c bs rule: bin_rsplitl_aux.induct)
   apply (subst bin_rsplitl_aux.simps)
   apply (subst bin_rsplitl_aux.simps)
   apply (clarsimp split: ls_splits)
+  apply auto
   done
 
 lemmas rsplit_aux_apps [where bs = "[]"] =
@@ -1024,17 +1026,18 @@
 declare bin_split_pred_simp [simp]
 
 lemma bin_rsplit_aux_simp_alt:
-  "bin_rsplit_aux (n, bs, m, c) =
+  "bin_rsplit_aux n m c bs =
    (if m = 0 \<or> n = 0 
    then bs
    else let (a, b) = bin_split n c in bin_rsplit n (m - n, a) @ b # bs)"
-  apply (rule trans)
-   apply (subst bin_rsplit_aux.simps, rule refl)
-  apply (simp add: rsplit_aux_alts)
+  unfolding bin_rsplit_aux.simps [of n m c bs]
+  apply simp
+  apply (subst rsplit_aux_alts)
+  apply (simp add: bin_rsplit_def)
   done
 
 lemmas bin_rsplit_simp_alt = 
-  trans [OF bin_rsplit_def [THEN meta_eq_to_obj_eq]
+  trans [OF bin_rsplit_def
             bin_rsplit_aux_simp_alt, standard]
 
 lemmas bthrs = bin_rsplit_simp_alt [THEN [2] trans]
@@ -1089,27 +1092,33 @@
   apply (rule allI)
   apply (subst bin_rsplitl_aux.simps)
   apply (subst bin_rsplit_aux.simps)
-  apply (clarsimp simp: rsplit_aux_alts Let_def split: ls_splits)
+  apply (clarsimp simp: Let_def split: ls_splits)
   apply (drule bin_split_trunc)
   apply (drule sym [THEN trans], assumption)
-  apply fast
+  apply (subst rsplit_aux_alts(1))
+  apply (subst rsplit_aux_alts(2))
+  apply clarsimp
+  unfolding bin_rsplit_def bin_rsplitl_def
+  apply simp
   done
-    
+
 lemma bin_rsplit_rcat [rule_format] :
   "n > 0 --> bin_rsplit n (n * size ws, bin_rcat n ws) = map (bintrunc n) ws"
   apply (unfold bin_rsplit_def bin_rcat_def)
   apply (rule_tac xs = "ws" in rev_induct)
    apply clarsimp
   apply clarsimp
-  apply (clarsimp simp add: bin_split_cat rsplit_aux_alts)
+  apply (subst rsplit_aux_alts)
+  unfolding bin_split_cat
+  apply simp
   done
 
 lemma bin_rsplit_aux_len_le [rule_format] :
-  "ALL ws m. n \<noteq> 0 --> ws = bin_rsplit_aux (n, bs, nw, w) --> 
-    (length ws <= m) = (nw + length bs * n <= m * n)"
-  apply (rule_tac u=n and v=bs and w=nw and x=w in bin_rsplit_aux.induct)
+  "\<forall>ws m. n \<noteq> 0 \<longrightarrow> ws = bin_rsplit_aux n nw w bs \<longrightarrow>
+    length ws \<le> m \<longleftrightarrow> nw + length bs * n \<le> m * n"
+  apply (induct n nw w bs rule: bin_rsplit_aux.induct)
   apply (subst bin_rsplit_aux.simps)
-  apply (simp add:lrlem Let_def split: ls_splits )
+  apply (simp add: lrlem Let_def split: ls_splits)
   done
 
 lemma bin_rsplit_len_le: 
@@ -1117,9 +1126,9 @@
   unfolding bin_rsplit_def by (clarsimp simp add : bin_rsplit_aux_len_le)
  
 lemma bin_rsplit_aux_len [rule_format] :
-  "n\<noteq>0 --> length (bin_rsplit_aux (n, cs, nw, w)) = 
+  "n\<noteq>0 --> length (bin_rsplit_aux n nw w cs) = 
     (nw + n - 1) div n + length cs"
-  apply (rule_tac u=n and v=cs and w=nw and x=w in bin_rsplit_aux.induct)
+  apply (induct n nw w cs rule: bin_rsplit_aux.induct)
   apply (subst bin_rsplit_aux.simps)
   apply (clarsimp simp: Let_def split: ls_splits)
   apply (erule thin_rl)
@@ -1134,27 +1143,30 @@
   "n\<noteq>0 ==> length (bin_rsplit n (nw, w)) = (nw + n - 1) div n"
   unfolding bin_rsplit_def by (clarsimp simp add : bin_rsplit_aux_len)
 
-lemma bin_rsplit_aux_len_indep [rule_format] :
-  "n\<noteq>0 ==> (ALL v bs. length bs = length cs --> 
-    length (bin_rsplit_aux (n, bs, nw, v)) = 
-    length (bin_rsplit_aux (n, cs, nw, w)))"
-  apply (rule_tac u=n and v=cs and w=nw and x=w in bin_rsplit_aux.induct)
-  apply clarsimp
-  apply (simp (no_asm_simp) add: bin_rsplit_aux_simp_alt Let_def 
-                            split: ls_splits)
-  apply clarify 
-  apply (erule allE)+
-  apply (erule impE)
-   apply (fast elim!: sym)
-  apply (simp (no_asm_use) add: rsplit_aux_alts)
-  apply (erule impE)
-  apply (rule_tac x="ba # bs" in exI)
-  apply auto
-  done
+lemma bin_rsplit_aux_len_indep:
+  "n \<noteq> 0 \<Longrightarrow> length bs = length cs \<Longrightarrow>
+    length (bin_rsplit_aux n nw v bs) =
+    length (bin_rsplit_aux n nw w cs)"
+proof (induct n nw w cs arbitrary: v bs rule: bin_rsplit_aux.induct)
+  case (1 n m w cs v bs) show ?case
+  proof (cases "m = 0")
+    case True then show ?thesis by simp
+  next
+    case False
+    from "1.hyps" `m \<noteq> 0` `n \<noteq> 0` have hyp: "\<And>v bs. length bs = Suc (length cs) \<Longrightarrow>
+      length (bin_rsplit_aux n (m - n) v bs) =
+      length (bin_rsplit_aux n (m - n) (fst (bin_split n w)) (snd (bin_split n w) # cs))"
+    by auto
+    show ?thesis using `length bs = length cs` `n \<noteq> 0`
+      by (auto simp add: bin_rsplit_aux_simp_alt Let_def bin_rsplit_len
+        split: ls_splits)
+  qed
+qed
 
 lemma bin_rsplit_len_indep: 
   "n\<noteq>0 ==> length (bin_rsplit n (nw, v)) = length (bin_rsplit n (nw, w))"
   apply (unfold bin_rsplit_def)
+  apply (simp (no_asm))
   apply (erule bin_rsplit_aux_len_indep)
   apply (rule refl)
   done
diff -r 90b02960c8ce -r 9e7f95903b24 src/HOL/Word/BinGeneral.thy
--- a/src/HOL/Word/BinGeneral.thy	Fri Apr 04 13:40:23 2008 +0200
+++ b/src/HOL/Word/BinGeneral.thy	Fri Apr 04 13:40:24 2008 +0200
@@ -9,98 +9,201 @@
 
 header {* Basic Definitions for Binary Integers *}
 
-theory BinGeneral imports Num_Lemmas
-
+theory BinGeneral
+imports Num_Lemmas
 begin
 
-subsection {* Recursion combinator for binary integers *}
+subsection {* Further properties of numerals *}
+
+datatype bit = B0 | B1
+
+definition
+  Bit :: "int \<Rightarrow> bit \<Rightarrow> int" (infixl "BIT" 90) where
+  "k BIT b = (case b of B0 \<Rightarrow> 0 | B1 \<Rightarrow> 1) + k + k"
+
+lemma BIT_B0_eq_Bit0 [simp]: "w BIT B0 = Int.Bit0 w"
+  unfolding Bit_def Bit0_def by simp
+
+lemma BIT_B1_eq_Bit1 [simp]: "w BIT B1 = Int.Bit1 w"
+  unfolding Bit_def Bit1_def by simp
+
+lemmas BIT_simps = BIT_B0_eq_Bit0 BIT_B1_eq_Bit1
 
-lemma brlem: "(bin = Int.Min) = (- bin + Int.pred 0 = 0)"
-  unfolding Min_def pred_def by arith
+hide (open) const B0 B1
+
+lemma Min_ne_Pls [iff]:  
+  "Int.Min ~= Int.Pls"
+  unfolding Min_def Pls_def by auto
+
+lemmas Pls_ne_Min [iff] = Min_ne_Pls [symmetric]
+
+lemmas PlsMin_defs [intro!] = 
+  Pls_def Min_def Pls_def [symmetric] Min_def [symmetric]
+
+lemmas PlsMin_simps [simp] = PlsMin_defs [THEN Eq_TrueI]
+
+lemma number_of_False_cong: 
+  "False \<Longrightarrow> number_of x = number_of y"
+  by (rule FalseE)
+
+(** ways in which type Bin resembles a datatype **)
 
-function
-  bin_rec :: "'a \<Rightarrow> 'a \<Rightarrow> (int \<Rightarrow> bit \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> int \<Rightarrow> 'a"  
-where 
-  "bin_rec f1 f2 f3 bin = (if bin = Int.Pls then f1 
-    else if bin = Int.Min then f2
-    else case bin_rl bin of (w, b) => f3 w b (bin_rec f1 f2 f3 w))"
-  by pat_completeness auto
+lemma BIT_eq: "u BIT b = v BIT c ==> u = v & b = c"
+  apply (unfold Bit_def)
+  apply (simp (no_asm_use) split: bit.split_asm)
+     apply simp_all
+   apply (drule_tac f=even in arg_cong, clarsimp)+
+  done
+     
+lemmas BIT_eqE [elim!] = BIT_eq [THEN conjE, standard]
+
+lemma BIT_eq_iff [simp]: 
+  "(u BIT b = v BIT c) = (u = v \<and> b = c)"
+  by (rule iffI) auto
+
+lemmas BIT_eqI [intro!] = conjI [THEN BIT_eq_iff [THEN iffD2]]
+
+lemma less_Bits: 
+  "(v BIT b < w BIT c) = (v < w | v <= w & b = bit.B0 & c = bit.B1)"
+  unfolding Bit_def by (auto split: bit.split)
 
-termination 
-  apply (relation "measure (nat o abs o snd o snd o snd)")
-   apply simp
-  apply (simp add: Pls_def brlem)
-  apply (clarsimp simp: bin_rl_char pred_def)
-  apply (frule thin_rl [THEN refl [THEN bin_abs_lem [rule_format]]]) 
-    apply (unfold Pls_def Min_def number_of_eq)
-    prefer 2
-    apply (erule asm_rl)
-   apply auto
+lemma le_Bits: 
+  "(v BIT b <= w BIT c) = (v < w | v <= w & (b ~= bit.B1 | c ~= bit.B0))" 
+  unfolding Bit_def by (auto split: bit.split)
+
+lemma no_no [simp]: "number_of (number_of i) = i"
+  unfolding number_of_eq by simp
+
+lemma Bit_B0:
+  "k BIT bit.B0 = k + k"
+   by (unfold Bit_def) simp
+
+lemma Bit_B1:
+  "k BIT bit.B1 = k + k + 1"
+   by (unfold Bit_def) simp
+  
+lemma Bit_B0_2t: "k BIT bit.B0 = 2 * k"
+  by (rule trans, rule Bit_B0) simp
+
+lemma Bit_B1_2t: "k BIT bit.B1 = 2 * k + 1"
+  by (rule trans, rule Bit_B1) simp
+
+lemma B_mod_2': 
+  "X = 2 ==> (w BIT bit.B1) mod X = 1 & (w BIT bit.B0) mod X = 0"
+  apply (simp (no_asm) only: Bit_B0 Bit_B1)
+  apply (simp add: z1pmod2)
   done
 
-declare bin_rec.simps [simp del]
+lemma B1_mod_2 [simp]: "(Int.Bit1 w) mod 2 = 1"
+  unfolding numeral_simps number_of_is_id by (simp add: z1pmod2)
 
-lemma bin_rec_PM:
-  "f = bin_rec f1 f2 f3 ==> f Int.Pls = f1 & f Int.Min = f2"
-  by (auto simp add: bin_rec.simps)
-
-lemma bin_rec_Pls: "bin_rec f1 f2 f3 Int.Pls = f1"
-  by (simp add: bin_rec.simps)
+lemma B0_mod_2 [simp]: "(Int.Bit0 w) mod 2 = 0"
+  unfolding numeral_simps number_of_is_id by simp
 
-lemma bin_rec_Min: "bin_rec f1 f2 f3 Int.Min = f2"
-  by (simp add: bin_rec.simps)
+lemma neB1E [elim!]:
+  assumes ne: "y \<noteq> bit.B1"
+  assumes y: "y = bit.B0 \<Longrightarrow> P"
+  shows "P"
+  apply (rule y)
+  apply (cases y rule: bit.exhaust, simp)
+  apply (simp add: ne)
+  done
 
-lemma bin_rec_Bit0:
-  "f3 Int.Pls bit.B0 f1 = f1 \<Longrightarrow>
-    bin_rec f1 f2 f3 (Int.Bit0 w) = f3 w bit.B0 (bin_rec f1 f2 f3 w)"
-  apply (simp add: bin_rec_Pls bin_rec.simps [of _ _ _ "Int.Bit0 w"])
-  unfolding Pls_def Min_def Bit0_def
-  apply auto
-  apply presburger
-  apply (simp add: bin_rec.simps)
+lemma bin_ex_rl: "EX w b. w BIT b = bin"
+  apply (unfold Bit_def)
+  apply (cases "even bin")
+   apply (clarsimp simp: even_equiv_def)
+   apply (auto simp: odd_equiv_def split: bit.split)
   done
 
-lemma bin_rec_Bit1:
-  "f3 Int.Min bit.B1 f2 = f2 \<Longrightarrow>
-    bin_rec f1 f2 f3 (Int.Bit1 w) = f3 w bit.B1 (bin_rec f1 f2 f3 w)"
-  apply (simp add: bin_rec.simps [of _ _ _ "Int.Bit1 w"])
-  unfolding Pls_def Min_def Bit1_def
-  apply auto
-  apply (cases w)
-  apply auto
-  apply (simp add: bin_rec.simps)
-    unfolding Min_def Pls_def number_of_is_id apply auto
-  unfolding Bit0_def apply presburger
+lemma bin_exhaust:
+  assumes Q: "\<And>x b. bin = x BIT b \<Longrightarrow> Q"
+  shows "Q"
+  apply (insert bin_ex_rl [of bin])  
+  apply (erule exE)+
+  apply (rule Q)
+  apply force
   done
-  
-lemma bin_rec_Bit:
-  "f = bin_rec f1 f2 f3  ==> f3 Int.Pls bit.B0 f1 = f1 ==> 
-    f3 Int.Min bit.B1 f2 = f2 ==> f (w BIT b) = f3 w b (f w)"
-  by (cases b, simp add: bin_rec_Bit0, simp add: bin_rec_Bit1)
 
-lemmas bin_rec_simps = refl [THEN bin_rec_Bit] bin_rec_Pls bin_rec_Min
-  bin_rec_Bit0 bin_rec_Bit1
 
 subsection {* Destructors for binary integers *}
 
+definition bin_rl :: "int \<Rightarrow> int \<times> bit" where 
+  [code func del]: "bin_rl w = (THE (r, l). w = r BIT l)"
+
+lemma bin_rl_char: "(bin_rl w = (r, l)) = (r BIT l = w)"
+  apply (unfold bin_rl_def)
+  apply safe
+   apply (cases w rule: bin_exhaust)
+   apply auto
+  done
+
 definition
   bin_rest_def [code func del]: "bin_rest w = fst (bin_rl w)"
 
 definition
   bin_last_def [code func del] : "bin_last w = snd (bin_rl w)"
 
-definition
-  bin_sign_def [code func del] : "bin_sign = bin_rec Int.Pls Int.Min (%w b s. s)"
-
 primrec bin_nth where
-  "bin_nth.Z" : "bin_nth w 0 = (bin_last w = bit.B1)"
-  | "bin_nth.Suc" : "bin_nth w (Suc n) = bin_nth (bin_rest w) n"
+  Z: "bin_nth w 0 = (bin_last w = bit.B1)"
+  | Suc: "bin_nth w (Suc n) = bin_nth (bin_rest w) n"
 
 lemma bin_rl: "bin_rl w = (bin_rest w, bin_last w)"
   unfolding bin_rest_def bin_last_def by auto
 
+lemma bin_rl_simps [simp]:
+  "bin_rl Int.Pls = (Int.Pls, bit.B0)"
+  "bin_rl Int.Min = (Int.Min, bit.B1)"
+  "bin_rl (Int.Bit0 r) = (r, bit.B0)"
+  "bin_rl (Int.Bit1 r) = (r, bit.B1)"
+  "bin_rl (r BIT b) = (r, b)"
+  unfolding bin_rl_char by simp_all
+
+declare bin_rl_simps(1-4) [code func]
+
 lemmas bin_rl_simp [simp] = iffD1 [OF bin_rl_char bin_rl]
 
+lemma bin_abs_lem:
+  "bin = (w BIT b) ==> ~ bin = Int.Min --> ~ bin = Int.Pls -->
+    nat (abs w) < nat (abs bin)"
+  apply (clarsimp simp add: bin_rl_char)
+  apply (unfold Pls_def Min_def Bit_def)
+  apply (cases b)
+   apply (clarsimp, arith)
+  apply (clarsimp, arith)
+  done
+
+lemma bin_induct:
+  assumes PPls: "P Int.Pls"
+    and PMin: "P Int.Min"
+    and PBit: "!!bin bit. P bin ==> P (bin BIT bit)"
+  shows "P bin"
+  apply (rule_tac P=P and a=bin and f1="nat o abs" 
+                  in wf_measure [THEN wf_induct])
+  apply (simp add: measure_def inv_image_def)
+  apply (case_tac x rule: bin_exhaust)
+  apply (frule bin_abs_lem)
+  apply (auto simp add : PPls PMin PBit)
+  done
+
+lemma numeral_induct:
+  assumes Pls: "P Int.Pls"
+  assumes Min: "P Int.Min"
+  assumes Bit0: "\<And>w. \<lbrakk>P w; w \<noteq> Int.Pls\<rbrakk> \<Longrightarrow> P (Int.Bit0 w)"
+  assumes Bit1: "\<And>w. \<lbrakk>P w; w \<noteq> Int.Min\<rbrakk> \<Longrightarrow> P (Int.Bit1 w)"
+  shows "P x"
+  apply (induct x rule: bin_induct)
+    apply (rule Pls)
+   apply (rule Min)
+  apply (case_tac bit)
+   apply (case_tac "bin = Int.Pls")
+    apply simp
+   apply (simp add: Bit0)
+  apply (case_tac "bin = Int.Min")
+   apply simp
+  apply (simp add: Bit1)
+  done
+
 lemma bin_rest_simps [simp]: 
   "bin_rest Int.Pls = Int.Pls"
   "bin_rest Int.Min = Int.Min"
@@ -121,16 +224,6 @@
 
 declare bin_last_simps(1-4) [code func]
 
-lemma bin_sign_simps [simp]:
-  "bin_sign Int.Pls = Int.Pls"
-  "bin_sign Int.Min = Int.Min"
-  "bin_sign (Int.Bit0 w) = bin_sign w"
-  "bin_sign (Int.Bit1 w) = bin_sign w"
-  "bin_sign (w BIT b) = bin_sign w"
-  unfolding bin_sign_def by (auto simp: bin_rec_simps)
-
-declare bin_sign_simps(1-4) [code func]
-
 lemma bin_r_l_extras [simp]:
   "bin_last 0 = bit.B0"
   "bin_last (- 1) = bit.B1"
@@ -237,11 +330,94 @@
   bin_nth_0 bin_nth_Suc bin_nth_Pls bin_nth_Min bin_nth_minus
   bin_nth_minus_Bit0 bin_nth_minus_Bit1
 
+
+subsection {* Recursion combinator for binary integers *}
+
+lemma brlem: "(bin = Int.Min) = (- bin + Int.pred 0 = 0)"
+  unfolding Min_def pred_def by arith
+
+function
+  bin_rec :: "'a \<Rightarrow> 'a \<Rightarrow> (int \<Rightarrow> bit \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> int \<Rightarrow> 'a"  
+where 
+  "bin_rec f1 f2 f3 bin = (if bin = Int.Pls then f1 
+    else if bin = Int.Min then f2
+    else case bin_rl bin of (w, b) => f3 w b (bin_rec f1 f2 f3 w))"
+  by pat_completeness auto
+
+termination 
+  apply (relation "measure (nat o abs o snd o snd o snd)")
+   apply simp
+  apply (simp add: Pls_def brlem)
+  apply (clarsimp simp: bin_rl_char pred_def)
+  apply (frule thin_rl [THEN refl [THEN bin_abs_lem [rule_format]]]) 
+    apply (unfold Pls_def Min_def number_of_eq)
+    prefer 2
+    apply (erule asm_rl)
+   apply auto
+  done
+
+declare bin_rec.simps [simp del]
+
+lemma bin_rec_PM:
+  "f = bin_rec f1 f2 f3 ==> f Int.Pls = f1 & f Int.Min = f2"
+  by (auto simp add: bin_rec.simps)
+
+lemma bin_rec_Pls: "bin_rec f1 f2 f3 Int.Pls = f1"
+  by (simp add: bin_rec.simps)
+
+lemma bin_rec_Min: "bin_rec f1 f2 f3 Int.Min = f2"
+  by (simp add: bin_rec.simps)
+
+lemma bin_rec_Bit0:
+  "f3 Int.Pls bit.B0 f1 = f1 \<Longrightarrow>
+    bin_rec f1 f2 f3 (Int.Bit0 w) = f3 w bit.B0 (bin_rec f1 f2 f3 w)"
+  apply (simp add: bin_rec_Pls bin_rec.simps [of _ _ _ "Int.Bit0 w"])
+  unfolding Pls_def Min_def Bit0_def
+  apply auto
+  apply presburger
+  apply (simp add: bin_rec.simps)
+  done
+
+lemma bin_rec_Bit1:
+  "f3 Int.Min bit.B1 f2 = f2 \<Longrightarrow>
+    bin_rec f1 f2 f3 (Int.Bit1 w) = f3 w bit.B1 (bin_rec f1 f2 f3 w)"
+  apply (simp add: bin_rec.simps [of _ _ _ "Int.Bit1 w"])
+  unfolding Pls_def Min_def Bit1_def
+  apply auto
+  apply (cases w)
+  apply auto
+  apply (simp add: bin_rec.simps)
+    unfolding Min_def Pls_def number_of_is_id apply auto
+  unfolding Bit0_def apply presburger
+  done
+  
+lemma bin_rec_Bit:
+  "f = bin_rec f1 f2 f3  ==> f3 Int.Pls bit.B0 f1 = f1 ==> 
+    f3 Int.Min bit.B1 f2 = f2 ==> f (w BIT b) = f3 w b (f w)"
+  by (cases b, simp add: bin_rec_Bit0, simp add: bin_rec_Bit1)
+
+lemmas bin_rec_simps = refl [THEN bin_rec_Bit] bin_rec_Pls bin_rec_Min
+  bin_rec_Bit0 bin_rec_Bit1
+
+
+subsection {* Truncating binary integers *}
+
+definition
+  bin_sign_def [code func del] : "bin_sign = bin_rec Int.Pls Int.Min (%w b s. s)"
+
+lemma bin_sign_simps [simp]:
+  "bin_sign Int.Pls = Int.Pls"
+  "bin_sign Int.Min = Int.Min"
+  "bin_sign (Int.Bit0 w) = bin_sign w"
+  "bin_sign (Int.Bit1 w) = bin_sign w"
+  "bin_sign (w BIT b) = bin_sign w"
+  unfolding bin_sign_def by (auto simp: bin_rec_simps)
+
+declare bin_sign_simps(1-4) [code func]
+
 lemma bin_sign_rest [simp]: 
   "bin_sign (bin_rest w) = (bin_sign w)"
-  by (case_tac w rule: bin_exhaust) auto
-
-subsection {* Truncating binary integers *}
+  by (cases w rule: bin_exhaust) auto
 
 consts
   bintrunc :: "nat => int => int"
@@ -718,18 +894,14 @@
 
 subsection {* Splitting and concatenation *}
 
-consts
-  bin_split :: "nat => int => int * int"
-primrec
-  Z : "bin_split 0 w = (w, Int.Pls)"
-  Suc : "bin_split (Suc n) w = (let (w1, w2) = bin_split n (bin_rest w)
-    in (w1, w2 BIT bin_last w))"
+primrec bin_split :: "nat \<Rightarrow> int \<Rightarrow> int \<times> int" where
+  Z: "bin_split 0 w = (w, Int.Pls)"
+  | Suc: "bin_split (Suc n) w = (let (w1, w2) = bin_split n (bin_rest w)
+        in (w1, w2 BIT bin_last w))"
 
-consts
-  bin_cat :: "int => nat => int => int"
-primrec
-  Z : "bin_cat w 0 v = w"
-  Suc : "bin_cat w (Suc n) v = bin_cat w n (bin_rest v) BIT bin_last v"
+primrec bin_cat :: "int \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int" where
+  Z: "bin_cat w 0 v = w"
+  | Suc: "bin_cat w (Suc n) v = bin_cat w n (bin_rest v) BIT bin_last v"
 
 subsection {* Miscellaneous lemmas *}