1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
19 axiom F:Type.(*F=funzioni regolari*)
24 axiom De: F→F. (*funzione derivata*)
26 non associative with precedence 80
28 interpretation "function derivative" 'deriv x =
29 (cic:/matita/didactic/deriv/De.con x).
30 interpretation "function mult" 'mult x y =
31 (cic:/matita/didactic/deriv/fmult.con x y).
32 interpretation "function compositon" 'compose x y =
33 (cic:/matita/didactic/deriv/fcomp.con x y).
35 notation "hvbox(a break + b)"
36 right associative with precedence 45
37 for @{ 'oplus $a $b }.
39 interpretation "function plus" 'plus x y =
40 (cic:/matita/didactic/deriv/fplus.con x y).
42 axiom i:R→F. (*mappatura R in F*)
43 coercion cic:/matita/didactic/deriv/i.con.
44 axiom i_comm_plus: ∀x,y:R. (i (x+y)) = (i x) + (i y).
45 axiom i_comm_mult: ∀x,y:R. (i (Rmult x y)) = (i x) · (i y).
49 non associative with precedence 100
51 interpretation "function flip" 'rho =
52 cic:/matita/didactic/deriv/freflex.con.
53 axiom reflex_ok: ∀f:F. ρ ∘ f = (i (-R1)) · f.
54 axiom dereflex: ρ ' = i (-R1). (*Togliere*)
56 axiom id:F. (* Funzione identita' *)
57 axiom fcomp_id_neutral: ∀f:F. f ∘ id = f.
58 axiom fcomp_id_commutative: ∀f:F. f ∘ id = id ∘ f.
59 axiom deid: id ' = i R1.
60 axiom rho_id: ρ ∘ ρ = id.
62 lemma rho_disp: ρ = ρ ∘ (ρ ∘ ρ).
63 we need to prove (ρ = ρ ∘ (ρ ∘ ρ)).
67 lemma id_disp: id = ρ ∘ (id ∘ ρ).
68 we need to prove (id = ρ ∘ (id ∘ ρ)).
72 let rec felev (f:F) (n:nat) on n: F ≝
75 | S n ⇒ f · (felev f n)
80 axiom fplus_commutative: ∀ f,g:F. f + g = g + f.
81 axiom fplus_associative: ∀ f,g,h:F. f + (g + h) = (f + g) + h.
82 axiom fplus_neutral: ∀f:F. (i R0) + f = f.
83 axiom fmult_commutative: ∀ f,g:F. f · g = g · f.
84 axiom fmult_associative: ∀ f,g,h:F. f · (g · h) = (f · g) · h.
85 axiom fmult_neutral: ∀f:F. (i R1) · f = f.
86 axiom fmult_assorb: ∀f:F. (i R0) · f = (i R0).
87 axiom fdistr: ∀ f,g,h:F. (f + g) · h = (f · h) + (g · h).
88 axiom fcomp_associative: ∀ f,g,h:F. f ∘ (g ∘ h) = (f ∘ g) ∘ h.
90 axiom fcomp_distr1: ∀ f,g,h:F. (f + g) ∘ h = (f ∘ h) + (g ∘ h).
91 axiom fcomp_distr2: ∀ f,g,h:F. (f · g) ∘ h = (f ∘ h) · (g ∘ h).
93 axiom demult: ∀ f,g:F. (f · g) ' = (f ' · g) + (f · g ').
94 axiom decomp: ∀ f,g:F. (f ∘ g) ' = (f ' ∘ g) · g '.
95 axiom deplus: ∀ f,g:F. (f + g) ' = (f ') + (g ').
97 axiom cost_assorb: ∀x:R. ∀f:F. (i x) ∘ f = i x.
98 axiom cost_deriv: ∀x:R. (i x) ' = i R0.
101 definition fpari ≝ λ f:F. f = f ∘ ρ.
102 definition fdispari ≝ λ f:F. f = ρ ∘ (f ∘ ρ).
103 axiom cost_pari: ∀ x:R. fpari (i x).
105 axiom meno_piu_i: (i (-R1)) · (i (-R1)) = i R1.
107 notation "hvbox(a break ^ b)"
108 right associative with precedence 75
109 for @{ 'elev $a $b }.
111 interpretation "function power" 'elev x y =
112 (cic:/matita/didactic/deriv/felev.con x y).
114 axiom tech1: ∀n,m. F_OF_nat n + F_OF_nat m = F_OF_nat (n + m).