helm/software/matita/contribs/ng_assembly/utility/ascii.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 (* DEFINIZIONE ASCII MINIMALE *)
  27 (* ************************** *)
  28
  29 ninductive ascii : Type ≝
  30 (* numeri *)
  31   ch_0: ascii
  32 | ch_1: ascii
  33 | ch_2: ascii
  34 | ch_3: ascii
  35 | ch_4: ascii
  36 | ch_5: ascii
  37 | ch_6: ascii
  38 | ch_7: ascii
  39 | ch_8: ascii
  40 | ch_9: ascii
  41
  42 (* simboli *)
  43 | ch__: ascii
  44
  45 (* maiuscole *)
  46 | ch_A: ascii
  47 | ch_B: ascii
  48 | ch_C: ascii
  49 | ch_D: ascii
  50 | ch_E: ascii
  51 | ch_F: ascii
  52 | ch_G: ascii
  53 | ch_H: ascii
  54 | ch_I: ascii
  55 | ch_J: ascii
  56 | ch_K: ascii
  57 | ch_L: ascii
  58 | ch_M: ascii
  59 | ch_N: ascii
  60 | ch_O: ascii
  61 | ch_P: ascii
  62 | ch_Q: ascii
  63 | ch_R: ascii
  64 | ch_S: ascii
  65 | ch_T: ascii
  66 | ch_U: ascii
  67 | ch_V: ascii
  68 | ch_W: ascii
  69 | ch_X: ascii
  70 | ch_Y: ascii
  71 | ch_Z: ascii
  72
  73 (* minuscole *)
  74 | ch_a: ascii
  75 | ch_b: ascii
  76 | ch_c: ascii
  77 | ch_d: ascii
  78 | ch_e: ascii
  79 | ch_f: ascii
  80 | ch_g: ascii
  81 | ch_h: ascii
  82 | ch_i: ascii
  83 | ch_j: ascii
  84 | ch_k: ascii
  85 | ch_l: ascii
  86 | ch_m: ascii
  87 | ch_n: ascii
  88 | ch_o: ascii
  89 | ch_p: ascii
  90 | ch_q: ascii
  91 | ch_r: ascii
  92 | ch_s: ascii
  93 | ch_t: ascii
  94 | ch_u: ascii
  95 | ch_v: ascii
  96 | ch_w: ascii
  97 | ch_x: ascii
  98 | ch_y: ascii
  99 | ch_z: ascii.
 100
 101 (*ndefinition ascii_ind
 102  : ΠP:ascii → Prop.
 103    P ch_0 → P ch_1 → P ch_2 → P ch_3 → P ch_4 → P ch_5 → P ch_6 → P ch_7 → P ch_8 → P ch_9 → P ch__ →
 104    P ch_A → P ch_B → P ch_C → P ch_D → P ch_E → P ch_F → P ch_G → P ch_H → P ch_I → P ch_J → P ch_K →
 105    P ch_L → P ch_M → P ch_N → P ch_O → P ch_P → P ch_Q → P ch_R → P ch_S → P ch_T → P ch_U → P ch_V →
 106    P ch_W → P ch_X → P ch_Y → P ch_Z → P ch_a → P ch_b → P ch_c → P ch_d → P ch_e → P ch_f → P ch_g →
 107    P ch_h → P ch_i → P ch_j → P ch_k → P ch_l → P ch_m → P ch_n → P ch_o → P ch_p → P ch_q → P ch_r →
 108    P ch_s → P ch_t → P ch_u → P ch_v → P ch_w → P ch_x → P ch_y → P ch_z → Πa:ascii.P a ≝
 109 λP:ascii → Prop.
 110 λp:P ch_0.λp1:P ch_1.λp2:P ch_2.λp3:P ch_3.λp4:P ch_4.λp5:P ch_5.λp6:P ch_6.λp7:P ch_7.λp8:P ch_8.λp9:P ch_9.
 111 λp10:P ch__.λp11:P ch_A.λp12:P ch_B.λp13:P ch_C.λp14:P ch_D.λp15:P ch_E.λp16:P ch_F.λp17:P ch_G.λp18:P ch_H.
 112 λp19:P ch_I.λp20:P ch_J.λp21:P ch_K.λp22:P ch_L.λp23:P ch_M.λp24:P ch_N.λp25:P ch_O.λp26:P ch_P.λp27:P ch_Q.
 113 λp28:P ch_R.λp29:P ch_S.λp30:P ch_T.λp31:P ch_U.λp32:P ch_V.λp33:P ch_W.λp34:P ch_X.λp35:P ch_Y.λp36:P ch_Z.
 114 λp37:P ch_a.λp38:P ch_b.λp39:P ch_c.λp40:P ch_d.λp41:P ch_e.λp42:P ch_f.λp43:P ch_g.λp44:P ch_h.λp45:P ch_i.
 115 λp46:P ch_j.λp47:P ch_k.λp48:P ch_l.λp49:P ch_m.λp50:P ch_n.λp51:P ch_o.λp52:P ch_p.λp53:P ch_q.λp54:P ch_r.
 116 λp55:P ch_s.λp56:P ch_t.λp57:P ch_u.λp58:P ch_v.λp59:P ch_w.λp60:P ch_x.λp61:P ch_y.λp62:P ch_z.λa:ascii.
 117  match a with
 118   [ ch_0 ⇒ p | ch_1 ⇒ p1 | ch_2 ⇒ p2 | ch_3 ⇒ p3 | ch_4 ⇒ p4 | ch_5 ⇒ p5 | ch_6 ⇒ p6 | ch_7 ⇒ p7
 119   | ch_8 ⇒ p8 | ch_9 ⇒ p9 | ch__ ⇒ p10 | ch_A ⇒ p11 | ch_B ⇒ p12 | ch_C ⇒ p13 | ch_D ⇒ p14 | ch_E ⇒ p15
 120   | ch_F ⇒ p16 | ch_G ⇒ p17 | ch_H ⇒ p18 | ch_I ⇒ p19 | ch_J ⇒ p20 | ch_K ⇒ p21 | ch_L ⇒ p22 | ch_M ⇒ p23
 121   | ch_N ⇒ p24 | ch_O ⇒ p25 | ch_P ⇒ p26 | ch_Q ⇒ p27 | ch_R ⇒ p28 | ch_S ⇒ p29 | ch_T ⇒ p30 | ch_U ⇒ p31
 122   | ch_V ⇒ p32 | ch_W ⇒ p33 | ch_X ⇒ p34 | ch_Y ⇒ p35 | ch_Z ⇒ p36 | ch_a ⇒ p37 | ch_b ⇒ p38 | ch_c ⇒ p39
 123   | ch_d ⇒ p40 | ch_e ⇒ p41 | ch_f ⇒ p42 | ch_g ⇒ p43 | ch_h ⇒ p44 | ch_i ⇒ p45 | ch_j ⇒ p46 | ch_k ⇒ p47
 124   | ch_l ⇒ p48 | ch_m ⇒ p49 | ch_n ⇒ p50 | ch_o ⇒ p51 | ch_p ⇒ p52 | ch_q ⇒ p53 | ch_r ⇒ p54 | ch_s ⇒ p55
 125   | ch_t ⇒ p56 | ch_u ⇒ p57 | ch_v ⇒ p58 | ch_w ⇒ p59 | ch_x ⇒ p60 | ch_y ⇒ p61 | ch_z ⇒ p62 ].
 126
 127 ndefinition ascii_rect
 128  : ΠP:ascii → Type.
 129    P ch_0 → P ch_1 → P ch_2 → P ch_3 → P ch_4 → P ch_5 → P ch_6 → P ch_7 → P ch_8 → P ch_9 → P ch__ →
 130    P ch_A → P ch_B → P ch_C → P ch_D → P ch_E → P ch_F → P ch_G → P ch_H → P ch_I → P ch_J → P ch_K →
 131    P ch_L → P ch_M → P ch_N → P ch_O → P ch_P → P ch_Q → P ch_R → P ch_S → P ch_T → P ch_U → P ch_V →
 132    P ch_W → P ch_X → P ch_Y → P ch_Z → P ch_a → P ch_b → P ch_c → P ch_d → P ch_e → P ch_f → P ch_g →
 133    P ch_h → P ch_i → P ch_j → P ch_k → P ch_l → P ch_m → P ch_n → P ch_o → P ch_p → P ch_q → P ch_r →
 134    P ch_s → P ch_t → P ch_u → P ch_v → P ch_w → P ch_x → P ch_y → P ch_z → Πa:ascii.P a ≝
 135 λP:ascii → Type.
 136 λp:P ch_0.λp1:P ch_1.λp2:P ch_2.λp3:P ch_3.λp4:P ch_4.λp5:P ch_5.λp6:P ch_6.λp7:P ch_7.λp8:P ch_8.λp9:P ch_9.
 137 λp10:P ch__.λp11:P ch_A.λp12:P ch_B.λp13:P ch_C.λp14:P ch_D.λp15:P ch_E.λp16:P ch_F.λp17:P ch_G.λp18:P ch_H.
 138 λp19:P ch_I.λp20:P ch_J.λp21:P ch_K.λp22:P ch_L.λp23:P ch_M.λp24:P ch_N.λp25:P ch_O.λp26:P ch_P.λp27:P ch_Q.
 139 λp28:P ch_R.λp29:P ch_S.λp30:P ch_T.λp31:P ch_U.λp32:P ch_V.λp33:P ch_W.λp34:P ch_X.λp35:P ch_Y.λp36:P ch_Z.
 140 λp37:P ch_a.λp38:P ch_b.λp39:P ch_c.λp40:P ch_d.λp41:P ch_e.λp42:P ch_f.λp43:P ch_g.λp44:P ch_h.λp45:P ch_i.
 141 λp46:P ch_j.λp47:P ch_k.λp48:P ch_l.λp49:P ch_m.λp50:P ch_n.λp51:P ch_o.λp52:P ch_p.λp53:P ch_q.λp54:P ch_r.
 142 λp55:P ch_s.λp56:P ch_t.λp57:P ch_u.λp58:P ch_v.λp59:P ch_w.λp60:P ch_x.λp61:P ch_y.λp62:P ch_z.λa:ascii.
 143  match a with
 144   [ ch_0 ⇒ p | ch_1 ⇒ p1 | ch_2 ⇒ p2 | ch_3 ⇒ p3 | ch_4 ⇒ p4 | ch_5 ⇒ p5 | ch_6 ⇒ p6 | ch_7 ⇒ p7
 145   | ch_8 ⇒ p8 | ch_9 ⇒ p9 | ch__ ⇒ p10 | ch_A ⇒ p11 | ch_B ⇒ p12 | ch_C ⇒ p13 | ch_D ⇒ p14 | ch_E ⇒ p15
 146   | ch_F ⇒ p16 | ch_G ⇒ p17 | ch_H ⇒ p18 | ch_I ⇒ p19 | ch_J ⇒ p20 | ch_K ⇒ p21 | ch_L ⇒ p22 | ch_M ⇒ p23
 147   | ch_N ⇒ p24 | ch_O ⇒ p25 | ch_P ⇒ p26 | ch_Q ⇒ p27 | ch_R ⇒ p28 | ch_S ⇒ p29 | ch_T ⇒ p30 | ch_U ⇒ p31
 148   | ch_V ⇒ p32 | ch_W ⇒ p33 | ch_X ⇒ p34 | ch_Y ⇒ p35 | ch_Z ⇒ p36 | ch_a ⇒ p37 | ch_b ⇒ p38 | ch_c ⇒ p39
 149   | ch_d ⇒ p40 | ch_e ⇒ p41 | ch_f ⇒ p42 | ch_g ⇒ p43 | ch_h ⇒ p44 | ch_i ⇒ p45 | ch_j ⇒ p46 | ch_k ⇒ p47
 150   | ch_l ⇒ p48 | ch_m ⇒ p49 | ch_n ⇒ p50 | ch_o ⇒ p51 | ch_p ⇒ p52 | ch_q ⇒ p53 | ch_r ⇒ p54 | ch_s ⇒ p55
 151   | ch_t ⇒ p56 | ch_u ⇒ p57 | ch_v ⇒ p58 | ch_w ⇒ p59 | ch_x ⇒ p60 | ch_y ⇒ p61 | ch_z ⇒ p62 ].
 152 *)
 153 (* confronto fra ascii *)
 154 ndefinition eq_ascii ≝
 155 λc,c':ascii.match c with
 156  [ ch_0 ⇒ match c' with [ ch_0 ⇒ true | _ ⇒ false ]
 157  | ch_1 ⇒ match c' with [ ch_1 ⇒ true | _ ⇒ false ]
 158  | ch_2 ⇒ match c' with [ ch_2 ⇒ true | _ ⇒ false ]
 159  | ch_3 ⇒ match c' with [ ch_3 ⇒ true | _ ⇒ false ]
 160  | ch_4 ⇒ match c' with [ ch_4 ⇒ true | _ ⇒ false ]
 161  | ch_5 ⇒ match c' with [ ch_5 ⇒ true | _ ⇒ false ]
 162  | ch_6 ⇒ match c' with [ ch_6 ⇒ true | _ ⇒ false ]
 163  | ch_7 ⇒ match c' with [ ch_7 ⇒ true | _ ⇒ false ]
 164  | ch_8 ⇒ match c' with [ ch_8 ⇒ true | _ ⇒ false ]
 165  | ch_9 ⇒ match c' with [ ch_9 ⇒ true | _ ⇒ false ]
 166  | ch__ ⇒ match c' with [ ch__ ⇒ true | _ ⇒ false ]
 167  | ch_A ⇒ match c' with [ ch_A ⇒ true | _ ⇒ false ]
 168  | ch_B ⇒ match c' with [ ch_B ⇒ true | _ ⇒ false ]
 169  | ch_C ⇒ match c' with [ ch_C ⇒ true | _ ⇒ false ]
 170  | ch_D ⇒ match c' with [ ch_D ⇒ true | _ ⇒ false ]
 171  | ch_E ⇒ match c' with [ ch_E ⇒ true | _ ⇒ false ]
 172  | ch_F ⇒ match c' with [ ch_F ⇒ true | _ ⇒ false ]
 173  | ch_G ⇒ match c' with [ ch_G ⇒ true | _ ⇒ false ]
 174  | ch_H ⇒ match c' with [ ch_H ⇒ true | _ ⇒ false ]
 175  | ch_I ⇒ match c' with [ ch_I ⇒ true | _ ⇒ false ]
 176  | ch_J ⇒ match c' with [ ch_J ⇒ true | _ ⇒ false ]
 177  | ch_K ⇒ match c' with [ ch_K ⇒ true | _ ⇒ false ]
 178  | ch_L ⇒ match c' with [ ch_L ⇒ true | _ ⇒ false ]
 179  | ch_M ⇒ match c' with [ ch_M ⇒ true | _ ⇒ false ]
 180  | ch_N ⇒ match c' with [ ch_N ⇒ true | _ ⇒ false ]
 181  | ch_O ⇒ match c' with [ ch_O ⇒ true | _ ⇒ false ]
 182  | ch_P ⇒ match c' with [ ch_P ⇒ true | _ ⇒ false ]
 183  | ch_Q ⇒ match c' with [ ch_Q ⇒ true | _ ⇒ false ]
 184  | ch_R ⇒ match c' with [ ch_R ⇒ true | _ ⇒ false ]
 185  | ch_S ⇒ match c' with [ ch_S ⇒ true | _ ⇒ false ]
 186  | ch_T ⇒ match c' with [ ch_T ⇒ true | _ ⇒ false ]
 187  | ch_U ⇒ match c' with [ ch_U ⇒ true | _ ⇒ false ]
 188  | ch_V ⇒ match c' with [ ch_V ⇒ true | _ ⇒ false ]
 189  | ch_W ⇒ match c' with [ ch_W ⇒ true | _ ⇒ false ]
 190  | ch_X ⇒ match c' with [ ch_X ⇒ true | _ ⇒ false ]
 191  | ch_Y ⇒ match c' with [ ch_Y ⇒ true | _ ⇒ false ]
 192  | ch_Z ⇒ match c' with [ ch_Z ⇒ true | _ ⇒ false ]
 193  | ch_a ⇒ match c' with [ ch_a ⇒ true | _ ⇒ false ]
 194  | ch_b ⇒ match c' with [ ch_b ⇒ true | _ ⇒ false ]
 195  | ch_c ⇒ match c' with [ ch_c ⇒ true | _ ⇒ false ]
 196  | ch_d ⇒ match c' with [ ch_d ⇒ true | _ ⇒ false ]
 197  | ch_e ⇒ match c' with [ ch_e ⇒ true | _ ⇒ false ]
 198  | ch_f ⇒ match c' with [ ch_f ⇒ true | _ ⇒ false ]
 199  | ch_g ⇒ match c' with [ ch_g ⇒ true | _ ⇒ false ]
 200  | ch_h ⇒ match c' with [ ch_h ⇒ true | _ ⇒ false ]
 201  | ch_i ⇒ match c' with [ ch_i ⇒ true | _ ⇒ false ]
 202  | ch_j ⇒ match c' with [ ch_j ⇒ true | _ ⇒ false ]
 203  | ch_k ⇒ match c' with [ ch_k ⇒ true | _ ⇒ false ]
 204  | ch_l ⇒ match c' with [ ch_l ⇒ true | _ ⇒ false ]
 205  | ch_m ⇒ match c' with [ ch_m ⇒ true | _ ⇒ false ]
 206  | ch_n ⇒ match c' with [ ch_n ⇒ true | _ ⇒ false ]
 207  | ch_o ⇒ match c' with [ ch_o ⇒ true | _ ⇒ false ]
 208  | ch_p ⇒ match c' with [ ch_p ⇒ true | _ ⇒ false ]
 209  | ch_q ⇒ match c' with [ ch_q ⇒ true | _ ⇒ false ]
 210  | ch_r ⇒ match c' with [ ch_r ⇒ true | _ ⇒ false ]
 211  | ch_s ⇒ match c' with [ ch_s ⇒ true | _ ⇒ false ]
 212  | ch_t ⇒ match c' with [ ch_t ⇒ true | _ ⇒ false ]
 213  | ch_u ⇒ match c' with [ ch_u ⇒ true | _ ⇒ false ]
 214  | ch_v ⇒ match c' with [ ch_v ⇒ true | _ ⇒ false ]
 215  | ch_w ⇒ match c' with [ ch_w ⇒ true | _ ⇒ false ]
 216  | ch_x ⇒ match c' with [ ch_x ⇒ true | _ ⇒ false ]
 217  | ch_y ⇒ match c' with [ ch_y ⇒ true | _ ⇒ false ]
 218  | ch_z ⇒ match c' with [ ch_z ⇒ true | _ ⇒ false ]
 219  ].