X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fturing%2Fsimple_machines.ma;h=4b51989000dafecac35ab0bbaf14cea2b43e05aa;hb=d7d92f459cf6d76051c255497ee1ca898b111b76;hp=66ca59a06fcfe12a3d82f105e69aa51b357221f0;hpb=3b280742956d9d62aab53dd81704c250e3befe91;p=helm.git

diff --git a/matita/matita/lib/turing/simple_machines.ma b/matita/matita/lib/turing/simple_machines.ma
index 66ca59a06..4b5198900 100644
--- a/matita/matita/lib/turing/simple_machines.ma
+++ b/matita/matita/lib/turing/simple_machines.ma
@@ -9,7 +9,203 @@
      \ /   GNU General Public License Version 2   
       V_____________________________________________________________*)
 
-include "turing/multi_universal/match.ma".
+include "turing/if_multi.ma".
+include "turing/inject.ma".
+include "turing/basic_machines.ma".
+
+definition Rtc_multi_true ≝ 
+  λalpha,test,n,i.λt1,t2:Vector ? (S n).
+   (∃c. current alpha (nth i ? t1 (niltape ?)) = Some ? c ∧ test c = true) ∧ t2 = t1.
+   
+definition Rtc_multi_false ≝ 
+  λalpha,test,n,i.λt1,t2:Vector ? (S n).
+    (∀c. current alpha (nth i ? t1 (niltape ?)) = Some ? c → test c = false) ∧ t2 = t1.
+
+lemma sem_test_char_multi :
+  ∀alpha,test,n,i.i ≤ n → 
+  inject_TM ? (test_char ? test) n i ⊨ 
+  [ tc_true : Rtc_multi_true alpha test n i, Rtc_multi_false alpha test n i ].
+#alpha #test #n #i #Hin #int
+cases (acc_sem_inject … Hin (sem_test_char alpha test) int)
+#k * #outc * * #Hloop #Htrue #Hfalse %{k} %{outc} % [ %
+[ @Hloop
+| #Hqtrue lapply (Htrue Hqtrue) * * * #c *
+  #Hcur #Htestc #Hnth_i #Hnth_j %
+  [ %{c} % //
+  | @(eq_vec … (niltape ?)) #i0 #Hi0
+    cases (decidable_eq_nat i0 i) #Hi0i
+    [ >Hi0i @Hnth_i
+    | @sym_eq @Hnth_j @sym_not_eq // ] ] ]
+| #Hqfalse lapply (Hfalse Hqfalse) * * #Htestc #Hnth_i #Hnth_j %
+  [ @Htestc
+  | @(eq_vec … (niltape ?)) #i0 #Hi0
+    cases (decidable_eq_nat i0 i) #Hi0i
+    [ >Hi0i @Hnth_i
+    | @sym_eq @Hnth_j @sym_not_eq // ] ] ]
+qed.
+
+definition Rm_test_null_true ≝ 
+  λalpha,n,i.λt1,t2:Vector ? (S n).
+   current alpha (nth i ? t1 (niltape ?)) ≠ None ? ∧ t2 = t1.
+   
+definition Rm_test_null_false ≝ 
+  λalpha,n,i.λt1,t2:Vector ? (S n).
+    current alpha (nth i ? t1 (niltape ?)) = None ? ∧ t2 = t1.
+
+lemma sem_test_null_multi : ∀alpha,n,i.i ≤ n → 
+  inject_TM ? (test_null ?) n i ⊨ 
+    [ tc_true : Rm_test_null_true alpha n i, Rm_test_null_false alpha n i ].
+#alpha #n #i #Hin #int
+cases (acc_sem_inject … Hin (sem_test_null alpha) int)
+#k * #outc * * #Hloop #Htrue #Hfalse %{k} %{outc} % [ %
+[ @Hloop
+| #Hqtrue lapply (Htrue Hqtrue) * * #Hcur #Hnth_i #Hnth_j % //
+  @(eq_vec … (niltape ?)) #i0 #Hi0 cases (decidable_eq_nat i0 i) #Hi0i
+  [ >Hi0i @sym_eq @Hnth_i | @sym_eq @Hnth_j @sym_not_eq // ] ] 
+| #Hqfalse lapply (Hfalse Hqfalse) * * #Hcur #Hnth_i #Hnth_j %
+  [ @Hcur
+  | @(eq_vec … (niltape ?)) #i0 #Hi0 cases (decidable_eq_nat i0 i) // 
+    #Hi0i @sym_eq @Hnth_j @sym_not_eq // ] ] 
+qed.
+(* move a single tape *)
+definition mmove_states ≝ initN 2.
+
+definition mmove0 : mmove_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 2 (refl …)).
+definition mmove1 : mmove_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 2 (refl …)).
+
+definition trans_mmove ≝ 
+ λi,sig,n,D.
+ λp:mmove_states × (Vector (option sig) (S n)).
+ let 〈q,a〉 ≝ p in match (pi1 … q) with
+ [ O ⇒ 〈mmove1,change_vec ? (S n) (null_action ? n) (〈None ?,D〉) i〉
+ | S _ ⇒ 〈mmove1,null_action sig n〉 ].
+
+definition mmove ≝ 
+  λi,sig,n,D.
+  mk_mTM sig n mmove_states (trans_mmove i sig n D) 
+    mmove0 (λq.q == mmove1).
+    
+definition Rm_multi ≝ 
+  λalpha,n,i,D.λt1,t2:Vector ? (S n).
+  t2 = change_vec ? (S n) t1 (tape_move alpha (nth i ? t1 (niltape ?)) D) i.
+   
+lemma sem_move_multi :
+  ∀alpha,n,i,D.i ≤ n → 
+  mmove i alpha n D ⊨ Rm_multi alpha n i D.
+#alpha #n #i #D #Hin #int %{2}
+%{(mk_mconfig ? mmove_states n mmove1 ?)} 
+[| %
+ [ whd in ⊢ (??%?); @eq_f whd in ⊢ (??%?); @eq_f %
+ | whd >tape_move_multi_def
+   <(change_vec_same … (ctapes …) i (niltape ?))
+   >pmap_change <tape_move_multi_def >tape_move_null_action % ] ]
+ qed.
+
+(* simple copy with no move *)
+definition copy_states ≝ initN 3.
+
+definition cc0 : copy_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 3 (refl …)).
+definition cc1 : copy_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 3 (refl …)).
+
+definition trans_copy_char_N ≝ 
+ λsrc,dst.λsig:FinSet.λn.
+ λp:copy_states × (Vector (option sig) (S n)).
+ let 〈q,a〉 ≝ p in
+ match pi1 … q with
+ [ O ⇒ 〈cc1,change_vec ? (S n) 
+           (change_vec ? (S n) (null_action ? n) (〈None ?,N〉) src)
+           (〈nth src ? a (None ?),N〉) dst〉
+ | S _ ⇒ 〈cc1,null_action ? n〉 ].
+
+definition copy_char_N ≝ 
+  λsrc,dst,sig,n.
+  mk_mTM sig n copy_states (trans_copy_char_N src dst sig n) 
+    cc0 (λq.q == cc1).
+
+definition R_copy_char_N ≝ 
+  λsrc,dst,sig,n.λint,outt: Vector (tape sig) (S n).
+  outt = change_vec ?? int
+          (tape_write  ? (nth dst ? int (niltape ?))
+            (current ? (nth src ? int (niltape ?)))) dst.
+
+lemma copy_char_N_q0_q1 :
+  ∀src,dst,sig,n,v.src ≠ dst → src < S n → dst < S n → 
+  step sig n (copy_char_N src dst sig n) (mk_mconfig ??? cc0 v) =
+    mk_mconfig ??? cc1 
+     (change_vec ?? v
+       (tape_write  ? (nth dst ? v (niltape ?))
+          (current ? (nth src ? v (niltape ?)))) dst).
+#src #dst #sig #n #v #Heq #Hsrc #Hdst
+whd in ⊢ (??%?); @eq_f
+<(change_vec_same … v dst (niltape ?)) in ⊢ (??%?);
+<(change_vec_same … v src (niltape ?)) in ⊢ (??%?);
+>tape_move_multi_def
+>pmap_change >pmap_change <tape_move_multi_def
+>tape_move_null_action @eq_f3 //
+[ >change_vec_same %
+| >change_vec_same >change_vec_same >nth_current_chars // ]
+qed.
+
+lemma sem_copy_char_N:
+  ∀src,dst,sig,n.src ≠ dst → src < S n → dst < S n → 
+  copy_char_N src dst sig n ⊨ R_copy_char_N src dst sig n.
+#src #dst #sig #n #Hneq #Hsrc #Hdst #int
+%{2} % [| % [ % | whd >copy_char_N_q0_q1 // ]]
+qed.
+
+(**************** copy and advance  ***********************)
+definition copy_char_states ≝ initN 3.
+
+definition trans_copy_char ≝ 
+ λsrc,dst.λsig:FinSet.λn.
+ λp:copy_char_states × (Vector (option sig) (S n)).
+ let 〈q,a〉 ≝ p in
+ match pi1 … q with
+ [ O ⇒ 〈cc1,change_vec ? (S n) 
+           (change_vec ? (S n) (null_action ? n) (〈None ?,R〉) src)
+           (〈nth src ? a (None ?),R〉) dst〉
+ | S _ ⇒ 〈cc1,null_action ? n〉 ].
+
+definition copy_char ≝ 
+  λsrc,dst,sig,n.
+  mk_mTM sig n copy_char_states (trans_copy_char src dst sig n) 
+    cc0 (λq.q == cc1).
+
+definition R_copy_char ≝ 
+  λsrc,dst,sig,n.λint,outt: Vector (tape sig) (S n).
+  outt = change_vec ?? 
+         (change_vec ?? int
+          (tape_move_mono ? (nth src ? int (niltape ?)) 〈None ?, R〉) src)
+          (tape_move_mono ? (nth dst ? int (niltape ?)) 
+           〈current ? (nth src ? int (niltape ?)), R〉) dst.
+
+lemma copy_char_q0_q1 :
+  ∀src,dst,sig,n,v.src ≠ dst → src < S n → dst < S n → 
+  step sig n (copy_char src dst sig n) (mk_mconfig ??? cc0 v) =
+    mk_mconfig ??? cc1 
+     (change_vec ? (S n) 
+       (change_vec ?? v
+         (tape_move_mono ? (nth src ? v (niltape ?)) 〈None ?, R〉) src)
+            (tape_move_mono ? (nth dst ? v (niltape ?)) 〈current ? (nth src ? v (niltape ?)), R〉) dst).
+#src #dst #sig #n #v #Heq #Hsrc #Hdst
+whd in ⊢ (??%?);
+<(change_vec_same … v dst (niltape ?)) in ⊢ (??%?);
+<(change_vec_same … v src (niltape ?)) in ⊢ (??%?);
+>tape_move_multi_def @eq_f2 //
+>pmap_change >pmap_change <tape_move_multi_def
+>tape_move_null_action @eq_f2 // @eq_f2
+[ >change_vec_same %
+| >change_vec_same >change_vec_same // ]
+qed.
+
+lemma sem_copy_char:
+  ∀src,dst,sig,n.src ≠ dst → src < S n → dst < S n → 
+  copy_char src dst sig n ⊨ R_copy_char src dst sig n.
+#src #dst #sig #n #Hneq #Hsrc #Hdst #int
+%{2} % [| % [ % | whd >copy_char_q0_q1 // ]]
+qed.
+
+
 
 (********************** look_ahead test *************************)