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.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.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.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.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.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