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/if_multi.ma".
13 include "turing/inject.ma".
14 include "turing/basic_machines.ma".
16 definition Rtc_multi_true ≝
17 λalpha,test,n,i.λt1,t2:Vector ? (S n).
18 (∃c. current alpha (nth i ? t1 (niltape ?)) = Some ? c ∧ test c = true) ∧ t2 = t1.
20 definition Rtc_multi_false ≝
21 λalpha,test,n,i.λt1,t2:Vector ? (S n).
22 (∀c. current alpha (nth i ? t1 (niltape ?)) = Some ? c → test c = false) ∧ t2 = t1.
24 lemma sem_test_char_multi :
25 ∀alpha,test,n,i.i ≤ n →
26 inject_TM ? (test_char ? test) n i ⊨
27 [ tc_true : Rtc_multi_true alpha test n i, Rtc_multi_false alpha test n i ].
28 #alpha #test #n #i #Hin #int
29 cases (acc_sem_inject … Hin (sem_test_char alpha test) int)
30 #k * #outc * * #Hloop #Htrue #Hfalse %{k} %{outc} % [ %
32 | #Hqtrue lapply (Htrue Hqtrue) * * * #c *
33 #Hcur #Htestc #Hnth_i #Hnth_j %
35 | @(eq_vec … (niltape ?)) #i0 #Hi0
36 cases (decidable_eq_nat i0 i) #Hi0i
38 | @sym_eq @Hnth_j @sym_not_eq // ] ] ]
39 | #Hqfalse lapply (Hfalse Hqfalse) * * #Htestc #Hnth_i #Hnth_j %
41 | @(eq_vec … (niltape ?)) #i0 #Hi0
42 cases (decidable_eq_nat i0 i) #Hi0i
44 | @sym_eq @Hnth_j @sym_not_eq // ] ] ]
47 definition Rm_test_null_true ≝
48 λalpha,n,i.λt1,t2:Vector ? (S n).
49 current alpha (nth i ? t1 (niltape ?)) ≠ None ? ∧ t2 = t1.
51 definition Rm_test_null_false ≝
52 λalpha,n,i.λt1,t2:Vector ? (S n).
53 current alpha (nth i ? t1 (niltape ?)) = None ? ∧ t2 = t1.
55 lemma sem_test_null_multi : ∀alpha,n,i.i ≤ n →
56 inject_TM ? (test_null ?) n i ⊨
57 [ tc_true : Rm_test_null_true alpha n i, Rm_test_null_false alpha n i ].
58 #alpha #n #i #Hin #int
59 cases (acc_sem_inject … Hin (sem_test_null alpha) int)
60 #k * #outc * * #Hloop #Htrue #Hfalse %{k} %{outc} % [ %
62 | #Hqtrue lapply (Htrue Hqtrue) * * #Hcur #Hnth_i #Hnth_j % //
63 @(eq_vec … (niltape ?)) #i0 #Hi0 cases (decidable_eq_nat i0 i) #Hi0i
64 [ >Hi0i @sym_eq @Hnth_i | @sym_eq @Hnth_j @sym_not_eq // ] ]
65 | #Hqfalse lapply (Hfalse Hqfalse) * * #Hcur #Hnth_i #Hnth_j %
67 | @(eq_vec … (niltape ?)) #i0 #Hi0 cases (decidable_eq_nat i0 i) //
68 #Hi0i @sym_eq @Hnth_j @sym_not_eq // ] ]
71 (* move a single tape *)
72 definition smove_states ≝ initN 2.
74 definition smove0 : smove_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 2 (refl …)).
75 definition smove1 : smove_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 2 (refl …)).
77 definition trans_smove ≝
79 λp:smove_states × (option sig).
80 let 〈q,a〉 ≝ p in match (pi1 … q) with
81 [ O ⇒ 〈smove1,None sig, D〉
82 | S _ ⇒ 〈smove1,None sig, N〉 ].
85 λsig,D.mk_TM sig smove_states (trans_smove sig D) smove0 (λq.q == smove1).
87 definition mmove ≝ λi,sig,n,D.inject_TM sig (move sig D) n i.
90 λalpha,D,t1,t2. t2 = tape_move alpha t1 D.
92 lemma sem_move_single :
93 ∀alpha,D.move alpha D ⊨ Rmove alpha D.
94 #alpha #D #int %{2} %{(mk_config ? smove_states smove1 ?)} [| % % ]
98 λalpha,n,i,D.λt1,t2:Vector ? (S n).
99 t2 = change_vec ? (S n) t1 (tape_move alpha (nth i ? t1 (niltape ?)) D) i.
101 lemma sem_move_multi :
103 mmove i alpha n D ⊨ Rm_multi alpha n i D.
104 #alpha #n #i #D #Hin #ta cases (sem_inject … Hin (sem_move_single alpha D) ta)
105 #k * #outc * #Hloop * whd in ⊢ (%→?); #Htb1 #Htb2 %{k} %{outc} % [ @Hloop ]
106 whd @(eq_vec … (niltape ?)) #i0 #Hi0 cases (decidable_eq_nat i0 i) #Hi0i
107 [ >Hi0i >Htb1 >nth_change_vec //
108 | >nth_change_vec_neq [|@sym_not_eq //] <Htb2 // @sym_not_eq // ]
111 (* simple copy with no move *)
112 definition copy_states ≝ initN 3.
114 definition cc0 : copy_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 3 (refl …)).
115 definition cc1 : copy_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 3 (refl …)).
117 definition trans_copy_char_N ≝
118 λsrc,dst.λsig:FinSet.λn.
119 λp:copy_states × (Vector (option sig) (S n)).
122 [ O ⇒ 〈cc1,change_vec ? (S n)
123 (change_vec ? (S n) (null_action ? n) (〈None ?,N〉) src)
124 (〈nth src ? a (None ?),N〉) dst〉
125 | S _ ⇒ 〈cc1,null_action ? n〉 ].
127 definition copy_char_N ≝
129 mk_mTM sig n copy_states (trans_copy_char_N src dst sig n)
132 definition R_copy_char_N ≝
133 λsrc,dst,sig,n.λint,outt: Vector (tape sig) (S n).
134 outt = change_vec ?? int
135 (tape_write ? (nth dst ? int (niltape ?))
136 (current ? (nth src ? int (niltape ?)))) dst.
138 lemma copy_char_N_q0_q1 :
139 ∀src,dst,sig,n,v.src ≠ dst → src < S n → dst < S n →
140 step sig n (copy_char_N src dst sig n) (mk_mconfig ??? cc0 v) =
143 (tape_write ? (nth dst ? v (niltape ?))
144 (current ? (nth src ? v (niltape ?)))) dst).
145 #src #dst #sig #n #v #Heq #Hsrc #Hdst
146 whd in ⊢ (??%?); @eq_f
147 <(change_vec_same … v dst (niltape ?)) in ⊢ (??%?);
148 <(change_vec_same … v src (niltape ?)) in ⊢ (??%?);
150 >pmap_change >pmap_change <tape_move_multi_def
151 >tape_move_null_action @eq_f3 //
153 | >change_vec_same >change_vec_same >nth_current_chars // ]
156 lemma sem_copy_char_N:
157 ∀src,dst,sig,n.src ≠ dst → src < S n → dst < S n →
158 copy_char_N src dst sig n ⊨ R_copy_char_N src dst sig n.
159 #src #dst #sig #n #Hneq #Hsrc #Hdst #int
160 %{2} % [| % [ % | whd >copy_char_N_q0_q1 // ]]
163 (**************** copy and advance ***********************)
164 definition copy_char_states ≝ initN 3.
166 definition trans_copy_char ≝
167 λsrc,dst.λsig:FinSet.λn.
168 λp:copy_char_states × (Vector (option sig) (S n)).
171 [ O ⇒ 〈cc1,change_vec ? (S n)
172 (change_vec ? (S n) (null_action ? n) (〈None ?,R〉) src)
173 (〈nth src ? a (None ?),R〉) dst〉
174 | S _ ⇒ 〈cc1,null_action ? n〉 ].
176 definition copy_char ≝
178 mk_mTM sig n copy_char_states (trans_copy_char src dst sig n)
181 definition R_copy_char ≝
182 λsrc,dst,sig,n.λint,outt: Vector (tape sig) (S n).
185 (tape_move_mono ? (nth src ? int (niltape ?)) 〈None ?, R〉) src)
186 (tape_move_mono ? (nth dst ? int (niltape ?))
187 〈current ? (nth src ? int (niltape ?)), R〉) dst.
189 lemma copy_char_q0_q1 :
190 ∀src,dst,sig,n,v.src ≠ dst → src < S n → dst < S n →
191 step sig n (copy_char src dst sig n) (mk_mconfig ??? cc0 v) =
195 (tape_move_mono ? (nth src ? v (niltape ?)) 〈None ?, R〉) src)
196 (tape_move_mono ? (nth dst ? v (niltape ?)) 〈current ? (nth src ? v (niltape ?)), R〉) dst).
197 #src #dst #sig #n #v #Heq #Hsrc #Hdst
199 <(change_vec_same … v dst (niltape ?)) in ⊢ (??%?);
200 <(change_vec_same … v src (niltape ?)) in ⊢ (??%?);
201 >tape_move_multi_def @eq_f2 //
202 >pmap_change >pmap_change <tape_move_multi_def
203 >tape_move_null_action @eq_f2 // @eq_f2
205 | >change_vec_same >change_vec_same // ]
209 ∀src,dst,sig,n.src ≠ dst → src < S n → dst < S n →
210 copy_char src dst sig n ⊨ R_copy_char src dst sig n.
211 #src #dst #sig #n #Hneq #Hsrc #Hdst #int
212 %{2} % [| % [ % | whd >copy_char_q0_q1 // ]]