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 (left) MACHINE
15 Sposta il carattere binario su cui si trova la testina appena prima del primo #
19 (ls,cs,rs can be empty; # is a parameter)
35 include "turing/basic_machines.ma".
36 include "turing/if_machine.ma".
38 definition mcl_step ≝ λalpha:FinSet.λsep:alpha.
39 ifTM alpha (test_char ? (λc.¬c==sep))
40 (single_finalTM … (seq … (swap alpha sep) (move_l ?))) (nop ?) tc_true.
42 definition Rmcl_step_true ≝
45 t1 = midtape alpha ls b (a::rs) →
47 t2 = mk_tape alpha (tail ? ls) (option_hd ? ls) (a::b::rs).
49 definition Rmcl_step_false ≝
51 right ? t1 ≠ [] → current alpha t1 ≠ None alpha →
52 current alpha t1 = Some alpha sep ∧ t2 = t1.
57 [inr … (inl … (inr … start_nop)): Rmcl_step_true alpha sep, Rmcl_step_false alpha sep].
60 (sem_test_char …) (sem_seq …(sem_swap …) (sem_move_l …)) (sem_nop …))
61 [#intape #outtape #tapea whd in ⊢ (%→%→%);
62 #Htapea * #tapeb * whd in ⊢ (%→%→?);
63 #Htapeb #Houttape #a #b #ls #rs #Hintape
64 >Hintape in Htapea; #Htapea cases (Htapea ? (refl …)) -Htapea
65 #Hbsep #Htapea % [@(\Pf (injective_notb ? false Hbsep))]
67 |#intape #outtape #tapea whd in ⊢ (%→%→%);
68 cases (current alpha intape)
69 [#_ #_ #_ * #Hfalse @False_ind @Hfalse %
70 |#c #H #Htapea #_ #_ cases (H c (refl …)) #csep #Hintape % //
71 lapply (injective_notb ? true csep) -csep #csep >(\P csep) //
76 (* the move_char (variant left) machine *)
77 definition move_char_l ≝
78 λalpha,sep.whileTM alpha (mcl_step alpha sep) (inr … (inl … (inr … start_nop))).
80 definition R_move_char_l ≝
82 ∀b,a,ls,rs. t1 = midtape alpha ls b (a::rs) →
84 (∀ls1,ls2.ls = ls1@sep::ls2 →
85 b ≠ sep → memb ? sep ls1 = false →
86 t2 = midtape alpha ls2 sep (a::reverse ? ls1@b::rs)).
88 lemma sem_move_char_l :
90 WRealize alpha (move_char_l alpha sep) (R_move_char_l alpha sep).
91 #alpha #sep #inc #i #outc #Hloop
92 lapply (sem_while … (sem_mcl_step alpha sep) inc i outc Hloop) [%]
93 -Hloop * #t1 * #Hstar @(star_ind_l ??????? Hstar)
94 [ #tapea whd in ⊢ (% → ?); #H1 #b #a #ls #rs #Htapea
96 [ #Hb >Htapea in H1; >Hb #H1 cases (H1 ??)
97 [#_ #H2 >H2 % |*: % #H2 normalize in H2; destruct (H2) ]
98 | #rs1 #rs2 #Hrs #Hb #Hrs1
99 >Htapea in H1; (* normalize in ⊢ (% → ?); *) #H1 cases (H1 ??)
100 [ #Hfalse normalize in Hfalse; @False_ind @(absurd ?? Hb) destruct %
101 |*:% normalize #H2 destruct (H2) ]
103 | #tapea #tapeb #tapec #Hstar1 #HRtrue #IH #HRfalse
104 lapply (IH HRfalse) -IH whd in ⊢ (%→%); #IH
105 #a0 #b0 #ls #rs #Htapea cases (Hstar1 … Htapea)
107 [ #Hfalse @False_ind @(absurd ?? Ha0) //
109 [ #ls2 whd in ⊢ (???%→?); #Hls #_ #_
110 >Hls in Htapeb; #Htapeb normalize in Htapeb;
111 cases (IH … Htapeb) #Houtc #_ >Houtc normalize //
112 | #l0 #ls0 #ls2 #Hls #_ #Hls0
113 cut (l0 ≠ sep ∧ memb … sep ls0 = false)
115 [ % #Hl0 >Hl0 in Hls0; >memb_hd #Hfalse destruct
116 | whd in Hls0:(??%?); cases (sep==l0) in Hls0; normalize #Hfalse
121 #Hl0 -Hls0 #Hls0 >Hls in Htapeb;
122 normalize in ⊢ (%→?); #Htapeb
123 cases (IH … Htapeb) -IH #_ #IH
124 >reverse_cons >associative_append @IH //
129 lemma terminate_move_char_l :
130 ∀alpha,sep.∀t,b,a,ls,rs. t = midtape alpha ls b (a::rs) →
131 (b = sep ∨ memb ? sep ls = true) → Terminate alpha (move_char_l alpha sep) t.
132 #alpha #sep #t #b #a #ls #rs #Ht #Hsep
133 @(terminate_while … (sem_mcl_step alpha sep))
135 |generalize in match Hsep; -Hsep
136 generalize in match Ht; -Ht
137 generalize in match rs; -rs
138 generalize in match a; -a
139 generalize in match b; -b
140 generalize in match t; -t
142 [#t #b #a #rs #Ht #Hsep % #tinit
143 whd in ⊢ (%→?); #H @False_ind
144 cases (H … Ht) #Hb #_ cases Hb #eqb @eqb
145 cases Hsep // whd in ⊢ ((??%?)→?); #abs destruct
146 |#l0 #ls0 #Hind #t #b #a #rs #Ht #Hsep % #tinit
148 cases (H … Ht) #Hbsep #Htinit
149 @(Hind … Htinit) cases Hsep
150 [#Hb @False_ind /2/ | #Hmemb cases (orb_true_l … Hmemb)
151 [#eqsep %1 >(\P eqsep) // | #H %2 //]
155 (* NO GOOD: we must stop if current = None too!!!
156 lemma ssem_move_char_l :
158 Realize alpha (move_char_l alpha sep) (R_move_char_l alpha sep).
160 [ %{5} % [| % [whd in ⊢ (??%?);
161 @WRealize_to_Realize // @terminate_move_char_l
164 axiom ssem_move_char_l :
166 Realize alpha (move_char_l alpha sep) (R_move_char_l alpha sep).