]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/contribs/dama/dama_didactic/deriv.ma
fixed some regressions
[helm.git] / helm / software / matita / contribs / dama / dama_didactic / deriv.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 "reals.ma".
18
19 axiom F:Type.(*F=funzioni regolari*)
20 axiom fplus:F→F→F.
21 axiom fmult:F→F→F.
22 axiom fcomp:F→F→F.
23
24 axiom De: F→F. (*funzione derivata*)
25 notation "a '"
26   non associative with precedence 80
27 for @{ 'deriv $a }.
28 interpretation "function derivative" 'deriv x = (De x). 
29 interpretation "function mult" 'mult x y = (fmult x y). 
30 interpretation "function compositon" 'compose x y = (fcomp x y).
31
32 notation "hvbox(a break + b)"
33   right associative with precedence 45
34 for @{ 'oplus $a $b }.
35
36 interpretation "function plus" 'plus x y = (fplus x y).
37
38 axiom i:R→F. (*mappatura  R in F*)
39 coercion cic:/matita/didactic/deriv/i.con.
40 axiom i_comm_plus: ∀x,y:R. (i (x+y)) = (i x) + (i y).
41 axiom i_comm_mult: ∀x,y:R. (i (Rmult x y)) = (i x) · (i y).
42
43 axiom freflex:F.
44 notation "ρ"
45   non associative with precedence 100
46 for @{ 'rho }.
47 interpretation "function flip" 'rho = freflex.
48 axiom reflex_ok: ∀f:F. ρ ∘ f = (i (-R1)) · f.
49 axiom dereflex: ρ ' = i (-R1). (*Togliere*)
50
51 axiom id:F. (* Funzione identita' *)
52 axiom fcomp_id_neutral: ∀f:F. f ∘ id = f.
53 axiom fcomp_id_commutative: ∀f:F. f ∘ id = id ∘ f.
54 axiom deid: id ' = i R1.
55 axiom rho_id: ρ ∘ ρ = id.
56
57 lemma rho_disp: ρ = ρ ∘ (ρ ∘ ρ).
58  we need to prove (ρ = ρ ∘ (ρ ∘ ρ)).
59  by _ done.
60 qed.
61
62 lemma id_disp: id = ρ ∘ (id ∘ ρ).
63  we need to prove (id = ρ ∘ (id ∘ ρ)).
64  by _ done.
65 qed.
66
67 let rec felev (f:F) (n:nat) on n: F ≝
68  match n with
69  [ O ⇒ i R1
70  | S n ⇒ f · (felev f n)
71  ].
72
73 (* Proprietà *)
74
75 axiom fplus_commutative: ∀ f,g:F. f + g = g + f.
76 axiom fplus_associative: ∀ f,g,h:F. f + (g + h) = (f + g) + h.
77 axiom fplus_neutral: ∀f:F. (i R0) + f = f.
78 axiom fmult_commutative: ∀ f,g:F. f · g = g · f.
79 axiom fmult_associative: ∀ f,g,h:F. f · (g · h) = (f · g) · h.
80 axiom fmult_neutral: ∀f:F. (i R1) · f = f.
81 axiom fmult_assorb: ∀f:F. (i R0) · f = (i R0).
82 axiom fdistr: ∀ f,g,h:F. (f + g) · h = (f · h) + (g · h).
83 axiom fcomp_associative: ∀ f,g,h:F. f ∘ (g ∘ h) = (f ∘ g) ∘ h.
84
85 axiom fcomp_distr1: ∀ f,g,h:F. (f + g) ∘ h = (f ∘ h) + (g ∘ h).
86 axiom fcomp_distr2: ∀ f,g,h:F. (f · g) ∘ h = (f ∘ h) · (g ∘ h).
87
88 axiom demult: ∀ f,g:F. (f · g) ' = (f ' · g) + (f · g ').
89 axiom decomp: ∀ f,g:F. (f ∘ g) ' = (f ' ∘ g) · g '.
90 axiom deplus: ∀ f,g:F. (f + g) ' = (f ') + (g ').
91
92 axiom cost_assorb: ∀x:R. ∀f:F. (i x) ∘ f = i x.
93 axiom cost_deriv: ∀x:R. (i x) ' = i R0.
94
95
96 definition fpari ≝ λ f:F. f = f ∘ ρ.
97 definition fdispari ≝ λ f:F. f = ρ ∘ (f ∘ ρ).
98 axiom cost_pari: ∀ x:R. fpari (i x).
99
100 axiom meno_piu_i: (i (-R1)) · (i (-R1)) = i R1.
101
102 notation "hvbox(a break ^ b)"
103   right associative with precedence 75
104 for @{ 'elev $a $b }.
105  
106 interpretation "function power" 'elev x y = (felev x y). 
107
108 axiom tech1: ∀n,m. F_OF_nat n + F_OF_nat m = F_OF_nat (n + m).