helm/software/matita/contribs/ng_assembly/common/ascii_lemmas.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 (*   Ultima modifica: 05/08/2009                                          *)
  20 (*                                                                        *)
  21 (* ********************************************************************** *)
  22
  23 include "common/ascii.ma".
  24 include "num/bool_lemmas.ma".
  25
  26 (* ************************** *)
  27 (* DEFINIZIONE ASCII MINIMALE *)
  28 (* ************************** *)
  29
  30 ndefinition ascii_destruct_aux ≝
  31 Πc1,c2.ΠP:Prop.c1 = c2 →
  32  match eq_ascii c1 c2 with [ true ⇒ P → P | false ⇒ P ].
  33
  34 nlemma ascii_destruct : ascii_destruct_aux.
  35  #c1; #c2; #P; #H;
  36  nrewrite < H;
  37  nelim c1;
  38  nnormalize;
  39  napply (λx.x).
  40 nqed.
  41
  42 nlemma eq_to_eqascii : ∀n1,n2.n1 = n2 → eq_ascii n1 n2 = true.
  43  #n1; #n2; #H;
  44  nrewrite > H;
  45  nelim n2;
  46  nnormalize;
  47  napply refl_eq.
  48 nqed.
  49
  50 nlemma neqascii_to_neq : ∀n1,n2.eq_ascii n1 n2 = false → n1 ≠ n2.
  51  #n1; #n2; #H;
  52  napply (not_to_not (n1 = n2) (eq_ascii n1 n2 = true) …);
  53  ##[ ##1: napply (eq_to_eqascii n1 n2)
  54  ##| ##2: napply (eqfalse_to_neqtrue … H)
  55  ##]
  56 nqed.
  57
  58 nlemma eqascii_to_eq1 : ∀a2.eq_ascii ch_0 a2 = true → ch_0 = a2. #a2; ncases a2; nnormalize; #H; ##[ ##1: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
  59 nlemma eqascii_to_eq2 : ∀a2.eq_ascii ch_1 a2 = true → ch_1 = a2. #a2; ncases a2; nnormalize; #H; ##[ ##2: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
  60 nlemma eqascii_to_eq3 : ∀a2.eq_ascii ch_2 a2 = true → ch_2 = a2. #a2; ncases a2; nnormalize; #H; ##[ ##3: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
  61 nlemma eqascii_to_eq4 : ∀a2.eq_ascii ch_3 a2 = true → ch_3 = a2. #a2; ncases a2; nnormalize; #H; ##[ ##4: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
  62 nlemma eqascii_to_eq5 : ∀a2.eq_ascii ch_4 a2 = true → ch_4 = a2. #a2; ncases a2; nnormalize; #H; ##[ ##5: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
  63 nlemma eqascii_to_eq6 : ∀a2.eq_ascii ch_5 a2 = true → ch_5 = a2. #a2; ncases a2; nnormalize; #H; ##[ ##6: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
  64 nlemma eqascii_to_eq7 : ∀a2.eq_ascii ch_6 a2 = true → ch_6 = a2. #a2; ncases a2; nnormalize; #H; ##[ ##7: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
  65 nlemma eqascii_to_eq8 : ∀a2.eq_ascii ch_7 a2 = true → ch_7 = a2. #a2; ncases a2; nnormalize; #H; ##[ ##8: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
  66 nlemma eqascii_to_eq9 : ∀a2.eq_ascii ch_8 a2 = true → ch_8 = a2. #a2; ncases a2; nnormalize; #H; ##[ ##9: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
  67 nlemma eqascii_to_eq10 : ∀a2.eq_ascii ch_9 a2 = true → ch_9 = a2. #a2; ncases a2; nnormalize; #H; ##[ ##10: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
  68 nlemma eqascii_to_eq11 : ∀a2.eq_ascii ch__ a2 = true → ch__ = a2. #a2; ncases a2; nnormalize; #H; ##[ ##11: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
  69 nlemma eqascii_to_eq12 : ∀a2.eq_ascii ch_A a2 = true → ch_A = a2. #a2; ncases a2; nnormalize; #H; ##[ ##12: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
  70 nlemma eqascii_to_eq13 : ∀a2.eq_ascii ch_B a2 = true → ch_B = a2. #a2; ncases a2; nnormalize; #H; ##[ ##13: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
  71 nlemma eqascii_to_eq14 : ∀a2.eq_ascii ch_C a2 = true → ch_C = a2. #a2; ncases a2; nnormalize; #H; ##[ ##14: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
  72 nlemma eqascii_to_eq15 : ∀a2.eq_ascii ch_D a2 = true → ch_D = a2. #a2; ncases a2; nnormalize; #H; ##[ ##15: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
  73 nlemma eqascii_to_eq16 : ∀a2.eq_ascii ch_E a2 = true → ch_E = a2. #a2; ncases a2; nnormalize; #H; ##[ ##16: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
  74 nlemma eqascii_to_eq17 : ∀a2.eq_ascii ch_F a2 = true → ch_F = a2. #a2; ncases a2; nnormalize; #H; ##[ ##17: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
  75 nlemma eqascii_to_eq18 : ∀a2.eq_ascii ch_G a2 = true → ch_G = a2. #a2; ncases a2; nnormalize; #H; ##[ ##18: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
  76 nlemma eqascii_to_eq19 : ∀a2.eq_ascii ch_H a2 = true → ch_H = a2. #a2; ncases a2; nnormalize; #H; ##[ ##19: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
  77 nlemma eqascii_to_eq20 : ∀a2.eq_ascii ch_I a2 = true → ch_I = a2. #a2; ncases a2; nnormalize; #H; ##[ ##20: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
  78 nlemma eqascii_to_eq21 : ∀a2.eq_ascii ch_J a2 = true → ch_J = a2. #a2; ncases a2; nnormalize; #H; ##[ ##21: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
  79 nlemma eqascii_to_eq22 : ∀a2.eq_ascii ch_K a2 = true → ch_K = a2. #a2; ncases a2; nnormalize; #H; ##[ ##22: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
  80 nlemma eqascii_to_eq23 : ∀a2.eq_ascii ch_L a2 = true → ch_L = a2. #a2; ncases a2; nnormalize; #H; ##[ ##23: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
  81 nlemma eqascii_to_eq24 : ∀a2.eq_ascii ch_M a2 = true → ch_M = a2. #a2; ncases a2; nnormalize; #H; ##[ ##24: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
  82 nlemma eqascii_to_eq25 : ∀a2.eq_ascii ch_N a2 = true → ch_N = a2. #a2; ncases a2; nnormalize; #H; ##[ ##25: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
  83 nlemma eqascii_to_eq26 : ∀a2.eq_ascii ch_O a2 = true → ch_O = a2. #a2; ncases a2; nnormalize; #H; ##[ ##26: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
  84 nlemma eqascii_to_eq27 : ∀a2.eq_ascii ch_P a2 = true → ch_P = a2. #a2; ncases a2; nnormalize; #H; ##[ ##27: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
  85 nlemma eqascii_to_eq28 : ∀a2.eq_ascii ch_Q a2 = true → ch_Q = a2. #a2; ncases a2; nnormalize; #H; ##[ ##28: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
  86 nlemma eqascii_to_eq29 : ∀a2.eq_ascii ch_R a2 = true → ch_R = a2. #a2; ncases a2; nnormalize; #H; ##[ ##29: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
  87 nlemma eqascii_to_eq30 : ∀a2.eq_ascii ch_S a2 = true → ch_S = a2. #a2; ncases a2; nnormalize; #H; ##[ ##30: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
  88 nlemma eqascii_to_eq31 : ∀a2.eq_ascii ch_T a2 = true → ch_T = a2. #a2; ncases a2; nnormalize; #H; ##[ ##31: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
  89 nlemma eqascii_to_eq32 : ∀a2.eq_ascii ch_U a2 = true → ch_U = a2. #a2; ncases a2; nnormalize; #H; ##[ ##32: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
  90 nlemma eqascii_to_eq33 : ∀a2.eq_ascii ch_V a2 = true → ch_V = a2. #a2; ncases a2; nnormalize; #H; ##[ ##33: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
  91 nlemma eqascii_to_eq34 : ∀a2.eq_ascii ch_W a2 = true → ch_W = a2. #a2; ncases a2; nnormalize; #H; ##[ ##34: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
  92 nlemma eqascii_to_eq35 : ∀a2.eq_ascii ch_X a2 = true → ch_X = a2. #a2; ncases a2; nnormalize; #H; ##[ ##35: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
  93 nlemma eqascii_to_eq36 : ∀a2.eq_ascii ch_Y a2 = true → ch_Y = a2. #a2; ncases a2; nnormalize; #H; ##[ ##36: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
  94 nlemma eqascii_to_eq37 : ∀a2.eq_ascii ch_Z a2 = true → ch_Z = a2. #a2; ncases a2; nnormalize; #H; ##[ ##37: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
  95 nlemma eqascii_to_eq38 : ∀a2.eq_ascii ch_a a2 = true → ch_a = a2. #a2; ncases a2; nnormalize; #H; ##[ ##38: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
  96 nlemma eqascii_to_eq39 : ∀a2.eq_ascii ch_b a2 = true → ch_b = a2. #a2; ncases a2; nnormalize; #H; ##[ ##39: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
  97 nlemma eqascii_to_eq40 : ∀a2.eq_ascii ch_c a2 = true → ch_c = a2. #a2; ncases a2; nnormalize; #H; ##[ ##40: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
  98 nlemma eqascii_to_eq41 : ∀a2.eq_ascii ch_d a2 = true → ch_d = a2. #a2; ncases a2; nnormalize; #H; ##[ ##41: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
  99 nlemma eqascii_to_eq42 : ∀a2.eq_ascii ch_e a2 = true → ch_e = a2. #a2; ncases a2; nnormalize; #H; ##[ ##42: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
 100 nlemma eqascii_to_eq43 : ∀a2.eq_ascii ch_f a2 = true → ch_f = a2. #a2; ncases a2; nnormalize; #H; ##[ ##43: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
 101 nlemma eqascii_to_eq44 : ∀a2.eq_ascii ch_g a2 = true → ch_g = a2. #a2; ncases a2; nnormalize; #H; ##[ ##44: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
 102 nlemma eqascii_to_eq45 : ∀a2.eq_ascii ch_h a2 = true → ch_h = a2. #a2; ncases a2; nnormalize; #H; ##[ ##45: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
 103 nlemma eqascii_to_eq46 : ∀a2.eq_ascii ch_i a2 = true → ch_i = a2. #a2; ncases a2; nnormalize; #H; ##[ ##46: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
 104 nlemma eqascii_to_eq47 : ∀a2.eq_ascii ch_j a2 = true → ch_j = a2. #a2; ncases a2; nnormalize; #H; ##[ ##47: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
 105 nlemma eqascii_to_eq48 : ∀a2.eq_ascii ch_k a2 = true → ch_k = a2. #a2; ncases a2; nnormalize; #H; ##[ ##48: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
 106 nlemma eqascii_to_eq49 : ∀a2.eq_ascii ch_l a2 = true → ch_l = a2. #a2; ncases a2; nnormalize; #H; ##[ ##49: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
 107 nlemma eqascii_to_eq50 : ∀a2.eq_ascii ch_m a2 = true → ch_m = a2. #a2; ncases a2; nnormalize; #H; ##[ ##50: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
 108 nlemma eqascii_to_eq51 : ∀a2.eq_ascii ch_n a2 = true → ch_n = a2. #a2; ncases a2; nnormalize; #H; ##[ ##51: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
 109 nlemma eqascii_to_eq52 : ∀a2.eq_ascii ch_o a2 = true → ch_o = a2. #a2; ncases a2; nnormalize; #H; ##[ ##52: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
 110 nlemma eqascii_to_eq53 : ∀a2.eq_ascii ch_p a2 = true → ch_p = a2. #a2; ncases a2; nnormalize; #H; ##[ ##53: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
 111 nlemma eqascii_to_eq54 : ∀a2.eq_ascii ch_q a2 = true → ch_q = a2. #a2; ncases a2; nnormalize; #H; ##[ ##54: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
 112 nlemma eqascii_to_eq55 : ∀a2.eq_ascii ch_r a2 = true → ch_r = a2. #a2; ncases a2; nnormalize; #H; ##[ ##55: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
 113 nlemma eqascii_to_eq56 : ∀a2.eq_ascii ch_s a2 = true → ch_s = a2. #a2; ncases a2; nnormalize; #H; ##[ ##56: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
 114 nlemma eqascii_to_eq57 : ∀a2.eq_ascii ch_t a2 = true → ch_t = a2. #a2; ncases a2; nnormalize; #H; ##[ ##57: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
 115 nlemma eqascii_to_eq58 : ∀a2.eq_ascii ch_u a2 = true → ch_u = a2. #a2; ncases a2; nnormalize; #H; ##[ ##58: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
 116 nlemma eqascii_to_eq59 : ∀a2.eq_ascii ch_v a2 = true → ch_v = a2. #a2; ncases a2; nnormalize; #H; ##[ ##59: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
 117 nlemma eqascii_to_eq60 : ∀a2.eq_ascii ch_w a2 = true → ch_w = a2. #a2; ncases a2; nnormalize; #H; ##[ ##60: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
 118 nlemma eqascii_to_eq61 : ∀a2.eq_ascii ch_x a2 = true → ch_x = a2. #a2; ncases a2; nnormalize; #H; ##[ ##61: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
 119 nlemma eqascii_to_eq62 : ∀a2.eq_ascii ch_y a2 = true → ch_y = a2. #a2; ncases a2; nnormalize; #H; ##[ ##62: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
 120 nlemma eqascii_to_eq63 : ∀a2.eq_ascii ch_z a2 = true → ch_z = a2. #a2; ncases a2; nnormalize; #H; ##[ ##63: napply refl_eq | ##*: napply (bool_destruct … H) ##] nqed.
 121
 122 nlemma eqascii_to_eq : ∀c1,c2.eq_ascii c1 c2 = true → c1 = c2.
 123  #c1; ncases c1;
 124  ##[ ##1: napply eqascii_to_eq1 ##| ##2: napply eqascii_to_eq2
 125  ##| ##3: napply eqascii_to_eq3 ##| ##4: napply eqascii_to_eq4
 126  ##| ##5: napply eqascii_to_eq5 ##| ##6: napply eqascii_to_eq6
 127  ##| ##7: napply eqascii_to_eq7 ##| ##8: napply eqascii_to_eq8
 128  ##| ##9: napply eqascii_to_eq9 ##| ##10: napply eqascii_to_eq10
 129  ##| ##11: napply eqascii_to_eq11 ##| ##12: napply eqascii_to_eq12
 130  ##| ##13: napply eqascii_to_eq13 ##| ##14: napply eqascii_to_eq14
 131  ##| ##15: napply eqascii_to_eq15 ##| ##16: napply eqascii_to_eq16
 132  ##| ##17: napply eqascii_to_eq17 ##| ##18: napply eqascii_to_eq18
 133  ##| ##19: napply eqascii_to_eq19 ##| ##20: napply eqascii_to_eq20
 134  ##| ##21: napply eqascii_to_eq21 ##| ##22: napply eqascii_to_eq22
 135  ##| ##23: napply eqascii_to_eq23 ##| ##24: napply eqascii_to_eq24
 136  ##| ##25: napply eqascii_to_eq25 ##| ##26: napply eqascii_to_eq26
 137  ##| ##27: napply eqascii_to_eq27 ##| ##28: napply eqascii_to_eq28
 138  ##| ##29: napply eqascii_to_eq29 ##| ##30: napply eqascii_to_eq30
 139  ##| ##31: napply eqascii_to_eq31 ##| ##32: napply eqascii_to_eq32
 140  ##| ##33: napply eqascii_to_eq33 ##| ##34: napply eqascii_to_eq34
 141  ##| ##35: napply eqascii_to_eq35 ##| ##36: napply eqascii_to_eq36
 142  ##| ##37: napply eqascii_to_eq37 ##| ##38: napply eqascii_to_eq38
 143  ##| ##39: napply eqascii_to_eq39 ##| ##40: napply eqascii_to_eq40
 144  ##| ##41: napply eqascii_to_eq41 ##| ##42: napply eqascii_to_eq42
 145  ##| ##43: napply eqascii_to_eq43 ##| ##44: napply eqascii_to_eq44
 146  ##| ##45: napply eqascii_to_eq45 ##| ##46: napply eqascii_to_eq46
 147  ##| ##47: napply eqascii_to_eq47 ##| ##48: napply eqascii_to_eq48
 148  ##| ##49: napply eqascii_to_eq49 ##| ##50: napply eqascii_to_eq50
 149  ##| ##51: napply eqascii_to_eq51 ##| ##52: napply eqascii_to_eq52
 150  ##| ##53: napply eqascii_to_eq53 ##| ##54: napply eqascii_to_eq54
 151  ##| ##55: napply eqascii_to_eq55 ##| ##56: napply eqascii_to_eq56
 152  ##| ##57: napply eqascii_to_eq57 ##| ##58: napply eqascii_to_eq58
 153  ##| ##59: napply eqascii_to_eq59 ##| ##60: napply eqascii_to_eq60
 154  ##| ##61: napply eqascii_to_eq61 ##| ##62: napply eqascii_to_eq62
 155  ##| ##63: napply eqascii_to_eq63 ##]
 156 nqed.
 157
 158 nlemma neq_to_neqascii : ∀n1,n2.n1 ≠ n2 → eq_ascii n1 n2 = false.
 159  #n1; #n2; #H;
 160  napply (neqtrue_to_eqfalse (eq_ascii n1 n2));
 161  napply (not_to_not (eq_ascii n1 n2 = true) (n1 = n2) ? H);
 162  napply (eqascii_to_eq n1 n2).
 163 nqed.
 164
 165 nlemma decidable_ascii : ∀x,y:ascii.decidable (x = y).
 166  #x; #y; nnormalize;
 167  napply (or2_elim (eq_ascii x y = true) (eq_ascii x y = false) ? (decidable_bexpr ?));
 168  ##[ ##1: #H; napply (or2_intro1 (x = y) (x ≠ y) (eqascii_to_eq … H))
 169  ##| ##2: #H; napply (or2_intro2 (x = y) (x ≠ y) (neqascii_to_neq … H))
 170  ##]
 171 nqed.
 172
 173 nlemma symmetric_eqascii : symmetricT ascii bool eq_ascii.
 174  #n1; #n2;
 175  napply (or2_elim (n1 = n2) (n1 ≠ n2) ? (decidable_ascii n1 n2));
 176  ##[ ##1: #H; nrewrite > H; napply refl_eq
 177  ##| ##2: #H; nrewrite > (neq_to_neqascii n1 n2 H);
 178           napply (symmetric_eq ? (eq_ascii n2 n1) false);
 179           napply (neq_to_neqascii n2 n1 (symmetric_neq ? n1 n2 H))
 180  ##]
 181 nqed.