matita/matita/lib/turing/universal/tests.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/if_machine.ma".
  13
  14 (* TEST CHAR
  15
  16    stato finale diverso a seconda che il carattere
  17    corrente soddisfi un test booleano oppure no
  18
  19    q1 = true or no current char
  20    q2 = false
  21 *)
  22
  23 definition tc_states ≝ initN 3.
  24
  25 definition tc_true ≝ 1.
  26
  27 definition test_char ≝
  28   λalpha:FinSet.λtest:alpha→bool.
  29   mk_TM alpha tc_states
  30   (λp.let 〈q,a〉 ≝ p in
  31    match a with
  32    [ None ⇒ 〈1, None ?〉
  33    | Some a' ⇒
  34      match test a' with
  35      [ true ⇒ 〈1,None ?〉
  36      | false ⇒ 〈2,None ?〉 ]])
  37   O (λx.notb (x == 0)).
  38
  39 definition Rtc_true ≝
  40   λalpha,test,t1,t2.
  41    ∀c. current alpha t1 = Some ? c →
  42    test c = true ∧ t2 = t1.
  43
  44 definition Rtc_false ≝
  45   λalpha,test,t1,t2.
  46     ∀c. current alpha t1 = Some ? c →
  47     test c = false ∧ t2 = t1.
  48
  49 lemma tc_q0_q1 :
  50   ∀alpha,test,ls,a0,rs. test a0 = true →
  51   step alpha (test_char alpha test)
  52     (mk_config ?? 0 (midtape … ls a0 rs)) =
  53   mk_config alpha (states ? (test_char alpha test)) 1
  54     (midtape … ls a0 rs).
  55 #alpha #test #ls #a0 #ts #Htest normalize >Htest %
  56 qed.
  57
  58 lemma tc_q0_q2 :
  59   ∀alpha,test,ls,a0,rs. test a0 = false →
  60   step alpha (test_char alpha test)
  61     (mk_config ?? 0 (midtape … ls a0 rs)) =
  62   mk_config alpha (states ? (test_char alpha test)) 2
  63     (midtape … ls a0 rs).
  64 #alpha #test #ls #a0 #ts #Htest normalize >Htest %
  65 qed.
  66
  67 lemma sem_test_char :
  68   ∀alpha,test.
  69   accRealize alpha (test_char alpha test)
  70     1 (Rtc_true alpha test) (Rtc_false alpha test).
  71 #alpha #test *
  72 [ @(ex_intro ?? 2)
  73   @(ex_intro ?? (mk_config ?? 1 (niltape ?))) %
  74   [ % // #_ #c normalize #Hfalse destruct | #_ #c normalize #Hfalse destruct (Hfalse) ]
  75 | #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? 1 (leftof ? a al)))
  76   % [ % // #_ #c normalize #Hfalse destruct | #_ #c normalize #Hfalse destruct (Hfalse) ]
  77 | #a #al @(ex_intro ?? 2) @(ex_intro ?? (mk_config ?? 1 (rightof ? a al)))
  78   % [ % // #_ #c normalize #Hfalse destruct | #_ #c normalize #Hfalse destruct (Hfalse) ]
  79 | #ls #c #rs @(ex_intro ?? 2)
  80   cases (true_or_false (test c)) #Htest
  81   [ @(ex_intro ?? (mk_config ?? 1 ?))
  82     [| %
  83       [ %
  84         [ whd in ⊢ (??%?); >tc_q0_q1 //
  85         | #_ #c0 #Hc0 % // normalize in Hc0; destruct // ]
  86       | * #Hfalse @False_ind @Hfalse % ]
  87     ]
  88   | @(ex_intro ?? (mk_config ?? 2 (midtape ? ls c rs)))
  89     %
  90     [ %
  91       [ whd in ⊢ (??%?); >tc_q0_q2 //
  92       | #Hfalse destruct (Hfalse) ]
  93     | #_ #c0 #Hc0 % // normalize in Hc0; destruct (Hc0) //
  94     ]
  95   ]
  96 ]
  97 qed.