Added in basics

[helm.git] / matita / matita / lib / turing / turing_old.ma

diff --git a/matita/matita/lib/turing/turing_old.ma b/matita/matita/lib/turing/turing_old.ma
new file mode 100644 (file)
index 0000000..f504269
--- /dev/null
+++ b/matita/matita/lib/turing/turing_old.ma
@@ -0,0 +1,119 @@
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic   
+    ||A||  Library of Mathematics, developed at the Computer Science 
+    ||T||  Department of the University of Bologna, Italy.           
+    ||I||                                                            
+    ||T||  
+    ||A||  
+    \   /  This file is distributed under the terms of the       
+     \ /   GNU General Public License Version 2   
+      V_____________________________________________________________*)
+
+include "basics/finset.ma".
+
+record Vector (A:Type[0]) (n:nat): Type[0] ≝ 
+{ vec :> list A;
+  len: length ? vec = n
+}.
+
+record TM (sig:FinSet): Type[1] ≝ 
+{ states : FinSet;
+  tapes_no: nat;
+  trans : states × (option sig) × (Vector (option sig) tapes_no) → 
+    states × bool × (Vector (list sig) tapes_no);
+  start: states;
+  halt : states
+}.
+
+definition config ≝ λsig.λM:TM sig.
+  states sig M × (list sig) × (Vector (list sig) (tapes_no sig M)).
+
+definition option_hd ≝ λA.λl:list A.
+  match l with
+  [nil ⇒ None ?
+  |cons a _ ⇒ Some ? a
+  ].
+
+lemma length_tail: ∀A,l. length ? (tail A l) = pred (length ? l).
+#A #l elim l // 
+qed.
+
+definition vec_tail ≝ λA.λn.λv:Vector A n.
+mk_Vector A (pred n) (tail A v) ?.
+>length_tail >(len A n v) //
+qed.
+
+definition vec_cons ≝ λA.λa.λn.λv:Vector A n.
+mk_Vector A (S n) (cons A a v) ?.
+normalize >(len A n v) //
+qed.
+
+lemma length_map: ∀A,B,l.∀f:A→B. length ? (map ?? f l) = length ? l.
+#A #B #l #f elim l // #a #tl #Hind normalize //
+qed.
+
+definition vec_map ≝ λA,B.λf:A→B.λn.λv:Vector A n.
+mk_Vector B n (map ?? f v) 
+  (trans_eq … (length_map …) (len A n v)).
+  
+definition hds ≝ λsig.λM.λc:config sig M. vec_map ?? (option_hd ?) (tapes_no sig M) (\snd c).
+
+definition tls ≝ λsig.λM.λc:config sig M.vec_map ?? (tail ?) (tapes_no sig M) (\snd c).
+
+let rec compose A B C (f:A→B→C) l1 l2 on l1 ≝
+   match l1 with
+   [ nil ⇒ nil C
+   | cons a tlA ⇒ 
+     match l2 with
+     [nil ⇒ nil C
+     |cons b tlB ⇒ (f a b)::compose A B C f tlA tlB
+     ]
+   ].
+
+lemma length_compose: ∀A,B,C.∀f:A→B→C.∀l1,l2.
+length C (compose  A B C f l1 l2) = 
+  min (length A l1) (length B l2).
+#A #B #C #f #l1 elim l1 // #a #tlA #Hind #l2 cases l2 //
+#b #tlB lapply (Hind tlB) normalize 
+cases (true_or_false (leb (length A tlA) (length B tlB))) #H >H
+normalize //
+qed.
+
+definition compose_vec ≝ λA,B,C.λf:A→B→C.λn.λvA:Vector A n.λvB:Vector B n.
+mk_Vector C n (compose A B C f vA vB) ?.
+>length_compose >(len A n vA) >(len B n vB) normalize 
+>(le_to_leb_true … (le_n n)) //
+qed.
+
+definition step ≝ λsig.λM:TM sig.λc:config sig M.
+  match (trans sig M 〈〈\fst (\fst c),option_hd ? (\snd (\fst c))〉,hds sig M c〉) with
+  [mk_Prod p l ⇒ 
+    let work_tapes ≝ compose_vec ??? (append ?) (tapes_no sig M) l (tls sig M c) in
+    match p with 
+    [mk_Prod s b ⇒ 
+      let old_input ≝ \snd (\fst c) in
+      let input ≝ if b then tail ? old_input else  old_input in
+      〈〈s,input〉,work_tapes〉]].
+
+definition empty_tapes ≝ λsig.λM:TM sig.
+mk_Vector ? (tapes_no sig M) (make_list (list sig) [ ] (tapes_no sig M)) ?.
+elim (tapes_no sig M) // normalize //
+qed.
+
+definition init ≝ λsig.λM:TM sig.λi:(list sig).
+  〈〈start sig M,i〉,empty_tapes sig M〉.
+
+definition stop ≝ λsig.λM:TM sig.λc:config sig M.
+  eqb (states sig M) (\fst(\fst c)) (halt sig M).
+
+let rec loop (A:Type[0]) n (f:A→A) p a on n ≝
+  match n with 
+  [ O ⇒ None ?
+  | S m ⇒ if p a then (Some ? a) else loop A m f p (f a)
+  ].
+
+definition Compute ≝ λsig.λM:TM sig.λf:(list sig) → (list sig).
+∀l.∃i.∃c.((loop ? i (step sig M) (stop sig M) (init sig M l) = Some ? c) ∧
+  (hd ? (\snd c) [ ] = f l)).
+
+(* An extended machine *)
\ No newline at end of file