cfg_to_obj completed (modulo daemons)

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

diff --git a/matita/matita/lib/turing/multi_universal/alphabet.ma b/matita/matita/lib/turing/multi_universal/alphabet.ma
index deb1dceec1f4247d133d5a4bb4e9caf104f3dc0c..1c4cd806073449a11932a251dba46b405e1fc5d5 100644 (file)
--- a/matita/matita/lib/turing/multi_universal/alphabet.ma
+++ b/matita/matita/lib/turing/multi_universal/alphabet.ma
@@ -1,47 +1,59 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic   
+    ||A||  Library of Mathematics, developed at the Computer Science 
+    ||T||  Department of the University of Bologna, Italy.           
+    ||I||                                                            
+    ||T||  
+    ||A||  
+    \   /  This file is distributed under the terms of the       
+     \ /   GNU General Public License Version 2   
+      V_____________________________________________________________*)
 
 include "basics/finset.ma".
+include "basics/lists/list.ma".
 
 inductive unialpha : Type[0] ≝ 
-| bit : bool → unialpha
-| bar : unialpha.
+| bit  : bool → unialpha
+| null : unialpha
+| bar  : unialpha.
 
 definition unialpha_eq ≝ 
   λa1,a2.match a1 with
   [ bit x ⇒ match a2 with [ bit y ⇒ ¬ xorb x y | _ ⇒ false ]
-  | bar ⇒ match a2 with [ bar ⇒ true | _ ⇒ false ] ].
+  | bar ⇒ match a2 with [ bar ⇒ true | _ ⇒ false ] 
+  | null ⇒ match a2 with [ null ⇒ true | _ ⇒ false ] ].
   
 definition DeqUnialpha ≝ mk_DeqSet unialpha unialpha_eq ?.
 * [ #x * [ #y cases x cases y normalize % // #Hfalse destruct
          | *: normalize % #Hfalse destruct ]
-  | * [ #y ] normalize % #H1 destruct % ]
+  | *: * [1,4: #y ] normalize % #H1 destruct % ]
 qed.
 
 lemma unialpha_unique : 
-  uniqueb DeqUnialpha [bit true;bit false;bar] = true.
+  uniqueb DeqUnialpha [bit true;bit false;null;bar] = true.
 // qed.
 
 lemma unialpha_complete :∀x:DeqUnialpha. 
-  memb ? x [bit true;bit false;bar] = true.
+  memb ? x [bit true;bit false;null;bar] = true.
 * // * //
 qed.
 
 definition FSUnialpha ≝ 
-  mk_FinSet DeqUnialpha [bit true;bit false;bar] 
+  mk_FinSet DeqUnialpha [bit true;bit false;null;bar] 
   unialpha_unique unialpha_complete.
 
+unification hint  0 ≔ ; 
+    X ≟ FSUnialpha
+(* ---------------------------------------- *) ⊢ 
+    unialpha ≡ FinSetcarr X.
+    
 (*************************** testing characters *******************************)
 definition is_bit ≝ λc.match c with [ bit _ ⇒ true | _ ⇒ false ].
-definition is_bar ≝ λc.match c with [ bar ⇒ true | _ ⇒ false ].
\ No newline at end of file
+definition is_bar ≝ λc:DeqUnialpha. c == bar.
+definition is_null ≝ λc:DeqUnialpha. c == null.
+
+definition only_bits ≝ λl.
+  ∀c.mem ? c l → is_bit c = true.
+
+definition no_bars ≝ λl.
+  ∀c.mem ? c l → is_bar c = false.