From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Mon, 30 Apr 2012 09:29:09 +0000 (+0000)
Subject: Definition of accRealize
X-Git-Tag: make_still_working~1791
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=100184e7920cc3c70b50b694a17fa40ecde45e77;p=helm.git

Definition of accRealize
---

diff --git a/matita/matita/lib/turing/if_machine.ma b/matita/matita/lib/turing/if_machine.ma
index 592c90947..0fe4a4f11 100644
--- a/matita/matita/lib/turing/if_machine.ma
+++ b/matita/matita/lib/turing/if_machine.ma
@@ -41,10 +41,9 @@ definition ifTM ≝ λsig. λcondM,thenM,elseM : TM sig.
         [ inl s2 ⇒ halt sig thenM s2
         | inr s3 ⇒ halt sig elseM s3 ]]). 
 
-theorem sem_seq: ∀sig,M1,M2,M3,P,R2,R3,q1,q2.
-  Frealize sig M1 P → Realize sig M2 R2 → Realize sig M3 R3 → 
-    Realize sig (ifTN sig M1 M2 M2) 
-      λt1.t2. (P t1 q1 t11 → R2 t11 t2) ∨ (P t1 q2 t12 → R3 t12 t2).
+theorem sem_if: ∀sig,M1,M2,M3,Rtrue,Rfalse,R2,R3,acc.
+  accRealize sig M1 acc Rtrue Rfalse → Realize sig M2 R2 → Realize sig M3 R3 → 
+    Realize sig (ifTM sig M1 M2 M3 acc) (λt1,t2. (Rtrue ∘ R2) t1 t2 ∨ (Rfalse ∘ R3) t1 t2).
 
 (* We do not distinuish an input tape *)
 
diff --git a/matita/matita/lib/turing/mono.ma b/matita/matita/lib/turing/mono.ma
index 7f261e48d..4078c4483 100644
--- a/matita/matita/lib/turing/mono.ma
+++ b/matita/matita/lib/turing/mono.ma
@@ -118,6 +118,13 @@ definition Realize ≝ λsig.λM:TM sig.λR:relation (tape sig).
   loop ? i (step sig M) (λc.halt sig M (cstate ?? c)) (initc sig M t) = Some ? outc ∧
   R t (ctape ?? outc).
 
+
+definition accRealize ≝ λsig.λM:TM sig.λacc:states sig M.λRtrue,Rfalse:relation (tape sig).
+∀t.∃i.∃outc.
+  loop ? i (step sig M) (λc.halt sig M (cstate ?? c)) (initc sig M t) = Some ? outc ∧
+  (cstate ?? outc = acc → Rtrue t (ctape ?? outc)) ∧ 
+  (cstate ?? outc ≠ acc → Rfalse t (ctape ?? outc)).
+
 (* Compositions *)
 
 definition seq_trans ≝ λsig. λM1,M2 : TM sig.