helm/software/matita/contribs/ng_assembly/freescale/nat.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 (*                           Progetto FreeScale                           *)
  17 (*                                                                        *)
  18 (* Sviluppato da:                                                         *)
  19 (*   Cosimo Oliboni, oliboni@cs.unibo.it                                  *)
  20 (*                                                                        *)
  21 (* Questo materiale fa parte della tesi:                                  *)
  22 (*   "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale"   *)
  23 (*                                                                        *)
  24 (*                    data ultima modifica 15/11/2007                     *)
  25 (* ********************************************************************** *)
  26
  27 include "freescale/pts.ma".
  28 include "freescale/bool.ma".
  29
  30 (* ******** *)
  31 (* NATURALI *)
  32 (* ******** *)
  33
  34 inductive nat : Type ≝
  35   O : nat
  36 | S : nat → nat.
  37
  38 interpretation "Natural numbers" 'N = nat.
  39
  40 default "natural numbers" cic:/matita/freescale/nat/nat.ind.
  41
  42 alias num (instance 0) = "natural number".
  43
  44 nlet rec nat_ind (P:nat → Prop) (p:P O) (f:Πn:nat.P n → P (S n)) (n:nat) on n : P n ≝
  45  match n with [ O ⇒ p | S (n1:nat) ⇒ f n1 (nat_ind P p f n1) ].
  46
  47 nlet rec nat_rec (P:nat → Set) (p:P O) (f:Πn:nat.P n → P (S n)) (n:nat) on n : P n ≝
  48  match n with [ O ⇒ p | S (n1:nat) ⇒ f n1 (nat_rec P p f n1) ].
  49
  50 nlet rec nat_rect (P:nat → Type) (p:P O) (f:Πn:nat.P n → P (S n)) (n:nat) on n : P n ≝
  51  match n with [ O ⇒ p | S (n1:nat) ⇒ f n1 (nat_rect P p f n1) ].
  52
  53 nlet rec eq_nat (n1,n2:nat) on n1 ≝
  54  match n1 with
  55   [ O ⇒ match n2 with [ O ⇒ true | S _ ⇒ false ]
  56   | S n1' ⇒ match n2 with [ O ⇒ false | S n2' ⇒ eq_nat n1' n2' ]
  57   ].
  58
  59 nlet rec le_nat n m ≝
  60  match n with
  61   [ O ⇒ true
  62   | (S p) ⇒ match m with
  63    [ O ⇒ false | (S q) ⇒ le_nat p q ]
  64   ].
  65
  66 nlet rec plus (n1,n2:nat) on n1 ≝
  67  match n1 with
  68   [ O ⇒ n2
  69   | (S n1') ⇒ S (plus n1' n2) ].
  70
  71 interpretation "natural plus" 'plus x y = (plus x y).
  72
  73 nlet rec times (n1,n2:nat) on n1 ≝
  74  match n1 with
  75   [ O ⇒ O
  76   | (S n1') ⇒ n2 + (times n1' n2) ].
  77
  78 interpretation "natural times" 'times x y = (times x y).