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_____________________________________________________________*)
13 (* MOVE_CHAR RIGHT MACHINE
15 Sposta il carattere binario su cui si trova la testina appena prima del primo # alla sua destra.
18 (ls,cs,rs can be empty; # is a parameter)
30 include "turing/basic_machines.ma".
31 include "turing/if_machine.ma".
33 definition mcr_step ≝ λalpha:FinSet.λsep:alpha.
34 ifTM alpha (test_char ? (λc.¬c==sep))
35 (single_finalTM … (swap_l alpha sep · move_r ?)) (nop ?) tc_true.
37 definition Rmcr_step_true ≝
40 t1 = midtape alpha (a::ls) b rs →
42 t2 = mk_tape alpha (a::b::ls) (option_hd ? rs) (tail ? rs).
44 definition Rmcr_step_false ≝
46 left ? t1 ≠ [] → current alpha t1 ≠ None alpha →
47 current alpha t1 = Some alpha sep ∧ t2 = t1.
52 [inr … (inl … (inr … start_nop)): Rmcr_step_true alpha sep, Rmcr_step_false alpha sep].
55 (sem_test_char …) (sem_seq …(sem_swap_l …) (sem_move_r …)) (sem_nop …))
56 [#intape #outtape #tapea whd in ⊢ (%→%→%);
57 #Htapea * #tapeb * whd in ⊢ (%→%→?);
58 #Htapeb #Houttape #a #b #ls #rs #Hintape
59 >Hintape in Htapea; #Htapea cases (Htapea ? (refl …)) -Htapea
60 #Hbsep #Htapea % [@(\Pf (injective_notb ? false Hbsep))]
62 |#intape #outtape #tapea whd in ⊢ (%→%→%);
63 cases (current alpha intape)
64 [#_ #_ #_ * #Hfalse @False_ind @Hfalse %
65 |#c #H #Htapea #_ #_ cases (H c (refl …)) #csep #Hintape % //
66 lapply (injective_notb ? true csep) -csep #csep >(\P csep) //
71 (* the move_char (variant c) machine *)
72 definition move_char_r ≝
73 λalpha,sep.whileTM alpha (mcr_step alpha sep) (inr … (inl … (inr … start_nop))).
75 definition R_move_char_r ≝
77 ∀b,a,ls,rs. t1 = midtape alpha (a::ls) b rs →
79 (∀rs1,rs2.rs = rs1@sep::rs2 →
80 b ≠ sep → memb ? sep rs1 = false →
81 t2 = midtape alpha (a::reverse ? rs1@b::ls) sep rs2).
83 lemma sem_move_char_r :
85 WRealize alpha (move_char_r alpha sep) (R_move_char_r alpha sep).
86 #alpha #sep #inc #i #outc #Hloop
87 lapply (sem_while … (sem_mcr_step alpha sep) inc i outc Hloop) [%]
88 -Hloop * #t1 * #Hstar @(star_ind_l ??????? Hstar)
89 [ #tapea whd in ⊢ (% → ?); #H1 #b #a #ls #rs #Htapea
91 [ #Hb >Htapea in H1; >Hb #H1 cases (H1 ??)
92 [#_ #H2 >H2 % |*: % #H2 normalize in H2; destruct (H2)]
93 | #rs1 #rs2 #Hrs #Hb #Hrs1
94 >Htapea in H1; #H1 cases (H1 ??)
95 [#Hfalse @False_ind @(absurd ?? Hb) normalize in Hfalse; destruct %
96 |*:% #H2 normalize in H2; destruct (H2) ]
98 | #tapea #tapeb #tapec #Hstar1 #HRtrue #IH #HRfalse
99 lapply (IH HRfalse) -IH whd in ⊢ (%→%); #IH
100 #a0 #b0 #ls #rs #Htapea cases (Hstar1 … Htapea)
102 [ #Hfalse @False_ind @(absurd ?? Ha0) //
104 [ #rs2 whd in ⊢ (???%→?); #Hrs #_ #_ (* normalize *)
105 >Hrs in Htapeb; #Htapeb normalize in Htapeb;
106 cases (IH … Htapeb) #Houtc #_ >Houtc normalize //
107 | #r0 #rs0 #rs2 #Hrs #_ #Hrs0
108 cut (r0 ≠ sep ∧ memb … sep rs0 = false)
110 [ % #Hr0 >Hr0 in Hrs0; >memb_hd #Hfalse destruct
111 | whd in Hrs0:(??%?); cases (sep==r0) in Hrs0; normalize #Hfalse
116 #Hr0 -Hrs0 #Hrs0 >Hrs in Htapeb;
117 normalize in ⊢ (%→?); #Htapeb
118 cases (IH … Htapeb) -IH #_ #IH
119 >reverse_cons >associative_append @IH //
124 lemma terminate_move_char_r :
125 ∀alpha,sep.∀t,b,a,ls,rs. t = midtape alpha (a::ls) b rs →
126 (b = sep ∨ memb ? sep rs = true) → Terminate alpha (move_char_r alpha sep) t.
127 #alpha #sep #t #b #a #ls #rs #Ht #Hsep
128 @(terminate_while … (sem_mcr_step alpha sep))
130 |generalize in match Hsep; -Hsep
131 generalize in match Ht; -Ht
132 generalize in match ls; -ls
133 generalize in match a; -a
134 generalize in match b; -b
135 generalize in match t; -t
137 [#t #b #a #ls #Ht #Hsep % #tinit
138 whd in ⊢ (%→?); #H @False_ind
139 cases (H … Ht) #Hb #_ cases Hb #eqb @eqb
140 cases Hsep // whd in ⊢ ((??%?)→?); #abs destruct
141 |#r0 #rs0 #Hind #t #b #a #ls #Ht #Hsep % #tinit
143 cases (H … Ht) #Hbsep #Htinit
144 @(Hind … Htinit) cases Hsep
145 [#Hb @False_ind /2/ | #Hmemb cases (orb_true_l … Hmemb)
146 [#eqsep %1 >(\P eqsep) // | #H %2 //]
150 (* NO GOOD: we must stop if current = None too!!! *)
152 axiom ssem_move_char_r :
154 Realize alpha (move_char_r alpha sep) (R_move_char_r alpha sep).
157 (******************************* move_char_l **********************************)
158 (* MOVE_CHAR (left) MACHINE
160 Sposta il carattere binario su cui si trova la testina appena prima del primo #
164 (ls,cs,rs can be empty; # is a parameter)
171 Initial state = 〈0,#〉
176 include "turing/basic_machines.ma".
177 include "turing/if_machine.ma".
179 definition mcl_step ≝ λalpha:FinSet.λsep:alpha.
180 ifTM alpha (test_char ? (λc.¬c==sep))
181 (single_finalTM … (swap_r alpha sep · move_l ?)) (nop ?) tc_true.
183 definition Rmcl_step_true ≝
186 t1 = midtape alpha ls b (a::rs) →
188 t2 = mk_tape alpha (tail ? ls) (option_hd ? ls) (a::b::rs).
190 definition Rmcl_step_false ≝
192 right ? t1 ≠ [] → current alpha t1 ≠ None alpha →
193 current alpha t1 = Some alpha sep ∧ t2 = t1.
195 definition mcls_acc: ∀alpha:FinSet.∀sep:alpha.states ? (mcl_step alpha sep)
196 ≝ λalpha,sep.inr … (inl … (inr … start_nop)).
201 [mcls_acc alpha sep: Rmcl_step_true alpha sep, Rmcl_step_false alpha sep].
204 (sem_test_char …) (sem_seq …(sem_swap_r …) (sem_move_l …)) (sem_nop …))
205 [#intape #outtape #tapea whd in ⊢ (%→%→%);
206 #Htapea * #tapeb * whd in ⊢ (%→%→?);
207 #Htapeb #Houttape #a #b #ls #rs #Hintape
208 >Hintape in Htapea; #Htapea cases (Htapea ? (refl …)) -Htapea
209 #Hbsep #Htapea % [@(\Pf (injective_notb ? false Hbsep))]
211 |#intape #outtape #tapea whd in ⊢ (%→%→%);
212 cases (current alpha intape)
213 [#_ #_ #_ * #Hfalse @False_ind @Hfalse %
214 |#c #H #Htapea #_ #_ cases (H c (refl …)) #csep #Hintape % //
215 lapply (injective_notb ? true csep) -csep #csep >(\P csep) //
220 (* the move_char (variant left) machine *)
221 definition move_char_l ≝
222 λalpha,sep.whileTM alpha (mcl_step alpha sep) (inr … (inl … (inr … start_nop))).
224 definition R_move_char_l ≝
226 ∀b,a,ls,rs. t1 = midtape alpha ls b (a::rs) →
227 (b = sep → t2 = t1) ∧
228 (∀ls1,ls2.ls = ls1@sep::ls2 →
229 b ≠ sep → memb ? sep ls1 = false →
230 t2 = midtape alpha ls2 sep (a::reverse ? ls1@b::rs)).
232 lemma sem_move_char_l :
234 WRealize alpha (move_char_l alpha sep) (R_move_char_l alpha sep).
235 #alpha #sep #inc #i #outc #Hloop
236 lapply (sem_while … (sem_mcl_step alpha sep) inc i outc Hloop) [%]
237 -Hloop * #t1 * #Hstar @(star_ind_l ??????? Hstar)
238 [ #tapea whd in ⊢ (% → ?); #H1 #b #a #ls #rs #Htapea
240 [ #Hb >Htapea in H1; >Hb #H1 cases (H1 ??)
241 [#_ #H2 >H2 % |*: % #H2 normalize in H2; destruct (H2) ]
242 | #rs1 #rs2 #Hrs #Hb #Hrs1
243 >Htapea in H1; (* normalize in ⊢ (% → ?); *) #H1 cases (H1 ??)
244 [ #Hfalse normalize in Hfalse; @False_ind @(absurd ?? Hb) destruct %
245 |*:% normalize #H2 destruct (H2) ]
247 | #tapea #tapeb #tapec #Hstar1 #HRtrue #IH #HRfalse
248 lapply (IH HRfalse) -IH whd in ⊢ (%→%); #IH
249 #a0 #b0 #ls #rs #Htapea cases (Hstar1 … Htapea)
251 [ #Hfalse @False_ind @(absurd ?? Ha0) //
253 [ #ls2 whd in ⊢ (???%→?); #Hls #_ #_
254 >Hls in Htapeb; #Htapeb normalize in Htapeb;
255 cases (IH … Htapeb) #Houtc #_ >Houtc normalize //
256 | #l0 #ls0 #ls2 #Hls #_ #Hls0
257 cut (l0 ≠ sep ∧ memb … sep ls0 = false)
259 [ % #Hl0 >Hl0 in Hls0; >memb_hd #Hfalse destruct
260 | whd in Hls0:(??%?); cases (sep==l0) in Hls0; normalize #Hfalse
265 #Hl0 -Hls0 #Hls0 >Hls in Htapeb;
266 normalize in ⊢ (%→?); #Htapeb
267 cases (IH … Htapeb) -IH #_ #IH
268 >reverse_cons >associative_append @IH //
273 lemma terminate_move_char_l :
274 ∀alpha,sep.∀t,b,a,ls,rs. t = midtape alpha ls b (a::rs) →
275 (b = sep ∨ memb ? sep ls = true) → Terminate alpha (move_char_l alpha sep) t.
276 #alpha #sep #t #b #a #ls #rs #Ht #Hsep
277 @(terminate_while … (sem_mcl_step alpha sep))
279 |generalize in match Hsep; -Hsep
280 generalize in match Ht; -Ht
281 generalize in match rs; -rs
282 generalize in match a; -a
283 generalize in match b; -b
284 generalize in match t; -t
286 [#t #b #a #rs #Ht #Hsep % #tinit
287 whd in ⊢ (%→?); #H @False_ind
288 cases (H … Ht) #Hb #_ cases Hb #eqb @eqb
289 cases Hsep // whd in ⊢ ((??%?)→?); #abs destruct
290 |#l0 #ls0 #Hind #t #b #a #rs #Ht #Hsep % #tinit
292 cases (H … Ht) #Hbsep #Htinit
293 @(Hind … Htinit) cases Hsep
294 [#Hb @False_ind /2/ | #Hmemb cases (orb_true_l … Hmemb)
295 [#eqsep %1 >(\P eqsep) // | #H %2 //]
299 (* NO GOOD: we must stop if current = None too!!!
300 lemma ssem_move_char_l :
302 Realize alpha (move_char_l alpha sep) (R_move_char_l alpha sep).
304 [ %{5} % [| % [whd in ⊢ (??%?);
305 @WRealize_to_Realize // @terminate_move_char_l
308 axiom ssem_move_char_l :
310 Realize alpha (move_char_l alpha sep) (R_move_char_l alpha sep).