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_____________________________________________________________*)
17 include "turing/universal/copy.ma".
23 if is_true(current) (* current state is final *)
35 if is_marked(current) = false (* match ok *)
48 case bit false: move_tape_l
49 case bit true: move_tape_r
50 case null: adv_to_grid_l; move_l; adv_to_grid_l;
57 definition init_match ≝
59 (seq ? (adv_to_mark_r ? (λc:STape.is_grid (\fst c)))
63 (adv_to_mark_l ? (is_marked ?)))))).
65 definition R_init_match ≝ λt1,t2.
66 ∀ls,l,rs,c,d. no_grids (〈c,false〉::l) → no_marks l →
67 t1 = midtape STape ls 〈c,false〉 (l@〈grid,false〉::〈d,false〉::rs) →
68 t2 = midtape STape ls 〈c,true〉 (l@〈grid,false〉::〈d,true〉::rs).
70 lemma sem_init_match : Realize ? init_match R_init_match.
72 cases (sem_seq ????? (sem_mark ?)
73 (sem_seq ????? (sem_adv_to_mark_r ? (λc:STape.is_grid (\fst c)))
74 (sem_seq ????? (sem_move_r ?)
75 (sem_seq ????? (sem_mark ?)
76 (sem_seq ????? (sem_move_l ?)
77 (sem_adv_to_mark_l ? (is_marked ?)))))) intape)
78 #k * #outc * #Hloop #HR
79 @(ex_intro ?? k) @(ex_intro ?? outc) % [@Hloop] -Hloop
80 #ls #l #rs #c #d #Hnogrids #Hnomarks #Hintape
82 #ta * whd in ⊢ (%→?); #Hta lapply (Hta … Hintape) -Hta -Hintape #Hta
83 * #tb * whd in ⊢ (%→?); #Htb cases (Htb … Hta) -Htb -Hta
84 [* #Hgridc @False_ind @(absurd … Hgridc) @eqnot_to_noteq
85 @(Hnogrids 〈c,false〉) @memb_hd ]
86 * #Hgrdic #Htb lapply (Htb l 〈grid,false〉 (〈d,false〉::rs) (refl …) (refl …) ?)
87 [#x #membl @Hnogrids @memb_cons @membl] -Htb #Htb
88 * #tc * whd in ⊢ (%→?); #Htc lapply (Htc … Htb) -Htc -Htb #Htc
89 * #td * whd in ⊢ (%→?); #Htd lapply (Htd … Htc) -Htd -Htc #Htd
90 * #te * whd in ⊢ (%→?); #Hte lapply (Hte … Htd) -Hte -Htd #Hte
91 whd in ⊢ (%→?); #Htf cases (Htf … Hte) -Htf -Hte
92 [* whd in ⊢ ((??%?)→?); #Habs destruct (Habs)]
93 * #_ #Htf lapply (Htf (reverse ? l) 〈c,true〉 ls (refl …) (refl …) ?)
94 [#x #membl @Hnomarks @daemon] -Htf #Htf >Htf >reverse_reverse %
97 #Htb lapply (Htb ??? (refl …) (refl …))
99 lapply (Htb l 〈grid,false〉 (〈d,false〉::rs) (refl … ))
102 * #tc * whd in ⊢ (%→?); #Htc
103 * #td * whd in ⊢ (%→%→?); #Htd #Houtc
104 #l1 #c #l2 #b #l3 #c1 #rs #c0 #b0 #Hl1 #Hl2 #Hc #Hc0 #Hintape
105 cases (Hta … Hintape) [ * #Hfalse normalize in Hfalse; destruct (Hfalse) ]
106 -Hta * #_ #Hta lapply (Hta l1 〈c,true〉 ? (refl ??) ??) [@Hl1|%]
107 -Hta #Hta lapply (Htb … Hta) -Htb #Htb cases (Htc … Htb) [ >Hc -Hc * #Hc destruct (Hc) ]
108 -Htc * #_ #Htc lapply (Htc … (refl ??) (refl ??) ?) [@Hl2]
109 -Htc #Htc lapply (Htd … Htc) -Htd
110 >reverse_append >reverse_cons
111 >reverse_cons in Hc0; cases (reverse … l2)
112 [ normalize in ⊢ (%→?); #Hc0 destruct (Hc0)
113 #Htd >(Houtc … Htd) %
114 | * #c2 #b2 #tl2 normalize in ⊢ (%→?);
115 #Hc0 #Htd >(Houtc … Htd)
116 whd in ⊢ (???%); destruct (Hc0)
117 >associative_append >associative_append %
121 definition match_tuple_step ≝
122 ifTM ? (test_char ? (λc:STape.¬ is_grid (\fst c)))
125 (ifTM ? (test_char ? (λc:STape.is_grid (\fst c)))
127 (seq ? mark_next_tuple
128 (ifTM ? (test_char ? (λc:STape.is_grid (\fst c)))
129 (mark ?) (seq ? (move_l ?) init_current) tc_true)) tc_true)))