X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Flib%2Fturing%2Funiversal%2Funi_step.ma;h=1198bb9f1040286a6271dbe2d7da9c46fb93ad5e;hb=0ebe34030d5d1dbac686def6fba0e59d22c7b4b6;hp=d24dc07ba9f3bdbf2e8f4e6d463414f9109b8824;hpb=1695dd8b1861176954666067243c02020e1dcea5;p=helm.git

diff --git a/matita/matita/lib/turing/universal/uni_step.ma b/matita/matita/lib/turing/universal/uni_step.ma
index d24dc07ba..1198bb9f1 100644
--- a/matita/matita/lib/turing/universal/uni_step.ma
+++ b/matita/matita/lib/turing/universal/uni_step.ma
@@ -237,72 +237,91 @@ qed. *)
 include "turing/universal/move_tape.ma".
 
 definition exec_move ≝ 
-  seq ? (adv_to_mark_r … (is_marked ?))
-    (seq ? init_copy
-      (seq ? copy
-        (seq ? (move_r …)
-          (seq ? move_tape (move_r …))))).
-
-definition lift_tape ≝ λls,c,rs.
-  let 〈c0,b〉 ≝ c in
-  let c' ≝ match c0 with
-  [ null ⇒ None ?
-  | _ ⇒ Some ? c ]
-  in
-  mk_tape STape ls c' rs.
-  
-definition sim_current_of_tape ≝ λt.
-  match current STape t with
-  [ None ⇒ 〈null,false〉
-  | Some c0 ⇒ c0 ].
-
-(*
- t1 =  ls # cs c # table # rs  
- 
- let simt ≝ lift_tape ls c rs in
- let simt' ≝ move_left simt' in
- 
- t2 = left simt'# cs (sim_current_of_tape simt') # table # right simt'
-*)
-          
-(*
-definition R_move
+  seq ? init_copy
+    (seq ? copy
+      (seq ? (move_r …) move_tape)).
 
 definition R_exec_move ≝ λt1,t2.
-  ∀ls,current,table1,newcurrent,table2,rs.
-  t1 = midtape STape (current@〈grid,false〉::ls) 〈grid,false〉
-       (table1@〈comma,true〉::newcurrent@〈comma,false〉::move::table2@
-        〈grid,false〉::rs) → 
-  table_TM (table1@〈comma,false〉::newcurrent@〈comma,false〉::move::table2) →
-  t2 = midtape
-*)
-
-(*
-
-step :
-
-if is_true(current) (* current state is final *)
-   then nop
-   else 
-   init_match;
-   match_tuple;
-   if is_marked(current) = false (* match ok *)
-      then exec_move; 
-      else sink;
-        
-*)
-
-definition mk_tuple ≝ λc,newc,mv.
-  c @ 〈comma,false〉:: newc @ 〈comma,false〉 :: [〈mv,false〉].
+  ∀n,curconfig,ls,rs,c0,c1,s0,s1,table1,newconfig,mv,table2.
+  table_TM n (table1@〈comma,false〉::〈s1,false〉::newconfig@〈c1,false〉::〈comma,false〉::〈mv,false〉::table2) → 
+  no_marks curconfig → only_bits (curconfig@[〈s0,false〉]) → only_bits (〈s1,false〉::newconfig) → 
+  no_nulls ls → no_nulls rs → 
+  t1 = midtape STape (〈c0,false〉::curconfig@〈s0,false〉::〈grid,false〉::ls) 〈grid,false〉 
+    (table1@〈comma,true〉::〈s1,false〉::newconfig@〈c1,false〉::〈comma,false〉::〈mv,false〉::table2@〈grid,false〉::rs) → 
+  ∀t1'.t1' = lift_tape ls 〈c0,false〉 rs → 
+  ∃ls1,rs1,c2.
+  t2 = midtape STape ls1 〈grid,false〉 
+    (〈s1,false〉::newconfig@〈c2,false〉::〈grid,false〉::
+     table1@〈comma,false〉::〈s1,false〉::newconfig@〈c1,false〉::〈comma,false〉::〈mv,false〉::table2@〈grid,false〉::rs1) ∧   
+  lift_tape ls1 〈c2,false〉 rs1 = 
+  tape_move STape t1' (Some ? 〈〈c2,false〉,move_of_unialpha mv〉).
+  
+lemma sem_exec_move : Realize ? exec_move R_exec_move.
+#intape
+cases (sem_seq … sem_init_copy
+        (sem_seq … sem_copy
+          (sem_seq … (sem_move_r …) sem_move_tape )) intape)
+#k * #outc * #Hloop #HR
+@(ex_intro ?? k) @(ex_intro ?? outc) % [ @Hloop ] -Hloop
+#n #curconfig #ls #rs #c0 #c1 #s0 #s1 #table1 #newconfig #mv #table2
+#Htable #Hcurconfig1 #Hcurconfig2 #Hnewconfig #Hls #Hrs #Hintape #t1' #Ht1'
+cases HR -HR #ta * whd in ⊢ (%→?); #Hta
+lapply (Hta (〈c0,false〉::curconfig) table1 s0 ls s1
+        (newconfig@〈c1,false〉::〈comma,false〉::〈mv,false〉::table2@〈grid,false〉::rs) … Hintape) -Hta
+[ (*Hcurconfig2*) @daemon
+| (*Htable*) @daemon
+| (*FIXME*) @daemon
+| (*FIXME*) @daemon
+| #Hta * #tb * whd in ⊢ (%→?); #Htb
+  lapply (Htb (〈grid,false〉::ls) s0 s1 c0 c1 (〈mv,false〉::table2@〈grid,false〉::rs) newconfig (〈comma,false〉::reverse ? table1) curconfig Hta ????????) -Htb
+  [9:|*:(* rivedere le precondizioni *) @daemon ]
+  #Htb * #tc * whd in ⊢ (%→?); #Htc lapply (Htc … Htb) -Htc whd in ⊢(???(??%%%)→?);#Htc
+  whd in ⊢ (%→?); #Houtc whd in Htc:(???%); whd in Htc:(???(??%%%));
+  lapply (Houtc rs n 
+    (〈comma,false〉::〈s1,false〉::reverse ? newconfig@@〈comma,false〉::reverse ? table1)
+    mv table2 (merge_char curc d1) (merge_config curconfig (reverse ? newconfig1)) ls ????? 
+    Hls Hrs ??)
+  [3: >Htc @(eq_f3 … (midtape ?))
+    [ @eq_f >associative_append >Hnewconfig
+      >reverse_cons >associative_append @eq_f
+      whd in ⊢ (???%); @eq_f whd in ⊢ (???%); @eq_f
+      <Heqcurconfig <reverse_cons >Hnewconfig1 >reverse_append
+      >merge_cons %
+    | %
+    | % ]
+  | %
+  || >reverse_cons >reverse_append >reverse_reverse >reverse_cons
+     >reverse_reverse 
+     >associative_append >associative_append >associative_append
+     normalize @Htable
+  | (* only bits or nulls c1,c2 → only bits or nulls (merge c1 c2) *) @daemon
+  | (* add to hyps? *) @daemon
+  | (* bit_or_null c1,c2 → bit_or_null (merge_char c1 c2) *) @daemon
+  | -Houtc * #ls1 * #rs1 * #newc * #Houtc *
+    [ *
+      [ * #Hmv #Htapemove
+        @(ex_intro ?? ls1) @(ex_intro ?? rs1) @(ex_intro ?? (\fst newc))
+        %
+        [ >Houtc >reverse_merge_config [| @daemon ]
+          >reverse_reverse @eq_f
+          >reverse_cons >reverse_append >reverse_cons
+          >reverse_reverse >reverse_reverse
+          @daemon
+        | >Hmv >Ht1' whd in Htapemove:(???%); whd in ⊢ (???%);
+          whd in match (lift_tape ???) in ⊢ (???%);
+          >Htapemove
+    
+    
+  
+   >Heqcurconfig
+>append_cons in Hintape; >associative_append
+cases (Hta 
 
-inductive match_in_table (c,newc:list STape) (mv:unialpha) : list STape → Prop ≝ 
-| mit_hd : 
-   ∀tb.
-   match_in_table c newc mv (mk_tuple c newc mv@〈bar,false〉::tb)
-| mit_tl :
-   ∀c0,newc0,mv0,tb.
-   match_in_table c newc mv tb → 
-   match_in_table c newc mv (mk_tuple c0 newc0 mv0@〈bar,false〉::tb).
+ cases (Hta … Hintape) -Hta
+[ * normalize in ⊢ (%→?); #Hfalse destruct (Hfalse) ]
+* #_ #Hta lapply (Hta ? 〈comma,true〉 … (refl ??) (refl ??) ?)
+[ @daemon ] -Hta #Hta
+* #tb * whd in ⊢ (%→?); #Htb lapply (Htb … Hta)
 
 definition move_of_unialpha ≝ 
   λc.match c with
@@ -325,43 +344,3 @@ definition R_uni_step ≝ λt1,t2.
 definition no_nulls ≝ 
  λl:list STape.∀x.memb ? x l = true → is_null (\fst x) = false.
  
-definition R_move_tape_r_abstract ≝ λt1,t2.
-  ∀rs,n,table,curc,curconfig,ls.
-  bit_or_null curc = true → only_bits_or_nulls curconfig → table_TM n table → 
-  t1 = midtape STape (table@〈grid,false〉::〈curc,false〉::curconfig@〈grid,false〉::ls) 
-         〈grid,false〉 rs →
-  no_nulls rs → 
-  ∀t1'.t1' = lift_tape ls 〈curc,false〉 rs → 
-  ∃ls1,rs1,newc.
-  (t2 = midtape STape ls1 〈grid,false〉 (reverse ? curconfig@newc::
-    〈grid,false〉::reverse ? table@〈grid,false〉::rs1) ∧
-   lift_tape ls1 newc rs1 = 
-   tape_move_right STape ls 〈curc,false〉 rs).
-   
-lemma lift_tape_not_null :
-  ∀ls,c,rs. is_null (\fst c) = false → 
-  lift_tape ls c rs = mk_tape STape ls (Some ? c) rs.
-#ls * #c0 #bc0 #rs cases c0
-[|normalize in ⊢ (%→?); #Hfalse destruct (Hfalse) ]
-//
-qed.
- 
-lemma mtr_concrete_to_abstract :
-  ∀t1,t2.R_move_tape_r t1 t2 → R_move_tape_r_abstract t1 t2.
-#t1 #t2 whd in ⊢(%→?); #Hconcrete
-#rs #n #table #curc #curconfig #ls #Hcurc #Hcurconfig #Htable #Ht1
-#Hrsnonulls #t1' #Ht1'
-cases (Hconcrete … Htable Ht1) //
-[ * #Hrs #Ht2
-  @(ex_intro ?? (〈curc,false〉::ls)) @(ex_intro ?? [])
-  @(ex_intro ?? 〈null,false〉) %
-  [ >Ht2 %
-  | >Hrs % ]
-| * #r0 * #rs0 * #Hrs #Ht2 
-  @(ex_intro ?? (〈curc,false〉::ls)) @(ex_intro ?? rs0)
-  @(ex_intro ?? r0) %
-  [ >Ht2 %
-  | >Hrs >lift_tape_not_null
-    [ %
-    | @Hrsnonulls >Hrs @memb_hd ] ]
-qed.
\ No newline at end of file