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