matita/matita/lib/turing/universal/alphabet.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
  13 (* ALphabet of the universal machine *)
  14
  15 include "basics/finset.ma".
  16
  17 (*
  18 include "turing/if_machine.ma".
  19 include "turing/universal/tests.ma". *)
  20
  21 inductive unialpha : Type[0] ≝
  22 | bit : bool → unialpha
  23 | null : unialpha
  24 | comma : unialpha
  25 | bar : unialpha
  26 | grid : unialpha.
  27
  28 definition unialpha_eq ≝
  29   λa1,a2.match a1 with
  30   [ bit x ⇒ match a2 with [ bit y ⇒ ¬ xorb x y | _ ⇒ false ]
  31   | null ⇒ match a2 with [ null ⇒ true | _ ⇒ false ]
  32   | comma ⇒ match a2 with [ comma ⇒ true | _ ⇒ false ]
  33   | bar ⇒ match a2 with [ bar ⇒ true | _ ⇒ false ]
  34   | grid ⇒ match a2 with [ grid ⇒ true | _ ⇒ false ] ].
  35
  36 definition DeqUnialpha ≝ mk_DeqSet unialpha unialpha_eq ?.
  37 * [ #x * [ #y cases x cases y normalize % // #Hfalse destruct
  38          | *: normalize % #Hfalse destruct ]
  39   |*: * [1,6,11,16: #y ] normalize % #H1 destruct % ]
  40 qed.
  41
  42 lemma unialpha_unique :
  43   uniqueb DeqUnialpha [bit true;bit false;null;comma;bar;grid] = true.
  44 // qed.
  45
  46 lemma unialpha_complete :∀x:DeqUnialpha.
  47   memb ? x [bit true;bit false;null;comma;bar;grid] = true.
  48 * // * //
  49 qed.
  50
  51 definition FSUnialpha ≝
  52   mk_FinSet DeqUnialpha [bit true;bit false;null;comma;bar;grid]
  53   unialpha_unique unialpha_complete.
  54
  55 (*************************** testing characters *******************************)
  56 definition is_bit ≝ λc.match c with [ bit _ ⇒ true | _ ⇒ false ].
  57
  58 definition is_null ≝ λc.match c with [ null ⇒ true | _ ⇒ false ].
  59
  60 definition is_grid ≝ λc.match c with [ grid ⇒ true | _ ⇒ false ].
  61
  62 definition is_bar ≝ λc.match c with [ bar ⇒ true | _ ⇒ false ].
  63
  64 definition is_comma ≝ λc.match c with [ comma ⇒ true | _ ⇒ false ].
  65
  66 definition bit_or_null ≝ λc.is_bit c ∨ is_null c.
  67
  68 lemma bit_not_grid: ∀d. is_bit d = true → is_grid d = false.
  69 * // normalize #H destruct
  70 qed.
  71
  72 lemma bit_or_null_not_grid: ∀d. bit_or_null d = true → is_grid d = false.
  73 * // normalize #H destruct
  74 qed.
  75
  76 lemma bit_not_bar: ∀d. is_bit d = true → is_bar d = false.
  77 * // normalize #H destruct
  78 qed.
  79
  80 lemma bit_or_null_not_bar: ∀d. bit_or_null d = true → is_bar d = false.
  81 * // normalize #H destruct
  82 qed.
  83
  84 lemma is_bit_to_bit_or_null :
  85   ∀x.is_bit x = true → bit_or_null x = true.
  86 * // normalize #H destruct
  87 qed.
  88
  89 (**************************** testing strings *********************************)
  90 definition is_marked ≝ λalpha.λp:FinProd … alpha FinBool.
  91   let 〈x,b〉 ≝ p in b.
  92
  93 definition STape ≝ FinProd … FSUnialpha FinBool.
  94
  95 definition only_bits ≝ λl.
  96   ∀c.memb STape c l = true → is_bit (\fst c) = true.
  97
  98 definition only_bits_or_nulls ≝ λl.
  99   ∀c.memb STape c l = true → bit_or_null (\fst c) = true.
 100
 101 definition no_grids ≝ λl.
 102   ∀c.memb STape c l = true → is_grid (\fst c) = false.
 103
 104 definition no_bars ≝ λl.
 105   ∀c.memb STape c l = true → is_bar (\fst c) = false.
 106
 107 definition no_marks ≝ λl.
 108   ∀c.memb STape c l = true → is_marked ? c = false.
 109
 110 definition bar_or_grid ≝ λc:STape.is_bar (\fst c) ∨ is_grid (\fst c).
 111