matita/matita/contribs/assembly/string/ascii_min.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 (*                                                                        *)
  17 (* Sviluppato da:                                                         *)
  18 (*   Cosimo Oliboni, oliboni@cs.unibo.it                                  *)
  19 (*                                                                        *)
  20 (* ********************************************************************** *)
  21
  22 include "freescale/byte8.ma".
  23
  24 (* ************************** *)
  25 (* DEFINIZIONE ASCII MINIMALE *)
  26 (* ************************** *)
  27
  28 inductive ascii_min : Type ≝
  29 (* numeri *)
  30   ch_0: ascii_min
  31 | ch_1: ascii_min
  32 | ch_2: ascii_min
  33 | ch_3: ascii_min
  34 | ch_4: ascii_min
  35 | ch_5: ascii_min
  36 | ch_6: ascii_min
  37 | ch_7: ascii_min
  38 | ch_8: ascii_min
  39 | ch_9: ascii_min
  40
  41 (* simboli *)
  42 | ch__: ascii_min
  43
  44 (* maiuscole *)
  45 | ch_A: ascii_min
  46 | ch_B: ascii_min
  47 | ch_C: ascii_min
  48 | ch_D: ascii_min
  49 | ch_E: ascii_min
  50 | ch_F: ascii_min
  51 | ch_G: ascii_min
  52 | ch_H: ascii_min
  53 | ch_I: ascii_min
  54 | ch_J: ascii_min
  55 | ch_K: ascii_min
  56 | ch_L: ascii_min
  57 | ch_M: ascii_min
  58 | ch_N: ascii_min
  59 | ch_O: ascii_min
  60 | ch_P: ascii_min
  61 | ch_Q: ascii_min
  62 | ch_R: ascii_min
  63 | ch_S: ascii_min
  64 | ch_T: ascii_min
  65 | ch_U: ascii_min
  66 | ch_V: ascii_min
  67 | ch_W: ascii_min
  68 | ch_X: ascii_min
  69 | ch_Y: ascii_min
  70 | ch_Z: ascii_min
  71
  72 (* minuscole *)
  73 | ch_a: ascii_min
  74 | ch_b: ascii_min
  75 | ch_c: ascii_min
  76 | ch_d: ascii_min
  77 | ch_e: ascii_min
  78 | ch_f: ascii_min
  79 | ch_g: ascii_min
  80 | ch_h: ascii_min
  81 | ch_i: ascii_min
  82 | ch_j: ascii_min
  83 | ch_k: ascii_min
  84 | ch_l: ascii_min
  85 | ch_m: ascii_min
  86 | ch_n: ascii_min
  87 | ch_o: ascii_min
  88 | ch_p: ascii_min
  89 | ch_q: ascii_min
  90 | ch_r: ascii_min
  91 | ch_s: ascii_min
  92 | ch_t: ascii_min
  93 | ch_u: ascii_min
  94 | ch_v: ascii_min
  95 | ch_w: ascii_min
  96 | ch_x: ascii_min
  97 | ch_y: ascii_min
  98 | ch_z: ascii_min.
  99
 100 (* ascii_min → byte8 *)
 101 definition magic_of_ascii_min ≝
 102 λc:ascii_min.match c with
 103 (* numeri *)
 104 [ ch_0 ⇒ 〈x0,x0〉
 105 | ch_1 ⇒ 〈x0,x1〉
 106 | ch_2 ⇒ 〈x0,x2〉
 107 | ch_3 ⇒ 〈x0,x3〉
 108 | ch_4 ⇒ 〈x0,x4〉
 109 | ch_5 ⇒ 〈x0,x5〉
 110 | ch_6 ⇒ 〈x0,x6〉
 111 | ch_7 ⇒ 〈x0,x7〉
 112 | ch_8 ⇒ 〈x0,x8〉
 113 | ch_9 ⇒ 〈x0,x9〉
 114
 115 (* simboli *)
 116 | ch__ ⇒ 〈x0,xA〉
 117
 118 (* maiuscole *)
 119 | ch_A ⇒ 〈x0,xB〉
 120 | ch_B ⇒ 〈x0,xC〉
 121 | ch_C ⇒ 〈x0,xD〉
 122 | ch_D ⇒ 〈x0,xE〉
 123 | ch_E ⇒ 〈x0,xF〉
 124 | ch_F ⇒ 〈x1,x0〉
 125 | ch_G ⇒ 〈x1,x1〉
 126 | ch_H ⇒ 〈x1,x2〉
 127 | ch_I ⇒ 〈x1,x3〉
 128 | ch_J ⇒ 〈x1,x4〉
 129 | ch_K ⇒ 〈x1,x5〉
 130 | ch_L ⇒ 〈x1,x6〉
 131 | ch_M ⇒ 〈x1,x7〉
 132 | ch_N ⇒ 〈x1,x8〉
 133 | ch_O ⇒ 〈x1,x9〉
 134 | ch_P ⇒ 〈x1,xA〉
 135 | ch_Q ⇒ 〈x1,xB〉
 136 | ch_R ⇒ 〈x1,xC〉
 137 | ch_S ⇒ 〈x1,xD〉
 138 | ch_T ⇒ 〈x1,xE〉
 139 | ch_U ⇒ 〈x1,xF〉
 140 | ch_V ⇒ 〈x2,x0〉
 141 | ch_W ⇒ 〈x2,x1〉
 142 | ch_X ⇒ 〈x2,x2〉
 143 | ch_Y ⇒ 〈x2,x3〉
 144 | ch_Z ⇒ 〈x2,x4〉
 145
 146 (* minuscole *)
 147 | ch_a ⇒ 〈x2,x5〉
 148 | ch_b ⇒ 〈x2,x6〉
 149 | ch_c ⇒ 〈x2,x7〉
 150 | ch_d ⇒ 〈x2,x8〉
 151 | ch_e ⇒ 〈x2,x9〉
 152 | ch_f ⇒ 〈x2,xA〉
 153 | ch_g ⇒ 〈x2,xB〉
 154 | ch_h ⇒ 〈x2,xC〉
 155 | ch_i ⇒ 〈x2,xD〉
 156 | ch_j ⇒ 〈x2,xE〉
 157 | ch_k ⇒ 〈x2,xF〉
 158 | ch_l ⇒ 〈x3,x0〉
 159 | ch_m ⇒ 〈x3,x1〉
 160 | ch_n ⇒ 〈x3,x2〉
 161 | ch_o ⇒ 〈x3,x3〉
 162 | ch_p ⇒ 〈x3,x4〉
 163 | ch_q ⇒ 〈x3,x5〉
 164 | ch_r ⇒ 〈x3,x6〉
 165 | ch_s ⇒ 〈x3,x7〉
 166 | ch_t ⇒ 〈x3,x8〉
 167 | ch_u ⇒ 〈x3,x9〉
 168 | ch_v ⇒ 〈x3,xA〉
 169 | ch_w ⇒ 〈x3,xB〉
 170 | ch_x ⇒ 〈x3,xC〉
 171 | ch_y ⇒ 〈x3,xD〉
 172 | ch_z ⇒ 〈x3,xE〉
 173 ].
 174
 175 (* confronto fra ascii_min *)
 176 definition eqAsciiMin ≝
 177 λc,c':ascii_min.(eq_b8 (magic_of_ascii_min c) (magic_of_ascii_min c')).
 178
 179 lemma eq_to_eqasciimin : ∀a1,a2.a1 = a2 → eqAsciiMin a1 a2 = true.
 180  do 3 intro;
 181  unfold eqAsciiMin;
 182  rewrite > H;
 183  elim a2;
 184  reflexivity.
 185 qed.
 186
 187 (* 63^2 casi... *)
 188 lemma eqasciimin_to_eq_00 : ∀a.eqAsciiMin ch_0 a = true → ch_0 = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
 189 lemma eqasciimin_to_eq_01 : ∀a.eqAsciiMin ch_1 a = true → ch_1 = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
 190 lemma eqasciimin_to_eq_02 : ∀a.eqAsciiMin ch_2 a = true → ch_2 = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
 191 lemma eqasciimin_to_eq_03 : ∀a.eqAsciiMin ch_3 a = true → ch_3 = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
 192 lemma eqasciimin_to_eq_04 : ∀a.eqAsciiMin ch_4 a = true → ch_4 = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
 193 lemma eqasciimin_to_eq_05 : ∀a.eqAsciiMin ch_5 a = true → ch_5 = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
 194 lemma eqasciimin_to_eq_06 : ∀a.eqAsciiMin ch_6 a = true → ch_6 = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
 195 lemma eqasciimin_to_eq_07 : ∀a.eqAsciiMin ch_7 a = true → ch_7 = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
 196 lemma eqasciimin_to_eq_08 : ∀a.eqAsciiMin ch_8 a = true → ch_8 = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
 197 lemma eqasciimin_to_eq_09 : ∀a.eqAsciiMin ch_9 a = true → ch_9 = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
 198 lemma eqasciimin_to_eq_10 : ∀a.eqAsciiMin ch__ a = true → ch__ = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
 199 lemma eqasciimin_to_eq_11 : ∀a.eqAsciiMin ch_A a = true → ch_A = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
 200 lemma eqasciimin_to_eq_12 : ∀a.eqAsciiMin ch_B a = true → ch_B = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
 201 lemma eqasciimin_to_eq_13 : ∀a.eqAsciiMin ch_C a = true → ch_C = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
 202 lemma eqasciimin_to_eq_14 : ∀a.eqAsciiMin ch_D a = true → ch_D = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
 203 lemma eqasciimin_to_eq_15 : ∀a.eqAsciiMin ch_E a = true → ch_E = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
 204 lemma eqasciimin_to_eq_16 : ∀a.eqAsciiMin ch_F a = true → ch_F = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
 205 lemma eqasciimin_to_eq_17 : ∀a.eqAsciiMin ch_G a = true → ch_G = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
 206 lemma eqasciimin_to_eq_18 : ∀a.eqAsciiMin ch_H a = true → ch_H = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
 207 lemma eqasciimin_to_eq_19 : ∀a.eqAsciiMin ch_I a = true → ch_I = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
 208 lemma eqasciimin_to_eq_20 : ∀a.eqAsciiMin ch_J a = true → ch_J = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
 209 lemma eqasciimin_to_eq_21 : ∀a.eqAsciiMin ch_K a = true → ch_K = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
 210 lemma eqasciimin_to_eq_22 : ∀a.eqAsciiMin ch_L a = true → ch_L = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
 211 lemma eqasciimin_to_eq_23 : ∀a.eqAsciiMin ch_M a = true → ch_M = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
 212 lemma eqasciimin_to_eq_24 : ∀a.eqAsciiMin ch_N a = true → ch_N = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
 213 lemma eqasciimin_to_eq_25 : ∀a.eqAsciiMin ch_O a = true → ch_O = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
 214 lemma eqasciimin_to_eq_26 : ∀a.eqAsciiMin ch_P a = true → ch_P = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
 215 lemma eqasciimin_to_eq_27 : ∀a.eqAsciiMin ch_Q a = true → ch_Q = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
 216 lemma eqasciimin_to_eq_28 : ∀a.eqAsciiMin ch_R a = true → ch_R = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
 217 lemma eqasciimin_to_eq_29 : ∀a.eqAsciiMin ch_S a = true → ch_S = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
 218 lemma eqasciimin_to_eq_30 : ∀a.eqAsciiMin ch_T a = true → ch_T = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
 219 lemma eqasciimin_to_eq_31 : ∀a.eqAsciiMin ch_U a = true → ch_U = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
 220 lemma eqasciimin_to_eq_32 : ∀a.eqAsciiMin ch_V a = true → ch_V = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
 221 lemma eqasciimin_to_eq_33 : ∀a.eqAsciiMin ch_W a = true → ch_W = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
 222 lemma eqasciimin_to_eq_34 : ∀a.eqAsciiMin ch_X a = true → ch_X = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
 223 lemma eqasciimin_to_eq_35 : ∀a.eqAsciiMin ch_Y a = true → ch_Y = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
 224 lemma eqasciimin_to_eq_36 : ∀a.eqAsciiMin ch_Z a = true → ch_Z = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
 225 lemma eqasciimin_to_eq_37 : ∀a.eqAsciiMin ch_a a = true → ch_a = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
 226 lemma eqasciimin_to_eq_38 : ∀a.eqAsciiMin ch_b a = true → ch_b = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
 227 lemma eqasciimin_to_eq_39 : ∀a.eqAsciiMin ch_c a = true → ch_c = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
 228 lemma eqasciimin_to_eq_40 : ∀a.eqAsciiMin ch_d a = true → ch_d = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
 229 lemma eqasciimin_to_eq_41 : ∀a.eqAsciiMin ch_e a = true → ch_e = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
 230 lemma eqasciimin_to_eq_42 : ∀a.eqAsciiMin ch_f a = true → ch_f = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
 231 lemma eqasciimin_to_eq_43 : ∀a.eqAsciiMin ch_g a = true → ch_g = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
 232 lemma eqasciimin_to_eq_44 : ∀a.eqAsciiMin ch_h a = true → ch_h = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
 233 lemma eqasciimin_to_eq_45 : ∀a.eqAsciiMin ch_i a = true → ch_i = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
 234 lemma eqasciimin_to_eq_46 : ∀a.eqAsciiMin ch_j a = true → ch_j = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
 235 lemma eqasciimin_to_eq_47 : ∀a.eqAsciiMin ch_k a = true → ch_k = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
 236 lemma eqasciimin_to_eq_48 : ∀a.eqAsciiMin ch_l a = true → ch_l = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
 237 lemma eqasciimin_to_eq_49 : ∀a.eqAsciiMin ch_m a = true → ch_m = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
 238 lemma eqasciimin_to_eq_50 : ∀a.eqAsciiMin ch_n a = true → ch_n = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
 239 lemma eqasciimin_to_eq_51 : ∀a.eqAsciiMin ch_o a = true → ch_o = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
 240 lemma eqasciimin_to_eq_52 : ∀a.eqAsciiMin ch_p a = true → ch_p = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
 241 lemma eqasciimin_to_eq_53 : ∀a.eqAsciiMin ch_q a = true → ch_q = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
 242 lemma eqasciimin_to_eq_54 : ∀a.eqAsciiMin ch_r a = true → ch_r = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
 243 lemma eqasciimin_to_eq_55 : ∀a.eqAsciiMin ch_s a = true → ch_s = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
 244 lemma eqasciimin_to_eq_56 : ∀a.eqAsciiMin ch_t a = true → ch_t = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
 245 lemma eqasciimin_to_eq_57 : ∀a.eqAsciiMin ch_u a = true → ch_u = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
 246 lemma eqasciimin_to_eq_58 : ∀a.eqAsciiMin ch_v a = true → ch_v = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
 247 lemma eqasciimin_to_eq_59 : ∀a.eqAsciiMin ch_w a = true → ch_w = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
 248 lemma eqasciimin_to_eq_60 : ∀a.eqAsciiMin ch_x a = true → ch_x = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
 249 lemma eqasciimin_to_eq_61 : ∀a.eqAsciiMin ch_y a = true → ch_y = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
 250 lemma eqasciimin_to_eq_62 : ∀a.eqAsciiMin ch_z a = true → ch_z = a. intro; elim a 0; normalize; intro; try destruct H; reflexivity. qed.
 251
 252 lemma eqasciimin_to_eq : ∀a1.∀a2.eqAsciiMin a1 a2 = true → a1 = a2.
 253  do 1 intro;
 254  elim a1 0;
 255  [  1: apply eqasciimin_to_eq_00 |  2: apply eqasciimin_to_eq_01 |  3: apply eqasciimin_to_eq_02 |  4: apply eqasciimin_to_eq_03
 256  |  5: apply eqasciimin_to_eq_04 |  6: apply eqasciimin_to_eq_05 |  7: apply eqasciimin_to_eq_06 |  8: apply eqasciimin_to_eq_07
 257  |  9: apply eqasciimin_to_eq_08 | 10: apply eqasciimin_to_eq_09 | 11: apply eqasciimin_to_eq_10 | 12: apply eqasciimin_to_eq_11
 258  | 13: apply eqasciimin_to_eq_12 | 14: apply eqasciimin_to_eq_13 | 15: apply eqasciimin_to_eq_14 | 16: apply eqasciimin_to_eq_15
 259  | 17: apply eqasciimin_to_eq_16 | 18: apply eqasciimin_to_eq_17 | 19: apply eqasciimin_to_eq_18 | 20: apply eqasciimin_to_eq_19
 260  | 21: apply eqasciimin_to_eq_20 | 22: apply eqasciimin_to_eq_21 | 23: apply eqasciimin_to_eq_22 | 24: apply eqasciimin_to_eq_23
 261  | 25: apply eqasciimin_to_eq_24 | 26: apply eqasciimin_to_eq_25 | 27: apply eqasciimin_to_eq_26 | 28: apply eqasciimin_to_eq_27
 262  | 29: apply eqasciimin_to_eq_28 | 30: apply eqasciimin_to_eq_29 | 31: apply eqasciimin_to_eq_30 | 32: apply eqasciimin_to_eq_31
 263  | 33: apply eqasciimin_to_eq_32 | 34: apply eqasciimin_to_eq_33 | 35: apply eqasciimin_to_eq_34 | 36: apply eqasciimin_to_eq_35
 264  | 37: apply eqasciimin_to_eq_36 | 38: apply eqasciimin_to_eq_37 | 39: apply eqasciimin_to_eq_38 | 40: apply eqasciimin_to_eq_39
 265  | 41: apply eqasciimin_to_eq_40 | 42: apply eqasciimin_to_eq_41 | 43: apply eqasciimin_to_eq_42 | 44: apply eqasciimin_to_eq_43
 266  | 45: apply eqasciimin_to_eq_44 | 46: apply eqasciimin_to_eq_45 | 47: apply eqasciimin_to_eq_46 | 48: apply eqasciimin_to_eq_47
 267  | 49: apply eqasciimin_to_eq_48 | 50: apply eqasciimin_to_eq_49 | 51: apply eqasciimin_to_eq_50 | 52: apply eqasciimin_to_eq_51
 268  | 53: apply eqasciimin_to_eq_52 | 54: apply eqasciimin_to_eq_53 | 55: apply eqasciimin_to_eq_54 | 56: apply eqasciimin_to_eq_55
 269  | 57: apply eqasciimin_to_eq_56 | 58: apply eqasciimin_to_eq_57 | 59: apply eqasciimin_to_eq_58 | 60: apply eqasciimin_to_eq_59
 270  | 61: apply eqasciimin_to_eq_60 | 62: apply eqasciimin_to_eq_61 | 63: apply eqasciimin_to_eq_62 ].
 271 qed.