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 ≝
23 interpretation "test for finite colength (rtmap)"
24 'IsFinite f = (isfin f).
26 (* Basic eliminators ********************************************************)
28 lemma isfin_ind (R:predicate rtmap): (∀f. 𝐈⦃f⦄ → R f) →
29 (∀f. 𝐅⦃f⦄ → R f → R (⫯f)) →
30 (∀f. 𝐅⦃f⦄ → R f → R (↑f)) →
32 #R #IH1 #IH2 #IH3 #f #H elim H -H
33 #n #H elim H -f -n /3 width=2 by ex_intro/
36 (* Basic inversion lemmas ***************************************************)
38 lemma isfin_inv_push: ∀g. 𝐅⦃g⦄ → ∀f. ⫯f = g → 𝐅⦃f⦄.
39 #g * /3 width=4 by fcla_inv_px, ex_intro/
42 lemma isfin_inv_next: ∀g. 𝐅⦃g⦄ → ∀f. ↑f = g → 𝐅⦃f⦄.
43 #g * #n #H #f #H0 elim (fcla_inv_nx … H … H0) -g
44 /2 width=2 by ex_intro/
47 (* Basic properties *********************************************************)
49 lemma isfin_eq_repl_back: eq_repl_back … isfin.
50 #f1 * /3 width=4 by fcla_eq_repl_back, ex_intro/
53 lemma isfin_eq_repl_fwd: eq_repl_fwd … isfin.
54 /3 width=3 by isfin_eq_repl_back, eq_repl_sym/ qed-.
56 lemma isfin_isid: ∀f. 𝐈⦃f⦄ → 𝐅⦃f⦄.
57 /3 width=2 by fcla_isid, ex_intro/ qed.
59 lemma isfin_push: ∀f. 𝐅⦃f⦄ → 𝐅⦃⫯f⦄.
60 #f * /3 width=2 by fcla_push, ex_intro/
63 lemma isfin_next: ∀f. 𝐅⦃f⦄ → 𝐅⦃↑f⦄.
64 #f * /3 width=2 by fcla_next, ex_intro/
67 (* Properties with iterated push ********************************************)
69 lemma isfin_pushs: ∀n,f. 𝐅⦃f⦄ → 𝐅⦃⫯*[n]f⦄.
70 #n elim n -n /3 width=3 by isfin_push/
73 (* Inversion lemmas with iterated push **************************************)
75 lemma isfin_inv_pushs: ∀n,g. 𝐅⦃⫯*[n]g⦄ → 𝐅⦃g⦄.
76 #n elim n -n /3 width=3 by isfin_inv_push/
79 (* Properties with tail *****************************************************)
81 lemma isfin_tl: ∀f. 𝐅⦃f⦄ → 𝐅⦃⫱f⦄.
82 #f elim (pn_split f) * #g #H #Hf destruct
83 /3 width=3 by isfin_inv_push, isfin_inv_next/
86 (* Inversion lemmas with tail ***********************************************)
88 lemma isfin_inv_tl: ∀f. 𝐅⦃⫱f⦄ → 𝐅⦃f⦄.
89 #f elim (pn_split f) * /2 width=1 by isfin_next, isfin_push/
92 (* Inversion lemmas with iterated tail **************************************)
94 lemma isfin_inv_tls: ∀n,f. 𝐅⦃⫱*[n]f⦄ → 𝐅⦃f⦄.
95 #n elim n -n /3 width=1 by isfin_inv_tl/