src/HOL/Real/real_arith0.ML
author wenzelm
Tue Aug 06 11:22:05 2002 +0200 (2002-08-06)
changeset 13462 56610e2ba220
parent 12483 0a01efff43e9
child 13554 4679359bb218
permissions -rw-r--r--
sane interface for simprocs;
     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 add_rules = 
    13     [order_less_irrefl, real_numeral_0_eq_0, real_numeral_1_eq_1,
    14      add_real_number_of, minus_real_number_of, diff_real_number_of,
    15      mult_real_number_of, eq_real_number_of, less_real_number_of,
    16      le_real_number_of_eq_not_less, real_diff_def,
    17      real_minus_add_distrib, real_minus_minus, real_mult_assoc,
    18      real_minus_zero,
    19      real_add_zero_left, real_add_zero_right,
    20      real_add_minus, real_add_minus_left,
    21      real_mult_0, real_mult_0_right,
    22      real_mult_1, real_mult_1_right,
    23      real_mult_minus_eq1, real_mult_minus_eq2];
    24 
    25 val simprocs = [Real_Times_Assoc.conv, Real_Numeral_Simprocs.combine_numerals]@
    26                Real_Numeral_Simprocs.cancel_numerals @
    27                Real_Numeral_Simprocs.eval_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 fun cvar(th,_ $ (_ $ _ $ var)) = cterm_of (#sign(rep_thm th)) var;
    47 
    48 val real_mult_mono_thms =
    49  [(rotate_prems 1 real_mult_less_mono2,
    50    cvar(real_mult_less_mono2, hd(prems_of real_mult_less_mono2))),
    51   (real_mult_le_mono2,
    52    cvar(real_mult_le_mono2, hd(tl(prems_of real_mult_le_mono2))))]
    53 
    54 in
    55 
    56 val fast_real_arith_simproc = Simplifier.simproc (Theory.sign_of (the_context ()))
    57   "fast_real_arith" ["(m::real) < n","(m::real) <= n", "(m::real) = n"]
    58   Fast_Arith.lin_arith_prover;
    59 
    60 val real_arith_setup =
    61  [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset} =>
    62    {add_mono_thms = add_mono_thms @ add_mono_thms_real,
    63     mult_mono_thms = mult_mono_thms @ real_mult_mono_thms,
    64     inj_thms = inj_thms, (*FIXME: add real*)
    65     lessD = lessD,  (*We don't change LA_Data_Ref.lessD because the real ordering is dense!*)
    66     simpset = simpset addsimps add_rules
    67                       addsimprocs simprocs}),
    68   arith_discrete ("RealDef.real",false),
    69   Simplifier.change_simpset_of (op addsimprocs) [fast_real_arith_simproc]];
    70 
    71 (* some thms for injection nat => real:
    72 real_of_nat_zero
    73 ?zero_eq_numeral_0
    74 real_of_nat_add
    75 *)
    76 
    77 end;
    78 
    79 
    80 (* Some test data [omitting examples that assume the ordering to be discrete!]
    81 Goal "!!a::real. [| a <= b; c <= d; x+y<z |] ==> a+c <= b+d";
    82 by (fast_arith_tac 1);
    83 qed "";
    84 
    85 Goal "!!a::real. [| a <= b; b+b <= c |] ==> a+a <= c";
    86 by (fast_arith_tac 1);
    87 qed "";
    88 
    89 Goal "!!a::real. [| a+b <= i+j; a<=b; i<=j |] ==> a+a <= j+j";
    90 by (fast_arith_tac 1);
    91 qed "";
    92 
    93 Goal "!!a::real. a+b+c <= i+j+k & a<=b & b<=c & i<=j & j<=k --> a+a+a <= k+k+k";
    94 by (arith_tac 1);
    95 qed "";
    96 
    97 Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
    98 \     ==> a <= l";
    99 by (fast_arith_tac 1);
   100 qed "";
   101 
   102 Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
   103 \     ==> a+a+a+a <= l+l+l+l";
   104 by (fast_arith_tac 1);
   105 qed "";
   106 
   107 Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
   108 \     ==> a+a+a+a+a <= l+l+l+l+i";
   109 by (fast_arith_tac 1);
   110 qed "";
   111 
   112 Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
   113 \     ==> a+a+a+a+a+a <= l+l+l+l+i+l";
   114 by (fast_arith_tac 1);
   115 qed "";
   116 
   117 Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
   118 \     ==> 6*a <= 5*l+i";
   119 by (fast_arith_tac 1);
   120 qed "";
   121 *)