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