matita/matita/contribs/ng_assembly2/common/ascii_base.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: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
  19 (*   Sviluppo: 2008-2010                                                  *)
  20 (*                                                                        *)
  21 (* ********************************************************************** *)
  22
  23 include "num/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 (* iteratore sugli ascii *)
 102 ndefinition forall_ascii ≝ λP.
 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 ⊗
 104  P ch_8 ⊗ P ch_9 ⊗ P ch__ ⊗ P ch_A ⊗ P ch_B ⊗ P ch_C ⊗ P ch_D ⊗ P ch_E ⊗
 105  P ch_F ⊗ P ch_G ⊗ P ch_H ⊗ P ch_I ⊗ P ch_J ⊗ P ch_K ⊗ P ch_L ⊗ P ch_M ⊗
 106  P ch_N ⊗ P ch_O ⊗ P ch_P ⊗ P ch_Q ⊗ P ch_R ⊗ P ch_S ⊗ P ch_T ⊗ P ch_U ⊗
 107  P ch_V ⊗ P ch_W ⊗ P ch_X ⊗ P ch_Y ⊗ P ch_Z ⊗ P ch_a ⊗ P ch_b ⊗ P ch_c ⊗
 108  P ch_d ⊗ P ch_e ⊗ P ch_f ⊗ P ch_g ⊗ P ch_h ⊗ P ch_i ⊗ P ch_j ⊗ P ch_k ⊗
 109  P ch_l ⊗ P ch_m ⊗ P ch_n ⊗ P ch_o ⊗ P ch_p ⊗ P ch_q ⊗ P ch_r ⊗ P ch_s ⊗
 110  P ch_t ⊗ P ch_u ⊗ P ch_v ⊗ P ch_w ⊗ P ch_x ⊗ P ch_y ⊗ P ch_z.
 111
 112 (* confronto fra ascii *)
 113 ndefinition eq_ascii ≝
 114 λc,c':ascii.match c with
 115  [ ch_0 ⇒ match c' with [ ch_0 ⇒ true | _ ⇒ false ] | ch_1 ⇒ match c' with [ ch_1 ⇒ true | _ ⇒ false ]
 116  | ch_2 ⇒ match c' with [ ch_2 ⇒ true | _ ⇒ false ] | ch_3 ⇒ match c' with [ ch_3 ⇒ true | _ ⇒ false ]
 117  | ch_4 ⇒ match c' with [ ch_4 ⇒ true | _ ⇒ false ] | ch_5 ⇒ match c' with [ ch_5 ⇒ true | _ ⇒ false ]
 118  | ch_6 ⇒ match c' with [ ch_6 ⇒ true | _ ⇒ false ] | ch_7 ⇒ match c' with [ ch_7 ⇒ true | _ ⇒ false ]
 119  | ch_8 ⇒ match c' with [ ch_8 ⇒ true | _ ⇒ false ] | ch_9 ⇒ match c' with [ ch_9 ⇒ true | _ ⇒ false ]
 120  | ch__ ⇒ match c' with [ ch__ ⇒ true | _ ⇒ false ] | ch_A ⇒ match c' with [ ch_A ⇒ true | _ ⇒ false ]
 121  | ch_B ⇒ match c' with [ ch_B ⇒ true | _ ⇒ false ] | ch_C ⇒ match c' with [ ch_C ⇒ true | _ ⇒ false ]
 122  | ch_D ⇒ match c' with [ ch_D ⇒ true | _ ⇒ false ] | ch_E ⇒ match c' with [ ch_E ⇒ true | _ ⇒ false ]
 123  | ch_F ⇒ match c' with [ ch_F ⇒ true | _ ⇒ false ] | ch_G ⇒ match c' with [ ch_G ⇒ true | _ ⇒ false ]
 124  | ch_H ⇒ match c' with [ ch_H ⇒ true | _ ⇒ false ] | ch_I ⇒ match c' with [ ch_I ⇒ true | _ ⇒ false ]
 125  | ch_J ⇒ match c' with [ ch_J ⇒ true | _ ⇒ false ] | ch_K ⇒ match c' with [ ch_K ⇒ true | _ ⇒ false ]
 126  | ch_L ⇒ match c' with [ ch_L ⇒ true | _ ⇒ false ] | ch_M ⇒ match c' with [ ch_M ⇒ true | _ ⇒ false ]
 127  | ch_N ⇒ match c' with [ ch_N ⇒ true | _ ⇒ false ] | ch_O ⇒ match c' with [ ch_O ⇒ true | _ ⇒ false ]
 128  | ch_P ⇒ match c' with [ ch_P ⇒ true | _ ⇒ false ] | ch_Q ⇒ match c' with [ ch_Q ⇒ true | _ ⇒ false ]
 129  | ch_R ⇒ match c' with [ ch_R ⇒ true | _ ⇒ false ] | ch_S ⇒ match c' with [ ch_S ⇒ true | _ ⇒ false ]
 130  | ch_T ⇒ match c' with [ ch_T ⇒ true | _ ⇒ false ] | ch_U ⇒ match c' with [ ch_U ⇒ true | _ ⇒ false ]
 131  | ch_V ⇒ match c' with [ ch_V ⇒ true | _ ⇒ false ] | ch_W ⇒ match c' with [ ch_W ⇒ true | _ ⇒ false ]
 132  | ch_X ⇒ match c' with [ ch_X ⇒ true | _ ⇒ false ] | ch_Y ⇒ match c' with [ ch_Y ⇒ true | _ ⇒ false ]
 133  | ch_Z ⇒ match c' with [ ch_Z ⇒ true | _ ⇒ false ] | ch_a ⇒ match c' with [ ch_a ⇒ true | _ ⇒ false ]
 134  | ch_b ⇒ match c' with [ ch_b ⇒ true | _ ⇒ false ] | ch_c ⇒ match c' with [ ch_c ⇒ true | _ ⇒ false ]
 135  | ch_d ⇒ match c' with [ ch_d ⇒ true | _ ⇒ false ] | ch_e ⇒ match c' with [ ch_e ⇒ true | _ ⇒ false ]
 136  | ch_f ⇒ match c' with [ ch_f ⇒ true | _ ⇒ false ] | ch_g ⇒ match c' with [ ch_g ⇒ true | _ ⇒ false ]
 137  | ch_h ⇒ match c' with [ ch_h ⇒ true | _ ⇒ false ] | ch_i ⇒ match c' with [ ch_i ⇒ true | _ ⇒ false ]
 138  | ch_j ⇒ match c' with [ ch_j ⇒ true | _ ⇒ false ] | ch_k ⇒ match c' with [ ch_k ⇒ true | _ ⇒ false ]
 139  | ch_l ⇒ match c' with [ ch_l ⇒ true | _ ⇒ false ] | ch_m ⇒ match c' with [ ch_m ⇒ true | _ ⇒ false ]
 140  | ch_n ⇒ match c' with [ ch_n ⇒ true | _ ⇒ false ] | ch_o ⇒ match c' with [ ch_o ⇒ true | _ ⇒ false ]
 141  | ch_p ⇒ match c' with [ ch_p ⇒ true | _ ⇒ false ] | ch_q ⇒ match c' with [ ch_q ⇒ true | _ ⇒ false ]
 142  | ch_r ⇒ match c' with [ ch_r ⇒ true | _ ⇒ false ] | ch_s ⇒ match c' with [ ch_s ⇒ true | _ ⇒ false ]
 143  | ch_t ⇒ match c' with [ ch_t ⇒ true | _ ⇒ false ] | ch_u ⇒ match c' with [ ch_u ⇒ true | _ ⇒ false ]
 144  | ch_v ⇒ match c' with [ ch_v ⇒ true | _ ⇒ false ] | ch_w ⇒ match c' with [ ch_w ⇒ true | _ ⇒ false ]
 145  | ch_x ⇒ match c' with [ ch_x ⇒ true | _ ⇒ false ] | ch_y ⇒ match c' with [ ch_y ⇒ true | _ ⇒ false ]
 146  | ch_z ⇒ match c' with [ ch_z ⇒ true | _ ⇒ false ]
 147  ].