From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Fri, 18 Jan 2013 11:08:33 +0000 (+0000)
Subject: high level semantics
X-Git-Tag: make_still_working~1330
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f4047107dfd976f173151174269f356b1f431ab7;p=helm.git

high level semantics
---

diff --git a/matita/matita/lib/basics/vectors.ma b/matita/matita/lib/basics/vectors.ma
index e680e91a7..a48f04d0f 100644
--- a/matita/matita/lib/basics/vectors.ma
+++ b/matita/matita/lib/basics/vectors.ma
@@ -16,6 +16,9 @@ record Vector (A:Type[0]) (n:nat): Type[0] ≝
   len: length ? vec = n
 }.
 
+lemma Vector_of_list ≝ λA,l. 
+  mk_Vector A (|l|) l (refl ??).
+
 lemma Vector_eq : ∀A,n,v1,v2.
   vec A n v1 = vec A n v2 → v1 = v2.
 #A #n * #l1 #H1 * #l2 #H2 #eql1l2 generalize in match H1; 
diff --git a/matita/matita/lib/turing/multi_universal/unistep_aux.ma b/matita/matita/lib/turing/multi_universal/unistep_aux.ma
index 86f442783..7a8062ee3 100644
--- a/matita/matita/lib/turing/multi_universal/unistep_aux.ma
+++ b/matita/matita/lib/turing/multi_universal/unistep_aux.ma
@@ -329,9 +329,18 @@ definition R_unistep ≝ λn,l,h.λt1,t2: Vector ? 3.
       change_vec ??
         (change_vec ?? t1 (midtape ? [ ] bar (nstate@[nchar])) cfg)
         (tape_move_mono ? (nth obj ? t1 (niltape ?)) 〈Some ? nchar,char_to_move m〉) obj.
-    
-  
+
+definition tape_map ≝ λA,B:FinSet.λf:A→B.λt.
+  mk_tape B (map ?? f (left ? t)) 
+    (option_map ?? f (current ? t)) 
+    (map ?? f (right ? t)).
+
+definition low ≝ λM:normalTM.λc:nconfig (no_states M).Vector_of_list ?
+  [tape_map ?? bit (ctape ?? c);
+   midtape ? [ ] bar (bits_of_state ? (nhalt M) (cstate ?? c));
+   ?].
+
   
   
   
-  
\ No newline at end of file
+  .
\ No newline at end of file