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 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)) ā
31 āf. š
ā¦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_next: āg. š
ā¦gā¦ ā āf. ā«Æf = g ā š
ā¦fā¦.
39 #g * #n #H #f #H0 elim (fcla_inv_nx ā¦ H ā¦ H0) -g
40 /2 width=2 by ex_intro/
43 (* Basic forward lemmas *****************************************************)
45 lemma isfin_fwd_push: āg. š
ā¦gā¦ ā āf. āf = g ā š
ā¦fā¦.
46 #g * /3 width=4 by fcla_inv_px, ex_intro/
49 (* Basic properties *********************************************************)
51 lemma isfin_eq_repl_back: eq_repl_back ā¦ isfin.
52 #f1 * /3 width=4 by fcla_eq_repl_back, ex_intro/
55 lemma isfin_eq_repl_fwd: eq_repl_fwd ā¦ isfin.
56 /3 width=3 by isfin_eq_repl_back, eq_repl_sym/ qed-.
58 lemma isfin_isid: āf. šā¦fā¦ ā š
ā¦fā¦.
59 /3 width=2 by fcla_isid, ex_intro/ qed.
61 lemma isfin_push: āf. š
ā¦fā¦ ā š
ā¦āfā¦.
62 #f * /3 width=2 by fcla_push, ex_intro/
65 lemma isfin_next: āf. š
ā¦fā¦ ā š
ā¦ā«Æfā¦.
66 #f * /3 width=2 by fcla_next, ex_intro/
69 lemma isfin_tl: āf. š
ā¦fā¦ ā š
ā¦ā«±fā¦.
70 #f elim (pn_split f) * #g #H #Hf destruct
71 /3 width=3 by isfin_fwd_push, isfin_inv_next/
74 (* Inversion lemmas with tail ***********************************************)
76 lemma isfin_inv_tl: āf. š
ā¦ā«±fā¦ ā š
ā¦fā¦.
77 #f elim (pn_split f) * /2 width=1 by isfin_next, isfin_push/
80 (* Inversion lemmas with tls ********************************************************)
82 lemma isfin_inv_tls: ān,f. š
ā¦ā«±*[n]fā¦ ā š
ā¦fā¦.
83 #n elim n -n /3 width=1 by isfin_inv_tl/