matita/contribs/dama/dama_didactic/reals.ma

   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
  16
  17 include "nat/plus.ma".
  18
  19 axiom R:Type.
  20 axiom R0:R.
  21 axiom R1:R.
  22 axiom Rplus: R→R→R.
  23 axiom Ropp:R→R. (*funzione da x → -x*)
  24 axiom Rmult: R→R→R.
  25 axiom Rdiv: R→R→R.
  26 axiom Relev: R→R→R.
  27 axiom Rle: R→R→Prop.
  28 axiom Rge: R→R→Prop.
  29
  30 interpretation "real plus" 'plus x y =
  31  (cic:/matita/didactic/reals/Rplus.con x y).
  32
  33 interpretation "real opp" 'uminus x =
  34  (cic:/matita/didactic/reals/Ropp.con x).
  35
  36 notation "hvbox(a break · b)"
  37   right associative with precedence 55
  38 for @{ 'mult $a $b }.
  39
  40 interpretation "real mult" 'mult x y =
  41  (cic:/matita/didactic/reals/Rmult.con x y).
  42
  43 interpretation "real leq" 'leq x y =
  44  (cic:/matita/didactic/reals/Rle.con x y).
  45
  46 interpretation "real geq" 'geq x y =
  47  (cic:/matita/didactic/reals/Rge.con x y).
  48
  49 let rec elev (x:R) (n:nat) on n: R ≝
  50  match n with
  51   [O ⇒ R1
  52   | S n ⇒ Rmult x (elev x n)
  53   ].
  54
  55 let rec real_of_nat (n:nat) : R ≝
  56  match n with
  57   [ O ⇒ R0
  58   | S n ⇒
  59      match n with
  60       [ O ⇒ R1
  61       | _ ⇒ real_of_nat n + R1
  62       ]
  63   ].
  64
  65 coercion cic:/matita/didactic/reals/real_of_nat.con.
  66
  67 axiom Rplus_commutative: ∀x,y:R. x+y = y+x.
  68 axiom R0_neutral: ∀x:R. x+R0=x.
  69 axiom Rdiv_le: ∀x,y:R. R1 ≤ y → Rdiv x y ≤ x.
  70 axiom R2_1: R1 ≤ S (S O).
  71 (* assioma falso! *)
  72 axiom Rmult_Rle: ∀x,y,z,w. x ≤ y → z ≤ w → Rmult x z ≤ Rmult y w.
  73
  74 axiom Rdiv_pos: ∀ x,y:R. R0 ≤ x → R1 ≤ y → R0 ≤ Rdiv x y.
  75 axiom Rle_R0_R1: R0 ≤ R1.
  76 axiom div: ∀x:R. x = Rdiv x (S (S O)) → x = O.
  77 (* Proprieta' elevamento a potenza NATURALE *)
  78 axiom elev_incr: ∀x:R.∀n:nat. R1 ≤ x → elev x (S n) ≥ elev x n.
  79 axiom elev_decr: ∀x:R.∀n:nat. R0 ≤ x ∧ x ≤ R1 → elev x (S n) ≤ elev x n.
  80 axiom Rle_to_Rge: ∀x,y:R. x ≤ y → y ≥ x.
  81 axiom Rge_to_Rle: ∀x,y:R. x ≥ y → y ≤ x.
  82
  83 (* Proprieta' elevamento a potenza TRA REALI *)
  84 (*
  85 axiom Relev_ge: ∀x,y:R.
  86  (x ≥ R1 ∧ y ≥ R1) ∨ (x ≤ R1 ∧ y ≤ R1) → Relev x y ≥ x.
  87 axiom Relev_le: ∀x,y:R.
  88  (x ≥ R1 ∧ y ≤ R1) ∨ (x ≤ R1 ∧ y ≥ R1) → Relev x y ≤ x.
  89 *)
  90
  91 lemma stupido: ∀x:R.R0+x=x.
  92  assume x:R.
  93  conclude (R0+x) = (x+R0) by _.
  94                = x by _
  95  done.
  96 qed.
  97
  98 axiom opposto1: ∀x:R. x + -x = R0.
  99 axiom opposto2: ∀x:R. -x = Rmult x (-R1).
 100 axiom meno_piu: Rmult (-R1) (-R1) = R1.
 101 axiom R1_neutral: ∀x:R.Rmult R1 x = x.
 102 (* assioma falso *)
 103 axiom uffa: ∀x,y:R. R1 ≤ x → y ≤ x · y.