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