]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/lib/turing/multi_universal/par_test.ma
unistep_aux
[helm.git] / matita / matita / lib / turing / multi_universal / par_test.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/turing.ma".
13 include "turing/inject.ma".
14 include "turing/while_multi.ma".
15
16 definition partest_states ≝ initN 3.
17
18 definition partest0 : partest_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 3 (refl …)).
19 definition partest1 : partest_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 3 (refl …)).
20 definition partest2 : partest_states ≝ mk_Sig ?? 2 (leb_true_to_le 3 3 (refl …)).
21
22 definition trans_partest ≝ 
23  λsig,n,test.
24  λp:partest_states × (Vector (option sig) (S n)).
25  let 〈q,a〉 ≝ p in
26  if test a then 〈partest1,null_action sig n〉 
27  else 〈partest2,null_action ? n〉.
28
29 definition partest ≝ 
30   λsig,n,test.
31   mk_mTM sig n partest_states (trans_partest sig n test) 
32     partest0 (λq.q == partest1 ∨ q == partest2).
33
34 definition R_partest_true ≝ 
35   λsig,n,test.λint,outt: Vector (tape sig) (S n).
36   test (current_chars ?? int) = true ∧ outt = int.
37   
38 definition R_partest_false ≝ 
39   λsig,n,test.λint,outt: Vector (tape sig) (S n).
40   test (current_chars ?? int) = false ∧ outt = int.
41
42 lemma partest_q0_q1:
43   ∀sig,n,test,v.
44   test (current_chars ?? v) = true → 
45   step sig n (partest sig n test)(mk_mconfig ??? partest0 v) 
46     = mk_mconfig ??? partest1 v.
47 #sig #n #test #v #Htest
48 whd in ⊢ (??%?); >(eq_pair_fst_snd … (trans ????)) whd in ⊢ (??%?);
49 @eq_f2
50 [ whd in ⊢ (??(???%)?); >Htest %
51 | whd in ⊢ (??(????(???%))?); >Htest @tape_move_null_action ]
52 qed.
53
54 lemma partest_q0_q2:
55   ∀sig,n,test,v.
56   test (current_chars ?? v) = false → 
57   step sig n (partest sig n test)(mk_mconfig ??? partest0 v) 
58     = mk_mconfig ??? partest2 v.
59 #sig #n #test #v #Htest
60 whd in ⊢ (??%?); >(eq_pair_fst_snd … (trans ????)) whd in ⊢ (??%?);
61 @eq_f2
62 [ whd in ⊢ (??(???%)?); >Htest %
63 | whd in ⊢ (??(????(???%))?); >Htest @tape_move_null_action ]
64 qed.
65
66 lemma sem_partest:
67   ∀sig,n,test.
68   partest sig n test ⊨ 
69     [ partest1: R_partest_true sig n test, R_partest_false sig n test ].
70 #sig #n #test #int
71 cases (true_or_false (test (current_chars ?? int))) #Htest
72 [ %{2} %{(mk_mconfig ? partest_states n partest1 int)} %
73   [ % [ whd in ⊢ (??%?); >partest_q0_q1 /2/ | #_ % // ] 
74   | * #H @False_ind @H %
75   ]
76 | %{2} %{(mk_mconfig ? partest_states n partest2 int)} %
77   [ % [ whd in ⊢ (??%?); >partest_q0_q2 /2/ 
78       | whd in ⊢ (??%%→?); #H destruct (H)]
79   | #_ % //]
80 ]
81 qed.