helm/software/matita/contribs/ng_assembly/freescale/prod.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/bool.ma".
  28
  29 (* ***** *)
  30 (* TUPLE *)
  31 (* ***** *)
  32
  33 ninductive ProdT (T1:Type) (T2:Type) : Type ≝
  34  pair : T1 → T2 → ProdT T1 T2.
  35
  36 ndefinition ProdT_ind
  37  : ΠT1,T2:Type.ΠP:ProdT T1 T2 → Prop.
  38    (Πt:T1.Πt1:T2.P (pair T1 T2 t t1)) →
  39    Πp:ProdT T1 T2.P p ≝
  40 λT1,T2:Type.λP:ProdT T1 T2 → Prop.
  41 λf:Πt:T1.Πt1:T2.P (pair T1 T2 t t1).
  42 λp:ProdT T1 T2.
  43  match p with [ pair t t1 ⇒ f t t1 ].
  44
  45 ndefinition ProdT_rec
  46  : ΠT1,T2:Type.ΠP:ProdT T1 T2 → Set.
  47    (Πt:T1.Πt1:T2.P (pair T1 T2 t t1)) →
  48    Πp:ProdT T1 T2.P p ≝
  49 λT1,T2:Type.λP:ProdT T1 T2 → Set.
  50 λf:Πt:T1.Πt1:T2.P (pair T1 T2 t t1).
  51 λp:ProdT T1 T2.
  52  match p with [ pair t t1 ⇒ f t t1 ].
  53
  54 ndefinition ProdT_rect
  55  : ΠT1,T2:Type.ΠP:ProdT T1 T2 → Type.
  56    (Πt:T1.Πt1:T2.P (pair T1 T2 t t1)) →
  57    Πp:ProdT T1 T2.P p ≝
  58 λT1,T2:Type.λP:ProdT T1 T2 → Type.
  59 λf:Πt:T1.Πt1:T2.P (pair T1 T2 t t1).
  60 λp:ProdT T1 T2.
  61  match p with [ pair t t1 ⇒ f t t1 ].
  62
  63 ndefinition fst ≝
  64 λT1,T2:Type.λp:ProdT T1 T2.match p with [ pair  x _ ⇒ x ].
  65
  66 ndefinition snd ≝
  67 λT1,T2:Type.λp:ProdT T1 T2.match p with [ pair  _ x ⇒ x ].
  68
  69 ndefinition eq_pair ≝
  70 λT1,T2:Type.λp1,p2:ProdT T1 T2.
  71 λf1:T1 → T1 → bool.λf2:T2 → T2 → bool.
  72  match p1 with [ pair x1 y1 ⇒
  73   match p2 with [ pair x2 y2 ⇒
  74    (f1 x1 x2) ⊗ (f2 y1 y2) ]].
  75
  76 ninductive Prod3T (T1:Type) (T2:Type) (T3:Type) : Type ≝
  77 triple : T1 → T2 → T3 → Prod3T T1 T2 T3.
  78
  79 ndefinition Prod3T_ind
  80  : ΠT1,T2,T3:Type.ΠP:Prod3T T1 T2 T3 → Prop.
  81    (Πt:T1.Πt1:T2.Πt2:T3.P (triple T1 T2 T3 t t1 t2)) →
  82    Πp:Prod3T T1 T2 T3.P p ≝
  83 λT1,T2,T3:Type.λP:Prod3T T1 T2 T3 → Prop.
  84 λf:Πt:T1.Πt1:T2.Πt2:T3.P (triple T1 T2 T3 t t1 t2).
  85 λp:Prod3T T1 T2 T3.
  86  match p with [ triple t t1 t2 ⇒ f t t1 t2 ].
  87
  88 ndefinition Prod3T_rec
  89  : ΠT1,T2,T3:Type.ΠP:Prod3T T1 T2 T3 → Set.
  90    (Πt:T1.Πt1:T2.Πt2:T3.P (triple T1 T2 T3 t t1 t2)) →
  91    Πp:Prod3T T1 T2 T3.P p ≝
  92 λT1,T2,T3:Type.λP:Prod3T T1 T2 T3 → Set.
  93 λf:Πt:T1.Πt1:T2.Πt2:T3.P (triple T1 T2 T3 t t1 t2).
  94 λp:Prod3T T1 T2 T3.
  95  match p with [ triple t t1 t2 ⇒ f t t1 t2 ].
  96
  97 ndefinition Prod3T_rect
  98  : ΠT1,T2,T3:Type.ΠP:Prod3T T1 T2 T3 → Type.
  99    (Πt:T1.Πt1:T2.Πt2:T3.P (triple T1 T2 T3 t t1 t2)) →
 100    Πp:Prod3T T1 T2 T3.P p ≝
 101 λT1,T2,T3:Type.λP:Prod3T T1 T2 T3 → Type.
 102 λf:Πt:T1.Πt1:T2.Πt2:T3.P (triple T1 T2 T3 t t1 t2).
 103 λp:Prod3T T1 T2 T3.
 104  match p with [ triple t t1 t2 ⇒ f t t1 t2 ].
 105
 106 ndefinition fst3T ≝
 107 λT1.λT2.λT3.λp:Prod3T T1 T2 T3.match p with [ triple x _ _ ⇒ x ].
 108
 109 ndefinition snd3T ≝
 110 λT1.λT2.λT3.λp:Prod3T T1 T2 T3.match p with [ triple _ x _ ⇒ x ].
 111
 112 ndefinition thd3T ≝
 113 λT1.λT2.λT3.λp:Prod3T T1 T2 T3.match p with [ triple _ _ x ⇒ x ].
 114
 115 ndefinition eq_triple ≝
 116 λT1,T2,T3:Type.λp1,p2:Prod3T T1 T2 T3.
 117 λf1:T1 → T1 → bool.λf2:T2 → T2 → bool.λf3:T3 → T3 → bool.
 118  match p1 with [ triple x1 y1 z1 ⇒
 119   match p2 with [ triple x2 y2 z2 ⇒
 120    (f1 x1 x2) ⊗ (f2 y1 y2) ⊗ (f3 z1 z2) ]].
 121
 122 ninductive Prod4T (T1:Type) (T2:Type) (T3:Type) (T4:Type) : Type ≝
 123 quadruple : T1 → T2 → T3 → T4 → Prod4T T1 T2 T3 T4.
 124
 125 ndefinition Prod4T_ind
 126  : ΠT1,T2,T3,T4:Type.ΠP:Prod4T T1 T2 T3 T4 → Prop.
 127    (Πt:T1.Πt1:T2.Πt2:T3.Πt3:T4.P (quadruple T1 T2 T3 T4 t t1 t2 t3)) →
 128    Πp:Prod4T T1 T2 T3 T4.P p ≝
 129 λT1,T2,T3,T4:Type.λP:Prod4T T1 T2 T3 T4 → Prop.
 130 λf:Πt:T1.Πt1:T2.Πt2:T3.Πt3:T4.P (quadruple T1 T2 T3 T4 t t1 t2 t3).
 131 λp:Prod4T T1 T2 T3 T4.
 132  match p with [ quadruple t t1 t2 t3 ⇒ f t t1 t2 t3 ].
 133
 134 ndefinition Prod4T_rec
 135  : ΠT1,T2,T3,T4:Type.ΠP:Prod4T T1 T2 T3 T4 → Set.
 136    (Πt:T1.Πt1:T2.Πt2:T3.Πt3:T4.P (quadruple T1 T2 T3 T4 t t1 t2 t3)) →
 137    Πp:Prod4T T1 T2 T3 T4.P p ≝
 138 λT1,T2,T3,T4:Type.λP:Prod4T T1 T2 T3 T4 → Set.
 139 λf:Πt:T1.Πt1:T2.Πt2:T3.Πt3:T4.P (quadruple T1 T2 T3 T4 t t1 t2 t3).
 140 λp:Prod4T T1 T2 T3 T4.
 141  match p with [ quadruple t t1 t2 t3 ⇒ f t t1 t2 t3 ].
 142
 143 ndefinition Prod4T_rect
 144  : ΠT1,T2,T3,T4:Type.ΠP:Prod4T T1 T2 T3 T4 → Type.
 145    (Πt:T1.Πt1:T2.Πt2:T3.Πt3:T4.P (quadruple T1 T2 T3 T4 t t1 t2 t3)) →
 146    Πp:Prod4T T1 T2 T3 T4.P p ≝
 147 λT1,T2,T3,T4:Type.λP:Prod4T T1 T2 T3 T4 → Type.
 148 λf:Πt:T1.Πt1:T2.Πt2:T3.Πt3:T4.P (quadruple T1 T2 T3 T4 t t1 t2 t3).
 149 λp:Prod4T T1 T2 T3 T4.
 150  match p with [ quadruple t t1 t2 t3 ⇒ f t t1 t2 t3 ].
 151
 152 ndefinition fst4T ≝
 153 λT1.λT2.λT3.λT4.λp:Prod4T T1 T2 T3 T4.match p with [ quadruple x _ _ _ ⇒ x ].
 154
 155 ndefinition snd4T ≝
 156 λT1.λT2.λT3.λT4.λp:Prod4T T1 T2 T3 T4.match p with [ quadruple _ x _ _ ⇒ x ].
 157
 158 ndefinition thd4T ≝
 159 λT1.λT2.λT3.λT4.λp:Prod4T T1 T2 T3 T4.match p with [ quadruple _ _ x _ ⇒ x ].
 160
 161 ndefinition fth4T ≝
 162 λT1.λT2.λT3.λT4.λp:Prod4T T1 T2 T3 T4.match p with [ quadruple _ _ _ x ⇒ x ].
 163
 164 ndefinition eq_quadruple ≝
 165 λT1,T2,T3,T4:Type.λp1,p2:Prod4T T1 T2 T3 T4.
 166 λf1:T1 → T1 → bool.λf2:T2 → T2 → bool.λf3:T3 → T3 → bool.λf4:T4 → T4 → bool.
 167  match p1 with [ quadruple x1 y1 z1 w1 ⇒
 168   match p2 with [ quadruple x2 y2 z2 w2 ⇒
 169    (f1 x1 x2) ⊗ (f2 y1 y2) ⊗ (f3 z1 z2) ⊗ (f4 w1 w2) ]].
 170
 171 ninductive Prod5T (T1:Type) (T2:Type) (T3:Type) (T4:Type) (T5:Type) : Type ≝
 172 quintuple : T1 → T2 → T3 → T4 → T5 → Prod5T T1 T2 T3 T4 T5.
 173
 174 ndefinition Pro54T_ind
 175  : ΠT1,T2,T3,T4,T5:Type.ΠP:Prod5T T1 T2 T3 T4 T5 → Prop.
 176    (Πt:T1.Πt1:T2.Πt2:T3.Πt3:T4.Πt4:T5.P (quintuple T1 T2 T3 T4 T5 t t1 t2 t3 t4)) →
 177    Πp:Prod5T T1 T2 T3 T4 T5.P p ≝
 178 λT1,T2,T3,T4,T5:Type.λP:Prod5T T1 T2 T3 T4 T5 → Prop.
 179 λf:Πt:T1.Πt1:T2.Πt2:T3.Πt3:T4.Πt4:T5.P (quintuple T1 T2 T3 T4 T5 t t1 t2 t3 t4).
 180 λp:Prod5T T1 T2 T3 T4 T5.
 181  match p with [ quintuple t t1 t2 t3 t4 ⇒ f t t1 t2 t3 t4 ].
 182
 183 ndefinition Pro54T_rec
 184  : ΠT1,T2,T3,T4,T5:Type.ΠP:Prod5T T1 T2 T3 T4 T5 → Set.
 185    (Πt:T1.Πt1:T2.Πt2:T3.Πt3:T4.Πt4:T5.P (quintuple T1 T2 T3 T4 T5 t t1 t2 t3 t4)) →
 186    Πp:Prod5T T1 T2 T3 T4 T5.P p ≝
 187 λT1,T2,T3,T4,T5:Type.λP:Prod5T T1 T2 T3 T4 T5 → Set.
 188 λf:Πt:T1.Πt1:T2.Πt2:T3.Πt3:T4.Πt4:T5.P (quintuple T1 T2 T3 T4 T5 t t1 t2 t3 t4).
 189 λp:Prod5T T1 T2 T3 T4 T5.
 190  match p with [ quintuple t t1 t2 t3 t4 ⇒ f t t1 t2 t3 t4 ].
 191
 192 ndefinition Pro54T_rect
 193  : ΠT1,T2,T3,T4,T5:Type.ΠP:Prod5T T1 T2 T3 T4 T5 → Type.
 194    (Πt:T1.Πt1:T2.Πt2:T3.Πt3:T4.Πt4:T5.P (quintuple T1 T2 T3 T4 T5 t t1 t2 t3 t4)) →
 195    Πp:Prod5T T1 T2 T3 T4 T5.P p ≝
 196 λT1,T2,T3,T4,T5:Type.λP:Prod5T T1 T2 T3 T4 T5 → Type.
 197 λf:Πt:T1.Πt1:T2.Πt2:T3.Πt3:T4.Πt4:T5.P (quintuple T1 T2 T3 T4 T5 t t1 t2 t3 t4).
 198 λp:Prod5T T1 T2 T3 T4 T5.
 199  match p with [ quintuple t t1 t2 t3 t4 ⇒ f t t1 t2 t3 t4 ].
 200
 201 ndefinition fst5T ≝
 202 λT1.λT2.λT3.λT4.λT5.λp:Prod5T T1 T2 T3 T4 T5.match p with [ quintuple x _ _ _ _ ⇒ x ].
 203
 204 ndefinition snd5T ≝
 205 λT1.λT2.λT3.λT4.λT5.λp:Prod5T T1 T2 T3 T4 T5.match p with [ quintuple _ x _ _ _ ⇒ x ].
 206
 207 ndefinition thd5T ≝
 208 λT1.λT2.λT3.λT4.λT5.λp:Prod5T T1 T2 T3 T4 T5.match p with [ quintuple _ _ x _ _ ⇒ x ].
 209
 210 ndefinition frth5T ≝
 211 λT1.λT2.λT3.λT4.λT5.λp:Prod5T T1 T2 T3 T4 T5.match p with [ quintuple _ _ _ x _ ⇒ x ].
 212
 213 ndefinition ffth5T ≝
 214 λT1.λT2.λT3.λT4.λT5.λp:Prod5T T1 T2 T3 T4 T5.match p with [ quintuple _ _ _ _ x ⇒ x ].
 215
 216 ndefinition eq_quintuple ≝
 217 λT1,T2,T3,T4,T5:Type.λp1,p2:Prod5T T1 T2 T3 T4 T5.
 218 λf1:T1 → T1 → bool.λf2:T2 → T2 → bool.λf3:T3 → T3 → bool.λf4:T4 → T4 → bool.λf5:T5 → T5 → bool.
 219  match p1 with [ quintuple x1 y1 z1 w1 v1 ⇒
 220   match p2 with [ quintuple x2 y2 z2 w2 v2 ⇒
 221    (f1 x1 x2) ⊗ (f2 y1 y2) ⊗ (f3 z1 z2) ⊗ (f4 w1 w2) ⊗ (f5 v1 v2) ]].