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 (variant c) 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)
34 include "turing/basic_machines.ma".
35 include "turing/if_machine.ma".
37 definition mcc_step ≝ λalpha:FinSet.λsep:alpha.
38 ifTM alpha (test_char ? (λc.¬c==sep))
39 (single_finalTM … (seq … (swap_r alpha sep) (move_r ?))) (nop ?) tc_true.
41 definition Rmcc_step_true ≝
44 t1 = midtape alpha (a::ls) b rs →
46 t2 = mk_tape alpha (a::b::ls) (option_hd ? rs) (tail ? rs).
48 definition Rmcc_step_false ≝
50 left ? t1 ≠ [] → current alpha t1 ≠ None alpha →
51 current alpha t1 = Some alpha sep ∧ t2 = t1.
56 [inr … (inl … (inr … start_nop)): Rmcc_step_true alpha sep, Rmcc_step_false alpha sep].
59 (sem_test_char …) (sem_seq …(sem_swap_r …) (sem_move_r …)) (sem_nop …))
60 [#intape #outtape #tapea whd in ⊢ (%→%→%);
61 #Htapea * #tapeb * whd in ⊢ (%→%→?);
62 #Htapeb #Houttape #a #b #ls #rs #Hintape
63 >Hintape in Htapea; #Htapea cases (Htapea ? (refl …)) -Htapea
64 #Hbsep #Htapea % [@(\Pf (injective_notb ? false Hbsep))]
66 |#intape #outtape #tapea whd in ⊢ (%→%→%);
67 cases (current alpha intape)
68 [#_ #_ #_ * #Hfalse @False_ind @Hfalse %
69 |#c #H #Htapea #_ #_ cases (H c (refl …)) #csep #Hintape % //
70 lapply (injective_notb ? true csep) -csep #csep >(\P csep) //
75 (* the move_char (variant c) machine *)
76 definition move_char_c ≝
77 λalpha,sep.whileTM alpha (mcc_step alpha sep) (inr … (inl … (inr … start_nop))).
79 definition R_move_char_c ≝
81 ∀b,a,ls,rs. t1 = midtape alpha (a::ls) b rs →
83 (∀rs1,rs2.rs = rs1@sep::rs2 →
84 b ≠ sep → memb ? sep rs1 = false →
85 t2 = midtape alpha (a::reverse ? rs1@b::ls) sep rs2).
87 lemma sem_move_char_c :
89 WRealize alpha (move_char_c alpha sep) (R_move_char_c alpha sep).
90 #alpha #sep #inc #i #outc #Hloop
91 lapply (sem_while … (sem_mcc_step alpha sep) inc i outc Hloop) [%]
92 -Hloop * #t1 * #Hstar @(star_ind_l ??????? Hstar)
93 [ #tapea whd in ⊢ (% → ?); #H1 #b #a #ls #rs #Htapea
95 [ #Hb >Htapea in H1; >Hb #H1 cases (H1 ??)
96 [#_ #H2 >H2 % |*: % #H2 normalize in H2; destruct (H2)]
97 | #rs1 #rs2 #Hrs #Hb #Hrs1
98 >Htapea in H1; #H1 cases (H1 ??)
99 [#Hfalse @False_ind @(absurd ?? Hb) normalize in Hfalse; destruct %
100 |*:% #H2 normalize in H2; destruct (H2) ]
102 | #tapea #tapeb #tapec #Hstar1 #HRtrue #IH #HRfalse
103 lapply (IH HRfalse) -IH whd in ⊢ (%→%); #IH
104 #a0 #b0 #ls #rs #Htapea cases (Hstar1 … Htapea)
106 [ #Hfalse @False_ind @(absurd ?? Ha0) //
108 [ #rs2 whd in ⊢ (???%→?); #Hrs #_ #_ (* normalize *)
109 >Hrs in Htapeb; #Htapeb normalize in Htapeb;
110 cases (IH … Htapeb) #Houtc #_ >Houtc normalize //
111 | #r0 #rs0 #rs2 #Hrs #_ #Hrs0
112 cut (r0 ≠ sep ∧ memb … sep rs0 = false)
114 [ % #Hr0 >Hr0 in Hrs0; >memb_hd #Hfalse destruct
115 | whd in Hrs0:(??%?); cases (sep==r0) in Hrs0; normalize #Hfalse
120 #Hr0 -Hrs0 #Hrs0 >Hrs in Htapeb;
121 normalize in ⊢ (%→?); #Htapeb
122 cases (IH … Htapeb) -IH #_ #IH
123 >reverse_cons >associative_append @IH //
128 lemma terminate_move_char_c :
129 ∀alpha,sep.∀t,b,a,ls,rs. t = midtape alpha (a::ls) b rs →
130 (b = sep ∨ memb ? sep rs = true) → Terminate alpha (move_char_c alpha sep) t.
131 #alpha #sep #t #b #a #ls #rs #Ht #Hsep
132 @(terminate_while … (sem_mcc_step alpha sep))
134 |generalize in match Hsep; -Hsep
135 generalize in match Ht; -Ht
136 generalize in match ls; -ls
137 generalize in match a; -a
138 generalize in match b; -b
139 generalize in match t; -t
141 [#t #b #a #ls #Ht #Hsep % #tinit
142 whd in ⊢ (%→?); #H @False_ind
143 cases (H … Ht) #Hb #_ cases Hb #eqb @eqb
144 cases Hsep // whd in ⊢ ((??%?)→?); #abs destruct
145 |#r0 #rs0 #Hind #t #b #a #ls #Ht #Hsep % #tinit
147 cases (H … Ht) #Hbsep #Htinit
148 @(Hind … Htinit) cases Hsep
149 [#Hb @False_ind /2/ | #Hmemb cases (orb_true_l … Hmemb)
150 [#eqsep %1 >(\P eqsep) // | #H %2 //]
154 (* NO GOOD: we must stop if current = None too!!! *)
156 axiom ssem_move_char_c :
158 Realize alpha (move_char_c alpha sep) (R_move_char_c alpha sep).