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/functions/uparrowstar_2.ma".
16 include "apps_2/notation/functional/uparrow_2.ma".
17 include "static_2/relocation/lifts.ma".
19 (* GENERIC FUNCTIONAL RELOCATION ********************************************)
21 rec definition flifts f U on U ≝ match U with
22 [ TAtom I ⇒ match I with
27 | TPair I V T ⇒ match I with
28 [ Bind2 p I ⇒ ⓑ[p,I](flifts f V).(flifts (⫯f) T)
29 | Flat2 I ⇒ ⓕ[I](flifts f V).(flifts f T)
33 interpretation "generic functional relocation (term)"
34 'UpArrowStar f T = (flifts f T).
36 interpretation "uniform functional relocation (term)"
37 'UpArrow i T = (flifts (uni i) T).
39 (* Basic properties *********************************************************)
41 lemma flifts_lref (f) (i): ↑*[f](#i) = #(f@⧣❨i❩).
44 lemma flifts_bind (f) (p) (I) (V) (T): ↑*[f](ⓑ[p,I]V.T) = ⓑ[p,I]↑*[f]V.↑*[⫯f]T.
47 lemma flifts_flat (f) (I) (V) (T): ↑*[f](ⓕ[I]V.T) = ⓕ[I]↑*[f]V.↑*[f]T.
50 (* Main properties **********************************************************)
52 theorem flifts_lifts: ∀T,f. ⇧*[f]T ≘ ↑*[f]T.
54 /2 width=1 by lifts_sort, lifts_lref, lifts_gref, lifts_bind, lifts_flat/
57 (* Main inversion properties ************************************************)
59 theorem flifts_inv_lifts: ∀f,T1,T2. ⇧*[f]T1 ≘ T2 → ↑*[f]T1 = T2.
60 #f #T1 #T2 #H elim H -f -T1 -T2 //
61 [ #f #i1 #i2 #H <(at_inv_total … H) //
62 | #f #p #I #V1 #V2 #T1 #T2 #_ #_ #IHV #IHT <IHV <IHT -V2 -T2 //
63 | #f #I #V1 #V2 #T1 #T2 #_ #_ #IHV #IHT <IHV <IHT -V2 -T2 //
67 (* Derived properties *******************************************************)
69 lemma flifts_comp: ∀f1,f2. f1 ≡ f2 → ∀T. ↑*[f1]T = ↑*[f2]T.
70 /3 width=3 by flifts_inv_lifts, lifts_eq_repl_fwd/ qed.
72 (* Derived properties with uniform relocation *******************************)
74 lemma flifts_lref_uni: ∀l,i. ↑[l](#i) = #(l+i).
75 /3 width=1 by flifts_inv_lifts, lifts_lref_uni/ qed.