src/HOL/Real/real_arith.ML
author nipkow
Mon Aug 16 14:22:27 2004 +0200 (2004-08-16)
changeset 15131 c69542757a4d
parent 15003 6145dd7538d7
child 15184 d2c19aea17bc
permissions -rw-r--r--
New theory header syntax.
paulson@14426
     1
(*  Title:      HOL/Real/real_arith.ML
wenzelm@9436
     2
    ID:         $Id$
wenzelm@9436
     3
    Author:     Tobias Nipkow, TU Muenchen
paulson@14352
     4
    Copyright   1999 TU Muenchen
wenzelm@9436
     5
paulson@14352
     6
Simprocs for common factor cancellation & Rational coefficient handling
paulson@14352
     7
paulson@14352
     8
Instantiation of the generic linear arithmetic package for type real.
wenzelm@9436
     9
*)
wenzelm@9436
    10
paulson@14365
    11
(*FIXME DELETE*)
paulson@14365
    12
val real_mult_left_mono =
paulson@14365
    13
    read_instantiate_sg(sign_of (the_context())) [("a","?a::real")] mult_left_mono;
paulson@14365
    14
paulson@14387
    15
val real_le_def = thm "real_le_def";
paulson@14387
    16
val real_diff_def = thm "real_diff_def";
paulson@14387
    17
val real_divide_def = thm "real_divide_def";
paulson@14365
    18
paulson@14387
    19
val realrel_in_real = thm"realrel_in_real";
paulson@14387
    20
val real_add_commute = thm"real_add_commute";
paulson@14387
    21
val real_add_assoc = thm"real_add_assoc";
paulson@14387
    22
val real_add_zero_left = thm"real_add_zero_left";
paulson@14365
    23
paulson@14387
    24
val real_mult_commute = thm"real_mult_commute";
paulson@14387
    25
val real_mult_assoc = thm"real_mult_assoc";
paulson@14387
    26
val real_mult_1 = thm"real_mult_1";
paulson@14387
    27
val real_mult_1_right = thm"real_mult_1_right";
paulson@14387
    28
val preal_le_linear = thm"preal_le_linear";
paulson@14387
    29
val real_mult_inverse_left = thm"real_mult_inverse_left";
paulson@14387
    30
val real_not_refl2 = thm"real_not_refl2";
paulson@14387
    31
val real_of_preal_add = thm"real_of_preal_add";
paulson@14387
    32
val real_of_preal_mult = thm"real_of_preal_mult";
paulson@14387
    33
val real_of_preal_trichotomy = thm"real_of_preal_trichotomy";
paulson@14387
    34
val real_of_preal_minus_less_zero = thm"real_of_preal_minus_less_zero";
paulson@14387
    35
val real_of_preal_not_minus_gt_zero = thm"real_of_preal_not_minus_gt_zero";
paulson@14387
    36
val real_of_preal_zero_less = thm"real_of_preal_zero_less";
paulson@14387
    37
val real_le_imp_less_or_eq = thm"real_le_imp_less_or_eq";
paulson@14387
    38
val real_le_refl = thm"real_le_refl";
paulson@14387
    39
val real_le_linear = thm"real_le_linear";
paulson@14387
    40
val real_le_trans = thm"real_le_trans";
paulson@14387
    41
val real_less_le = thm"real_less_le";
paulson@14387
    42
val real_less_sum_gt_zero = thm"real_less_sum_gt_zero";
paulson@14387
    43
val real_gt_zero_preal_Ex = thm "real_gt_zero_preal_Ex";
paulson@14387
    44
val real_gt_preal_preal_Ex = thm "real_gt_preal_preal_Ex";
paulson@14387
    45
val real_ge_preal_preal_Ex = thm "real_ge_preal_preal_Ex";
paulson@14387
    46
val real_less_all_preal = thm "real_less_all_preal";
paulson@14387
    47
val real_less_all_real2 = thm "real_less_all_real2";
paulson@14387
    48
val real_of_preal_le_iff = thm "real_of_preal_le_iff";
paulson@14387
    49
val real_mult_order = thm "real_mult_order";
paulson@14387
    50
val real_add_less_le_mono = thm "real_add_less_le_mono";
paulson@14387
    51
val real_add_le_less_mono = thm "real_add_le_less_mono";
paulson@14387
    52
val real_add_order = thm "real_add_order";
paulson@14387
    53
val real_le_add_order = thm "real_le_add_order";
paulson@14387
    54
val real_le_square = thm "real_le_square";
paulson@14387
    55
val real_mult_less_mono2 = thm "real_mult_less_mono2";
paulson@14289
    56
paulson@14387
    57
val real_mult_less_iff1 = thm "real_mult_less_iff1";
paulson@14387
    58
val real_mult_le_cancel_iff1 = thm "real_mult_le_cancel_iff1";
paulson@14387
    59
val real_mult_le_cancel_iff2 = thm "real_mult_le_cancel_iff2";
paulson@14387
    60
val real_mult_less_mono = thm "real_mult_less_mono";
paulson@14387
    61
val real_mult_less_mono' = thm "real_mult_less_mono'";
paulson@14387
    62
val real_sum_squares_cancel = thm "real_sum_squares_cancel";
paulson@14387
    63
val real_sum_squares_cancel2 = thm "real_sum_squares_cancel2";
paulson@14289
    64
paulson@14387
    65
val real_mult_left_cancel = thm"real_mult_left_cancel";
paulson@14387
    66
val real_mult_right_cancel = thm"real_mult_right_cancel";
paulson@14387
    67
val real_inverse_unique = thm "real_inverse_unique";
paulson@14387
    68
val real_inverse_gt_one = thm "real_inverse_gt_one";
paulson@14289
    69
paulson@14387
    70
val real_of_int_zero = thm"real_of_int_zero";
paulson@14387
    71
val real_of_one = thm"real_of_one";
paulson@14387
    72
val real_of_int_add = thm"real_of_int_add";
paulson@14387
    73
val real_of_int_minus = thm"real_of_int_minus";
paulson@14387
    74
val real_of_int_diff = thm"real_of_int_diff";
paulson@14387
    75
val real_of_int_mult = thm"real_of_int_mult";
paulson@14387
    76
val real_of_int_real_of_nat = thm"real_of_int_real_of_nat";
paulson@14387
    77
val real_of_int_inject = thm"real_of_int_inject";
paulson@14387
    78
val real_of_int_less_iff = thm"real_of_int_less_iff";
paulson@14387
    79
val real_of_int_le_iff = thm"real_of_int_le_iff";
paulson@14387
    80
val real_of_nat_zero = thm "real_of_nat_zero";
paulson@14387
    81
val real_of_nat_one = thm "real_of_nat_one";
paulson@14387
    82
val real_of_nat_add = thm "real_of_nat_add";
paulson@14387
    83
val real_of_nat_Suc = thm "real_of_nat_Suc";
paulson@14387
    84
val real_of_nat_less_iff = thm "real_of_nat_less_iff";
paulson@14387
    85
val real_of_nat_le_iff = thm "real_of_nat_le_iff";
paulson@14387
    86
val real_of_nat_ge_zero = thm "real_of_nat_ge_zero";
paulson@14387
    87
val real_of_nat_Suc_gt_zero = thm "real_of_nat_Suc_gt_zero";
paulson@14387
    88
val real_of_nat_mult = thm "real_of_nat_mult";
paulson@14387
    89
val real_of_nat_inject = thm "real_of_nat_inject";
paulson@14387
    90
val real_of_nat_diff = thm "real_of_nat_diff";
paulson@14387
    91
val real_of_nat_zero_iff = thm "real_of_nat_zero_iff";
paulson@14387
    92
val real_of_nat_gt_zero_cancel_iff = thm "real_of_nat_gt_zero_cancel_iff";
paulson@14387
    93
val real_of_nat_le_zero_cancel_iff = thm "real_of_nat_le_zero_cancel_iff";
paulson@14387
    94
val not_real_of_nat_less_zero = thm "not_real_of_nat_less_zero";
paulson@14387
    95
val real_of_nat_ge_zero_cancel_iff = thm "real_of_nat_ge_zero_cancel_iff";
paulson@14390
    96
val real_number_of = thm"real_number_of";
paulson@14390
    97
val real_of_nat_number_of = thm"real_of_nat_number_of";
paulson@14426
    98
val real_of_int_of_nat_eq = thm"real_of_int_of_nat_eq";
paulson@14352
    99
paulson@14352
   100
paulson@14352
   101
(****Instantiation of the generic linear arithmetic package****)
paulson@14352
   102
paulson@14289
   103
local
paulson@14289
   104
nipkow@10693
   105
fun cvar(th,_ $ (_ $ _ $ var)) = cterm_of (#sign(rep_thm th)) var;
nipkow@10693
   106
nipkow@10693
   107
val real_mult_mono_thms =
nipkow@10693
   108
 [(rotate_prems 1 real_mult_less_mono2,
nipkow@10693
   109
   cvar(real_mult_less_mono2, hd(prems_of real_mult_less_mono2))),
paulson@14334
   110
  (real_mult_left_mono,
paulson@14334
   111
   cvar(real_mult_left_mono, hd(tl(prems_of real_mult_left_mono))))]
nipkow@10693
   112
paulson@14369
   113
val simps = [real_of_nat_zero, real_of_nat_Suc, real_of_nat_add, 
paulson@14369
   114
       real_of_nat_mult, real_of_int_zero, real_of_one, real_of_int_add RS sym,
paulson@14369
   115
       real_of_int_minus RS sym, real_of_int_diff RS sym,
paulson@14426
   116
       real_of_int_mult RS sym, real_of_int_of_nat_eq,
paulson@14390
   117
       real_of_nat_number_of, real_number_of];
nipkow@14355
   118
nipkow@14355
   119
val int_inj_thms = [real_of_int_le_iff RS iffD2, real_of_int_less_iff RS iffD2,
nipkow@14355
   120
                    real_of_int_inject RS iffD2];
nipkow@14355
   121
nipkow@14355
   122
val nat_inj_thms = [real_of_nat_le_iff RS iffD2, real_of_nat_less_iff RS iffD2,
nipkow@14355
   123
                    real_of_nat_inject RS iffD2];
paulson@14352
   124
wenzelm@9436
   125
in
wenzelm@9436
   126
paulson@14387
   127
val fast_real_arith_simproc =
paulson@14387
   128
 Simplifier.simproc (Theory.sign_of (the_context ()))
paulson@14352
   129
  "fast_real_arith" ["(m::real) < n","(m::real) <= n", "(m::real) = n"]
paulson@14352
   130
  Fast_Arith.lin_arith_prover;
paulson@14352
   131
wenzelm@9436
   132
val real_arith_setup =
nipkow@10693
   133
 [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset} =>
paulson@14368
   134
   {add_mono_thms = add_mono_thms,
nipkow@10693
   135
    mult_mono_thms = mult_mono_thms @ real_mult_mono_thms,
nipkow@14355
   136
    inj_thms = int_inj_thms @ nat_inj_thms @ inj_thms,
paulson@14365
   137
    lessD = lessD,  (*Can't change LA_Data_Ref.lessD: the reals are dense!*)
paulson@14387
   138
    simpset = simpset addsimps simps}),
nipkow@14355
   139
  arith_inj_const ("RealDef.real", HOLogic.natT --> HOLogic.realT),
nipkow@14355
   140
  arith_inj_const ("RealDef.real", HOLogic.intT --> HOLogic.realT),
paulson@14352
   141
  arith_discrete ("RealDef.real",false),
paulson@14352
   142
  Simplifier.change_simpset_of (op addsimprocs) [fast_real_arith_simproc]];
paulson@14352
   143
paulson@14352
   144
(* some thms for injection nat => real:
paulson@14352
   145
real_of_nat_zero
paulson@14352
   146
real_of_nat_add
paulson@14352
   147
*)
wenzelm@9436
   148
wenzelm@9436
   149
end;
wenzelm@9436
   150
paulson@14352
   151
paulson@14352
   152
(* Some test data [omitting examples that assume the ordering to be discrete!]
paulson@14352
   153
Goal "!!a::real. [| a <= b; c <= d; x+y<z |] ==> a+c <= b+d";
paulson@14352
   154
by (fast_arith_tac 1);
paulson@14352
   155
qed "";
paulson@14352
   156
paulson@14352
   157
Goal "!!a::real. [| a <= b; b+b <= c |] ==> a+a <= c";
paulson@14352
   158
by (fast_arith_tac 1);
paulson@14352
   159
qed "";
paulson@14352
   160
paulson@14352
   161
Goal "!!a::real. [| a+b <= i+j; a<=b; i<=j |] ==> a+a <= j+j";
paulson@14352
   162
by (fast_arith_tac 1);
paulson@14352
   163
qed "";
paulson@14352
   164
paulson@14352
   165
Goal "!!a::real. a+b+c <= i+j+k & a<=b & b<=c & i<=j & j<=k --> a+a+a <= k+k+k";
paulson@14352
   166
by (arith_tac 1);
paulson@14352
   167
qed "";
paulson@14352
   168
paulson@14352
   169
Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
paulson@14352
   170
\     ==> a <= l";
paulson@14352
   171
by (fast_arith_tac 1);
paulson@14352
   172
qed "";
paulson@14352
   173
paulson@14352
   174
Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
paulson@14352
   175
\     ==> a+a+a+a <= l+l+l+l";
paulson@14352
   176
by (fast_arith_tac 1);
paulson@14352
   177
qed "";
paulson@14352
   178
paulson@14352
   179
Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
paulson@14352
   180
\     ==> a+a+a+a+a <= l+l+l+l+i";
paulson@14352
   181
by (fast_arith_tac 1);
paulson@14352
   182
qed "";
paulson@14352
   183
paulson@14352
   184
Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
paulson@14352
   185
\     ==> a+a+a+a+a+a <= l+l+l+l+i+l";
paulson@14352
   186
by (fast_arith_tac 1);
paulson@14352
   187
qed "";
paulson@14352
   188
paulson@14352
   189
Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
paulson@14352
   190
\     ==> 6*a <= 5*l+i";
paulson@14352
   191
by (fast_arith_tac 1);
paulson@14352
   192
qed "";
paulson@14352
   193
paulson@14352
   194
Goal "a<=b ==> a < b+(1::real)";
paulson@14352
   195
by (fast_arith_tac 1);
paulson@14352
   196
qed "";
paulson@14352
   197
paulson@14352
   198
Goal "a<=b ==> a-(3::real) < b";
paulson@14352
   199
by (fast_arith_tac 1);
paulson@14352
   200
qed "";
paulson@14352
   201
paulson@14352
   202
Goal "a<=b ==> a-(1::real) < b";
paulson@14352
   203
by (fast_arith_tac 1);
paulson@14352
   204
qed "";
paulson@14352
   205
wenzelm@9436
   206
*)
paulson@14352
   207
paulson@14352
   208
paulson@14352
   209