matita/matita/lib/turing/if_machine.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 include "turing/mono.ma".
  13
  14 definition single_finalTM ≝
  15   λsig.λM:TM sig.seq ? M (nop ?).
  16
  17 lemma sem_single_final :
  18   ∀sig,M,R.Realize ? M R → Realize ? (single_finalTM sig M) R.
  19 #sig #M #R #HR #intape
  20 cases (sem_seq ????? HR (sem_nop …) intape)
  21 #k * #outc * #Hloop * #ta * #Hta whd in ⊢ (%→?); #Houtc
  22 @(ex_intro ?? k) @(ex_intro ?? outc) %  [ @Hloop | >Houtc // ]
  23 qed.
  24
  25 definition if_trans ≝ λsig. λM1,M2,M3 : TM sig. λq:states sig M1.
  26 λp. let 〈s,a〉 ≝ p in
  27   match s with
  28   [ inl s1 ⇒
  29       if halt sig M1 s1 then
  30         if s1==q then 〈inr … (inl … (start sig M2)), None ?〉
  31         else 〈inr … (inr … (start sig M3)), None ?〉
  32       else let 〈news1,m〉 ≝ trans sig M1 〈s1,a〉 in
  33        〈inl … news1,m〉
  34   | inr s' ⇒
  35       match s' with
  36       [ inl s2 ⇒ let 〈news2,m〉 ≝ trans sig M2 〈s2,a〉 in
  37          〈inr … (inl … news2),m〉
  38       | inr s3 ⇒ let 〈news3,m〉 ≝ trans sig M3 〈s3,a〉 in
  39          〈inr … (inr … news3),m〉
  40       ]
  41   ].
  42
  43 definition ifTM ≝ λsig. λcondM,thenM,elseM : TM sig.
  44   λqacc: states sig condM.
  45   mk_TM sig
  46     (FinSum (states sig condM) (FinSum (states sig thenM) (states sig elseM)))
  47     (if_trans sig condM thenM elseM qacc)
  48     (inl … (start sig condM))
  49     (λs.match s with
  50       [ inl _ ⇒ false
  51       | inr s' ⇒ match s' with
  52         [ inl s2 ⇒ halt sig thenM s2
  53         | inr s3 ⇒ halt sig elseM s3 ]]).
  54
  55 axiom daemon : ∀X:Prop.X.
  56 axiom tdaemon : ∀X:Type[0].X.
  57
  58 axiom sem_if: ∀sig,M1,M2,M3,Rtrue,Rfalse,R2,R3,acc.
  59   accRealize sig M1 acc Rtrue Rfalse → Realize sig M2 R2 → Realize sig M3 R3 →
  60     Realize sig (ifTM sig M1 M2 M3 acc) (λt1,t2. (Rtrue ∘ R2) t1 t2 ∨ (Rfalse ∘ R3) t1 t2).
  61 (*
  62 #sig #M1 #M2 #M3 #Rtrue #Rfalse #R2 #R3 #acc #HaccR #HR2 #HR3 #t
  63 cases (HaccR t) #k1 * #outc1 * * #Hloop1 #HMtrue #HMfalse
  64 cases (true_or_false (cstate ?? outc1 == acc)) #Hacc
  65   [cases (HR2 (ctape sig ? outc1)) #k2 * #outc2 * #Hloop2 #HM2
  66    @(ex_intro … (k1+k2)) @(ex_intro … (lift_confR … (lift_confL … outc2)))
  67    %
  68    [@(loop_merge ???????????
  69     (loop_lift ???
  70       (lift_confL sig (states ? M1) (FinSum (states ? M2) (states ? M3)))
  71       (step sig M1) (step sig (ifTM sig M1 M2 M3 acc))
  72       (λc.halt sig M1 (cstate … c))
  73       (λc.halt_liftL ?? (halt sig M1) (cstate … c))
  74       … Hloop1))
  75      [* *
  76        [ #sl #tl whd in ⊢ (??%? → ?); #Hl %
  77        | #sr #tr whd in ⊢ (??%? → ?); #Hr destruct (Hr) ]
  78      || #c0 #Hhalt @daemon  (* <step_lift_confL // *)
  79      | #x <p_halt_liftL %
  80      |6:cases outc1 #s1 #t1 %
  81      |7:@(loop_lift … (initc ?? (ctape … outc1)) … Hloop2)
  82        [ * #s2 #t2 %
  83        | #c0 #Hhalt @daemon (* <step_lift_confR // *) ]
  84      |whd in ⊢ (??(???%)?);whd in ⊢ (??%?);
  85       generalize in match Hloop1; cases outc1 #sc1 #tc1 #Hloop10
  86       >(trans_liftL_true sig M1 M2 ??)
  87        [ whd in ⊢ (??%?); whd in ⊢ (???%);
  88          @daemon
  89 (*         @config_eq whd in ⊢ (???%); // *)
  90        | @(loop_Some ?????? Hloop10)
  91        | @tdaemon
  92        | skip ]
  93       ]
  94      |
  95      |4:cases outc1 #s1 #t1 %
  96      |5:
  97
  98          @(loop_liftR … Hloop2)
  99          |whd in ⊢ (??(???%)?);whd in ⊢ (??%?);
 100           generalize in match Hloop1; cases outc1 #sc1 #tc1 #Hloop10
 101           >(trans_liftL_true sig M1 M2 ??)
 102            [ whd in ⊢ (??%?); whd in ⊢ (???%);
 103              @config_eq //
 104            | @(loop_Some ?????? Hloop10) ]
 105            ]
 106 | @(ex_intro … (ctape ? (seq sig M1 M2) (lift_confL … outc1)))
 107   % //
 108 ]
 109 qed.
 110 *)