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"