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 lemma sem_if_app: ∀sig,M1,M2,M3,Rtrue,Rfalse,R2,R3,R4,acc.
63 accRealize sig M1 acc Rtrue Rfalse → Realize sig M2 R2 → Realize sig M3 R3 →
64 (∀t1,t2,t3. (Rtrue t1 t3 ∧ R2 t3 t2) ∨ (Rfalse t1 t3 ∧ R3 t3 t2) → R4 t1 t2) →
66 (ifTM sig M1 M2 M3 acc) R4.
67 #sig #M1 #M2 #M3 #Rtrue #Rfalse #R2 #R3 #R4 #acc
68 #HRacc #HRtrue #HRfalse #Hsub
69 #t cases (sem_if … HRacc HRtrue HRfalse t)
70 #k * #outc * #Hloop #Houtc @(ex_intro … k) @(ex_intro … outc)
71 % [@Hloop] cases Houtc
72 [* #t3 * #Hleft #Hright @(Hsub … t3) %1 /2/
73 |* #t3 * #Hleft #Hright @(Hsub … t3) %2 /2/ ]
76 axiom acc_sem_if: ∀sig,M1,M2,M3,Rtrue,Rfalse,R2,R3,acc.
77 accRealize sig M1 acc Rtrue Rfalse → Realize sig M2 R2 → Realize sig M3 R3 →
79 (ifTM sig M1 (single_finalTM … M2) M3 acc)
80 (inr … (inl … (inr … start_nop)))
84 lemma acc_sem_if_app: ∀sig,M1,M2,M3,Rtrue,Rfalse,R2,R3,R4,R5,acc.
85 accRealize sig M1 acc Rtrue Rfalse → Realize sig M2 R2 → Realize sig M3 R3 →
86 (∀t1,t2,t3. Rtrue t1 t3 → R2 t3 t2 → R4 t1 t2) →
87 (∀t1,t2,t3. Rfalse t1 t3 → R3 t3 t2 → R5 t1 t2) →
89 (ifTM sig M1 (single_finalTM … M2) M3 acc)
90 (inr … (inl … (inr … start_nop)))
92 #sig #M1 #M2 #M3 #Rtrue #Rfalse #R2 #R3 #R4 #R5 #acc
93 #HRacc #HRtrue #HRfalse #Hsub1 #Hsub2
94 #t cases (acc_sem_if … HRacc HRtrue HRfalse t)
95 #k * #outc * * #Hloop #Houtc1 #Houtc2 @(ex_intro … k) @(ex_intro … outc)
97 |#H cases (Houtc1 H) #t3 * #Hleft #Hright @Hsub1 // ]
98 |#H cases (Houtc2 H) #t3 * #Hleft #Hright @Hsub2 // ]
102 #sig #M1 #M2 #M3 #Rtrue #Rfalse #R2 #R3 #acc #HaccR #HR2 #HR3 #t
103 cases (HaccR t) #k1 * #outc1 * * #Hloop1 #HMtrue #HMfalse
104 cases (true_or_false (cstate ?? outc1 == acc)) #Hacc
105 [cases (HR2 (ctape sig ? outc1)) #k2 * #outc2 * #Hloop2 #HM2
106 @(ex_intro … (k1+k2)) @(ex_intro … (lift_confR … (lift_confL … outc2)))
108 [@(loop_merge ???????????
110 (lift_confL sig (states ? M1) (FinSum (states ? M2) (states ? M3)))
111 (step sig M1) (step sig (ifTM sig M1 M2 M3 acc))
112 (λc.halt sig M1 (cstate … c))
113 (λc.halt_liftL ?? (halt sig M1) (cstate … c))
116 [ #sl #tl whd in ⊢ (??%? → ?); #Hl %
117 | #sr #tr whd in ⊢ (??%? → ?); #Hr destruct (Hr) ]
118 || #c0 #Hhalt @daemon (* <step_lift_confL // *)
120 |6:cases outc1 #s1 #t1 %
121 |7:@(loop_lift … (initc ?? (ctape … outc1)) … Hloop2)
123 | #c0 #Hhalt @daemon (* <step_lift_confR // *) ]
124 |whd in ⊢ (??(???%)?);whd in ⊢ (??%?);
125 generalize in match Hloop1; cases outc1 #sc1 #tc1 #Hloop10
126 >(trans_liftL_true sig M1 M2 ??)
127 [ whd in ⊢ (??%?); whd in ⊢ (???%);
129 (* @config_eq whd in ⊢ (???%); // *)
130 | @(loop_Some ?????? Hloop10)
135 |4:cases outc1 #s1 #t1 %
138 @(loop_liftR … Hloop2)
139 |whd in ⊢ (??(???%)?);whd in ⊢ (??%?);
140 generalize in match Hloop1; cases outc1 #sc1 #tc1 #Hloop10
141 >(trans_liftL_true sig M1 M2 ??)
142 [ whd in ⊢ (??%?); whd in ⊢ (???%);
144 | @(loop_Some ?????? Hloop10) ]
146 | @(ex_intro … (ctape ? (seq sig M1 M2) (lift_confL … outc1)))