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_____________________________________________________________*)
17 include "turing/while_machine.ma".
19 (* ADVANCE TO MARK (right)
21 sposta la testina a destra fino a raggiungere il primo carattere marcato
25 (* 0, a ≠ mark _ ⇒ 0, R
26 0, a = mark _ ⇒ 1, N *)
28 definition atm_states ≝ initN 3.
30 definition atmr_step ≝
31 λalpha:FinSet.λtest:alpha→bool.
32 mk_TM alpha atm_states
39 | false ⇒ 〈2,Some ? 〈a',R〉〉 ]])
42 definition Ratmr_step_true ≝
45 t1 = midtape alpha ls a rs ∧ test a = false ∧
46 t2 = mk_tape alpha (a::ls) (option_hd ? rs) (tail ? rs).
48 definition Ratmr_step_false ≝
51 (current alpha t1 = None ? ∨
52 (∃a.current ? t1 = Some ? a ∧ test a = true)).
55 ∀alpha,test,ls,a0,rs. test a0 = true →
56 step alpha (atmr_step alpha test)
57 (mk_config ?? 0 (midtape … ls a0 rs)) =
58 mk_config alpha (states ? (atmr_step alpha test)) 1
60 #alpha #test #ls #a0 #ts #Htest normalize >Htest %
64 ∀alpha,test,ls,a0,rs. test a0 = false →
65 step alpha (atmr_step alpha test)
66 (mk_config ?? 0 (midtape … ls a0 rs)) =
67 mk_config alpha (states ? (atmr_step alpha test)) 2
68 (mk_tape … (a0::ls) (option_hd ? rs) (tail ? rs)).
69 #alpha #test #ls #a0 #ts #Htest normalize >Htest cases ts //
74 accRealize alpha (atmr_step alpha test)
75 2 (Ratmr_step_true alpha test) (Ratmr_step_false alpha test).
78 @(ex_intro ?? (mk_config ?? 1 (niltape ?))) %
79 [ % // #Hfalse destruct | #_ % // % % ]
80 | #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? 1 (leftof ? a al)))
81 % [ % // #Hfalse destruct | #_ % // % % ]
82 | #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? 1 (rightof ? a al)))
83 % [ % // #Hfalse destruct | #_ % // % % ]
84 | #ls #c #rs @(ex_intro ?? 2)
85 cases (true_or_false (test c)) #Htest
86 [ @(ex_intro ?? (mk_config ?? 1 ?))
89 [ whd in ⊢ (??%?); >atmr_q0_q1 //
91 | #_ % // %2 @(ex_intro ?? c) % // ]
93 | @(ex_intro ?? (mk_config ?? 2 (mk_tape ? (c::ls) (option_hd ? rs) (tail ? rs))))
96 [ whd in ⊢ (??%?); >atmr_q0_q2 //
97 | #_ @(ex_intro ?? ls) @(ex_intro ?? c) @(ex_intro ?? rs)
100 | #Hfalse @False_ind @(absurd ?? Hfalse) %
106 definition R_adv_to_mark_r ≝ λalpha,test,t1,t2.
108 (t1 = midtape alpha ls c rs →
109 ((test c = true ∧ t2 = t1) ∨
111 ∀rs1,b,rs2. rs = rs1@b::rs2 →
112 test b = true → (∀x.memb ? x rs1 = true → test x = false) →
113 t2 = midtape ? (reverse ? rs1@c::ls) b rs2))).
115 definition adv_to_mark_r ≝
116 λalpha,test.whileTM alpha (atmr_step alpha test) 2.
118 lemma sem_adv_to_mark_r :
120 WRealize alpha (adv_to_mark_r alpha test) (R_adv_to_mark_r alpha test).
121 #alpha #test #t #i #outc #Hloop
122 lapply (sem_while … (sem_atmr_step alpha test) t i outc Hloop) [%]
123 -Hloop * #t1 * #Hstar @(star_ind_l ??????? Hstar)
125 [ #H1 #ls #c #rs #H2 >H2 in H1; whd in ⊢ (??%? → ?);
126 #Hfalse destruct (Hfalse)
127 | * #a * #Ha #Htest #ls #c #rs #H2 %
128 >H2 in Ha; whd in ⊢ (??%? → ?); #Heq destruct (Heq) % //
131 | #tapea #tapeb #tapec #Hleft #Hright #IH #HRfalse
132 lapply (IH HRfalse) -IH #IH
133 #ls #c #rs #Htapea %2
134 cases Hleft #ls0 * #a0 * #rs0 * * #Htapea' #Htest #Htapeb
136 >Htapea' in Htapea; #Htapea destruct (Htapea) % // *
137 [ #b #rs2 #Hrs >Hrs in Htapeb; #Htapeb #Htestb #_
139 [ * #_ #Houtc >Houtc >Htapeb %
140 | * #Hfalse >Hfalse in Htestb; #Htestb destruct (Htestb) ]
141 | #r1 #rs1 #b #rs2 #Hrs >Hrs in Htapeb; #Htapeb #Htestb #Hmemb
143 [ * #Hfalse >(Hmemb …) in Hfalse;
144 [ #Hft destruct (Hft)
146 | * #Htestr1 #H1 >reverse_cons >associative_append
147 @H1 // #x #Hx @Hmemb @memb_cons //
152 lemma terminate_adv_to_mark_r :
154 ∀t. (* ∀b,a,ls,rs. t = midtape alpha (a::ls) b rs →
155 (b = sep ∨ memb ? sep rs = true) → *)
156 Terminate alpha (adv_to_mark_r alpha test) t.
158 @(terminate_while … (sem_atmr_step alpha test))
160 | % #t1 whd in ⊢ (% → ?); * #ls * #c * #rs
161 * * generalize in match c; generalize in match ls;
163 [ #ls #c #Ht #Hc #Ht1
164 % >Ht1 #t2 * #ls0 * #c0 * #rs0 * *
165 normalize in ⊢ (%→?); #Hfalse destruct (Hfalse)
170 [ % #a whd in ⊢ (% → ?);
172 #sep #t #b #a #ls #rs #Ht #Hsep
173 @(terminate_while … (sem_mcc_step alpha sep))
175 |generalize in match Hsep; -Hsep
176 generalize in match Ht; -Ht
177 generalize in match ls; -ls
178 generalize in match a; -a
179 generalize in match b; -b
180 generalize in match t; -t
182 [#t #b #a #ls #Ht #Hsep % #tinit
183 whd in ⊢ (%→?); #H @False_ind
184 cases (H … Ht) #Hb #_ cases Hb #eqb @eqb
185 cases Hsep // whd in ⊢ ((??%?)→?); #abs destruct
186 |#r0 #rs0 #Hind #t #b #a #ls #Ht #Hsep % #tinit
188 cases (H … Ht) #Hbsep #Htinit
189 @(Hind … Htinit) cases Hsep
190 [#Hb @False_ind /2/ | #Hmemb cases (orb_true_l … Hmemb)
191 [#eqsep %1 >(\P eqsep) // | #H %2 //]