wneuper/isa: src/HOL/Hyperreal/HyperArith0.ML@3c50a2cd6f00

     1 (*  Title:      HOL/Hyperreal/HyperRealArith0.ML

     2     ID:         $Id$

     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory

     4     Copyright   1999  University of Cambridge

     6 Assorted facts that need binary literals and the arithmetic decision procedure

     8 Also, common factor cancellation

     9 *)

    11 Goal "((x * y = Numeral0) = (x = Numeral0 | y = (Numeral0::hypreal)))";

    12 by Auto_tac;

    13 by (cut_inst_tac [("x","x"),("y","y")] hypreal_mult_zero_disj 1);

    14 by Auto_tac;

    15 qed "hypreal_mult_is_0";

    16 AddIffs [hypreal_mult_is_0];

    18 (** Division and inverse **)

    20 Goal "Numeral0/x = (Numeral0::hypreal)";

    21 by (simp_tac (simpset() addsimps [hypreal_divide_def]) 1);

    22 qed "hypreal_0_divide";

    23 Addsimps [hypreal_0_divide];

    25 Goal "((Numeral0::hypreal) < inverse x) = (Numeral0 < x)";

    26 by (case_tac "x=Numeral0" 1);

    27 by (asm_simp_tac (HOL_ss addsimps [rename_numerals HYPREAL_INVERSE_ZERO]) 1);

    28 by (auto_tac (claset() addDs [hypreal_inverse_less_0],

    29               simpset() addsimps [linorder_neq_iff,

    30                                   hypreal_inverse_gt_0]));

    31 qed "hypreal_0_less_inverse_iff";

    32 Addsimps [hypreal_0_less_inverse_iff];

    34 Goal "(inverse x < (Numeral0::hypreal)) = (x < Numeral0)";

    35 by (case_tac "x=Numeral0" 1);

    36 by (asm_simp_tac (HOL_ss addsimps [rename_numerals HYPREAL_INVERSE_ZERO]) 1);

    37 by (auto_tac (claset() addDs [hypreal_inverse_less_0],

    38               simpset() addsimps [linorder_neq_iff,

    39                                   hypreal_inverse_gt_0]));

    40 qed "hypreal_inverse_less_0_iff";

    41 Addsimps [hypreal_inverse_less_0_iff];

    43 Goal "((Numeral0::hypreal) <= inverse x) = (Numeral0 <= x)";

    44 by (simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1);

    45 qed "hypreal_0_le_inverse_iff";

    46 Addsimps [hypreal_0_le_inverse_iff];

    48 Goal "(inverse x <= (Numeral0::hypreal)) = (x <= Numeral0)";

    49 by (simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1);

    50 qed "hypreal_inverse_le_0_iff";

    51 Addsimps [hypreal_inverse_le_0_iff];

    53 Goalw [hypreal_divide_def] "x/(Numeral0::hypreal) = Numeral0";

    54 by (stac (rename_numerals HYPREAL_INVERSE_ZERO) 1);

    55 by (Simp_tac 1);

    56 qed "HYPREAL_DIVIDE_ZERO";

    58 Goal "inverse (x::hypreal) = Numeral1/x";

    59 by (simp_tac (simpset() addsimps [hypreal_divide_def]) 1);

    60 qed "hypreal_inverse_eq_divide";

    62 Goal "((Numeral0::hypreal) < x/y) = (Numeral0 < x & Numeral0 < y | x < Numeral0 & y < Numeral0)";

    63 by (simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_0_less_mult_iff]) 1);

    64 qed "hypreal_0_less_divide_iff";

    65 Addsimps [inst "x" "number_of ?w" hypreal_0_less_divide_iff];

    67 Goal "(x/y < (Numeral0::hypreal)) = (Numeral0 < x & y < Numeral0 | x < Numeral0 & Numeral0 < y)";

    68 by (simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_mult_less_0_iff]) 1);

    69 qed "hypreal_divide_less_0_iff";

    70 Addsimps [inst "x" "number_of ?w" hypreal_divide_less_0_iff];

    72 Goal "((Numeral0::hypreal) <= x/y) = ((x <= Numeral0 | Numeral0 <= y) & (Numeral0 <= x | y <= Numeral0))";

    73 by (simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_0_le_mult_iff]) 1);

    74 by Auto_tac;

    75 qed "hypreal_0_le_divide_iff";

    76 Addsimps [inst "x" "number_of ?w" hypreal_0_le_divide_iff];

    78 Goal "(x/y <= (Numeral0::hypreal)) = ((x <= Numeral0 | y <= Numeral0) & (Numeral0 <= x | Numeral0 <= y))";

    79 by (simp_tac (simpset() addsimps [hypreal_divide_def,

    80                                   hypreal_mult_le_0_iff]) 1);

    81 by Auto_tac;

    82 qed "hypreal_divide_le_0_iff";

    83 Addsimps [inst "x" "number_of ?w" hypreal_divide_le_0_iff];

    85 Goal "(inverse(x::hypreal) = Numeral0) = (x = Numeral0)";

    86 by (auto_tac (claset(),

    87               simpset() addsimps [rename_numerals HYPREAL_INVERSE_ZERO]));

    88 by (rtac ccontr 1);

    89 by (blast_tac (claset() addDs [rename_numerals hypreal_inverse_not_zero]) 1);

    90 qed "hypreal_inverse_zero_iff";

    91 Addsimps [hypreal_inverse_zero_iff];

    93 Goal "(x/y = Numeral0) = (x=Numeral0 | y=(Numeral0::hypreal))";

    94 by (auto_tac (claset(), simpset() addsimps [hypreal_divide_def]));

    95 qed "hypreal_divide_eq_0_iff";

    96 Addsimps [hypreal_divide_eq_0_iff];

    98 Goal "h ~= (Numeral0::hypreal) ==> h/h = Numeral1";

    99 by (asm_simp_tac

   100     (simpset() addsimps [hypreal_divide_def, hypreal_mult_inverse_left]) 1);

   101 qed "hypreal_divide_self_eq";

   102 Addsimps [hypreal_divide_self_eq];

   105 (**** Factor cancellation theorems for "hypreal" ****)

   107 (** Cancellation laws for k*m < k*n and m*k < n*k, also for <= and =,

   108     but not (yet?) for k*m < n*k. **)

   110 bind_thm ("hypreal_mult_minus_right", hypreal_minus_mult_eq2 RS sym);

   112 Goal "(-y < -x) = ((x::hypreal) < y)";

   113 by (arith_tac 1);

   114 qed "hypreal_minus_less_minus";

   115 Addsimps [hypreal_minus_less_minus];

   117 Goal "[| i<j;  k < (0::hypreal) |] ==> j*k < i*k";

   118 by (rtac (hypreal_minus_less_minus RS iffD1) 1);

   119 by (auto_tac (claset(),

   120               simpset() delsimps [hypreal_minus_mult_eq2 RS sym]

   121                         addsimps [hypreal_minus_mult_eq2,

   122                                   hypreal_mult_less_mono1]));

   123 qed "hypreal_mult_less_mono1_neg";

   125 Goal "[| i<j;  k < (0::hypreal) |] ==> k*j < k*i";

   126 by (rtac (hypreal_minus_less_minus RS iffD1) 1);

   127 by (auto_tac (claset(),

   128               simpset() delsimps [hypreal_minus_mult_eq1 RS sym]

   129                         addsimps [hypreal_minus_mult_eq1,

   130                                   hypreal_mult_less_mono2]));

   131 qed "hypreal_mult_less_mono2_neg";

   133 Goal "[| i <= j;  k <= (0::hypreal) |] ==> j*k <= i*k";

   134 by (auto_tac (claset(),

   135           simpset() addsimps [order_le_less, hypreal_mult_less_mono1_neg]));

   136 qed "hypreal_mult_le_mono1_neg";

   138 Goal "[| i <= j;  k <= (0::hypreal) |] ==> k*j <= k*i";

   139 by (dtac hypreal_mult_le_mono1_neg 1);

   140 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [hypreal_mult_commute])));

   141 qed "hypreal_mult_le_mono2_neg";

   143 Goal "(m*k < n*k) = (((Numeral0::hypreal) < k & m<n) | (k < Numeral0 & n<m))";

   144 by (case_tac "k = (0::hypreal)" 1);

   145 by (auto_tac (claset(),

   146           simpset() addsimps [linorder_neq_iff,

   147                       hypreal_mult_less_mono1, hypreal_mult_less_mono1_neg]));

   148 by (auto_tac (claset(),

   149               simpset() addsimps [linorder_not_less,

   150 				  inst "y1" "m*k" (linorder_not_le RS sym),

   151                                   inst "y1" "m" (linorder_not_le RS sym)]));

   152 by (TRYALL (etac notE));

   153 by (auto_tac (claset(),

   154               simpset() addsimps [order_less_imp_le, hypreal_mult_le_mono1,

   155                                   hypreal_mult_le_mono1_neg]));

   156 qed "hypreal_mult_less_cancel2";

   158 Goal "(m*k <= n*k) = (((Numeral0::hypreal) < k --> m<=n) & (k < Numeral0 --> n<=m))";

   159 by (simp_tac (simpset() addsimps [linorder_not_less RS sym,

   160                                   hypreal_mult_less_cancel2]) 1);

   161 qed "hypreal_mult_le_cancel2";

   163 Goal "(k*m < k*n) = (((Numeral0::hypreal) < k & m<n) | (k < Numeral0 & n<m))";

   164 by (simp_tac (simpset() addsimps [inst "z" "k" hypreal_mult_commute,

   165                                   hypreal_mult_less_cancel2]) 1);

   166 qed "hypreal_mult_less_cancel1";

   168 Goal "!!k::hypreal. (k*m <= k*n) = ((Numeral0 < k --> m<=n) & (k < Numeral0 --> n<=m))";

   169 by (simp_tac (simpset() addsimps [linorder_not_less RS sym,

   170                                   hypreal_mult_less_cancel1]) 1);

   171 qed "hypreal_mult_le_cancel1";

   173 Goal "!!k::hypreal. (k*m = k*n) = (k = Numeral0 | m=n)";

   174 by (case_tac "k=0" 1);

   175 by (auto_tac (claset(), simpset() addsimps [hypreal_mult_left_cancel]));

   176 qed "hypreal_mult_eq_cancel1";

   178 Goal "!!k::hypreal. (m*k = n*k) = (k = Numeral0 | m=n)";

   179 by (case_tac "k=0" 1);

   180 by (auto_tac (claset(), simpset() addsimps [hypreal_mult_right_cancel]));

   181 qed "hypreal_mult_eq_cancel2";

   183 Goal "!!k::hypreal. k~=Numeral0 ==> (k*m) / (k*n) = (m/n)";

   184 by (asm_simp_tac

   185     (simpset() addsimps [hypreal_divide_def, hypreal_inverse_distrib]) 1);

   186 by (subgoal_tac "k * m * (inverse k * inverse n) = \

   187 \                (k * inverse k) * (m * inverse n)" 1);

   188 by (asm_full_simp_tac (simpset() addsimps []) 1);

   189 by (asm_full_simp_tac (HOL_ss addsimps hypreal_mult_ac) 1);

   190 qed "hypreal_mult_div_cancel1";

   192 (*For ExtractCommonTerm*)

   193 Goal "(k*m) / (k*n) = (if k = (Numeral0::hypreal) then Numeral0 else m/n)";

   194 by (simp_tac (simpset() addsimps [hypreal_mult_div_cancel1]) 1);

   195 qed "hypreal_mult_div_cancel_disj";

   198 local

   199   open Hyperreal_Numeral_Simprocs

   200 in

   202 val rel_hypreal_number_of = [eq_hypreal_number_of, less_hypreal_number_of,

   203                           le_hypreal_number_of_eq_not_less];

   205 structure CancelNumeralFactorCommon =

   206   struct

   207   val mk_coeff		= mk_coeff

   208   val dest_coeff	= dest_coeff 1

   209   val trans_tac         = trans_tac

   210   val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps mult_plus_1s))

   211      THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@hypreal_mult_minus_simps))

   212      THEN ALLGOALS

   213 	  (simp_tac

   214 	   (HOL_ss addsimps [eq_hypreal_number_of, mult_hypreal_number_of,

   215                              hypreal_mult_number_of_left]@

   216            hypreal_minus_from_mult_simps @ hypreal_mult_ac))

   217   val numeral_simp_tac	=

   218          ALLGOALS (simp_tac (HOL_ss addsimps rel_hypreal_number_of@bin_simps))

   219   val simplify_meta_eq  = simplify_meta_eq

   220   end

   222 structure DivCancelNumeralFactor = CancelNumeralFactorFun

   223  (open CancelNumeralFactorCommon

   224   val prove_conv = prove_conv "hyprealdiv_cancel_numeral_factor"

   225   val mk_bal   = HOLogic.mk_binop "HOL.divide"

   226   val dest_bal = HOLogic.dest_bin "HOL.divide" hyprealT

   227   val cancel = hypreal_mult_div_cancel1 RS trans

   228   val neg_exchanges = false

   229 )

   231 structure EqCancelNumeralFactor = CancelNumeralFactorFun

   232  (open CancelNumeralFactorCommon

   233   val prove_conv = prove_conv "hyprealeq_cancel_numeral_factor"

   234   val mk_bal   = HOLogic.mk_eq

   235   val dest_bal = HOLogic.dest_bin "op =" hyprealT

   236   val cancel = hypreal_mult_eq_cancel1 RS trans

   237   val neg_exchanges = false

   238 )

   240 structure LessCancelNumeralFactor = CancelNumeralFactorFun

   241  (open CancelNumeralFactorCommon

   242   val prove_conv = prove_conv "hyprealless_cancel_numeral_factor"

   243   val mk_bal   = HOLogic.mk_binrel "op <"

   244   val dest_bal = HOLogic.dest_bin "op <" hyprealT

   245   val cancel = hypreal_mult_less_cancel1 RS trans

   246   val neg_exchanges = true

   247 )

   249 structure LeCancelNumeralFactor = CancelNumeralFactorFun

   250  (open CancelNumeralFactorCommon

   251   val prove_conv = prove_conv "hyprealle_cancel_numeral_factor"

   252   val mk_bal   = HOLogic.mk_binrel "op <="

   253   val dest_bal = HOLogic.dest_bin "op <=" hyprealT

   254   val cancel = hypreal_mult_le_cancel1 RS trans

   255   val neg_exchanges = true

   256 )

   258 val hypreal_cancel_numeral_factors_relations =

   259   map prep_simproc

   260    [("hyprealeq_cancel_numeral_factor",

   261      prep_pats ["(l::hypreal) * m = n", "(l::hypreal) = m * n"],

   262      EqCancelNumeralFactor.proc),

   263     ("hyprealless_cancel_numeral_factor",

   264      prep_pats ["(l::hypreal) * m < n", "(l::hypreal) < m * n"],

   265      LessCancelNumeralFactor.proc),

   266     ("hyprealle_cancel_numeral_factor",

   267      prep_pats ["(l::hypreal) * m <= n", "(l::hypreal) <= m * n"],

   268      LeCancelNumeralFactor.proc)];

   270 val hypreal_cancel_numeral_factors_divide = prep_simproc

   271 	("hyprealdiv_cancel_numeral_factor",

   272 	 prep_pats ["((l::hypreal) * m) / n", "(l::hypreal) / (m * n)",

   273                      "((number_of v)::hypreal) / (number_of w)"],

   274 	 DivCancelNumeralFactor.proc);

   276 val hypreal_cancel_numeral_factors =

   277     hypreal_cancel_numeral_factors_relations @

   278     [hypreal_cancel_numeral_factors_divide];

   280 end;

   282 Addsimprocs hypreal_cancel_numeral_factors;

   285 (*examples:

   286 print_depth 22;

   287 set timing;

   288 set trace_simp;

   289 fun test s = (Goal s; by (Simp_tac 1));

   291 test "Numeral0 <= (y::hypreal) * -2";

   292 test "9*x = 12 * (y::hypreal)";

   293 test "(9*x) / (12 * (y::hypreal)) = z";

   294 test "9*x < 12 * (y::hypreal)";

   295 test "9*x <= 12 * (y::hypreal)";

   297 test "-99*x = 123 * (y::hypreal)";

   298 test "(-99*x) / (123 * (y::hypreal)) = z";

   299 test "-99*x < 123 * (y::hypreal)";

   300 test "-99*x <= 123 * (y::hypreal)";

   302 test "999*x = -396 * (y::hypreal)";

   303 test "(999*x) / (-396 * (y::hypreal)) = z";

   304 test "999*x < -396 * (y::hypreal)";

   305 test "999*x <= -396 * (y::hypreal)";

   307 test "-99*x = -81 * (y::hypreal)";

   308 test "(-99*x) / (-81 * (y::hypreal)) = z";

   309 test "-99*x <= -81 * (y::hypreal)";

   310 test "-99*x < -81 * (y::hypreal)";

   312 test "-2 * x = -1 * (y::hypreal)";

   313 test "-2 * x = -(y::hypreal)";

   314 test "(-2 * x) / (-1 * (y::hypreal)) = z";

   315 test "-2 * x < -(y::hypreal)";

   316 test "-2 * x <= -1 * (y::hypreal)";

   317 test "-x < -23 * (y::hypreal)";

   318 test "-x <= -23 * (y::hypreal)";

   319 *)

   322 (** Declarations for ExtractCommonTerm **)

   324 local

   325   open Hyperreal_Numeral_Simprocs

   326 in

   328 structure CancelFactorCommon =

   329   struct

   330   val mk_sum    	= long_mk_prod

   331   val dest_sum		= dest_prod

   332   val mk_coeff		= mk_coeff

   333   val dest_coeff	= dest_coeff

   334   val find_first	= find_first []

   335   val trans_tac         = trans_tac

   336   val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps mult_1s@hypreal_mult_ac))

   337   end;

   339 structure EqCancelFactor = ExtractCommonTermFun

   340  (open CancelFactorCommon

   341   val prove_conv = prove_conv "hypreal_eq_cancel_factor"

   342   val mk_bal   = HOLogic.mk_eq

   343   val dest_bal = HOLogic.dest_bin "op =" hyprealT

   344   val simplify_meta_eq  = cancel_simplify_meta_eq hypreal_mult_eq_cancel1

   345 );

   348 structure DivideCancelFactor = ExtractCommonTermFun

   349  (open CancelFactorCommon

   350   val prove_conv = prove_conv "hypreal_divide_cancel_factor"

   351   val mk_bal   = HOLogic.mk_binop "HOL.divide"

   352   val dest_bal = HOLogic.dest_bin "HOL.divide" hyprealT

   353   val simplify_meta_eq  = cancel_simplify_meta_eq hypreal_mult_div_cancel_disj

   354 );

   356 val hypreal_cancel_factor =

   357   map prep_simproc

   358    [("hypreal_eq_cancel_factor",

   359      prep_pats ["(l::hypreal) * m = n", "(l::hypreal) = m * n"],

   360      EqCancelFactor.proc),

   361     ("hypreal_divide_cancel_factor",

   362      prep_pats ["((l::hypreal) * m) / n", "(l::hypreal) / (m * n)"],

   363      DivideCancelFactor.proc)];

   365 end;

   367 Addsimprocs hypreal_cancel_factor;

   370 (*examples:

   371 print_depth 22;

   372 set timing;

   373 set trace_simp;

   374 fun test s = (Goal s; by (Asm_simp_tac 1));

   376 test "x*k = k*(y::hypreal)";

   377 test "k = k*(y::hypreal)";

   378 test "a*(b*c) = (b::hypreal)";

   379 test "a*(b*c) = d*(b::hypreal)*(x*a)";

   382 test "(x*k) / (k*(y::hypreal)) = (uu::hypreal)";

   383 test "(k) / (k*(y::hypreal)) = (uu::hypreal)";

   384 test "(a*(b*c)) / ((b::hypreal)) = (uu::hypreal)";

   385 test "(a*(b*c)) / (d*(b::hypreal)*(x*a)) = (uu::hypreal)";

   387 (*FIXME: what do we do about this?*)

   388 test "a*(b*c)/(y*z) = d*(b::hypreal)*(x*a)/z";

   389 *)

   392 (*** Simplification of inequalities involving literal divisors ***)

   394 Goal "Numeral0<z ==> ((x::hypreal) <= y/z) = (x*z <= y)";

   395 by (subgoal_tac "(x*z <= y) = (x*z <= (y/z)*z)" 1);

   396 by (asm_simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_mult_assoc]) 2);

   397 by (etac ssubst 1);

   398 by (stac hypreal_mult_le_cancel2 1);

   399 by (Asm_simp_tac 1);

   400 qed "pos_hypreal_le_divide_eq";

   401 Addsimps [inst "z" "number_of ?w" pos_hypreal_le_divide_eq];

   403 Goal "z<Numeral0 ==> ((x::hypreal) <= y/z) = (y <= x*z)";

   404 by (subgoal_tac "(y <= x*z) = ((y/z)*z <= x*z)" 1);

   405 by (asm_simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_mult_assoc]) 2);

   406 by (etac ssubst 1);

   407 by (stac hypreal_mult_le_cancel2 1);

   408 by (Asm_simp_tac 1);

   409 qed "neg_hypreal_le_divide_eq";

   410 Addsimps [inst "z" "number_of ?w" neg_hypreal_le_divide_eq];

   412 Goal "Numeral0<z ==> (y/z <= (x::hypreal)) = (y <= x*z)";

   413 by (subgoal_tac "(y <= x*z) = ((y/z)*z <= x*z)" 1);

   414 by (asm_simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_mult_assoc]) 2);

   415 by (etac ssubst 1);

   416 by (stac hypreal_mult_le_cancel2 1);

   417 by (Asm_simp_tac 1);

   418 qed "pos_hypreal_divide_le_eq";

   419 Addsimps [inst "z" "number_of ?w" pos_hypreal_divide_le_eq];

   421 Goal "z<Numeral0 ==> (y/z <= (x::hypreal)) = (x*z <= y)";

   422 by (subgoal_tac "(x*z <= y) = (x*z <= (y/z)*z)" 1);

   423 by (asm_simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_mult_assoc]) 2);

   424 by (etac ssubst 1);

   425 by (stac hypreal_mult_le_cancel2 1);

   426 by (Asm_simp_tac 1);

   427 qed "neg_hypreal_divide_le_eq";

   428 Addsimps [inst "z" "number_of ?w" neg_hypreal_divide_le_eq];

   430 Goal "Numeral0<z ==> ((x::hypreal) < y/z) = (x*z < y)";

   431 by (subgoal_tac "(x*z < y) = (x*z < (y/z)*z)" 1);

   432 by (asm_simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_mult_assoc]) 2);

   433 by (etac ssubst 1);

   434 by (stac hypreal_mult_less_cancel2 1);

   435 by (Asm_simp_tac 1);

   436 qed "pos_hypreal_less_divide_eq";

   437 Addsimps [inst "z" "number_of ?w" pos_hypreal_less_divide_eq];

   439 Goal "z<Numeral0 ==> ((x::hypreal) < y/z) = (y < x*z)";

   440 by (subgoal_tac "(y < x*z) = ((y/z)*z < x*z)" 1);

   441 by (asm_simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_mult_assoc]) 2);

   442 by (etac ssubst 1);

   443 by (stac hypreal_mult_less_cancel2 1);

   444 by (Asm_simp_tac 1);

   445 qed "neg_hypreal_less_divide_eq";

   446 Addsimps [inst "z" "number_of ?w" neg_hypreal_less_divide_eq];

   448 Goal "Numeral0<z ==> (y/z < (x::hypreal)) = (y < x*z)";

   449 by (subgoal_tac "(y < x*z) = ((y/z)*z < x*z)" 1);

   450 by (asm_simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_mult_assoc]) 2);

   451 by (etac ssubst 1);

   452 by (stac hypreal_mult_less_cancel2 1);

   453 by (Asm_simp_tac 1);

   454 qed "pos_hypreal_divide_less_eq";

   455 Addsimps [inst "z" "number_of ?w" pos_hypreal_divide_less_eq];

   457 Goal "z<Numeral0 ==> (y/z < (x::hypreal)) = (x*z < y)";

   458 by (subgoal_tac "(x*z < y) = (x*z < (y/z)*z)" 1);

   459 by (asm_simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_mult_assoc]) 2);

   460 by (etac ssubst 1);

   461 by (stac hypreal_mult_less_cancel2 1);

   462 by (Asm_simp_tac 1);

   463 qed "neg_hypreal_divide_less_eq";

   464 Addsimps [inst "z" "number_of ?w" neg_hypreal_divide_less_eq];

   466 Goal "z~=Numeral0 ==> ((x::hypreal) = y/z) = (x*z = y)";

   467 by (subgoal_tac "(x*z = y) = (x*z = (y/z)*z)" 1);

   468 by (asm_simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_mult_assoc]) 2);

   469 by (etac ssubst 1);

   470 by (stac hypreal_mult_eq_cancel2 1);

   471 by (Asm_simp_tac 1);

   472 qed "hypreal_eq_divide_eq";

   473 Addsimps [inst "z" "number_of ?w" hypreal_eq_divide_eq];

   475 Goal "z~=Numeral0 ==> (y/z = (x::hypreal)) = (y = x*z)";

   476 by (subgoal_tac "(y = x*z) = ((y/z)*z = x*z)" 1);

   477 by (asm_simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_mult_assoc]) 2);

   478 by (etac ssubst 1);

   479 by (stac hypreal_mult_eq_cancel2 1);

   480 by (Asm_simp_tac 1);

   481 qed "hypreal_divide_eq_eq";

   482 Addsimps [inst "z" "number_of ?w" hypreal_divide_eq_eq];

   484 Goal "(m/k = n/k) = (k = Numeral0 | m = (n::hypreal))";

   485 by (case_tac "k=Numeral0" 1);

   486 by (asm_simp_tac (simpset() addsimps [HYPREAL_DIVIDE_ZERO]) 1);

   487 by (asm_simp_tac (simpset() addsimps [hypreal_divide_eq_eq, hypreal_eq_divide_eq,

   488                                       hypreal_mult_eq_cancel2]) 1);

   489 qed "hypreal_divide_eq_cancel2";

   491 Goal "(k/m = k/n) = (k = Numeral0 | m = (n::hypreal))";

   492 by (case_tac "m=Numeral0 | n = Numeral0" 1);

   493 by (auto_tac (claset(),

   494               simpset() addsimps [HYPREAL_DIVIDE_ZERO, hypreal_divide_eq_eq,

   495                                   hypreal_eq_divide_eq, hypreal_mult_eq_cancel1]));

   496 qed "hypreal_divide_eq_cancel1";

   498 Goal "[| Numeral0 < r; Numeral0 < x|] ==> (inverse x < inverse (r::hypreal)) = (r < x)";

   499 by (auto_tac (claset() addIs [hypreal_inverse_less_swap], simpset()));

   500 by (res_inst_tac [("t","r")] (hypreal_inverse_inverse RS subst) 1);

   501 by (res_inst_tac [("t","x")] (hypreal_inverse_inverse RS subst) 1);

   502 by (auto_tac (claset() addIs [hypreal_inverse_less_swap],

   503 	      simpset() delsimps [hypreal_inverse_inverse]

   504 			addsimps [hypreal_inverse_gt_zero]));

   505 qed "hypreal_inverse_less_iff";

   507 Goal "[| Numeral0 < r; Numeral0 < x|] ==> (inverse x <= inverse r) = (r <= (x::hypreal))";

   508 by (asm_simp_tac (simpset() addsimps [linorder_not_less RS sym,

   509                                       hypreal_inverse_less_iff]) 1);

   510 qed "hypreal_inverse_le_iff";

   512 (** Division by 1, -1 **)

   514 Goal "(x::hypreal)/Numeral1 = x";

   515 by (simp_tac (simpset() addsimps [hypreal_divide_def]) 1);

   516 qed "hypreal_divide_1";

   517 Addsimps [hypreal_divide_1];

   519 Goal "x/-1 = -(x::hypreal)";

   520 by (Simp_tac 1);

   521 qed "hypreal_divide_minus1";

   522 Addsimps [hypreal_divide_minus1];

   524 Goal "-1/(x::hypreal) = - (Numeral1/x)";

   525 by (simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_minus_inverse]) 1);

   526 qed "hypreal_minus1_divide";

   527 Addsimps [hypreal_minus1_divide];

   529 Goal "[| (Numeral0::hypreal) < d1; Numeral0 < d2 |] ==> EX e. Numeral0 < e & e < d1 & e < d2";

   530 by (res_inst_tac [("x","(min d1 d2)/2")] exI 1);

   531 by (asm_simp_tac (simpset() addsimps [min_def]) 1);

   532 qed "hypreal_lbound_gt_zero";

   535 (*** General rewrites to improve automation, like those for type "int" ***)

   537 (** The next several equations can make the simplifier loop! **)

   539 Goal "(x < - y) = (y < - (x::hypreal))";

   540 by Auto_tac;

   541 qed "hypreal_less_minus";

   543 Goal "(- x < y) = (- y < (x::hypreal))";

   544 by Auto_tac;

   545 qed "hypreal_minus_less";

   547 Goal "(x <= - y) = (y <= - (x::hypreal))";

   548 by Auto_tac;

   549 qed "hypreal_le_minus";

   551 Goal "(- x <= y) = (- y <= (x::hypreal))";

   552 by Auto_tac;

   553 qed "hypreal_minus_le";

   555 Goal "(x = - y) = (y = - (x::hypreal))";

   556 by Auto_tac;

   557 qed "hypreal_equation_minus";

   559 Goal "(- x = y) = (- (y::hypreal) = x)";

   560 by Auto_tac;

   561 qed "hypreal_minus_equation";

   563 Goal "(x + - a = (Numeral0::hypreal)) = (x=a)";

   564 by (arith_tac 1);

   565 qed "hypreal_add_minus_iff";

   566 Addsimps [hypreal_add_minus_iff];

   568 Goal "(-b = -a) = (b = (a::hypreal))";

   569 by (arith_tac 1);

   570 qed "hypreal_minus_eq_cancel";

   571 Addsimps [hypreal_minus_eq_cancel];

   573 Goal "(-s <= -r) = ((r::hypreal) <= s)";

   574 by (stac hypreal_minus_le 1);

   575 by (Simp_tac 1);

   576 qed "hypreal_le_minus_iff";

   577 Addsimps [hypreal_le_minus_iff];

   580 (*Distributive laws for literals*)

   581 Addsimps (map (inst "w" "number_of ?v")

   582 	  [hypreal_add_mult_distrib, hypreal_add_mult_distrib2,

   583 	   hypreal_diff_mult_distrib, hypreal_diff_mult_distrib2]);

   585 Addsimps (map (inst "x" "number_of ?v")

   586 	  [hypreal_less_minus, hypreal_le_minus, hypreal_equation_minus]);

   587 Addsimps (map (inst "y" "number_of ?v")

   588 	  [hypreal_minus_less, hypreal_minus_le, hypreal_minus_equation]);

   591 (*** Simprules combining x+y and Numeral0 ***)

   593 Goal "(x+y = (Numeral0::hypreal)) = (y = -x)";

   594 by Auto_tac;

   595 qed "hypreal_add_eq_0_iff";

   596 AddIffs [hypreal_add_eq_0_iff];

   598 Goal "(x+y < (Numeral0::hypreal)) = (y < -x)";

   599 by Auto_tac;

   600 qed "hypreal_add_less_0_iff";

   601 AddIffs [hypreal_add_less_0_iff];

   603 Goal "((Numeral0::hypreal) < x+y) = (-x < y)";

   604 by Auto_tac;

   605 qed "hypreal_0_less_add_iff";

   606 AddIffs [hypreal_0_less_add_iff];

   608 Goal "(x+y <= (Numeral0::hypreal)) = (y <= -x)";

   609 by Auto_tac;

   610 qed "hypreal_add_le_0_iff";

   611 AddIffs [hypreal_add_le_0_iff];

   613 Goal "((Numeral0::hypreal) <= x+y) = (-x <= y)";

   614 by Auto_tac;

   615 qed "hypreal_0_le_add_iff";

   616 AddIffs [hypreal_0_le_add_iff];

   619 (** Simprules combining x-y and Numeral0; see also hypreal_less_iff_diff_less_0 etc

   620     in HyperBin

   621 **)

   623 Goal "((Numeral0::hypreal) < x-y) = (y < x)";

   624 by Auto_tac;

   625 qed "hypreal_0_less_diff_iff";

   626 AddIffs [hypreal_0_less_diff_iff];

   628 Goal "((Numeral0::hypreal) <= x-y) = (y <= x)";

   629 by Auto_tac;

   630 qed "hypreal_0_le_diff_iff";

   631 AddIffs [hypreal_0_le_diff_iff];

   633 (*

   634 FIXME: we should have this, as for type int, but many proofs would break.

   635 It replaces x+-y by x-y.

   636 Addsimps [symmetric hypreal_diff_def];

   637 *)

   639 Goal "-(x-y) = y - (x::hypreal)";

   640 by (arith_tac 1);

   641 qed "hypreal_minus_diff_eq";

   642 Addsimps [hypreal_minus_diff_eq];

   645 (*** Density of the Hyperreals ***)

   647 Goal "x < y ==> x < (x+y) / (2::hypreal)";

   648 by Auto_tac;

   649 qed "hypreal_less_half_sum";

   651 Goal "x < y ==> (x+y)/(2::hypreal) < y";

   652 by Auto_tac;

   653 qed "hypreal_gt_half_sum";

   655 Goal "x < y ==> EX r::hypreal. x < r & r < y";

   656 by (blast_tac (claset() addSIs [hypreal_less_half_sum, hypreal_gt_half_sum]) 1);

   657 qed "hypreal_dense";

   660 (*Replaces "inverse #nn" by Numeral1/#nn *)

   661 Addsimps [inst "x" "number_of ?w" hypreal_inverse_eq_divide];

author	wenzelm
	Sat, 06 Oct 2001 00:02:46 +0200
changeset 11704	3c50a2cd6f00
parent 11701	3d51fbf81c17
child 12018	ec054019c910
permissions	-rw-r--r--