]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/ground/relocation/pr_fcla.ma
update in delayed_updating
[helm.git] / matita / matita / contribs / lambdadelta / ground / relocation / pr_fcla.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/notation/relations/rfun_c_2.ma".
16 include "ground/arith/nat_succ.ma".
17 include "ground/relocation/pr_isi.ma".
18
19 (* FINITE COLENGTH ASSIGNMENT FOR PARTIAL RELOCATION MAPS *******************)
20
21 (*** fcla *)
22 inductive pr_fcla: relation2 pr_map nat ā‰
23 (*** fcla_isid *)
24 | pr_fcla_isi (f): šˆāØfā© ā†’ pr_fcla f (šŸŽ)
25 (*** fcla_push *)
26 | pr_fcla_push (f) (n): pr_fcla f n ā†’ pr_fcla (ā«Æf) n
27 (*** fcla_next *)
28 | pr_fcla_next (f) (n): pr_fcla f n ā†’ pr_fcla (ā†‘f) (ā†‘n)
29 .
30
31 interpretation
32   "finite colength assignment (partial relocation maps)"
33   'RFunC f n = (pr_fcla f n).
34
35 (* Basic inversions *********************************************************)
36
37 (*** fcla_inv_px *)
38 lemma pr_fcla_inv_push (g) (m): š‚āØgā© ā‰˜ m ā†’ āˆ€f. ā«Æf = g ā†’ š‚āØfā© ā‰˜ m.
39 #g #m * -g -m
40 [ /3 width=3 by pr_fcla_isi, pr_isi_inv_push/
41 | #g #m #Hg #f #H >(eq_inv_pr_push_bi ā€¦ H) -f //
42 | #g #m #_ #f #H elim (eq_inv_pr_push_next ā€¦ H)
43 ]
44 qed-.
45
46 (*** fcla_inv_nx *)
47 lemma pr_fcla_inv_next (g) (m): š‚āØgā© ā‰˜ m ā†’ āˆ€f. ā†‘f = g ā†’ āˆƒāˆƒn. š‚āØfā© ā‰˜ n & ā†‘n = m.
48 #g #m * -g -m
49 [ #g #Hg #f #H destruct
50   elim (pr_isi_inv_next ā€¦ Hg) -Hg //
51 | #g #m #_ #f #H elim (eq_inv_pr_next_push ā€¦ H)
52 | #g #m #Hg #f #H >(eq_inv_pr_next_bi ā€¦  H) -f
53   /2 width=3 by ex2_intro/
54 ]
55 qed-.
56
57 (* Advanced inversions ******************************************************)
58
59 (*** cla_inv_nn *)
60 lemma pr_cla_inv_next_succ (g) (m): š‚āØgā© ā‰˜ m ā†’ āˆ€f,n. ā†‘f = g ā†’ ā†‘n = m ā†’ š‚āØfā© ā‰˜ n.
61 #g #m #H #f #n #H1 #H2 elim (pr_fcla_inv_next ā€¦ H ā€¦ H1) -g
62 #x #Hf #H destruct <(eq_inv_nsucc_bi ā€¦ H) -n //
63 qed-.
64
65 (*** cla_inv_np *)
66 lemma pr_cla_inv_next_zero (g) (m): š‚āØgā© ā‰˜ m ā†’ āˆ€f. ā†‘f = g ā†’ šŸŽ = m ā†’ āŠ„.
67 #g #m #H #f #H1 elim (pr_fcla_inv_next ā€¦ H ā€¦ H1) -g
68 #x #_ #H1 #H2 destruct /2 width=2 by eq_inv_zero_nsucc/
69 qed-.
70
71 (*** fcla_inv_xp *)
72 lemma pr_fcla_inv_zero (g) (m): š‚āØgā© ā‰˜ m ā†’ šŸŽ = m ā†’ šˆāØgā©.
73 #g #m #H elim H -g -m /3 width=3 by pr_isi_push/
74 #g #m #_ #_ #H destruct elim (eq_inv_zero_nsucc ā€¦ H)
75 qed-.
76
77 (*** fcla_inv_isid *)
78 lemma pr_fcla_inv_isi (g) (m): š‚āØgā© ā‰˜ m ā†’ šˆāØgā© ā†’ šŸŽ = m.
79 #f #n #H elim H -f -n /3 width=3 by pr_isi_inv_push/
80 #f #n #_ #_ #H elim (pr_isi_inv_next ā€¦ H) -H //
81 qed-.