src/HOL/Real/real_arith.ML
changeset 24093 5d0ecd0c8f3c
parent 23081 636cda81978a
child 27545 7165068bb61f
     1.1 --- a/src/HOL/Real/real_arith.ML	Tue Jul 31 19:40:23 2007 +0200
     1.2 +++ b/src/HOL/Real/real_arith.ML	Tue Jul 31 19:40:24 2007 +0200
     1.3 @@ -29,74 +29,14 @@
     1.4  in
     1.5  
     1.6  val real_arith_setup =
     1.7 -  Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
     1.8 +  LinArith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
     1.9     {add_mono_thms = add_mono_thms,
    1.10      mult_mono_thms = mult_mono_thms,
    1.11      inj_thms = int_inj_thms @ nat_inj_thms @ inj_thms,
    1.12 -    lessD = lessD,  (*Can't change LA_Data_Ref.lessD: the reals are dense!*)
    1.13 +    lessD = lessD,  (*Can't change lessD: the reals are dense!*)
    1.14      neqE = neqE,
    1.15      simpset = simpset addsimps simps}) #>
    1.16    arith_inj_const ("RealDef.real", HOLogic.natT --> HOLogic.realT) #>
    1.17    arith_inj_const ("RealDef.real", HOLogic.intT --> HOLogic.realT)
    1.18  
    1.19  end;
    1.20 -
    1.21 -
    1.22 -(* Some test data [omitting examples that assume the ordering to be discrete!]
    1.23 -Goal "!!a::real. [| a <= b; c <= d; x+y<z |] ==> a+c <= b+d";
    1.24 -by (fast_arith_tac 1);
    1.25 -qed "";
    1.26 -
    1.27 -Goal "!!a::real. [| a <= b; b+b <= c |] ==> a+a <= c";
    1.28 -by (fast_arith_tac 1);
    1.29 -qed "";
    1.30 -
    1.31 -Goal "!!a::real. [| a+b <= i+j; a<=b; i<=j |] ==> a+a <= j+j";
    1.32 -by (fast_arith_tac 1);
    1.33 -qed "";
    1.34 -
    1.35 -Goal "!!a::real. a+b+c <= i+j+k & a<=b & b<=c & i<=j & j<=k --> a+a+a <= k+k+k";
    1.36 -by (arith_tac 1);
    1.37 -qed "";
    1.38 -
    1.39 -Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
    1.40 -\     ==> a <= l";
    1.41 -by (fast_arith_tac 1);
    1.42 -qed "";
    1.43 -
    1.44 -Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
    1.45 -\     ==> a+a+a+a <= l+l+l+l";
    1.46 -by (fast_arith_tac 1);
    1.47 -qed "";
    1.48 -
    1.49 -Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
    1.50 -\     ==> a+a+a+a+a <= l+l+l+l+i";
    1.51 -by (fast_arith_tac 1);
    1.52 -qed "";
    1.53 -
    1.54 -Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
    1.55 -\     ==> a+a+a+a+a+a <= l+l+l+l+i+l";
    1.56 -by (fast_arith_tac 1);
    1.57 -qed "";
    1.58 -
    1.59 -Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
    1.60 -\     ==> 6*a <= 5*l+i";
    1.61 -by (fast_arith_tac 1);
    1.62 -qed "";
    1.63 -
    1.64 -Goal "a<=b ==> a < b+(1::real)";
    1.65 -by (fast_arith_tac 1);
    1.66 -qed "";
    1.67 -
    1.68 -Goal "a<=b ==> a-(3::real) < b";
    1.69 -by (fast_arith_tac 1);
    1.70 -qed "";
    1.71 -
    1.72 -Goal "a<=b ==> a-(1::real) < b";
    1.73 -by (fast_arith_tac 1);
    1.74 -qed "";
    1.75 -
    1.76 -*)
    1.77 -
    1.78 -
    1.79 -