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_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/