X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fturing%2Funiversal.ma;h=35d7e0290ff87badba5bd22f2b1020eb98f8ddee;hb=d10880b504902558609fc620d0a62bcf30ea912a;hp=92b61436bb443d7147b9805f4bf33844be438a50;hpb=98b3343239c260021bd2a6837df0a5102b22527e;p=helm.git

diff --git a/matita/matita/lib/turing/universal.ma b/matita/matita/lib/turing/universal.ma
index 92b61436b..35d7e0290 100644
--- a/matita/matita/lib/turing/universal.ma
+++ b/matita/matita/lib/turing/universal.ma
@@ -1,10 +1,5 @@
 include "turing/turing.ma".
 
-axiom Q : FinSet.
-axiom q0 : Q. axiom q1 : Q. axiom q2 : Q. axiom q3 : Q. axiom q4 : Q. axiom q5 : Q. 
-axiom q6 : Q. axiom q7 : Q. axiom q8 : Q. axiom q9 : Q. axiom q10 : Q. axiom q11 : Q. 
-axiom q12 : Q. axiom q13 : Q. axiom q14 : Q. axiom q15 : Q. axiom q16 : Q.
-
 (* 
 Simboli:
 0 1 *0 *1 # | ,
@@ -81,55 +76,61 @@ STATO 9:
 
 *)
 
-match s with
-[ q0 ⇒ match c with
-  [ grid ⇒ 〈q1,〈#,R〉〉
-  | _ ⇒ 〈qsink,〈c,N〉〉 ]
-| q1 ⇒ match c with
-  [ mark x ⇒ 〈q2 x,〈bit x,R〉〉
-  | _ ⇒ 〈q1,〈c,L〉〉 ]
-| q2 x ⇒ match c with
-  [ bit y ⇒ 〈q3 x,〈mark y,R〉〉
-  | grid ⇒ 〈q3 x,〈grid,R〉〉
-  | _ ⇒ 〈qsink,〈c,N〉〉 ]
-| q3 x ⇒ match c with
-  [ mark y ⇒ match bool_eqb x y with
-    [ true ⇒ 〈q4,〈bit y,R〉〉
-    | false ⇒ 〈q5,〈bit y,R〉〉 ]
-  | _ ⇒ 〈q3 x,〈c,R〉〉 ]
-| q4 ⇒ match c with
-  [ comma ⇒ 〈qSuccess,〈comma,R〉〉
-  | bit x ⇒ 〈q1,〈mark x,L〉〉
-  | _ ⇒ 〈qsink,〈c,N〉〉 ]
-| q5 ⇒ match c with
-  | bar ⇒ 〈q6,〈bar,R〉〉
-  | _ ⇒ 〈q5,〈c,R〉〉
-| q6 ⇒ match c with 
-  [ bit x ⇒ 〈q7,〈mark x,L〉〉
-  | _ ⇒ 〈qsink,〈c,N〉〉 ]
-| q7 ⇒ match c with
-  [ grid ⇒ 〈q8,〈grid,L〉〉
-  | _ ⇒ 〈q7,〈c,L〉〉 ]
-| q8 ⇒ match c with
-  [ grid ⇒ 〈q9,〈grid,R〉〉 
-  | mark x ⇒ 〈q8,〈bit x,L〉〉 
-  | _ ⇒ 〈q8,〈c,L〉〉 ]
-| q9 ⇒ match c with
-  [ bit x ⇒ 〈qFailure,〈mark x,L〉〉 
-  | _ ⇒ 〈qsink,〈c,N〉〉 ]
-| qsink ⇒ 〈qsink,〈c,N〉〉 ]
-
-  
-
-
-
-
-
-
+inductive alpha_uni : Type[0] ≝ 
+| bit : bool → alpha_uni
+| mark : bool → alpha_uni
+| grid : alpha_uni | bar : alpha_uni | comma : alpha_uni.
 
+inductive Qmatch : Type[0] ≝
+| qm0 : Qmatch | qm1 : Qmatch | qm2 : bool → Qmatch | qm3 : bool → Qmatch
+| qm4 : Qmatch | qm5 : Qmatch | qm6 : Qmatch | qm7 : Qmatch 
+| qm8 : Qmatch | qm9 : Qmatch 
+| qmsuccess : Qmatch | qmfailure : Qmatch | qmsink : Qmatch.
 
+definition bool_eqb ≝ λb1,b2:bool.¬ (xorb b1 b2).
 
+definition tmatch ≝ λs,c.
+match s with
+[ qm0 ⇒ match c with
+  [ grid ⇒ 〈qm1,〈grid,R〉〉
+  | _ ⇒ 〈qmsink,〈c,N〉〉 ]
+| qm1 ⇒ match c with
+  [ mark x ⇒ 〈qm2 x,〈bit x,R〉〉
+  | _ ⇒ 〈qm1,〈c,L〉〉 ]
+| qm2 x ⇒ match c with
+  [ bit y ⇒ 〈qm3 x,〈mark y,R〉〉
+  | grid ⇒ 〈qm3 x,〈grid,R〉〉
+  | _ ⇒ 〈qmsink,〈c,N〉〉 ]
+| qm3 x ⇒ match c with
+  [ mark y ⇒ match bool_eqb x y with
+    [ true ⇒ 〈qm4,〈bit y,R〉〉
+    | false ⇒ 〈qm5,〈bit y,R〉〉 ]
+  | _ ⇒ 〈qm3 x,〈c,R〉〉 ]
+| qm4 ⇒ match c with
+  [ comma ⇒ 〈qmsuccess,〈comma,R〉〉
+  | bit x ⇒ 〈qm1,〈mark x,L〉〉
+  | _ ⇒ 〈qmsink,〈c,N〉〉 ]
+| qm5 ⇒ match c with
+  [ bar ⇒ 〈qm6,〈bar,R〉〉
+  | _ ⇒ 〈qm5,〈c,R〉〉 ]
+| qm6 ⇒ match c with 
+  [ bit x ⇒ 〈qm7,〈mark x,L〉〉
+  | _ ⇒ 〈qmsink,〈c,N〉〉 ]
+| qm7 ⇒ match c with
+  [ grid ⇒ 〈qm8,〈grid,L〉〉
+  | _ ⇒ 〈qm7,〈c,L〉〉 ]
+| qm8 ⇒ match c with
+  [ grid ⇒ 〈qm9,〈grid,R〉〉 
+  | mark x ⇒ 〈qm8,〈bit x,L〉〉 
+  | _ ⇒ 〈qm8,〈c,L〉〉 ]
+| qm9 ⇒ match c with
+  [ bit x ⇒ 〈qmfailure,〈mark x,L〉〉 
+  | _ ⇒ 〈qmsink,〈c,N〉〉 ]
+| qmsink ⇒ 〈qmsink,〈c,N〉〉 
+| qmsuccess ⇒ 〈qmsuccess,〈c,N〉〉
+| qmfailure ⇒ 〈qmfailure,〈c,N〉〉].
 
+  
 (*
 ==============================
 MACCHINA PER COPIA NUOVO STATO IN CURRENT
@@ -148,7 +149,7 @@ Output:
 
 STATO 0:
   \forall x. x/*x/L --> 1
-
+  
 STATO 1:
   [01,|]/L --> 1
   #/L --> 2
@@ -182,8 +183,55 @@ STATO 8:
 
 STATO 9:
   stato finale
-
-
+*)
+(* TODO
+match s with
+ [ q0 ⇒ match c with
+   [ bit x ⇒ 〈q1,〈mark x,L〉〉
+   | _ ⇒ 〈qsink,〈c,N〉〉 ]
+ | q1 ⇒ match c with
+   [ bit x ⇒ 〈q1,〈c,L〉〉
+   | comma ⇒ 〈q1,〈c,L〉〉
+   | bar ⇒ 〈q1,〈c,L〉〉
+   | grid ⇒ 〈q2,〈c,R〉〉
+   | _ ⇒ 〈qsink,〈c,N〉〉 ]
+ | q2 ⇒ match c with
+   [ bit x ⇒ 〈q2,〈c,L〉〉
+   | grid ⇒ 〈q3,〈c,R〉〉 
+   | _ ⇒ 〈qsink,〈c,N〉〉 ]
+ | q3 ⇒ match c with
+   [ bit x ⇒ 〈q4,〈mark x,R〉〉
+   | grid ⇒ 〈q8,〈c,R〉〉
+   | _ ⇒ 〈qsink,〈c,N〉〉 ]
+ | q4 ⇒ match c with
+   [ bit x ⇒ 〈q4,〈c,R〉〉
+   | comma ⇒ 〈q4,〈c,R〉〉
+   | bar ⇒ 〈q4,〈c,R〉〉
+   | grid ⇒ 〈q4,〈c,R〉〉
+   | mark x ⇒ 〈q5 x,〈bit x,R〉〉 ]
+ | q5 x ⇒ match c with
+   [ grid ⇒ 〈q6 x,〈c,R〉〉
+   | bit y ⇒ 〈q7 x,〈mark y,L〉〉
+   | _ ⇒ 〈qsink,〈c,N〉〉 ]
+ | q6 x ⇒ match c with
+   [ bit D ⇒ 〈q7 x,〈mark D,L〉〉
+   | _ ⇒ 〈qsink,〈c,N〉〉 ]
+ | q7 x ⇒ match c with
+   [ bit y ⇒ 〈q7 x,〈c,L〉〉
+   | comma ⇒ 〈q7 x,〈c,L〉〉
+   | bar ⇒ 〈q7 x,〈c,L〉〉
+   | grid ⇒ 〈q7 x,〈c,L〉〉
+   | mark y ⇒ 〈q3,〈bit x,R〉〉 ]
+ | q8 ⇒ match c with
+   [ bit y ⇒ 〈q8,〈c,R〉〉
+   | comma ⇒ 〈q8,〈c,R〉〉
+   | bar ⇒ 〈q8,〈c,R〉〉
+   | grid ⇒ 〈q8,〈c,R〉〉
+   | mark D ⇒ 〈q9,〈bit D,L〉〉 ]
+ | q9 ⇒ ? (* successo *)
+ ].
+*)
+(*
 ==================================
 MACCHINE PER SPOSTARE LA "TESTINA"
 ================================
@@ -242,8 +290,20 @@ STATO 3:
 
 STATO 4:
   stato finale
-
-
+*)
+(* TODO
+match s with
+ [ q0 ⇒ match c with
+   [ bit x ⇒ 〈q1 x,〈c,L〉〉
+   | _ ⇒ 〈qsink,〈c,N〉〉 ]
+ | q1 x ⇒ match c with
+   [ grid ⇒ 〈q3,〈bit x,R〉〉
+   | _ ⇒ 〈q2 c,〈bit x,R〉〉 ]
+ | q2 d ⇒ 〈q0,〈d,L〉〉
+ | q3 ⇒ 〈q4,〈grid,L〉〉
+ | q4 ⇒ (* finale *) ].
+*)
+(*
 MACCHINA B
 ----------
 Sposta il carattere binario su cui si trova la testina oltre il primo # alla sua destra.
@@ -274,8 +334,20 @@ STATO 3:
 
 STATO 4:
   stato finale
-
-
+*)
+(* TODO
+match s with
+[ q0 ⇒ match c with
+  [ bit x ⇒ 〈q1 x,〈c,R〉〉
+  | _ ⇒ 〈qsink,〈c,N〉〉]
+| q1 x ⇒ match c with
+  [ grid ⇒ 〈q3,〈bit x,L〉〉
+  | _ ⇒ 〈q2 c,〈bit x,L〉〉 ]
+| q2 d ⇒ 〈q0,〈d,R〉〉
+| q3 ⇒ 〈q4,〈grid,L〉〉 
+| q4 ⇒ (* finale *) ].
+*)
+(*
 MACCHINA C
 ----------
 Sposta il carattere binario su cui si trova la testina appena prima del primo # alla sua destra.
@@ -304,3 +376,14 @@ STATO 3:
   stato finale
 
 *)
+(* TODO
+match s with 
+[ q0 ⇒ match c with
+  [ bit x ⇒ 〈q1 x,〈c,R〉〉
+  | _ ⇒ 〈qsink,〈c,N〉〉 ]
+| q1 x ⇒ match c with
+  [ grid ⇒ 〈q3,〈grid,L〉〉
+  | _ ⇒ 〈q2 c,〈bit x,L〉〉
+| q2 d ⇒ 〈q0,〈c,R〉〉
+| q3 ⇒ (* finale *) ].
+*)
\ No newline at end of file