src/HOL/Real/RealDef.thy
changeset 19765 dfe940911617
parent 19023 5652a536b7e8
child 20217 25b068a99d2b
     1.1 --- a/src/HOL/Real/RealDef.thy	Fri Jun 02 20:12:59 2006 +0200
     1.2 +++ b/src/HOL/Real/RealDef.thy	Fri Jun 02 23:22:29 2006 +0200
     1.3 @@ -13,22 +13,21 @@
     1.4  uses ("real_arith.ML")
     1.5  begin
     1.6  
     1.7 -constdefs
     1.8 +definition
     1.9    realrel   ::  "((preal * preal) * (preal * preal)) set"
    1.10 -  "realrel == {p. \<exists>x1 y1 x2 y2. p = ((x1,y1),(x2,y2)) & x1+y2 = x2+y1}"
    1.11 +  "realrel = {p. \<exists>x1 y1 x2 y2. p = ((x1,y1),(x2,y2)) & x1+y2 = x2+y1}"
    1.12  
    1.13  typedef (Real)  real = "UNIV//realrel"
    1.14    by (auto simp add: quotient_def)
    1.15  
    1.16  instance real :: "{ord, zero, one, plus, times, minus, inverse}" ..
    1.17  
    1.18 -constdefs
    1.19 +definition
    1.20  
    1.21    (** these don't use the overloaded "real" function: users don't see them **)
    1.22  
    1.23    real_of_preal :: "preal => real"
    1.24 -  "real_of_preal m     ==
    1.25 -           Abs_Real(realrel``{(m + preal_of_rat 1, preal_of_rat 1)})"
    1.26 +  "real_of_preal m = Abs_Real(realrel``{(m + preal_of_rat 1, preal_of_rat 1)})"
    1.27  
    1.28  consts
    1.29     (*Overloaded constant denoting the Real subset of enclosing
    1.30 @@ -38,8 +37,8 @@
    1.31     (*overloaded constant for injecting other types into "real"*)
    1.32     real :: "'a => real"
    1.33  
    1.34 -syntax (xsymbols)
    1.35 -  Reals     :: "'a set"                   ("\<real>")
    1.36 +const_syntax (xsymbols)
    1.37 +  Reals  ("\<real>")
    1.38  
    1.39  
    1.40  defs (overloaded)
    1.41 @@ -1018,7 +1017,6 @@
    1.42  lemma abs_le_interval_iff: "(abs x \<le> r) = (-r\<le>x & x\<le>(r::real))"
    1.43  by (force simp add: OrderedGroup.abs_le_iff)
    1.44  
    1.45 -(*FIXME: used only once, in SEQ.ML*)
    1.46  lemma abs_add_one_gt_zero [simp]: "(0::real) < 1 + abs(x)"
    1.47  by (simp add: abs_if)
    1.48  
    1.49 @@ -1030,7 +1028,6 @@
    1.50  apply (auto intro: abs_ge_self [THEN order_trans])
    1.51  done
    1.52   
    1.53 -text{*Used only in Hyperreal/Lim.ML*}
    1.54  lemma abs_sum_triangle_ineq: "abs ((x::real) + y + (-l + -m)) \<le> abs(x + -l) + abs(y + -m)"
    1.55  apply (simp add: real_add_assoc)
    1.56  apply (rule_tac a1 = y in add_left_commute [THEN ssubst])
    1.57 @@ -1038,19 +1035,4 @@
    1.58  apply (rule abs_triangle_ineq)
    1.59  done
    1.60  
    1.61 -
    1.62 -ML
    1.63 -{*
    1.64 -val real_lbound_gt_zero = thm"real_lbound_gt_zero";
    1.65 -val real_less_half_sum = thm"real_less_half_sum";
    1.66 -val real_gt_half_sum = thm"real_gt_half_sum";
    1.67 -
    1.68 -val abs_interval_iff = thm"abs_interval_iff";
    1.69 -val abs_le_interval_iff = thm"abs_le_interval_iff";
    1.70 -val abs_add_one_gt_zero = thm"abs_add_one_gt_zero";
    1.71 -val abs_add_one_not_less_self = thm"abs_add_one_not_less_self";
    1.72 -val abs_sum_triangle_ineq = thm"abs_sum_triangle_ineq";
    1.73 -*}
    1.74 -
    1.75 -
    1.76  end