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.
8 \ / This file is distributed under the terms of the
9 \ / GNU General Public License Version 2
10 V_____________________________________________________________*)
12 include "basics/finset.ma".
13 include "basics/lists/list.ma".
15 inductive unialpha : Type[0] ≝
16 | bit : bool → unialpha
20 definition unialpha_eq ≝
22 [ bit x ⇒ match a2 with [ bit y ⇒ ¬ xorb x y | _ ⇒ false ]
23 | bar ⇒ match a2 with [ bar ⇒ true | _ ⇒ false ]
24 | null ⇒ match a2 with [ null ⇒ 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 | *: * [1,4: #y ] normalize % #H1 destruct % ]
32 lemma unialpha_unique :
33 uniqueb DeqUnialpha [bit true;bit false;null;bar] = true.
36 lemma unialpha_complete :∀x:DeqUnialpha.
37 memb ? x [bit true;bit false;null;bar] = true.
41 definition FSUnialpha ≝
42 mk_FinSet DeqUnialpha [bit true;bit false;null;bar]
43 unialpha_unique unialpha_complete.
45 unification hint 0 ≔ ;
47 (* ---------------------------------------- *) ⊢
48 unialpha ≡ FinSetcarr X.
50 (*************************** testing characters *******************************)
51 definition is_bit ≝ λc.match c with [ bit _ ⇒ true | _ ⇒ false ].
52 definition is_bar ≝ λc:DeqUnialpha. c == bar.
53 definition is_null ≝ λc:DeqUnialpha. c == null.
55 definition only_bits ≝ λl.
56 ∀c.mem ? c l → is_bit c = true.
58 definition no_bars ≝ λl.
59 ∀c.mem ? c l → is_bar c = false.