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/simple_machines.ma".
13 include "turing/multi_universal/unistep_aux.ma".
15 axiom sem_unistep: ∀M. unistep ⊨ R_unistep_high M.
18 match c with [ bit b ⇒ notb b | _ ⇒ true].
21 ifTM ?? (mtestR ? cfg 2 stop)
22 (single_finalTM ?? unistep)
23 (nop …) (mtestR_acc ? cfg 2 stop).
25 definition acc_body : states ?? uni_body ≝ (inr … (inl … (inr … start_nop))).
27 definition ub_R_true ≝ λM,t1,t2.
28 ∀c: nconfig (no_states M).
30 t2=low_tapes M (step FinBool M c) ∧ halt ? M (cstate … c) = false.
32 definition ub_R_false ≝ λM,t1,t2.
33 ∀c: nconfig (no_states M).
34 t1 = low_tapes M c → t1 = t2 ∧ halt ? M (cstate … c) = true.
36 lemma sem_uni_body: ∀M.
37 uni_body ⊨ [acc_body: ub_R_true M, ub_R_false M].
39 @(acc_sem_if_app ????????????
40 (sem_mtestR ? cfg 2 stop (le_S ?? (le_n 1)))
43 [#t1 #t2 #t3 whd in ⊢ (%→?); #Htest #Ht2 * #q #Mt #Ht1
44 >Ht1 in Htest; >cfg_low_tapes whd in match (bits_of_state ???);
45 #Htest lapply (Htest … (refl ??)) * <Ht1 #Ht3 #Hstop >Ht3 in Ht2;
46 #Ht2 % [@Ht2 //] lapply Hstop whd in match (nhalt ??);
47 cases (nhalt M q) whd in match (stop ?); * /2/
48 |#t1 #t2 #t3 whd in ⊢ (%→?); #Htest #Hnop >Hnop -Hnop * #q #Mt #Ht1 >Ht1 in Htest;
49 >cfg_low_tapes whd in match (bits_of_state ???);
50 #Htest lapply (Htest … (refl ??)) whd in match (nhalt ??);
51 cases (nhalt M q) whd in match (stop ?); * /2/
55 definition universalTM ≝ whileTM ?? uni_body acc_body.
57 definition low_R ≝ λM,q,R.λt1,t2:Vector (tape FSUnialpha) 3.
58 ∀Mt. t1 = low_tapes M (mk_config ?? q Mt) →
59 ∃cout. R Mt (ctape … cout) ∧
60 halt ? M (cstate … cout) = true ∧ t2 = low_tapes M cout.
62 theorem sem_universal: ∀M:normalTM. ∀q.
63 universalTM ⊫ low_R M q (R_TM FinBool M q).
64 #M #q #intape #i #outc #Hloop
65 lapply (sem_while … (sem_uni_body M … ) intape i outc Hloop) [%] -Hloop
66 * #ta * #Hstar lapply q -q @(star_ind_l ??????? Hstar) -Hstar
67 [#q whd in ⊢ (%→?); #HFalse whd #Mt #Hta
68 lapply (HFalse … Hta) * #Hta1 #Hhalt %{(mk_config ?? q Mt)} %
69 [%[%{1} %{(mk_config ?? q Mt)} % // whd in ⊢ (??%?); >Hhalt % |@Hhalt]
72 |#t1 #t2 whd in ⊢ (%→?); #Hstep #Hstar #IH #q #Hta whd #Mt #Ht1
73 lapply (Hstep … Ht1) * -Hstep #Ht2 #Hhalt
74 lapply(IH (cstate … (step FinBool M (mk_config ?? q Mt))) Hta ??) [@Ht2|skip] -IH
75 * #cout * * #HRTM #Hhalt1 #Houtc
77 %[%[cases HRTM #k * #outc1 * <config_expand #Hloop #Houtc1
79 [whd in ⊢ (??%?); >Hhalt whd in ⊢ (??%?); @Hloop
88 theorem sem_universal2: ∀M:normalTM. ∀R.
89 M ⊫ R → universalTM ⊫ (low_R M (start ? M) R).
90 #M #R #HMR lapply (sem_universal … M (start ? M)) @WRealize_to_WRealize
91 #t1 #t2 whd in ⊢ (%→%); #H #tape1 #Htape1 cases (H ? Htape1)
92 #c * * #HRTM #Hhalt #Ht2 %{c}
93 % [% [@(R_TM_to_R … HRTM) @HMR | //] | //]
99 lemma halting_case: ∀M:normalTM.∀t,q. halt ? M q = true →
100 universalTM↓low_tapes M (mk_config ?? q t).
102 @(terminate_while ?? uni_body ????? (sem_uni_body … M)) [%]
103 % #ta whd in ⊢ (%→?); #H cases (H … (refl ??)) #_ >Hhalt
104 #Habs destruct (Habs)
107 theorem terminate_UTM: ∀M:normalTM.∀t.
108 M ↓ t → universalTM ↓ (low_tapes M (mk_config ?? (start ? M) t)).
109 #M #t #H @(terminate_while ?? uni_body ????? (sem_uni_body … M)) [%]
110 lapply H -H * #x (* we need to generalize to an arbitrary initial configuration *)
111 whd in match (initc ? M t); generalize in match (start ? M); lapply t -t
113 [#t #q * #outc whd in ⊢ (??%?→?); #Habs destruct
114 |#n #Hind #t #q cases (true_or_false (halt ? M q)) #Hhaltq
115 [* #outc whd in ⊢ (??%?→?); >Hhaltq whd in ⊢ (??%?→?); #HSome destruct (HSome)
116 % #ta whd in ⊢ (%→?); #H cases (H … (refl ??)) #_ >Hhaltq
117 #Habs destruct (Habs)
118 |* #outc whd in ⊢ (??%?→?); >Hhaltq whd in ⊢ (??%?→?); #Hloop
119 % #t1 whd in ⊢ (%→?); #Hstep lapply (Hstep … (refl ??)) *
120 #Ht1 #_ >Ht1 @Hind %{outc} <config_expand @Hloop