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/isfinite_1.ma".
16 include "ground_2/relocation/rtmap_fcla.ma".
18 (* RELOCATION MAP ***********************************************************)
20 definition isfin: predicate rtmap ā
21 Ī»f. ān. šā¦fā¦ ā” n.
23 interpretation "test for finite colength (rtmap)"
24 'IsFinite f = (isfin f).
26 (* Basic properties *********************************************************)
28 lemma isfin_isid: āf. šā¦fā¦ ā š
ā¦fā¦.
29 /3 width=2 by fcla_isid, ex_intro/ qed.
31 lemma isfin_push: āf. š
ā¦fā¦ ā š
ā¦āfā¦.
32 #f * /3 width=2 by fcla_push, ex_intro/
35 lemma isfin_next: āf. š
ā¦fā¦ ā š
ā¦ā«Æfā¦.
36 #f * /3 width=2 by fcla_next, ex_intro/
39 lemma isfin_eq_repl_back: eq_repl_back ā¦ isfin.
40 #f1 * /3 width=4 by fcla_eq_repl_back, ex_intro/
43 lemma isfin_eq_repl_fwd: eq_repl_fwd ā¦ isfin.
44 /3 width=3 by isfin_eq_repl_back, eq_repl_sym/ qed-.
46 (* Basic eliminators ********************************************************)
48 lemma isfin_ind (R:predicate rtmap): (āf. šā¦fā¦ ā R f) ā
49 (āf. š
ā¦fā¦ ā R f ā R (āf)) ā
50 (āf. š
ā¦fā¦ ā R f ā R (ā«Æf)) ā
51 āf. š
ā¦fā¦ ā R f.
52 #R #IH1 #IH2 #IH3 #f #H elim H -H
53 #n #H elim H -f -n /3 width=2 by ex_intro/
56 (* Basic inversion lemmas ***************************************************)
58 lemma isfin_inv_next: āg. š
ā¦gā¦ ā āf. ā«Æf = g ā š
ā¦fā¦.
59 #g * #n #H #f #H0 elim (fcla_inv_nx ā¦ H ā¦ H0) -g
60 /2 width=2 by ex_intro/
63 (* Basic forward lemmas *****************************************************)
65 lemma isfin_fwd_push: āg. š
ā¦gā¦ ā āf. āf = g ā š
ā¦fā¦.
66 #g * /3 width=4 by fcla_inv_px, ex_intro/