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