mem, split

[helm.git] / matita / matita / lib / turing / universal / alphabet.ma

diff --git a/matita/matita/lib/turing/universal/alphabet.ma b/matita/matita/lib/turing/universal/alphabet.ma
index 646d8ebbd2cb4beef9bbfabe93937f2cde220b2e..bf2484f29fadf94ae268dc9a7dad93ec54bfafac 100644 (file)
--- a/matita/matita/lib/turing/universal/alphabet.ma
+++ b/matita/matita/lib/turing/universal/alphabet.ma
@@ -20,6 +20,7 @@ include "turing/universal/tests.ma". *)
 
 inductive unialpha : Type[0] ≝ 
 | bit : bool → unialpha
+| null : unialpha
 | comma : unialpha
 | bar : unialpha
 | grid : unialpha.
@@ -27,6 +28,7 @@ inductive unialpha : Type[0] ≝
 definition unialpha_eq ≝ 
   λa1,a2.match a1 with
   [ bit x ⇒ match a2 with [ bit y ⇒ ¬ xorb x y | _ ⇒ false ]
+  | null ⇒ match a2 with [ null ⇒ true | _ ⇒ false ]
   | comma ⇒ match a2 with [ comma ⇒ true | _ ⇒ false ]
   | bar ⇒ match a2 with [ bar ⇒ true | _ ⇒ false ]
   | grid ⇒ match a2 with [ grid ⇒ true | _ ⇒ false ] ].
@@ -34,19 +36,30 @@ definition unialpha_eq ≝
 definition DeqUnialpha ≝ mk_DeqSet unialpha unialpha_eq ?.
 * [ #x * [ #y cases x cases y normalize % // #Hfalse destruct
          | *: normalize % #Hfalse destruct ]
-  |*: * [1,5,9,13: #y ] normalize % #H1 destruct % ]
+  |*: * [1,6,11,16: #y ] normalize % #H1 destruct % ]
 qed.
 
-axiom unialpha_unique : uniqueb DeqUnialpha [bit true;bit false;comma;bar;grid] = true.
+lemma unialpha_unique : 
+  uniqueb DeqUnialpha [bit true;bit false;null;comma;bar;grid] = true.
+// qed.
+
+lemma unialpha_complete :∀x:DeqUnialpha. 
+  memb ? x [bit true;bit false;null;comma;bar;grid] = true.
+* // * //
+qed.
 
 definition FSUnialpha ≝ 
-  mk_FinSet DeqUnialpha [bit true;bit false;comma;bar;grid] unialpha_unique.
+  mk_FinSet DeqUnialpha [bit true;bit false;null;comma;bar;grid] 
+  unialpha_unique unialpha_complete.
 
 definition is_bit ≝ λc.match c with [ bit _ ⇒ true | _ ⇒ false ].
 
+definition is_null ≝ λc.match c with [ null ⇒ true | _ ⇒ false ].
+
 definition is_grid ≝ λc.match c with [ grid ⇒ true | _ ⇒ false ].
 
 definition is_bar ≝ λc.match c with [ bar ⇒ true | _ ⇒ false ].
 
 definition is_comma ≝ λc.match c with [ comma ⇒ true | _ ⇒ false ].
 
+definition bit_or_null ≝ λc.is_bit c ∨ is_null c.