]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/dama_didactic/reals.ma
Notation improved.
[helm.git] / helm / software / matita / 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 set "baseuri" "cic:/matita/didactic/reals".
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.