helm/matita/library/nat/exp.ma

   1 (**************************************************************************)
   2 (*       ___                                                                *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
   8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU Lesser General Public License Version 2.1         *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 set "baseuri" "cic:/matita/nat/exp".
  16
  17 include "nat/times.ma".
  18
  19 let rec exp n m on m\def
  20  match m with
  21  [ O \Rightarrow (S O)
  22  | (S p) \Rightarrow (times n (exp n p)) ].
  23
  24 theorem exp_plus_times : \forall n,p,q:nat.
  25 eq nat (exp n (plus p q)) (times (exp n p) (exp n q)).
  26 intros.elim p.
  27 simplify.rewrite < plus_n_O.reflexivity.
  28 simplify.rewrite > H.symmetry.
  29 apply assoc_times.
  30 qed.
  31
  32 theorem exp_n_O : \forall n:nat. eq nat (S O) (exp n O).
  33 intro.simplify.reflexivity.
  34 qed.
  35
  36 theorem exp_n_SO : \forall n:nat. eq nat n (exp n (S O)).
  37 intro.simplify.rewrite < times_n_SO.reflexivity.
  38 qed.
  39
  40 theorem exp_exp_times : \forall n,p,q:nat.
  41 eq nat (exp (exp n p) q) (exp n (times p q)).
  42 intros.
  43 elim q.simplify.rewrite < times_n_O.simplify.reflexivity.
  44 simplify.rewrite > H.rewrite < exp_plus_times.
  45 rewrite < times_n_Sm.reflexivity.
  46 qed.