more new primrec
authorhaftmann
Fri Apr 04 13:40:24 2008 +0200 (2008-04-04)
changeset 265579e7f95903b24
parent 26556 90b02960c8ce
child 26558 7fcc10088e72
more new primrec
src/HOL/Word/BinBoolList.thy
src/HOL/Word/BinGeneral.thy
     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.197 -          simp add: numeral_simps ring_simps cong add : number_of_False_cong)+
   1.198 +  apply (erule allE, erule xtr8 [rotated],
   1.199 +         simp add: numeral_simps ring_simps cong add : number_of_False_cong)+
   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.176 -  by (cases b, simp add: bin_rec_Bit0, simp add: bin_rec_Bit1)
   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.272 -  "bin_sign Int.Pls = Int.Pls"
   2.273 -  "bin_sign Int.Min = Int.Min"
   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.352 +  by (cases b, simp add: bin_rec_Bit0, simp add: bin_rec_Bit1)
   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.364 +  "bin_sign Int.Pls = Int.Pls"
   2.365 +  "bin_sign Int.Min = Int.Min"
   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