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
21 definition unialpha_eq ≝
23 [ bit x ⇒ match a2 with [ bit y ⇒ ¬ xorb x y | _ ⇒ false ]
24 | bar ⇒ match a2 with [ bar ⇒ true | _ ⇒ false ] ].
26 definition DeqUnialpha ≝ mk_DeqSet unialpha unialpha_eq ?.
27 * [ #x * [ #y cases x cases y normalize % // #Hfalse destruct
28 | *: normalize % #Hfalse destruct ]
29 | * [ #y ] normalize % #H1 destruct % ]
32 lemma unialpha_unique :
33 uniqueb DeqUnialpha [bit true;bit false;bar] = true.
36 lemma unialpha_complete :∀x:DeqUnialpha.
37 memb ? x [bit true;bit false;bar] = true.
41 definition FSUnialpha ≝
42 mk_FinSet DeqUnialpha [bit true;bit false;bar]
43 unialpha_unique unialpha_complete.
45 (*************************** testing characters *******************************)
46 definition is_bit ≝ λc.match c with [ bit _ ⇒ true | _ ⇒ false ].
47 definition is_bar ≝ λc.match c with [ bar ⇒ true | _ ⇒ false ].