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 | comma : unialpha
  24 | bar : unialpha
  25 | grid : unialpha.
  26
  27 definition unialpha_eq ≝
  28   λa1,a2.match a1 with
  29   [ bit x ⇒ match a2 with [ bit y ⇒ ¬ xorb x y | _ ⇒ false ]
  30   | comma ⇒ match a2 with [ comma ⇒ true | _ ⇒ false ]
  31   | bar ⇒ match a2 with [ bar ⇒ true | _ ⇒ false ]
  32   | grid ⇒ match a2 with [ grid ⇒ true | _ ⇒ false ] ].
  33
  34 definition DeqUnialpha ≝ mk_DeqSet unialpha unialpha_eq ?.
  35 * [ #x * [ #y cases x cases y normalize % // #Hfalse destruct
  36          | *: normalize % #Hfalse destruct ]
  37   |*: * [1,5,9,13: #y ] normalize % #H1 destruct % ]
  38 qed.
  39
  40 axiom unialpha_unique : uniqueb DeqUnialpha [bit true;bit false;comma;bar;grid] = true.
  41
  42 definition FSUnialpha ≝
  43   mk_FinSet DeqUnialpha [bit true;bit false;comma;bar;grid] unialpha_unique.
  44
  45 definition is_bit ≝ λc.match c with [ bit _ ⇒ true | _ ⇒ false ].
  46
  47 definition is_grid ≝ λc.match c with [ grid ⇒ true | _ ⇒ false ].
  48
  49 definition is_bar ≝ λc.match c with [ bar ⇒ true | _ ⇒ false ].
  50
  51 definition is_comma ≝ λc.match c with [ comma ⇒ true | _ ⇒ false ].
  52