helm/matita/library/nat/primes1.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 (*       \ /        Matita 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/primes1".
  16
  17 include "datatypes/constructors.ma".
  18 include "nat/primes.ma".
  19 include "nat/exp.ma".
  20
  21 (* p is just an upper bound, acc is an accumulator *)
  22 let rec n_divides_aux p n m acc \def
  23   match (mod n m) with
  24   [ O \Rightarrow
  25     match p with
  26       [ O \Rightarrow pair nat nat acc n
  27       | (S p) \Rightarrow n_divides_aux p (div n m) m (S acc)]
  28   | (S a) \Rightarrow pair nat nat acc n].
  29
  30 (* n_divides n m = <q,r> if m divides n q times, with remainder r *)
  31 definition n_divides \def \lambda n,m:nat.n_divides_aux n n m O.
  32
  33 (*
  34 theorem n_divides_to_Prop: \forall n,m,p,a.
  35   match n_divides_aux p n m a with
  36   [ (pair q r) \Rightarrow n = (exp m a)*r].
  37 intros.
  38 apply nat_case (mod n m). *)
  39