1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "basics/finset.ma".
17 inductive unialpha : Type[0] ≝
18 | bit : bool → unialpha
22 definition unialpha_eq ≝
24 [ bit x ⇒ match a2 with [ bit y ⇒ ¬ xorb x y | _ ⇒ false ]
25 | bar ⇒ match a2 with [ bar ⇒ true | _ ⇒ false ]
26 | null ⇒ match a2 with [ null ⇒ true | _ ⇒ false ] ].
28 definition DeqUnialpha ≝ mk_DeqSet unialpha unialpha_eq ?.
29 * [ #x * [ #y cases x cases y normalize % // #Hfalse destruct
30 | *: normalize % #Hfalse destruct ]
31 | *: * [1,4: #y ] normalize % #H1 destruct % ]
34 lemma unialpha_unique :
35 uniqueb DeqUnialpha [bit true;bit false;null;bar] = true.
38 lemma unialpha_complete :∀x:DeqUnialpha.
39 memb ? x [bit true;bit false;null;bar] = true.
43 definition FSUnialpha ≝
44 mk_FinSet DeqUnialpha [bit true;bit false;null;bar]
45 unialpha_unique unialpha_complete.
47 (*************************** testing characters *******************************)
48 definition is_bit ≝ λc.match c with [ bit _ ⇒ true | _ ⇒ false ].
49 definition is_bar ≝ λc.match c with [ bar ⇒ true | _ ⇒ false ].
50 definition is_null ≝ λc.match c with [ null ⇒ true | _ ⇒ false ].