]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/ground/relocation/pr_map.ma
update in delayed_updating
[helm.git] / matita / matita / contribs / lambdadelta / ground / relocation / pr_map.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/functions/upspoon_1.ma".
16 include "ground/notation/functions/uparrow_1.ma".
17 include "ground/lib/stream.ma".
18 include "ground/lib/bool.ma".
19
20 (* PARTIAL RELOCATION MAPS **************************************************)
21
22 (*** rtmap *)
23 definition pr_map: Type[0] ≝ stream bool.
24
25 (*** push *)
26 definition pr_push (f): pr_map ≝ Ⓕ⨮f.
27
28 interpretation
29   "push (partial relocation maps)"
30   'UpSpoon f = (pr_push f).
31
32 (*** next *)
33 definition pr_next (f): pr_map ≝ Ⓣ⨮f.
34
35 interpretation
36   "next (partial relocation maps)"
37   'UpArrow f = (pr_next f).
38
39 (* Basic constructions (specific) *******************************************)
40
41 (*** push_rew *)
42 lemma pr_push_unfold (f): Ⓕ⨮f = ⫯f.
43 // qed.
44
45 (*** next_rew *)
46 lemma pr_next_unfold (f): Ⓣ⨮f = ↑f.
47 // qed.
48
49 (* Basic inversions *********************************************************)
50
51 (*** injective_push *)
52 lemma eq_inv_pr_push_bi: injective ? ? pr_push.
53 #f1 #f2 <pr_push_unfold <pr_push_unfold #H destruct //
54 qed-.
55
56 (*** discr_push_next *)
57 lemma eq_inv_pr_push_next (f1) (f2): ⫯f1 = ↑f2 → ⊥.
58 #f1 #f2 <pr_push_unfold <pr_next_unfold #H destruct
59 qed-.
60
61 (*** discr_next_push *)
62 lemma eq_inv_pr_next_push (f1) (f2): ↑f1 = ⫯f2 → ⊥.
63 #f1 #f2 <pr_next_unfold <pr_push_unfold #H destruct
64 qed-.
65
66 (*** injective_next *)
67 lemma eq_inv_pr_next_bi: injective ? ? pr_next.
68 #f1 #f2 <pr_next_unfold <pr_next_unfold #H destruct //
69 qed-.