From 7ac5fca2e08ea671a75c9adf4ef070dbd0ea2c37 Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Fri, 8 Jun 2012 11:48:47 +0000
Subject: [PATCH] merging of char_move_c and char_move_l

---
 matita/matita/lib/turing/char_move.ma | 208 ++++++++++++++++++++++++++
 1 file changed, 208 insertions(+)
 create mode 100644 matita/matita/lib/turing/char_move.ma

diff --git a/matita/matita/lib/turing/char_move.ma b/matita/matita/lib/turing/char_move.ma
new file mode 100644
index 000000000..66d92830a
--- /dev/null
+++ b/matita/matita/lib/turing/char_move.ma
@@ -0,0 +1,208 @@
+include "turing/turing.ma".
+
+(* 
+Simboli:
+0 1 *0 *1 # | ,
+
+[lista di simboli] fa match su un simbolo qualunque nella lista
+ad esempio [#|,] fa match con la gratella "#", la barra verticale "|" e la virgola ","
+
+Convenzione variabili:
+- x,y,z,D     = bit (non marcati)
+- *x,*y,*z,*D = bit marcati
+- c,d,e = caratteri (bit marcati e non marcati e separatori)
+
+Convenzioni mosse:
+c/D --> Q : leggo c, scrivo c, mi sposto a D e passo allo stato Q
+c/d/D --> Q : leggo c, scrivo d, mi sposto a D e passo allo stato Q
+
+*)
+
+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).
+
+(*
+==================================
+MACCHINE PER SPOSTARE LA "TESTINA"
+================================
+
+Lo spostamento a sx si ottiene mediante
+
+ls x # current y # macchina # rs
+----C--->
+ls x # current # y macchina # rs
+----B--->
+ls x # current # macchina # y rs
+----B--->
+ls # x current # macchina # y rs
+----C--->
+ls # current x # macchina # y rs
+
+
+Lo spostamento a dx si ottiene mediante
+
+ls # current x # macchina # y rs
+----A--->
+ls x # current # macchina # y rs
+----A--->
+ls x # current # macchina y # rs
+----A--->
+ls x # current y # macchina # rs
+
+
+MACCHINA A
+----------
+Sposta il carattere binario su cui si trova la testina oltre il primo # alla sua sinistra.
+
+Input:
+  
+  ls # cs x rs
+          ^
+          0
+
+Output:
+  ls x # cs rs
+     ^
+     4
+
+STATO 0:
+  \forall x.x/L --> 1(x)
+
+STATO 1(x):
+  \forall c != #. c/x/R --> 2(c)
+  #/x/R --> 3
+
+STATO 2(c):
+  \forall d. d/c/L --> 0
+
+STATO 3:
+  \forall c. c/#/L --> 4
+
+STATO 4:
+  stato finale
+*)
+
+(* struttura generica della semantica *) 
+lemma move_char_sem: ∀inc. prec inc → ∃i. ∃outc. loop i step inc = Some outc 
+∧ postc outc inc. 
+
+lemma sequential : ∀M1,M2. 
+
+definition pre c ≝ 
+  let s ≝ state c in
+  let tp ≝ tape c in
+  let left ≝ 
+  
+definition post c1 c2 ≝
+  let s1 ≝ state c1 in
+  let tp1 ≝ tape c1 in
+  let leftt ≝ left tp1 in
+  let rightt ≝ right tp1 in
+  c2 = mk_config finals 
+  
+
+
+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.
+
+Input:
+
+  ls x cs # rs
+     ^
+     0
+
+Output:
+  ls cs # x rs
+          ^
+          4
+
+STATO 0:
+  \forall x.x/R --> 1(x)
+
+STATO 1(x):
+  \forall c != #. c/x/L --> 2(c)
+  #/x/L --> 3
+
+STATO 2(c):
+  \forall d. d/c/R --> 0
+
+STATO 3:
+  \forall c. c/#/L --> 4
+
+STATO 4:
+  stato finale
+*)
+
+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.
+
+Input:
+  ls x cs # rs
+     ^
+     0
+
+Output:
+  ls cs x # rs
+        ^
+        3
+
+STATO 0:
+  \forall x. x/R --> 1(x)
+
+STATO 1(x):
+  \forall c != #. c/x/L --> 2(c)
+  #/#/L --> 3
+
+STATO 2(c):
+  \forall d. d/c/R --> 0
+
+STATO 3:
+  stato finale
+
+*)
+
+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 *) ].
-- 
2.39.2