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/notation/relations/predicate_f_1.ma".
16 include "ground/relocation/gr_fcla.ma".
18 (* FINITE COLENGTH CONDITION FOR GENERIC RELOCATION MAPS *)
21 definition gr_isf: predicate gr_map ā
22 Ī»f. ān. šāŖfā« ā n.
25 "finite colength condition (generic relocation maps)"
26 'PredicateF f = (gr_isf f).
28 (* Basic eliminators ********************************************************)
31 lemma gr_isf_ind (Q:predicate ā¦):
32 (āf. šāŖfā« ā Q f) ā
33 (āf. š
āŖfā« ā Q f ā Q (ā«Æf)) ā
34 (āf. š
āŖfā« ā Q f ā Q (āf)) ā
35 āf. š
āŖfā« ā Q f.
36 #Q #IH1 #IH2 #IH3 #f #H elim H -H
37 #n #H elim H -f -n /3 width=2 by ex_intro/
40 (* Basic inversion lemmas ***************************************************)
42 (*** isfin_inv_push *)
43 lemma gr_isf_inv_push (g): š
āŖgā« ā āf. ā«Æf = g ā š
āŖfā«.
44 #g * /3 width=4 by gr_fcla_inv_push, ex_intro/
47 (*** isfin_inv_next *)
48 lemma gr_isf_inv_next (g): š
āŖgā« ā āf. āf = g ā š
āŖfā«.
49 #g * #n #H #f #H0 elim (gr_fcla_inv_next ā¦ H ā¦ H0) -g
50 /2 width=2 by ex_intro/
53 (* Basic properties *********************************************************)
56 lemma gr_isf_isi (f): šāŖfā« ā š
āŖfā«.
57 /3 width=2 by gr_fcla_isi, ex_intro/ qed.
60 lemma gr_isf_push (f): š
āŖfā« ā š
āŖā«Æfā«.
61 #f * /3 width=2 by gr_fcla_push, ex_intro/
65 lemma gr_isf_next (f): š
āŖfā« ā š
āŖāfā«.
66 #f * /3 width=2 by gr_fcla_next, ex_intro/