New notation for congruence

[helm.git] / matita / matita / lib / turing / universal / alphabet.ma

diff --git a/matita/matita/lib/turing/universal/alphabet.ma b/matita/matita/lib/turing/universal/alphabet.ma
index bf2484f29fadf94ae268dc9a7dad93ec54bfafac..390bc2b839d308a6222816fc9d479e6edb3999b1 100644 (file)
--- a/matita/matita/lib/turing/universal/alphabet.ma
+++ b/matita/matita/lib/turing/universal/alphabet.ma
@@ -52,6 +52,7 @@ definition FSUnialpha ≝
   mk_FinSet DeqUnialpha [bit true;bit false;null;comma;bar;grid] 
   unialpha_unique unialpha_complete.
 
+(*************************** testing characters *******************************)
 definition is_bit ≝ λc.match c with [ bit _ ⇒ true | _ ⇒ false ].
 
 definition is_null ≝ λc.match c with [ null ⇒ true | _ ⇒ false ].
@@ -63,3 +64,48 @@ definition is_bar ≝ λc.match c with [ bar ⇒ true | _ ⇒ false ].
 definition is_comma ≝ λc.match c with [ comma ⇒ true | _ ⇒ false ].
 
 definition bit_or_null ≝ λc.is_bit c ∨ is_null c.
+
+lemma bit_not_grid: ∀d. is_bit d = true → is_grid d = false.
+* // normalize #H destruct
+qed.
+
+lemma bit_or_null_not_grid: ∀d. bit_or_null d = true → is_grid d = false.
+* // normalize #H destruct
+qed.
+
+lemma bit_not_bar: ∀d. is_bit d = true → is_bar d = false.
+* // normalize #H destruct
+qed.
+
+lemma bit_or_null_not_bar: ∀d. bit_or_null d = true → is_bar d = false.
+* // normalize #H destruct
+qed.
+
+lemma is_bit_to_bit_or_null : 
+  ∀x.is_bit x = true → bit_or_null x = true.
+* // normalize #H destruct
+qed.
+
+(**************************** testing strings *********************************)
+definition is_marked ≝ λalpha.λp:FinProd … alpha FinBool.
+  let 〈x,b〉 ≝ p in b.
+
+definition STape ≝ FinProd … FSUnialpha FinBool.
+
+definition only_bits ≝ λl.
+  ∀c.memb STape c l = true → is_bit (\fst c) = true.
+
+definition only_bits_or_nulls ≝ λl.
+  ∀c.memb STape c l = true → bit_or_null (\fst c) = true.
+  
+definition no_grids ≝ λl.
+  ∀c.memb STape c l = true → is_grid (\fst c) = false.
+
+definition no_bars ≝ λl.
+  ∀c.memb STape c l = true → is_bar (\fst c) = false.
+
+definition no_marks ≝ λl.
+  ∀c.memb STape c l = true → is_marked ? c = false.
+
+definition bar_or_grid ≝ λc:STape.is_bar (\fst c) ∨ is_grid (\fst c).
+