src/HOL/Real/RealArith0.ML
author wenzelm
Tue Aug 06 11:22:05 2002 +0200 (2002-08-06)
changeset 13462 56610e2ba220
parent 12483 0a01efff43e9
child 13485 acf39e924091
permissions -rw-r--r--
sane interface for simprocs;
     1 (*  Title:      HOL/Real/RealArith.ML
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1999  University of Cambridge
     5 
     6 Assorted facts that need binary literals and the arithmetic decision procedure
     7 
     8 Also, common factor cancellation
     9 *)
    10 
    11 Goal "x - - y = x + (y::real)";
    12 by (Simp_tac 1);
    13 qed "real_diff_minus_eq";
    14 Addsimps [real_diff_minus_eq];
    15 
    16 (** Division and inverse **)
    17 
    18 Goal "0/x = (0::real)";
    19 by (simp_tac (simpset() addsimps [real_divide_def]) 1);
    20 qed "real_0_divide";
    21 Addsimps [real_0_divide];
    22 
    23 Goal "((0::real) < inverse x) = (0 < x)";
    24 by (case_tac "x=0" 1);
    25 by (asm_simp_tac (HOL_ss addsimps [INVERSE_ZERO]) 1);
    26 by (auto_tac (claset() addDs [real_inverse_less_0],
    27               simpset() addsimps [linorder_neq_iff, real_inverse_gt_0]));
    28 qed "real_0_less_inverse_iff";
    29 Addsimps [real_0_less_inverse_iff];
    30 
    31 Goal "(inverse x < (0::real)) = (x < 0)";
    32 by (case_tac "x=0" 1);
    33 by (asm_simp_tac (HOL_ss addsimps [INVERSE_ZERO]) 1);
    34 by (auto_tac (claset() addDs [real_inverse_less_0],
    35               simpset() addsimps [linorder_neq_iff, real_inverse_gt_0]));
    36 qed "real_inverse_less_0_iff";
    37 Addsimps [real_inverse_less_0_iff];
    38 
    39 Goal "((0::real) <= inverse x) = (0 <= x)";
    40 by (simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1);
    41 qed "real_0_le_inverse_iff";
    42 Addsimps [real_0_le_inverse_iff];
    43 
    44 Goal "(inverse x <= (0::real)) = (x <= 0)";
    45 by (simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1);
    46 qed "real_inverse_le_0_iff";
    47 Addsimps [real_inverse_le_0_iff];
    48 
    49 Goalw [real_divide_def] "x/(0::real) = 0";
    50 by (stac INVERSE_ZERO 1);
    51 by (Simp_tac 1);
    52 qed "REAL_DIVIDE_ZERO";
    53 
    54 Goal "inverse (x::real) = 1/x";
    55 by (simp_tac (simpset() addsimps [real_divide_def]) 1);
    56 qed "real_inverse_eq_divide";
    57 
    58 Goal "((0::real) < x/y) = (0 < x & 0 < y | x < 0 & y < 0)";
    59 by (simp_tac (simpset() addsimps [real_divide_def, real_0_less_mult_iff]) 1);
    60 qed "real_0_less_divide_iff";
    61 Addsimps [inst "x" "number_of ?w" real_0_less_divide_iff];
    62 
    63 Goal "(x/y < (0::real)) = (0 < x & y < 0 | x < 0 & 0 < y)";
    64 by (simp_tac (simpset() addsimps [real_divide_def, real_mult_less_0_iff]) 1);
    65 qed "real_divide_less_0_iff";
    66 Addsimps [inst "x" "number_of ?w" real_divide_less_0_iff];
    67 
    68 Goal "((0::real) <= x/y) = ((x <= 0 | 0 <= y) & (0 <= x | y <= 0))";
    69 by (simp_tac (simpset() addsimps [real_divide_def, real_0_le_mult_iff]) 1);
    70 by Auto_tac;
    71 qed "real_0_le_divide_iff";
    72 Addsimps [inst "x" "number_of ?w" real_0_le_divide_iff];
    73 
    74 Goal "(x/y <= (0::real)) = ((x <= 0 | y <= 0) & (0 <= x | 0 <= y))";
    75 by (simp_tac (simpset() addsimps [real_divide_def, real_mult_le_0_iff]) 1);
    76 by Auto_tac;
    77 qed "real_divide_le_0_iff";
    78 Addsimps [inst "x" "number_of ?w" real_divide_le_0_iff];
    79 
    80 Goal "(inverse(x::real) = 0) = (x = 0)";
    81 by (auto_tac (claset(), simpset() addsimps [INVERSE_ZERO]));
    82 by (rtac ccontr 1);
    83 by (blast_tac (claset() addDs [real_inverse_not_zero]) 1);
    84 qed "real_inverse_zero_iff";
    85 Addsimps [real_inverse_zero_iff];
    86 
    87 Goal "(x/y = 0) = (x=0 | y=(0::real))";
    88 by (auto_tac (claset(), simpset() addsimps [real_divide_def]));
    89 qed "real_divide_eq_0_iff";
    90 Addsimps [real_divide_eq_0_iff];
    91 
    92 Goal "h ~= (0::real) ==> h/h = 1";
    93 by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_inv_left]) 1);
    94 qed "real_divide_self_eq";
    95 Addsimps [real_divide_self_eq];
    96 
    97 
    98 (**** Factor cancellation theorems for "real" ****)
    99 
   100 (** Cancellation laws for k*m < k*n and m*k < n*k, also for <= and =,
   101     but not (yet?) for k*m < n*k. **)
   102 (* unused?? bind_thm ("real_mult_minus_right", real_minus_mult_eq2 RS sym); *)
   103 
   104 Goal "(-y < -x) = ((x::real) < y)";
   105 by (arith_tac 1);
   106 qed "real_minus_less_minus";
   107 Addsimps [real_minus_less_minus];
   108 
   109 Goal "[| i<j;  k < (0::real) |] ==> j*k < i*k";
   110 by (rtac (real_minus_less_minus RS iffD1) 1);
   111 by (auto_tac (claset(),
   112               simpset() delsimps [real_mult_minus_eq2]
   113                         addsimps [real_minus_mult_eq2]));
   114 qed "real_mult_less_mono1_neg";
   115 
   116 Goal "[| i<j;  k < (0::real) |] ==> k*j < k*i";
   117 by (rtac (real_minus_less_minus RS iffD1) 1);
   118 by (auto_tac (claset(),
   119               simpset() delsimps [real_mult_minus_eq1]
   120                         addsimps [real_minus_mult_eq1]));
   121 qed "real_mult_less_mono2_neg";
   122 
   123 Goal "[| i <= j;  k <= (0::real) |] ==> j*k <= i*k";
   124 by (auto_tac (claset(),
   125               simpset() addsimps [order_le_less, real_mult_less_mono1_neg]));
   126 qed "real_mult_le_mono1_neg";
   127 
   128 Goal "[| i <= j;  k <= (0::real) |] ==> k*j <= k*i";
   129 by (dtac real_mult_le_mono1_neg 1);
   130 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [real_mult_commute])));
   131 qed "real_mult_le_mono2_neg";
   132 
   133 Goal "(m*k < n*k) = (((0::real) < k & m<n) | (k < 0 & n<m))";
   134 by (case_tac "k = (0::real)" 1);
   135 by (auto_tac (claset(),
   136               simpset() addsimps [linorder_neq_iff,
   137                           real_mult_less_mono1, real_mult_less_mono1_neg]));
   138 by (auto_tac (claset(),
   139               simpset() addsimps [linorder_not_less,
   140                                   inst "y1" "m*k" (linorder_not_le RS sym),
   141                                   inst "y1" "m" (linorder_not_le RS sym)]));
   142 by (TRYALL (etac notE));
   143 by (auto_tac (claset(),
   144               simpset() addsimps [order_less_imp_le, real_mult_le_mono1,
   145                                             real_mult_le_mono1_neg]));
   146 qed "real_mult_less_cancel2";
   147 
   148 Goal "(m*k <= n*k) = (((0::real) < k --> m<=n) & (k < 0 --> n<=m))";
   149 by (simp_tac (simpset() addsimps [linorder_not_less RS sym,
   150                                   real_mult_less_cancel2]) 1);
   151 qed "real_mult_le_cancel2";
   152 
   153 Goal "(k*m < k*n) = (((0::real) < k & m<n) | (k < 0 & n<m))";
   154 by (simp_tac (simpset() addsimps [inst "z" "k" real_mult_commute,
   155                                   real_mult_less_cancel2]) 1);
   156 qed "real_mult_less_cancel1";
   157 
   158 Goal "!!k::real. (k*m <= k*n) = ((0 < k --> m<=n) & (k < 0 --> n<=m))";
   159 by (simp_tac (simpset() addsimps [linorder_not_less RS sym,
   160                                   real_mult_less_cancel1]) 1);
   161 qed "real_mult_le_cancel1";
   162 
   163 Goal "!!k::real. (k*m = k*n) = (k = 0 | m=n)";
   164 by (case_tac "k=0" 1);
   165 by (auto_tac (claset(), simpset() addsimps [real_mult_left_cancel]));
   166 qed "real_mult_eq_cancel1";
   167 
   168 Goal "!!k::real. (m*k = n*k) = (k = 0 | m=n)";
   169 by (case_tac "k=0" 1);
   170 by (auto_tac (claset(), simpset() addsimps [real_mult_right_cancel]));
   171 qed "real_mult_eq_cancel2";
   172 
   173 Goal "!!k::real. k~=0 ==> (k*m) / (k*n) = (m/n)";
   174 by (asm_simp_tac
   175     (simpset() addsimps [real_divide_def, real_inverse_distrib]) 1);
   176 by (subgoal_tac "k * m * (inverse k * inverse n) = \
   177 \                (k * inverse k) * (m * inverse n)" 1);
   178 by (asm_full_simp_tac (simpset() addsimps []) 1);
   179 by (asm_full_simp_tac (HOL_ss addsimps real_mult_ac) 1);
   180 qed "real_mult_div_cancel1";
   181 
   182 (*For ExtractCommonTerm*)
   183 Goal "(k*m) / (k*n) = (if k = (0::real) then 0 else m/n)";
   184 by (simp_tac (simpset() addsimps [real_mult_div_cancel1]) 1);
   185 qed "real_mult_div_cancel_disj";
   186 
   187 
   188 local
   189   open Real_Numeral_Simprocs
   190 in
   191 
   192 val rel_real_number_of = [eq_real_number_of, less_real_number_of,
   193                           le_real_number_of_eq_not_less]
   194 
   195 structure CancelNumeralFactorCommon =
   196   struct
   197   val mk_coeff          = mk_coeff
   198   val dest_coeff        = dest_coeff 1
   199   val trans_tac         = trans_tac
   200   val norm_tac =
   201      ALLGOALS (simp_tac (HOL_ss addsimps real_minus_from_mult_simps @ mult_1s))
   202      THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@real_mult_minus_simps))
   203      THEN ALLGOALS (simp_tac (HOL_ss addsimps real_mult_ac))
   204   val numeral_simp_tac  =
   205          ALLGOALS (simp_tac (HOL_ss addsimps rel_real_number_of@bin_simps))
   206   val simplify_meta_eq  = simplify_meta_eq
   207   end
   208 
   209 structure DivCancelNumeralFactor = CancelNumeralFactorFun
   210  (open CancelNumeralFactorCommon
   211   val prove_conv = prove_conv "realdiv_cancel_numeral_factor"
   212   val mk_bal   = HOLogic.mk_binop "HOL.divide"
   213   val dest_bal = HOLogic.dest_bin "HOL.divide" HOLogic.realT
   214   val cancel = real_mult_div_cancel1 RS trans
   215   val neg_exchanges = false
   216 )
   217 
   218 structure EqCancelNumeralFactor = CancelNumeralFactorFun
   219  (open CancelNumeralFactorCommon
   220   val prove_conv = prove_conv "realeq_cancel_numeral_factor"
   221   val mk_bal   = HOLogic.mk_eq
   222   val dest_bal = HOLogic.dest_bin "op =" HOLogic.realT
   223   val cancel = real_mult_eq_cancel1 RS trans
   224   val neg_exchanges = false
   225 )
   226 
   227 structure LessCancelNumeralFactor = CancelNumeralFactorFun
   228  (open CancelNumeralFactorCommon
   229   val prove_conv = prove_conv "realless_cancel_numeral_factor"
   230   val mk_bal   = HOLogic.mk_binrel "op <"
   231   val dest_bal = HOLogic.dest_bin "op <" HOLogic.realT
   232   val cancel = real_mult_less_cancel1 RS trans
   233   val neg_exchanges = true
   234 )
   235 
   236 structure LeCancelNumeralFactor = CancelNumeralFactorFun
   237  (open CancelNumeralFactorCommon
   238   val prove_conv = prove_conv "realle_cancel_numeral_factor"
   239   val mk_bal   = HOLogic.mk_binrel "op <="
   240   val dest_bal = HOLogic.dest_bin "op <=" HOLogic.realT
   241   val cancel = real_mult_le_cancel1 RS trans
   242   val neg_exchanges = true
   243 )
   244 
   245 val real_cancel_numeral_factors_relations =
   246   map prep_simproc
   247    [("realeq_cancel_numeral_factor",
   248      ["(l::real) * m = n", "(l::real) = m * n"],
   249      EqCancelNumeralFactor.proc),
   250     ("realless_cancel_numeral_factor",
   251      ["(l::real) * m < n", "(l::real) < m * n"],
   252      LessCancelNumeralFactor.proc),
   253     ("realle_cancel_numeral_factor",
   254      ["(l::real) * m <= n", "(l::real) <= m * n"],
   255      LeCancelNumeralFactor.proc)]
   256 
   257 val real_cancel_numeral_factors_divide = prep_simproc
   258         ("realdiv_cancel_numeral_factor",
   259          ["((l::real) * m) / n", "(l::real) / (m * n)",
   260           "((number_of v)::real) / (number_of w)"],
   261          DivCancelNumeralFactor.proc)
   262 
   263 val real_cancel_numeral_factors =
   264     real_cancel_numeral_factors_relations @
   265     [real_cancel_numeral_factors_divide]
   266 
   267 end;
   268 
   269 Addsimprocs real_cancel_numeral_factors;
   270 
   271 
   272 (*examples:
   273 print_depth 22;
   274 set timing;
   275 set trace_simp;
   276 fun test s = (Goal s; by (Simp_tac 1));
   277 
   278 test "0 <= (y::real) * -2";
   279 test "9*x = 12 * (y::real)";
   280 test "(9*x) / (12 * (y::real)) = z";
   281 test "9*x < 12 * (y::real)";
   282 test "9*x <= 12 * (y::real)";
   283 
   284 test "-99*x = 132 * (y::real)";
   285 test "(-99*x) / (132 * (y::real)) = z";
   286 test "-99*x < 132 * (y::real)";
   287 test "-99*x <= 132 * (y::real)";
   288 
   289 test "999*x = -396 * (y::real)";
   290 test "(999*x) / (-396 * (y::real)) = z";
   291 test "999*x < -396 * (y::real)";
   292 test "999*x <= -396 * (y::real)";
   293 
   294 test  "(- ((2::real) * x) <= 2 * y)";
   295 test "-99*x = -81 * (y::real)";
   296 test "(-99*x) / (-81 * (y::real)) = z";
   297 test "-99*x <= -81 * (y::real)";
   298 test "-99*x < -81 * (y::real)";
   299 
   300 test "-2 * x = -1 * (y::real)";
   301 test "-2 * x = -(y::real)";
   302 test "(-2 * x) / (-1 * (y::real)) = z";
   303 test "-2 * x < -(y::real)";
   304 test "-2 * x <= -1 * (y::real)";
   305 test "-x < -23 * (y::real)";
   306 test "-x <= -23 * (y::real)";
   307 *)
   308 
   309 
   310 (** Declarations for ExtractCommonTerm **)
   311 
   312 local
   313   open Real_Numeral_Simprocs
   314 in
   315 
   316 structure CancelFactorCommon =
   317   struct
   318   val mk_sum            = long_mk_prod
   319   val dest_sum          = dest_prod
   320   val mk_coeff          = mk_coeff
   321   val dest_coeff        = dest_coeff
   322   val find_first        = find_first []
   323   val trans_tac         = trans_tac
   324   val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps mult_1s@real_mult_ac))
   325   end;
   326 
   327 structure EqCancelFactor = ExtractCommonTermFun
   328  (open CancelFactorCommon
   329   val prove_conv = prove_conv "real_eq_cancel_factor"
   330   val mk_bal   = HOLogic.mk_eq
   331   val dest_bal = HOLogic.dest_bin "op =" HOLogic.realT
   332   val simplify_meta_eq  = cancel_simplify_meta_eq real_mult_eq_cancel1
   333 );
   334 
   335 
   336 structure DivideCancelFactor = ExtractCommonTermFun
   337  (open CancelFactorCommon
   338   val prove_conv = prove_conv "real_divide_cancel_factor"
   339   val mk_bal   = HOLogic.mk_binop "HOL.divide"
   340   val dest_bal = HOLogic.dest_bin "HOL.divide" HOLogic.realT
   341   val simplify_meta_eq  = cancel_simplify_meta_eq real_mult_div_cancel_disj
   342 );
   343 
   344 val real_cancel_factor =
   345   map prep_simproc
   346    [("real_eq_cancel_factor", ["(l::real) * m = n", "(l::real) = m * n"], EqCancelFactor.proc),
   347     ("real_divide_cancel_factor", ["((l::real) * m) / n", "(l::real) / (m * n)"],
   348      DivideCancelFactor.proc)];
   349 
   350 end;
   351 
   352 Addsimprocs real_cancel_factor;
   353 
   354 
   355 (*examples:
   356 print_depth 22;
   357 set timing;
   358 set trace_simp;
   359 fun test s = (Goal s; by (Asm_simp_tac 1));
   360 
   361 test "x*k = k*(y::real)";
   362 test "k = k*(y::real)";
   363 test "a*(b*c) = (b::real)";
   364 test "a*(b*c) = d*(b::real)*(x*a)";
   365 
   366 
   367 test "(x*k) / (k*(y::real)) = (uu::real)";
   368 test "(k) / (k*(y::real)) = (uu::real)";
   369 test "(a*(b*c)) / ((b::real)) = (uu::real)";
   370 test "(a*(b*c)) / (d*(b::real)*(x*a)) = (uu::real)";
   371 
   372 (*FIXME: what do we do about this?*)
   373 test "a*(b*c)/(y*z) = d*(b::real)*(x*a)/z";
   374 *)
   375 
   376 
   377 (*** Simplification of inequalities involving literal divisors ***)
   378 
   379 Goal "0<z ==> ((x::real) <= y/z) = (x*z <= y)";
   380 by (subgoal_tac "(x*z <= y) = (x*z <= (y/z)*z)" 1);
   381 by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2);
   382 by (etac ssubst 1);
   383 by (stac real_mult_le_cancel2 1);
   384 by (Asm_simp_tac 1);
   385 qed "pos_real_le_divide_eq";
   386 Addsimps [inst "z" "number_of ?w" pos_real_le_divide_eq];
   387 
   388 Goal "z<0 ==> ((x::real) <= y/z) = (y <= x*z)";
   389 by (subgoal_tac "(y <= x*z) = ((y/z)*z <= x*z)" 1);
   390 by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2);
   391 by (etac ssubst 1);
   392 by (stac real_mult_le_cancel2 1);
   393 by (Asm_simp_tac 1);
   394 qed "neg_real_le_divide_eq";
   395 Addsimps [inst "z" "number_of ?w" neg_real_le_divide_eq];
   396 
   397 Goal "0<z ==> (y/z <= (x::real)) = (y <= x*z)";
   398 by (subgoal_tac "(y <= x*z) = ((y/z)*z <= x*z)" 1);
   399 by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2);
   400 by (etac ssubst 1);
   401 by (stac real_mult_le_cancel2 1);
   402 by (Asm_simp_tac 1);
   403 qed "pos_real_divide_le_eq";
   404 Addsimps [inst "z" "number_of ?w" pos_real_divide_le_eq];
   405 
   406 Goal "z<0 ==> (y/z <= (x::real)) = (x*z <= y)";
   407 by (subgoal_tac "(x*z <= y) = (x*z <= (y/z)*z)" 1);
   408 by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2);
   409 by (etac ssubst 1);
   410 by (stac real_mult_le_cancel2 1);
   411 by (Asm_simp_tac 1);
   412 qed "neg_real_divide_le_eq";
   413 Addsimps [inst "z" "number_of ?w" neg_real_divide_le_eq];
   414 
   415 Goal "0<z ==> ((x::real) < y/z) = (x*z < y)";
   416 by (subgoal_tac "(x*z < y) = (x*z < (y/z)*z)" 1);
   417 by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2);
   418 by (etac ssubst 1);
   419 by (stac real_mult_less_cancel2 1);
   420 by (Asm_simp_tac 1);
   421 qed "pos_real_less_divide_eq";
   422 Addsimps [inst "z" "number_of ?w" pos_real_less_divide_eq];
   423 
   424 Goal "z<0 ==> ((x::real) < y/z) = (y < x*z)";
   425 by (subgoal_tac "(y < x*z) = ((y/z)*z < x*z)" 1);
   426 by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2);
   427 by (etac ssubst 1);
   428 by (stac real_mult_less_cancel2 1);
   429 by (Asm_simp_tac 1);
   430 qed "neg_real_less_divide_eq";
   431 Addsimps [inst "z" "number_of ?w" neg_real_less_divide_eq];
   432 
   433 Goal "0<z ==> (y/z < (x::real)) = (y < x*z)";
   434 by (subgoal_tac "(y < x*z) = ((y/z)*z < x*z)" 1);
   435 by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2);
   436 by (etac ssubst 1);
   437 by (stac real_mult_less_cancel2 1);
   438 by (Asm_simp_tac 1);
   439 qed "pos_real_divide_less_eq";
   440 Addsimps [inst "z" "number_of ?w" pos_real_divide_less_eq];
   441 
   442 Goal "z<0 ==> (y/z < (x::real)) = (x*z < y)";
   443 by (subgoal_tac "(x*z < y) = (x*z < (y/z)*z)" 1);
   444 by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2);
   445 by (etac ssubst 1);
   446 by (stac real_mult_less_cancel2 1);
   447 by (Asm_simp_tac 1);
   448 qed "neg_real_divide_less_eq";
   449 Addsimps [inst "z" "number_of ?w" neg_real_divide_less_eq];
   450 
   451 Goal "z~=0 ==> ((x::real) = y/z) = (x*z = y)";
   452 by (subgoal_tac "(x*z = y) = (x*z = (y/z)*z)" 1);
   453 by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2);
   454 by (etac ssubst 1);
   455 by (stac real_mult_eq_cancel2 1);
   456 by (Asm_simp_tac 1);
   457 qed "real_eq_divide_eq";
   458 Addsimps [inst "z" "number_of ?w" real_eq_divide_eq];
   459 
   460 Goal "z~=0 ==> (y/z = (x::real)) = (y = x*z)";
   461 by (subgoal_tac "(y = x*z) = ((y/z)*z = x*z)" 1);
   462 by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2);
   463 by (etac ssubst 1);
   464 by (stac real_mult_eq_cancel2 1);
   465 by (Asm_simp_tac 1);
   466 qed "real_divide_eq_eq";
   467 Addsimps [inst "z" "number_of ?w" real_divide_eq_eq];
   468 
   469 Goal "(m/k = n/k) = (k = 0 | m = (n::real))";
   470 by (case_tac "k=0" 1);
   471 by (asm_simp_tac (simpset() addsimps [REAL_DIVIDE_ZERO]) 1);
   472 by (asm_simp_tac (simpset() addsimps [real_divide_eq_eq, real_eq_divide_eq,
   473                                       real_mult_eq_cancel2]) 1);
   474 qed "real_divide_eq_cancel2";
   475 
   476 Goal "(k/m = k/n) = (k = 0 | m = (n::real))";
   477 by (case_tac "m=0 | n = 0" 1);
   478 by (auto_tac (claset(),
   479               simpset() addsimps [REAL_DIVIDE_ZERO, real_divide_eq_eq,
   480                                   real_eq_divide_eq, real_mult_eq_cancel1]));
   481 qed "real_divide_eq_cancel1";
   482 
   483 (*Moved from RealOrd.ML to use 0 *)
   484 Goal "[| 0 < r; 0 < x|] ==> (inverse x < inverse (r::real)) = (r < x)";
   485 by (auto_tac (claset() addIs [real_inverse_less_swap], simpset()));
   486 by (res_inst_tac [("t","r")] (real_inverse_inverse RS subst) 1);
   487 by (res_inst_tac [("t","x")] (real_inverse_inverse RS subst) 1);
   488 by (auto_tac (claset() addIs [real_inverse_less_swap],
   489               simpset() delsimps [real_inverse_inverse]
   490                         addsimps [real_inverse_gt_0]));
   491 qed "real_inverse_less_iff";
   492 
   493 Goal "[| 0 < r; 0 < x|] ==> (inverse x <= inverse r) = (r <= (x::real))";
   494 by (asm_simp_tac (simpset() addsimps [linorder_not_less RS sym,
   495                                       real_inverse_less_iff]) 1);
   496 qed "real_inverse_le_iff";
   497 
   498 (** Division by 1, -1 **)
   499 
   500 Goal "(x::real)/1 = x";
   501 by (simp_tac (simpset() addsimps [real_divide_def]) 1);
   502 qed "real_divide_1";
   503 Addsimps [real_divide_1];
   504 
   505 Goal "x/-1 = -(x::real)";
   506 by (Simp_tac 1);
   507 qed "real_divide_minus1";
   508 Addsimps [real_divide_minus1];
   509 
   510 Goal "-1/(x::real) = - (1/x)";
   511 by (simp_tac (simpset() addsimps [real_divide_def, real_minus_inverse]) 1);
   512 qed "real_minus1_divide";
   513 Addsimps [real_minus1_divide];
   514 
   515 Goal "[| (0::real) < d1; 0 < d2 |] ==> EX e. 0 < e & e < d1 & e < d2";
   516 by (res_inst_tac [("x","(min d1 d2)/2")] exI 1);
   517 by (asm_simp_tac (simpset() addsimps [min_def]) 1);
   518 qed "real_lbound_gt_zero";
   519 
   520 Goal "(inverse x = inverse y) = (x = (y::real))";
   521 by (case_tac "x=0 | y=0" 1);
   522 by (auto_tac (claset(),
   523               simpset() addsimps [real_inverse_eq_divide,
   524                                   DIVISION_BY_ZERO]));
   525 by (dres_inst_tac [("f","%u. x*y*u")] arg_cong 1);
   526 by (Asm_full_simp_tac 1);
   527 qed "real_inverse_eq_iff";
   528 Addsimps [real_inverse_eq_iff];
   529 
   530 Goal "(z/x = z/y) = (z = 0 | x = (y::real))";
   531 by (case_tac "x=0 | y=0" 1);
   532 by (auto_tac (claset(),
   533               simpset() addsimps [DIVISION_BY_ZERO]));
   534 by (dres_inst_tac [("f","%u. x*y*u")] arg_cong 1);
   535 by Auto_tac;
   536 qed "real_divide_eq_iff";
   537 Addsimps [real_divide_eq_iff];
   538 
   539 
   540 (*** General rewrites to improve automation, like those for type "int" ***)
   541 
   542 (** The next several equations can make the simplifier loop! **)
   543 
   544 Goal "(x < - y) = (y < - (x::real))";
   545 by Auto_tac;
   546 qed "real_less_minus";
   547 
   548 Goal "(- x < y) = (- y < (x::real))";
   549 by Auto_tac;
   550 qed "real_minus_less";
   551 
   552 Goal "(x <= - y) = (y <= - (x::real))";
   553 by Auto_tac;
   554 qed "real_le_minus";
   555 
   556 Goal "(- x <= y) = (- y <= (x::real))";
   557 by Auto_tac;
   558 qed "real_minus_le";
   559 
   560 Goal "(x = - y) = (y = - (x::real))";
   561 by Auto_tac;
   562 qed "real_equation_minus";
   563 
   564 Goal "(- x = y) = (- (y::real) = x)";
   565 by Auto_tac;
   566 qed "real_minus_equation";
   567 
   568 
   569 Goal "(x + - a = (0::real)) = (x=a)";
   570 by (arith_tac 1);
   571 qed "real_add_minus_iff";
   572 Addsimps [real_add_minus_iff];
   573 
   574 Goal "(-b = -a) = (b = (a::real))";
   575 by (arith_tac 1);
   576 qed "real_minus_eq_cancel";
   577 Addsimps [real_minus_eq_cancel];
   578 
   579 
   580 (*Distributive laws for literals*)
   581 Addsimps (map (inst "w" "number_of ?v")
   582           [real_add_mult_distrib, real_add_mult_distrib2,
   583            real_diff_mult_distrib, real_diff_mult_distrib2]);
   584 
   585 Addsimps (map (inst "x" "number_of ?v")
   586           [real_less_minus, real_le_minus, real_equation_minus]);
   587 Addsimps (map (inst "y" "number_of ?v")
   588           [real_minus_less, real_minus_le, real_minus_equation]);
   589 
   590 (*Equations and inequations involving 1*)
   591 Addsimps (map (simplify (simpset()) o inst "x" "1")
   592           [real_less_minus, real_le_minus, real_equation_minus]);
   593 Addsimps (map (simplify (simpset()) o inst "y" "1")
   594           [real_minus_less, real_minus_le, real_minus_equation]);
   595 
   596 (*** Simprules combining x+y and 0 ***)
   597 
   598 Goal "(x+y = (0::real)) = (y = -x)";
   599 by Auto_tac;
   600 qed "real_add_eq_0_iff";
   601 AddIffs [real_add_eq_0_iff];
   602 
   603 Goal "(x+y < (0::real)) = (y < -x)";
   604 by Auto_tac;
   605 qed "real_add_less_0_iff";
   606 AddIffs [real_add_less_0_iff];
   607 
   608 Goal "((0::real) < x+y) = (-x < y)";
   609 by Auto_tac;
   610 qed "real_0_less_add_iff";
   611 AddIffs [real_0_less_add_iff];
   612 
   613 Goal "(x+y <= (0::real)) = (y <= -x)";
   614 by Auto_tac;
   615 qed "real_add_le_0_iff";
   616 AddIffs [real_add_le_0_iff];
   617 
   618 Goal "((0::real) <= x+y) = (-x <= y)";
   619 by Auto_tac;
   620 qed "real_0_le_add_iff";
   621 AddIffs [real_0_le_add_iff];
   622 
   623 
   624 (** Simprules combining x-y and 0; see also real_less_iff_diff_less_0, etc.,
   625     in RealBin
   626 **)
   627 
   628 Goal "((0::real) < x-y) = (y < x)";
   629 by Auto_tac;
   630 qed "real_0_less_diff_iff";
   631 AddIffs [real_0_less_diff_iff];
   632 
   633 Goal "((0::real) <= x-y) = (y <= x)";
   634 by Auto_tac;
   635 qed "real_0_le_diff_iff";
   636 AddIffs [real_0_le_diff_iff];
   637 
   638 (*
   639 FIXME: we should have this, as for type int, but many proofs would break.
   640 It replaces x+-y by x-y.
   641 Addsimps [symmetric real_diff_def];
   642 *)
   643 
   644 Goal "-(x-y) = y - (x::real)";
   645 by (arith_tac 1);
   646 qed "real_minus_diff_eq";
   647 Addsimps [real_minus_diff_eq];
   648 
   649 
   650 (*** Density of the Reals ***)
   651 
   652 Goal "x < y ==> x < (x+y) / (2::real)";
   653 by Auto_tac;
   654 qed "real_less_half_sum";
   655 
   656 Goal "x < y ==> (x+y)/(2::real) < y";
   657 by Auto_tac;
   658 qed "real_gt_half_sum";
   659 
   660 Goal "x < y ==> EX r::real. x < r & r < y";
   661 by (blast_tac (claset() addSIs [real_less_half_sum, real_gt_half_sum]) 1);
   662 qed "real_dense";
   663 
   664 
   665 (*Replaces "inverse #nn" by 1/#nn *)
   666 Addsimps [inst "x" "number_of ?w" real_inverse_eq_divide];
   667 
   668