helm/software/matita/contribs/CoRN-Procedural/reals/Max_AbsIR.mma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* This file was automatically generated: do not edit *********************)
  16
  17 include "CoRN.ma".
  18
  19 (* $Id: Max_AbsIR.v,v 1.13 2004/04/23 10:01:04 lcf Exp $ *)
  20
  21 (*#* printing Max %\ensuremath{\max}% *)
  22
  23 (*#* printing Min %\ensuremath{\min}% *)
  24
  25 include "reals/CauchySeq.ma".
  26
  27 (* UNEXPORTED
  28 Section Maximum
  29 *)
  30
  31 (* UNEXPORTED
  32 Section Max_function
  33 *)
  34
  35 (*#* ** Maximum, Minimum and Absolute Value
  36
  37 %\begin{convention}%
  38 Let [x] and [y] be reals
  39 (we will define the maximum of [x] and [y]).
  40 %\end{convention}%
  41 *)
  42
  43 alias id "x" = "cic:/CoRN/reals/Max_AbsIR/Maximum/Max_function/x.var".
  44
  45 alias id "y" = "cic:/CoRN/reals/Max_AbsIR/Maximum/Max_function/y.var".
  46
  47 inline procedural "cic:/CoRN/reals/Max_AbsIR/Max_seq.con".
  48
  49 inline procedural "cic:/CoRN/reals/Max_AbsIR/Max_seq_char.con".
  50
  51 inline procedural "cic:/CoRN/reals/Max_AbsIR/Cauchy_Max_seq.con".
  52
  53 inline procedural "cic:/CoRN/reals/Max_AbsIR/Max_CauchySeq.con".
  54
  55 inline procedural "cic:/CoRN/reals/Max_AbsIR/MAX.con".
  56
  57 (*#*
  58 Constructively, the elementary properties of the maximum function are:
  59 - [x [<=] Max (x,y)],
  60 - [x [<=] Max (y,x)],
  61 - [z [<] Max(x,y) -> z [<] x or z [<] y].
  62
  63 (This can be more concisely expressed as
  64 [z [<] Max(x,y) Iff z [<] x or z [<] y]).
  65 From these elementary properties we can prove all other properties, including
  66 strong extensionality.
  67 With strong extensionality, we can make the binary operation [Max].
  68 (So [Max] is [MAX] coupled with some proofs.)
  69 *)
  70
  71 inline procedural "cic:/CoRN/reals/Max_AbsIR/lft_leEq_MAX.con".
  72
  73 inline procedural "cic:/CoRN/reals/Max_AbsIR/rht_leEq_MAX.con".
  74
  75 inline procedural "cic:/CoRN/reals/Max_AbsIR/less_MAX_imp.con".
  76
  77 (* UNEXPORTED
  78 End Max_function
  79 *)
  80
  81 inline procedural "cic:/CoRN/reals/Max_AbsIR/MAX_strext.con".
  82
  83 inline procedural "cic:/CoRN/reals/Max_AbsIR/MAX_wd.con".
  84
  85 (* UNEXPORTED
  86 Section properties_of_Max
  87 *)
  88
  89 (*#* *** Maximum *)
  90
  91 inline procedural "cic:/CoRN/reals/Max_AbsIR/Max.con".
  92
  93 inline procedural "cic:/CoRN/reals/Max_AbsIR/Max_wd_unfolded.con".
  94
  95 inline procedural "cic:/CoRN/reals/Max_AbsIR/lft_leEq_Max.con".
  96
  97 inline procedural "cic:/CoRN/reals/Max_AbsIR/rht_leEq_Max.con".
  98
  99 inline procedural "cic:/CoRN/reals/Max_AbsIR/less_Max_imp.con".
 100
 101 inline procedural "cic:/CoRN/reals/Max_AbsIR/Max_leEq.con".
 102
 103 inline procedural "cic:/CoRN/reals/Max_AbsIR/Max_less.con".
 104
 105 inline procedural "cic:/CoRN/reals/Max_AbsIR/equiv_imp_eq_max.con".
 106
 107 inline procedural "cic:/CoRN/reals/Max_AbsIR/Max_id.con".
 108
 109 inline procedural "cic:/CoRN/reals/Max_AbsIR/Max_comm.con".
 110
 111 inline procedural "cic:/CoRN/reals/Max_AbsIR/leEq_imp_Max_is_rht.con".
 112
 113 inline procedural "cic:/CoRN/reals/Max_AbsIR/Max_is_rht_imp_leEq.con".
 114
 115 inline procedural "cic:/CoRN/reals/Max_AbsIR/Max_minus_eps_leEq.con".
 116
 117 inline procedural "cic:/CoRN/reals/Max_AbsIR/max_one_ap_zero.con".
 118
 119 inline procedural "cic:/CoRN/reals/Max_AbsIR/pos_max_one.con".
 120
 121 inline procedural "cic:/CoRN/reals/Max_AbsIR/x_div_Max_leEq_x.con".
 122
 123 (* UNEXPORTED
 124 End properties_of_Max
 125 *)
 126
 127 (* UNEXPORTED
 128 End Maximum
 129 *)
 130
 131 (* UNEXPORTED
 132 Hint Resolve Max_id: algebra.
 133 *)
 134
 135 (* UNEXPORTED
 136 Section Minimum
 137 *)
 138
 139 (*#* *** Mininum
 140
 141 The minimum is defined by the formula
 142 [Min(x,y) [=] [--]Max( [--]x,[--]y)].
 143 *)
 144
 145 inline procedural "cic:/CoRN/reals/Max_AbsIR/MIN.con".
 146
 147 inline procedural "cic:/CoRN/reals/Max_AbsIR/MIN_wd.con".
 148
 149 inline procedural "cic:/CoRN/reals/Max_AbsIR/MIN_strext.con".
 150
 151 inline procedural "cic:/CoRN/reals/Max_AbsIR/Min.con".
 152
 153 inline procedural "cic:/CoRN/reals/Max_AbsIR/Min_wd_unfolded.con".
 154
 155 inline procedural "cic:/CoRN/reals/Max_AbsIR/Min_strext_unfolded.con".
 156
 157 inline procedural "cic:/CoRN/reals/Max_AbsIR/Min_leEq_lft.con".
 158
 159 inline procedural "cic:/CoRN/reals/Max_AbsIR/Min_leEq_rht.con".
 160
 161 inline procedural "cic:/CoRN/reals/Max_AbsIR/Min_less_imp.con".
 162
 163 inline procedural "cic:/CoRN/reals/Max_AbsIR/leEq_Min.con".
 164
 165 inline procedural "cic:/CoRN/reals/Max_AbsIR/less_Min.con".
 166
 167 inline procedural "cic:/CoRN/reals/Max_AbsIR/equiv_imp_eq_min.con".
 168
 169 inline procedural "cic:/CoRN/reals/Max_AbsIR/Min_id.con".
 170
 171 inline procedural "cic:/CoRN/reals/Max_AbsIR/Min_comm.con".
 172
 173 inline procedural "cic:/CoRN/reals/Max_AbsIR/leEq_imp_Min_is_lft.con".
 174
 175 inline procedural "cic:/CoRN/reals/Max_AbsIR/Min_is_lft_imp_leEq.con".
 176
 177 inline procedural "cic:/CoRN/reals/Max_AbsIR/leEq_Min_plus_eps.con".
 178
 179 alias id "a" = "cic:/CoRN/reals/Max_AbsIR/Minimum/a.var".
 180
 181 alias id "b" = "cic:/CoRN/reals/Max_AbsIR/Minimum/b.var".
 182
 183 inline procedural "cic:/CoRN/reals/Max_AbsIR/Min_leEq_Max.con".
 184
 185 inline procedural "cic:/CoRN/reals/Max_AbsIR/Min_leEq_Max'.con".
 186
 187 inline procedural "cic:/CoRN/reals/Max_AbsIR/Min3_leEq_Max3.con".
 188
 189 inline procedural "cic:/CoRN/reals/Max_AbsIR/Min_less_Max.con".
 190
 191 inline procedural "cic:/CoRN/reals/Max_AbsIR/ap_imp_Min_less_Max.con".
 192
 193 inline procedural "cic:/CoRN/reals/Max_AbsIR/Min_less_Max_imp_ap.con".
 194
 195 (* UNEXPORTED
 196 End Minimum
 197 *)
 198
 199 (*#**********************************)
 200
 201 (* UNEXPORTED
 202 Section Absolute
 203 *)
 204
 205 (*#**********************************)
 206
 207 (*#* *** Absolute value *)
 208
 209 inline procedural "cic:/CoRN/reals/Max_AbsIR/ABSIR.con".
 210
 211 inline procedural "cic:/CoRN/reals/Max_AbsIR/ABSIR_strext.con".
 212
 213 inline procedural "cic:/CoRN/reals/Max_AbsIR/ABSIR_wd.con".
 214
 215 inline procedural "cic:/CoRN/reals/Max_AbsIR/AbsIR.con".
 216
 217 inline procedural "cic:/CoRN/reals/Max_AbsIR/AbsIR_wd.con".
 218
 219 inline procedural "cic:/CoRN/reals/Max_AbsIR/AbsIR_wdl.con".
 220
 221 inline procedural "cic:/CoRN/reals/Max_AbsIR/AbsIR_wdr.con".
 222
 223 inline procedural "cic:/CoRN/reals/Max_AbsIR/AbsIRz_isz.con".
 224
 225 inline procedural "cic:/CoRN/reals/Max_AbsIR/AbsIR_nonneg.con".
 226
 227 inline procedural "cic:/CoRN/reals/Max_AbsIR/AbsIR_pos.con".
 228
 229 inline procedural "cic:/CoRN/reals/Max_AbsIR/AbsIR_cancel_ap_zero.con".
 230
 231 inline procedural "cic:/CoRN/reals/Max_AbsIR/AbsIR_resp_ap_zero.con".
 232
 233 inline procedural "cic:/CoRN/reals/Max_AbsIR/leEq_AbsIR.con".
 234
 235 inline procedural "cic:/CoRN/reals/Max_AbsIR/inv_leEq_AbsIR.con".
 236
 237 inline procedural "cic:/CoRN/reals/Max_AbsIR/AbsSmall_e.con".
 238
 239 inline procedural "cic:/CoRN/reals/Max_AbsIR/AbsSmall_imp_AbsIR.con".
 240
 241 inline procedural "cic:/CoRN/reals/Max_AbsIR/AbsIR_eq_AbsSmall.con".
 242
 243 inline procedural "cic:/CoRN/reals/Max_AbsIR/AbsIR_imp_AbsSmall.con".
 244
 245 inline procedural "cic:/CoRN/reals/Max_AbsIR/AbsSmall_transitive.con".
 246
 247 inline procedural "cic:/CoRN/reals/Max_AbsIR/zero_less_AbsIR_plus_one.con".
 248
 249 inline procedural "cic:/CoRN/reals/Max_AbsIR/AbsIR_inv.con".
 250
 251 inline procedural "cic:/CoRN/reals/Max_AbsIR/AbsIR_minus.con".
 252
 253 inline procedural "cic:/CoRN/reals/Max_AbsIR/AbsIR_eq_x.con".
 254
 255 inline procedural "cic:/CoRN/reals/Max_AbsIR/AbsIR_eq_inv_x.con".
 256
 257 inline procedural "cic:/CoRN/reals/Max_AbsIR/less_AbsIR.con".
 258
 259 inline procedural "cic:/CoRN/reals/Max_AbsIR/leEq_distr_AbsIR.con".
 260
 261 inline procedural "cic:/CoRN/reals/Max_AbsIR/AbsIR_approach_zero.con".
 262
 263 inline procedural "cic:/CoRN/reals/Max_AbsIR/AbsIR_eq_zero.con".
 264
 265 inline procedural "cic:/CoRN/reals/Max_AbsIR/Abs_Max.con".
 266
 267 inline procedural "cic:/CoRN/reals/Max_AbsIR/AbsIR_str_bnd.con".
 268
 269 inline procedural "cic:/CoRN/reals/Max_AbsIR/AbsIR_bnd.con".
 270
 271 (* UNEXPORTED
 272 End Absolute
 273 *)
 274
 275 (* UNEXPORTED
 276 Hint Resolve AbsIRz_isz: algebra.
 277 *)
 278
 279 (* UNEXPORTED
 280 Section Part_Function_Max
 281 *)
 282
 283 (*#* *** Functional Operators
 284
 285 The existence of these operators allows us to lift them to functions.  We will define the maximum, minimum and absolute value of two partial functions.
 286
 287 %\begin{convention}%
 288 Let [F,G:PartIR] and denote by [P] and [Q] their respective domains.
 289 %\end{convention}%
 290 *)
 291
 292 alias id "F" = "cic:/CoRN/reals/Max_AbsIR/Part_Function_Max/F.var".
 293
 294 alias id "G" = "cic:/CoRN/reals/Max_AbsIR/Part_Function_Max/G.var".
 295
 296 (* begin hide *)
 297
 298 inline procedural "cic:/CoRN/reals/Max_AbsIR/Part_Function_Max/P.con" "Part_Function_Max__".
 299
 300 inline procedural "cic:/CoRN/reals/Max_AbsIR/Part_Function_Max/Q.con" "Part_Function_Max__".
 301
 302 (* end hide *)
 303
 304 inline procedural "cic:/CoRN/reals/Max_AbsIR/part_function_Max_strext.con".
 305
 306 inline procedural "cic:/CoRN/reals/Max_AbsIR/FMax.con".
 307
 308 (* UNEXPORTED
 309 End Part_Function_Max
 310 *)
 311
 312 (* UNEXPORTED
 313 Section Part_Function_Abs
 314 *)
 315
 316 alias id "F" = "cic:/CoRN/reals/Max_AbsIR/Part_Function_Abs/F.var".
 317
 318 alias id "G" = "cic:/CoRN/reals/Max_AbsIR/Part_Function_Abs/G.var".
 319
 320 (* begin hide *)
 321
 322 inline procedural "cic:/CoRN/reals/Max_AbsIR/Part_Function_Abs/P.con" "Part_Function_Abs__".
 323
 324 inline procedural "cic:/CoRN/reals/Max_AbsIR/Part_Function_Abs/Q.con" "Part_Function_Abs__".
 325
 326 (* end hide *)
 327
 328 inline procedural "cic:/CoRN/reals/Max_AbsIR/FMin.con".
 329
 330 inline procedural "cic:/CoRN/reals/Max_AbsIR/FAbs.con".
 331
 332 (* UNEXPORTED
 333 Opaque Max.
 334 *)
 335
 336 inline procedural "cic:/CoRN/reals/Max_AbsIR/FMin_char.con".
 337
 338 (* UNEXPORTED
 339 Transparent Max.
 340 *)
 341
 342 inline procedural "cic:/CoRN/reals/Max_AbsIR/FAbs_char.con".
 343
 344 (* UNEXPORTED
 345 End Part_Function_Abs
 346 *)
 347
 348 (* UNEXPORTED
 349 Hint Resolve FAbs_char: algebra.
 350 *)
 351
 352 inline procedural "cic:/CoRN/reals/Max_AbsIR/FAbs_char'.con".
 353
 354 inline procedural "cic:/CoRN/reals/Max_AbsIR/FAbs_nonneg.con".
 355
 356 (* UNEXPORTED
 357 Hint Resolve FAbs_char': algebra.
 358 *)
 359
 360 (* UNEXPORTED
 361 Section Inclusion
 362 *)
 363
 364 alias id "F" = "cic:/CoRN/reals/Max_AbsIR/Inclusion/F.var".
 365
 366 alias id "G" = "cic:/CoRN/reals/Max_AbsIR/Inclusion/G.var".
 367
 368 (* begin hide *)
 369
 370 inline procedural "cic:/CoRN/reals/Max_AbsIR/Inclusion/P.con" "Inclusion__".
 371
 372 inline procedural "cic:/CoRN/reals/Max_AbsIR/Inclusion/Q.con" "Inclusion__".
 373
 374 (* end hide *)
 375
 376 (*#*
 377 %\begin{convention}% Let [R:IR->CProp].
 378 %\end{convention}%
 379 *)
 380
 381 alias id "R" = "cic:/CoRN/reals/Max_AbsIR/Inclusion/R.var".
 382
 383 inline procedural "cic:/CoRN/reals/Max_AbsIR/included_FMax.con".
 384
 385 inline procedural "cic:/CoRN/reals/Max_AbsIR/included_FMax'.con".
 386
 387 inline procedural "cic:/CoRN/reals/Max_AbsIR/included_FMax''.con".
 388
 389 inline procedural "cic:/CoRN/reals/Max_AbsIR/included_FMin.con".
 390
 391 inline procedural "cic:/CoRN/reals/Max_AbsIR/included_FMin'.con".
 392
 393 inline procedural "cic:/CoRN/reals/Max_AbsIR/included_FMin''.con".
 394
 395 inline procedural "cic:/CoRN/reals/Max_AbsIR/included_FAbs.con".
 396
 397 inline procedural "cic:/CoRN/reals/Max_AbsIR/included_FAbs'.con".
 398
 399 (* UNEXPORTED
 400 End Inclusion
 401 *)
 402
 403 (* UNEXPORTED
 404 Hint Resolve included_FMax included_FMin included_FAbs : included.
 405 *)
 406
 407 (* UNEXPORTED
 408 Hint Immediate included_FMax' included_FMin' included_FAbs'
 409   included_FMax'' included_FMin'' : included.
 410 *)
 411