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_2/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 (* Main properties **********************************************************)
41 theorem flifts_lifts: ∀T,f. ⬆*[f]T ≘ ↑*[f]T.
43 /2 width=1 by lifts_sort, lifts_lref, lifts_gref, lifts_bind, lifts_flat/
46 (* Main inversion properties ************************************************)
48 theorem flifts_inv_lifts: ∀f,T1,T2. ⬆*[f]T1 ≘ T2 → ↑*[f]T1 = T2.
49 #f #T1 #T2 #H elim H -f -T1 -T2 //
50 [ #f #i1 #i2 #H <(at_inv_total … H) //
51 | #f #p #I #V1 #V2 #T1 #T2 #_ #_ #IHV #IHT <IHV <IHT -V2 -T2 //
52 | #f #I #V1 #V2 #T1 #T2 #_ #_ #IHV #IHT <IHV <IHT -V2 -T2 //
56 (* Derived properties *******************************************************)
58 lemma flifts_lref_uni: ∀l,i. ↑[l](#i) = #(l+i).
59 /3 width=1 by flifts_inv_lifts, lifts_lref_uni/ qed.
61 lemma flift_join: ∀e1,e2,T. ⬆[e1, e2] ↑[0, e1] T ≡ ↑[0, e1 + e2] T.
63 lapply (flift_lift T 0 (e1+e2)) #H
64 elim (lift_split … H e1 e1) -H // #U #H
65 >(flift_inv_lift … H) -H //