X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fturing%2Fbasic_machines.ma;h=f92afc7b9b30c3c1e07fa9e2ccf45c96d4f64eda;hb=fc803c84d8d99e1bf1f5f655312e120dcd87d90e;hp=a2357682972f1ddd4e67458f16e98de02d191eb2;hpb=99865bbdbb8b4694c85085abb0e98b4d3be7ea9f;p=helm.git

diff --git a/matita/matita/lib/turing/basic_machines.ma b/matita/matita/lib/turing/basic_machines.ma
index a23576829..f92afc7b9 100644
--- a/matita/matita/lib/turing/basic_machines.ma
+++ b/matita/matita/lib/turing/basic_machines.ma
@@ -21,8 +21,8 @@ definition write ≝ λalpha,c.
   mk_TM alpha write_states
   (λp.let 〈q,a〉 ≝ p in
     match pi1 … q with 
-    [ O ⇒ 〈wr1,Some ? 〈c,N〉〉
-    | S _ ⇒ 〈wr1,None ?〉 ])
+    [ O ⇒ 〈wr1,Some ? c,N〉
+    | S _ ⇒ 〈wr1,None ?,N〉 ])
   wr0 (λx.x == wr1).
   
 definition R_write ≝ λalpha,c,t1,t2.
@@ -43,10 +43,10 @@ definition move_r ≝
   λalpha:FinSet.mk_TM alpha move_states
   (λp.let 〈q,a〉 ≝ p in
     match a with
-    [ None ⇒ 〈move1,None ?〉
+    [ None ⇒ 〈move1,None ?,N〉
     | Some a' ⇒ match (pi1 … q) with
-      [ O ⇒ 〈move1,Some ? 〈a',R〉〉
-      | S q ⇒ 〈move1,None ?〉 ] ])
+      [ O ⇒ 〈move1,Some ? a',R〉
+      | S q ⇒ 〈move1,None ?,N〉 ] ])
   move0 (λq.q == move1).
   
 definition R_move_r ≝ λalpha,t1,t2.
@@ -80,10 +80,10 @@ definition move_l ≝
   λalpha:FinSet.mk_TM alpha move_states
   (λp.let 〈q,a〉 ≝ p in
     match a with
-    [ None ⇒ 〈move1,None ?〉
+    [ None ⇒ 〈move1,None ?,N〉
     | Some a' ⇒ match pi1 … q with
-      [ O ⇒ 〈move1,Some ? 〈a',L〉〉
-      | S q ⇒ 〈move1,None ?〉 ] ])
+      [ O ⇒ 〈move1,Some ? a',L〉
+      | S q ⇒ 〈move1,None ?,N〉 ] ])
   move0 (λq.q == move1).
 
 definition R_move_l ≝ λalpha,t1,t2.
@@ -106,6 +106,30 @@ lemma sem_move_l :
   #ls1 #c1 #rs1 #H destruct cases ls1 // ] ] ]
 qed.
 
+(* a slightly different move machine. *)
+definition smove_states ≝ initN 2.
+
+definition smove0 : smove_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 2 (refl …)).
+definition smove1 : smove_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 2 (refl …)).
+
+definition trans_smove ≝ 
+ λsig,D.
+ λp:smove_states × (option sig).
+ let 〈q,a〉 ≝ p in match (pi1 … q) with
+ [ O ⇒ 〈smove1,None sig, D〉
+ | S _ ⇒ 〈smove1,None sig, N〉 ].
+
+definition move ≝ 
+  λsig,D.mk_TM sig smove_states (trans_smove sig D) smove0 (λq.q == smove1).
+
+definition Rmove ≝ 
+  λalpha,D,t1,t2. t2 = tape_move alpha t1 D.
+
+lemma sem_move_single :
+  ∀alpha,D.move alpha D ⊨ Rmove alpha D.
+#alpha #D #int %{2} %{(mk_config ? smove_states smove1 ?)} [| % % ]
+qed.
+
 (********************************* test char **********************************)
 
 (* the test_char machine ends up in two different states q1 and q2 wether or not
@@ -125,11 +149,11 @@ definition test_char ≝
   mk_TM alpha tc_states
   (λp.let 〈q,a〉 ≝ p in
    match a with
-   [ None ⇒ 〈tc_false, None ?〉
+   [ None ⇒ 〈tc_false, None ?,N〉
    | Some a' ⇒ 
      match test a' with
-     [ true ⇒ 〈tc_true,None ?〉
-     | false ⇒ 〈tc_false,None ?〉 ]])
+     [ true ⇒ 〈tc_true,None ?,N〉
+     | false ⇒ 〈tc_false,None ?,N〉 ]])
   tc_start (λx.notb (x == tc_start)).
 
 definition Rtc_true ≝ 
@@ -234,15 +258,15 @@ definition swap_r ≝
   let 〈q',b〉 ≝ q in
   let q' ≝ pi1 nat (λi.i<4) q' in
   match a with 
-  [ None ⇒ 〈〈swap3,foo〉,None ?〉 (* if tape is empty then stop *)
+  [ None ⇒ 〈〈swap3,foo〉,None ?,N〉 (* if tape is empty then stop *)
   | Some a' ⇒ 
   match q' with
-  [ O ⇒ (* q0 *) 〈〈swap1,a'〉,Some ? 〈a',R〉〉  (* save in register and move R *)
+  [ O ⇒ (* q0 *) 〈〈swap1,a'〉,Some ? a',R〉  (* save in register and move R *)
   | S q' ⇒ match q' with
-    [ O ⇒ (* q1 *) 〈〈swap2,a'〉,Some ? 〈b,L〉〉 (* swap with register and move L *)
+    [ O ⇒ (* q1 *) 〈〈swap2,a'〉,Some ? b,L〉 (* swap with register and move L *)
     | S q' ⇒ match q' with
-      [ O ⇒ (* q2 *) 〈〈swap3,foo〉,Some ? 〈b,N〉〉 (* copy from register and stay *)
-      | S q' ⇒ (* q3 *) 〈〈swap3,foo〉,None ?〉 (* final state *)
+      [ O ⇒ (* q2 *) 〈〈swap3,foo〉,Some ? b,N〉 (* copy from register and stay *)
+      | S q' ⇒ (* q3 *) 〈〈swap3,foo〉,None ?,N〉 (* final state *)
       ]
     ]
   ]])
@@ -283,15 +307,15 @@ definition swap_l ≝
   let 〈q',b〉 ≝ q in
   let q' ≝ pi1 nat (λi.i<4) q' in
   match a with 
-  [ None ⇒ 〈〈swap3,foo〉,None ?〉 (* if tape is empty then stop *)
+  [ None ⇒ 〈〈swap3,foo〉,None ?,N〉 (* if tape is empty then stop *)
   | Some a' ⇒ 
   match q' with
-  [ O ⇒ (* q0 *) 〈〈swap1,a'〉,Some ? 〈a',L〉〉  (* save in register and move L *)
+  [ O ⇒ (* q0 *) 〈〈swap1,a'〉,Some ? a',L〉  (* save in register and move L *)
   | S q' ⇒ match q' with
-    [ O ⇒ (* q1 *) 〈〈swap2,a'〉,Some ? 〈b,R〉〉 (* swap with register and move R *)
+    [ O ⇒ (* q1 *) 〈〈swap2,a'〉,Some ? b,R〉 (* swap with register and move R *)
     | S q' ⇒ match q' with
-      [ O ⇒ (* q2 *) 〈〈swap3,foo〉,Some ? 〈b,N〉〉 (* copy from register and stay *)
-      | S q' ⇒ (* q3 *) 〈〈swap3,foo〉,None ?〉 (* final state *)
+      [ O ⇒ (* q2 *) 〈〈swap3,foo〉,Some ? b,N〉 (* copy from register and stay *)
+      | S q' ⇒ (* q3 *) 〈〈swap3,foo〉,None ?,N〉 (* final state *)
       ]
     ]
   ]])