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 "ground_2/notation/relations/isuniform_1.ma".
16 include "ground_2/relocation/rtmap_isfin.ma".
18 (* RELOCATION MAP ***********************************************************)
20 inductive isuni: predicate rtmap ā
21 | isuni_isid: āf. šāŖfā« ā isuni f
22 | isuni_next: āf. isuni f ā āg. āf = g ā isuni g
25 interpretation "test for uniformity (rtmap)"
26 'IsUniform f = (isuni f).
28 (* Basic inversion lemmas ***************************************************)
30 lemma isuni_inv_push: āg. šāŖgā« ā āf. ā«Æf = g ā šāŖfā«.
31 #g * -g /2 width=3 by isid_inv_push/
32 #f #_ #g #H #x #Hx destruct elim (discr_push_next ā¦ Hx)
35 lemma isuni_inv_next: āg. šāŖgā« ā āf. āf = g ā šāŖfā«.
37 [ #x #Hx elim (isid_inv_next ā¦ Hf ā¦ Hx)
38 | #g #H #x #Hx destruct /2 width=1 by injective_push/
42 lemma isuni_split: āg. šāŖgā« ā (āāf. šāŖfā« & ā«Æf = g) āØ (āāf.šāŖfā« & āf = g).
43 #g #H elim (pn_split g) * #f #Hf
44 /4 width=3 by isuni_inv_next, isuni_inv_push, or_introl, or_intror, ex2_intro/
47 (* basic forward lemmas *****************************************************)
49 lemma isuni_fwd_push: āg. šāŖgā« ā āf. ā«Æf = g ā šāŖfā«.
50 /3 width=3 by isuni_inv_push, isuni_isid/ qed-.
52 (* Forward lemmas with test for finite colength *****************************)
54 lemma isuni_fwd_isfin: āf. šāŖfā« ā š
āŖfā«.
55 #f #H elim H -f /3 width=1 by isfin_next, isfin_isid/