src/HOL/Real/RealBin.ML
author wenzelm
Mon, 08 May 2000 20:57:02 +0200
changeset 8838 4eaa99f0d223
parent 8552 8c4ff19a7286
child 9013 9dd0274f76af
permissions -rw-r--r--
replaced rabs by overloaded abs;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
7292
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
     1
(*  Title:      HOL/RealBin.ML
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
     2
    ID:         $Id$
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
     4
    Copyright   1999  University of Cambridge
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
     5
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
     6
Binary arithmetic for the reals (integer literals only)
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
     7
*)
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
     8
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
     9
(** real_of_int (coercion from int to real) **)
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
    10
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
    11
Goal "real_of_int (number_of w) = number_of w";
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
    12
by (simp_tac (simpset() addsimps [real_number_of_def]) 1);
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
    13
qed "real_number_of";
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
    14
Addsimps [real_number_of];
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
    15
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
    16
Goalw [real_number_of_def] "0r = #0";
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
    17
by (simp_tac (simpset() addsimps [real_of_int_zero RS sym]) 1);
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
    18
qed "zero_eq_numeral_0";
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
    19
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
    20
Goalw [real_number_of_def] "1r = #1";
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
    21
by (simp_tac (simpset() addsimps [real_of_int_one RS sym]) 1);
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
    22
qed "one_eq_numeral_1";
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
    23
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
    24
(** Addition **)
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
    25
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
    26
Goal "(number_of v :: real) + number_of v' = number_of (bin_add v v')";
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
    27
by (simp_tac
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
    28
    (simpset_of Int.thy addsimps [real_number_of_def, 
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
    29
				  real_of_int_add, number_of_add]) 1);
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
    30
qed "add_real_number_of";
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
    31
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
    32
Addsimps [add_real_number_of];
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
    33
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
    34
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
    35
(** Subtraction **)
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
    36
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
    37
Goalw [real_number_of_def] "- (number_of w :: real) = number_of (bin_minus w)";
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
    38
by (simp_tac
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
    39
    (simpset_of Int.thy addsimps [number_of_minus, real_of_int_minus]) 1);
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
    40
qed "minus_real_number_of";
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
    41
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
    42
Goalw [real_number_of_def]
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
    43
   "(number_of v :: real) - number_of w = number_of (bin_add v (bin_minus w))";
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
    44
by (simp_tac
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
    45
    (simpset_of Int.thy addsimps [diff_number_of_eq, real_of_int_diff]) 1);
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
    46
qed "diff_real_number_of";
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
    47
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
    48
Addsimps [minus_real_number_of, diff_real_number_of];
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
    49
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
    50
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
    51
(** Multiplication **)
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
    52
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
    53
Goal "(number_of v :: real) * number_of v' = number_of (bin_mult v v')";
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
    54
by (simp_tac
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
    55
    (simpset_of Int.thy addsimps [real_number_of_def, 
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
    56
				  real_of_int_mult, number_of_mult]) 1);
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
    57
qed "mult_real_number_of";
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
    58
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
    59
Addsimps [mult_real_number_of];
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
    60
7588
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or
paulson
parents: 7583
diff changeset
    61
Goal "(#2::real) = #1 + #1";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or
paulson
parents: 7583
diff changeset
    62
by (Simp_tac 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or
paulson
parents: 7583
diff changeset
    63
val lemma = result();
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or
paulson
parents: 7583
diff changeset
    64
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or
paulson
parents: 7583
diff changeset
    65
(*For specialist use: NOT as default simprules*)
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or
paulson
parents: 7583
diff changeset
    66
Goal "#2 * z = (z+z::real)";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or
paulson
parents: 7583
diff changeset
    67
by (simp_tac (simpset_of RealDef.thy
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or
paulson
parents: 7583
diff changeset
    68
	      addsimps [lemma, real_add_mult_distrib,
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or
paulson
parents: 7583
diff changeset
    69
			one_eq_numeral_1 RS sym]) 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or
paulson
parents: 7583
diff changeset
    70
qed "real_mult_2";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or
paulson
parents: 7583
diff changeset
    71
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or
paulson
parents: 7583
diff changeset
    72
Goal "z * #2 = (z+z::real)";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or
paulson
parents: 7583
diff changeset
    73
by (stac real_mult_commute 1 THEN rtac real_mult_2 1);
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or
paulson
parents: 7583
diff changeset
    74
qed "real_mult_2_right";
26384af93359 Tidying to exploit the new arith_tac. RealBin no longer imports RealPow or
paulson
parents: 7583
diff changeset
    75
7292
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
    76
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
    77
(*** Comparisons ***)
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
    78
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
    79
(** Equals (=) **)
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
    80
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
    81
Goal "((number_of v :: real) = number_of v') = \
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
    82
\     iszero (number_of (bin_add v (bin_minus v')))";
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
    83
by (simp_tac
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
    84
    (simpset_of Int.thy addsimps [real_number_of_def, 
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
    85
				  real_of_int_eq_iff, eq_number_of_eq]) 1);
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
    86
qed "eq_real_number_of";
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
    87
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
    88
Addsimps [eq_real_number_of];
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
    89
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
    90
(** Less-than (<) **)
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
    91
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
    92
(*"neg" is used in rewrite rules for binary comparisons*)
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
    93
Goal "((number_of v :: real) < number_of v') = \
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
    94
\     neg (number_of (bin_add v (bin_minus v')))";
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
    95
by (simp_tac
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
    96
    (simpset_of Int.thy addsimps [real_number_of_def, real_of_int_less_iff, 
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
    97
				  less_number_of_eq_neg]) 1);
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
    98
qed "less_real_number_of";
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
    99
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
   100
Addsimps [less_real_number_of];
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
   101
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
   102
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
   103
(** Less-than-or-equals (<=) **)
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
   104
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
   105
Goal "(number_of x <= (number_of y::real)) = \
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
   106
\     (~ number_of y < (number_of x::real))";
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
   107
by (rtac (linorder_not_less RS sym) 1);
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
   108
qed "le_real_number_of_eq_not_less"; 
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
   109
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
   110
Addsimps [le_real_number_of_eq_not_less];
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
   111
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
   112
8838
4eaa99f0d223 replaced rabs by overloaded abs;
wenzelm
parents: 8552
diff changeset
   113
(** abs (absolute value) **)
7292
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
   114
8838
4eaa99f0d223 replaced rabs by overloaded abs;
wenzelm
parents: 8552
diff changeset
   115
Goalw [abs_real_def]
4eaa99f0d223 replaced rabs by overloaded abs;
wenzelm
parents: 8552
diff changeset
   116
     "abs (number_of v :: real) = \
7292
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
   117
\       (if neg (number_of v) then number_of (bin_minus v) \
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
   118
\        else number_of v)";
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
   119
by (simp_tac
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
   120
    (simpset_of Int.thy addsimps
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
   121
      bin_arith_simps@
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
   122
      [minus_real_number_of, zero_eq_numeral_0, le_real_number_of_eq_not_less,
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
   123
       less_real_number_of, real_of_int_le_iff]) 1);
8838
4eaa99f0d223 replaced rabs by overloaded abs;
wenzelm
parents: 8552
diff changeset
   124
qed "abs_nat_number_of";
7292
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
   125
8838
4eaa99f0d223 replaced rabs by overloaded abs;
wenzelm
parents: 8552
diff changeset
   126
Addsimps [abs_nat_number_of];
7292
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
   127
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
   128
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
   129
(*** New versions of existing theorems involving 0r, 1r ***)
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
   130
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
   131
Goal "- #1 = (#-1::real)";
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
   132
by (Simp_tac 1);
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
   133
qed "minus_numeral_one";
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
   134
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
   135
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
   136
(*Maps 0r to #0 and 1r to #1 and -1r to #-1*)
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
   137
val real_numeral_ss = 
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
   138
    HOL_ss addsimps [zero_eq_numeral_0, one_eq_numeral_1, 
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
   139
		     minus_numeral_one];
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
   140
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
   141
fun rename_numerals thy th = simplify real_numeral_ss (change_theory thy th);
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
   142
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
   143
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
   144
(*Now insert some identities previously stated for 0r and 1r*)
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
   145
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
   146
(** RealDef & Real **)
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
   147
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
   148
Addsimps (map (rename_numerals thy) 
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
   149
	  [real_minus_zero, real_minus_zero_iff,
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
   150
	   real_add_zero_left, real_add_zero_right, 
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
   151
	   real_diff_0, real_diff_0_right,
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
   152
	   real_mult_0_right, real_mult_0, real_mult_1_right, real_mult_1,
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
   153
	   real_mult_minus_1_right, real_mult_minus_1, real_rinv_1,
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
   154
	   real_minus_zero_less_iff]);
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
   155
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
   156
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
   157
(*Perhaps add some theorems that aren't in the default simpset, as
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
   158
  done in Integ/NatBin.ML*)
dff3470c5c62 real literals using binary arithmetic
paulson
parents:
diff changeset
   159
7583
d1b40e0464b1 Restructured lin.arith.package and fixed a proof in RComplete.
nipkow
parents: 7292
diff changeset
   160
d1b40e0464b1 Restructured lin.arith.package and fixed a proof in RComplete.
nipkow
parents: 7292
diff changeset
   161
(*  Author:     Tobias Nipkow, TU Muenchen
d1b40e0464b1 Restructured lin.arith.package and fixed a proof in RComplete.
nipkow
parents: 7292
diff changeset
   162
    Copyright   1999 TU Muenchen
d1b40e0464b1 Restructured lin.arith.package and fixed a proof in RComplete.
nipkow
parents: 7292
diff changeset
   163
d1b40e0464b1 Restructured lin.arith.package and fixed a proof in RComplete.
nipkow
parents: 7292
diff changeset
   164
Instantiate linear arithmetic decision procedure for the reals.
d1b40e0464b1 Restructured lin.arith.package and fixed a proof in RComplete.
nipkow
parents: 7292
diff changeset
   165
FIXME: multiplication with constants (eg #2 * x) does not work yet.
d1b40e0464b1 Restructured lin.arith.package and fixed a proof in RComplete.
nipkow
parents: 7292
diff changeset
   166
Solution: there should be a simproc for combining coefficients.
d1b40e0464b1 Restructured lin.arith.package and fixed a proof in RComplete.
nipkow
parents: 7292
diff changeset
   167
*)
d1b40e0464b1 Restructured lin.arith.package and fixed a proof in RComplete.
nipkow
parents: 7292
diff changeset
   168
d1b40e0464b1 Restructured lin.arith.package and fixed a proof in RComplete.
nipkow
parents: 7292
diff changeset
   169
let
d1b40e0464b1 Restructured lin.arith.package and fixed a proof in RComplete.
nipkow
parents: 7292
diff changeset
   170
d1b40e0464b1 Restructured lin.arith.package and fixed a proof in RComplete.
nipkow
parents: 7292
diff changeset
   171
(* reduce contradictory <= to False *)
d1b40e0464b1 Restructured lin.arith.package and fixed a proof in RComplete.
nipkow
parents: 7292
diff changeset
   172
val simps = [order_less_irrefl,zero_eq_numeral_0,one_eq_numeral_1,
d1b40e0464b1 Restructured lin.arith.package and fixed a proof in RComplete.
nipkow
parents: 7292
diff changeset
   173
  add_real_number_of,minus_real_number_of,diff_real_number_of,
d1b40e0464b1 Restructured lin.arith.package and fixed a proof in RComplete.
nipkow
parents: 7292
diff changeset
   174
  mult_real_number_of,eq_real_number_of,less_real_number_of,
d1b40e0464b1 Restructured lin.arith.package and fixed a proof in RComplete.
nipkow
parents: 7292
diff changeset
   175
  le_real_number_of_eq_not_less];
d1b40e0464b1 Restructured lin.arith.package and fixed a proof in RComplete.
nipkow
parents: 7292
diff changeset
   176
d1b40e0464b1 Restructured lin.arith.package and fixed a proof in RComplete.
nipkow
parents: 7292
diff changeset
   177
val simprocs = [Real_Cancel.sum_conv, Real_Cancel.rel_conv];
d1b40e0464b1 Restructured lin.arith.package and fixed a proof in RComplete.
nipkow
parents: 7292
diff changeset
   178
d1b40e0464b1 Restructured lin.arith.package and fixed a proof in RComplete.
nipkow
parents: 7292
diff changeset
   179
val add_mono_thms =
d1b40e0464b1 Restructured lin.arith.package and fixed a proof in RComplete.
nipkow
parents: 7292
diff changeset
   180
  map (fn s => prove_goal thy s
d1b40e0464b1 Restructured lin.arith.package and fixed a proof in RComplete.
nipkow
parents: 7292
diff changeset
   181
                 (fn prems => [cut_facts_tac prems 1,
d1b40e0464b1 Restructured lin.arith.package and fixed a proof in RComplete.
nipkow
parents: 7292
diff changeset
   182
                      asm_simp_tac (simpset() addsimps
d1b40e0464b1 Restructured lin.arith.package and fixed a proof in RComplete.
nipkow
parents: 7292
diff changeset
   183
     [real_add_le_mono,real_add_less_mono,
d1b40e0464b1 Restructured lin.arith.package and fixed a proof in RComplete.
nipkow
parents: 7292
diff changeset
   184
      real_add_less_le_mono,real_add_le_less_mono]) 1]))
d1b40e0464b1 Restructured lin.arith.package and fixed a proof in RComplete.
nipkow
parents: 7292
diff changeset
   185
    ["(i <= j) & (k <= l) ==> i + k <= j + (l::real)",
d1b40e0464b1 Restructured lin.arith.package and fixed a proof in RComplete.
nipkow
parents: 7292
diff changeset
   186
     "(i  = j) & (k <= l) ==> i + k <= j + (l::real)",
d1b40e0464b1 Restructured lin.arith.package and fixed a proof in RComplete.
nipkow
parents: 7292
diff changeset
   187
     "(i <= j) & (k  = l) ==> i + k <= j + (l::real)",
d1b40e0464b1 Restructured lin.arith.package and fixed a proof in RComplete.
nipkow
parents: 7292
diff changeset
   188
     "(i  = j) & (k  = l) ==> i + k  = j + (l::real)",
d1b40e0464b1 Restructured lin.arith.package and fixed a proof in RComplete.
nipkow
parents: 7292
diff changeset
   189
     "(i < j) & (k = l)   ==> i + k < j + (l::real)",
d1b40e0464b1 Restructured lin.arith.package and fixed a proof in RComplete.
nipkow
parents: 7292
diff changeset
   190
     "(i = j) & (k < l)   ==> i + k < j + (l::real)",
d1b40e0464b1 Restructured lin.arith.package and fixed a proof in RComplete.
nipkow
parents: 7292
diff changeset
   191
     "(i < j) & (k <= l)  ==> i + k < j + (l::real)",
d1b40e0464b1 Restructured lin.arith.package and fixed a proof in RComplete.
nipkow
parents: 7292
diff changeset
   192
     "(i <= j) & (k < l)  ==> i + k < j + (l::real)",
d1b40e0464b1 Restructured lin.arith.package and fixed a proof in RComplete.
nipkow
parents: 7292
diff changeset
   193
     "(i < j) & (k < l)   ==> i + k < j + (l::real)"];
d1b40e0464b1 Restructured lin.arith.package and fixed a proof in RComplete.
nipkow
parents: 7292
diff changeset
   194
d1b40e0464b1 Restructured lin.arith.package and fixed a proof in RComplete.
nipkow
parents: 7292
diff changeset
   195
in
d1b40e0464b1 Restructured lin.arith.package and fixed a proof in RComplete.
nipkow
parents: 7292
diff changeset
   196
LA_Data_Ref.add_mono_thms := !LA_Data_Ref.add_mono_thms @ add_mono_thms;
d1b40e0464b1 Restructured lin.arith.package and fixed a proof in RComplete.
nipkow
parents: 7292
diff changeset
   197
LA_Data_Ref.ss_ref := !LA_Data_Ref.ss_ref addsimps simps
d1b40e0464b1 Restructured lin.arith.package and fixed a proof in RComplete.
nipkow
parents: 7292
diff changeset
   198
                      addsimprocs simprocs;
d1b40e0464b1 Restructured lin.arith.package and fixed a proof in RComplete.
nipkow
parents: 7292
diff changeset
   199
LA_Data_Ref.discrete := !LA_Data_Ref.discrete @ [("RealDef.real",false)]
d1b40e0464b1 Restructured lin.arith.package and fixed a proof in RComplete.
nipkow
parents: 7292
diff changeset
   200
end;
d1b40e0464b1 Restructured lin.arith.package and fixed a proof in RComplete.
nipkow
parents: 7292
diff changeset
   201
d1b40e0464b1 Restructured lin.arith.package and fixed a proof in RComplete.
nipkow
parents: 7292
diff changeset
   202
let
d1b40e0464b1 Restructured lin.arith.package and fixed a proof in RComplete.
nipkow
parents: 7292
diff changeset
   203
val real_arith_simproc_pats =
d1b40e0464b1 Restructured lin.arith.package and fixed a proof in RComplete.
nipkow
parents: 7292
diff changeset
   204
  map (fn s => Thm.read_cterm (Theory.sign_of thy) (s, HOLogic.boolT))
d1b40e0464b1 Restructured lin.arith.package and fixed a proof in RComplete.
nipkow
parents: 7292
diff changeset
   205
      ["(m::real) < n","(m::real) <= n", "(m::real) = n"];
d1b40e0464b1 Restructured lin.arith.package and fixed a proof in RComplete.
nipkow
parents: 7292
diff changeset
   206
d1b40e0464b1 Restructured lin.arith.package and fixed a proof in RComplete.
nipkow
parents: 7292
diff changeset
   207
val fast_real_arith_simproc = mk_simproc
d1b40e0464b1 Restructured lin.arith.package and fixed a proof in RComplete.
nipkow
parents: 7292
diff changeset
   208
  "fast_real_arith" real_arith_simproc_pats Fast_Arith.lin_arith_prover;
d1b40e0464b1 Restructured lin.arith.package and fixed a proof in RComplete.
nipkow
parents: 7292
diff changeset
   209
in
d1b40e0464b1 Restructured lin.arith.package and fixed a proof in RComplete.
nipkow
parents: 7292
diff changeset
   210
Addsimprocs [fast_real_arith_simproc]
d1b40e0464b1 Restructured lin.arith.package and fixed a proof in RComplete.
nipkow
parents: 7292
diff changeset
   211
end;
d1b40e0464b1 Restructured lin.arith.package and fixed a proof in RComplete.
nipkow
parents: 7292
diff changeset
   212
8838
4eaa99f0d223 replaced rabs by overloaded abs;
wenzelm
parents: 8552
diff changeset
   213
Goalw [abs_real_def]
4eaa99f0d223 replaced rabs by overloaded abs;
wenzelm
parents: 8552
diff changeset
   214
  "P(abs (x::real)) = ((#0 <= x --> P x) & (x < #0 --> P(-x)))";
7583
d1b40e0464b1 Restructured lin.arith.package and fixed a proof in RComplete.
nipkow
parents: 7292
diff changeset
   215
by(auto_tac (claset(), simpset() addsimps [zero_eq_numeral_0]));
8838
4eaa99f0d223 replaced rabs by overloaded abs;
wenzelm
parents: 8552
diff changeset
   216
qed "abs_split";
7583
d1b40e0464b1 Restructured lin.arith.package and fixed a proof in RComplete.
nipkow
parents: 7292
diff changeset
   217
8838
4eaa99f0d223 replaced rabs by overloaded abs;
wenzelm
parents: 8552
diff changeset
   218
arith_tac_split_thms := !arith_tac_split_thms @ [abs_split];
7583
d1b40e0464b1 Restructured lin.arith.package and fixed a proof in RComplete.
nipkow
parents: 7292
diff changeset
   219