1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* ********************************************************************** *)
16 (* Progetto FreeScale *)
18 (* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *)
19 (* Cosimo Oliboni, oliboni@cs.unibo.it *)
21 (* ********************************************************************** *)
23 include "freescale/bool.ma".
25 (* ************************** *)
26 (* DEFINIZIONE ASCII MINIMALE *)
27 (* ************************** *)
29 ninductive ascii : Type ≝
101 ndefinition ascii_ind
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 ≝
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.
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 ].
127 ndefinition ascii_rec
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 ≝
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.
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 ].
153 ndefinition ascii_rect
155 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__ →
156 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 →
157 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 →
158 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 →
159 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 →
160 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 ≝
162 λ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.
163 λ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.
164 λ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.
165 λ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.
166 λ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.
167 λ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.
168 λ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.
170 [ ch_0 ⇒ p | ch_1 ⇒ p1 | ch_2 ⇒ p2 | ch_3 ⇒ p3 | ch_4 ⇒ p4 | ch_5 ⇒ p5 | ch_6 ⇒ p6 | ch_7 ⇒ p7
171 | ch_8 ⇒ p8 | ch_9 ⇒ p9 | ch__ ⇒ p10 | ch_A ⇒ p11 | ch_B ⇒ p12 | ch_C ⇒ p13 | ch_D ⇒ p14 | ch_E ⇒ p15
172 | ch_F ⇒ p16 | ch_G ⇒ p17 | ch_H ⇒ p18 | ch_I ⇒ p19 | ch_J ⇒ p20 | ch_K ⇒ p21 | ch_L ⇒ p22 | ch_M ⇒ p23
173 | ch_N ⇒ p24 | ch_O ⇒ p25 | ch_P ⇒ p26 | ch_Q ⇒ p27 | ch_R ⇒ p28 | ch_S ⇒ p29 | ch_T ⇒ p30 | ch_U ⇒ p31
174 | ch_V ⇒ p32 | ch_W ⇒ p33 | ch_X ⇒ p34 | ch_Y ⇒ p35 | ch_Z ⇒ p36 | ch_a ⇒ p37 | ch_b ⇒ p38 | ch_c ⇒ p39
175 | ch_d ⇒ p40 | ch_e ⇒ p41 | ch_f ⇒ p42 | ch_g ⇒ p43 | ch_h ⇒ p44 | ch_i ⇒ p45 | ch_j ⇒ p46 | ch_k ⇒ p47
176 | ch_l ⇒ p48 | ch_m ⇒ p49 | ch_n ⇒ p50 | ch_o ⇒ p51 | ch_p ⇒ p52 | ch_q ⇒ p53 | ch_r ⇒ p54 | ch_s ⇒ p55
177 | ch_t ⇒ p56 | ch_u ⇒ p57 | ch_v ⇒ p58 | ch_w ⇒ p59 | ch_x ⇒ p60 | ch_y ⇒ p61 | ch_z ⇒ p62 ].
179 (* confronto fra ascii *)
180 ndefinition eq_ascii ≝
181 λc,c':ascii.match c with
182 [ ch_0 ⇒ match c' with [ ch_0 ⇒ true | _ ⇒ false ]
183 | ch_1 ⇒ match c' with [ ch_1 ⇒ true | _ ⇒ false ]
184 | ch_2 ⇒ match c' with [ ch_2 ⇒ true | _ ⇒ false ]
185 | ch_3 ⇒ match c' with [ ch_3 ⇒ true | _ ⇒ false ]
186 | ch_4 ⇒ match c' with [ ch_4 ⇒ true | _ ⇒ false ]
187 | ch_5 ⇒ match c' with [ ch_5 ⇒ true | _ ⇒ false ]
188 | ch_6 ⇒ match c' with [ ch_6 ⇒ true | _ ⇒ false ]
189 | ch_7 ⇒ match c' with [ ch_7 ⇒ true | _ ⇒ false ]
190 | ch_8 ⇒ match c' with [ ch_8 ⇒ true | _ ⇒ false ]
191 | ch_9 ⇒ match c' with [ ch_9 ⇒ true | _ ⇒ false ]
192 | ch__ ⇒ match c' with [ ch__ ⇒ 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 | ch_a ⇒ match c' with [ ch_a ⇒ true | _ ⇒ false ]
220 | ch_b ⇒ match c' with [ ch_b ⇒ true | _ ⇒ false ]
221 | ch_c ⇒ match c' with [ ch_c ⇒ true | _ ⇒ false ]
222 | ch_d ⇒ match c' with [ ch_d ⇒ true | _ ⇒ false ]
223 | ch_e ⇒ match c' with [ ch_e ⇒ true | _ ⇒ false ]
224 | ch_f ⇒ match c' with [ ch_f ⇒ true | _ ⇒ false ]
225 | ch_g ⇒ match c' with [ ch_g ⇒ true | _ ⇒ false ]
226 | ch_h ⇒ match c' with [ ch_h ⇒ true | _ ⇒ false ]
227 | ch_i ⇒ match c' with [ ch_i ⇒ true | _ ⇒ false ]
228 | ch_j ⇒ match c' with [ ch_j ⇒ true | _ ⇒ false ]
229 | ch_k ⇒ match c' with [ ch_k ⇒ true | _ ⇒ false ]
230 | ch_l ⇒ match c' with [ ch_l ⇒ true | _ ⇒ false ]
231 | ch_m ⇒ match c' with [ ch_m ⇒ true | _ ⇒ false ]
232 | ch_n ⇒ match c' with [ ch_n ⇒ true | _ ⇒ false ]
233 | ch_o ⇒ match c' with [ ch_o ⇒ true | _ ⇒ false ]
234 | ch_p ⇒ match c' with [ ch_p ⇒ true | _ ⇒ false ]
235 | ch_q ⇒ match c' with [ ch_q ⇒ true | _ ⇒ false ]
236 | ch_r ⇒ match c' with [ ch_r ⇒ true | _ ⇒ false ]
237 | ch_s ⇒ match c' with [ ch_s ⇒ true | _ ⇒ false ]
238 | ch_t ⇒ match c' with [ ch_t ⇒ true | _ ⇒ false ]
239 | ch_u ⇒ match c' with [ ch_u ⇒ true | _ ⇒ false ]
240 | ch_v ⇒ match c' with [ ch_v ⇒ true | _ ⇒ false ]
241 | ch_w ⇒ match c' with [ ch_w ⇒ true | _ ⇒ false ]
242 | ch_x ⇒ match c' with [ ch_x ⇒ true | _ ⇒ false ]
243 | ch_y ⇒ match c' with [ ch_y ⇒ true | _ ⇒ false ]
244 | ch_z ⇒ match c' with [ ch_z ⇒ true | _ ⇒ false ]