src/HOL/Hyperreal/HyperArith.thy
changeset 14378 69c4d5997669
parent 14371 c78c7da09519
child 14387 e96d5c42c4b0
     1.1 --- a/src/HOL/Hyperreal/HyperArith.thy	Thu Feb 05 10:45:28 2004 +0100
     1.2 +++ b/src/HOL/Hyperreal/HyperArith.thy	Tue Feb 10 12:02:11 2004 +0100
     1.3 @@ -77,7 +77,7 @@
     1.4  
     1.5  lemma eq_hypreal_number_of [simp]:
     1.6       "((number_of v :: hypreal) = 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  apply (simp only: hypreal_number_of_def hypreal_of_real_eq_iff eq_real_number_of)
    1.10  done
    1.11  
    1.12 @@ -87,7 +87,7 @@
    1.13  (*"neg" is used in rewrite rules for binary comparisons*)
    1.14  lemma less_hypreal_number_of [simp]:
    1.15       "((number_of v :: hypreal) < number_of v') =
    1.16 -      neg (number_of (bin_add v (bin_minus v')))"
    1.17 +      neg (number_of (bin_add v (bin_minus v')) :: int)"
    1.18  by (simp only: hypreal_number_of_def hypreal_of_real_less_iff less_real_number_of)
    1.19  
    1.20  
    1.21 @@ -139,10 +139,6 @@
    1.22  
    1.23  setup hypreal_arith_setup
    1.24  
    1.25 -text{*Used once in NSA*}
    1.26 -lemma hypreal_add_minus_eq_minus: "x + y = (0::hypreal) ==> x = -y"
    1.27 -by arith
    1.28 -
    1.29  lemma hypreal_le_add_order: "[| 0 \<le> x; 0 \<le> y |] ==> (0::hypreal) \<le> x + y"
    1.30  by arith
    1.31  
    1.32 @@ -192,7 +188,7 @@
    1.33  
    1.34  lemma hrabs_number_of [simp]:
    1.35       "abs (number_of v :: hypreal) =
    1.36 -        (if neg (number_of v) then number_of (bin_minus v)
    1.37 +        (if neg (number_of v :: int) then number_of (bin_minus v)
    1.38           else number_of v)"
    1.39  by (simp add: hrabs_def)
    1.40  
    1.41 @@ -229,8 +225,11 @@
    1.42  
    1.43  constdefs
    1.44  
    1.45 -  hypreal_of_nat :: "nat => hypreal"
    1.46 -  "hypreal_of_nat (n::nat) == hypreal_of_real (real n)"
    1.47 +  hypreal_of_nat   :: "nat => hypreal"
    1.48 +   "hypreal_of_nat m  == of_nat m"
    1.49 +
    1.50 +lemma SNat_eq: "Nats = {n. \<exists>N. n = hypreal_of_nat N}"
    1.51 +by (force simp add: hypreal_of_nat_def Nats_def) 
    1.52  
    1.53  
    1.54  lemma hypreal_of_nat_add [simp]:
    1.55 @@ -252,46 +251,42 @@
    1.56  (* is a hyperreal c.f. NS extension                           *)
    1.57  (*------------------------------------------------------------*)
    1.58  
    1.59 -lemma hypreal_of_nat_iff:
    1.60 -     "hypreal_of_nat  m = Abs_hypreal(hyprel``{%n. real m})"
    1.61 -by (simp add: hypreal_of_nat_def hypreal_of_real_def real_of_nat_def)
    1.62 +lemma hypreal_of_nat_eq:
    1.63 +     "hypreal_of_nat (n::nat) = hypreal_of_real (real n)"
    1.64 +apply (induct n) 
    1.65 +apply (simp_all add: hypreal_of_nat_def real_of_nat_def)
    1.66 +done
    1.67  
    1.68 -lemma inj_hypreal_of_nat: "inj hypreal_of_nat"
    1.69 -by (simp add: inj_on_def hypreal_of_nat_def)
    1.70 +lemma hypreal_of_nat:
    1.71 +     "hypreal_of_nat m = Abs_hypreal(hyprel``{%n. real m})"
    1.72 +apply (induct m) 
    1.73 +apply (simp_all add: hypreal_of_nat_def real_of_nat_def hypreal_zero_def 
    1.74 +                     hypreal_one_def hypreal_add)
    1.75 +done
    1.76  
    1.77  lemma hypreal_of_nat_Suc:
    1.78       "hypreal_of_nat (Suc n) = hypreal_of_nat n + (1::hypreal)"
    1.79 -by (simp add: hypreal_of_nat_def real_of_nat_Suc)
    1.80 +by (simp add: hypreal_of_nat_def)
    1.81  
    1.82  (*"neg" is used in rewrite rules for binary comparisons*)
    1.83  lemma hypreal_of_nat_number_of [simp]:
    1.84       "hypreal_of_nat (number_of v :: nat) =
    1.85 -         (if neg (number_of v) then 0
    1.86 +         (if neg (number_of v :: int) then 0
    1.87            else (number_of v :: hypreal))"
    1.88 -by (simp add: hypreal_of_nat_def)
    1.89 +by (simp add: hypreal_of_nat_eq)
    1.90  
    1.91  lemma hypreal_of_nat_zero [simp]: "hypreal_of_nat 0 = 0"
    1.92 -by (simp del: numeral_0_eq_0 add: numeral_0_eq_0 [symmetric])
    1.93 +by (simp add: hypreal_of_nat_def) 
    1.94  
    1.95  lemma hypreal_of_nat_one [simp]: "hypreal_of_nat 1 = 1"
    1.96 -by (simp add: hypreal_of_nat_Suc)
    1.97 -
    1.98 -lemma hypreal_of_nat: "hypreal_of_nat m = Abs_hypreal(hyprel `` {%n. real m})"
    1.99 -apply (induct_tac "m")
   1.100 -apply (auto simp add: hypreal_zero_def hypreal_of_nat_Suc hypreal_zero_num hypreal_one_num hypreal_add real_of_nat_Suc)
   1.101 -done
   1.102 +by (simp add: hypreal_of_nat_def) 
   1.103  
   1.104 -lemma hypreal_of_nat_le_iff:
   1.105 -      "(hypreal_of_nat n \<le> hypreal_of_nat m) = (n \<le> m)"
   1.106 -apply (auto simp add: linorder_not_less [symmetric])
   1.107 -done
   1.108 -declare hypreal_of_nat_le_iff [simp]
   1.109 +lemma hypreal_of_nat_le_iff [simp]:
   1.110 +     "(hypreal_of_nat n \<le> hypreal_of_nat m) = (n \<le> m)"
   1.111 +by (simp add: hypreal_of_nat_def) 
   1.112  
   1.113 -lemma hypreal_of_nat_ge_zero: "0 \<le> hypreal_of_nat n"
   1.114 -apply (simp (no_asm) add: hypreal_of_nat_zero [symmetric] 
   1.115 -         del: hypreal_of_nat_zero)
   1.116 -done
   1.117 -declare hypreal_of_nat_ge_zero [simp]
   1.118 +lemma hypreal_of_nat_ge_zero [simp]: "0 \<le> hypreal_of_nat n"
   1.119 +by (simp add: hypreal_of_nat_def) 
   1.120  
   1.121  
   1.122  (*
   1.123 @@ -302,7 +297,6 @@
   1.124  
   1.125  ML
   1.126  {*
   1.127 -val hypreal_add_minus_eq_minus = thm "hypreal_add_minus_eq_minus";
   1.128  val hypreal_le_add_order = thm"hypreal_le_add_order";
   1.129  
   1.130  val hypreal_of_nat_def = thm"hypreal_of_nat_def";
   1.131 @@ -316,8 +310,6 @@
   1.132  val hypreal_of_nat_add = thm "hypreal_of_nat_add";
   1.133  val hypreal_of_nat_mult = thm "hypreal_of_nat_mult";
   1.134  val hypreal_of_nat_less_iff = thm "hypreal_of_nat_less_iff";
   1.135 -val hypreal_of_nat_iff = thm "hypreal_of_nat_iff";
   1.136 -val inj_hypreal_of_nat = thm "inj_hypreal_of_nat";
   1.137  val hypreal_of_nat_Suc = thm "hypreal_of_nat_Suc";
   1.138  val hypreal_of_nat_number_of = thm "hypreal_of_nat_number_of";
   1.139  val hypreal_of_nat_zero = thm "hypreal_of_nat_zero";