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