include "turing/multi_universal/alphabet.ma".
include "turing/mono.ma".
-(************************* turning DeqMove into a DeqSet **********************)
-definition move_eq ≝ λm1,m2:move.
- match m1 with
- [R ⇒ match m2 with [R ⇒ true | _ ⇒ false]
- |L ⇒ match m2 with [L ⇒ true | _ ⇒ false]
- |N ⇒ match m2 with [N ⇒ true | _ ⇒ false]].
-
-lemma move_eq_true:∀m1,m2.
- move_eq m1 m2 = true ↔ m1 = m2.
-*
- [* normalize [% #_ % |2,3: % #H destruct ]
- |* normalize [1,3: % #H destruct |% #_ % ]
- |* normalize [1,2: % #H destruct |% #_ % ]
-qed.
-
-definition DeqMove ≝ mk_DeqSet move move_eq move_eq_true.
-
-unification hint 0 ≔ ;
- X ≟ DeqMove
-(* ---------------------------------------- *) ⊢
- move ≡ carr X.
-
-unification hint 0 ≔ m1,m2;
- X ≟ DeqMove
-(* ---------------------------------------- *) ⊢
- move_eq m1 m2 ≡ eqb X m1 m2.
-
-
-(************************ turning DeqMove into a FinSet ***********************)
-definition move_enum ≝ [L;R;N].
-
-lemma move_enum_unique: uniqueb ? [L;R;N] = true.
-// qed.
-
-lemma move_enum_complete: ∀x:move. memb ? x [L;R;N] = true.
-* // qed.
-
-definition FinMove ≝
- mk_FinSet DeqMove [L;R;N] move_enum_unique move_enum_complete.
-
-unification hint 0 ≔ ;
- X ≟ FinMove
-(* ---------------------------------------- *) ⊢
- move ≡ FinSetcarr X.
-
(*************************** normal Turing Machines ***************************)
(* A normal turing machine is just an ordinary machine where:
nhalt : initN no_states → bool
}.
+lemma decomp_target : ∀n.∀tg: trans_target n.
+ ∃qout,cout,m. tg = 〈qout,cout,m〉.
+#n * * #q #c #m %{q} %{c} %{m} //
+qed.
+
(* A normal machine is just a special case of Turing Machine. *)
+definition nstart_state ≝ λM.mk_Sig ?? 0 (pos_no_states M).
+
definition normalTM_to_TM ≝ λM:normalTM.
mk_TM FinBool (initN (no_states M))
- (ntrans M) (mk_Sig ?? 0 (pos_no_states M)) (nhalt M).
+ (ntrans M) (nstart_state M) (nhalt M).
coercion normalTM_to_TM.
definition nconfig ≝ λn. config FinBool (initN n).
+(* A normal machine has a non empty graph *)
+
+definition sample_input: ∀M.trans_source (no_states M).
+#M % [@(nstart_state M) | %]
+qed.
+
+lemma nTM_nog: ∀M. graph_enum ?? (ntrans M) ≠ [ ].
+#M % #H lapply(graph_enum_complete ?? (ntrans M) (sample_input M) ? (refl ??))
+>H normalize #Hd destruct
+qed.
+
(******************************** tuples **************************************)
(* By general results on FinSets we know that every function f between two
| N ⇒ null
].
+lemma injective_low_char: injective … low_char.
+#c1 #c2 cases c1 cases c2 normalize //
+ [#b1 #H destruct
+ |#b1 #H destruct
+ |#b1 #b2 #H destruct //
+ ]
+qed.
+
+lemma injective_low_mv: injective … low_mv.
+#m1 #m2 cases m1 cases m2 // normalize #H destruct
+qed.
+
(******************************** tuple encoding ******************************)
definition tuple_type ≝ λn.
(Nat_to n × (option FinBool)) × (Nat_to n × (option FinBool) × move).