From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Wed, 4 Apr 2012 07:28:38 +0000 (+0000)
Subject: Added in basics
X-Git-Tag: make_still_working~1820
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=65a3b93b01f2d00960c56df3563b879f36f3cbfd;p=helm.git

Added in basics
- vectors.ma
- finset.ma

Added turing

minor ntegrations in list,ma and listb.ma
---

diff --git a/matita/matita/lib/basics/finset.ma b/matita/matita/lib/basics/finset.ma
new file mode 100644
index 000000000..1b972ec06
--- /dev/null
+++ b/matita/matita/lib/basics/finset.ma
@@ -0,0 +1,70 @@
+(*
+    ||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/lists/listb.ma".
+
+(****** DeqSet: a set with a decidbale equality ******)
+
+record FinSet : Type[1] ≝ 
+{ carr:> DeqSet;
+  enum: list carr;
+  enum_complete: ∀x.memb carr x enum = true;
+  enum_unique: uniqueb carr enum = true
+}.
+
+(*
+definition DeqBool ≝ mk_DeqSet bool beqb beqb_true.
+
+unification hint  0 ≔ ; 
+    X ≟ mk_DeqSet bool beqb beqb_true
+(* ---------------------------------------- *) ⊢ 
+    bool ≡ carr X.
+    
+unification hint  0 ≔ b1,b2:bool; 
+    X ≟ mk_DeqSet bool beqb beqb_true
+(* ---------------------------------------- *) ⊢ 
+    beqb b1 b2 ≡ eqb X b1 b2.
+    
+example exhint: ∀b:bool. (b == false) = true → b = false. 
+#b #H @(\P H).
+qed.
+
+(* pairs *)
+definition eq_pairs ≝
+  λA,B:DeqSet.λp1,p2:A×B.(\fst p1 == \fst p2) ∧ (\snd p1 == \snd p2).
+
+lemma eq_pairs_true: ∀A,B:DeqSet.∀p1,p2:A×B.
+  eq_pairs A B p1 p2 = true ↔ p1 = p2.
+#A #B * #a1 #b1 * #a2 #b2 %
+  [#H cases (andb_true …H) #eqa #eqb >(\P eqa) >(\P eqb) //
+  |#H destruct normalize >(\b (refl … a2)) >(\b (refl … b2)) //
+  ]
+qed.
+
+definition DeqProd ≝ λA,B:DeqSet.
+  mk_DeqSet (A×B) (eq_pairs A B) (eq_pairs_true A B).
+  
+unification hint  0 ≔ C1,C2; 
+    T1 ≟ carr C1,
+    T2 ≟ carr C2,
+    X ≟ DeqProd C1 C2
+(* ---------------------------------------- *) ⊢ 
+    T1×T2 ≡ carr X.
+
+unification hint  0 ≔ T1,T2,p1,p2; 
+    X ≟ DeqProd T1 T2
+(* ---------------------------------------- *) ⊢ 
+    eq_pairs T1 T2 p1 p2 ≡ eqb X p1 p2.
+
+example hint2: ∀b1,b2. 
+  〈b1,true〉==〈false,b2〉=true → 〈b1,true〉=〈false,b2〉.
+#b1 #b2 #H @(\P H).
+*)
\ No newline at end of file
diff --git a/matita/matita/lib/basics/lists/list.ma b/matita/matita/lib/basics/lists/list.ma
index 021e9d400..2ed7fcc86 100644
--- a/matita/matita/lib/basics/lists/list.ma
+++ b/matita/matita/lib/basics/lists/list.ma
@@ -31,12 +31,12 @@ notation "hvbox(l1 break @ l2)"
 interpretation "nil" 'nil = (nil ?).
 interpretation "cons" 'cons hd tl = (cons ? hd tl).
 
-definition not_nil: ∀A:Type[0].list A → Prop ≝
+definition is_nil: ∀A:Type[0].list A → Prop ≝
  λA.λl.match l with [ nil ⇒ True | cons hd tl ⇒ False ].
 
 theorem nil_cons:
   ∀A:Type[0].∀l:list A.∀a:A. a::l ≠ [].
-  #A #l #a @nmk #Heq (change with (not_nil ? (a::l))) >Heq //
+  #A #l #a @nmk #Heq (change with (is_nil ? (a::l))) >Heq //
 qed.
 
 (*
@@ -165,11 +165,19 @@ let rec length (A:Type[0]) (l:list A) on l ≝
 notation "|M|" non associative with precedence 60 for @{'norm $M}.
 interpretation "norm" 'norm l = (length ? l).
 
+lemma length_tail: ∀A,l. length ? (tail A l) = pred (length ? l).
+#A #l elim l // 
+qed.
+
 lemma length_append: ∀A.∀l1,l2:list A. 
   |l1@l2| = |l1|+|l2|.
 #A #l1 elim l1 // normalize /2/
 qed.
 
+lemma length_map: ∀A,B,l.∀f:A→B. length ? (map ?? f l) = length ? l.
+#A #B #l #f elim l // #a #tl #Hind normalize //
+qed.
+
 (****************************** nth ********************************)
 let rec nth n (A:Type[0]) (l:list A) (d:A)  ≝  
   match n with
diff --git a/matita/matita/lib/basics/lists/listb.ma b/matita/matita/lib/basics/lists/listb.ma
index 5abf50f14..b6d5864f8 100644
--- a/matita/matita/lib/basics/lists/listb.ma
+++ b/matita/matita/lib/basics/lists/listb.ma
@@ -16,6 +16,13 @@ include "basics/lists/list.ma".
 include "basics/sets.ma".
 include "basics/deqsets.ma".
 
+(********* isnilb *********)
+let rec isnilb A (l: list A) on l ≝
+match l with
+[ nil ⇒ true
+| cons hd tl ⇒ false
+].
+
 (********* search *********)
 
 let rec memb (S:DeqSet) (x:S) (l: list S) on l  ≝
diff --git a/matita/matita/lib/basics/vectors.ma b/matita/matita/lib/basics/vectors.ma
new file mode 100644
index 000000000..b43014b7b
--- /dev/null
+++ b/matita/matita/lib/basics/vectors.ma
@@ -0,0 +1,60 @@
+(*
+    ||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".
+
+record Vector (A:Type[0]) (n:nat): Type[0] ≝ 
+{ vec :> list A;
+  len: length ? vec = n
+}.
+
+definition vec_tail ≝ λA.λn.λv:Vector A n.
+mk_Vector A (pred n) (tail A v) ?.
+>length_tail >(len A n v) //
+qed.
+
+definition vec_cons ≝ λA.λa.λn.λv:Vector A n.
+mk_Vector A (S n) (cons A a v) ?.
+normalize >(len A n v) //
+qed.
+
+definition vec_append ≝ λA.λn1,n2.λv1:Vector A n1.λv2: Vector A n2.
+mk_Vector A (n1+n2) (v1@v2).
+
+definition vec_map ≝ λA,B.λf:A→B.λn.λv:Vector A n.
+mk_Vector B n (map ?? f v) 
+  (trans_eq … (length_map …) (len A n v)).
+ 
+let rec pmap A B C (f:A→B→C) l1 l2 on l1 ≝
+   match l1 with
+   [ nil ⇒ nil C
+   | cons a tlA ⇒ 
+     match l2 with
+     [nil ⇒ nil C
+     |cons b tlB ⇒ (f a b)::pmap A B C f tlA tlB
+     ]
+   ].
+
+lemma length_pmap: ∀A,B,C.∀f:A→B→C.∀l1,l2.
+length C (pmap  A B C f l1 l2) = 
+  min (length A l1) (length B l2).
+#A #B #C #f #l1 elim l1 // #a #tlA #Hind #l2 cases l2 //
+#b #tlB lapply (Hind tlB) normalize 
+cases (true_or_false (leb (length A tlA) (length B tlB))) #H >H
+normalize //
+qed.
+
+definition pmap_vec ≝ λA,B,C.λf:A→B→C.λn.λvA:Vector A n.λvB:Vector B n.
+mk_Vector C n (pmap A B C f vA vB) ?.
+>length_pmap >(len A n vA) >(len B n vB) normalize 
+>(le_to_leb_true … (le_n n)) //
+qed.
+
diff --git a/matita/matita/lib/re/moves.ma b/matita/matita/lib/re/moves.ma
index 6e4dbb974..1372b4976 100644
--- a/matita/matita/lib/re/moves.ma
+++ b/matita/matita/lib/re/moves.ma
@@ -15,6 +15,19 @@
 include "re/re.ma".
 include "basics/lists/listb.ma".
 
+(* 
+Moves
+
+We now define the move operation, that corresponds to the advancement of the 
+state in response to the processing of an input character a. The intuition is 
+clear: we have to look at points inside $e$ preceding the given character a,
+let the point traverse the character, and broadcast it. All other points must 
+be removed.
+
+We can give a particularly elegant definition in terms of the
+lifted operators of the previous section:
+*)
+
 let rec move (S: DeqSet) (x:S) (E: pitem S) on E : pre S ≝
  match E with
   [ pz ⇒ 〈 `∅, false 〉
@@ -67,10 +80,25 @@ theorem move_ok:
     [>(\P H) % [* // #bot @False_ind //| #H1 destruct /2/]
     |% [@False_ind |#H1 cases (\Pf H) #H2 @H2 destruct //]
     ]
-  |#i1 #i2 #HI1 #HI2 #w >move_cat
-   @iff_trans[|@sem_odot] >same_kernel >sem_cat_w
-   @iff_trans[||@(iff_or_l … (HI2 w))] @iff_or_r 
+  |#i1 #i2 #HI1 #HI2 #w 
+   (* lhs = w∈\sem{move S a (i1·i2)} *)
+   >move_cat
+   (* lhs = w∈\sem{move S a i1}⊙\sem{move S a i2} *)
+   @iff_trans[|@sem_odot] >same_kernel 
+   (* lhs = w∈\sem{move S a i1}·\sem{|i2|} ∨ a∈\sem{move S a i2} *)
+   (* now we work on the rhs, that is
+      rhs = a::w1∈\sem{i1·i2} *)
+   >sem_cat_w
+   (* rhs = a::w1∈\sem{i1}\sem{|i2|} ∨ a::w∈\sem{i2} *)
+   @iff_trans[||@(iff_or_l … (HI2 w))] 
+   (* rhs = a::w1∈\sem{i1}\sem{|i2|} ∨ w∈\sem{move S a i2} *)
+   @iff_or_r 
+   check deriv_middot 
+   (* we are left to prove that 
+     w∈\sem{move S a i1}·\sem{|i2|} ↔ a::w∈\sem{i1}\sem{|i2|}
+     we use deriv_middot on the rhs *)
    @iff_trans[||@iff_sym @deriv_middot //]
+   (* w∈\sem{move S a i1}·\sem{|i2|} ↔ w∈(deriv S \sem{i1} a) · \sem{|i2|} *)
    @cat_ext_l @HI1
   |#i1 #i2 #HI1 #HI2 #w >(sem_plus S i1 i2) >move_plus >sem_plus_w 
    @iff_trans[|@sem_oplus] 
@@ -117,15 +145,12 @@ theorem decidable_sem: ∀S:DeqSet.∀w: word S. ∀e:pre S.
 #S #w elim w 
  [* #i #b >moves_empty cases b % /2/
  |#a #w1 #Hind #e >moves_cons
+ check not_epsilon_sem
   @iff_trans [||@iff_sym @not_epsilon_sem]
   @iff_trans [||@move_ok] @Hind
  ]
 qed.
 
-(* lemma not_true_to_false: ∀b.b≠true → b =false.
-#b * cases b // #H @False_ind /2/ 
-qed. *)
-
 (************************ pit state ***************************)
 definition pit_pre ≝ λS.λi.〈blank S (|i|), false〉. 
 
@@ -180,7 +205,11 @@ qed.
 (* bisimulation *)
 definition cofinal ≝ λS.λp:(pre S)×(pre S). 
   \snd (\fst p) = \snd (\snd p).
-  
+
+(* As a corollary of decidable_sem, we have that two expressions
+e1 and e2 are equivalent iff for any word w the states reachable 
+through w are cofinal. *)
+
 theorem equiv_sem: ∀S:DeqSet.∀e1,e2:pre S. 
   \sem{e1} =1 \sem{e2} ↔ ∀w.cofinal ? 〈moves ? w e1,moves ? w e2〉.
 #S #e1 #e2 % 
@@ -192,6 +221,11 @@ theorem equiv_sem: ∀S:DeqSet.∀e1,e2:pre S.
 |#H #w1 @iff_trans [||@decidable_sem] <H @iff_sym @decidable_sem]
 qed.
 
+(* This does not directly imply decidability: we have no bound over the
+length of w; moreover, so far, we made no assumption over the cardinality 
+of S. Instead of requiring S to be finite, we may restrict the analysis
+to characters occurring in the given pres. *)
+
 definition occ ≝ λS.λe1,e2:pre S. 
   unique_append ? (occur S (|\fst e1|)) (occur S (|\fst e2|)).
 
@@ -205,12 +239,23 @@ cases (decidable_sublist S w (occ S e1 e2)) [@H] -H #H
  //
 qed.
 
+(* The following is a stronger version of equiv_sem, relative to characters
+occurring the given regular expressions. *)
+
 lemma equiv_sem_occ: ∀S.∀e1,e2:pre S.
 (∀w.(sublist S w (occ S e1 e2))→ cofinal ? 〈moves ? w e1,moves ? w e2〉)
 → \sem{e1}=1\sem{e2}.
 #S #e1 #e2 #H @(proj2 … (equiv_sem …)) @occ_enough #w @H 
 qed.
 
+(* 
+We say that a list of pairs of pres is a bisimulation if it is closed
+w.r.t. moves, and all its members are cofinal.
+*)
+
+(* the sons of p w.r.t a list of symbols l are all states reachable from p 
+with a move in l *)
+
 definition sons ≝ λS:DeqSet.λl:list S.λp:(pre S)×(pre S). 
  map ?? (λa.〈move S a (\fst (\fst p)),move S a (\fst (\snd p))〉) l.
 
@@ -225,6 +270,8 @@ qed.
 definition is_bisim ≝ λS:DeqSet.λl:list ?.λalpha:list S.
   ∀p:(pre S)×(pre S). memb ? p l = true → cofinal ? p ∧ (sublist ? (sons ? alpha p) l).
 
+(* Using lemma equiv_sem_occ it is easy to prove the following result: *)
+
 lemma bisim_to_sem: ∀S:DeqSet.∀l:list ?.∀e1,e2: pre S. 
   is_bisim S l (occ S e1 e2) → memb ? 〈e1,e2〉 l = true → \sem{e1}=1\sem{e2}.
 #S #l #e1 #e2 #Hbisim #Hmemb @equiv_sem_occ 
@@ -237,7 +284,31 @@ lapply Hsub @(list_elim_left … w) [//]
   ]
 qed.
 
-(* the algorithm *)
+(* This is already an interesting result: checking if l is a bisimulation 
+is decidable, hence we could generate l with some untrusted piece of code 
+and then run a (boolean version of) is_bisim to check that it is actually 
+a bisimulation. 
+However, in order to prove that equivalence of regular expressions
+is decidable we must prove that we can always effectively build such a list 
+(or find a counterexample).
+The idea is that the list we are interested in is just the set of 
+all pair of pres reachable from the initial pair via some
+sequence of moves. 
+
+The algorithm for computing reachable nodes in graph is a very 
+traditional one. We split nodes in two disjoint lists: a list of 
+visited nodes and a frontier, composed by all nodes connected
+to a node in visited but not visited already. At each step we select a node 
+a from the frontier, compute its sons, add a to the set of 
+visited nodes and the (not already visited) sons to the frontier. 
+
+Instead of fist computing reachable nodes and then performing the 
+bisimilarity test we can directly integrate it in the algorithm:
+the set of visited nodes is closed by construction w.r.t. reachability,
+so we have just to check cofinality for any node we add to visited.
+
+Here is the extremely simple algorithm: *)
+
 let rec bisim S l n (frontier,visited: list ?) on n ≝
   match n with 
   [ O ⇒ 〈false,visited〉 (* assert false *)
@@ -267,7 +338,15 @@ lemma unfold_bisim: ∀S,l,n.∀frontier,visited: list ?.
     ]
   ].
 #S #l #n cases n // qed.
-  
+
+(* The integer n is an upper bound to the number of recursive call, 
+equal to the dimension of the graph. It returns a pair composed
+by a boolean and a the set of visited nodes; the boolean is true
+if and only if all visited nodes are cofinal. 
+
+The following results explicitly state the behaviour of bisim is the general
+case and in some relevant instances *)
+ 
 lemma bisim_never: ∀S,l.∀frontier,visited: list ?.
   bisim S l O frontier visited = 〈false,visited〉.
 #frontier #visited >unfold_bisim // 
@@ -296,6 +375,9 @@ lemma notb_eq_true_l: ∀b. notb b = true → b = false.
 #b cases b normalize //
 qed.
 
+(* In order to prove termination of bisim we must be able to effectively 
+enumerate all possible pres: *)
+
 let rec pitem_enum S (i:re S) on i ≝
   match i with
   [ z ⇒ [pz S]
@@ -333,6 +415,11 @@ lemma space_enum_complete : ∀S.∀e1,e2: pre S.
 #S #e1 #e2 @(memb_compose … (λi,b.〈i,b〉))
 // qed.
 
+(* We are ready to prove that bisim is correct; we use the invariant 
+that at each call of bisim the two lists visited and frontier only contain 
+nodes reachable from \langle e_1,e_2\rangle, hence it is absurd to suppose 
+to meet a pair which is not cofinal. *)
+
 definition all_reachable ≝ λS.λe1,e2:pre S.λl: list ?.
 uniqueb ? l = true ∧ 
   ∀p. memb ? p l = true → 
@@ -391,6 +478,10 @@ definition all_true ≝ λS.λl.∀p:(pre S) × (pre S). memb ? p l = true →
 definition sub_sons ≝ λS,l,l1,l2.∀x:(pre S) × (pre S). 
 memb ? x l1 = true → sublist ? (sons ? l x) l2. 
 
+(* For completeness, we use the invariant that all the nodes in visited are cofinal, 
+and the sons of visited are either in visited or in the frontier; since
+at the end frontier is empty, visited is hence a bisimulation. *)
+
 lemma bisim_complete: 
  ∀S,l,n.∀frontier,visited,visited_res:list ?.
  all_true S visited →
@@ -488,6 +579,25 @@ definition exp1 ≝ ((a·b)^*·a).
 definition exp2 ≝ a·(b·a)^*.
 definition exp4 ≝ (b·a)^*.
 
+definition exp5 ≝ (a·(a·(a·b)^*·b)^*·b)^*.
+
+example 
+  moves1: \snd (moves DeqNat [0;1;0] (•(blank ? exp2))) = true.
+normalize // 
+qed.
+
+example 
+  moves2: \snd (moves DeqNat [0;1;0;0;0] (•(blank ? exp2))) = false.
+normalize // qed.
+
+example 
+  moves3: \snd (moves DeqNat [0;0;0;1;0;1;1;0;1;1] (•(blank ? exp5))) = true.
+normalize // qed.
+
+example 
+  moves4: \snd (moves DeqNat [0;0;0;1;0;1;1;0;1;1;1;0] (•(blank ? exp5))) = false.
+normalize // qed.
+
 definition exp6 ≝ a·(a ·a ·b^* + b^* ).
 definition exp7 ≝ a · a^* · b^*.
 
@@ -506,3 +616,4 @@ normalize // qed.
 
 
 
+\v
\ No newline at end of file
diff --git a/matita/matita/lib/re/re.ma b/matita/matita/lib/re/re.ma
index 5894af561..9b6378846 100644
--- a/matita/matita/lib/re/re.ma
+++ b/matita/matita/lib/re/re.ma
@@ -14,6 +14,9 @@
 
 include "re/lang.ma".
 
+(* The type re of regular expressions over an alphabet $S$ is the smallest 
+collection of objects generated by the following constructors: *)
+
 inductive re (S: DeqSet) : Type[0] ≝
    z: re S
  | e: re S
@@ -34,6 +37,9 @@ interpretation "atom" 'ps a = (s ? a).
 notation "`∅" non associative with precedence 90 for @{ 'empty }.
 interpretation "empty" 'empty = (z ?).
 
+(* The language sem{e} associated with the regular expression e is inductively 
+defined by the following function: *)
+
 let rec in_l (S : DeqSet) (r : re S) on r : word S → Prop ≝ 
 match r with
 [ z ⇒ ∅
@@ -50,8 +56,37 @@ interpretation "in_l mem" 'mem w l = (in_l ? l w).
 lemma rsem_star : ∀S.∀r: re S. \sem{r^*} = \sem{r}^*.
 // qed.
 
+(* 
+Pointed Regular expressions
+
+We now introduce pointed regular expressions, that are the main tool we shall 
+use for the construction of the automaton. 
+A pointed regular expression is just a regular expression internally labelled 
+with some additional points. Intuitively, points mark the positions inside the 
+regular expression which have been reached after reading some prefix of
+the input string, or better the positions where the processing of the remaining 
+string has to be started. Each pointed expression for $e$ represents a state of 
+the {\em deterministic} automaton associated with $e$; since we obviously have 
+only a finite number of possible labellings, the number of states of the automaton 
+is finite.
+
+Pointed regular expressions provide the tool for an algebraic revisitation of 
+McNaughton and Yamada's algorithm for position automata, making the proof of its 
+correctness, that is far from trivial, particularly clear and simple. In particular, 
+pointed expressions offer an appealing alternative to Brzozowski's derivatives, 
+avoiding their weakest point, namely the fact of being forced to quotient derivatives 
+w.r.t. a suitable notion of equivalence in order to get a finite number of states 
+(that is not essential for recognizing strings, but is crucial for comparing regular 
+expressions). 
+
+Our main data structure is the notion of pointed item, that is meant whose purpose
+is to encode a set of positions inside a regular expression. 
+The idea of formalizing pointers inside a data type by means of a labelled version 
+of the data type itself is probably one of the first, major lessons learned in the 
+formalization of the metatheory of programming languages. For our purposes, it is 
+enough to mark positions preceding individual characters, so we shall have two kinds 
+of characters •a (pp a) and a (ps a) according to the case a is pointed or not. *)
 
-(* pointed items *)
 inductive pitem (S: DeqSet) : Type[0] ≝
    pz: pitem S
  | pe: pitem S
@@ -61,6 +96,12 @@ inductive pitem (S: DeqSet) : Type[0] ≝
  | po: pitem S → pitem S → pitem S
  | pk: pitem S → pitem S.
  
+(* A pointed regular expression (pre) is just a pointed item with an additional 
+boolean, that must be understood as the possibility to have a trailing point at 
+the end of the expression. As we shall see, pointed regular expressions can be 
+understood as states of a DFA, and the boolean indicates if
+the state is final or not. *)
+
 definition pre ≝ λS.pitem S × bool.
 
 interpretation "pitem star" 'star a = (pk ? a).
@@ -73,6 +114,10 @@ interpretation "pitem ps" 'ps a = (ps ? a).
 interpretation "pitem epsilon" 'epsilon = (pe ?).
 interpretation "pitem empty" 'empty = (pz ?).
 
+(* The carrier $|i|$ of an item i is the regular expression obtained from i by 
+removing all the points. Similarly, the carrier of a pointed regular expression 
+is the carrier of its item. *)
+
 let rec forget (S: DeqSet) (l : pitem S) on l: re S ≝
  match l with
   [ pz ⇒ `∅
@@ -96,7 +141,14 @@ lemma erase_plus : ∀S.∀i1,i2:pitem S.
 lemma erase_star : ∀S.∀i:pitem S.|i^*| = |i|^*. 
 // qed.
 
-(* boolean equality *)
+(* 
+Comparing items and pres
+
+Items and pres are very concrete datatypes: they can be effectively compared, 
+and enumerated. In particular, we can define a boolean equality beqitem and a proof
+beqitem_true that it refects propositional equality, enriching the set (pitem S)
+to a DeqSet. *)
+
 let rec beqitem S (i1,i2: pitem S) on i1 ≝ 
   match i1 with
   [ pz ⇒ match i2 with [ pz ⇒ true | _ ⇒ false]
@@ -144,7 +196,11 @@ qed.
 
 definition DeqItem ≝ λS.
   mk_DeqSet (pitem S) (beqitem S) (beqitem_true S).
-  
+
+(* We also add a couple of unification hints to allow the type inference system 
+to look at (pitem S) as the carrier of a DeqSet, and at beqitem as if it was the 
+equality function of a DeqSet. *)
+
 unification hint  0 ≔ S; 
     X ≟ mk_DeqSet (pitem S) (beqitem S) (beqitem_true S)
 (* ---------------------------------------- *) ⊢ 
@@ -155,7 +211,12 @@ unification hint  0 ≔ S,i1,i2;
 (* ---------------------------------------- *) ⊢ 
     beqitem S i1 i2 ≡ eqb X i1 i2.
 
-(* semantics *)
+(*
+Semantics of pointed regular expressions
+
+The intuitive semantic of a point is to mark the position where
+we should start reading the regular expression. The language associated
+to a pre is the union of the languages associated with its points. *)
 
 let rec in_pl (S : DeqSet) (r : pitem S) on r : word S → Prop ≝ 
 match r with
@@ -176,6 +237,8 @@ definition in_prl ≝ λS : DeqSet.λp:pre S.
 interpretation "in_prl mem" 'mem w l = (in_prl ? l w).
 interpretation "in_prl" 'in_l E = (in_prl ? E).
 
+(* The following, trivial lemmas are only meant for rewriting purposes. *)
+
 lemma sem_pre_true : ∀S.∀i:pitem S. 
   \sem{〈i,true〉} = \sem{i} ∪ {ϵ}. 
 // qed.
@@ -208,6 +271,14 @@ lemma sem_star_w : ∀S.∀i:pitem S.∀w.
   \sem{i^*} w = (∃w1,w2.w1 @ w2 = w ∧ \sem{i} w1 ∧ \sem{|i|}^* w2).
 // qed.
 
+(* Below are a few, simple, semantic properties of items. In particular:
+- not_epsilon_item : ∀S:DeqSet.∀i:pitem S. ¬ (\sem{i} ϵ).
+- epsilon_pre : ∀S.∀e:pre S. (\sem{i} ϵ) ↔ (\snd e = true).
+- minus_eps_item: ∀S.∀i:pitem S. \sem{i} =1 \sem{i}-{[ ]}.
+- minus_eps_pre: ∀S.∀e:pre S. \sem{\fst e} =1 \sem{e}-{[ ]}.
+The first property is proved by a simple induction on $i$; the other
+results are easy corollaries. We need an auxiliary lemma first. *)
+
 lemma append_eq_nil : ∀S.∀w1,w2:word S. w1 @ w2 = ϵ → w1 = ϵ.
 #S #w1 #w2 cases w1 // #a #tl normalize #H destruct qed.
 
@@ -220,7 +291,6 @@ lemma not_epsilon_lp : ∀S:DeqSet.∀e:pitem S. ¬ (ϵ ∈ e).
   ]
 qed.
 
-(* lemma 12 *)
 lemma epsilon_to_true : ∀S.∀e:pre S. ϵ ∈ e → \snd e = true.
 #S * #i #b cases b // normalize #H @False_ind /2/ 
 qed.
@@ -244,6 +314,33 @@ lemma minus_eps_pre: ∀S.∀e:pre S. \sem{\fst e} =1 \sem{e}-{[ ]}.
   ]
 qed.
 
+(*
+Broadcasting points
+
+Intuitively, a regular expression e must be understood as a pointed expression with a single 
+point in front of it. Since however we only allow points before symbols, we must broadcast 
+this initial point inside e traversing all nullable subexpressions, that essentially corresponds 
+to the ϵ-closure operation on automata. We use the notation •(_) to denote such an operation;
+its definition is the expected one: let us start discussing an example.
+
+Example
+Let us broadcast a point inside (a + ϵ)(b*a + b)b. We start working in parallel on the 
+first occurrence of a (where the point stops), and on ϵ that gets traversed. We have hence 
+reached the end of a + ϵ and we must pursue broadcasting inside (b*a + b)b. Again, we work in 
+parallel on the two additive subterms b^*a and b; the first point is allowed to both enter the 
+star, and to traverse it, stopping in front of a; the second point just stops in front of b. 
+No point reached that end of b^*a + b hence no further propagation is possible. In conclusion: 
+               •((a + ϵ)(b^*a + b)b) = 〈(•a + ϵ)((•b)^*•a + •b)b, false〉
+*)
+
+(* Broadcasting a point inside an item generates a pre, since the point could possibly reach 
+the end of the expression. 
+Broadcasting inside a i1+i2 amounts to broadcast in parallel inside i1 and i2.
+If we define
+                 〈i1,b1〉 ⊕ 〈i2,b2〉 = 〈i1 + i2, b1 ∨ b2〉
+then, we just have •(i1+i2) = •(i1)⊕ •(i2).
+*)
+
 definition lo ≝ λS:DeqSet.λa,b:pre S.〈\fst a + \fst b,\snd a ∨ \snd b〉.
 notation "a ⊕ b" left associative with precedence 60 for @{'oplus $a $b}.
 interpretation "oplus" 'oplus a b = (lo ? a b).
@@ -251,12 +348,31 @@ interpretation "oplus" 'oplus a b = (lo ? a b).
 lemma lo_def: ∀S.∀i1,i2:pitem S.∀b1,b2. 〈i1,b1〉⊕〈i2,b2〉=〈i1+i2,b1∨b2〉.
 // qed.
 
+(*
+Concatenation is a bit more complex. In order to broadcast a point inside i1 · i2 
+we should start broadcasting it inside i1 and then proceed into i2 if and only if a 
+point reached the end of i1. This suggests to define •(i1 · i2) as •(i1) ▹ i2, where 
+e ▹ i is a general operation of concatenation between a pre and an item, defined by 
+cases on the boolean in e: 
+
+       〈i1,true〉 ▹ i2  = i1 ◃ •(i_2)
+       〈i1,false〉 ▹ i2 = i1 · i2
+       
+In turn, ◃ says how to concatenate an item with a pre, that is however extremely simple:
+
+        i1 ◃ 〈i1,b〉  = 〈i_1 · i2, b〉
+
+Let us come to the formalized definitions:
+*)
+
 definition pre_concat_r ≝ λS:DeqSet.λi:pitem S.λe:pre S.
   match e with [ mk_Prod i1 b ⇒ 〈i · i1, b〉].
  
 notation "i ◃ e" left associative with precedence 60 for @{'lhd $i $e}.
 interpretation "pre_concat_r" 'lhd i e = (pre_concat_r ? i e).
 
+(* The behaviour of ◃ is summarized by the following, easy lemma: *)
+
 lemma eq_to_ex_eq: ∀S.∀A,B:word S → Prop. 
   A = B → A =1 B. 
 #S #A #B #H >H /2/ qed.
@@ -266,7 +382,13 @@ lemma sem_pre_concat_r : ∀S,i.∀e:pre S.
 #S #i * #i1 #b1 cases b1 [2: @eq_to_ex_eq //] 
 >sem_pre_true >sem_cat >sem_pre_true /2/ 
 qed.
- 
+
+(* The definition of $•(-)$ (eclose) and ▹ (pre_concat_l) are mutually recursive.
+In this situation, a viable alternative that is usually simpler to reason about, 
+is to abstract one of the two functions with respect to the other. In particular
+we abstract pre_concat_l with respect to an input bcast function from items to
+pres. *)
+
 definition pre_concat_l ≝ λS:DeqSet.λbcast:∀S:DeqSet.pitem S → pre S.λe1:pre S.λi2:pitem S.
   match e1 with 
   [ mk_Prod i1 b1 ⇒ match b1 with 
@@ -280,6 +402,8 @@ interpretation "item-pre concat" 'tril op a b = (pre_concat_l ? op a b).
 
 notation "•" non associative with precedence 60 for @{eclose ?}.
 
+(* We are ready to give the formal definition of the broadcasting operation. *)
+
 let rec eclose (S: DeqSet) (i: pitem S) on i : pre S ≝
  match i with
   [ pz ⇒ 〈 `∅, false 〉
@@ -293,6 +417,8 @@ let rec eclose (S: DeqSet) (i: pitem S) on i : pre S ≝
 notation "• x" non associative with precedence 60 for @{'eclose $x}.
 interpretation "eclose" 'eclose x = (eclose ? x).
 
+(* Here are a few simple properties of ▹ and •(-) *)
+
 lemma eclose_plus: ∀S:DeqSet.∀i1,i2:pitem S.
   •(i1 + i2) = •i1 ⊕ •i2.
 // qed.
@@ -305,22 +431,6 @@ lemma eclose_star: ∀S:DeqSet.∀i:pitem S.
   •i^* = 〈(\fst(•i))^*,true〉.
 // qed.
 
-definition lift ≝ λS.λf:pitem S →pre S.λe:pre S. 
-  match e with 
-  [ mk_Prod i b ⇒ 〈\fst (f i), \snd (f i) ∨ b〉].
-  
-definition preclose ≝ λS. lift S (eclose S). 
-interpretation "preclose" 'eclose x = (preclose ? x).
-
-(* theorem 16: 2 *)
-lemma sem_oplus: ∀S:DeqSet.∀e1,e2:pre S.
-  \sem{e1 ⊕ e2} =1 \sem{e1} ∪ \sem{e2}. 
-#S * #i1 #b1 * #i2 #b2 #w %
-  [cases b1 cases b2 normalize /2/ * /3/ * /3/
-  |cases b1 cases b2 normalize /2/ * /3/ * /3/
-  ]
-qed.
-
 lemma odot_true : 
   ∀S.∀i1,i2:pitem S.
   〈i1,true〉 ▹ i2 = i1 ◃ (•i2).
@@ -336,9 +446,18 @@ lemma odot_false:
   〈i1,false〉 ▹ i2 = 〈i1 · i2, false〉.
 // qed.
 
-lemma LcatE : ∀S.∀e1,e2:pitem S.
-  \sem{e1 · e2} = \sem{e1} · \sem{|e2|} ∪ \sem{e2}. 
-// qed.
+(* The definition of •(-) (eclose) can then be lifted from items to pres
+in the obvious way. *)
+
+definition lift ≝ λS.λf:pitem S →pre S.λe:pre S. 
+  match e with 
+  [ mk_Prod i b ⇒ 〈\fst (f i), \snd (f i) ∨ b〉].
+  
+definition preclose ≝ λS. lift S (eclose S). 
+interpretation "preclose" 'eclose x = (preclose ? x).
+
+(* Obviously, broadcasting does not change the carrier of the item,
+as it is easily proved by structural induction. *)
 
 lemma erase_bull : ∀S.∀i:pitem S. |\fst (•i)| = |i|.
 #S #i elim i // 
@@ -350,13 +469,36 @@ lemma erase_bull : ∀S.∀i:pitem S. |\fst (•i)| = |i|.
   ]
 qed.
 
-(*
-lemma sem_eclose_star: ∀S:DeqSet.∀i:pitem S.
-  \sem{〈i^*,true〉} =1 \sem{〈i,false〉}·\sem{|i|}^* ∪ {ϵ}.
-/2/ qed.
-*)
+(* We are now ready to state the main semantic properties of ⊕, ◃ and •(-):
+
+sem_oplus:     \sem{e1 ⊕ e2} =1 \sem{e1} ∪ \sem{e2} 
+sem_pcl:       \sem{e1 ▹ i2} =1  \sem{e1} · \sem{|i2|} ∪ \sem{i2}
+sem_bullet     \sem{•i} =1 \sem{i} ∪ \sem{|i|}
+
+The proof of sem_oplus is straightforward. *)
+
+lemma sem_oplus: ∀S:DeqSet.∀e1,e2:pre S.
+  \sem{e1 ⊕ e2} =1 \sem{e1} ∪ \sem{e2}. 
+#S * #i1 #b1 * #i2 #b2 #w %
+  [cases b1 cases b2 normalize /2/ * /3/ * /3/
+  |cases b1 cases b2 normalize /2/ * /3/ * /3/
+  ]
+qed.
+
+(* For the others, we proceed as follow: we first prove the following 
+auxiliary lemma, that assumes sem_bullet:
+
+sem_pcl_aux: 
+   \sem{•i2} =1  \sem{i2} ∪ \sem{|i2|} →
+   \sem{e1 ▹ i2} =1  \sem{e1} · \sem{|i2|} ∪ \sem{i2}.
+
+Then, using the previous result, we prove sem_bullet by induction 
+on i. Finally, sem_pcl_aux and sem_bullet give sem_pcl. *)
+
+lemma LcatE : ∀S.∀e1,e2:pitem S.
+  \sem{e1 · e2} = \sem{e1} · \sem{|e2|} ∪ \sem{e2}. 
+// qed.
 
-(* theorem 16: 1 → 3 *)
 lemma odot_dot_aux : ∀S.∀e1:pre S.∀i2:pitem S.
    \sem{•i2} =1  \sem{i2} ∪ \sem{|i2|} →
    \sem{e1 ▹ i2} =1  \sem{e1} · \sem{|i2|} ∪ \sem{i2}.
@@ -378,21 +520,31 @@ lemma minus_eps_pre_aux: ∀S.∀e:pre S.∀i:pitem S.∀A.
 @eqP_substract_r //
 qed.
 
-(* theorem 16: 1 *)
 theorem sem_bull: ∀S:DeqSet. ∀i:pitem S.  \sem{•i} =1 \sem{i} ∪ \sem{|i|}.
 #S #e elim e 
   [#w normalize % [/2/ | * //]
   |/2/ 
   |#x normalize #w % [ /2/ | * [@False_ind | //]]
   |#x normalize #w % [ /2/ | * // ] 
-  |#i1 #i2 #IH1 #IH2 >eclose_dot
-   @eqP_trans [|@odot_dot_aux //] >sem_cat 
+  |#i1 #i2 #IH1 #IH2 
+   (* lhs = \sem{•(i1 ·i2)} *)
+   >eclose_dot
+   (* lhs =\sem{•(i1) ▹ i2)} *) 
+   @eqP_trans [|@odot_dot_aux //] 
+   (* lhs = \sem{•(i1)·\sem{|i2|}∪\sem{i2} *)
    @eqP_trans
      [|@eqP_union_r
        [|@eqP_trans [|@(cat_ext_l … IH1)] @distr_cat_r]]
+   (* lhs = \sem{i1}·\sem{|i2|}∪\sem{|i1|}·\sem{|i2|}∪\sem{i2} *) 
    @eqP_trans [|@union_assoc]
+   (* lhs = \sem{i1}·\sem{|i2|}∪(\sem{|i1|}·\sem{|i2|}∪\sem{i2}) *) 
+   (* Now we work on the rhs that is 
+      rhs = \sem{i1·i2} ∪ \sem{|i1·i2|} *)
+   >sem_cat 
+   (* rhs = \sem{i1}·\sem{|i2|} ∪ \sem{i2} ∪ \sem{|i1·i2|} *)
    @eqP_trans [||@eqP_sym @union_assoc]
-   @eqP_union_l //
+   (* rhs = \sem{i1}·\sem{|i2|}∪ (\sem{i2} ∪ \sem{|i1·i2|}) *)
+   @eqP_union_l @union_comm 
   |#i1 #i2 #IH1 #IH2 >eclose_plus
    @eqP_trans [|@sem_oplus] >sem_plus >erase_plus 
    @eqP_trans [|@(eqP_union_l … IH2)]
@@ -409,7 +561,15 @@ theorem sem_bull: ∀S:DeqSet. ∀i:pitem S.  \sem{•i} =1 \sem{i} ∪ \sem{|i|
   ]
 qed.
 
-(* blank item *)
+(*
+Blank item
+ 
+As a corollary of theorem sem_bullet, given a regular expression e, we can easily 
+find an item with the same semantics of $e$: it is enough to get an item (blank e) 
+having e as carrier and no point, and then broadcast a point in it. The semantics of
+(blank e) is obviously the empty language: from the point of view of the automaton,
+it corresponds with the pit state. *)
+
 let rec blank (S: DeqSet) (i: re S) on i :pitem S ≝
  match i with
   [ z ⇒ `∅
@@ -446,7 +606,12 @@ theorem re_embedding: ∀S.∀e:re S.
 @eqP_trans [|@union_comm] @union_empty_r.
 qed.
 
-(* lefted operations *)
+(*
+Lifted Operators
+ 
+Plus and bullet have been already lifted from items to pres. We can now 
+do a similar job for concatenation ⊙ and Kleene's star ⊛. *)
+
 definition lifted_cat ≝ λS:DeqSet.λe:pre S. 
   lift S (pre_concat_l S eclose e).
 
@@ -469,6 +634,8 @@ lemma erase_odot:∀S.∀e1,e2:pre S.
 #S * #i1 * * #i2 #b2 // >odot_true_b // 
 qed.
 
+(* Let us come to the star operation: *)
+
 definition lk ≝ λS:DeqSet.λe:pre S.
   match e with 
   [ mk_Prod i1 b1 ⇒
@@ -513,6 +680,9 @@ cut (e1 ⊙ 〈i,false〉 = 〈\fst (e1 ▹ i), \snd(e1 ▹ i) ∨ false〉) [//
 cases (e1 ▹ i) #i1 #b1 cases b1 #H @H
 qed.
 
+(* We conclude this section with the proof of the main semantic properties
+of ⊙ and ⊛. *)
+
 lemma sem_odot: 
   ∀S.∀e1,e2: pre S. \sem{e1 ⊙ e2} =1 \sem{e1}· \sem{|\fst e2|} ∪ \sem{e2}.
 #S #e1 * #i2 * 
@@ -522,17 +692,28 @@ lemma sem_odot:
   |>sem_pre_false >eq_odot_false @odot_dot_aux //
   ]
 qed.
-
-(* theorem 16: 4 *)      
+      
 theorem sem_ostar: ∀S.∀e:pre S. 
   \sem{e^⊛} =1  \sem{e} · \sem{|\fst e|}^*.
 #S * #i #b cases b
-  [>sem_pre_true >sem_pre_true >sem_star >erase_bull
+  [(* lhs = \sem{〈i,true〉^⊛} *)
+   >sem_pre_true (* >sem_pre_true *) 
+   (* lhs = \sem{(\fst (•i))^*}∪{ϵ} *)
+   >sem_star >erase_bull
+   (* lhs = \sem{\fst (•i)}·(\sem{|i|)^*∪{ϵ} *)
    @eqP_trans [|@eqP_union_r[|@cat_ext_l [|@minus_eps_pre_aux //]]]
+   (* lhs = (\sem{i}∪(\sem{|i|}-{ϵ})·(\sem{|i|)^*∪{ϵ} *)
    @eqP_trans [|@eqP_union_r [|@distr_cat_r]]
+   (* lhs = (\sem{i}·(\sem{|i|)^*∪(\sem{|i|}-{ϵ})·(\sem{|i|)^*∪{ϵ} *)
+   @eqP_trans [|@union_assoc]
+   (* lhs = (\sem{i}·(\sem{|i|)^*∪((\sem{|i|}-{ϵ})·(\sem{|i|)^*∪{ϵ}) *)
+   @eqP_trans [|@eqP_union_l[|@eqP_sym @star_fix_eps]]
+   (* lhs = (\sem{i}·(\sem{|i|)^*∪(\sem{|i|)^* *)
+   (* now we work on the right hand side, that is
+      rhs = \sem{〈i,true〉}·(\sem{|i|}^* *)
    @eqP_trans [||@eqP_sym @distr_cat_r]
-   @eqP_trans [|@union_assoc] @eqP_union_l
-   @eqP_trans [||@eqP_sym @epsilon_cat_l] @eqP_sym @star_fix_eps 
+   (* rhs = (\sem{i}·(\sem{|i|)^*∪{ϵ}·(\sem{|i|)^* *)
+   @eqP_union_l @eqP_sym @epsilon_cat_l
   |>sem_pre_false >sem_pre_false >sem_star /2/
   ]
 qed.
diff --git a/matita/matita/lib/turing/ntm.ma b/matita/matita/lib/turing/ntm.ma
new file mode 100644
index 000000000..603a0a0da
--- /dev/null
+++ b/matita/matita/lib/turing/ntm.ma
@@ -0,0 +1,150 @@
+(*
+    ||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/star.ma".
+include "turing/turing.ma".
+
+(*
+record Vector (A:Type[0]) (n:nat): Type[0] ≝ 
+{ vec :> list A;
+  len: length ? vec = n
+}.
+
+record tape (sig:FinSet): Type[0] ≝ 
+{ left : list sig;
+  right: list sig
+}.
+
+inductive move : Type[0] ≝
+| L : move 
+| R : move
+| N : move
+. 
+*)
+
+record NTM (sig:FinSet): Type[1] ≝ 
+{ states : FinSet;
+  tapes_no: nat; (* additional working tapes *)
+  trans : list ((states × (Vector (option sig) (S tapes_no))) ×
+    (states  × (Vector (sig × move) (S tapes_no))));
+  output: list sig;
+  start: states;
+  halt : states → bool;
+  accept : states → bool
+}.
+
+record config (sig:FinSet) (M:NTM sig): Type[0] ≝
+{ state : states sig M;
+  tapes : Vector (tape sig) (S (tapes_no sig M))
+}.
+
+(*
+definition option_hd ≝ λA.λl:list A.
+  match l with
+  [nil ⇒ None ?
+  |cons a _ ⇒ Some ? a
+  ].
+
+lemma length_tail: ∀A,l. length ? (tail A l) = pred (length ? l).
+#A #l elim l // 
+qed.
+
+definition vec_tail ≝ λA.λn.λv:Vector A n.
+mk_Vector A (pred n) (tail A v) ?.
+>length_tail >(len A n v) //
+qed.
+
+definition vec_cons ≝ λA.λa.λn.λv:Vector A n.
+mk_Vector A (S n) (cons A a v) ?.
+normalize >(len A n v) //
+qed.
+
+lemma length_map: ∀A,B,l.∀f:A→B. length ? (map ?? f l) = length ? l.
+#A #B #l #f elim l // #a #tl #Hind normalize //
+qed.
+
+definition vec_map ≝ λA,B.λf:A→B.λn.λv:Vector A n.
+mk_Vector B n (map ?? f v) 
+  (trans_eq … (length_map …) (len A n v)). 
+  
+definition tape_move ≝ λsig.λt: tape sig.λm:sig × move.
+  match \snd m with
+  [ R ⇒ mk_tape sig ((\fst m)::(left ? t)) (tail ? (right ? t))
+  | L ⇒ mk_tape sig (tail ? (left ? t)) ((\fst m)::(right ? t))
+  ].
+*)
+
+(*  
+definition hds ≝ λsig.λM.λc:config sig M. vec_map ?? (option_hd ?) (tapes_no sig M) (\snd c).
+
+definition tls ≝ λsig.λM.λc:config sig M.vec_map ?? (tail ?) (tapes_no sig M) (\snd c).
+*)
+(*
+let rec compose A B C (f:A→B→C) l1 l2 on l1 ≝
+   match l1 with
+   [ nil ⇒ nil C
+   | cons a tlA ⇒ 
+     match l2 with
+     [nil ⇒ nil C
+     |cons b tlB ⇒ (f a b)::compose A B C f tlA tlB
+     ]
+   ].
+
+lemma length_compose: ∀A,B,C.∀f:A→B→C.∀l1,l2.
+length C (compose  A B C f l1 l2) = 
+  min (length A l1) (length B l2).
+#A #B #C #f #l1 elim l1 // #a #tlA #Hind #l2 cases l2 //
+#b #tlB lapply (Hind tlB) normalize 
+cases (true_or_false (leb (length A tlA) (length B tlB))) #H >H
+normalize //
+qed.
+
+definition compose_vec ≝ λA,B,C.λf:A→B→C.λn.λvA:Vector A n.λvB:Vector B n.
+mk_Vector C n (compose A B C f vA vB) ?.
+>length_compose >(len A n vA) >(len B n vB) normalize 
+>(le_to_leb_true … (le_n n)) //
+qed.
+*)
+
+definition current_chars ≝ λsig.λM:NTM sig.λc:config sig M.
+  vec_map ?? (λt.option_hd ? (right ? t)) (S (tapes_no sig M)) (tapes ?? c).
+
+let rec mem A (a:A) (l:list A) on l ≝
+  match l with
+  [ nil ⇒ False
+  | cons hd tl ⇒ a=hd ∨ mem A a tl
+  ]. 
+
+definition reach ≝ λsig.λM:NTM sig.λc,c1:config sig M.
+  ∃q,l,q1,mvs. 
+    state ?? c = q ∧ 
+    halt ?? q = false ∧
+    current_chars ?? c = l ∧
+    mem ? 〈〈q,l〉,〈q1,mvs〉〉 (trans ? M)  ∧ 
+    state ?? c1 = q1 ∧
+    tapes ?? c1 = (compose_vec ??? (tape_move sig) ? (tapes ?? c) mvs).
+
+(*
+definition empty_tapes ≝ λsig.λn.
+mk_Vector ? n (make_list (tape sig) (mk_tape sig [] []) n) ?.
+elim n // normalize //
+qed.
+*)
+
+definition init ≝ λsig.λM:NTM sig.λi:(list sig).
+  mk_config ??
+    (start sig M)
+    (vec_cons ? (mk_tape sig [] i) ? (empty_tapes sig (tapes_no sig M))).
+
+definition accepted ≝ λsig.λM:NTM sig.λw:(list sig).
+∃c. star ? (reach sig M) (init sig M w) c ∧
+  accept ?? (state ?? c) = true.
+
diff --git a/matita/matita/lib/turing/oracle.ma b/matita/matita/lib/turing/oracle.ma
new file mode 100644
index 000000000..4b6d7b1c7
--- /dev/null
+++ b/matita/matita/lib/turing/oracle.ma
@@ -0,0 +1,99 @@
+(*
+    ||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 "turing/turing.ma". 
+
+(* Oracle machines *)
+
+record TM (sig:FinSet): Type[1] ≝ 
+{ states : FinSet;
+  tapes_no: nat; (* additional working tapes *)
+  trans : states × (Vector (option sig) (S tapes_no)) → 
+    states  × (Vector (sig × move) (S tapes_no)) × (option sig) ;
+  output: list sig;
+  start: states;
+  halt : states → bool
+}.
+
+inductive oracle_states :Type[0] ≝
+  | query : oracle_states
+  | yes : oracle_states
+  | no : oracle_states.
+
+record config (sig:FinSet) (M:TM sig): Type[0] ≝
+{ state : states sig M;
+  query : list sig;
+  tapes : Vector (tape sig) (S (tapes_no sig M));
+  out : list sig
+}.
+
+definition option_hd ≝ λA.λl:list A.
+  match l with
+  [nil ⇒ None ?
+  |cons a _ ⇒ Some ? a
+  ].
+
+definition tape_move ≝ λsig.λt: tape sig.λm:sig × move.
+  match \snd m with
+  [ R ⇒ mk_tape sig ((\fst m)::(left ? t)) (tail ? (right ? t))
+  | L ⇒ mk_tape sig (tail ? (left ? t)) ((\fst m)::(right ? t))
+  | N ⇒ mk_tape sig (left ? t) ((\fst m)::(tail ? (right ? t)))
+  ].
+
+definition current_chars ≝ λsig.λM:TM sig.λc:config sig M.
+  vec_map ?? (λt.option_hd ? (right ? t)) (S (tapes_no sig M)) (tapes ?? c).
+
+definition opt_cons ≝ λA.λa:option A.λl:list A.
+  match a with
+  [ None ⇒ l
+  | Some a ⇒ a::l
+  ].
+
+definition step ≝ λsig.λM:TM sig.λc:config sig M.
+  let 〈news,mvs,outchar〉 ≝ trans sig M 〈state ?? c,current_chars ?? c〉 in
+  mk_config ?? 
+    news 
+    (pmap_vec ??? (tape_move sig) ? (tapes ?? c) mvs)
+    (opt_cons ? outchar (out ?? c)).
+
+definition empty_tapes ≝ λsig.λn.
+mk_Vector ? n (make_list (tape sig) (mk_tape sig [] []) n) ?.
+elim n // normalize //
+qed.
+
+definition init ≝ λsig.λM:TM sig.λi:(list sig).
+  mk_config ??
+    (start sig M)
+    (vec_cons ? (mk_tape sig [] i) ? (empty_tapes sig (tapes_no sig M)))
+    [ ].
+
+definition stop ≝ λsig.λM:TM sig.λc:config sig M.
+  halt sig M (state sig M c).
+
+let rec loop (A:Type[0]) n (f:A→A) p a on n ≝
+  match n with 
+  [ O ⇒ None ?
+  | S m ⇒ if p a then (Some ? a) else loop A m f p (f a)
+  ].
+
+(* Compute ? M f states that f is computed by M *)
+definition Compute ≝ λsig.λM:TM sig.λf:(list sig) → (list sig).
+∀l.∃i.∃c.
+  loop ? i (step sig M) (stop sig M) (init sig M l) = Some ? c ∧
+  out ?? c = f l.
+
+(* for decision problems, we accept a string if on termination
+output is not empty *)
+
+definition ComputeB ≝ λsig.λM:TM sig.λf:(list sig) → bool.
+∀l.∃i.∃c.
+  loop ? i (step sig M) (stop sig M) (init sig M l) = Some ? c ∧
+  (isnilb ? (out ?? c) = false).
diff --git a/matita/matita/lib/turing/turing.ma b/matita/matita/lib/turing/turing.ma
new file mode 100644
index 000000000..946999784
--- /dev/null
+++ b/matita/matita/lib/turing/turing.ma
@@ -0,0 +1,103 @@
+(*
+    ||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/vectors.ma".
+
+record tape (sig:FinSet): Type[0] ≝ 
+{ left : list sig;
+  right: list sig
+}.
+
+inductive move : Type[0] ≝
+| L : move 
+| R : move
+| N : move. 
+
+(* We do not distinuish an input tape *)
+
+record TM (sig:FinSet): Type[1] ≝ 
+{ states : FinSet;
+  tapes_no: nat; (* additional working tapes *)
+  trans : states × (Vector (option sig) (S tapes_no)) → 
+    states  × (Vector (sig × move) (S tapes_no)) × (option sig) ;
+  output: list sig;
+  start: states;
+  halt : states → bool
+}.
+
+record config (sig:FinSet) (M:TM sig): Type[0] ≝
+{ state : states sig M;
+  tapes : Vector (tape sig) (S (tapes_no sig M));
+  out : list sig
+}.
+
+definition option_hd ≝ λA.λl:list A.
+  match l with
+  [nil ⇒ None ?
+  |cons a _ ⇒ Some ? a
+  ].
+
+definition tape_move ≝ λsig.λt: tape sig.λm:sig × move.
+  match \snd m with
+  [ R ⇒ mk_tape sig ((\fst m)::(left ? t)) (tail ? (right ? t))
+  | L ⇒ mk_tape sig (tail ? (left ? t)) ((\fst m)::(right ? t))
+  | N ⇒ mk_tape sig (left ? t) ((\fst m)::(tail ? (right ? t)))
+  ].
+
+definition current_chars ≝ λsig.λM:TM sig.λc:config sig M.
+  vec_map ?? (λt.option_hd ? (right ? t)) (S (tapes_no sig M)) (tapes ?? c).
+
+definition opt_cons ≝ λA.λa:option A.λl:list A.
+  match a with
+  [ None ⇒ l
+  | Some a ⇒ a::l
+  ].
+
+definition step ≝ λsig.λM:TM sig.λc:config sig M.
+  let 〈news,mvs,outchar〉 ≝ trans sig M 〈state ?? c,current_chars ?? c〉 in
+  mk_config ?? 
+    news 
+    (pmap_vec ??? (tape_move sig) ? (tapes ?? c) mvs)
+    (opt_cons ? outchar (out ?? c)).
+
+definition empty_tapes ≝ λsig.λn.
+mk_Vector ? n (make_list (tape sig) (mk_tape sig [] []) n) ?.
+elim n // normalize //
+qed.
+
+definition init ≝ λsig.λM:TM sig.λi:(list sig).
+  mk_config ??
+    (start sig M)
+    (vec_cons ? (mk_tape sig [] i) ? (empty_tapes sig (tapes_no sig M)))
+    [ ].
+
+definition stop ≝ λsig.λM:TM sig.λc:config sig M.
+  halt sig M (state sig M c).
+
+let rec loop (A:Type[0]) n (f:A→A) p a on n ≝
+  match n with 
+  [ O ⇒ None ?
+  | S m ⇒ if p a then (Some ? a) else loop A m f p (f a)
+  ].
+
+(* Compute ? M f states that f is computed by M *)
+definition Compute ≝ λsig.λM:TM sig.λf:(list sig) → (list sig).
+∀l.∃i.∃c.
+  loop ? i (step sig M) (stop sig M) (init sig M l) = Some ? c ∧
+  out ?? c = f l.
+
+(* for decision problems, we accept a string if on termination
+output is not empty *)
+
+definition ComputeB ≝ λsig.λM:TM sig.λf:(list sig) → bool.
+∀l.∃i.∃c.
+  loop ? i (step sig M) (stop sig M) (init sig M l) = Some ? c ∧
+  (isnilb ? (out ?? c) = false).
diff --git a/matita/matita/lib/turing/turing_old.ma b/matita/matita/lib/turing/turing_old.ma
new file mode 100644
index 000000000..f50426985
--- /dev/null
+++ b/matita/matita/lib/turing/turing_old.ma
@@ -0,0 +1,119 @@
+(*
+    ||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".
+
+record Vector (A:Type[0]) (n:nat): Type[0] ≝ 
+{ vec :> list A;
+  len: length ? vec = n
+}.
+
+record TM (sig:FinSet): Type[1] ≝ 
+{ states : FinSet;
+  tapes_no: nat;
+  trans : states × (option sig) × (Vector (option sig) tapes_no) → 
+    states × bool × (Vector (list sig) tapes_no);
+  start: states;
+  halt : states
+}.
+
+definition config ≝ λsig.λM:TM sig.
+  states sig M × (list sig) × (Vector (list sig) (tapes_no sig M)).
+
+definition option_hd ≝ λA.λl:list A.
+  match l with
+  [nil ⇒ None ?
+  |cons a _ ⇒ Some ? a
+  ].
+
+lemma length_tail: ∀A,l. length ? (tail A l) = pred (length ? l).
+#A #l elim l // 
+qed.
+
+definition vec_tail ≝ λA.λn.λv:Vector A n.
+mk_Vector A (pred n) (tail A v) ?.
+>length_tail >(len A n v) //
+qed.
+
+definition vec_cons ≝ λA.λa.λn.λv:Vector A n.
+mk_Vector A (S n) (cons A a v) ?.
+normalize >(len A n v) //
+qed.
+
+lemma length_map: ∀A,B,l.∀f:A→B. length ? (map ?? f l) = length ? l.
+#A #B #l #f elim l // #a #tl #Hind normalize //
+qed.
+
+definition vec_map ≝ λA,B.λf:A→B.λn.λv:Vector A n.
+mk_Vector B n (map ?? f v) 
+  (trans_eq … (length_map …) (len A n v)).
+  
+definition hds ≝ λsig.λM.λc:config sig M. vec_map ?? (option_hd ?) (tapes_no sig M) (\snd c).
+
+definition tls ≝ λsig.λM.λc:config sig M.vec_map ?? (tail ?) (tapes_no sig M) (\snd c).
+
+let rec compose A B C (f:A→B→C) l1 l2 on l1 ≝
+   match l1 with
+   [ nil ⇒ nil C
+   | cons a tlA ⇒ 
+     match l2 with
+     [nil ⇒ nil C
+     |cons b tlB ⇒ (f a b)::compose A B C f tlA tlB
+     ]
+   ].
+
+lemma length_compose: ∀A,B,C.∀f:A→B→C.∀l1,l2.
+length C (compose  A B C f l1 l2) = 
+  min (length A l1) (length B l2).
+#A #B #C #f #l1 elim l1 // #a #tlA #Hind #l2 cases l2 //
+#b #tlB lapply (Hind tlB) normalize 
+cases (true_or_false (leb (length A tlA) (length B tlB))) #H >H
+normalize //
+qed.
+
+definition compose_vec ≝ λA,B,C.λf:A→B→C.λn.λvA:Vector A n.λvB:Vector B n.
+mk_Vector C n (compose A B C f vA vB) ?.
+>length_compose >(len A n vA) >(len B n vB) normalize 
+>(le_to_leb_true … (le_n n)) //
+qed.
+
+definition step ≝ λsig.λM:TM sig.λc:config sig M.
+  match (trans sig M 〈〈\fst (\fst c),option_hd ? (\snd (\fst c))〉,hds sig M c〉) with
+  [mk_Prod p l ⇒ 
+    let work_tapes ≝ compose_vec ??? (append ?) (tapes_no sig M) l (tls sig M c) in
+    match p with 
+    [mk_Prod s b ⇒ 
+      let old_input ≝ \snd (\fst c) in
+      let input ≝ if b then tail ? old_input else  old_input in
+      〈〈s,input〉,work_tapes〉]].
+
+definition empty_tapes ≝ λsig.λM:TM sig.
+mk_Vector ? (tapes_no sig M) (make_list (list sig) [ ] (tapes_no sig M)) ?.
+elim (tapes_no sig M) // normalize //
+qed.
+
+definition init ≝ λsig.λM:TM sig.λi:(list sig).
+  〈〈start sig M,i〉,empty_tapes sig M〉.
+
+definition stop ≝ λsig.λM:TM sig.λc:config sig M.
+  eqb (states sig M) (\fst(\fst c)) (halt sig M).
+
+let rec loop (A:Type[0]) n (f:A→A) p a on n ≝
+  match n with 
+  [ O ⇒ None ?
+  | S m ⇒ if p a then (Some ? a) else loop A m f p (f a)
+  ].
+
+definition Compute ≝ λsig.λM:TM sig.λf:(list sig) → (list sig).
+∀l.∃i.∃c.((loop ? i (step sig M) (stop sig M) (init sig M l) = Some ? c) ∧
+  (hd ? (\snd c) [ ] = f l)).
+
+(* An extended machine *)
\ No newline at end of file