src/HOL/Real/RealDef.ML
author paulson
Thu Oct 01 18:18:01 1998 +0200 (1998-10-01)
changeset 5588 a3ab526bb891
child 7077 60b098bb8b8a
permissions -rw-r--r--
Revised version with Abelian group simprocs
     1 (*  Title       : Real/RealDef.ML
     2     Author      : Jacques D. Fleuriot
     3     Copyright   : 1998  University of Cambridge
     4     Description : The reals
     5 *)
     6 
     7 (*** Proving that realrel is an equivalence relation ***)
     8 
     9 Goal "[| (x1::preal) + y2 = x2 + y1; x2 + y3 = x3 + y2 |] \
    10 \            ==> x1 + y3 = x3 + y1";        
    11 by (res_inst_tac [("C","y2")] preal_add_right_cancel 1);
    12 by (rotate_tac 1 1 THEN dtac sym 1);
    13 by (asm_full_simp_tac (simpset() addsimps preal_add_ac) 1);
    14 by (rtac (preal_add_left_commute RS subst) 1);
    15 by (res_inst_tac [("x1","x1")] (preal_add_assoc RS subst) 1);
    16 by (asm_full_simp_tac (simpset() addsimps preal_add_ac) 1);
    17 qed "preal_trans_lemma";
    18 
    19 (** Natural deduction for realrel **)
    20 
    21 Goalw [realrel_def]
    22     "(((x1,y1),(x2,y2)): realrel) = (x1 + y2 = x2 + y1)";
    23 by (Blast_tac 1);
    24 qed "realrel_iff";
    25 
    26 Goalw [realrel_def]
    27     "[| x1 + y2 = x2 + y1 |] ==> ((x1,y1),(x2,y2)): realrel";
    28 by (Blast_tac  1);
    29 qed "realrelI";
    30 
    31 Goalw [realrel_def]
    32   "p: realrel --> (EX x1 y1 x2 y2. \
    33 \                  p = ((x1,y1),(x2,y2)) & x1 + y2 = x2 + y1)";
    34 by (Blast_tac 1);
    35 qed "realrelE_lemma";
    36 
    37 val [major,minor] = goal thy
    38   "[| p: realrel;  \
    39 \     !!x1 y1 x2 y2. [| p = ((x1,y1),(x2,y2));  x1+y2 = x2+y1 \
    40 \                    |] ==> Q |] ==> Q";
    41 by (cut_facts_tac [major RS (realrelE_lemma RS mp)] 1);
    42 by (REPEAT (eresolve_tac [asm_rl,exE,conjE,minor] 1));
    43 qed "realrelE";
    44 
    45 AddSIs [realrelI];
    46 AddSEs [realrelE];
    47 
    48 Goal "(x,x): realrel";
    49 by (stac surjective_pairing 1 THEN rtac (refl RS realrelI) 1);
    50 qed "realrel_refl";
    51 
    52 Goalw [equiv_def, refl_def, sym_def, trans_def]
    53     "equiv {x::(preal*preal).True} realrel";
    54 by (fast_tac (claset() addSIs [realrel_refl] 
    55                       addSEs [sym,preal_trans_lemma]) 1);
    56 qed "equiv_realrel";
    57 
    58 val equiv_realrel_iff =
    59     [TrueI, TrueI] MRS 
    60     ([CollectI, CollectI] MRS 
    61     (equiv_realrel RS eq_equiv_class_iff));
    62 
    63 Goalw  [real_def,realrel_def,quotient_def] "realrel^^{(x,y)}:real";
    64 by (Blast_tac 1);
    65 qed "realrel_in_real";
    66 
    67 Goal "inj_on Abs_real real";
    68 by (rtac inj_on_inverseI 1);
    69 by (etac Abs_real_inverse 1);
    70 qed "inj_on_Abs_real";
    71 
    72 Addsimps [equiv_realrel_iff,inj_on_Abs_real RS inj_on_iff,
    73           realrel_iff, realrel_in_real, Abs_real_inverse];
    74 
    75 Addsimps [equiv_realrel RS eq_equiv_class_iff];
    76 val eq_realrelD = equiv_realrel RSN (2,eq_equiv_class);
    77 
    78 Goal "inj(Rep_real)";
    79 by (rtac inj_inverseI 1);
    80 by (rtac Rep_real_inverse 1);
    81 qed "inj_Rep_real";
    82 
    83 (** real_preal: the injection from preal to real **)
    84 Goal "inj(real_preal)";
    85 by (rtac injI 1);
    86 by (rewtac real_preal_def);
    87 by (dtac (inj_on_Abs_real RS inj_onD) 1);
    88 by (REPEAT (rtac realrel_in_real 1));
    89 by (dtac eq_equiv_class 1);
    90 by (rtac equiv_realrel 1);
    91 by (Blast_tac 1);
    92 by Safe_tac;
    93 by (Asm_full_simp_tac 1);
    94 qed "inj_real_preal";
    95 
    96 val [prem] = goal thy
    97     "(!!x y. z = Abs_real(realrel^^{(x,y)}) ==> P) ==> P";
    98 by (res_inst_tac [("x1","z")] 
    99     (rewrite_rule [real_def] Rep_real RS quotientE) 1);
   100 by (dres_inst_tac [("f","Abs_real")] arg_cong 1);
   101 by (res_inst_tac [("p","x")] PairE 1);
   102 by (rtac prem 1);
   103 by (asm_full_simp_tac (simpset() addsimps [Rep_real_inverse]) 1);
   104 qed "eq_Abs_real";
   105 
   106 (**** real_minus: additive inverse on real ****)
   107 
   108 Goalw [congruent_def]
   109   "congruent realrel (%p. split (%x y. realrel^^{(y,x)}) p)";
   110 by Safe_tac;
   111 by (asm_full_simp_tac (simpset() addsimps [preal_add_commute]) 1);
   112 qed "real_minus_congruent";
   113 
   114 (*Resolve th against the corresponding facts for real_minus*)
   115 val real_minus_ize = RSLIST [equiv_realrel, real_minus_congruent];
   116 
   117 Goalw [real_minus_def]
   118       "- (Abs_real(realrel^^{(x,y)})) = Abs_real(realrel ^^ {(y,x)})";
   119 by (res_inst_tac [("f","Abs_real")] arg_cong 1);
   120 by (simp_tac (simpset() addsimps 
   121    [realrel_in_real RS Abs_real_inverse,real_minus_ize UN_equiv_class]) 1);
   122 qed "real_minus";
   123 
   124 Goal "- (- z) = (z::real)";
   125 by (res_inst_tac [("z","z")] eq_Abs_real 1);
   126 by (asm_simp_tac (simpset() addsimps [real_minus]) 1);
   127 qed "real_minus_minus";
   128 
   129 Addsimps [real_minus_minus];
   130 
   131 Goal "inj(%r::real. -r)";
   132 by (rtac injI 1);
   133 by (dres_inst_tac [("f","uminus")] arg_cong 1);
   134 by (asm_full_simp_tac (simpset() addsimps [real_minus_minus]) 1);
   135 qed "inj_real_minus";
   136 
   137 Goalw [real_zero_def] "-0r = 0r";
   138 by (simp_tac (simpset() addsimps [real_minus]) 1);
   139 qed "real_minus_zero";
   140 
   141 Addsimps [real_minus_zero];
   142 
   143 Goal "(-x = 0r) = (x = 0r)"; 
   144 by (res_inst_tac [("z","x")] eq_Abs_real 1);
   145 by (auto_tac (claset(),
   146 	      simpset() addsimps [real_zero_def, real_minus] @ preal_add_ac));
   147 qed "real_minus_zero_iff";
   148 
   149 Addsimps [real_minus_zero_iff];
   150 
   151 Goal "(-x ~= 0r) = (x ~= 0r)"; 
   152 by Auto_tac;
   153 qed "real_minus_not_zero_iff";
   154 
   155 (*** Congruence property for addition ***)
   156 Goalw [congruent2_def]
   157     "congruent2 realrel (%p1 p2.                  \
   158 \         split (%x1 y1. split (%x2 y2. realrel^^{(x1+x2, y1+y2)}) p2) p1)";
   159 by Safe_tac;
   160 by (asm_simp_tac (simpset() addsimps [preal_add_assoc]) 1);
   161 by (res_inst_tac [("z1.1","x1a")] (preal_add_left_commute RS ssubst) 1);
   162 by (asm_simp_tac (simpset() addsimps [preal_add_assoc RS sym]) 1);
   163 by (asm_simp_tac (simpset() addsimps preal_add_ac) 1);
   164 qed "real_add_congruent2";
   165 
   166 (*Resolve th against the corresponding facts for real_add*)
   167 val real_add_ize = RSLIST [equiv_realrel, real_add_congruent2];
   168 
   169 Goalw [real_add_def]
   170   "Abs_real(realrel^^{(x1,y1)}) + Abs_real(realrel^^{(x2,y2)}) = \
   171 \  Abs_real(realrel^^{(x1+x2, y1+y2)})";
   172 by (asm_simp_tac (simpset() addsimps [real_add_ize UN_equiv_class2]) 1);
   173 qed "real_add";
   174 
   175 Goal "(z::real) + w = w + z";
   176 by (res_inst_tac [("z","z")] eq_Abs_real 1);
   177 by (res_inst_tac [("z","w")] eq_Abs_real 1);
   178 by (asm_simp_tac (simpset() addsimps preal_add_ac @ [real_add]) 1);
   179 qed "real_add_commute";
   180 
   181 Goal "((z1::real) + z2) + z3 = z1 + (z2 + z3)";
   182 by (res_inst_tac [("z","z1")] eq_Abs_real 1);
   183 by (res_inst_tac [("z","z2")] eq_Abs_real 1);
   184 by (res_inst_tac [("z","z3")] eq_Abs_real 1);
   185 by (asm_simp_tac (simpset() addsimps [real_add, preal_add_assoc]) 1);
   186 qed "real_add_assoc";
   187 
   188 (*For AC rewriting*)
   189 Goal "(x::real)+(y+z)=y+(x+z)";
   190 by (rtac (real_add_commute RS trans) 1);
   191 by (rtac (real_add_assoc RS trans) 1);
   192 by (rtac (real_add_commute RS arg_cong) 1);
   193 qed "real_add_left_commute";
   194 
   195 (* real addition is an AC operator *)
   196 val real_add_ac = [real_add_assoc,real_add_commute,real_add_left_commute];
   197 
   198 Goalw [real_preal_def,real_zero_def] "0r + z = z";
   199 by (res_inst_tac [("z","z")] eq_Abs_real 1);
   200 by (asm_full_simp_tac (simpset() addsimps [real_add] @ preal_add_ac) 1);
   201 qed "real_add_zero_left";
   202 Addsimps [real_add_zero_left];
   203 
   204 Goal "z + 0r = z";
   205 by (simp_tac (simpset() addsimps [real_add_commute]) 1);
   206 qed "real_add_zero_right";
   207 Addsimps [real_add_zero_right];
   208 
   209 Goalw [real_zero_def] "z + -z = 0r";
   210 by (res_inst_tac [("z","z")] eq_Abs_real 1);
   211 by (asm_full_simp_tac (simpset() addsimps [real_minus,
   212         real_add, preal_add_commute]) 1);
   213 qed "real_add_minus";
   214 Addsimps [real_add_minus];
   215 
   216 Goal "-z + z = 0r";
   217 by (simp_tac (simpset() addsimps [real_add_commute]) 1);
   218 qed "real_add_minus_left";
   219 Addsimps [real_add_minus_left];
   220 
   221 
   222 Goal "z + (- z + w) = (w::real)";
   223 by (simp_tac (simpset() addsimps [real_add_assoc RS sym]) 1);
   224 qed "real_add_minus_cancel";
   225 
   226 Goal "(-z) + (z + w) = (w::real)";
   227 by (simp_tac (simpset() addsimps [real_add_assoc RS sym]) 1);
   228 qed "real_minus_add_cancel";
   229 
   230 Addsimps [real_add_minus_cancel, real_minus_add_cancel];
   231 
   232 Goal "? y. (x::real) + y = 0r";
   233 by (blast_tac (claset() addIs [real_add_minus]) 1);
   234 qed "real_minus_ex";
   235 
   236 Goal "?! y. (x::real) + y = 0r";
   237 by (auto_tac (claset() addIs [real_add_minus],simpset()));
   238 by (dres_inst_tac [("f","%x. ya+x")] arg_cong 1);
   239 by (asm_full_simp_tac (simpset() addsimps [real_add_assoc RS sym]) 1);
   240 by (asm_full_simp_tac (simpset() addsimps [real_add_commute]) 1);
   241 qed "real_minus_ex1";
   242 
   243 Goal "?! y. y + (x::real) = 0r";
   244 by (auto_tac (claset() addIs [real_add_minus_left],simpset()));
   245 by (dres_inst_tac [("f","%x. x+ya")] arg_cong 1);
   246 by (asm_full_simp_tac (simpset() addsimps [real_add_assoc]) 1);
   247 by (asm_full_simp_tac (simpset() addsimps [real_add_commute]) 1);
   248 qed "real_minus_left_ex1";
   249 
   250 Goal "x + y = 0r ==> x = -y";
   251 by (cut_inst_tac [("z","y")] real_add_minus_left 1);
   252 by (res_inst_tac [("x1","y")] (real_minus_left_ex1 RS ex1E) 1);
   253 by (Blast_tac 1);
   254 qed "real_add_minus_eq_minus";
   255 
   256 Goal "-(x + y) = -x + -(y::real)";
   257 by (res_inst_tac [("z","x")] eq_Abs_real 1);
   258 by (res_inst_tac [("z","y")] eq_Abs_real 1);
   259 by (auto_tac (claset(),simpset() addsimps [real_minus,real_add]));
   260 qed "real_minus_add_distrib";
   261 
   262 Addsimps [real_minus_add_distrib];
   263 
   264 Goal "((x::real) + y = x + z) = (y = z)";
   265 by (Step_tac 1);
   266 by (dres_inst_tac [("f","%t.-x + t")] arg_cong 1);
   267 by (asm_full_simp_tac (simpset() addsimps [real_add_assoc RS sym]) 1);
   268 qed "real_add_left_cancel";
   269 
   270 Goal "(y + (x::real)= z + x) = (y = z)";
   271 by (simp_tac (simpset() addsimps [real_add_commute,real_add_left_cancel]) 1);
   272 qed "real_add_right_cancel";
   273 
   274 Goal "0r - x = -x";
   275 by (simp_tac (simpset() addsimps [real_diff_def]) 1);
   276 qed "real_diff_0";
   277 
   278 Goal "x - 0r = x";
   279 by (simp_tac (simpset() addsimps [real_diff_def]) 1);
   280 qed "real_diff_0_right";
   281 
   282 Goal "x - x = 0r";
   283 by (simp_tac (simpset() addsimps [real_diff_def]) 1);
   284 qed "real_diff_self";
   285 
   286 Addsimps [real_diff_0, real_diff_0_right, real_diff_self];
   287 
   288 
   289 (*** Congruence property for multiplication ***)
   290 
   291 Goal "!!(x1::preal). [| x1 + y2 = x2 + y1 |] ==> \
   292 \         x * x1 + y * y1 + (x * y2 + x2 * y) = \
   293 \         x * x2 + y * y2 + (x * y1 + x1 * y)";
   294 by (asm_full_simp_tac (simpset() addsimps [preal_add_left_commute,
   295     preal_add_assoc RS sym,preal_add_mult_distrib2 RS sym]) 1);
   296 by (rtac (preal_mult_commute RS subst) 1);
   297 by (res_inst_tac [("y1","x2")] (preal_mult_commute RS subst) 1);
   298 by (asm_full_simp_tac (simpset() addsimps [preal_add_assoc,
   299     preal_add_mult_distrib2 RS sym]) 1);
   300 by (asm_full_simp_tac (simpset() addsimps [preal_add_commute]) 1);
   301 qed "real_mult_congruent2_lemma";
   302 
   303 Goal 
   304     "congruent2 realrel (%p1 p2.                  \
   305 \         split (%x1 y1. split (%x2 y2. realrel^^{(x1*x2 + y1*y2, x1*y2+x2*y1)}) p2) p1)";
   306 by (rtac (equiv_realrel RS congruent2_commuteI) 1);
   307 by Safe_tac;
   308 by (rewtac split_def);
   309 by (asm_simp_tac (simpset() addsimps [preal_mult_commute,preal_add_commute]) 1);
   310 by (auto_tac (claset(),simpset() addsimps [real_mult_congruent2_lemma]));
   311 qed "real_mult_congruent2";
   312 
   313 (*Resolve th against the corresponding facts for real_mult*)
   314 val real_mult_ize = RSLIST [equiv_realrel, real_mult_congruent2];
   315 
   316 Goalw [real_mult_def]
   317    "Abs_real((realrel^^{(x1,y1)})) * Abs_real((realrel^^{(x2,y2)})) =   \
   318 \   Abs_real(realrel ^^ {(x1*x2+y1*y2,x1*y2+x2*y1)})";
   319 by (simp_tac (simpset() addsimps [real_mult_ize UN_equiv_class2]) 1);
   320 qed "real_mult";
   321 
   322 Goal "(z::real) * w = w * z";
   323 by (res_inst_tac [("z","z")] eq_Abs_real 1);
   324 by (res_inst_tac [("z","w")] eq_Abs_real 1);
   325 by (asm_simp_tac
   326     (simpset() addsimps [real_mult] @ preal_add_ac @ preal_mult_ac) 1);
   327 qed "real_mult_commute";
   328 
   329 Goal "((z1::real) * z2) * z3 = z1 * (z2 * z3)";
   330 by (res_inst_tac [("z","z1")] eq_Abs_real 1);
   331 by (res_inst_tac [("z","z2")] eq_Abs_real 1);
   332 by (res_inst_tac [("z","z3")] eq_Abs_real 1);
   333 by (asm_simp_tac (simpset() addsimps [preal_add_mult_distrib2,real_mult] @ 
   334                                      preal_add_ac @ preal_mult_ac) 1);
   335 qed "real_mult_assoc";
   336 
   337 qed_goal "real_mult_left_commute" thy
   338     "(z1::real) * (z2 * z3) = z2 * (z1 * z3)"
   339  (fn _ => [rtac (real_mult_commute RS trans) 1, rtac (real_mult_assoc RS trans) 1,
   340            rtac (real_mult_commute RS arg_cong) 1]);
   341 
   342 (* real multiplication is an AC operator *)
   343 val real_mult_ac = [real_mult_assoc, real_mult_commute, real_mult_left_commute];
   344 
   345 Goalw [real_one_def,pnat_one_def] "1r * z = z";
   346 by (res_inst_tac [("z","z")] eq_Abs_real 1);
   347 by (asm_full_simp_tac
   348     (simpset() addsimps [real_mult,
   349 			 preal_add_mult_distrib2,preal_mult_1_right] 
   350                         @ preal_mult_ac @ preal_add_ac) 1);
   351 qed "real_mult_1";
   352 
   353 Addsimps [real_mult_1];
   354 
   355 Goal "z * 1r = z";
   356 by (simp_tac (simpset() addsimps [real_mult_commute]) 1);
   357 qed "real_mult_1_right";
   358 
   359 Addsimps [real_mult_1_right];
   360 
   361 Goalw [real_zero_def,pnat_one_def] "0r * z = 0r";
   362 by (res_inst_tac [("z","z")] eq_Abs_real 1);
   363 by (asm_full_simp_tac (simpset() addsimps [real_mult,
   364     preal_add_mult_distrib2,preal_mult_1_right] 
   365     @ preal_mult_ac @ preal_add_ac) 1);
   366 qed "real_mult_0";
   367 
   368 Goal "z * 0r = 0r";
   369 by (simp_tac (simpset() addsimps [real_mult_commute, real_mult_0]) 1);
   370 qed "real_mult_0_right";
   371 
   372 Addsimps [real_mult_0_right, real_mult_0];
   373 
   374 Goal "-(x * y) = -x * (y::real)";
   375 by (res_inst_tac [("z","x")] eq_Abs_real 1);
   376 by (res_inst_tac [("z","y")] eq_Abs_real 1);
   377 by (auto_tac (claset(),
   378 	      simpset() addsimps [real_minus,real_mult] 
   379     @ preal_mult_ac @ preal_add_ac));
   380 qed "real_minus_mult_eq1";
   381 
   382 Goal "-(x * y) = x * -(y::real)";
   383 by (res_inst_tac [("z","x")] eq_Abs_real 1);
   384 by (res_inst_tac [("z","y")] eq_Abs_real 1);
   385 by (auto_tac (claset(),
   386 	      simpset() addsimps [real_minus,real_mult] 
   387     @ preal_mult_ac @ preal_add_ac));
   388 qed "real_minus_mult_eq2";
   389 
   390 Goal "- 1r * z = -z";
   391 by (simp_tac (simpset() addsimps [real_minus_mult_eq1 RS sym]) 1);
   392 qed "real_mult_minus_1";
   393 
   394 Addsimps [real_mult_minus_1];
   395 
   396 Goal "z * - 1r = -z";
   397 by (stac real_mult_commute 1);
   398 by (Simp_tac 1);
   399 qed "real_mult_minus_1_right";
   400 
   401 Addsimps [real_mult_minus_1_right];
   402 
   403 Goal "-x * -y = x * (y::real)";
   404 by (full_simp_tac (simpset() addsimps [real_minus_mult_eq2 RS sym,
   405     real_minus_mult_eq1 RS sym]) 1);
   406 qed "real_minus_mult_cancel";
   407 
   408 Addsimps [real_minus_mult_cancel];
   409 
   410 Goal "-x * y = x * -(y::real)";
   411 by (full_simp_tac (simpset() addsimps [real_minus_mult_eq2 RS sym,
   412     real_minus_mult_eq1 RS sym]) 1);
   413 qed "real_minus_mult_commute";
   414 
   415 (*-----------------------------------------------------------------------------
   416 
   417  -----------------------------------------------------------------------------*)
   418 
   419 (** Lemmas **)
   420 
   421 qed_goal "real_add_assoc_cong" thy
   422     "!!z. (z::real) + v = z' + v' ==> z + (v + w) = z' + (v' + w)"
   423  (fn _ => [(asm_simp_tac (simpset() addsimps [real_add_assoc RS sym]) 1)]);
   424 
   425 qed_goal "real_add_assoc_swap" thy "(z::real) + (v + w) = v + (z + w)"
   426  (fn _ => [(REPEAT (ares_tac [real_add_commute RS real_add_assoc_cong] 1))]);
   427 
   428 Goal "((z1::real) + z2) * w = (z1 * w) + (z2 * w)";
   429 by (res_inst_tac [("z","z1")] eq_Abs_real 1);
   430 by (res_inst_tac [("z","z2")] eq_Abs_real 1);
   431 by (res_inst_tac [("z","w")] eq_Abs_real 1);
   432 by (asm_simp_tac 
   433     (simpset() addsimps [preal_add_mult_distrib2, real_add, real_mult] @ 
   434                         preal_add_ac @ preal_mult_ac) 1);
   435 qed "real_add_mult_distrib";
   436 
   437 val real_mult_commute'= read_instantiate [("z","w")] real_mult_commute;
   438 
   439 Goal "(w::real) * (z1 + z2) = (w * z1) + (w * z2)";
   440 by (simp_tac (simpset() addsimps [real_mult_commute',real_add_mult_distrib]) 1);
   441 qed "real_add_mult_distrib2";
   442 
   443 (*** one and zero are distinct ***)
   444 Goalw [real_zero_def,real_one_def] "0r ~= 1r";
   445 by (auto_tac (claset(),
   446          simpset() addsimps [preal_self_less_add_left RS preal_not_refl2]));
   447 qed "real_zero_not_eq_one";
   448 
   449 (*** existence of inverse ***)
   450 (** lemma -- alternative definition for 0r **)
   451 Goalw [real_zero_def] "0r = Abs_real (realrel ^^ {(x, x)})";
   452 by (auto_tac (claset(),simpset() addsimps [preal_add_commute]));
   453 qed "real_zero_iff";
   454 
   455 Goalw [real_zero_def,real_one_def] 
   456           "!!(x::real). x ~= 0r ==> ? y. x*y = 1r";
   457 by (res_inst_tac [("z","x")] eq_Abs_real 1);
   458 by (cut_inst_tac [("r1.0","xa"),("r2.0","y")] preal_linear 1);
   459 by (auto_tac (claset() addSDs [preal_less_add_left_Ex],
   460            simpset() addsimps [real_zero_iff RS sym]));
   461 by (res_inst_tac [("x","Abs_real (realrel ^^ {(@#$#1p,pinv(D)+@#$#1p)})")] exI 1);
   462 by (res_inst_tac [("x","Abs_real (realrel ^^ {(pinv(D)+@#$#1p,@#$#1p)})")] exI 2);
   463 by (auto_tac (claset(),
   464 	      simpset() addsimps [real_mult,
   465     pnat_one_def,preal_mult_1_right,preal_add_mult_distrib2,
   466     preal_add_mult_distrib,preal_mult_1,preal_mult_inv_right] 
   467     @ preal_add_ac @ preal_mult_ac));
   468 qed "real_mult_inv_right_ex";
   469 
   470 Goal "!!(x::real). x ~= 0r ==> ? y. y*x = 1r";
   471 by (asm_simp_tac (simpset() addsimps [real_mult_commute,
   472     real_mult_inv_right_ex]) 1);
   473 qed "real_mult_inv_left_ex";
   474 
   475 Goalw [rinv_def] "!!(x::real). x ~= 0r ==> rinv(x)*x = 1r";
   476 by (forward_tac [real_mult_inv_left_ex] 1);
   477 by (Step_tac 1);
   478 by (rtac selectI2 1);
   479 by Auto_tac;
   480 qed "real_mult_inv_left";
   481 
   482 Goal "!!(x::real). x ~= 0r ==> x*rinv(x) = 1r";
   483 by (auto_tac (claset() addIs [real_mult_commute RS subst],
   484               simpset() addsimps [real_mult_inv_left]));
   485 qed "real_mult_inv_right";
   486 
   487 Goal "(c::real) ~= 0r ==> (c*a=c*b) = (a=b)";
   488 by Auto_tac;
   489 by (dres_inst_tac [("f","%x. x*rinv c")] arg_cong 1);
   490 by (asm_full_simp_tac (simpset() addsimps [real_mult_inv_right] @ real_mult_ac)  1);
   491 qed "real_mult_left_cancel";
   492     
   493 Goal "(c::real) ~= 0r ==> (a*c=b*c) = (a=b)";
   494 by (Step_tac 1);
   495 by (dres_inst_tac [("f","%x. x*rinv c")] arg_cong 1);
   496 by (asm_full_simp_tac (simpset() addsimps [real_mult_inv_right] @ real_mult_ac)  1);
   497 qed "real_mult_right_cancel";
   498 
   499 Goalw [rinv_def] "x ~= 0r ==> rinv(x) ~= 0r";
   500 by (forward_tac [real_mult_inv_left_ex] 1);
   501 by (etac exE 1);
   502 by (rtac selectI2 1);
   503 by (auto_tac (claset(),
   504 	      simpset() addsimps [real_mult_0,
   505     real_zero_not_eq_one]));
   506 qed "rinv_not_zero";
   507 
   508 Addsimps [real_mult_inv_left,real_mult_inv_right];
   509 
   510 Goal "x ~= 0r ==> rinv(rinv x) = x";
   511 by (res_inst_tac [("c1","rinv x")] (real_mult_right_cancel RS iffD1) 1);
   512 by (etac rinv_not_zero 1);
   513 by (auto_tac (claset() addDs [rinv_not_zero],simpset()));
   514 qed "real_rinv_rinv";
   515 
   516 Goalw [rinv_def] "rinv(1r) = 1r";
   517 by (cut_facts_tac [real_zero_not_eq_one RS 
   518        not_sym RS real_mult_inv_left_ex] 1);
   519 by (etac exE 1);
   520 by (rtac selectI2 1);
   521 by (auto_tac (claset(),
   522 	      simpset() addsimps 
   523     [real_zero_not_eq_one RS not_sym]));
   524 qed "real_rinv_1";
   525 
   526 Goal "x ~= 0r ==> rinv(-x) = -rinv(x)";
   527 by (res_inst_tac [("c1","-x")] (real_mult_right_cancel RS iffD1) 1);
   528 by Auto_tac;
   529 qed "real_minus_rinv";
   530 
   531       (*** theorems for ordering ***)
   532 (* prove introduction and elimination rules for real_less *)
   533 
   534 (* real_less is a strong order i.e nonreflexive and transitive *)
   535 (*** lemmas ***)
   536 Goal "!!(x::preal). [| x = y; x1 = y1 |] ==> x + y1 = x1 + y";
   537 by (asm_simp_tac (simpset() addsimps [preal_add_commute]) 1);
   538 qed "preal_lemma_eq_rev_sum";
   539 
   540 Goal "!!(b::preal). x + (b + y) = x1 + (b + y1) ==> x + y = x1 + y1";
   541 by (asm_full_simp_tac (simpset() addsimps preal_add_ac) 1);
   542 qed "preal_add_left_commute_cancel";
   543 
   544 Goal "!!(x::preal). [| x + y2a = x2a + y; \
   545 \                      x + y2b = x2b + y |] \
   546 \                   ==> x2a + y2b = x2b + y2a";
   547 by (dtac preal_lemma_eq_rev_sum 1);
   548 by (assume_tac 1);
   549 by (thin_tac "x + y2b = x2b + y" 1);
   550 by (asm_full_simp_tac (simpset() addsimps preal_add_ac) 1);
   551 by (dtac preal_add_left_commute_cancel 1);
   552 by (asm_full_simp_tac (simpset() addsimps preal_add_ac) 1);
   553 qed "preal_lemma_for_not_refl";
   554 
   555 Goal "~ (R::real) < R";
   556 by (res_inst_tac [("z","R")] eq_Abs_real 1);
   557 by (auto_tac (claset(),simpset() addsimps [real_less_def]));
   558 by (dtac preal_lemma_for_not_refl 1);
   559 by (assume_tac 1 THEN rotate_tac 2 1);
   560 by (auto_tac (claset(),simpset() addsimps [preal_less_not_refl]));
   561 qed "real_less_not_refl";
   562 
   563 (*** y < y ==> P ***)
   564 bind_thm("real_less_irrefl", real_less_not_refl RS notE);
   565 AddSEs [real_less_irrefl];
   566 
   567 Goal "!!(x::real). x < y ==> x ~= y";
   568 by (auto_tac (claset(),simpset() addsimps [real_less_not_refl]));
   569 qed "real_not_refl2";
   570 
   571 (* lemma re-arranging and eliminating terms *)
   572 Goal "!! (a::preal). [| a + b = c + d; \
   573 \            x2b + d + (c + y2e) < a + y2b + (x2e + b) |] \
   574 \         ==> x2b + y2e < x2e + y2b";
   575 by (asm_full_simp_tac (simpset() addsimps preal_add_ac) 1);
   576 by (res_inst_tac [("C","c+d")] preal_add_left_less_cancel 1);
   577 by (asm_full_simp_tac (simpset() addsimps [preal_add_assoc RS sym]) 1);
   578 qed "preal_lemma_trans";
   579 
   580 (** heavy re-writing involved*)
   581 Goal "!!(R1::real). [| R1 < R2; R2 < R3 |] ==> R1 < R3";
   582 by (res_inst_tac [("z","R1")] eq_Abs_real 1);
   583 by (res_inst_tac [("z","R2")] eq_Abs_real 1);
   584 by (res_inst_tac [("z","R3")] eq_Abs_real 1);
   585 by (auto_tac (claset(),simpset() addsimps [real_less_def]));
   586 by (REPEAT(rtac exI 1));
   587 by (EVERY[rtac conjI 1, rtac conjI 2]);
   588 by (REPEAT(Blast_tac 2));
   589 by (dtac preal_lemma_for_not_refl 1 THEN assume_tac 1);
   590 by (blast_tac (claset() addDs [preal_add_less_mono] 
   591     addIs [preal_lemma_trans]) 1);
   592 qed "real_less_trans";
   593 
   594 Goal "!! (R1::real). [| R1 < R2; R2 < R1 |] ==> P";
   595 by (dtac real_less_trans 1 THEN assume_tac 1);
   596 by (asm_full_simp_tac (simpset() addsimps [real_less_not_refl]) 1);
   597 qed "real_less_asym";
   598 
   599 (****)(****)(****)(****)(****)(****)(****)(****)(****)(****)
   600     (****** Map and more real_less ******)
   601 (*** mapping from preal into real ***)
   602 Goalw [real_preal_def] 
   603             "%#((z1::preal) + z2) = %#z1 + %#z2";
   604 by (asm_simp_tac (simpset() addsimps [real_add,
   605        preal_add_mult_distrib,preal_mult_1] addsimps preal_add_ac) 1);
   606 qed "real_preal_add";
   607 
   608 Goalw [real_preal_def] 
   609             "%#((z1::preal) * z2) = %#z1* %#z2";
   610 by (full_simp_tac (simpset() addsimps [real_mult,
   611         preal_add_mult_distrib2,preal_mult_1,
   612         preal_mult_1_right,pnat_one_def] 
   613         @ preal_add_ac @ preal_mult_ac) 1);
   614 qed "real_preal_mult";
   615 
   616 Goalw [real_preal_def]
   617       "!!(x::preal). y < x ==> ? m. Abs_real (realrel ^^ {(x,y)}) = %#m";
   618 by (auto_tac (claset() addSDs [preal_less_add_left_Ex],
   619     simpset() addsimps preal_add_ac));
   620 qed "real_preal_ExI";
   621 
   622 Goalw [real_preal_def]
   623       "!!(x::preal). ? m. Abs_real (realrel ^^ {(x,y)}) = %#m ==> y < x";
   624 by (auto_tac (claset(),
   625 	      simpset() addsimps 
   626     [preal_add_commute,preal_add_assoc]));
   627 by (asm_full_simp_tac (simpset() addsimps 
   628     [preal_add_assoc RS sym,preal_self_less_add_left]) 1);
   629 qed "real_preal_ExD";
   630 
   631 Goal "(? m. Abs_real (realrel ^^ {(x,y)}) = %#m) = (y < x)";
   632 by (blast_tac (claset() addSIs [real_preal_ExI,real_preal_ExD]) 1);
   633 qed "real_preal_iff";
   634 
   635 (*** Gleason prop 9-4.4 p 127 ***)
   636 Goalw [real_preal_def,real_zero_def] 
   637       "? m. (x::real) = %#m | x = 0r | x = -(%#m)";
   638 by (res_inst_tac [("z","x")] eq_Abs_real 1);
   639 by (auto_tac (claset(),simpset() addsimps [real_minus] @ preal_add_ac));
   640 by (cut_inst_tac [("r1.0","x"),("r2.0","y")] preal_linear 1);
   641 by (auto_tac (claset() addSDs [preal_less_add_left_Ex],
   642     simpset() addsimps [preal_add_assoc RS sym]));
   643 by (auto_tac (claset(),simpset() addsimps [preal_add_commute]));
   644 qed "real_preal_trichotomy";
   645 
   646 Goal "!!P. [| !!m. x = %#m ==> P; \
   647 \             x = 0r ==> P; \
   648 \             !!m. x = -(%#m) ==> P |] ==> P";
   649 by (cut_inst_tac [("x","x")] real_preal_trichotomy 1);
   650 by Auto_tac;
   651 qed "real_preal_trichotomyE";
   652 
   653 Goalw [real_preal_def] "%#m1 < %#m2 ==> m1 < m2";
   654 by (auto_tac (claset(),simpset() addsimps [real_less_def] @ preal_add_ac));
   655 by (auto_tac (claset(),simpset() addsimps [preal_add_assoc RS sym]));
   656 by (auto_tac (claset(),simpset() addsimps preal_add_ac));
   657 qed "real_preal_lessD";
   658 
   659 Goal "m1 < m2 ==> %#m1 < %#m2";
   660 by (dtac preal_less_add_left_Ex 1);
   661 by (auto_tac (claset(),
   662 	      simpset() addsimps [real_preal_add,
   663     real_preal_def,real_less_def]));
   664 by (REPEAT(rtac exI 1));
   665 by (EVERY[rtac conjI 1, rtac conjI 2]);
   666 by (REPEAT(Blast_tac 2));
   667 by (simp_tac (simpset() addsimps [preal_self_less_add_left] 
   668     delsimps [preal_add_less_iff2]) 1);
   669 qed "real_preal_lessI";
   670 
   671 Goal "(%#m1 < %#m2) = (m1 < m2)";
   672 by (blast_tac (claset() addIs [real_preal_lessI,real_preal_lessD]) 1);
   673 qed "real_preal_less_iff1";
   674 
   675 Addsimps [real_preal_less_iff1];
   676 
   677 Goal "- %#m < %#m";
   678 by (auto_tac (claset(),
   679 	      simpset() addsimps 
   680     [real_preal_def,real_less_def,real_minus]));
   681 by (REPEAT(rtac exI 1));
   682 by (EVERY[rtac conjI 1, rtac conjI 2]);
   683 by (REPEAT(Blast_tac 2));
   684 by (full_simp_tac (simpset() addsimps preal_add_ac) 1);
   685 by (full_simp_tac (simpset() addsimps [preal_self_less_add_right,
   686     preal_add_assoc RS sym]) 1);
   687 qed "real_preal_minus_less_self";
   688 
   689 Goalw [real_zero_def] "- %#m < 0r";
   690 by (auto_tac (claset(),
   691 	      simpset() addsimps [real_preal_def,real_less_def,real_minus]));
   692 by (REPEAT(rtac exI 1));
   693 by (EVERY[rtac conjI 1, rtac conjI 2]);
   694 by (REPEAT(Blast_tac 2));
   695 by (full_simp_tac (simpset() addsimps 
   696   [preal_self_less_add_right] @ preal_add_ac) 1);
   697 qed "real_preal_minus_less_zero";
   698 
   699 Goal "~ 0r < - %#m";
   700 by (cut_facts_tac [real_preal_minus_less_zero] 1);
   701 by (fast_tac (claset() addDs [real_less_trans] 
   702                         addEs [real_less_irrefl]) 1);
   703 qed "real_preal_not_minus_gt_zero";
   704 
   705 Goalw [real_zero_def] "0r < %#m";
   706 by (auto_tac (claset(),
   707 	      simpset() addsimps [real_preal_def,real_less_def,real_minus]));
   708 by (REPEAT(rtac exI 1));
   709 by (EVERY[rtac conjI 1, rtac conjI 2]);
   710 by (REPEAT(Blast_tac 2));
   711 by (full_simp_tac (simpset() addsimps 
   712 		   [preal_self_less_add_right] @ preal_add_ac) 1);
   713 qed "real_preal_zero_less";
   714 
   715 Goal "~ %#m < 0r";
   716 by (cut_facts_tac [real_preal_zero_less] 1);
   717 by (blast_tac (claset() addDs [real_less_trans] 
   718                addEs [real_less_irrefl]) 1);
   719 qed "real_preal_not_less_zero";
   720 
   721 Goal "0r < - - %#m";
   722 by (simp_tac (simpset() addsimps 
   723     [real_preal_zero_less]) 1);
   724 qed "real_minus_minus_zero_less";
   725 
   726 (* another lemma *)
   727 Goalw [real_zero_def] "0r < %#m + %#m1";
   728 by (auto_tac (claset(),
   729 	      simpset() addsimps [real_preal_def,real_less_def,real_add]));
   730 by (REPEAT(rtac exI 1));
   731 by (EVERY[rtac conjI 1, rtac conjI 2]);
   732 by (REPEAT(Blast_tac 2));
   733 by (full_simp_tac (simpset() addsimps preal_add_ac) 1);
   734 by (full_simp_tac (simpset() addsimps [preal_self_less_add_right,
   735     preal_add_assoc RS sym]) 1);
   736 qed "real_preal_sum_zero_less";
   737 
   738 Goal "- %#m < %#m1";
   739 by (auto_tac (claset(),
   740 	      simpset() addsimps [real_preal_def,real_less_def,real_minus]));
   741 by (REPEAT(rtac exI 1));
   742 by (EVERY[rtac conjI 1, rtac conjI 2]);
   743 by (REPEAT(Blast_tac 2));
   744 by (full_simp_tac (simpset() addsimps preal_add_ac) 1);
   745 by (full_simp_tac (simpset() addsimps [preal_self_less_add_right,
   746     preal_add_assoc RS sym]) 1);
   747 qed "real_preal_minus_less_all";
   748 
   749 Goal "~ %#m < - %#m1";
   750 by (cut_facts_tac [real_preal_minus_less_all] 1);
   751 by (blast_tac (claset() addDs [real_less_trans] 
   752                addEs [real_less_irrefl]) 1);
   753 qed "real_preal_not_minus_gt_all";
   754 
   755 Goal "- %#m1 < - %#m2 ==> %#m2 < %#m1";
   756 by (auto_tac (claset(),
   757 	      simpset() addsimps [real_preal_def,real_less_def,real_minus]));
   758 by (REPEAT(rtac exI 1));
   759 by (EVERY[rtac conjI 1, rtac conjI 2]);
   760 by (REPEAT(Blast_tac 2));
   761 by (auto_tac (claset(),simpset() addsimps preal_add_ac));
   762 by (asm_full_simp_tac (simpset() addsimps [preal_add_assoc RS sym]) 1);
   763 by (auto_tac (claset(),simpset() addsimps preal_add_ac));
   764 qed "real_preal_minus_less_rev1";
   765 
   766 Goal "%#m1 < %#m2 ==> - %#m2 < - %#m1";
   767 by (auto_tac (claset(),
   768 	      simpset() addsimps [real_preal_def,real_less_def,real_minus]));
   769 by (REPEAT(rtac exI 1));
   770 by (EVERY[rtac conjI 1, rtac conjI 2]);
   771 by (REPEAT(Blast_tac 2));
   772 by (auto_tac (claset(),simpset() addsimps preal_add_ac));
   773 by (asm_full_simp_tac (simpset() addsimps [preal_add_assoc RS sym]) 1);
   774 by (auto_tac (claset(),simpset() addsimps preal_add_ac));
   775 qed "real_preal_minus_less_rev2";
   776 
   777 Goal "(- %#m1 < - %#m2) = (%#m2 < %#m1)";
   778 by (blast_tac (claset() addSIs [real_preal_minus_less_rev1,
   779                real_preal_minus_less_rev2]) 1);
   780 qed "real_preal_minus_less_rev_iff";
   781 
   782 Addsimps [real_preal_minus_less_rev_iff];
   783 
   784 (*** linearity ***)
   785 Goal "(R1::real) < R2 | R1 = R2 | R2 < R1";
   786 by (res_inst_tac [("x","R1")]  real_preal_trichotomyE 1);
   787 by (ALLGOALS(res_inst_tac [("x","R2")]  real_preal_trichotomyE));
   788 by (auto_tac (claset() addSDs [preal_le_anti_sym],
   789               simpset() addsimps [preal_less_le_iff,real_preal_minus_less_zero,
   790                real_preal_zero_less,real_preal_minus_less_all]));
   791 qed "real_linear";
   792 
   793 Goal "!!w::real. (w ~= z) = (w<z | z<w)";
   794 by (cut_facts_tac [real_linear] 1);
   795 by (Blast_tac 1);
   796 qed "real_neq_iff";
   797 
   798 Goal "!!(R1::real). [| R1 < R2 ==> P;  R1 = R2 ==> P; \
   799 \                      R2 < R1 ==> P |] ==> P";
   800 by (cut_inst_tac [("R1.0","R1"),("R2.0","R2")] real_linear 1);
   801 by Auto_tac;
   802 qed "real_linear_less2";
   803 
   804 (*** Properties of <= ***)
   805 
   806 Goalw [real_le_def] "~(w < z) ==> z <= (w::real)";
   807 by (assume_tac 1);
   808 qed "real_leI";
   809 
   810 Goalw [real_le_def] "z<=w ==> ~(w<(z::real))";
   811 by (assume_tac 1);
   812 qed "real_leD";
   813 
   814 val real_leE = make_elim real_leD;
   815 
   816 Goal "(~(w < z)) = (z <= (w::real))";
   817 by (blast_tac (claset() addSIs [real_leI,real_leD]) 1);
   818 qed "real_less_le_iff";
   819 
   820 Goalw [real_le_def] "~ z <= w ==> w<(z::real)";
   821 by (Blast_tac 1);
   822 qed "not_real_leE";
   823 
   824 Goalw [real_le_def] "z < w ==> z <= (w::real)";
   825 by (blast_tac (claset() addEs [real_less_asym]) 1);
   826 qed "real_less_imp_le";
   827 
   828 Goalw [real_le_def] "!!(x::real). x <= y ==> x < y | x = y";
   829 by (cut_facts_tac [real_linear] 1);
   830 by (blast_tac (claset() addEs [real_less_irrefl,real_less_asym]) 1);
   831 qed "real_le_imp_less_or_eq";
   832 
   833 Goalw [real_le_def] "z<w | z=w ==> z <=(w::real)";
   834 by (cut_facts_tac [real_linear] 1);
   835 by (fast_tac (claset() addEs [real_less_irrefl,real_less_asym]) 1);
   836 qed "real_less_or_eq_imp_le";
   837 
   838 Goal "(x <= (y::real)) = (x < y | x=y)";
   839 by (REPEAT(ares_tac [iffI, real_less_or_eq_imp_le, real_le_imp_less_or_eq] 1));
   840 qed "real_le_less";
   841 
   842 Goal "w <= (w::real)";
   843 by (simp_tac (simpset() addsimps [real_le_less]) 1);
   844 qed "real_le_refl";
   845 
   846 AddIffs [real_le_refl];
   847 
   848 (* Axiom 'linorder_linear' of class 'linorder': *)
   849 Goal "(z::real) <= w | w <= z";
   850 by (simp_tac (simpset() addsimps [real_le_less]) 1);
   851 by (cut_facts_tac [real_linear] 1);
   852 by (Blast_tac 1);
   853 qed "real_le_linear";
   854 
   855 Goal "[| i <= j; j < k |] ==> i < (k::real)";
   856 by (dtac real_le_imp_less_or_eq 1);
   857 by (blast_tac (claset() addIs [real_less_trans]) 1);
   858 qed "real_le_less_trans";
   859 
   860 Goal "!! (i::real). [| i < j; j <= k |] ==> i < k";
   861 by (dtac real_le_imp_less_or_eq 1);
   862 by (blast_tac (claset() addIs [real_less_trans]) 1);
   863 qed "real_less_le_trans";
   864 
   865 Goal "[| i <= j; j <= k |] ==> i <= (k::real)";
   866 by (EVERY1 [dtac real_le_imp_less_or_eq, dtac real_le_imp_less_or_eq,
   867             rtac real_less_or_eq_imp_le, blast_tac (claset() addIs [real_less_trans])]);
   868 qed "real_le_trans";
   869 
   870 Goal "[| z <= w; w <= z |] ==> z = (w::real)";
   871 by (EVERY1 [dtac real_le_imp_less_or_eq, dtac real_le_imp_less_or_eq,
   872             fast_tac (claset() addEs [real_less_irrefl,real_less_asym])]);
   873 qed "real_le_anti_sym";
   874 
   875 Goal "[| ~ y < x; y ~= x |] ==> x < (y::real)";
   876 by (rtac not_real_leE 1);
   877 by (blast_tac (claset() addDs [real_le_imp_less_or_eq]) 1);
   878 qed "not_less_not_eq_real_less";
   879 
   880 (* Axiom 'order_less_le' of class 'order': *)
   881 Goal "(w::real) < z = (w <= z & w ~= z)";
   882 by (simp_tac (simpset() addsimps [real_le_def, real_neq_iff]) 1);
   883 by (blast_tac (claset() addSEs [real_less_asym]) 1);
   884 qed "real_less_le";
   885 
   886 
   887 Goal "(0r < -R) = (R < 0r)";
   888 by (res_inst_tac [("x","R")]  real_preal_trichotomyE 1);
   889 by (auto_tac (claset(),
   890 	      simpset() addsimps [real_preal_not_minus_gt_zero,
   891                         real_preal_not_less_zero,real_preal_zero_less,
   892                         real_preal_minus_less_zero]));
   893 qed "real_minus_zero_less_iff";
   894 
   895 Addsimps [real_minus_zero_less_iff];
   896 
   897 Goal "(-R < 0r) = (0r < R)";
   898 by (res_inst_tac [("x","R")]  real_preal_trichotomyE 1);
   899 by (auto_tac (claset(),
   900 	      simpset() addsimps [real_preal_not_minus_gt_zero,
   901                         real_preal_not_less_zero,real_preal_zero_less,
   902                         real_preal_minus_less_zero]));
   903 qed "real_minus_zero_less_iff2";
   904 
   905 
   906 (*Alternative definition for real_less*)
   907 Goal "!!(R::real). R < S ==> ? T. 0r < T & R + T = S";
   908 by (res_inst_tac [("x","R")]  real_preal_trichotomyE 1);
   909 by (ALLGOALS(res_inst_tac [("x","S")]  real_preal_trichotomyE));
   910 by (auto_tac (claset() addSDs [preal_less_add_left_Ex],
   911 	      simpset() addsimps [real_preal_not_minus_gt_all,
   912 				  real_preal_add, real_preal_not_less_zero,
   913 				  real_less_not_refl,
   914 				  real_preal_not_minus_gt_zero]));
   915 by (res_inst_tac [("x","%#D")] exI 1);
   916 by (res_inst_tac [("x","%#m+%#ma")] exI 2);
   917 by (res_inst_tac [("x","%#m")] exI 3);
   918 by (res_inst_tac [("x","%#D")] exI 4);
   919 by (auto_tac (claset(),
   920 	      simpset() addsimps [real_preal_zero_less,
   921 				  real_preal_sum_zero_less,real_add_assoc]));
   922 qed "real_less_add_positive_left_Ex";
   923 
   924 
   925 
   926 (** change naff name(s)! **)
   927 Goal "(W < S) ==> (0r < S + -W)";
   928 by (dtac real_less_add_positive_left_Ex 1);
   929 by (auto_tac (claset(),
   930 	      simpset() addsimps [real_add_minus,
   931     real_add_zero_right] @ real_add_ac));
   932 qed "real_less_sum_gt_zero";
   933 
   934 Goal "!!S::real. T = S + W ==> S = T + -W";
   935 by (asm_simp_tac (simpset() addsimps real_add_ac) 1);
   936 qed "real_lemma_change_eq_subj";
   937 
   938 (* FIXME: long! *)
   939 Goal "(0r < S + -W) ==> (W < S)";
   940 by (rtac ccontr 1);
   941 by (dtac (real_leI RS real_le_imp_less_or_eq) 1);
   942 by (auto_tac (claset(),
   943 	      simpset() addsimps [real_less_not_refl]));
   944 by (EVERY1[dtac real_less_add_positive_left_Ex, etac exE, etac conjE]);
   945 by (Asm_full_simp_tac 1);
   946 by (dtac real_lemma_change_eq_subj 1);
   947 by Auto_tac;
   948 by (dtac real_less_sum_gt_zero 1);
   949 by (asm_full_simp_tac (simpset() addsimps real_add_ac) 1);
   950 by (EVERY1[rotate_tac 1, dtac (real_add_left_commute RS ssubst)]);
   951 by (auto_tac (claset() addEs [real_less_asym], simpset()));
   952 qed "real_sum_gt_zero_less";
   953 
   954 Goal "(0r < S + -W) = (W < S)";
   955 by (blast_tac (claset() addIs [real_less_sum_gt_zero,
   956 			       real_sum_gt_zero_less]) 1);
   957 qed "real_less_sum_gt_0_iff";
   958 
   959 
   960 Goalw [real_diff_def] "(x<y) = (x-y < 0r)";
   961 by (stac (real_minus_zero_less_iff RS sym) 1);
   962 by (simp_tac (simpset() addsimps [real_add_commute,
   963 				  real_less_sum_gt_0_iff]) 1);
   964 qed "real_less_eq_diff";
   965 
   966 
   967 (*** Subtraction laws ***)
   968 
   969 Goal "x + (y - z) = (x + y) - (z::real)";
   970 by (simp_tac (simpset() addsimps real_diff_def::real_add_ac) 1);
   971 qed "real_add_diff_eq";
   972 
   973 Goal "(x - y) + z = (x + z) - (y::real)";
   974 by (simp_tac (simpset() addsimps real_diff_def::real_add_ac) 1);
   975 qed "real_diff_add_eq";
   976 
   977 Goal "(x - y) - z = x - (y + (z::real))";
   978 by (simp_tac (simpset() addsimps real_diff_def::real_add_ac) 1);
   979 qed "real_diff_diff_eq";
   980 
   981 Goal "x - (y - z) = (x + z) - (y::real)";
   982 by (simp_tac (simpset() addsimps real_diff_def::real_add_ac) 1);
   983 qed "real_diff_diff_eq2";
   984 
   985 Goal "(x-y < z) = (x < z + (y::real))";
   986 by (stac real_less_eq_diff 1);
   987 by (res_inst_tac [("y1", "z")] (real_less_eq_diff RS ssubst) 1);
   988 by (simp_tac (simpset() addsimps real_diff_def::real_add_ac) 1);
   989 qed "real_diff_less_eq";
   990 
   991 Goal "(x < z-y) = (x + (y::real) < z)";
   992 by (stac real_less_eq_diff 1);
   993 by (res_inst_tac [("y1", "z-y")] (real_less_eq_diff RS ssubst) 1);
   994 by (simp_tac (simpset() addsimps real_diff_def::real_add_ac) 1);
   995 qed "real_less_diff_eq";
   996 
   997 Goalw [real_le_def] "(x-y <= z) = (x <= z + (y::real))";
   998 by (simp_tac (simpset() addsimps [real_less_diff_eq]) 1);
   999 qed "real_diff_le_eq";
  1000 
  1001 Goalw [real_le_def] "(x <= z-y) = (x + (y::real) <= z)";
  1002 by (simp_tac (simpset() addsimps [real_diff_less_eq]) 1);
  1003 qed "real_le_diff_eq";
  1004 
  1005 Goalw [real_diff_def] "(x-y = z) = (x = z + (y::real))";
  1006 by (auto_tac (claset(), simpset() addsimps [real_add_assoc]));
  1007 qed "real_diff_eq_eq";
  1008 
  1009 Goalw [real_diff_def] "(x = z-y) = (x + (y::real) = z)";
  1010 by (auto_tac (claset(), simpset() addsimps [real_add_assoc]));
  1011 qed "real_eq_diff_eq";
  1012 
  1013 (*This list of rewrites simplifies (in)equalities by bringing subtractions
  1014   to the top and then moving negative terms to the other side.  
  1015   Use with real_add_ac*)
  1016 val real_compare_rls = 
  1017   [symmetric real_diff_def,
  1018    real_add_diff_eq, real_diff_add_eq, real_diff_diff_eq, real_diff_diff_eq2, 
  1019    real_diff_less_eq, real_less_diff_eq, real_diff_le_eq, real_le_diff_eq, 
  1020    real_diff_eq_eq, real_eq_diff_eq];
  1021 
  1022 
  1023 (** For the cancellation simproc.
  1024     The idea is to cancel like terms on opposite sides by subtraction **)
  1025 
  1026 Goal "(x::real) - y = x' - y' ==> (x<y) = (x'<y')";
  1027 by (stac real_less_eq_diff 1);
  1028 by (res_inst_tac [("y1", "y")] (real_less_eq_diff RS ssubst) 1);
  1029 by (Asm_simp_tac 1);
  1030 qed "real_less_eqI";
  1031 
  1032 Goal "(x::real) - y = x' - y' ==> (y<=x) = (y'<=x')";
  1033 by (dtac real_less_eqI 1);
  1034 by (asm_simp_tac (simpset() addsimps [real_le_def]) 1);
  1035 qed "real_le_eqI";
  1036 
  1037 Goal "(x::real) - y = x' - y' ==> (x=y) = (x'=y')";
  1038 by Safe_tac;
  1039 by (ALLGOALS
  1040     (asm_full_simp_tac
  1041      (simpset() addsimps [real_eq_diff_eq, real_diff_eq_eq])));
  1042 qed "real_eq_eqI";