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 =
  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).
  34
  35 notation "hvbox(a break + b)"
  36   right associative with precedence 45
  37 for @{ 'oplus $a $b }.
  38
  39 interpretation "function plus" 'plus x y =
  40  (cic:/matita/didactic/deriv/fplus.con x y).
  41
  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).
  46
  47 axiom freflex:F.
  48 notation "ρ"
  49   non associative with precedence 100
  50 for @{ 'rho }.
  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*)
  55
  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.
  61
  62 lemma rho_disp: ρ = ρ ∘ (ρ ∘ ρ).
  63  we need to prove (ρ = ρ ∘ (ρ ∘ ρ)).
  64  by _ done.
  65 qed.
  66
  67 lemma id_disp: id = ρ ∘ (id ∘ ρ).
  68  we need to prove (id = ρ ∘ (id ∘ ρ)).
  69  by _ done.
  70 qed.
  71
  72 let rec felev (f:F) (n:nat) on n: F ≝
  73  match n with
  74  [ O ⇒ i R1
  75  | S n ⇒ f · (felev f n)
  76  ].
  77
  78 (* Proprietà *)
  79
  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.
  89
  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).
  92
  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 ').
  96
  97 axiom cost_assorb: ∀x:R. ∀f:F. (i x) ∘ f = i x.
  98 axiom cost_deriv: ∀x:R. (i x) ' = i R0.
  99
 100
 101 definition fpari ≝ λ f:F. f = f ∘ ρ.
 102 definition fdispari ≝ λ f:F. f = ρ ∘ (f ∘ ρ).
 103 axiom cost_pari: ∀ x:R. fpari (i x).
 104
 105 axiom meno_piu_i: (i (-R1)) · (i (-R1)) = i R1.
 106
 107 notation "hvbox(a break ^ b)"
 108   right associative with precedence 75
 109 for @{ 'elev $a $b }.
 110
 111 interpretation "function power" 'elev x y =
 112  (cic:/matita/didactic/deriv/felev.con x y).
 113
 114 axiom tech1: ∀n,m. F_OF_nat n + F_OF_nat m = F_OF_nat (n + m).