src/HOL/Real/real_arith.ML
author paulson
Sun, 15 Feb 2004 10:46:37 +0100
changeset 14387 e96d5c42c4b0
parent 14369 c50188fe6366
child 14390 55fe71faadda
permissions -rw-r--r--
Polymorphic treatment of binary arithmetic using axclasses
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
14352
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14336
diff changeset
     1
(*  Title:      HOL/Real/real_arith0.ML
9436
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
     3
    Author:     Tobias Nipkow, TU Muenchen
14352
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14336
diff changeset
     4
    Copyright   1999 TU Muenchen
9436
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
     5
14352
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14336
diff changeset
     6
Simprocs for common factor cancellation & Rational coefficient handling
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14336
diff changeset
     7
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14336
diff changeset
     8
Instantiation of the generic linear arithmetic package for type real.
9436
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
     9
*)
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    10
14365
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents: 14356
diff changeset
    11
(*FIXME DELETE*)
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents: 14356
diff changeset
    12
val real_mult_left_mono =
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents: 14356
diff changeset
    13
    read_instantiate_sg(sign_of (the_context())) [("a","?a::real")] mult_left_mono;
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents: 14356
diff changeset
    14
14387
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
    15
val real_abs_def = thm "real_abs_def";
14365
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents: 14356
diff changeset
    16
14387
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
    17
val real_le_def = thm "real_le_def";
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
    18
val real_diff_def = thm "real_diff_def";
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
    19
val real_divide_def = thm "real_divide_def";
14365
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents: 14356
diff changeset
    20
14387
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
    21
val realrel_iff = thm"realrel_iff";
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
    22
val realrel_refl = thm"realrel_refl";
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
    23
val equiv_realrel = thm"equiv_realrel";
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
    24
val equiv_realrel_iff = thm"equiv_realrel_iff";
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
    25
val realrel_in_real = thm"realrel_in_real";
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
    26
val inj_on_Abs_REAL = thm"inj_on_Abs_REAL";
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
    27
val eq_realrelD = thm"eq_realrelD";
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
    28
val inj_Rep_REAL = thm"inj_Rep_REAL";
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
    29
val inj_real_of_preal = thm"inj_real_of_preal";
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
    30
val eq_Abs_REAL = thm"eq_Abs_REAL";
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
    31
val real_minus_congruent = thm"real_minus_congruent";
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
    32
val real_minus = thm"real_minus";
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
    33
val real_add = thm"real_add";
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
    34
val real_add_commute = thm"real_add_commute";
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
    35
val real_add_assoc = thm"real_add_assoc";
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
    36
val real_add_zero_left = thm"real_add_zero_left";
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
    37
val real_add_zero_right = thm"real_add_zero_right";
14365
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents: 14356
diff changeset
    38
14387
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
    39
val real_mult = thm"real_mult";
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
    40
val real_mult_commute = thm"real_mult_commute";
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
    41
val real_mult_assoc = thm"real_mult_assoc";
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
    42
val real_mult_1 = thm"real_mult_1";
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
    43
val real_mult_1_right = thm"real_mult_1_right";
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
    44
val preal_le_linear = thm"preal_le_linear";
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
    45
val real_mult_inverse_left = thm"real_mult_inverse_left";
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
    46
val real_not_refl2 = thm"real_not_refl2";
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
    47
val real_of_preal_add = thm"real_of_preal_add";
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
    48
val real_of_preal_mult = thm"real_of_preal_mult";
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
    49
val real_of_preal_trichotomy = thm"real_of_preal_trichotomy";
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
    50
val real_of_preal_minus_less_zero = thm"real_of_preal_minus_less_zero";
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
    51
val real_of_preal_not_minus_gt_zero = thm"real_of_preal_not_minus_gt_zero";
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
    52
val real_of_preal_zero_less = thm"real_of_preal_zero_less";
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
    53
val real_le_imp_less_or_eq = thm"real_le_imp_less_or_eq";
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
    54
val real_le_refl = thm"real_le_refl";
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
    55
val real_le_linear = thm"real_le_linear";
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
    56
val real_le_trans = thm"real_le_trans";
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
    57
val real_le_anti_sym = thm"real_le_anti_sym";
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
    58
val real_less_le = thm"real_less_le";
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
    59
val real_less_sum_gt_zero = thm"real_less_sum_gt_zero";
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
    60
val real_gt_zero_preal_Ex = thm "real_gt_zero_preal_Ex";
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
    61
val real_gt_preal_preal_Ex = thm "real_gt_preal_preal_Ex";
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
    62
val real_ge_preal_preal_Ex = thm "real_ge_preal_preal_Ex";
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
    63
val real_less_all_preal = thm "real_less_all_preal";
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
    64
val real_less_all_real2 = thm "real_less_all_real2";
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
    65
val real_of_preal_le_iff = thm "real_of_preal_le_iff";
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
    66
val real_mult_order = thm "real_mult_order";
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
    67
val real_zero_less_one = thm "real_zero_less_one";
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
    68
val real_add_less_le_mono = thm "real_add_less_le_mono";
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
    69
val real_add_le_less_mono = thm "real_add_le_less_mono";
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
    70
val real_add_order = thm "real_add_order";
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
    71
val real_le_add_order = thm "real_le_add_order";
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
    72
val real_le_square = thm "real_le_square";
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
    73
val real_mult_less_mono2 = thm "real_mult_less_mono2";
14289
deb8e1e62002 combining Real/{RealArith0,real_arith}.ML
paulson
parents: 14288
diff changeset
    74
14387
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
    75
val real_mult_less_iff1 = thm "real_mult_less_iff1";
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
    76
val real_mult_le_cancel_iff1 = thm "real_mult_le_cancel_iff1";
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
    77
val real_mult_le_cancel_iff2 = thm "real_mult_le_cancel_iff2";
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
    78
val real_mult_less_mono = thm "real_mult_less_mono";
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
    79
val real_mult_less_mono' = thm "real_mult_less_mono'";
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
    80
val real_sum_squares_cancel = thm "real_sum_squares_cancel";
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
    81
val real_sum_squares_cancel2 = thm "real_sum_squares_cancel2";
14289
deb8e1e62002 combining Real/{RealArith0,real_arith}.ML
paulson
parents: 14288
diff changeset
    82
14387
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
    83
val real_mult_left_cancel = thm"real_mult_left_cancel";
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
    84
val real_mult_right_cancel = thm"real_mult_right_cancel";
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
    85
val real_inverse_unique = thm "real_inverse_unique";
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
    86
val real_inverse_gt_one = thm "real_inverse_gt_one";
14289
deb8e1e62002 combining Real/{RealArith0,real_arith}.ML
paulson
parents: 14288
diff changeset
    87
14387
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
    88
val real_of_int_zero = thm"real_of_int_zero";
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
    89
val real_of_one = thm"real_of_one";
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
    90
val real_of_int_add = thm"real_of_int_add";
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
    91
val real_of_int_minus = thm"real_of_int_minus";
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
    92
val real_of_int_diff = thm"real_of_int_diff";
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
    93
val real_of_int_mult = thm"real_of_int_mult";
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
    94
val real_of_int_real_of_nat = thm"real_of_int_real_of_nat";
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
    95
val real_of_int_inject = thm"real_of_int_inject";
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
    96
val real_of_int_less_iff = thm"real_of_int_less_iff";
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
    97
val real_of_int_le_iff = thm"real_of_int_le_iff";
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
    98
val real_of_nat_zero = thm "real_of_nat_zero";
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
    99
val real_of_nat_one = thm "real_of_nat_one";
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
   100
val real_of_nat_add = thm "real_of_nat_add";
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
   101
val real_of_nat_Suc = thm "real_of_nat_Suc";
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
   102
val real_of_nat_less_iff = thm "real_of_nat_less_iff";
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
   103
val real_of_nat_le_iff = thm "real_of_nat_le_iff";
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
   104
val real_of_nat_ge_zero = thm "real_of_nat_ge_zero";
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
   105
val real_of_nat_Suc_gt_zero = thm "real_of_nat_Suc_gt_zero";
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
   106
val real_of_nat_mult = thm "real_of_nat_mult";
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
   107
val real_of_nat_inject = thm "real_of_nat_inject";
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
   108
val real_of_nat_diff = thm "real_of_nat_diff";
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
   109
val real_of_nat_zero_iff = thm "real_of_nat_zero_iff";
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
   110
val real_of_nat_gt_zero_cancel_iff = thm "real_of_nat_gt_zero_cancel_iff";
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
   111
val real_of_nat_le_zero_cancel_iff = thm "real_of_nat_le_zero_cancel_iff";
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
   112
val not_real_of_nat_less_zero = thm "not_real_of_nat_less_zero";
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
   113
val real_of_nat_ge_zero_cancel_iff = thm "real_of_nat_ge_zero_cancel_iff";
14352
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14336
diff changeset
   114
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14336
diff changeset
   115
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14336
diff changeset
   116
(****Instantiation of the generic linear arithmetic package****)
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14336
diff changeset
   117
14289
deb8e1e62002 combining Real/{RealArith0,real_arith}.ML
paulson
parents: 14288
diff changeset
   118
local
deb8e1e62002 combining Real/{RealArith0,real_arith}.ML
paulson
parents: 14288
diff changeset
   119
10693
9e4a0e84d0d6 moved mk_bin from Numerals to HOLogic
nipkow
parents: 10574
diff changeset
   120
fun cvar(th,_ $ (_ $ _ $ var)) = cterm_of (#sign(rep_thm th)) var;
9e4a0e84d0d6 moved mk_bin from Numerals to HOLogic
nipkow
parents: 10574
diff changeset
   121
9e4a0e84d0d6 moved mk_bin from Numerals to HOLogic
nipkow
parents: 10574
diff changeset
   122
val real_mult_mono_thms =
9e4a0e84d0d6 moved mk_bin from Numerals to HOLogic
nipkow
parents: 10574
diff changeset
   123
 [(rotate_prems 1 real_mult_less_mono2,
9e4a0e84d0d6 moved mk_bin from Numerals to HOLogic
nipkow
parents: 10574
diff changeset
   124
   cvar(real_mult_less_mono2, hd(prems_of real_mult_less_mono2))),
14334
6137d24eef79 tweaking of lemmas in RealDef, RealOrd
paulson
parents: 14321
diff changeset
   125
  (real_mult_left_mono,
6137d24eef79 tweaking of lemmas in RealDef, RealOrd
paulson
parents: 14321
diff changeset
   126
   cvar(real_mult_left_mono, hd(tl(prems_of real_mult_left_mono))))]
10693
9e4a0e84d0d6 moved mk_bin from Numerals to HOLogic
nipkow
parents: 10574
diff changeset
   127
14369
c50188fe6366 tidying up arithmetic for the hyperreals
paulson
parents: 14368
diff changeset
   128
val simps = [real_of_nat_zero, real_of_nat_Suc, real_of_nat_add, 
c50188fe6366 tidying up arithmetic for the hyperreals
paulson
parents: 14368
diff changeset
   129
       real_of_nat_mult, real_of_int_zero, real_of_one, real_of_int_add RS sym,
c50188fe6366 tidying up arithmetic for the hyperreals
paulson
parents: 14368
diff changeset
   130
       real_of_int_minus RS sym, real_of_int_diff RS sym,
14387
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
   131
       real_of_int_mult RS sym];
14355
67e2e96bfe36 Told linear arithmetic package about injections "real" from nat/int into real.
nipkow
parents: 14352
diff changeset
   132
67e2e96bfe36 Told linear arithmetic package about injections "real" from nat/int into real.
nipkow
parents: 14352
diff changeset
   133
val int_inj_thms = [real_of_int_le_iff RS iffD2, real_of_int_less_iff RS iffD2,
67e2e96bfe36 Told linear arithmetic package about injections "real" from nat/int into real.
nipkow
parents: 14352
diff changeset
   134
                    real_of_int_inject RS iffD2];
67e2e96bfe36 Told linear arithmetic package about injections "real" from nat/int into real.
nipkow
parents: 14352
diff changeset
   135
67e2e96bfe36 Told linear arithmetic package about injections "real" from nat/int into real.
nipkow
parents: 14352
diff changeset
   136
val nat_inj_thms = [real_of_nat_le_iff RS iffD2, real_of_nat_less_iff RS iffD2,
67e2e96bfe36 Told linear arithmetic package about injections "real" from nat/int into real.
nipkow
parents: 14352
diff changeset
   137
                    real_of_nat_inject RS iffD2];
14352
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14336
diff changeset
   138
9436
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
   139
in
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
   140
14387
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
   141
val fast_real_arith_simproc =
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
   142
 Simplifier.simproc (Theory.sign_of (the_context ()))
14352
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14336
diff changeset
   143
  "fast_real_arith" ["(m::real) < n","(m::real) <= n", "(m::real) = n"]
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14336
diff changeset
   144
  Fast_Arith.lin_arith_prover;
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14336
diff changeset
   145
9436
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
   146
val real_arith_setup =
10693
9e4a0e84d0d6 moved mk_bin from Numerals to HOLogic
nipkow
parents: 10574
diff changeset
   147
 [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset} =>
14368
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 14365
diff changeset
   148
   {add_mono_thms = add_mono_thms,
10693
9e4a0e84d0d6 moved mk_bin from Numerals to HOLogic
nipkow
parents: 10574
diff changeset
   149
    mult_mono_thms = mult_mono_thms @ real_mult_mono_thms,
14355
67e2e96bfe36 Told linear arithmetic package about injections "real" from nat/int into real.
nipkow
parents: 14352
diff changeset
   150
    inj_thms = int_inj_thms @ nat_inj_thms @ inj_thms,
14365
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents: 14356
diff changeset
   151
    lessD = lessD,  (*Can't change LA_Data_Ref.lessD: the reals are dense!*)
14387
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14369
diff changeset
   152
    simpset = simpset addsimps simps}),
14355
67e2e96bfe36 Told linear arithmetic package about injections "real" from nat/int into real.
nipkow
parents: 14352
diff changeset
   153
  arith_inj_const ("RealDef.real", HOLogic.natT --> HOLogic.realT),
67e2e96bfe36 Told linear arithmetic package about injections "real" from nat/int into real.
nipkow
parents: 14352
diff changeset
   154
  arith_inj_const ("RealDef.real", HOLogic.intT --> HOLogic.realT),
14352
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14336
diff changeset
   155
  arith_discrete ("RealDef.real",false),
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14336
diff changeset
   156
  Simplifier.change_simpset_of (op addsimprocs) [fast_real_arith_simproc]];
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14336
diff changeset
   157
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14336
diff changeset
   158
(* some thms for injection nat => real:
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14336
diff changeset
   159
real_of_nat_zero
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14336
diff changeset
   160
real_of_nat_add
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14336
diff changeset
   161
*)
9436
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
   162
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
   163
end;
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
   164
14352
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14336
diff changeset
   165
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14336
diff changeset
   166
(* Some test data [omitting examples that assume the ordering to be discrete!]
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14336
diff changeset
   167
Goal "!!a::real. [| a <= b; c <= d; x+y<z |] ==> a+c <= b+d";
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14336
diff changeset
   168
by (fast_arith_tac 1);
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14336
diff changeset
   169
qed "";
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14336
diff changeset
   170
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14336
diff changeset
   171
Goal "!!a::real. [| a <= b; b+b <= c |] ==> a+a <= c";
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14336
diff changeset
   172
by (fast_arith_tac 1);
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14336
diff changeset
   173
qed "";
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14336
diff changeset
   174
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14336
diff changeset
   175
Goal "!!a::real. [| a+b <= i+j; a<=b; i<=j |] ==> a+a <= j+j";
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14336
diff changeset
   176
by (fast_arith_tac 1);
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14336
diff changeset
   177
qed "";
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14336
diff changeset
   178
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14336
diff changeset
   179
Goal "!!a::real. a+b+c <= i+j+k & a<=b & b<=c & i<=j & j<=k --> a+a+a <= k+k+k";
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14336
diff changeset
   180
by (arith_tac 1);
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14336
diff changeset
   181
qed "";
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14336
diff changeset
   182
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14336
diff changeset
   183
Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14336
diff changeset
   184
\     ==> a <= l";
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14336
diff changeset
   185
by (fast_arith_tac 1);
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14336
diff changeset
   186
qed "";
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14336
diff changeset
   187
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14336
diff changeset
   188
Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14336
diff changeset
   189
\     ==> a+a+a+a <= l+l+l+l";
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14336
diff changeset
   190
by (fast_arith_tac 1);
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14336
diff changeset
   191
qed "";
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14336
diff changeset
   192
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14336
diff changeset
   193
Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14336
diff changeset
   194
\     ==> a+a+a+a+a <= l+l+l+l+i";
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14336
diff changeset
   195
by (fast_arith_tac 1);
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14336
diff changeset
   196
qed "";
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14336
diff changeset
   197
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14336
diff changeset
   198
Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14336
diff changeset
   199
\     ==> a+a+a+a+a+a <= l+l+l+l+i+l";
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14336
diff changeset
   200
by (fast_arith_tac 1);
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14336
diff changeset
   201
qed "";
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14336
diff changeset
   202
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14336
diff changeset
   203
Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14336
diff changeset
   204
\     ==> 6*a <= 5*l+i";
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14336
diff changeset
   205
by (fast_arith_tac 1);
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14336
diff changeset
   206
qed "";
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14336
diff changeset
   207
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14336
diff changeset
   208
Goal "a<=b ==> a < b+(1::real)";
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14336
diff changeset
   209
by (fast_arith_tac 1);
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14336
diff changeset
   210
qed "";
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14336
diff changeset
   211
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14336
diff changeset
   212
Goal "a<=b ==> a-(3::real) < b";
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14336
diff changeset
   213
by (fast_arith_tac 1);
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14336
diff changeset
   214
qed "";
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14336
diff changeset
   215
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14336
diff changeset
   216
Goal "a<=b ==> a-(1::real) < b";
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14336
diff changeset
   217
by (fast_arith_tac 1);
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14336
diff changeset
   218
qed "";
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14336
diff changeset
   219
9436
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
   220
*)
14352
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14336
diff changeset
   221
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14336
diff changeset
   222
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14336
diff changeset
   223