X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fturing%2Funiversal%2Fmove_char_c.ma;h=6e601ad2bdc8c1dea6764916676df073e231b706;hb=0460fd3dc2909efe0baa6592281d0cf0527165ff;hp=6bd3cef9b9e3bd456478e677f8915609c9569bcd;hpb=70279506c9837750cccf925dc9840b0b3d9951a5;p=helm.git

diff --git a/matita/matita/lib/turing/universal/move_char_c.ma b/matita/matita/lib/turing/universal/move_char_c.ma
index 6bd3cef9b..6e601ad2b 100644
--- a/matita/matita/lib/turing/universal/move_char_c.ma
+++ b/matita/matita/lib/turing/universal/move_char_c.ma
@@ -31,69 +31,12 @@ Final state = 〈4,#〉
 
 *)
 
-include "turing/while_machine.ma".
+include "turing/basic_machines.ma".
+include "turing/if_machine.ma".
 
-definition mcc_states : FinSet → FinSet ≝ λalpha:FinSet.FinProd (initN 5) alpha.
-
-definition mcc_step ≝ 
- λalpha:FinSet.λsep:alpha.
- mk_TM alpha (mcc_states alpha)
- (λp.let 〈q,a〉 ≝ p in
-  let 〈q',b〉 ≝ q in
-  match a with 
-  [ None ⇒ 〈〈4,sep〉,None ?〉 
-  | Some a' ⇒ 
-  match q' with
-  [ O ⇒ (* qinit *)
-    match a' == sep with
-    [ true ⇒ 〈〈4,sep〉,None ?〉
-    | false ⇒ 〈〈1,a'〉,Some ? 〈a',L〉〉 ]
-  | S q' ⇒ match q' with
-    [ O ⇒ (* q1 *)
-      〈〈2,a'〉,Some ? 〈b,R〉〉
-    | S q' ⇒ match q' with
-      [ O ⇒ (* q2 *)
-        〈〈3,sep〉,Some ? 〈b,R〉〉
-      | S q' ⇒ match q' with
-        [ O ⇒ (* qacc *)
-          〈〈3,sep〉,None ?〉
-        | S q' ⇒ (* qfail *)
-          〈〈4,sep〉,None ?〉 ] ] ] ] ])
-  〈0,sep〉
-  (λq.let 〈q',a〉 ≝ q in q' == 3 ∨ q' == 4).
-
-lemma mcc_q0_q1 : 
-  ∀alpha:FinSet.∀sep,a,ls,a0,rs.
-  a0 == sep = false → 
-  step alpha (mcc_step alpha sep)
-    (mk_config ?? 〈0,a〉 (mk_tape … ls (Some ? a0) rs)) =
-  mk_config alpha (states ? (mcc_step alpha sep)) 〈1,a0〉
-    (tape_move_left alpha ls a0 rs).
-#alpha #sep #a *
-[ #a0 #rs #Ha0 whd in ⊢ (??%?); 
-  normalize in match (trans ???); >Ha0 %
-| #a1 #ls #a0 #rs #Ha0 whd in ⊢ (??%?);
-  normalize in match (trans ???); >Ha0 %
-]
-qed.
-    
-lemma mcc_q1_q2 :
-  ∀alpha:FinSet.∀sep,a,ls,a0,rs.
-  step alpha (mcc_step alpha sep) 
-    (mk_config ?? 〈1,a〉 (mk_tape … ls (Some ? a0) rs)) = 
-  mk_config alpha (states ? (mcc_step alpha sep)) 〈2,a0〉 
-    (tape_move_right alpha ls a rs).
-#alpha #sep #a #ls #a0 * //
-qed.
-
-lemma mcc_q2_q3 :
-  ∀alpha:FinSet.∀sep,a,ls,a0,rs.
-  step alpha (mcc_step alpha sep) 
-    (mk_config ?? 〈2,a〉 (mk_tape … ls (Some ? a0) rs)) = 
-  mk_config alpha (states ? (mcc_step alpha sep)) 〈3,sep〉 
-    (tape_move_right alpha ls a rs).
-#alpha #sep #a #ls #a0 * //
-qed.
+definition mcc_step ≝ λalpha:FinSet.λsep:alpha.
+  ifTM alpha (test_char ? (λc.¬c==sep))
+     (single_finalTM … (seq … (swap_r alpha sep) (move_r ?))) (nop ?) tc_true.
 
 definition Rmcc_step_true ≝ 
   λalpha,sep,t1,t2.
@@ -107,75 +50,31 @@ definition Rmcc_step_false ≝
     left ? t1 ≠ [] →  current alpha t1 ≠ None alpha → 
       current alpha t1 = Some alpha sep ∧ t2 = t1.
     
-lemma loop_S_true : 
-  ∀A,n,f,p,a.  p a = true → 
-  loop A (S n) f p a = Some ? a. /2/
-qed.
-
-lemma loop_S_false : 
-  ∀A,n,f,p,a.  p a = false → 
-  loop A (S n) f p a = loop A n f p (f a).
-normalize #A #n #f #p #a #Hpa >Hpa %
-qed.
-
-lemma trans_init_sep: 
-  ∀alpha,sep,x.
-  trans ? (mcc_step alpha sep) 〈〈0,x〉,Some ? sep〉 = 〈〈4,sep〉,None ?〉.
-#alpha #sep #x normalize >(\b ?) //
-qed.
- 
-lemma trans_init_not_sep: 
-  ∀alpha,sep,x,y.y == sep = false → 
-  trans ? (mcc_step alpha sep) 〈〈0,x〉,Some ? y〉 = 〈〈1,y〉,Some ? 〈y,L〉〉.
-#alpha #sep #x #y #H1 normalize >H1 //
-qed.
-
 lemma sem_mcc_step :
   ∀alpha,sep.
-  accRealize alpha (mcc_step alpha sep) 
-    〈3,sep〉 (Rmcc_step_true alpha sep) (Rmcc_step_false alpha sep).
-#alpha #sep *
-[@(ex_intro ?? 2)  
-  @(ex_intro … (mk_config ?? 〈4,sep〉 (niltape ?)))
-  % [% [whd in ⊢ (??%?);% |#Hfalse destruct ] |#H1 #H2 @False_ind @(absurd ?? H2) %]
-|#l0 #lt0 @(ex_intro ?? 2)  
-  @(ex_intro … (mk_config ?? 〈4,sep〉 (leftof ? l0 lt0)))
-  % [% [whd in ⊢ (??%?);% |#Hfalse destruct ] |#H1 #H2 @False_ind @(absurd ?? H2) %]
-|#r0 #rt0 @(ex_intro ?? 2)  
-  @(ex_intro … (mk_config ?? 〈4,sep〉 (rightof ? r0 rt0)))
-  % [% [whd in ⊢ (??%?);% |#Hfalse destruct ] |#H1 #H2 #H3 @False_ind @(absurd ?? H3) %]
-| #lt #c #rt cases (true_or_false (c == sep)) #Hc
-  [ @(ex_intro ?? 2) 
-    @(ex_intro ?? (mk_config ?? 〈4,sep〉 (midtape ? lt c rt)))
-    % [ % 
-        [ >(\P Hc) >loop_S_false // >loop_S_true 
-         [ @eq_f whd in ⊢ (??%?); >trans_init_sep %
-         |>(\P Hc) whd in ⊢(??(???(???%))?); >trans_init_sep % ]
-        |   #Hfalse destruct ]
-      |#_ #H1 #H2 % // normalize >(\P Hc) % ]
-  | @(ex_intro ?? 4) cases lt
-    [ @ex_intro
-      [|% [ %
-            [ >loop_S_false // >mcc_q0_q1 //
-            | normalize in ⊢ (%→?); #Hfalse destruct (Hfalse) ]
-          | normalize in ⊢ (%→?); #_ #H1 @False_ind @(absurd ?? H1) % ] ]
-    | #l0 #lt @ex_intro
-      [| % [ %
-             [ >loop_S_false // >mcc_q0_q1 //
-             | #_ #a #b #ls #rs #Hb destruct % 
-               [ @(\Pf Hc)
-               | >mcc_q1_q2 >mcc_q2_q3 cases rs normalize // ] ]
-           | normalize in ⊢ (% → ?); * #Hfalse
-             @False_ind /2/ ]
-     ]
-   ]
- ]
-]
+  mcc_step alpha sep ⊨ 
+    [inr … (inl … (inr … start_nop)): Rmcc_step_true alpha sep, Rmcc_step_false alpha sep].  
+#alpha #sep 
+  @(acc_sem_if_app … 
+     (sem_test_char …) (sem_seq …(sem_swap_r …) (sem_move_r …)) (sem_nop …))
+  [#intape #outtape #tapea whd in ⊢ (%→%→%);
+   #Htapea * #tapeb * whd in ⊢ (%→%→?);
+   #Htapeb #Houttape #a #b #ls #rs #Hintape
+   >Hintape in Htapea; #Htapea cases (Htapea ? (refl …)) -Htapea
+   #Hbsep #Htapea % [@(\Pf (injective_notb ? false Hbsep))]
+   @Houttape @Htapeb //
+  |#intape #outtape #tapea whd in ⊢ (%→%→%);
+   cases (current alpha intape) 
+    [#_ #_ #_ * #Hfalse @False_ind @Hfalse %
+    |#c #H #Htapea #_ #_ cases (H c (refl …)) #csep #Hintape % //
+     lapply (injective_notb ? true csep) -csep #csep >(\P csep) //
+    ]
+  ]
 qed.
 
 (* the move_char (variant c) machine *)
 definition move_char_c ≝ 
-  λalpha,sep.whileTM alpha (mcc_step alpha sep) 〈3,sep〉.
+  λalpha,sep.whileTM alpha (mcc_step alpha sep) (inr … (inl … (inr … start_nop))).
 
 definition R_move_char_c ≝ 
   λalpha,sep,t1,t2.
@@ -185,7 +84,7 @@ definition R_move_char_c ≝
      b ≠ sep → memb ? sep rs1 = false → 
      t2 = midtape alpha (a::reverse ? rs1@b::ls) sep rs2).
     
-lemma sem_while_move_char :
+lemma sem_move_char_c :
   ∀alpha,sep.
   WRealize alpha (move_char_c alpha sep) (R_move_char_c alpha sep).
 #alpha #sep #inc #i #outc #Hloop
@@ -193,15 +92,12 @@ lapply (sem_while … (sem_mcc_step alpha sep) inc i outc Hloop) [%]
 -Hloop * #t1 * #Hstar @(star_ind_l ??????? Hstar)
 [ #tapea whd in ⊢ (% → ?); #H1 #b #a #ls #rs #Htapea
   %
-  [ #Hb >Htapea in H1; >Hb normalize in ⊢ (%→?); #H1
-   cases (H1 ??)
-   [#_ #H2 >H2 %
-   |*: % #H2 destruct (H2) ]
+  [ #Hb >Htapea in H1; >Hb #H1 cases (H1 ??)
+    [#_ #H2 >H2 % |*: % #H2 normalize in H2; destruct (H2)]
   | #rs1 #rs2 #Hrs #Hb #Hrs1 
-    >Htapea in H1; normalize in ⊢ (% → ?); #H1
-    cases (H1 ??)
-    [ #Hfalse @False_ind @(absurd ?? Hb) destruct %
-    |*:% #H2 destruct (H2) ]
+    >Htapea in H1; #H1 cases (H1 ??)
+    [#Hfalse @False_ind @(absurd ?? Hb) normalize in Hfalse; destruct %
+    |*:% #H2 normalize in H2; destruct (H2) ]
   ]
 | #tapea #tapeb #tapec #Hstar1 #HRtrue #IH #HRfalse
   lapply (IH HRfalse) -IH whd in ⊢ (%→%); #IH
@@ -209,10 +105,9 @@ lapply (sem_while … (sem_mcc_step alpha sep) inc i outc Hloop) [%]
   #Ha0 #Htapeb %
   [ #Hfalse @False_ind @(absurd ?? Ha0) //
   | *
-    [ #rs2 whd in ⊢ (???%→?); #Hrs #_ #_ normalize
-      >Hrs in Htapeb; normalize #Htapeb
-      cases (IH … Htapeb)
-      #Houtc #_ >Houtc //
+    [ #rs2 whd in ⊢ (???%→?); #Hrs #_ #_ (* normalize *)
+      >Hrs in Htapeb; #Htapeb normalize in Htapeb;
+      cases (IH … Htapeb) #Houtc #_ >Houtc normalize // 
     | #r0 #rs0 #rs2 #Hrs #_ #Hrs0
       cut (r0 ≠ sep ∧ memb … sep rs0 = false)
       [ %
@@ -254,4 +149,10 @@ lemma terminate_move_char_c :
       [#Hb @False_ind /2/ | #Hmemb cases (orb_true_l … Hmemb)
         [#eqsep %1 >(\P eqsep) // | #H %2 //]
   ]
-qed.
\ No newline at end of file
+qed.
+
+(* NO GOOD: we must stop if current = None too!!! *)
+
+axiom ssem_move_char_c :
+  ∀alpha,sep.
+  Realize alpha (move_char_c alpha sep) (R_move_char_c alpha sep).