decentralizing core notation continues ...

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

diff --git a/matita/matita/lib/turing/turing.ma b/matita/matita/lib/turing/turing.ma
index a8290de51d7d32eb365fa3b7fdc9786b3bc2a8bb..dc0a43e755968a27ea32aaea3deb2fa84548a03d 100644 (file)
--- a/matita/matita/lib/turing/turing.ma
+++ b/matita/matita/lib/turing/turing.ma
@@ -1,3 +1,4 @@
+include "basics/core_notation/fintersects_2.ma".
 include "turing/mono.ma".
 include "basics/vectors.ma".
 
@@ -8,7 +9,7 @@ include "basics/vectors.ma".
 record mTM (sig:FinSet) (tapes_no:nat) : Type[1] ≝ 
 { states : FinSet;
   trans : states × (Vector (option sig) (S tapes_no)) → 
-    states  × (Vector (option (sig × move))(S tapes_no));
+    states  × (Vector ((option sig) × move) (S tapes_no));
   start: states;
   halt : states → bool
 }.
@@ -32,11 +33,23 @@ qed.
 definition current_chars ≝ λsig.λn.λtapes.
   vec_map ?? (current sig) (S n) tapes.
 
+lemma nth_current_chars : ∀sig,n,tapes,i.
+  nth i ? (current_chars sig n tapes) (None ?) 
+   = current sig (nth i ? tapes (niltape sig)).
+#sig #n #tapes #i >(nth_vec_map … (current sig) i (S n)) %
+qed.
+
+definition tape_move_multi ≝ 
+  λsig,n,ts,mvs.
+  pmap_vec ??? (tape_move_mono sig) n ts mvs.
+  
+lemma tape_move_multi_def : ∀sig,n,ts,mvs.
+  tape_move_multi sig n ts mvs = pmap_vec ??? (tape_move_mono sig) n ts mvs.
+// qed.
+
 definition step ≝ λsig.λn.λM:mTM sig n.λc:mconfig sig (states ?? M) n.
   let 〈news,mvs〉 ≝ trans sig n M 〈cstate ??? c,current_chars ?? (ctapes ??? c)〉 in
-  mk_mconfig ??? 
-    news 
-    (pmap_vec ??? (tape_move sig) ? (ctapes ??? c) mvs).
+  mk_mconfig ??? news (tape_move_multi sig ? (ctapes ??? c) mvs).
 
 definition empty_tapes ≝ λsig.λn.
 mk_Vector ? n (make_list (tape sig) (niltape sig) n) ?.
@@ -189,7 +202,7 @@ definition start_nop : initN 1 ≝ mk_Sig ?? 0 (le_n … 1). *)
 
 definition nop ≝ 
   λalpha:FinSet.λn.mk_mTM alpha n nop_states
-  (λp.let 〈q,a〉 ≝ p in 〈q,mk_Vector ? (S n) (make_list ? (None ?) (S n)) ?〉)
+  (λp.let 〈q,a〉 ≝ p in 〈q,mk_Vector ? (S n) (make_list ? (〈None ?,N〉) (S n)) ?〉)
   start_nop (λ_.true).
 elim n normalize //
 qed.
@@ -210,12 +223,12 @@ generalize in match ltn1; generalize in match ltm1;
 
 (************************** Sequential Composition ****************************)
 definition null_action ≝ λsig.λn.
-mk_Vector ? (S n) (make_list (option (sig × move)) (None ?) (S n)) ?.
+mk_Vector ? (S n) (make_list (option sig × move) (〈None ?,N〉) (S n)) ?.
 elim (S n) // normalize //
 qed.
 
 lemma tape_move_null_action: ∀sig,n,tapes.
-  pmap_vec ??? (tape_move sig) (S n) tapes (null_action sig n) = tapes.
+  tape_move_multi sig (S n) tapes (null_action sig n) = tapes.
 #sig #n #tapes cases tapes -tapes #tapes whd in match (null_action ??);
 #Heq @Vector_eq <Heq -Heq elim tapes //
 #a #tl #Hind whd in ⊢ (??%?); @eq_f2 // @Hind