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 check unialpha
  51
  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.
  57
  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).
  62
  63 definition R_mark_next_tuple ≝
  64   λt1,t2.
  65     ∀ls,c,rs1,rs2.
  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)))
  73     ∨
  74     (memb ? bar rs1 = false ∧
  75      t2 = midtape ? (reverse ? rs1@c::ls) grid rs2).
  76
  77 axiom tech_split :
  78   ∀A:DeqSet.∀f,l.
  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).
  81 (*#A #f #l elim l
  82 [ % #x normalize #Hfalse *)
  83
  84 theorem sem_mark_next_tuple :
  85   Realize ? mark_next_tuple R_mark_next_tuple.
  86 #intape
  87 lapply (sem_seq ? (adv_to_mark_r ? bar_or_grid)
  88          (ifTM ? (test_char ? is_bar) (mark ?) (nop ?) 1) ????)
  89 [@sem_if //
  90 | //
  91 |||#Hif cases (Hif intape) -Hif
  92    #j * #outc * #Hloop * #ta * #Hleft #Hright
  93    @(ex_intro ?? j) @ex_intro [|% [@Hloop] ]
  94    -Hloop
  95    #ls #c #rs1 #rs2 #Hrs #Hrs1 #Hc
  96    cases (Hleft … Hrs)
  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
 106            | >Hta % ]
 107          | * #tb * whd in ⊢ (%→?); #Hcurrent
 108            cases (Hcurrent grid ?)
 109            [  #_ #Htb whd in ⊢ (%→?); #Houtc
 110              %2 %
 111              [ (* H1 *) @daemon
 112              | >Houtc >Htb >Hta % ]
 113            | >Hta % ]
 114          ]
 115        ]
 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
 122        cases Hright
 123        [ * #tb * whd in ⊢ (%→?); #Hta'
 124          whd in ⊢ (%→?); #Htb
 125          cases (Hta' c0 ?)
 126          [ #_ #Htb' >Htb' in Htb; #Htb
 127            generalize in match Hsplit; -Hsplit
 128            cases rs4 in Hta;
 129            [ >(eq_pair_fst_snd … grid)
 130              #Hta #Hsplit >(Htb … Hta)
 131              >(?:c0 = bar)
 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)
 137              >(?:c0 = bar)
 138              [ @(ex_intro ?? (\fst r5)) @(ex_intro ?? (\snd r5))
 139                % [ % [ % [ (* Hc0, Hsplit *) @daemon | (*Hrs3*) @daemon ] | % ]
 140                      | % ] | (* Hc0 *) @daemon ] ] | >Hta % ]
 141              | * #tb * whd in ⊢ (%→?); #Hta'
 142                whd in ⊢ (%→?); #Htb
 143                cases (Hta' c0 ?)
 144                [ #Hfalse @False_ind >Hfalse in Hc0;
 145                  #Hc0 destruct (Hc0)
 146                | >Hta % ]
 147 ]]]]
 148 qed.