matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_isfin.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "ground_2/notation/relations/isfinite_1.ma".
  16 include "ground_2/relocation/rtmap_fcla.ma".
  17
  18 (* RELOCATION MAP ***********************************************************)
  19
  20 definition isfin: predicate rtmap ≝
  21                   λf. ∃n. 𝐂⦃f⦄ ≡ n.
  22
  23 interpretation "test for finite colength (rtmap)"
  24    'IsFinite f = (isfin f).
  25
  26 (* Basic eliminators ********************************************************)
  27
  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/
  34 qed-.
  35
  36 (* Basic inversion lemmas ***************************************************)
  37
  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/
  41 qed-.
  42
  43 (* Basic forward lemmas *****************************************************)
  44
  45 lemma isfin_fwd_push: ∀g. 𝐅⦃g⦄ → ∀f. ↑f = g → 𝐅⦃f⦄.
  46 #g * /3 width=4 by fcla_inv_px, ex_intro/
  47 qed-.
  48
  49 (* Basic properties *********************************************************)
  50
  51 lemma isfin_eq_repl_back: eq_repl_back … isfin.
  52 #f1 * /3 width=4 by fcla_eq_repl_back, ex_intro/
  53 qed-.
  54
  55 lemma isfin_eq_repl_fwd: eq_repl_fwd … isfin.
  56 /3 width=3 by isfin_eq_repl_back, eq_repl_sym/ qed-.
  57
  58 lemma isfin_isid: ∀f. 𝐈⦃f⦄ → 𝐅⦃f⦄.
  59 /3 width=2 by fcla_isid, ex_intro/ qed.
  60
  61 lemma isfin_push: ∀f. 𝐅⦃f⦄ → 𝐅⦃↑f⦄.
  62 #f * /3 width=2 by fcla_push, ex_intro/
  63 qed.
  64
  65 lemma isfin_next: ∀f. 𝐅⦃f⦄ → 𝐅⦃⫯f⦄.
  66 #f * /3 width=2 by fcla_next, ex_intro/
  67 qed.
  68
  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/
  72 qed.
  73
  74 (* Inversion lemmas with tail ***********************************************)
  75
  76 lemma isfin_inv_tl: ∀f. 𝐅⦃⫱f⦄ → 𝐅⦃f⦄.
  77 #f elim (pn_split f) * /2 width=1 by isfin_next, isfin_push/
  78 qed-.