X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fturing%2Fmono.ma;h=6a006d5810fcca049c7eccc5b5395a7dabb98917;hb=d7ccf1bd91637d3c59a285df6f215ecfde2a2450;hp=bab3ab1ba067d1e1c23665fc6924def2603a176b;hpb=3f37ee83ce3c43f34d38729d192e72510f998a53;p=helm.git

diff --git a/matita/matita/lib/turing/mono.ma b/matita/matita/lib/turing/mono.ma
index bab3ab1ba..6a006d581 100644
--- a/matita/matita/lib/turing/mono.ma
+++ b/matita/matita/lib/turing/mono.ma
@@ -10,6 +10,7 @@
       V_____________________________________________________________*)
 
 include "basics/vectors.ma".
+include "basics/finset.ma".
 (* include "basics/relations.ma". *)
 
 (******************************** tape ****************************************)
@@ -47,6 +48,21 @@ definition mk_tape :
       | cons r0 rs0 ⇒ leftof ? r0 rs0 ]
     | cons l0 ls0 ⇒ rightof ? l0 ls0 ] ].
 
+lemma right_mk_tape : 
+  ∀sig,ls,c,rs.(c = None ? → ls = [ ] ∨ rs = [ ]) → right ? (mk_tape sig ls c rs) = rs.
+#sig #ls #c #rs cases c // cases ls 
+[ cases rs // 
+| #l0 #ls0 #H normalize cases (H (refl ??)) #H1 [ destruct (H1) | >H1 % ] ]
+qed-.
+
+lemma left_mk_tape : ∀sig,ls,c,rs.left ? (mk_tape sig ls c rs) = ls.
+#sig #ls #c #rs cases c // cases ls // cases rs //
+qed.
+
+lemma current_mk_tape : ∀sig,ls,c,rs.current ? (mk_tape sig ls c rs) = c.
+#sig #ls #c #rs cases c // cases ls // cases rs //
+qed.
+
 lemma current_to_midtape: ∀sig,t,c. current sig t = Some ? c →
   ∃ls,rs. t = midtape ? ls c rs.
 #sig *
@@ -134,6 +150,16 @@ definition step ≝ λsig.λM:TM sig.λc:config sig (states sig M).
   let 〈news,a,mv〉 ≝ trans sig M 〈cstate ?? c,current_char〉 in
   mk_config ?? news (tape_move sig (tape_write ? (ctape ?? c) a) mv).
 
+(*
+lemma step_eq : ∀sig,M,c. 
+  let current_char ≝ current ? (ctape ?? c) in
+  let 〈news,a,mv〉 ≝ trans sig M 〈cstate ?? c,current_char〉 in
+  step sig M c = 
+    mk_config ?? news (tape_move sig (tape_write ? (ctape ?? c) a) mv).
+#sig #M #c  
+ whd in match (tape_move_mono sig ??);
+*)
+  
 (******************************** loop ****************************************)
 let rec loop (A:Type[0]) n (f:A→A) p a on n ≝
   match n with