src/HOL/Real/RealDef.thy
changeset 14341 a09441bd4f1e
parent 14335 9c0b5e081037
child 14348 744c868ee0b7
     1.1 --- a/src/HOL/Real/RealDef.thy	Tue Jan 06 10:38:14 2004 +0100
     1.2 +++ b/src/HOL/Real/RealDef.thy	Tue Jan 06 10:40:15 2004 +0100
     1.3 @@ -330,6 +330,9 @@
     1.4  apply (rule someI2, auto)
     1.5  done
     1.6  
     1.7 +
     1.8 +subsection{*The Real Numbers form a Field*}
     1.9 +
    1.10  instance real :: field
    1.11  proof
    1.12    fix x y z :: real
    1.13 @@ -345,10 +348,13 @@
    1.14    show "0 \<noteq> (1::real)" by (rule real_zero_not_eq_one)
    1.15    show "x \<noteq> 0 ==> inverse x * x = 1" by (rule real_mult_inv_left)
    1.16    show "y \<noteq> 0 ==> x / y = x * inverse y" by (simp add: real_divide_def)
    1.17 +  assume eq: "z+x = z+y" 
    1.18 +    hence "(-z + z) + x = (-z + z) + y" by (simp only: eq real_add_assoc)
    1.19 +    thus "x = y" by (simp add: real_add_minus_left)
    1.20  qed
    1.21  
    1.22  
    1.23 -(** Inverse of zero!  Useful to simplify certain equations **)
    1.24 +text{*Inverse of zero!  Useful to simplify certain equations*}
    1.25  
    1.26  lemma INVERSE_ZERO: "inverse 0 = (0::real)"
    1.27  apply (unfold real_inverse_def)
    1.28 @@ -652,33 +658,6 @@
    1.29  done
    1.30  declare real_minus_zero_less_iff2 [simp]
    1.31  
    1.32 -ML
    1.33 -{*
    1.34 -val real_le_def = thm "real_le_def";
    1.35 -val real_diff_def = thm "real_diff_def";
    1.36 -val real_divide_def = thm "real_divide_def";
    1.37 -val real_of_nat_def = thm "real_of_nat_def";
    1.38 -
    1.39 -val preal_trans_lemma = thm"preal_trans_lemma";
    1.40 -val realrel_iff = thm"realrel_iff";
    1.41 -val realrel_refl = thm"realrel_refl";
    1.42 -val equiv_realrel = thm"equiv_realrel";
    1.43 -val equiv_realrel_iff = thm"equiv_realrel_iff";
    1.44 -val realrel_in_real = thm"realrel_in_real";
    1.45 -val inj_on_Abs_REAL = thm"inj_on_Abs_REAL";
    1.46 -val eq_realrelD = thm"eq_realrelD";
    1.47 -val inj_Rep_REAL = thm"inj_Rep_REAL";
    1.48 -val inj_real_of_preal = thm"inj_real_of_preal";
    1.49 -val eq_Abs_REAL = thm"eq_Abs_REAL";
    1.50 -val real_minus_congruent = thm"real_minus_congruent";
    1.51 -val real_minus = thm"real_minus";
    1.52 -val real_add = thm"real_add";
    1.53 -val real_add_commute = thm"real_add_commute";
    1.54 -val real_add_assoc = thm"real_add_assoc";
    1.55 -val real_add_zero_left = thm"real_add_zero_left";
    1.56 -val real_add_zero_right = thm"real_add_zero_right";
    1.57 -
    1.58 -*}
    1.59  
    1.60  subsection{*Properties of Less-Than Or Equals*}
    1.61  
    1.62 @@ -1068,6 +1047,30 @@
    1.63  {*
    1.64  val real_abs_def = thm "real_abs_def";
    1.65  
    1.66 +val real_le_def = thm "real_le_def";
    1.67 +val real_diff_def = thm "real_diff_def";
    1.68 +val real_divide_def = thm "real_divide_def";
    1.69 +val real_of_nat_def = thm "real_of_nat_def";
    1.70 +
    1.71 +val preal_trans_lemma = thm"preal_trans_lemma";
    1.72 +val realrel_iff = thm"realrel_iff";
    1.73 +val realrel_refl = thm"realrel_refl";
    1.74 +val equiv_realrel = thm"equiv_realrel";
    1.75 +val equiv_realrel_iff = thm"equiv_realrel_iff";
    1.76 +val realrel_in_real = thm"realrel_in_real";
    1.77 +val inj_on_Abs_REAL = thm"inj_on_Abs_REAL";
    1.78 +val eq_realrelD = thm"eq_realrelD";
    1.79 +val inj_Rep_REAL = thm"inj_Rep_REAL";
    1.80 +val inj_real_of_preal = thm"inj_real_of_preal";
    1.81 +val eq_Abs_REAL = thm"eq_Abs_REAL";
    1.82 +val real_minus_congruent = thm"real_minus_congruent";
    1.83 +val real_minus = thm"real_minus";
    1.84 +val real_add = thm"real_add";
    1.85 +val real_add_commute = thm"real_add_commute";
    1.86 +val real_add_assoc = thm"real_add_assoc";
    1.87 +val real_add_zero_left = thm"real_add_zero_left";
    1.88 +val real_add_zero_right = thm"real_add_zero_right";
    1.89 +
    1.90  val real_less_eq_diff = thm "real_less_eq_diff";
    1.91  
    1.92  val real_mult = thm"real_mult";