src/HOL/NatBin.thy
changeset 25919 8b1c0d434824
parent 25571 c9e39eafc7a0
child 25965 05df64f786a4
     1.1 --- a/src/HOL/NatBin.thy	Tue Jan 15 16:19:21 2008 +0100
     1.2 +++ b/src/HOL/NatBin.thy	Tue Jan 15 16:19:23 2008 +0100
     1.3 @@ -120,14 +120,14 @@
     1.4  
     1.5  lemma Suc_nat_number_of_add:
     1.6       "Suc (number_of v + n) =  
     1.7 -        (if neg (number_of v :: int) then 1+n else number_of (Numeral.succ v) + n)" 
     1.8 +        (if neg (number_of v :: int) then 1+n else number_of (Int.succ v) + n)" 
     1.9  by (simp del: nat_number_of 
    1.10           add: nat_number_of_def neg_nat
    1.11                Suc_nat_eq_nat_zadd1 number_of_succ) 
    1.12  
    1.13  lemma Suc_nat_number_of [simp]:
    1.14       "Suc (number_of v) =  
    1.15 -        (if neg (number_of v :: int) then 1 else number_of (Numeral.succ v))"
    1.16 +        (if neg (number_of v :: int) then 1 else number_of (Int.succ v))"
    1.17  apply (cut_tac n = 0 in Suc_nat_number_of_add)
    1.18  apply (simp cong del: if_weak_cong)
    1.19  done
    1.20 @@ -470,7 +470,7 @@
    1.21  
    1.22  lemma eq_number_of_Suc [simp]:
    1.23       "(number_of v = Suc n) =  
    1.24 -        (let pv = number_of (Numeral.pred v) in  
    1.25 +        (let pv = number_of (Int.pred v) in  
    1.26           if neg pv then False else nat pv = n)"
    1.27  apply (simp only: simp_thms Let_def neg_eq_less_0 linorder_not_less 
    1.28                    number_of_pred nat_number_of_def 
    1.29 @@ -481,13 +481,13 @@
    1.30  
    1.31  lemma Suc_eq_number_of [simp]:
    1.32       "(Suc n = number_of v) =  
    1.33 -        (let pv = number_of (Numeral.pred v) in  
    1.34 +        (let pv = number_of (Int.pred v) in  
    1.35           if neg pv then False else nat pv = n)"
    1.36  by (rule trans [OF eq_sym_conv eq_number_of_Suc])
    1.37  
    1.38  lemma less_number_of_Suc [simp]:
    1.39       "(number_of v < Suc n) =  
    1.40 -        (let pv = number_of (Numeral.pred v) in  
    1.41 +        (let pv = number_of (Int.pred v) in  
    1.42           if neg pv then True else nat pv < n)"
    1.43  apply (simp only: simp_thms Let_def neg_eq_less_0 linorder_not_less 
    1.44                    number_of_pred nat_number_of_def  
    1.45 @@ -498,7 +498,7 @@
    1.46  
    1.47  lemma less_Suc_number_of [simp]:
    1.48       "(Suc n < number_of v) =  
    1.49 -        (let pv = number_of (Numeral.pred v) in  
    1.50 +        (let pv = number_of (Int.pred v) in  
    1.51           if neg pv then False else n < nat pv)"
    1.52  apply (simp only: simp_thms Let_def neg_eq_less_0 linorder_not_less 
    1.53                    number_of_pred nat_number_of_def
    1.54 @@ -509,13 +509,13 @@
    1.55  
    1.56  lemma le_number_of_Suc [simp]:
    1.57       "(number_of v <= Suc n) =  
    1.58 -        (let pv = number_of (Numeral.pred v) in  
    1.59 +        (let pv = number_of (Int.pred v) in  
    1.60           if neg pv then True else nat pv <= n)"
    1.61  by (simp add: Let_def less_Suc_number_of linorder_not_less [symmetric])
    1.62  
    1.63  lemma le_Suc_number_of [simp]:
    1.64       "(Suc n <= number_of v) =  
    1.65 -        (let pv = number_of (Numeral.pred v) in  
    1.66 +        (let pv = number_of (Int.pred v) in  
    1.67           if neg pv then False else n <= nat pv)"
    1.68  by (simp add: Let_def less_number_of_Suc linorder_not_less [symmetric])
    1.69  
    1.70 @@ -550,15 +550,15 @@
    1.71  done
    1.72  
    1.73  lemma eq_number_of_BIT_Min:
    1.74 -     "((number_of (v BIT x) ::int) = number_of Numeral.Min) =  
    1.75 -      (x=bit.B1 & (((number_of v) ::int) = number_of Numeral.Min))"
    1.76 +     "((number_of (v BIT x) ::int) = number_of Int.Min) =  
    1.77 +      (x=bit.B1 & (((number_of v) ::int) = number_of Int.Min))"
    1.78  apply (simp only: simp_thms  add: number_of_BIT number_of_Min eq_commute
    1.79              split add: bit.split cong: imp_cong)
    1.80  apply (rule_tac x = "number_of v" in spec, auto)
    1.81  apply (drule_tac f = "%x. x mod 2" in arg_cong, auto)
    1.82  done
    1.83  
    1.84 -lemma eq_number_of_Pls_Min: "(Numeral0 ::int) ~= number_of Numeral.Min"
    1.85 +lemma eq_number_of_Pls_Min: "(Numeral0 ::int) ~= number_of Int.Min"
    1.86  by auto
    1.87  
    1.88  
    1.89 @@ -567,7 +567,7 @@
    1.90  
    1.91  lemma max_number_of_Suc [simp]:
    1.92       "max (Suc n) (number_of v) =  
    1.93 -        (let pv = number_of (Numeral.pred v) in  
    1.94 +        (let pv = number_of (Int.pred v) in  
    1.95           if neg pv then Suc n else Suc(max n (nat pv)))"
    1.96  apply (simp only: Let_def neg_eq_less_0 number_of_pred nat_number_of_def 
    1.97              split add: split_if nat.split)
    1.98 @@ -577,7 +577,7 @@
    1.99   
   1.100  lemma max_Suc_number_of [simp]:
   1.101       "max (number_of v) (Suc n) =  
   1.102 -        (let pv = number_of (Numeral.pred v) in  
   1.103 +        (let pv = number_of (Int.pred v) in  
   1.104           if neg pv then Suc n else Suc(max (nat pv) n))"
   1.105  apply (simp only: Let_def neg_eq_less_0 number_of_pred nat_number_of_def 
   1.106              split add: split_if nat.split)
   1.107 @@ -587,7 +587,7 @@
   1.108   
   1.109  lemma min_number_of_Suc [simp]:
   1.110       "min (Suc n) (number_of v) =  
   1.111 -        (let pv = number_of (Numeral.pred v) in  
   1.112 +        (let pv = number_of (Int.pred v) in  
   1.113           if neg pv then 0 else Suc(min n (nat pv)))"
   1.114  apply (simp only: Let_def neg_eq_less_0 number_of_pred nat_number_of_def 
   1.115              split add: split_if nat.split)
   1.116 @@ -597,7 +597,7 @@
   1.117   
   1.118  lemma min_Suc_number_of [simp]:
   1.119       "min (number_of v) (Suc n) =  
   1.120 -        (let pv = number_of (Numeral.pred v) in  
   1.121 +        (let pv = number_of (Int.pred v) in  
   1.122           if neg pv then 0 else Suc(min (nat pv) n))"
   1.123  apply (simp only: Let_def neg_eq_less_0 number_of_pred nat_number_of_def 
   1.124              split add: split_if nat.split)
   1.125 @@ -681,7 +681,7 @@
   1.126  lemma nat_number_of_Pls: "Numeral0 = (0::nat)"
   1.127    by (simp add: number_of_Pls nat_number_of_def)
   1.128  
   1.129 -lemma nat_number_of_Min: "number_of Numeral.Min = (0::nat)"
   1.130 +lemma nat_number_of_Min: "number_of Int.Min = (0::nat)"
   1.131    apply (simp only: number_of_Min nat_number_of_def nat_zminus_int)
   1.132    done
   1.133