2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department of the University of Bologna, Italy.
8 \ / This file is distributed under the terms of the
9 \ / GNU General Public License Version 2
10 V_____________________________________________________________*)
12 include "turing/mono.ma".
14 definition single_finalTM ≝
15 λsig.λM:TM sig.seq ? M (nop ?).
17 lemma sem_single_final :
18 ∀sig,M,R.Realize ? M R → Realize ? (single_finalTM sig M) R.
19 #sig #M #R #HR #intape
20 cases (sem_seq ????? HR (sem_nop …) intape)
21 #k * #outc * #Hloop * #ta * #Hta whd in ⊢ (%→?); #Houtc
22 @(ex_intro ?? k) @(ex_intro ?? outc) % [ @Hloop | >Houtc // ]
25 definition if_trans ≝ λsig. λM1,M2,M3 : TM sig. λq:states sig M1.
29 if halt sig M1 s1 then
30 if s1==q then 〈inr … (inl … (start sig M2)), None ?〉
31 else 〈inr … (inr … (start sig M3)), None ?〉
32 else let 〈news1,m〉 ≝ trans sig M1 〈s1,a〉 in
36 [ inl s2 ⇒ let 〈news2,m〉 ≝ trans sig M2 〈s2,a〉 in
37 〈inr … (inl … news2),m〉
38 | inr s3 ⇒ let 〈news3,m〉 ≝ trans sig M3 〈s3,a〉 in
39 〈inr … (inr … news3),m〉
43 definition ifTM ≝ λsig. λcondM,thenM,elseM : TM sig.
44 λqacc: states sig condM.
46 (FinSum (states sig condM) (FinSum (states sig thenM) (states sig elseM)))
47 (if_trans sig condM thenM elseM qacc)
48 (inl … (start sig condM))
51 | inr s' ⇒ match s' with
52 [ inl s2 ⇒ halt sig thenM s2
53 | inr s3 ⇒ halt sig elseM s3 ]]).
55 axiom daemon : ∀X:Prop.X.
56 axiom tdaemon : ∀X:Type[0].X.
58 axiom sem_if: ∀sig,M1,M2,M3,Rtrue,Rfalse,R2,R3,acc.
59 accRealize sig M1 acc Rtrue Rfalse → Realize sig M2 R2 → Realize sig M3 R3 →
60 Realize sig (ifTM sig M1 M2 M3 acc) (λt1,t2. (Rtrue ∘ R2) t1 t2 ∨ (Rfalse ∘ R3) t1 t2).
62 #sig #M1 #M2 #M3 #Rtrue #Rfalse #R2 #R3 #acc #HaccR #HR2 #HR3 #t
63 cases (HaccR t) #k1 * #outc1 * * #Hloop1 #HMtrue #HMfalse
64 cases (true_or_false (cstate ?? outc1 == acc)) #Hacc
65 [cases (HR2 (ctape sig ? outc1)) #k2 * #outc2 * #Hloop2 #HM2
66 @(ex_intro … (k1+k2)) @(ex_intro … (lift_confR … (lift_confL … outc2)))
68 [@(loop_merge ???????????
70 (lift_confL sig (states ? M1) (FinSum (states ? M2) (states ? M3)))
71 (step sig M1) (step sig (ifTM sig M1 M2 M3 acc))
72 (λc.halt sig M1 (cstate … c))
73 (λc.halt_liftL ?? (halt sig M1) (cstate … c))
76 [ #sl #tl whd in ⊢ (??%? → ?); #Hl %
77 | #sr #tr whd in ⊢ (??%? → ?); #Hr destruct (Hr) ]
78 || #c0 #Hhalt @daemon (* <step_lift_confL // *)
80 |6:cases outc1 #s1 #t1 %
81 |7:@(loop_lift … (initc ?? (ctape … outc1)) … Hloop2)
83 | #c0 #Hhalt @daemon (* <step_lift_confR // *) ]
84 |whd in ⊢ (??(???%)?);whd in ⊢ (??%?);
85 generalize in match Hloop1; cases outc1 #sc1 #tc1 #Hloop10
86 >(trans_liftL_true sig M1 M2 ??)
87 [ whd in ⊢ (??%?); whd in ⊢ (???%);
89 (* @config_eq whd in ⊢ (???%); // *)
90 | @(loop_Some ?????? Hloop10)
95 |4:cases outc1 #s1 #t1 %
98 @(loop_liftR … Hloop2)
99 |whd in ⊢ (??(???%)?);whd in ⊢ (??%?);
100 generalize in match Hloop1; cases outc1 #sc1 #tc1 #Hloop10
101 >(trans_liftL_true sig M1 M2 ??)
102 [ whd in ⊢ (??%?); whd in ⊢ (???%);
104 | @(loop_Some ?????? Hloop10) ]
106 | @(ex_intro … (ctape ? (seq sig M1 M2) (lift_confL … outc1)))