src/HOL/Real/real_arith.ML
author nipkow
Fri Dec 01 19:53:29 2000 +0100 (2000-12-01)
changeset 10574 8f98f0301d67
parent 9436 62bb04ab4b01
child 10693 9e4a0e84d0d6
permissions -rw-r--r--
Linear arithmetic now copes with mixed nat/int formulae.
     1 (*  Title:      HOL/Real/real_arith.ML
     2     ID:         $Id$
     3     Author:     Tobias Nipkow, TU Muenchen
     4     Copyright   1999 TU Muenchen
     5 
     6 Instantiation of the generic linear arithmetic package for type real.
     7 *)
     8 
     9 local
    10 
    11 (* reduce contradictory <= to False *)
    12 val simps = [order_less_irrefl, zero_eq_numeral_0, one_eq_numeral_1,
    13              add_real_number_of, minus_real_number_of, diff_real_number_of,
    14              mult_real_number_of, eq_real_number_of, less_real_number_of,
    15              le_real_number_of_eq_not_less, real_diff_def,
    16              real_minus_add_distrib, real_minus_minus];
    17 
    18 val add_rules =
    19     map rename_numerals
    20         [real_add_zero_left, real_add_zero_right,
    21          real_add_minus, real_add_minus_left,
    22          real_mult_0, real_mult_0_right,
    23          real_mult_1, real_mult_1_right,
    24          real_mult_minus_1, real_mult_minus_1_right];
    25 
    26 val simprocs = [Real_Times_Assoc.conv, Real_Numeral_Simprocs.combine_numerals]@
    27                Real_Numeral_Simprocs.cancel_numerals;
    28 
    29 val mono_ss = simpset() addsimps
    30                 [real_add_le_mono,real_add_less_mono,
    31                  real_add_less_le_mono,real_add_le_less_mono];
    32 
    33 val add_mono_thms_real =
    34   map (fn s => prove_goal (the_context ()) s
    35                  (fn prems => [cut_facts_tac prems 1, asm_simp_tac mono_ss 1]))
    36     ["(i <= j) & (k <= l) ==> i + k <= j + (l::real)",
    37      "(i  = j) & (k <= l) ==> i + k <= j + (l::real)",
    38      "(i <= j) & (k  = l) ==> i + k <= j + (l::real)",
    39      "(i  = j) & (k  = l) ==> i + k  = j + (l::real)",
    40      "(i < j) & (k = l)   ==> i + k < j + (l::real)",
    41      "(i = j) & (k < l)   ==> i + k < j + (l::real)",
    42      "(i < j) & (k <= l)  ==> i + k < j + (l::real)",
    43      "(i <= j) & (k < l)  ==> i + k < j + (l::real)",
    44      "(i < j) & (k < l)   ==> i + k < j + (l::real)"];
    45 
    46 val real_arith_simproc_pats =
    47   map (fn s => Thm.read_cterm (Theory.sign_of (the_context ())) (s, HOLogic.boolT))
    48       ["(m::real) < n","(m::real) <= n", "(m::real) = n"];
    49 
    50 in
    51 
    52 val fast_real_arith_simproc = mk_simproc
    53   "fast_real_arith" real_arith_simproc_pats Fast_Arith.lin_arith_prover;
    54 
    55 val real_arith_setup =
    56  [Fast_Arith.map_data (fn {add_mono_thms, inj_thms, lessD, simpset} =>
    57    {add_mono_thms = add_mono_thms @ add_mono_thms_real,
    58     inj_thms = inj_thms, (*FIXME: add real*)
    59     lessD = lessD,  (*We don't change LA_Data_Ref.lessD because the real ordering is dense!*)
    60     simpset = simpset addsimps simps@add_rules
    61                       addsimprocs simprocs
    62                       addcongs [if_weak_cong]}),
    63   arith_discrete ("RealDef.real",false),
    64   Simplifier.change_simpset_of (op addsimprocs) [fast_real_arith_simproc]];
    65 
    66 end;
    67 
    68 
    69 (* Some test data [omitting examples that assume the ordering to be discrete!]
    70 Goal "!!a::real. [| a <= b; c <= d; x+y<z |] ==> a+c <= b+d";
    71 by (fast_arith_tac 1);
    72 qed "";
    73 
    74 Goal "!!a::real. [| a <= b; b+b <= c |] ==> a+a <= c";
    75 by (fast_arith_tac 1);
    76 qed "";
    77 
    78 Goal "!!a::real. [| a+b <= i+j; a<=b; i<=j |] ==> a+a <= j+j";
    79 by (fast_arith_tac 1);
    80 qed "";
    81 
    82 Goal "!!a::real. a+b+c <= i+j+k & a<=b & b<=c & i<=j & j<=k --> a+a+a <= k+k+k";
    83 by (arith_tac 1);
    84 qed "";
    85 
    86 Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
    87 \     ==> a <= l";
    88 by (fast_arith_tac 1);
    89 qed "";
    90 
    91 Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
    92 \     ==> a+a+a+a <= l+l+l+l";
    93 by (fast_arith_tac 1);
    94 qed "";
    95 
    96 Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
    97 \     ==> a+a+a+a+a <= l+l+l+l+i";
    98 by (fast_arith_tac 1);
    99 qed "";
   100 
   101 Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
   102 \     ==> a+a+a+a+a+a <= l+l+l+l+i+l";
   103 by (fast_arith_tac 1);
   104 qed "";
   105 
   106 Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
   107 \     ==> #6*a <= #5*l+i";
   108 by (fast_arith_tac 1);
   109 qed "";
   110 *)