src/HOL/Integ/Bin.thy
 changeset 14378 69c4d5997669 parent 14365 3d4df8c166ae child 14387 e96d5c42c4b0
```     1.1 --- a/src/HOL/Integ/Bin.thy	Thu Feb 05 10:45:28 2004 +0100
1.2 +++ b/src/HOL/Integ/Bin.thy	Tue Feb 10 12:02:11 2004 +0100
1.3 @@ -8,7 +8,7 @@
1.4
1.5  header{*Arithmetic on Binary Integers*}
1.6
1.7 -theory Bin = Int + Numeral:
1.8 +theory Bin = IntDef + Numeral:
1.9
1.10  text{*The sign @{term Pls} stands for an infinite string of leading Falses.*}
1.11  text{*The sign @{term Min} stands for an infinite string of leading Trues.*}
1.12 @@ -258,7 +258,7 @@
1.13
1.14  lemma eq_number_of_eq:
1.15    "((number_of x::int) = number_of y) =
1.16 -   iszero (number_of (bin_add x (bin_minus y)))"
1.17 +   iszero (number_of (bin_add x (bin_minus y)) :: int)"
1.18  apply (unfold iszero_def)
1.19  apply (simp add: compare_rls number_of_add number_of_minus)
1.20  done
1.21 @@ -272,14 +272,15 @@
1.22  done
1.23
1.24  lemma iszero_number_of_BIT:
1.25 -     "iszero (number_of (w BIT x)) = (~x & iszero (number_of w::int))"
1.26 +     "iszero (number_of (w BIT x)::int) = (~x & iszero (number_of w::int))"
1.27  apply (unfold iszero_def)
1.28  apply (cases "(number_of w)::int" rule: int_cases)
1.29  apply (simp_all (no_asm_simp) add: compare_rls zero_reorient
1.30           zminus_zadd_distrib [symmetric] int_Suc0_eq_1 [symmetric] zadd_int)
1.31  done
1.32
1.33 -lemma iszero_number_of_0: "iszero (number_of (w BIT False)) = iszero (number_of w::int)"
1.34 +lemma iszero_number_of_0:
1.35 +     "iszero (number_of (w BIT False)::int) = iszero (number_of w::int)"
1.36  by (simp only: iszero_number_of_BIT simp_thms)
1.37
1.38  lemma iszero_number_of_1: "~ iszero (number_of (w BIT True)::int)"
1.39 @@ -291,24 +292,23 @@
1.40
1.41  lemma less_number_of_eq_neg:
1.42      "((number_of x::int) < number_of y)
1.43 -     = neg (number_of (bin_add x (bin_minus y)))"
1.44 +     = neg (number_of (bin_add x (bin_minus y)) ::int )"
1.45 +by (simp add: neg_def number_of_add number_of_minus compare_rls)
1.46
1.47 -apply (unfold zless_def zdiff_def)
1.48 -apply (simp add: bin_mult_simps)
1.49 -done
1.50
1.51  (*But if Numeral0 is rewritten to 0 then this rule can't be applied:
1.52    Numeral0 IS (number_of Pls) *)
1.53 -lemma not_neg_number_of_Pls: "~ neg (number_of bin.Pls)"
1.54 -by (simp add: neg_eq_less_0)
1.55 +lemma not_neg_number_of_Pls: "~ neg (number_of bin.Pls ::int)"
1.56 +by (simp add: neg_def)
1.57
1.58 -lemma neg_number_of_Min: "neg (number_of bin.Min)"
1.59 -by (simp add: neg_eq_less_0 int_0_less_1)
1.60 +lemma neg_number_of_Min: "neg (number_of bin.Min ::int)"
1.61 +by (simp add: neg_def int_0_less_1)
1.62
1.63 -lemma neg_number_of_BIT: "neg (number_of (w BIT x)) = neg (number_of w)"
1.64 +lemma neg_number_of_BIT:
1.65 +     "neg (number_of (w BIT x)::int) = neg (number_of w ::int)"
1.66  apply simp
1.67  apply (cases "(number_of w)::int" rule: int_cases)
1.68 -apply (simp_all (no_asm_simp) add: int_Suc0_eq_1 [symmetric] zadd_int neg_eq_less_0 zdiff_def [symmetric] compare_rls)
1.69 +apply (simp_all (no_asm_simp) add: int_Suc0_eq_1 [symmetric] zadd_int neg_def zdiff_def [symmetric] compare_rls)
1.70  done
1.71
1.72
1.73 @@ -326,9 +326,7 @@
1.74  lemma zabs_number_of:
1.75   "abs(number_of x::int) =
1.76    (if number_of x < (0::int) then -number_of x else number_of x)"
1.77 -apply (unfold zabs_def)
1.78 -apply (rule refl)
1.79 -done
1.80 +by (simp add: zabs_def)
1.81
1.82  (*0 and 1 require special rewrites because they aren't numerals*)
1.83  lemma zabs_0: "abs (0::int) = 0"
```