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/turing.ma".
14 (******************* inject a mono machine into a multi tape one **********************)
15 definition inject_trans ≝ λsig,states:FinSet.λn,i:nat.
16 λtrans:states × (option sig) → states × (option (sig × move)).
17 λp:states × (Vector (option sig) (S n)).
19 let 〈nq,na〉 ≝ trans 〈q,nth i ? a (None ?)〉 in
20 let nai ≝ λj.if (eqb j i) then na else (None ?) in
21 〈q, make_veci ? nai (S n) 0〉.
23 definition inject_TM ≝ λsig.λM:TM sig.λn,i.
26 (inject_trans ?? n i (trans ? M))
30 definition inject_R ≝ λsig.λR:relation (tape sig).λn,i:nat.
31 λv1,v2: (Vector (tape sig) (S n)).
32 R (nth i ? v1 (niltape ?)) (nth i ? v2 (niltape ?)) ∧
33 ∀j. j ≠ i → nth j ? v1 (niltape ?) = nth j ? v2 (niltape ?).
35 lemma nth_make : ∀A,i,n,j,a,d. i < n → nth i ? (make_veci A a n j) d = a (j+i).
37 [#n #j #a #d #ltOn @(lt_O_n_elim … ltOn) <plus_n_O //
38 |#m #Hind #n #j #a #d #Hlt lapply Hlt @(lt_O_n_elim … (ltn_to_ltO … Hlt))
39 #p <plus_n_Sm #ltmp @Hind @le_S_S_to_le //
43 theorem sem_inject: ∀sig.∀M:TM sig.∀R.∀n,i.
44 i≤n → M ⊨ R → inject_TM sig M n i ⊨ inject_R sig R n i.
45 #sig #M #R #n #i #lein #HR #vt cases (HR (nth i ? vt (niltape ?)))
46 #k * * #outs #outt * #Hloop #HRout @(ex_intro ?? k)
47 @(ex_intro ?? (mk_mconfig ?? n outs ?) )
48 [(* this is the vector of tapes in the last mk_config *)
49 @(make_veci ? (λj.if (eqb j i) then outt else (nth j ? vt (niltape ?))) (S n) 0)
52 |%[>nth_make [>(eq_to_eqb_true … (refl ? i)) @HRout|@le_S_S //]
53 |#j #neqji >nth_make [>(not_eq_to_eqb_false … neqji) // |@le_S_S //]