src/HOL/Hyperreal/HyperArith.thy

--- a/src/HOL/Hyperreal/HyperArith.thy	Fri Sep 09 17:47:37 2005 +0200
+++ b/src/HOL/Hyperreal/HyperArith.thy	Fri Sep 09 19:34:22 2005 +0200
@@ -13,63 +13,10 @@
 
 subsection{*Numerals and Arithmetic*}
 
-(*
-instance hypreal :: number ..
-
-defs (overloaded)
-  hypreal_number_of_def: "(number_of w :: hypreal) == of_int (Rep_Bin w)"
-    --{*the type constraint is essential!*}
-
-instance hypreal :: number_ring
-by (intro_classes, simp add: hypreal_number_of_def) 
-*)
-
-text{*Collapse applications of @{term hypreal_of_real} to @{term number_of}*}
-lemma hypreal_number_of [simp]: "hypreal_of_real (number_of w) = number_of w"
-by (simp add: hypreal_of_real_def)
-
-
-
 use "hypreal_arith.ML"
 
 setup hypreal_arith_setup
 
-lemma hypreal_le_add_order: "[| 0 \<le> x; 0 \<le> y |] ==> (0::hypreal) \<le> x + y"
-by arith
-
-
-subsection{*The Function @{term hypreal_of_real}*}
-
-lemma number_of_less_hypreal_of_real_iff [simp]:
-     "(number_of w < hypreal_of_real z) = (number_of w < z)"
-apply (subst hypreal_of_real_less_iff [symmetric])
-apply (simp (no_asm))
-done
-
-lemma number_of_le_hypreal_of_real_iff [simp]:
-     "(number_of w \<le> hypreal_of_real z) = (number_of w \<le> z)"
-apply (subst hypreal_of_real_le_iff [symmetric])
-apply (simp (no_asm))
-done
-
-lemma hypreal_of_real_eq_number_of_iff [simp]:
-     "(hypreal_of_real z = number_of w) = (z = number_of w)"
-apply (subst hypreal_of_real_eq_iff [symmetric])
-apply (simp (no_asm))
-done
-
-lemma hypreal_of_real_less_number_of_iff [simp]:
-     "(hypreal_of_real z < number_of w) = (z < number_of w)"
-apply (subst hypreal_of_real_less_iff [symmetric])
-apply (simp (no_asm))
-done
-
-lemma hypreal_of_real_le_number_of_iff [simp]:
-     "(hypreal_of_real z \<le> number_of w) = (z \<le> number_of w)"
-apply (subst hypreal_of_real_le_iff [symmetric])
-apply (simp (no_asm))
-done
-
 subsection{*Absolute Value Function for the Hyperreals*}
 
 lemma hrabs_add_less:
@@ -89,22 +36,18 @@
 
 lemma hypreal_of_real_hrabs:
     "abs (hypreal_of_real r) = hypreal_of_real (abs r)"
-apply (unfold hypreal_of_real_def)
-apply (auto simp add: hypreal_hrabs)
-done
+by (rule star_of_abs [symmetric])
 
 
 subsection{*Embedding the Naturals into the Hyperreals*}
 
 constdefs
-
   hypreal_of_nat   :: "nat => hypreal"
    "hypreal_of_nat m  == of_nat m"
 
 lemma SNat_eq: "Nats = {n. \<exists>N. n = hypreal_of_nat N}"
 by (force simp add: hypreal_of_nat_def Nats_def) 
 
-
 lemma hypreal_of_nat_add [simp]:
      "hypreal_of_nat (m + n) = hypreal_of_nat m + hypreal_of_nat n"
 by (simp add: hypreal_of_nat_def)
@@ -131,11 +74,10 @@
 done
 
 lemma hypreal_of_nat:
-     "hypreal_of_nat m = Abs_star(starrel``{%n. real m})"
-apply (fold star_n_def star_of_def)
+     "hypreal_of_nat m = star_n (%n. real m)"
+apply (fold star_of_def)
 apply (induct m)
-apply (simp_all add: hypreal_of_nat_def real_of_nat_def
-                     hypreal_add)
+apply (simp_all add: hypreal_of_nat_def real_of_nat_def star_n_add)
 done
 
 lemma hypreal_of_nat_Suc:
@@ -171,8 +113,6 @@
 
 ML
 {*
-val hypreal_le_add_order = thm"hypreal_le_add_order";
-
 val hypreal_of_nat_def = thm"hypreal_of_nat_def";
 
 val hrabs_add_less = thm "hrabs_add_less";