converting certain basic machines to composed machines

diff --git a/matita/matita/lib/turing/multi_universal/moves_2.ma b/matita/matita/lib/turing/multi_universal/moves_2.ma
index e56a0f183e434fe96c09a9402e3f982ad631b32b..a904414fafbfeb475d55f90dbbfc8b8743f494e1 100644 (file)
--- a/matita/matita/lib/turing/multi_universal/moves_2.ma
+++ b/matita/matita/lib/turing/multi_universal/moves_2.ma
@@ -13,6 +13,8 @@ include "turing/turing.ma".
 include "turing/inject.ma".
 include "turing/while_multi.ma".
 include "turing/while_machine.ma".
+include "turing/simple_machines.ma".
+include "turing/if_machine.ma".
 
 definition parmove_states ≝ initN 3.
 
@@ -311,22 +313,10 @@ qed.
         else nop
      }
  *)
- 
-definition mte_states ≝ initN 3.
-definition mte0 : mte_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 3 (refl …)).
-definition mte1 : mte_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 3 (refl …)).
-definition mte2 : mte_states ≝ mk_Sig ?? 2 (leb_true_to_le 3 3 (refl …)).
 
-definition mte_step ≝ 
-  λalpha:FinSet.λD.mk_TM alpha mte_states
-  (λp.let 〈q,a〉 ≝ p in
-    match a with
-    [ None ⇒ 〈mte1,None ?,N〉
-    | Some a' ⇒ match (pi1 … q) with
-      [ O ⇒ 〈mte2,Some ? a',D〉
-      | S q ⇒ 〈mte2,None ?,N〉 ] ])
-  mte0 (λq.q == mte1 ∨ q == mte2).
-  
+definition mte_step ≝ λalpha,D.
+ifTM ? (test_null alpha) (single_finalTM ? (move alpha D)) (nop ?) tc_true.
+ 
 definition R_mte_step_true ≝ λalpha,D,t1,t2.
   ∃ls,c,rs.
     t1 = midtape alpha ls c rs ∧ t2 = tape_move ? t1 D.
@@ -334,21 +324,25 @@ definition R_mte_step_true ≝ λalpha,D,t1,t2.
 definition R_mte_step_false ≝ λalpha.λt1,t2:tape alpha.
   current ? t1 = None ? ∧ t1 = t2.
 
+definition mte2 : ∀alpha,D.states ? (mte_step alpha D) ≝ 
+λalpha,D.(inr … (inl … (inr … start_nop))).
+  
 lemma sem_mte_step :
-  ∀alpha,D.mte_step alpha D ⊨ [ mte2 : R_mte_step_true alpha D, R_mte_step_false alpha ] .
-#alpha #D #intape @(ex_intro ?? 2) cases intape
-[ @ex_intro
-  [| % [ % [ % | normalize #H destruct ] | #_ % // ] ]
-|#a #al @ex_intro
-  [| % [ % [ % | normalize #H destruct ] | #_ % // ] ]
-|#a #al @ex_intro
-  [| % [ % [ % | normalize #H destruct ] | #_ % // ] ]
-| #ls #c #rs
-  @ex_intro [| % [ % [ % | #_ %{ls} %{c} %{rs} % // ]
-                     | normalize in ⊢ (?(??%?)→?); * #H @False_ind /2/ ] ] ]
+  ∀alpha,D.mte_step alpha D ⊨ 
+   [ mte2 … : R_mte_step_true alpha D, R_mte_step_false alpha ] .
+#alpha #D #ta
+@(acc_sem_if_app ??????????? (sem_test_null …) 
+  (sem_move_single …) (sem_nop alpha) ??)
+[ #tb #tc #td * #Hcurtb
+  lapply (refl ? (current ? tb)) cases (current ? tb) in ⊢ (???%→?);
+  [ #H @False_ind >H in Hcurtb; * /2/ ]
+  -Hcurtb #c #Hcurtb #Htb whd in ⊢ (%→?); #Htc whd
+  cases (current_to_midtape … Hcurtb) #ls * #rs #Hmidtb 
+  %{ls} %{c} %{rs} % //
+| #tb #tc #td * #Hcurtb #Htb whd in ⊢ (%→?); #Htc whd % // ]
 qed.
 
-definition move_to_end ≝ λsig,D.whileTM sig (mte_step sig D) mte2.
+definition move_to_end ≝ λsig,D.whileTM sig (mte_step sig D) (mte2 …).
 
 definition R_move_to_end_r ≝ 
   λsig,int,outt.

diff --git a/matita/matita/lib/turing/simple_machines.ma b/matita/matita/lib/turing/simple_machines.ma
index 4b51989000dafecac35ab0bbaf14cea2b43e05aa..2cfaf7c7acbef0ce8f3ac2abe290fa07f1e63138 100644 (file)
--- a/matita/matita/lib/turing/simple_machines.ma
+++ b/matita/matita/lib/turing/simple_machines.ma
@@ -67,39 +67,46 @@ cases (acc_sem_inject … Hin (sem_test_null alpha) int)
   | @(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 smove_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 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_mmove ≝ 
- λi,sig,n,D.
- λp:mmove_states × (Vector (option sig) (S n)).
+definition trans_smove ≝ 
+ λsig,D.
+ λp:smove_states × (option sig).
  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〉 ].
+ [ 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 mmove ≝ λi,sig,n,D.inject_TM sig (move sig D) n i.
+
+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.
 
-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.
+#alpha #n #i #D #Hin #ta cases (sem_inject … Hin (sem_move_single alpha D) ta)
+#k * #outc * #Hloop * whd in ⊢ (%→?); #Htb1 #Htb2 %{k} %{outc} % [ @Hloop ]
+whd @(eq_vec … (niltape ?)) #i0 #Hi0 cases (decidable_eq_nat i0 i) #Hi0i
+[ >Hi0i >Htb1 >nth_change_vec //
+| >nth_change_vec_neq [|@sym_not_eq //] <Htb2 // @sym_not_eq // ]
+qed.
 
 (* simple copy with no move *)
 definition copy_states ≝ initN 3.