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/marks.ma".
19 definition STape ≝ FinProd … FSUnialpha FinBool.
21 definition only_bits ≝ λl.
22 ∀c.memb STape c l = true → is_bit (\fst c) = true.
25 l0 x* a l1 x0* a0 l2 ------> l0 x a* l1 x0 a0* l2
28 if current (* x *) = #
33 if current (* x0 *) = 0
34 then advance_mark ----
38 else x = 1 (* analogo *)
44 MARK NEXT TUPLE machine
45 (partially axiomatized)
47 marks the first character after the first bar (rightwards)
52 axiom is_bar : FinProd … myalpha FinBool → bool.
53 axiom is_grid : FinProd … myalpha FinBool → bool.
54 definition bar_or_grid ≝ λc.is_bar c ∨ is_grid c.
55 axiom bar : FinProd … myalpha FinBool.
56 axiom grid : FinProd … myalpha FinBool.
58 definition mark_next_tuple ≝
59 seq ? (adv_to_mark_r ? bar_or_grid)
60 (ifTM ? (test_char ? is_bar)
61 (move_r_and_mark ?) (nop ?) 1).
63 definition R_mark_next_tuple ≝
66 (* c non può essere un separatore ... speriamo *)
67 t1 = midtape ? ls c (rs1@grid::rs2) →
68 memb ? grid rs1 = false → bar_or_grid c = false →
69 (∃rs3,rs4,d,b.rs1 = rs3 @ bar :: rs4 ∧
70 memb ? bar rs3 = false ∧
71 Some ? 〈d,b〉 = option_hd ? (rs4@grid::rs2) ∧
72 t2 = midtape ? (bar::reverse ? rs3@c::ls) 〈d,true〉 (tail ? (rs4@grid::rs2)))
74 (memb ? bar rs1 = false ∧
75 t2 = midtape ? (reverse ? rs1@c::ls) grid rs2).
79 (∀x.memb A x l = true → f x = false) ∨
80 (∃l1,c,l2.f c = true ∧ l = l1@c::l2 ∧ ∀x.memb ? x l1 = true → f c = false).
82 [ % #x normalize #Hfalse *)
84 theorem sem_mark_next_tuple :
85 Realize ? mark_next_tuple R_mark_next_tuple.
87 lapply (sem_seq ? (adv_to_mark_r ? bar_or_grid)
88 (ifTM ? (test_char ? is_bar) (mark ?) (nop ?) 1) ????)
91 |||#Hif cases (Hif intape) -Hif
92 #j * #outc * #Hloop * #ta * #Hleft #Hright
93 @(ex_intro ?? j) @ex_intro [|% [@Hloop] ]
95 #ls #c #rs1 #rs2 #Hrs #Hrs1 #Hc
97 [ * #Hfalse >Hfalse in Hc; #Htf destruct (Htf)
98 | * #_ #Hta cases (tech_split ? is_bar rs1)
99 [ #H1 lapply (Hta rs1 grid rs2 (refl ??) ? ?)
100 [ (* Hrs1, H1 *) @daemon
101 | (* bar_or_grid grid = true *) @daemon
102 | -Hta #Hta cases Hright
103 [ * #tb * whd in ⊢ (%→?); #Hcurrent
104 @False_ind cases(Hcurrent grid ?)
105 [ #Hfalse (* grid is not a bar *) @daemon
107 | * #tb * whd in ⊢ (%→?); #Hcurrent
108 cases (Hcurrent grid ?)
109 [ #_ #Htb whd in ⊢ (%→?); #Houtc
112 | >Houtc >Htb >Hta % ]
116 | * #rs3 * #c0 * #rs4 * * #Hc0 #Hsplit #Hrs3
117 % @(ex_intro ?? rs3) @(ex_intro ?? rs4)
118 lapply (Hta rs3 c0 (rs4@grid::rs2) ???)
119 [ #x #Hrs3' (* Hrs1, Hrs3, Hsplit *) @daemon
120 | (* bar → bar_or_grid *) @daemon
121 | >Hsplit >associative_append % ] -Hta #Hta
123 [ * #tb * whd in ⊢ (%→?); #Hta'
126 [ #_ #Htb' >Htb' in Htb; #Htb
127 generalize in match Hsplit; -Hsplit
129 [ >(eq_pair_fst_snd … grid)
130 #Hta #Hsplit >(Htb … Hta)
132 [ @(ex_intro ?? (\fst grid)) @(ex_intro ?? (\snd grid))
133 % [ % [ % [ (* Hsplit *) @daemon |(*Hrs3*) @daemon ] | % ] | % ]
134 | (* Hc0 *) @daemon ]
135 | #r5 #rs5 >(eq_pair_fst_snd … r5)
136 #Hta #Hsplit >(Htb … Hta)
138 [ @(ex_intro ?? (\fst r5)) @(ex_intro ?? (\snd r5))
139 % [ % [ % [ (* Hc0, Hsplit *) @daemon | (*Hrs3*) @daemon ] | % ]
140 | % ] | (* Hc0 *) @daemon ] ] | >Hta % ]
141 | * #tb * whd in ⊢ (%→?); #Hta'
144 [ #Hfalse @False_ind >Hfalse in Hc0;