author haftmann Fri Apr 04 13:40:24 2008 +0200 (2008-04-04) changeset 26557 9e7f95903b24 parent 26556 90b02960c8ce child 26558 7fcc10088e72
more new primrec
 src/HOL/Word/BinBoolList.thy file | annotate | diff | revisions src/HOL/Word/BinGeneral.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Word/BinBoolList.thy	Fri Apr 04 13:40:23 2008 +0200
1.2 +++ b/src/HOL/Word/BinBoolList.thy	Fri Apr 04 13:40:24 2008 +0200
1.3 @@ -9,33 +9,33 @@
1.4
1.5  header "Bool lists and integers"
1.6
1.7 -theory BinBoolList imports BinOperations begin
1.8 +theory BinBoolList
1.9 +imports BinOperations
1.10 +begin
1.11
1.12  subsection "Arithmetic in terms of bool lists"
1.13
1.14 -consts (* arithmetic operations in terms of the reversed bool list,
1.15 +(* arithmetic operations in terms of the reversed bool list,
1.16    assuming input list(s) the same length, and don't extend them *)
1.17 -  rbl_succ :: "bool list => bool list"
1.18 -  rbl_pred :: "bool list => bool list"
1.19 -  rbl_add :: "bool list => bool list => bool list"
1.20 -  rbl_mult :: "bool list => bool list => bool list"
1.21
1.22 -primrec
1.23 +primrec rbl_succ :: "bool list => bool list" where
1.24    Nil: "rbl_succ Nil = Nil"
1.25 -  Cons: "rbl_succ (x # xs) = (if x then False # rbl_succ xs else True # xs)"
1.26 +  | Cons: "rbl_succ (x # xs) = (if x then False # rbl_succ xs else True # xs)"
1.27
1.28 -primrec
1.29 -  Nil : "rbl_pred Nil = Nil"
1.30 -  Cons : "rbl_pred (x # xs) = (if x then False # xs else True # rbl_pred xs)"
1.31 +primrec rbl_pred :: "bool list => bool list" where
1.32 +  Nil: "rbl_pred Nil = Nil"
1.33 +  | Cons: "rbl_pred (x # xs) = (if x then False # xs else True # rbl_pred xs)"
1.34
1.35 -primrec (* result is length of first arg, second arg may be longer *)
1.36 -  Nil : "rbl_add Nil x = Nil"
1.37 -  Cons : "rbl_add (y # ys) x = (let ws = rbl_add ys (tl x) in
1.38 +primrec rbl_add :: "bool list => bool list => bool list" where
1.39 +    (* result is length of first arg, second arg may be longer *)
1.40 +  Nil: "rbl_add Nil x = Nil"
1.41 +  | Cons: "rbl_add (y # ys) x = (let ws = rbl_add ys (tl x) in
1.42      (y ~= hd x) # (if hd x & y then rbl_succ ws else ws))"
1.43
1.44 -primrec (* result is length of first arg, second arg may be longer *)
1.45 -  Nil : "rbl_mult Nil x = Nil"
1.46 -  Cons : "rbl_mult (y # ys) x = (let ws = False # rbl_mult ys x in
1.47 +primrec rbl_mult :: "bool list => bool list => bool list" where
1.48 +    (* result is length of first arg, second arg may be longer *)
1.49 +  Nil: "rbl_mult Nil x = Nil"
1.50 +  | Cons: "rbl_mult (y # ys) x = (let ws = False # rbl_mult ys x in
1.51      if y then rbl_add ws x else ws)"
1.52
1.53  lemma tl_take: "tl (take n l) = take (n - 1) (tl l)"
1.54 @@ -102,16 +102,16 @@
1.55
1.56  (** link between bin and bool list **)
1.57
1.58 -lemma bl_to_bin_aux_append [rule_format] :
1.59 -  "ALL w. bl_to_bin_aux w (bs @ cs) = bl_to_bin_aux (bl_to_bin_aux w bs) cs"
1.60 -  by (induct bs) auto
1.61 +lemma bl_to_bin_aux_append:
1.62 +  "bl_to_bin_aux (bs @ cs) w = bl_to_bin_aux cs (bl_to_bin_aux bs w)"
1.63 +  by (induct bs arbitrary: w) auto
1.64
1.65 -lemma bin_to_bl_aux_append [rule_format] :
1.66 -  "ALL w bs. bin_to_bl_aux n w bs @ cs = bin_to_bl_aux n w (bs @ cs)"
1.67 -  by (induct n) auto
1.68 +lemma bin_to_bl_aux_append:
1.69 +  "bin_to_bl_aux n w bs @ cs = bin_to_bl_aux n w (bs @ cs)"
1.70 +  by (induct n arbitrary: w bs) auto
1.71
1.72  lemma bl_to_bin_append:
1.73 -  "bl_to_bin (bs @ cs) = bl_to_bin_aux (bl_to_bin bs) cs"
1.74 +  "bl_to_bin (bs @ cs) = bl_to_bin_aux cs (bl_to_bin bs)"
1.75    unfolding bl_to_bin_def by (rule bl_to_bin_aux_append)
1.76
1.77  lemma bin_to_bl_aux_alt:
1.78 @@ -121,25 +121,25 @@
1.79  lemma bin_to_bl_0: "bin_to_bl 0 bs = []"
1.80    unfolding bin_to_bl_def by auto
1.81
1.82 -lemma size_bin_to_bl_aux [rule_format] :
1.83 -  "ALL w bs. size (bin_to_bl_aux n w bs) = n + length bs"
1.84 -  by (induct n) auto
1.85 +lemma size_bin_to_bl_aux:
1.86 +  "size (bin_to_bl_aux n w bs) = n + length bs"
1.87 +  by (induct n arbitrary: w bs) auto
1.88
1.89  lemma size_bin_to_bl: "size (bin_to_bl n w) = n"
1.90    unfolding bin_to_bl_def by (simp add : size_bin_to_bl_aux)
1.91
1.92 -lemma bin_bl_bin' [rule_format] :
1.93 -  "ALL w bs. bl_to_bin (bin_to_bl_aux n w bs) =
1.94 -    bl_to_bin_aux (bintrunc n w) bs"
1.95 -  by (induct n) (auto simp add : bl_to_bin_def)
1.96 +lemma bin_bl_bin':
1.97 +  "bl_to_bin (bin_to_bl_aux n w bs) =
1.98 +    bl_to_bin_aux bs (bintrunc n w)"
1.99 +  by (induct n arbitrary: w bs) (auto simp add : bl_to_bin_def)
1.100
1.101  lemma bin_bl_bin: "bl_to_bin (bin_to_bl n w) = bintrunc n w"
1.102    unfolding bin_to_bl_def bin_bl_bin' by auto
1.103
1.104 -lemma bl_bin_bl' [rule_format] :
1.105 -  "ALL w n. bin_to_bl (n + length bs) (bl_to_bin_aux w bs) =
1.106 +lemma bl_bin_bl':
1.107 +  "bin_to_bl (n + length bs) (bl_to_bin_aux bs w) =
1.108      bin_to_bl_aux n w bs"
1.109 -  apply (induct "bs")
1.110 +  apply (induct bs arbitrary: w n)
1.111     apply auto
1.112      apply (simp_all only : add_Suc [symmetric])
1.113      apply (auto simp add : bin_to_bl_def)
1.114 @@ -175,9 +175,9 @@
1.115  lemma bl_to_bin_Nil: "bl_to_bin [] = Int.Pls"
1.116    unfolding bl_to_bin_def by auto
1.117
1.118 -lemma bin_to_bl_Pls_aux [rule_format] :
1.119 -  "ALL bl. bin_to_bl_aux n Int.Pls bl = replicate n False @ bl"
1.120 -  by (induct n) (auto simp: replicate_app_Cons_same)
1.121 +lemma bin_to_bl_Pls_aux:
1.122 +  "bin_to_bl_aux n Int.Pls bl = replicate n False @ bl"
1.123 +  by (induct n arbitrary: bl) (auto simp: replicate_app_Cons_same)
1.124
1.125  lemma bin_to_bl_Pls: "bin_to_bl n Int.Pls = replicate n False"
1.126    unfolding bin_to_bl_def by (simp add : bin_to_bl_Pls_aux)
1.127 @@ -223,26 +223,26 @@
1.128  lemma bl_to_bin_rep_False: "bl_to_bin (replicate n False) = Int.Pls"
1.129    by (induct n) auto
1.130
1.131 -lemma len_bin_to_bl_aux [rule_format] :
1.132 -  "ALL w bs. length (bin_to_bl_aux n w bs) = n + length bs"
1.133 -  by (induct "n") auto
1.134 +lemma len_bin_to_bl_aux:
1.135 +  "length (bin_to_bl_aux n w bs) = n + length bs"
1.136 +  by (induct n arbitrary: w bs) auto
1.137
1.138  lemma len_bin_to_bl [simp]: "length (bin_to_bl n w) = n"
1.139    unfolding bin_to_bl_def len_bin_to_bl_aux by auto
1.140
1.141 -lemma sign_bl_bin' [rule_format] :
1.142 -  "ALL w. bin_sign (bl_to_bin_aux w bs) = bin_sign w"
1.143 -  by (induct bs) auto
1.144 +lemma sign_bl_bin':
1.145 +  "bin_sign (bl_to_bin_aux bs w) = bin_sign w"
1.146 +  by (induct bs arbitrary: w) auto
1.147
1.148  lemma sign_bl_bin: "bin_sign (bl_to_bin bs) = Int.Pls"
1.149    unfolding bl_to_bin_def by (simp add : sign_bl_bin')
1.150
1.151 -lemma bl_sbin_sign_aux [rule_format] :
1.152 -  "ALL w bs. hd (bin_to_bl_aux (Suc n) w bs) =
1.153 +lemma bl_sbin_sign_aux:
1.154 +  "hd (bin_to_bl_aux (Suc n) w bs) =
1.155      (bin_sign (sbintrunc n w) = Int.Min)"
1.156 -  apply (induct "n")
1.157 +  apply (induct n arbitrary: w bs)
1.158     apply clarsimp
1.159 -   apply (case_tac w rule: bin_exhaust)
1.160 +   apply (cases w rule: bin_exhaust)
1.161     apply (simp split add : bit.split)
1.162    apply clarsimp
1.163    done
1.164 @@ -251,15 +251,15 @@
1.165    "hd (bin_to_bl (Suc n) w) = (bin_sign (sbintrunc n w) = Int.Min)"
1.166    unfolding bin_to_bl_def by (rule bl_sbin_sign_aux)
1.167
1.168 -lemma bin_nth_of_bl_aux [rule_format] :
1.169 -  "ALL w. bin_nth (bl_to_bin_aux w bl) n =
1.170 +lemma bin_nth_of_bl_aux [rule_format]:
1.171 +  "\<forall>w. bin_nth (bl_to_bin_aux bl w) n =
1.172      (n < size bl & rev bl ! n | n >= length bl & bin_nth w (n - size bl))"
1.173    apply (induct_tac bl)
1.174     apply clarsimp
1.175    apply clarsimp
1.176    apply (cut_tac x=n and y="size list" in linorder_less_linear)
1.177    apply (erule disjE, simp add: nth_append)+
1.178 -  apply (simp add: nth_append)
1.179 +  apply auto
1.180    done
1.181
1.182  lemma bin_nth_of_bl: "bin_nth (bl_to_bin bl) n = (n < length bl & rev bl ! n)";
1.183 @@ -307,14 +307,14 @@
1.184  lemma nth_bin_to_bl: "n < m ==> (bin_to_bl m w) ! n = bin_nth w (m - Suc n)"
1.185    unfolding bin_to_bl_def by (simp add : nth_bin_to_bl_aux)
1.186
1.187 -lemma bl_to_bin_lt2p_aux [rule_format] :
1.188 -  "ALL w. bl_to_bin_aux w bs < (w + 1) * (2 ^ length bs)"
1.189 -  apply (induct "bs")
1.190 +lemma bl_to_bin_lt2p_aux [rule_format]:
1.191 +  "\<forall>w. bl_to_bin_aux bs w < (w + 1) * (2 ^ length bs)"
1.192 +  apply (induct bs)
1.193     apply clarsimp
1.194    apply clarsimp
1.195    apply safe
1.196 -   apply (erule allE, erule xtr8 [rotated],
1.198 +  apply (erule allE, erule xtr8 [rotated],
1.200    done
1.201
1.202  lemma bl_to_bin_lt2p: "bl_to_bin bs < (2 ^ length bs)"
1.203 @@ -326,7 +326,7 @@
1.204    done
1.205
1.206  lemma bl_to_bin_ge2p_aux [rule_format] :
1.207 -  "ALL w. bl_to_bin_aux w bs >= w * (2 ^ length bs)"
1.208 +  "\<forall>w. bl_to_bin_aux bs w >= w * (2 ^ length bs)"
1.209    apply (induct bs)
1.210     apply clarsimp
1.211    apply clarsimp
1.212 @@ -354,10 +354,10 @@
1.213  lemmas butlast_bin_rest = butlast_rest_bin
1.214    [where w="bl_to_bin bl" and n="length bl", simplified, standard]
1.215
1.216 -lemma butlast_rest_bl2bin_aux [rule_format] :
1.217 -  "ALL w. bl ~= [] -->
1.218 -    bl_to_bin_aux w (butlast bl) = bin_rest (bl_to_bin_aux w bl)"
1.219 -  by (induct bl) auto
1.220 +lemma butlast_rest_bl2bin_aux:
1.221 +  "bl ~= [] \<Longrightarrow>
1.222 +    bl_to_bin_aux (butlast bl) w = bin_rest (bl_to_bin_aux bl w)"
1.223 +  by (induct bl arbitrary: w) auto
1.224
1.225  lemma butlast_rest_bl2bin:
1.226    "bl_to_bin (butlast bl) = bin_rest (bl_to_bin bl)"
1.227 @@ -366,9 +366,9 @@
1.228     apply (auto simp add: butlast_rest_bl2bin_aux)
1.229    done
1.230
1.231 -lemma trunc_bl2bin_aux [rule_format] :
1.232 -  "ALL w. bintrunc m (bl_to_bin_aux w bl) =
1.233 -    bl_to_bin_aux (bintrunc (m - length bl) w) (drop (length bl - m) bl)"
1.234 +lemma trunc_bl2bin_aux [rule_format]:
1.235 +  "ALL w. bintrunc m (bl_to_bin_aux bl w) =
1.236 +    bl_to_bin_aux (drop (length bl - m) bl) (bintrunc (m - length bl) w)"
1.237    apply (induct_tac bl)
1.238     apply clarsimp
1.239    apply clarsimp
1.240 @@ -376,13 +376,13 @@
1.241     apply (case_tac "m - size list")
1.242      apply (simp add : diff_is_0_eq [THEN iffD1, THEN Suc_diff_le])
1.243     apply simp
1.244 -   apply (rule_tac f = "%nat. bl_to_bin_aux (Int.Bit1 (bintrunc nat w)) list"
1.245 +   apply (rule_tac f = "%nat. bl_to_bin_aux list (Int.Bit1 (bintrunc nat w))"
1.246                     in arg_cong)
1.247     apply simp
1.248    apply (case_tac "m - size list")
1.249     apply (simp add: diff_is_0_eq [THEN iffD1, THEN Suc_diff_le])
1.250    apply simp
1.251 -  apply (rule_tac f = "%nat. bl_to_bin_aux (Int.Bit0 (bintrunc nat w)) list"
1.252 +  apply (rule_tac f = "%nat. bl_to_bin_aux list (Int.Bit0 (bintrunc nat w))"
1.253                    in arg_cong)
1.254    apply simp
1.255    done
1.256 @@ -420,9 +420,9 @@
1.257  lemma hd_butlast: "size xs > 1 ==> hd (butlast xs) = hd xs"
1.258    by (cases xs) auto
1.259
1.260 -lemma last_bin_last' [rule_format] :
1.261 -  "ALL w. size xs > 0 --> last xs = (bin_last (bl_to_bin_aux w xs) = bit.B1)"
1.262 -  by (induct xs) auto
1.263 +lemma last_bin_last':
1.264 +  "size xs > 0 \<Longrightarrow> last xs = (bin_last (bl_to_bin_aux xs w) = bit.B1)"
1.265 +  by (induct xs arbitrary: w) auto
1.266
1.267  lemma last_bin_last:
1.268    "size xs > 0 ==> last xs = (bin_last (bl_to_bin xs) = bit.B1)"
1.269 @@ -437,16 +437,16 @@
1.270
1.271  (** links between bit-wise operations and operations on bool lists **)
1.272
1.273 -lemma app2_Nil [simp]: "app2 f [] ys = []"
1.274 -  unfolding app2_def by auto
1.275 +lemma map2_Nil [simp]: "map2 f [] ys = []"
1.276 +  unfolding map2_def by auto
1.277
1.278 -lemma app2_Cons [simp]:
1.279 -  "app2 f (x # xs) (y # ys) = f x y # app2 f xs ys"
1.280 -  unfolding app2_def by auto
1.281 +lemma map2_Cons [simp]:
1.282 +  "map2 f (x # xs) (y # ys) = f x y # map2 f xs ys"
1.283 +  unfolding map2_def by auto
1.284
1.285  lemma bl_xor_aux_bin [rule_format] : "ALL v w bs cs.
1.286 -    app2 (%x y. x ~= y) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) =
1.287 -    bin_to_bl_aux n (v XOR w) (app2 (%x y. x ~= y) bs cs)"
1.288 +    map2 (%x y. x ~= y) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) =
1.289 +    bin_to_bl_aux n (v XOR w) (map2 (%x y. x ~= y) bs cs)"
1.290    apply (induct_tac n)
1.291     apply safe
1.292     apply simp
1.293 @@ -458,8 +458,8 @@
1.294    done
1.295
1.296  lemma bl_or_aux_bin [rule_format] : "ALL v w bs cs.
1.297 -    app2 (op | ) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) =
1.298 -    bin_to_bl_aux n (v OR w) (app2 (op | ) bs cs)"
1.299 +    map2 (op | ) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) =
1.300 +    bin_to_bl_aux n (v OR w) (map2 (op | ) bs cs)"
1.301    apply (induct_tac n)
1.302     apply safe
1.303     apply simp
1.304 @@ -471,8 +471,8 @@
1.305    done
1.306
1.307  lemma bl_and_aux_bin [rule_format] : "ALL v w bs cs.
1.308 -    app2 (op & ) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) =
1.309 -    bin_to_bl_aux n (v AND w) (app2 (op & ) bs cs)"
1.310 +    map2 (op & ) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) =
1.311 +    bin_to_bl_aux n (v AND w) (map2 (op & ) bs cs)"
1.312    apply (induct_tac n)
1.313     apply safe
1.314     apply simp
1.315 @@ -498,13 +498,13 @@
1.316    [where cs = "[]", unfolded bin_to_bl_def [symmetric] map.simps]
1.317
1.318  lemmas bl_and_bin = bl_and_aux_bin [where bs="[]" and cs="[]",
1.319 -                                    unfolded app2_Nil, folded bin_to_bl_def]
1.320 +                                    unfolded map2_Nil, folded bin_to_bl_def]
1.321
1.322  lemmas bl_or_bin = bl_or_aux_bin [where bs="[]" and cs="[]",
1.323 -                                  unfolded app2_Nil, folded bin_to_bl_def]
1.324 +                                  unfolded map2_Nil, folded bin_to_bl_def]
1.325
1.326  lemmas bl_xor_bin = bl_xor_aux_bin [where bs="[]" and cs="[]",
1.327 -                                    unfolded app2_Nil, folded bin_to_bl_def]
1.328 +                                    unfolded map2_Nil, folded bin_to_bl_def]
1.329
1.330  lemma drop_bin2bl_aux [rule_format] :
1.331    "ALL m bin bs. drop m (bin_to_bl_aux n bin bs) =
1.332 @@ -651,8 +651,8 @@
1.333  (* links with function bl_to_bin *)
1.334
1.335  lemma bl_to_bin_aux_cat:
1.336 -  "!!nv v. bl_to_bin_aux (bin_cat w nv v) bs =
1.337 -    bin_cat w (nv + length bs) (bl_to_bin_aux v bs)"
1.338 +  "!!nv v. bl_to_bin_aux bs (bin_cat w nv v) =
1.339 +    bin_cat w (nv + length bs) (bl_to_bin_aux bs v)"
1.340    apply (induct bs)
1.341     apply simp
1.342    apply (simp add: bin_cat_Suc_Bit [symmetric] del: bin_cat.simps)
1.343 @@ -985,19 +985,21 @@
1.344    rsplit_aux_simp1s [OF disjI1] rsplit_aux_simp1s [OF disjI2]
1.345
1.346  lemma bin_rsplit_aux_append:
1.347 -  "bin_rsplit_aux (n, bs @ cs, m, c) = bin_rsplit_aux (n, bs, m, c) @ cs"
1.348 -  apply (rule_tac u=n and v=bs and w=m and x=c in bin_rsplit_aux.induct)
1.349 +  "bin_rsplit_aux n m c (bs @ cs) = bin_rsplit_aux n m c bs @ cs"
1.350 +  apply (induct n m c bs rule: bin_rsplit_aux.induct)
1.351    apply (subst bin_rsplit_aux.simps)
1.352    apply (subst bin_rsplit_aux.simps)
1.353    apply (clarsimp split: ls_splits)
1.354 +  apply auto
1.355    done
1.356
1.357  lemma bin_rsplitl_aux_append:
1.358 -  "bin_rsplitl_aux (n, bs @ cs, m, c) = bin_rsplitl_aux (n, bs, m, c) @ cs"
1.359 -  apply (rule_tac u=n and v=bs and w=m and x=c in bin_rsplitl_aux.induct)
1.360 +  "bin_rsplitl_aux n m c (bs @ cs) = bin_rsplitl_aux n m c bs @ cs"
1.361 +  apply (induct n m c bs rule: bin_rsplitl_aux.induct)
1.362    apply (subst bin_rsplitl_aux.simps)
1.363    apply (subst bin_rsplitl_aux.simps)
1.364    apply (clarsimp split: ls_splits)
1.365 +  apply auto
1.366    done
1.367
1.368  lemmas rsplit_aux_apps [where bs = "[]"] =
1.369 @@ -1024,17 +1026,18 @@
1.370  declare bin_split_pred_simp [simp]
1.371
1.372  lemma bin_rsplit_aux_simp_alt:
1.373 -  "bin_rsplit_aux (n, bs, m, c) =
1.374 +  "bin_rsplit_aux n m c bs =
1.375     (if m = 0 \<or> n = 0
1.376     then bs
1.377     else let (a, b) = bin_split n c in bin_rsplit n (m - n, a) @ b # bs)"
1.378 -  apply (rule trans)
1.379 -   apply (subst bin_rsplit_aux.simps, rule refl)
1.380 -  apply (simp add: rsplit_aux_alts)
1.381 +  unfolding bin_rsplit_aux.simps [of n m c bs]
1.382 +  apply simp
1.383 +  apply (subst rsplit_aux_alts)
1.384 +  apply (simp add: bin_rsplit_def)
1.385    done
1.386
1.387  lemmas bin_rsplit_simp_alt =
1.388 -  trans [OF bin_rsplit_def [THEN meta_eq_to_obj_eq]
1.389 +  trans [OF bin_rsplit_def
1.390              bin_rsplit_aux_simp_alt, standard]
1.391
1.392  lemmas bthrs = bin_rsplit_simp_alt [THEN [2] trans]
1.393 @@ -1089,27 +1092,33 @@
1.394    apply (rule allI)
1.395    apply (subst bin_rsplitl_aux.simps)
1.396    apply (subst bin_rsplit_aux.simps)
1.397 -  apply (clarsimp simp: rsplit_aux_alts Let_def split: ls_splits)
1.398 +  apply (clarsimp simp: Let_def split: ls_splits)
1.399    apply (drule bin_split_trunc)
1.400    apply (drule sym [THEN trans], assumption)
1.401 -  apply fast
1.402 +  apply (subst rsplit_aux_alts(1))
1.403 +  apply (subst rsplit_aux_alts(2))
1.404 +  apply clarsimp
1.405 +  unfolding bin_rsplit_def bin_rsplitl_def
1.406 +  apply simp
1.407    done
1.408 -
1.409 +
1.410  lemma bin_rsplit_rcat [rule_format] :
1.411    "n > 0 --> bin_rsplit n (n * size ws, bin_rcat n ws) = map (bintrunc n) ws"
1.412    apply (unfold bin_rsplit_def bin_rcat_def)
1.413    apply (rule_tac xs = "ws" in rev_induct)
1.414     apply clarsimp
1.415    apply clarsimp
1.416 -  apply (clarsimp simp add: bin_split_cat rsplit_aux_alts)
1.417 +  apply (subst rsplit_aux_alts)
1.418 +  unfolding bin_split_cat
1.419 +  apply simp
1.420    done
1.421
1.422  lemma bin_rsplit_aux_len_le [rule_format] :
1.423 -  "ALL ws m. n \<noteq> 0 --> ws = bin_rsplit_aux (n, bs, nw, w) -->
1.424 -    (length ws <= m) = (nw + length bs * n <= m * n)"
1.425 -  apply (rule_tac u=n and v=bs and w=nw and x=w in bin_rsplit_aux.induct)
1.426 +  "\<forall>ws m. n \<noteq> 0 \<longrightarrow> ws = bin_rsplit_aux n nw w bs \<longrightarrow>
1.427 +    length ws \<le> m \<longleftrightarrow> nw + length bs * n \<le> m * n"
1.428 +  apply (induct n nw w bs rule: bin_rsplit_aux.induct)
1.429    apply (subst bin_rsplit_aux.simps)
1.430 -  apply (simp add:lrlem Let_def split: ls_splits )
1.431 +  apply (simp add: lrlem Let_def split: ls_splits)
1.432    done
1.433
1.434  lemma bin_rsplit_len_le:
1.435 @@ -1117,9 +1126,9 @@
1.436    unfolding bin_rsplit_def by (clarsimp simp add : bin_rsplit_aux_len_le)
1.437
1.438  lemma bin_rsplit_aux_len [rule_format] :
1.439 -  "n\<noteq>0 --> length (bin_rsplit_aux (n, cs, nw, w)) =
1.440 +  "n\<noteq>0 --> length (bin_rsplit_aux n nw w cs) =
1.441      (nw + n - 1) div n + length cs"
1.442 -  apply (rule_tac u=n and v=cs and w=nw and x=w in bin_rsplit_aux.induct)
1.443 +  apply (induct n nw w cs rule: bin_rsplit_aux.induct)
1.444    apply (subst bin_rsplit_aux.simps)
1.445    apply (clarsimp simp: Let_def split: ls_splits)
1.446    apply (erule thin_rl)
1.447 @@ -1134,27 +1143,30 @@
1.448    "n\<noteq>0 ==> length (bin_rsplit n (nw, w)) = (nw + n - 1) div n"
1.449    unfolding bin_rsplit_def by (clarsimp simp add : bin_rsplit_aux_len)
1.450
1.451 -lemma bin_rsplit_aux_len_indep [rule_format] :
1.452 -  "n\<noteq>0 ==> (ALL v bs. length bs = length cs -->
1.453 -    length (bin_rsplit_aux (n, bs, nw, v)) =
1.454 -    length (bin_rsplit_aux (n, cs, nw, w)))"
1.455 -  apply (rule_tac u=n and v=cs and w=nw and x=w in bin_rsplit_aux.induct)
1.456 -  apply clarsimp
1.457 -  apply (simp (no_asm_simp) add: bin_rsplit_aux_simp_alt Let_def
1.458 -                            split: ls_splits)
1.459 -  apply clarify
1.460 -  apply (erule allE)+
1.461 -  apply (erule impE)
1.462 -   apply (fast elim!: sym)
1.463 -  apply (simp (no_asm_use) add: rsplit_aux_alts)
1.464 -  apply (erule impE)
1.465 -  apply (rule_tac x="ba # bs" in exI)
1.466 -  apply auto
1.467 -  done
1.468 +lemma bin_rsplit_aux_len_indep:
1.469 +  "n \<noteq> 0 \<Longrightarrow> length bs = length cs \<Longrightarrow>
1.470 +    length (bin_rsplit_aux n nw v bs) =
1.471 +    length (bin_rsplit_aux n nw w cs)"
1.472 +proof (induct n nw w cs arbitrary: v bs rule: bin_rsplit_aux.induct)
1.473 +  case (1 n m w cs v bs) show ?case
1.474 +  proof (cases "m = 0")
1.475 +    case True then show ?thesis by simp
1.476 +  next
1.477 +    case False
1.478 +    from "1.hyps" `m \<noteq> 0` `n \<noteq> 0` have hyp: "\<And>v bs. length bs = Suc (length cs) \<Longrightarrow>
1.479 +      length (bin_rsplit_aux n (m - n) v bs) =
1.480 +      length (bin_rsplit_aux n (m - n) (fst (bin_split n w)) (snd (bin_split n w) # cs))"
1.481 +    by auto
1.482 +    show ?thesis using `length bs = length cs` `n \<noteq> 0`
1.483 +      by (auto simp add: bin_rsplit_aux_simp_alt Let_def bin_rsplit_len
1.484 +        split: ls_splits)
1.485 +  qed
1.486 +qed
1.487
1.488  lemma bin_rsplit_len_indep:
1.489    "n\<noteq>0 ==> length (bin_rsplit n (nw, v)) = length (bin_rsplit n (nw, w))"
1.490    apply (unfold bin_rsplit_def)
1.491 +  apply (simp (no_asm))
1.492    apply (erule bin_rsplit_aux_len_indep)
1.493    apply (rule refl)
1.494    done
```
```     2.1 --- a/src/HOL/Word/BinGeneral.thy	Fri Apr 04 13:40:23 2008 +0200
2.2 +++ b/src/HOL/Word/BinGeneral.thy	Fri Apr 04 13:40:24 2008 +0200
2.3 @@ -9,98 +9,201 @@
2.4
2.5  header {* Basic Definitions for Binary Integers *}
2.6
2.7 -theory BinGeneral imports Num_Lemmas
2.8 -
2.9 +theory BinGeneral
2.10 +imports Num_Lemmas
2.11  begin
2.12
2.13 -subsection {* Recursion combinator for binary integers *}
2.14 +subsection {* Further properties of numerals *}
2.15 +
2.16 +datatype bit = B0 | B1
2.17 +
2.18 +definition
2.19 +  Bit :: "int \<Rightarrow> bit \<Rightarrow> int" (infixl "BIT" 90) where
2.20 +  "k BIT b = (case b of B0 \<Rightarrow> 0 | B1 \<Rightarrow> 1) + k + k"
2.21 +
2.22 +lemma BIT_B0_eq_Bit0 [simp]: "w BIT B0 = Int.Bit0 w"
2.23 +  unfolding Bit_def Bit0_def by simp
2.24 +
2.25 +lemma BIT_B1_eq_Bit1 [simp]: "w BIT B1 = Int.Bit1 w"
2.26 +  unfolding Bit_def Bit1_def by simp
2.27 +
2.28 +lemmas BIT_simps = BIT_B0_eq_Bit0 BIT_B1_eq_Bit1
2.29
2.30 -lemma brlem: "(bin = Int.Min) = (- bin + Int.pred 0 = 0)"
2.31 -  unfolding Min_def pred_def by arith
2.32 +hide (open) const B0 B1
2.33 +
2.34 +lemma Min_ne_Pls [iff]:
2.35 +  "Int.Min ~= Int.Pls"
2.36 +  unfolding Min_def Pls_def by auto
2.37 +
2.38 +lemmas Pls_ne_Min [iff] = Min_ne_Pls [symmetric]
2.39 +
2.40 +lemmas PlsMin_defs [intro!] =
2.41 +  Pls_def Min_def Pls_def [symmetric] Min_def [symmetric]
2.42 +
2.43 +lemmas PlsMin_simps [simp] = PlsMin_defs [THEN Eq_TrueI]
2.44 +
2.45 +lemma number_of_False_cong:
2.46 +  "False \<Longrightarrow> number_of x = number_of y"
2.47 +  by (rule FalseE)
2.48 +
2.49 +(** ways in which type Bin resembles a datatype **)
2.50
2.51 -function
2.52 -  bin_rec :: "'a \<Rightarrow> 'a \<Rightarrow> (int \<Rightarrow> bit \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> int \<Rightarrow> 'a"
2.53 -where
2.54 -  "bin_rec f1 f2 f3 bin = (if bin = Int.Pls then f1
2.55 -    else if bin = Int.Min then f2
2.56 -    else case bin_rl bin of (w, b) => f3 w b (bin_rec f1 f2 f3 w))"
2.57 -  by pat_completeness auto
2.58 +lemma BIT_eq: "u BIT b = v BIT c ==> u = v & b = c"
2.59 +  apply (unfold Bit_def)
2.60 +  apply (simp (no_asm_use) split: bit.split_asm)
2.61 +     apply simp_all
2.62 +   apply (drule_tac f=even in arg_cong, clarsimp)+
2.63 +  done
2.64 +
2.65 +lemmas BIT_eqE [elim!] = BIT_eq [THEN conjE, standard]
2.66 +
2.67 +lemma BIT_eq_iff [simp]:
2.68 +  "(u BIT b = v BIT c) = (u = v \<and> b = c)"
2.69 +  by (rule iffI) auto
2.70 +
2.71 +lemmas BIT_eqI [intro!] = conjI [THEN BIT_eq_iff [THEN iffD2]]
2.72 +
2.73 +lemma less_Bits:
2.74 +  "(v BIT b < w BIT c) = (v < w | v <= w & b = bit.B0 & c = bit.B1)"
2.75 +  unfolding Bit_def by (auto split: bit.split)
2.76
2.77 -termination
2.78 -  apply (relation "measure (nat o abs o snd o snd o snd)")
2.79 -   apply simp
2.80 -  apply (simp add: Pls_def brlem)
2.81 -  apply (clarsimp simp: bin_rl_char pred_def)
2.82 -  apply (frule thin_rl [THEN refl [THEN bin_abs_lem [rule_format]]])
2.83 -    apply (unfold Pls_def Min_def number_of_eq)
2.84 -    prefer 2
2.85 -    apply (erule asm_rl)
2.86 -   apply auto
2.87 +lemma le_Bits:
2.88 +  "(v BIT b <= w BIT c) = (v < w | v <= w & (b ~= bit.B1 | c ~= bit.B0))"
2.89 +  unfolding Bit_def by (auto split: bit.split)
2.90 +
2.91 +lemma no_no [simp]: "number_of (number_of i) = i"
2.92 +  unfolding number_of_eq by simp
2.93 +
2.94 +lemma Bit_B0:
2.95 +  "k BIT bit.B0 = k + k"
2.96 +   by (unfold Bit_def) simp
2.97 +
2.98 +lemma Bit_B1:
2.99 +  "k BIT bit.B1 = k + k + 1"
2.100 +   by (unfold Bit_def) simp
2.101 +
2.102 +lemma Bit_B0_2t: "k BIT bit.B0 = 2 * k"
2.103 +  by (rule trans, rule Bit_B0) simp
2.104 +
2.105 +lemma Bit_B1_2t: "k BIT bit.B1 = 2 * k + 1"
2.106 +  by (rule trans, rule Bit_B1) simp
2.107 +
2.108 +lemma B_mod_2':
2.109 +  "X = 2 ==> (w BIT bit.B1) mod X = 1 & (w BIT bit.B0) mod X = 0"
2.110 +  apply (simp (no_asm) only: Bit_B0 Bit_B1)
2.111 +  apply (simp add: z1pmod2)
2.112    done
2.113
2.114 -declare bin_rec.simps [simp del]
2.115 +lemma B1_mod_2 [simp]: "(Int.Bit1 w) mod 2 = 1"
2.116 +  unfolding numeral_simps number_of_is_id by (simp add: z1pmod2)
2.117
2.118 -lemma bin_rec_PM:
2.119 -  "f = bin_rec f1 f2 f3 ==> f Int.Pls = f1 & f Int.Min = f2"
2.120 -  by (auto simp add: bin_rec.simps)
2.121 -
2.122 -lemma bin_rec_Pls: "bin_rec f1 f2 f3 Int.Pls = f1"
2.123 -  by (simp add: bin_rec.simps)
2.124 +lemma B0_mod_2 [simp]: "(Int.Bit0 w) mod 2 = 0"
2.125 +  unfolding numeral_simps number_of_is_id by simp
2.126
2.127 -lemma bin_rec_Min: "bin_rec f1 f2 f3 Int.Min = f2"
2.128 -  by (simp add: bin_rec.simps)
2.129 +lemma neB1E [elim!]:
2.130 +  assumes ne: "y \<noteq> bit.B1"
2.131 +  assumes y: "y = bit.B0 \<Longrightarrow> P"
2.132 +  shows "P"
2.133 +  apply (rule y)
2.134 +  apply (cases y rule: bit.exhaust, simp)
2.135 +  apply (simp add: ne)
2.136 +  done
2.137
2.138 -lemma bin_rec_Bit0:
2.139 -  "f3 Int.Pls bit.B0 f1 = f1 \<Longrightarrow>
2.140 -    bin_rec f1 f2 f3 (Int.Bit0 w) = f3 w bit.B0 (bin_rec f1 f2 f3 w)"
2.141 -  apply (simp add: bin_rec_Pls bin_rec.simps [of _ _ _ "Int.Bit0 w"])
2.142 -  unfolding Pls_def Min_def Bit0_def
2.143 -  apply auto
2.144 -  apply presburger
2.145 -  apply (simp add: bin_rec.simps)
2.146 +lemma bin_ex_rl: "EX w b. w BIT b = bin"
2.147 +  apply (unfold Bit_def)
2.148 +  apply (cases "even bin")
2.149 +   apply (clarsimp simp: even_equiv_def)
2.150 +   apply (auto simp: odd_equiv_def split: bit.split)
2.151    done
2.152
2.153 -lemma bin_rec_Bit1:
2.154 -  "f3 Int.Min bit.B1 f2 = f2 \<Longrightarrow>
2.155 -    bin_rec f1 f2 f3 (Int.Bit1 w) = f3 w bit.B1 (bin_rec f1 f2 f3 w)"
2.156 -  apply (simp add: bin_rec.simps [of _ _ _ "Int.Bit1 w"])
2.157 -  unfolding Pls_def Min_def Bit1_def
2.158 -  apply auto
2.159 -  apply (cases w)
2.160 -  apply auto
2.161 -  apply (simp add: bin_rec.simps)
2.162 -    unfolding Min_def Pls_def number_of_is_id apply auto
2.163 -  unfolding Bit0_def apply presburger
2.164 +lemma bin_exhaust:
2.165 +  assumes Q: "\<And>x b. bin = x BIT b \<Longrightarrow> Q"
2.166 +  shows "Q"
2.167 +  apply (insert bin_ex_rl [of bin])
2.168 +  apply (erule exE)+
2.169 +  apply (rule Q)
2.170 +  apply force
2.171    done
2.172 -
2.173 -lemma bin_rec_Bit:
2.174 -  "f = bin_rec f1 f2 f3  ==> f3 Int.Pls bit.B0 f1 = f1 ==>
2.175 -    f3 Int.Min bit.B1 f2 = f2 ==> f (w BIT b) = f3 w b (f w)"
2.177
2.178 -lemmas bin_rec_simps = refl [THEN bin_rec_Bit] bin_rec_Pls bin_rec_Min
2.179 -  bin_rec_Bit0 bin_rec_Bit1
2.180
2.181  subsection {* Destructors for binary integers *}
2.182
2.183 +definition bin_rl :: "int \<Rightarrow> int \<times> bit" where
2.184 +  [code func del]: "bin_rl w = (THE (r, l). w = r BIT l)"
2.185 +
2.186 +lemma bin_rl_char: "(bin_rl w = (r, l)) = (r BIT l = w)"
2.187 +  apply (unfold bin_rl_def)
2.188 +  apply safe
2.189 +   apply (cases w rule: bin_exhaust)
2.190 +   apply auto
2.191 +  done
2.192 +
2.193  definition
2.194    bin_rest_def [code func del]: "bin_rest w = fst (bin_rl w)"
2.195
2.196  definition
2.197    bin_last_def [code func del] : "bin_last w = snd (bin_rl w)"
2.198
2.199 -definition
2.200 -  bin_sign_def [code func del] : "bin_sign = bin_rec Int.Pls Int.Min (%w b s. s)"
2.201 -
2.202  primrec bin_nth where
2.203 -  "bin_nth.Z" : "bin_nth w 0 = (bin_last w = bit.B1)"
2.204 -  | "bin_nth.Suc" : "bin_nth w (Suc n) = bin_nth (bin_rest w) n"
2.205 +  Z: "bin_nth w 0 = (bin_last w = bit.B1)"
2.206 +  | Suc: "bin_nth w (Suc n) = bin_nth (bin_rest w) n"
2.207
2.208  lemma bin_rl: "bin_rl w = (bin_rest w, bin_last w)"
2.209    unfolding bin_rest_def bin_last_def by auto
2.210
2.211 +lemma bin_rl_simps [simp]:
2.212 +  "bin_rl Int.Pls = (Int.Pls, bit.B0)"
2.213 +  "bin_rl Int.Min = (Int.Min, bit.B1)"
2.214 +  "bin_rl (Int.Bit0 r) = (r, bit.B0)"
2.215 +  "bin_rl (Int.Bit1 r) = (r, bit.B1)"
2.216 +  "bin_rl (r BIT b) = (r, b)"
2.217 +  unfolding bin_rl_char by simp_all
2.218 +
2.219 +declare bin_rl_simps(1-4) [code func]
2.220 +
2.221  lemmas bin_rl_simp [simp] = iffD1 [OF bin_rl_char bin_rl]
2.222
2.223 +lemma bin_abs_lem:
2.224 +  "bin = (w BIT b) ==> ~ bin = Int.Min --> ~ bin = Int.Pls -->
2.225 +    nat (abs w) < nat (abs bin)"
2.226 +  apply (clarsimp simp add: bin_rl_char)
2.227 +  apply (unfold Pls_def Min_def Bit_def)
2.228 +  apply (cases b)
2.229 +   apply (clarsimp, arith)
2.230 +  apply (clarsimp, arith)
2.231 +  done
2.232 +
2.233 +lemma bin_induct:
2.234 +  assumes PPls: "P Int.Pls"
2.235 +    and PMin: "P Int.Min"
2.236 +    and PBit: "!!bin bit. P bin ==> P (bin BIT bit)"
2.237 +  shows "P bin"
2.238 +  apply (rule_tac P=P and a=bin and f1="nat o abs"
2.239 +                  in wf_measure [THEN wf_induct])
2.240 +  apply (simp add: measure_def inv_image_def)
2.241 +  apply (case_tac x rule: bin_exhaust)
2.242 +  apply (frule bin_abs_lem)
2.243 +  apply (auto simp add : PPls PMin PBit)
2.244 +  done
2.245 +
2.246 +lemma numeral_induct:
2.247 +  assumes Pls: "P Int.Pls"
2.248 +  assumes Min: "P Int.Min"
2.249 +  assumes Bit0: "\<And>w. \<lbrakk>P w; w \<noteq> Int.Pls\<rbrakk> \<Longrightarrow> P (Int.Bit0 w)"
2.250 +  assumes Bit1: "\<And>w. \<lbrakk>P w; w \<noteq> Int.Min\<rbrakk> \<Longrightarrow> P (Int.Bit1 w)"
2.251 +  shows "P x"
2.252 +  apply (induct x rule: bin_induct)
2.253 +    apply (rule Pls)
2.254 +   apply (rule Min)
2.255 +  apply (case_tac bit)
2.256 +   apply (case_tac "bin = Int.Pls")
2.257 +    apply simp
2.258 +   apply (simp add: Bit0)
2.259 +  apply (case_tac "bin = Int.Min")
2.260 +   apply simp
2.261 +  apply (simp add: Bit1)
2.262 +  done
2.263 +
2.264  lemma bin_rest_simps [simp]:
2.265    "bin_rest Int.Pls = Int.Pls"
2.266    "bin_rest Int.Min = Int.Min"
2.267 @@ -121,16 +224,6 @@
2.268
2.269  declare bin_last_simps(1-4) [code func]
2.270
2.271 -lemma bin_sign_simps [simp]:
2.274 -  "bin_sign (Int.Bit0 w) = bin_sign w"
2.275 -  "bin_sign (Int.Bit1 w) = bin_sign w"
2.276 -  "bin_sign (w BIT b) = bin_sign w"
2.277 -  unfolding bin_sign_def by (auto simp: bin_rec_simps)
2.278 -
2.279 -declare bin_sign_simps(1-4) [code func]
2.280 -
2.281  lemma bin_r_l_extras [simp]:
2.282    "bin_last 0 = bit.B0"
2.283    "bin_last (- 1) = bit.B1"
2.284 @@ -237,11 +330,94 @@
2.285    bin_nth_0 bin_nth_Suc bin_nth_Pls bin_nth_Min bin_nth_minus
2.286    bin_nth_minus_Bit0 bin_nth_minus_Bit1
2.287
2.288 +
2.289 +subsection {* Recursion combinator for binary integers *}
2.290 +
2.291 +lemma brlem: "(bin = Int.Min) = (- bin + Int.pred 0 = 0)"
2.292 +  unfolding Min_def pred_def by arith
2.293 +
2.294 +function
2.295 +  bin_rec :: "'a \<Rightarrow> 'a \<Rightarrow> (int \<Rightarrow> bit \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> int \<Rightarrow> 'a"
2.296 +where
2.297 +  "bin_rec f1 f2 f3 bin = (if bin = Int.Pls then f1
2.298 +    else if bin = Int.Min then f2
2.299 +    else case bin_rl bin of (w, b) => f3 w b (bin_rec f1 f2 f3 w))"
2.300 +  by pat_completeness auto
2.301 +
2.302 +termination
2.303 +  apply (relation "measure (nat o abs o snd o snd o snd)")
2.304 +   apply simp
2.305 +  apply (simp add: Pls_def brlem)
2.306 +  apply (clarsimp simp: bin_rl_char pred_def)
2.307 +  apply (frule thin_rl [THEN refl [THEN bin_abs_lem [rule_format]]])
2.308 +    apply (unfold Pls_def Min_def number_of_eq)
2.309 +    prefer 2
2.310 +    apply (erule asm_rl)
2.311 +   apply auto
2.312 +  done
2.313 +
2.314 +declare bin_rec.simps [simp del]
2.315 +
2.316 +lemma bin_rec_PM:
2.317 +  "f = bin_rec f1 f2 f3 ==> f Int.Pls = f1 & f Int.Min = f2"
2.318 +  by (auto simp add: bin_rec.simps)
2.319 +
2.320 +lemma bin_rec_Pls: "bin_rec f1 f2 f3 Int.Pls = f1"
2.321 +  by (simp add: bin_rec.simps)
2.322 +
2.323 +lemma bin_rec_Min: "bin_rec f1 f2 f3 Int.Min = f2"
2.324 +  by (simp add: bin_rec.simps)
2.325 +
2.326 +lemma bin_rec_Bit0:
2.327 +  "f3 Int.Pls bit.B0 f1 = f1 \<Longrightarrow>
2.328 +    bin_rec f1 f2 f3 (Int.Bit0 w) = f3 w bit.B0 (bin_rec f1 f2 f3 w)"
2.329 +  apply (simp add: bin_rec_Pls bin_rec.simps [of _ _ _ "Int.Bit0 w"])
2.330 +  unfolding Pls_def Min_def Bit0_def
2.331 +  apply auto
2.332 +  apply presburger
2.333 +  apply (simp add: bin_rec.simps)
2.334 +  done
2.335 +
2.336 +lemma bin_rec_Bit1:
2.337 +  "f3 Int.Min bit.B1 f2 = f2 \<Longrightarrow>
2.338 +    bin_rec f1 f2 f3 (Int.Bit1 w) = f3 w bit.B1 (bin_rec f1 f2 f3 w)"
2.339 +  apply (simp add: bin_rec.simps [of _ _ _ "Int.Bit1 w"])
2.340 +  unfolding Pls_def Min_def Bit1_def
2.341 +  apply auto
2.342 +  apply (cases w)
2.343 +  apply auto
2.344 +  apply (simp add: bin_rec.simps)
2.345 +    unfolding Min_def Pls_def number_of_is_id apply auto
2.346 +  unfolding Bit0_def apply presburger
2.347 +  done
2.348 +
2.349 +lemma bin_rec_Bit:
2.350 +  "f = bin_rec f1 f2 f3  ==> f3 Int.Pls bit.B0 f1 = f1 ==>
2.351 +    f3 Int.Min bit.B1 f2 = f2 ==> f (w BIT b) = f3 w b (f w)"
2.353 +
2.354 +lemmas bin_rec_simps = refl [THEN bin_rec_Bit] bin_rec_Pls bin_rec_Min
2.355 +  bin_rec_Bit0 bin_rec_Bit1
2.356 +
2.357 +
2.358 +subsection {* Truncating binary integers *}
2.359 +
2.360 +definition
2.361 +  bin_sign_def [code func del] : "bin_sign = bin_rec Int.Pls Int.Min (%w b s. s)"
2.362 +
2.363 +lemma bin_sign_simps [simp]:
2.366 +  "bin_sign (Int.Bit0 w) = bin_sign w"
2.367 +  "bin_sign (Int.Bit1 w) = bin_sign w"
2.368 +  "bin_sign (w BIT b) = bin_sign w"
2.369 +  unfolding bin_sign_def by (auto simp: bin_rec_simps)
2.370 +
2.371 +declare bin_sign_simps(1-4) [code func]
2.372 +
2.373  lemma bin_sign_rest [simp]:
2.374    "bin_sign (bin_rest w) = (bin_sign w)"
2.375 -  by (case_tac w rule: bin_exhaust) auto
2.376 -
2.377 -subsection {* Truncating binary integers *}
2.378 +  by (cases w rule: bin_exhaust) auto
2.379
2.380  consts
2.381    bintrunc :: "nat => int => int"
2.382 @@ -718,18 +894,14 @@
2.383
2.384  subsection {* Splitting and concatenation *}
2.385
2.386 -consts
2.387 -  bin_split :: "nat => int => int * int"
2.388 -primrec
2.389 -  Z : "bin_split 0 w = (w, Int.Pls)"
2.390 -  Suc : "bin_split (Suc n) w = (let (w1, w2) = bin_split n (bin_rest w)
2.391 -    in (w1, w2 BIT bin_last w))"
2.392 +primrec bin_split :: "nat \<Rightarrow> int \<Rightarrow> int \<times> int" where
2.393 +  Z: "bin_split 0 w = (w, Int.Pls)"
2.394 +  | Suc: "bin_split (Suc n) w = (let (w1, w2) = bin_split n (bin_rest w)
2.395 +        in (w1, w2 BIT bin_last w))"
2.396
2.397 -consts
2.398 -  bin_cat :: "int => nat => int => int"
2.399 -primrec
2.400 -  Z : "bin_cat w 0 v = w"
2.401 -  Suc : "bin_cat w (Suc n) v = bin_cat w n (bin_rest v) BIT bin_last v"
2.402 +primrec bin_cat :: "int \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int" where
2.403 +  Z: "bin_cat w 0 v = w"
2.404 +  | Suc: "bin_cat w (Suc n) v = bin_cat w n (bin_rest v) BIT bin_last v"
2.405
2.406  subsection {* Miscellaneous lemmas *}
2.407
```