]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/lib/turing/universal/tuples.ma
3492f2e2cb8df64555ad752858a094ad3d363ed6
[helm.git] / matita / matita / lib / turing / universal / tuples.ma
1 (*
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.           
5     ||I||                                                            
6     ||T||  
7     ||A||  
8     \   /  This file is distributed under the terms of the       
9      \ /   GNU General Public License Version 2   
10       V_____________________________________________________________*)
11
12
13 (* COMPARE BIT
14
15 *)
16
17 include "turing/universal/marks.ma".
18
19 definition STape ≝ FinProd … FSUnialpha FinBool.
20
21 definition only_bits ≝ λl.
22   ∀c.memb STape c l = true → is_bit (\fst c) = true.
23
24 (*
25 l0 x* a l1 x0* a0 l2 ------> l0 x a* l1 x0 a0* l2
26    ^                               ^
27
28 if current (* x *) = #
29    then 
30    else if x = 0
31       then move_right; ----
32            adv_to_mark_r;
33            if current (* x0 *) = 0
34               then advance_mark ----
35                    adv_to_mark_l;
36                    advance_mark
37               else STOP
38       else x = 1 (* analogo *)
39
40 *)
41
42
43 (*
44    MARK NEXT TUPLE machine
45    (partially axiomatized)
46    
47    marks the first character after the first bar (rightwards)
48  *)
49  
50 definition bar_or_grid ≝ λc:STape.is_bar (\fst c) ∨ is_grid (\fst c).
51
52 definition mark_next_tuple ≝ 
53   seq ? (adv_to_mark_r ? bar_or_grid)
54      (ifTM ? (test_char ? (λc:STape.is_bar (\fst c)))
55        (move_right_and_mark ?) (nop ?) 1).
56
57 definition R_mark_next_tuple ≝ 
58   λt1,t2.
59     ∀ls,c,rs1,rs2.
60     (* c non può essere un separatore ... speriamo *)
61     t1 = midtape ? ls c (rs1@〈grid,false〉::rs2) → 
62     only_bits rs1 → bar_or_grid c = false → 
63     (∃rs3,rs4,d,b.rs1 = rs3 @ 〈bar,false〉 :: rs4 ∧
64       Some ? 〈d,b〉 = option_hd ? (rs4@〈grid,false〉::rs2) ∧
65       t2 = midtape ? (bar::reverse ? rs3@c::ls) 〈d,true〉 (tail ? (rs4@〈grid,false〉::rs2)))
66     ∨
67     (memb ? bar rs1 = false ∧ 
68      t2 = midtape ? (reverse ? rs1@c::ls) 〈grid,false〉 rs2).
69      
70 axiom tech_split :
71   ∀A:DeqSet.∀f,l.
72    (∀x.memb A x l = true → f x = false) ∨
73    (∃l1,c,l2.f c = true ∧ l = l1@c::l2 ∧ ∀x.memb ? x l1 = true → f c = false).
74 (*#A #f #l elim l
75 [ % #x normalize #Hfalse *)
76      
77 theorem sem_mark_next_tuple :
78   Realize ? mark_next_tuple R_mark_next_tuple.
79 #intape 
80 lapply (sem_seq ? (adv_to_mark_r ? bar_or_grid)
81          (ifTM ? (test_char ? is_bar) (mark ?) (nop ?) 1) ????)
82 [@sem_if //
83 | //
84 |||#Hif cases (Hif intape) -Hif
85    #j * #outc * #Hloop * #ta * #Hleft #Hright
86    @(ex_intro ?? j) @ex_intro [|% [@Hloop] ]
87    -Hloop
88    #ls #c #rs1 #rs2 #Hrs #Hrs1 #Hc
89    cases (Hleft … Hrs)
90    [ * #Hfalse >Hfalse in Hc; #Htf destruct (Htf)
91    | * #_ #Hta cases (tech_split ? is_bar rs1)
92      [ #H1 lapply (Hta rs1 grid rs2 (refl ??) ? ?)
93        [ (* Hrs1, H1 *) @daemon
94        | (* bar_or_grid grid = true *) @daemon
95        | -Hta #Hta cases Hright
96          [ * #tb * whd in ⊢ (%→?); #Hcurrent
97            @False_ind cases(Hcurrent grid ?)
98            [ #Hfalse (* grid is not a bar *) @daemon
99            | >Hta % ]
100          | * #tb * whd in ⊢ (%→?); #Hcurrent
101            cases (Hcurrent grid ?)
102            [  #_ #Htb whd in ⊢ (%→?); #Houtc
103              %2 %
104              [ (* H1 *) @daemon
105              | >Houtc >Htb >Hta % ]
106            | >Hta % ]
107          ]
108        ]
109     | * #rs3 * #c0 * #rs4 * * #Hc0 #Hsplit #Hrs3
110       % @(ex_intro ?? rs3) @(ex_intro ?? rs4)
111      lapply (Hta rs3 c0 (rs4@grid::rs2) ???)
112      [ #x #Hrs3' (* Hrs1, Hrs3, Hsplit *) @daemon
113      | (* bar → bar_or_grid *) @daemon
114      | >Hsplit >associative_append % ] -Hta #Hta
115        cases Hright
116        [ * #tb * whd in ⊢ (%→?); #Hta'
117          whd in ⊢ (%→?); #Htb
118          cases (Hta' c0 ?)
119          [ #_ #Htb' >Htb' in Htb; #Htb
120            generalize in match Hsplit; -Hsplit
121            cases rs4 in Hta;
122            [ >(eq_pair_fst_snd … grid)
123              #Hta #Hsplit >(Htb … Hta)
124              >(?:c0 = bar)
125              [ @(ex_intro ?? (\fst grid)) @(ex_intro ?? (\snd grid))
126                % [ % [ % [ (* Hsplit *) @daemon |(*Hrs3*) @daemon ] | % ] | % ] 
127                      | (* Hc0 *) @daemon ]
128            | #r5 #rs5 >(eq_pair_fst_snd … r5)
129              #Hta #Hsplit >(Htb … Hta)
130              >(?:c0 = bar)
131              [ @(ex_intro ?? (\fst r5)) @(ex_intro ?? (\snd r5))
132                % [ % [ % [ (* Hc0, Hsplit *) @daemon | (*Hrs3*) @daemon ] | % ]
133                      | % ] | (* Hc0 *) @daemon ] ] | >Hta % ]
134              | * #tb * whd in ⊢ (%→?); #Hta'
135                whd in ⊢ (%→?); #Htb
136                cases (Hta' c0 ?)
137                [ #Hfalse @False_ind >Hfalse in Hc0;
138                  #Hc0 destruct (Hc0)
139                | >Hta % ]
140 ]]]]
141 qed.