src/HOL/Real/RealArith.thy
changeset 14378 69c4d5997669
parent 14369 c50188fe6366
     1.1 --- a/src/HOL/Real/RealArith.thy	Thu Feb 05 10:45:28 2004 +0100
     1.2 +++ b/src/HOL/Real/RealArith.thy	Tue Feb 10 12:02:11 2004 +0100
     1.3 @@ -62,13 +62,13 @@
     1.4  
     1.5  lemma eq_real_number_of [simp]:
     1.6       "((number_of v :: real) = number_of v') =  
     1.7 -      iszero (number_of (bin_add v (bin_minus v')))"
     1.8 +      iszero (number_of (bin_add v (bin_minus v')) :: int)"
     1.9  by (simp only: real_number_of_def real_of_int_inject eq_number_of_eq)
    1.10  
    1.11  text{*@{term neg} is used in rewrite rules for binary comparisons*}
    1.12  lemma less_real_number_of [simp]:
    1.13       "((number_of v :: real) < number_of v') =  
    1.14 -      neg (number_of (bin_add v (bin_minus v')))"
    1.15 +      neg (number_of (bin_add v (bin_minus v')) :: int)"
    1.16  by (simp only: real_number_of_def real_of_int_less_iff less_number_of_eq_neg)
    1.17  
    1.18  
    1.19 @@ -134,12 +134,12 @@
    1.20  have. *}
    1.21  lemma real_of_nat_number_of [simp]:
    1.22       "real (number_of v :: nat) =  
    1.23 -        (if neg (number_of v) then 0  
    1.24 +        (if neg (number_of v :: int) then 0  
    1.25           else (number_of v :: real))"
    1.26  proof cases
    1.27 -  assume "neg (number_of v)" thus ?thesis by simp
    1.28 +  assume "neg (number_of v :: int)" thus ?thesis by simp
    1.29  next
    1.30 -  assume neg: "~ neg (number_of v)"
    1.31 +  assume neg: "~ neg (number_of v :: int)"
    1.32    thus ?thesis
    1.33      by (simp only: nat_number_of_def real_of_nat_real_of_int [OF neg], simp) 
    1.34  qed
    1.35 @@ -222,7 +222,7 @@
    1.36  
    1.37  lemma abs_nat_number_of [simp]: 
    1.38       "abs (number_of v :: real) =  
    1.39 -        (if neg (number_of v) then number_of (bin_minus v)  
    1.40 +        (if neg (number_of v :: int) then number_of (bin_minus v)  
    1.41           else number_of v)"
    1.42  by (simp add: real_abs_def bin_arith_simps minus_real_number_of
    1.43         less_real_number_of real_of_int_le_iff)