X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Flib%2Fturing%2Fmulti_universal%2Ftuples.ma;h=4a7f2b5f2b77ba556cdaddc76fd6b3b91b234769;hb=2002da6bcdbf12203a87a7d9630d738f67ede68c;hp=76e56068df9303450f7d7c179b3daf0eb0576827;hpb=1f740f74d94187a2376228a86faf79ea949c0dff;p=helm.git
diff --git a/matita/matita/lib/turing/multi_universal/tuples.ma b/matita/matita/lib/turing/multi_universal/tuples.ma
index 76e56068d..4a7f2b5f2 100644
--- a/matita/matita/lib/turing/multi_universal/tuples.ma
+++ b/matita/matita/lib/turing/multi_universal/tuples.ma
@@ -21,8 +21,30 @@ lemma table_TM_cons: ân,h,t,o.
table_TM n (t::o) h = (tuple_encoding n h t)@(table_TM n o h).
// qed.
+lemma initial_bar: ân,h,l. l â [ ] â
+ table_TM n l h = bar :: tail ? (table_TM n l h).
+#n #h *
+ [* #H @False_ind @H //
+ |#a #tl #_ >table_TM_cons lapply (is_tuple n h a)
+ * #qin * #cin * #qout * #cout * #mv * #_ #Htup >Htup %
+ ]
+qed.
+
(************************** matching in a table *******************************)
-lemma list_to_table: ân,l,h,tup. mem ? tup (tuples_list n h l) â
+lemma list_to_table: ân,l,h,t. mem ? t l â
+ âll,lr.table_TM n l h = ll@(tuple_encoding n h t)@lr.
+#n #l #h #t elim l
+ [@False_ind
+ |#hd #tl #Hind *
+ [#Htup %{[]} %{(table_TM n tl h)} >Htup %
+ |#H cases (Hind H) #ll * #lr #H1
+ %{((tuple_encoding n h hd)@ll)} %{lr}
+ >associative_append
Heq1 >(cons_injective_l ????? Heq) //
- |%2 % // >Heq1 >(cons_injective_l ????? Heq) //
- ]
- |@(cons_injective_r ????? Heq)
- ]
- ]
- ]
-qed.
-
lemma table_to_list: ân,l,h,c. is_config n c â
- (âll,lr.table_TM n l h = ll@c@lr) â
- âout,t. tuple_encoding n h t = (c@out) ⧠mem ? t l.
+ âll,lr.table_TM n l h = ll@c@lr â
+ âout,lr0,t. lr = out@lr0 ⧠tuple_encoding n h t = (c@out) ⧠mem ? t l.
#n #l #h #c * #qin * #cin * * * #H1 #H2 #H3 #H4
- * #ll * #lr lapply ll -ll elim l
+#ll #lr lapply ll -ll elim l
[>H4 #ll cases ll normalize [|#hd #tl ] #Habs destruct
|#t1 #othert #Hind #ll >table_TM_cons #Htuple
cut (S n < |ll@c@lr|)
@@ -80,8 +85,8 @@ lemma table_to_list: ân,l,h,c. is_config n c â
normalize in ⢠(???%â?); whd in ⢠(??%?â?); #Htemp
lapply (cons_injective_l ????? Htemp) #Hc1
lapply (cons_injective_r ????? Htemp) -Htemp #Heq2
- %{(q2@[c2;m])} %{t1} %
- [>Ht1 >Heq1 >Hc1 @eq_f >associative_append %
+ %{(q2@[c2;m])} %{(table_TM n othert h)} %{t1} %
+ [ %[ // |>Ht1 >Heq1 >Hc1 @eq_f >associative_append % ]
|%1 %
]
|(* ll not nil *)
@@ -89,8 +94,9 @@ lemma table_to_list: ân,l,h,c. is_config n c â
whd in ⢠(??%?â?); #Heq destruct (Heq)
cases (compare_append ⦠e0) #l *
[* cases l
- [#_ #Htab cases (Hind [ ] (sym_eq ⦠Htab)) #out * #t * #Ht #Hmemt
- %{out} %{t} % // %2 //
+ [#_ #Htab cases (Hind [ ] (sym_eq ⦠Htab))
+ #out * #lr0 * #t * * #Hlr #Ht #Hmemt
+ %{out} %{lr0} %{t} % [% //| %2 //]
|(* this case is absurd *)
#al #tll #Heq1 >H4 #Heq2 @False_ind
lapply (cons_injective_l ? bar ⦠Heq2) #Hbar append_cons in Heq; >Hcut (append_cons ? (low_char a1)) associative_append #Heq @sym_eq @(append_l2_injective ?????? Heq)
+ >Hc whd in ⢠(??%%); @eq_f >length_append >length_append
+ @eq_f2 // >length_map >Hlen whd in ⢠(??%?); @eq_f //
+ ]
+qed.
+*)
+
+lemma tuple_to_config: ân,h,t,out,m,c. is_config n c â
+ tuple_encoding n h t = c@out@[m] â is_config n (bar::out).
+#n #h * * #q0 #a0 * * #q1 #a1 #m #out #lowm #c * #q * #a * * * #Hq #Ha #Hlen #Hc
+whd in ⢠(??%?â?); #Heq %{(bits_of_state n h q1)} %{(low_char a1)} %
+ [% [ %[ // | cases a1 [|#b] normalize % #H destruct (H)]
+ |whd in ⢠(??%?); @eq_f //]
+ |@eq_f cut (âA.âa:A.âl1,l2. a::l1@l2 = (a::l1)@l2) [//] #Hcut
+ >append_cons in Heq; >Hcut (append_cons ? (low_char a1)) associative_append #Heq @sym_eq @(append_l2_injective ?????? Heq)
+ >Hc whd in ⢠(??%%); @eq_f >length_append >length_append
+ @eq_f2 // >length_map >Hlen whd in ⢠(??%?); @eq_f //
+ ]
+qed.
+
+(* da spostare *)
+lemma injective_nat_of: ân. injective ⦠(nat_of n).
+#n * #a0 #Ha0 * #b0 #Hb0 normalize #Heq
+generalize in match Ha0; generalize in match Hb0; >Heq //
+qed.
+
+lemma not_of_lt: ân,m. nat_of n m < n.
+#n * #a #lta //
+qed.
+
+(* da spostare *)
+lemma injective_map: âA,B,f. injective A B f â injective ⦠(map ⦠f).
+#A #B #f #injf #l1 elim l1
+ [* // #a2 #l2 normalize #H destruct
+ |#a1 -l1 #l1 #Hind *
+ [normalize #H destruct
+ |#a2 #l2 normalize #Hmap
+ >(injf ⦠(cons_injective_l ????? Hmap))
+ >(Hind ⦠(cons_injective_r ????? Hmap)) %
+ ]
+ ]
+qed.
+
+lemma deterministic: âM:normalTM.âl,t1,t2,c,out1,out2.
+ l = graph_enum ?? (ntrans M) â
+ mem ? t1 l â mem ? t2 l â
+ is_config (no_states M) c â
+ tuple_encoding ? (nhalt M) t1 = (c@out1) â
+ tuple_encoding ? (nhalt M) t2 = (c@out2) â
+ out1 = out2.
+#M #l * * #q1 #a1 * * #q11 #a11 #m1
+* * #q2 #a2 * * #q21 #a21 #m2 #c #out1 #out2 #Hl #memt1 #memt2 *
+#state * #char * * * #_ #_ #Hlen #Heqc #tuplet1 #tuplet2
+lapply (mem_to_memb ⦠memt1) >Hl #membt1
+lapply (graph_enum_correct ?? (ntrans M) ?? membt1) #Ht1
+lapply (mem_to_memb ⦠memt2) >Hl #membt2
+lapply (graph_enum_correct ?? (ntrans M) ?? membt2) #Ht2
+cut (bar::bits_of_state (no_states M) (nhalt M) q1@[low_char a1]=c)
+ [whd in tuplet1:(??%?); >(append_cons ? (low_char a1)) in tuplet1; #tuplet1
+ @(append_l1_injective ? (bar::bits_of_state ?? q1@[low_char a1]) ???? tuplet1)
+ >Heqc whd in ⢠(??%%); @eq_f >length_append >length_append
+ @eq_f2 // >length_map whd in ⢠(??%?); >Hlen @eq_f
+ >bitlist_length %] #Hcfg1
+cut (bar::bits_of_state (no_states M) (nhalt M) q2@[low_char a2]=c)
+ [whd in tuplet2:(??%?); >(append_cons ? (low_char a2)) in tuplet2; #tuplet2
+ @(append_l1_injective ? (bar::bits_of_state ?? q2@[low_char a2]) ???? tuplet2)
+ >Heqc whd in ⢠(??%%); @eq_f >length_append >length_append
+ @eq_f2 // >length_map whd in ⢠(??%?); >Hlen @eq_f
+ >bitlist_length %] #Hcfg2
+cut (a1 = a2)
+ [@injective_low_char
+ tuplet1
+@append_l2_injective %
+qed.