helm/software/matita/contribs/procedural/CoRN/reals/Bridges_iso.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 (* begin hide *)
  20
  21 (* file        : bridges_gives_our.v                               *)
  22
  23 (* version     : 1.50 - 09/05/2001                                 *)
  24
  25 (* version     : 1.00 - 09/03/2001                                 *)
  26
  27 (* author      : Milad Niqui                                       *)
  28
  29 (* language    : coq7.0bet26feb                                    *)
  30
  31 (* dependency  : least_upper_bound_principle                       *)
  32
  33 (* description : Bridges' proof of Cauchy completeness in TCS-219  *)
  34
  35 include "reals/Bridges_LUB.ma".
  36
  37 (* This lemma comes from lemmas.v of Martijn Oostdijk *)
  38
  39 inline procedural "cic:/CoRN/reals/Bridges_iso/le_witness_informative.con" as lemma.
  40
  41 (* UNEXPORTED
  42 Section bridges_axioms_imply_ours
  43 *)
  44
  45 (* UNEXPORTED
  46 cic:/CoRN/reals/Bridges_iso/bridges_axioms_imply_ours/OF.var
  47 *)
  48
  49 (* UNEXPORTED
  50 cic:/CoRN/reals/Bridges_iso/bridges_axioms_imply_ours/lubp.var
  51 *)
  52
  53 (* UNEXPORTED
  54 cic:/CoRN/reals/Bridges_iso/bridges_axioms_imply_ours/is_Archimedes.var
  55 *)
  56
  57 inline procedural "cic:/CoRN/reals/Bridges_iso/is_Archimedes'.con" as lemma.
  58
  59 (* UNEXPORTED
  60 Section proofs_in_TCS
  61 *)
  62
  63 inline procedural "cic:/CoRN/reals/Bridges_iso/leEq_geEq.con" as lemma.
  64
  65 inline procedural "cic:/CoRN/reals/Bridges_iso/glbp.con" as theorem.
  66
  67 (* UNEXPORTED
  68 Section supremum
  69 *)
  70
  71 (* UNEXPORTED
  72 cic:/CoRN/reals/Bridges_iso/bridges_axioms_imply_ours/proofs_in_TCS/supremum/P.var
  73 *)
  74
  75 inline procedural "cic:/CoRN/reals/Bridges_iso/inequality1.con" as lemma.
  76
  77 inline procedural "cic:/CoRN/reals/Bridges_iso/inequality2.con" as lemma.
  78
  79 inline procedural "cic:/CoRN/reals/Bridges_iso/inequality3.con" as lemma.
  80
  81 inline procedural "cic:/CoRN/reals/Bridges_iso/inequality4.con" as lemma.
  82
  83 inline procedural "cic:/CoRN/reals/Bridges_iso/Hum.con" as definition.
  84
  85 inline procedural "cic:/CoRN/reals/Bridges_iso/bound_tk1.con" as lemma.
  86
  87 inline procedural "cic:/CoRN/reals/Bridges_iso/bound_tk2.con" as lemma.
  88
  89 inline procedural "cic:/CoRN/reals/Bridges_iso/trick.con" as lemma.
  90
  91 inline procedural "cic:/CoRN/reals/Bridges_iso/trick'.con" as lemma.
  92
  93 inline procedural "cic:/CoRN/reals/Bridges_iso/up_bound_for_n_element.con" as theorem.
  94
  95 inline procedural "cic:/CoRN/reals/Bridges_iso/low_bound_for_n_element.con" as lemma.
  96
  97 inline procedural "cic:/CoRN/reals/Bridges_iso/saghf.con" as definition.
  98
  99 inline procedural "cic:/CoRN/reals/Bridges_iso/Psaghf.con" as lemma.
 100
 101 inline procedural "cic:/CoRN/reals/Bridges_iso/kaf.con" as definition.
 102
 103 inline procedural "cic:/CoRN/reals/Bridges_iso/Pkaf.con" as lemma.
 104
 105 (* UNEXPORTED
 106 cic:/CoRN/reals/Bridges_iso/bridges_axioms_imply_ours/proofs_in_TCS/supremum/is_finite_P.var
 107 *)
 108
 109 inline procedural "cic:/CoRN/reals/Bridges_iso/card.con" as definition.
 110
 111 inline procedural "cic:/CoRN/reals/Bridges_iso/Pcard1.con" as lemma.
 112
 113 inline procedural "cic:/CoRN/reals/Bridges_iso/seq.con" as definition.
 114
 115 inline procedural "cic:/CoRN/reals/Bridges_iso/Pseq1.con" as definition.
 116
 117 inline procedural "cic:/CoRN/reals/Bridges_iso/Pseq1_unfolded.con" as lemma.
 118
 119 inline procedural "cic:/CoRN/reals/Bridges_iso/indeks.con" as definition.
 120
 121 inline procedural "cic:/CoRN/reals/Bridges_iso/Pindeks.con" as lemma.
 122
 123 (* UNEXPORTED
 124 cic:/CoRN/reals/Bridges_iso/bridges_axioms_imply_ours/proofs_in_TCS/supremum/is_onto_seq_P.var
 125 *)
 126
 127 inline procedural "cic:/CoRN/reals/Bridges_iso/P_is_inhabited.con" as lemma.
 128
 129 (*
 130 Lemma bounded_quantifier:(N:nat;phi,psi:nat->Prop)
 131                  ((m:nat)(le m N)->(phi m)\/(psi m))->
 132         ((m:nat)(le m N)->(phi m))\/(Ex [j:nat](le j N)/\(psi j)).
 133 Proof.
 134  Intros.
 135  Induction N.
 136  Cut (phi O)\/(psi O).
 137  Intro.
 138  Case H0.
 139  Intros.
 140  Left.
 141  Intros.
 142  Rewrite <- (le_n_O_eq m H2).
 143  Assumption.
 144  Intro.
 145  Right.
 146  Exists O.
 147  Split.
 148  Constructor.
 149  Assumption.
 150  Apply H.
 151  Constructor.*)
 152
 153 (* n=(S n0) *)
 154
 155 (* Case HrecN.
 156  Intros.
 157  Apply H.
 158  Apply le_trans with m:=N.
 159  Assumption.
 160  Apply le_n_Sn.
 161  Intro.
 162  Case (H (S N)).
 163  Apply le_n.
 164  Intros.
 165  Left.
 166  Intros.
 167  Case (le_lt_eq_dec m (S N)).
 168  Assumption.
 169  Intros.
 170  Apply H0.
 171  Apply (lt_n_Sm_le m N).
 172  Assumption.
 173  Intro.
 174  Rewrite e.
 175  Assumption.
 176  Intro.
 177  Right.
 178  Exists (S N).
 179  Split.
 180  Apply le_n.
 181  Assumption.
 182  Intro.
 183  Right.
 184  Case H0.
 185  Intro j.
 186  Intros.
 187  Exists j.
 188  Elim H1.
 189  Intros.
 190  Split.
 191  Apply le_trans with m:=N.
 192  Assumption.
 193  Apply le_n_Sn.
 194  Assumption.
 195 Qed.
 196 *)
 197
 198 inline procedural "cic:/CoRN/reals/Bridges_iso/bounded_quantifier_informative.con" as lemma.
 199
 200 inline procedural "cic:/CoRN/reals/Bridges_iso/bridges_lemma1a.con" as lemma.
 201
 202 (* UNEXPORTED
 203 cic:/CoRN/reals/Bridges_iso/bridges_axioms_imply_ours/proofs_in_TCS/supremum/P_is_strongly_extensional.var
 204 *)
 205
 206 inline procedural "cic:/CoRN/reals/Bridges_iso/bridges_lemma1b.con" as lemma.
 207
 208 (* UNEXPORTED
 209 End supremum
 210 *)
 211
 212 (*#**********************************)
 213
 214 (*#**********************************)
 215
 216 (*#**********************************)
 217
 218 (*#**********************************)
 219
 220 (* UNEXPORTED
 221 Section Every_Cauchy_Sequence_is_bounded
 222 *)
 223
 224 inline procedural "cic:/CoRN/reals/Bridges_iso/seq2set.con" as definition.
 225
 226 (* UNEXPORTED
 227 cic:/CoRN/reals/Bridges_iso/bridges_axioms_imply_ours/proofs_in_TCS/Every_Cauchy_Sequence_is_bounded/g.var
 228 *)
 229
 230 inline procedural "cic:/CoRN/reals/Bridges_iso/bridges_axioms_imply_ours/proofs_in_TCS/Every_Cauchy_Sequence_is_bounded/g_.con" "bridges_axioms_imply_ours__proofs_in_TCS__Every_Cauchy_Sequence_is_bounded__" as definition.
 231
 232 inline procedural "cic:/CoRN/reals/Bridges_iso/bridges_axioms_imply_ours/proofs_in_TCS/Every_Cauchy_Sequence_is_bounded/pg.con" "bridges_axioms_imply_ours__proofs_in_TCS__Every_Cauchy_Sequence_is_bounded__" as definition.
 233
 234 inline procedural "cic:/CoRN/reals/Bridges_iso/bridges_axioms_imply_ours/proofs_in_TCS/Every_Cauchy_Sequence_is_bounded/P.con" "bridges_axioms_imply_ours__proofs_in_TCS__Every_Cauchy_Sequence_is_bounded__" as definition.
 235
 236 inline procedural "cic:/CoRN/reals/Bridges_iso/fin_is_fin.con" as lemma.
 237
 238 inline procedural "cic:/CoRN/reals/Bridges_iso/card_fin.con" as lemma.
 239
 240 inline procedural "cic:/CoRN/reals/Bridges_iso/finite_seq.con" as lemma.
 241
 242 inline procedural "cic:/CoRN/reals/Bridges_iso/bridges_lemma2a.con" as lemma.
 243
 244 inline procedural "cic:/CoRN/reals/Bridges_iso/sup.con" as definition.
 245
 246 inline procedural "cic:/CoRN/reals/Bridges_iso/Psup.con" as definition.
 247
 248 inline procedural "cic:/CoRN/reals/Bridges_iso/Psup_proj1.con" as lemma.
 249
 250 inline procedural "cic:/CoRN/reals/Bridges_iso/Psup_unfolded1.con" as lemma.
 251
 252 inline procedural "cic:/CoRN/reals/Bridges_iso/Psup_unfolded2.con" as lemma.
 253
 254 inline procedural "cic:/CoRN/reals/Bridges_iso/bridges_lemma2b.con" as lemma.
 255
 256 inline procedural "cic:/CoRN/reals/Bridges_iso/inf.con" as definition.
 257
 258 inline procedural "cic:/CoRN/reals/Bridges_iso/Pinf.con" as definition.
 259
 260 inline procedural "cic:/CoRN/reals/Bridges_iso/Pinf_proj1.con" as lemma.
 261
 262 inline procedural "cic:/CoRN/reals/Bridges_iso/Pinf_unfolded1.con" as lemma.
 263
 264 inline procedural "cic:/CoRN/reals/Bridges_iso/Pinf_unfolded2.con" as lemma.
 265
 266 (* I tried very much not to mention this lemma! *)
 267
 268 inline procedural "cic:/CoRN/reals/Bridges_iso/sup_leEq.con" as lemma.
 269
 270 inline procedural "cic:/CoRN/reals/Bridges_iso/inf_geEq.con" as lemma.
 271
 272 inline procedural "cic:/CoRN/reals/Bridges_iso/tail_is_Cauchy.con" as lemma.
 273
 274 inline procedural "cic:/CoRN/reals/Bridges_iso/tail_seq.con" as definition.
 275
 276 (* UNEXPORTED
 277 End Every_Cauchy_Sequence_is_bounded
 278 *)
 279
 280 (* UNEXPORTED
 281 cic:/CoRN/reals/Bridges_iso/bridges_axioms_imply_ours/proofs_in_TCS/g.var
 282 *)
 283
 284 inline procedural "cic:/CoRN/reals/Bridges_iso/bridges_axioms_imply_ours/proofs_in_TCS/g_.con" "bridges_axioms_imply_ours__proofs_in_TCS__" as definition.
 285
 286 inline procedural "cic:/CoRN/reals/Bridges_iso/bridges_axioms_imply_ours/proofs_in_TCS/pg.con" "bridges_axioms_imply_ours__proofs_in_TCS__" as definition.
 287
 288 inline procedural "cic:/CoRN/reals/Bridges_iso/bridges_axioms_imply_ours/proofs_in_TCS/sup_tail.con" "bridges_axioms_imply_ours__proofs_in_TCS__" as definition.
 289
 290 inline procedural "cic:/CoRN/reals/Bridges_iso/sup_tail_leEq.con" as lemma.
 291
 292 inline procedural "cic:/CoRN/reals/Bridges_iso/sup_tail_is_Cauchy.con" as lemma.
 293
 294 inline procedural "cic:/CoRN/reals/Bridges_iso/sup_tail_as_Cauchy.con" as definition.
 295
 296 inline procedural "cic:/CoRN/reals/Bridges_iso/bridges_axioms_imply_ours/proofs_in_TCS/L.con" "bridges_axioms_imply_ours__proofs_in_TCS__" as definition.
 297
 298 inline procedural "cic:/CoRN/reals/Bridges_iso/sup_tail_decrease.con" as lemma.
 299
 300 inline procedural "cic:/CoRN/reals/Bridges_iso/L_less_sup_n.con" as lemma.
 301
 302 inline procedural "cic:/CoRN/reals/Bridges_iso/Psup_unfolded2_informative.con" as lemma.
 303
 304 inline procedural "cic:/CoRN/reals/Bridges_iso/Pinf_unfolded2_informative.con" as lemma.
 305
 306 inline procedural "cic:/CoRN/reals/Bridges_iso/convergent_subseq.con" as lemma.
 307
 308 (* very elegant proof almost as short as text version! *)
 309
 310 inline procedural "cic:/CoRN/reals/Bridges_iso/lubp_gives_Cauchy.con" as theorem.
 311
 312 (* UNEXPORTED
 313 End proofs_in_TCS
 314 *)
 315
 316 inline procedural "cic:/CoRN/reals/Bridges_iso/Bridges_R_is_CReals.con" as definition.
 317
 318 inline procedural "cic:/CoRN/reals/Bridges_iso/Bridges_R_as_CReals.con" as definition.
 319
 320 (* UNEXPORTED
 321 End bridges_axioms_imply_ours
 322 *)
 323
 324 (* end hide *)
 325
 326 (*#* remove printing Q *)
 327