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).