Progress

[helm.git] / matita / matita / lib / turing / mono.ma

diff --git a/matita/matita/lib/turing/mono.ma b/matita/matita/lib/turing/mono.ma
index cd9598765f0ba881bf5b1afd3b6d6c6a73d276ad..e89d710c948d2cf157d516e703f9c61ce76033d0 100644 (file)
--- a/matita/matita/lib/turing/mono.ma
+++ b/matita/matita/lib/turing/mono.ma
@@ -44,6 +44,16 @@ definition current ≝
  λsig.λt:tape sig.match t with
  [ midtape _ c _ ⇒ Some ? c
  | _ ⇒ None ? ].
+ 
+definition mk_tape : 
+  ∀sig:FinSet.list sig → option sig → list sig → tape sig ≝ 
+  λsig,lt,c,rt.match c with
+  [ Some c' ⇒ midtape sig lt c' rt
+  | None ⇒ match lt with 
+    [ nil ⇒ match rt with
+      [ nil ⇒ niltape ?
+      | cons r0 rs0 ⇒ leftof ? r0 rs0 ]
+    | cons l0 ls0 ⇒ rightof ? l0 ls0 ] ].
 
 inductive move : Type[0] ≝
 | L : move 
@@ -146,6 +156,18 @@ let rec loop (A:Type[0]) n (f:A→A) p a on n ≝
   | S m ⇒ if p a then (Some ? a) else loop A m f p (f a)
   ].
   
+lemma loop_S_true : 
+  ∀A,n,f,p,a.  p a = true → 
+  loop A (S n) f p a = Some ? a.
+#A #n #f #p #a #pa normalize >pa //
+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 loop_incr : ∀A,f,p,k1,k2,a1,a2. 
   loop A k1 f p a1 = Some ? a2 → 
     loop A (k2+k1) f p a1 = Some ? a2.
@@ -229,7 +251,16 @@ definition WRealize ≝ λsig.λM:TM sig.λR:relation (tape sig).
 ∀t,i,outc.
   loop ? i (step sig M) (λc.halt sig M (cstate ?? c)) (initc sig M t) = Some ? outc → 
   R t (ctape ?? outc).
-  
+
+definition Terminate ≝ λsig.λM:TM sig.λt. ∃i,outc.
+  loop ? i (step sig M) (λc.halt sig M (cstate ?? c)) (initc sig M t) = Some ? outc.
+
+lemma WRealize_to_Realize : ∀sig.∀M: TM sig.∀R.
+  (∀t.Terminate sig M t) → WRealize sig M R → Realize sig M R.
+#sig #M #R #HT #HW #t cases (HT … t) #i * #outc #Hloop 
+@(ex_intro … i) @(ex_intro … outc) % // @(HW … i) //
+qed.
+
 lemma loop_eq : ∀sig,f,q,i,j,a,x,y. 
   loop sig i f q a = Some ? x → loop sig j f q a = Some ? y → x = y.
 #sig #f #q #i #j @(nat_elim2 … i j)
@@ -253,6 +284,25 @@ definition accRealize ≝ λsig.λM:TM sig.λacc:states sig M.λRtrue,Rfalse:rel
   (cstate ?? outc = acc → Rtrue t (ctape ?? outc)) ∧ 
   (cstate ?? outc ≠ acc → Rfalse t (ctape ?? outc)).
 
+(* NO OPERATION
+
+  t1 = t2
+  *)
+  
+definition nop_states ≝ initN 1.
+
+definition nop ≝ 
+  λalpha:FinSet.mk_TM alpha nop_states
+  (λp.let 〈q,a〉 ≝ p in 〈q,None ?〉)
+  O (λ_.true).
+  
+definition R_nop ≝ λalpha.λt1,t2:tape alpha.t2 = t1.
+
+lemma sem_nop :
+  ∀alpha.Realize alpha (nop alpha) (R_nop alpha).
+#alpha #intape @(ex_intro ?? 1) @ex_intro [| % normalize % ]
+qed.
+
 (* Compositions *)
 
 definition seq_trans ≝ λsig. λM1,M2 : TM sig.