2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department of the University of Bologna, Italy.
8 \ / This file is distributed under the terms of the
9 \ / GNU General Public License Version 2
10 V_____________________________________________________________*)
13 (* ALphabet of the universal machine *)
15 include "basics/finset.ma".
18 include "turing/if_machine.ma".
19 include "turing/universal/tests.ma". *)
21 inductive unialpha : Type[0] ≝
22 | bit : bool → unialpha
28 definition unialpha_eq ≝
30 [ bit x ⇒ match a2 with [ bit y ⇒ ¬ xorb x y | _ ⇒ false ]
31 | null ⇒ match a2 with [ null ⇒ true | _ ⇒ false ]
32 | comma ⇒ match a2 with [ comma ⇒ true | _ ⇒ false ]
33 | bar ⇒ match a2 with [ bar ⇒ true | _ ⇒ false ]
34 | grid ⇒ match a2 with [ grid ⇒ true | _ ⇒ false ] ].
36 definition DeqUnialpha ≝ mk_DeqSet unialpha unialpha_eq ?.
37 * [ #x * [ #y cases x cases y normalize % // #Hfalse destruct
38 | *: normalize % #Hfalse destruct ]
39 |*: * [1,6,11,16: #y ] normalize % #H1 destruct % ]
42 lemma unialpha_unique :
43 uniqueb DeqUnialpha [bit true;bit false;null;comma;bar;grid] = true.
46 lemma unialpha_complete :∀x:DeqUnialpha.
47 memb ? x [bit true;bit false;null;comma;bar;grid] = true.
51 definition FSUnialpha ≝
52 mk_FinSet DeqUnialpha [bit true;bit false;null;comma;bar;grid]
53 unialpha_unique unialpha_complete.
55 (*************************** testing characters *******************************)
56 definition is_bit ≝ λc.match c with [ bit _ ⇒ true | _ ⇒ false ].
58 definition is_null ≝ λc.match c with [ null ⇒ true | _ ⇒ false ].
60 definition is_grid ≝ λc.match c with [ grid ⇒ true | _ ⇒ false ].
62 definition is_bar ≝ λc.match c with [ bar ⇒ true | _ ⇒ false ].
64 definition is_comma ≝ λc.match c with [ comma ⇒ true | _ ⇒ false ].
66 definition bit_or_null ≝ λc.is_bit c ∨ is_null c.
68 lemma bit_not_grid: ∀d. is_bit d = true → is_grid d = false.
69 * // normalize #H destruct
72 lemma bit_or_null_not_grid: ∀d. bit_or_null d = true → is_grid d = false.
73 * // normalize #H destruct
76 lemma bit_not_bar: ∀d. is_bit d = true → is_bar d = false.
77 * // normalize #H destruct
80 lemma bit_or_null_not_bar: ∀d. bit_or_null d = true → is_bar d = false.
81 * // normalize #H destruct
84 lemma is_bit_to_bit_or_null :
85 ∀x.is_bit x = true → bit_or_null x = true.
86 * // normalize #H destruct
89 (**************************** testing strings *********************************)
90 definition is_marked ≝ λalpha.λp:FinProd … alpha FinBool.
93 definition STape ≝ FinProd … FSUnialpha FinBool.
95 definition only_bits ≝ λl.
96 ∀c.memb STape c l = true → is_bit (\fst c) = true.
98 definition only_bits_or_nulls ≝ λl.
99 ∀c.memb STape c l = true → bit_or_null (\fst c) = true.
101 definition no_grids ≝ λl.
102 ∀c.memb STape c l = true → is_grid (\fst c) = false.
104 definition no_bars ≝ λl.
105 ∀c.memb STape c l = true → is_bar (\fst c) = false.
107 definition no_marks ≝ λl.
108 ∀c.memb STape c l = true → is_marked ? c = false.
110 definition bar_or_grid ≝ λc:STape.is_bar (\fst c) ∨ is_grid (\fst c).