1 (* include "turing/auxiliary_machines.ma". *)
3 include "turing/multi_to_mono/exec_trace_move.ma".
4 (* include "turing/turing.ma". *)
6 let rec exec_moves Q sig n i on i : TM (MTA (HC Q n) sig (S n)) ≝
8 [ O ⇒ nop ? (* exec_move_i sig n 0 *)
9 | S j ⇒ seq ? (exec_moves Q sig n j) (exec_move_i Q sig n j)
13 λsig,n.λactions: Vector ((option sig) × move) n.
14 vec_map ?? (snd ??) n actions.
17 λsig,n.λactions: Vector ((option sig) × move) n.
18 vec_map ?? (fst ??) n actions.
20 definition tape_moves ≝
22 pmap_vec ??? (tape_move sig) n ts mvs.
24 lemma tape_moves_def : ∀sig,n,ts,mvs.
25 tape_moves sig n ts mvs = pmap_vec ??? (tape_move sig) n ts mvs.
28 definition tape_writem ≝
30 pmap_vec ??? (tape_write sig) n ts chars.
33 let rec i_moves a i on i : Vector move i ≝
35 [ O ⇒ mk_Vector ? 0 (nil ?) (refl ??)
36 | S j ⇒ vec_cons ? (nth j ? a N) j (i_moves a j)
39 definition vec_moves ≝ λQ,sig,n,a,i.
40 resize_vec … (get_moves Q sig n a) i N.
42 axiom vec_moves_cons: ∀Q,sig,n,a,j.j < n →
43 vec_moves Q sig n a (S j) =
44 vec_cons ? (get_move Q ? n a j) j (vec_moves Q sig n a j).
47 axiom actions_commute : ∀sig,n,ts,actions.
48 tape_moves sig n (tape_writem ?? ts (a_chars … actions)) (a_moves … actions) =
49 tape_move_multi ?? ts actions. *)
51 (* devo rafforzare la semantica, dicendo che i tape non toccati
52 dalle moves non cambiano *)
55 definition R_exec_moves ≝ λQ,sig,n,i,t1,t2.
57 t1 = midtape ? ls a rs →
58 (∀i.regular_trace (TA (HC Q n) sig) (S n) a ls rs i) →
59 is_head ?? (nth n ? (vec … a) (blank ?)) = true →
63 t2 = midtape (MTA (HC Q n) sig (S n)) ls1 a1 rs1 ∧
64 (∀i.regular_trace (TA (HC Q n) sig) (S n) a1 ls1 rs1 i) ∧
66 rb_trace_i ? (S n) ls1 (vec … a1) rs1 j =
67 tape_move ? (rb_trace_i ? (S n) ls (vec … a) rs j) (get_move Q sig n a j)) ∧
68 (* tape_moves ?? (readback ? (S n) ls (vec … a) rs i) (vec_moves Q sig n a i) ∧ *)
70 rb_trace_i ? (S n) ls1 (vec … a1) rs1 j =
71 rb_trace_i ? (S n) ls (vec … a) rs j).
73 (* alias id "Realize_to_Realize" =
74 "cic:/matita/turing/mono/Realize_to_Realize.def(13)". *)
77 lemma nth_readback: ∀sig,n,ls,a,rs,j,i. i < j →
78 nth i ? (readback sig n ls a rs j) (niltape ?) =
79 rb_trace_i sig n ls a rs (j - S i).
80 #sig #n #ls #a #rs #j elim j
81 [#i #lti0 @False_ind /2/
83 [#_ >minus_S_S <minus_n_O %
84 |#m #Hmj >minus_S_S @Hind @le_S_S_to_le //
89 lemma sem_exec_moves: ∀Q,sig,n,i. i ≤ n →
90 exec_moves Q sig n i ⊨ R_exec_moves Q sig n i.
92 [#_ @(Realize_to_Realize … (sem_nop …))
93 #t1 #t2 #H #a #ls #rs #Ht1 #Hreg #H1 #H2 #H3
94 %{ls} %{a} %{rs} %[% >H [%[@Ht1|@Hreg]| #j #ltjO @False_ind /2/]|//]
95 |#j #Hind #lttj lapply (lt_to_le … lttj) #ltj
96 @(sem_seq_app … (Hind ltj) (sem_exec_move_i … lttj)) -Hind
97 #int #outt * #t1 * #H1 #H2
98 #a #ls #rs #Hint #H3 #H4 #H5 #H6
99 lapply (H1 … Hint H3 H4 H5 H6)
100 * #ls1 * #a1 * #rs1 * * * #H7 #H8 #H9 #H10
101 lapply (reg_inv … (H8 n) ? H4 H5 H6)
103 -H3 -H4 -H5 -H6 * * #H3 #H4 #H5
104 lapply (H2 … H7 H8 H3 H4 H5)
105 * #ls2 * #a2 * #rs2 * * * #Houtt #Hregout #Hrboutt #Hrbid
107 cut (∀i. get_move Q sig n a i = get_move Q sig n a1 i)
109 %[%[%[@Houtt|@Hregout]
110 |#k #ltk cases (le_to_or_lt_eq … ltk) #Hk #lekn
111 [>(Hrbid … lekn) [2:@lt_to_not_eq @le_S_S_to_le @Hk]
112 @(H9 k ? lekn) @le_S_S_to_le @Hk
113 |destruct (Hk) <H10 // @Hrboutt
116 |#a #Hja #Han >(Hrbid … Han)
117 [@(H10 … Han) @lt_to_le @Hja |@sym_not_eq @lt_to_not_eq @Hja ]