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 "delayed_updating/notation/functions/uparrow_4.ma".
16 include "delayed_updating/notation/functions/uparrow_2.ma".
17 include "delayed_updating/syntax/path.ma".
18 include "ground/relocation/tr_id_pap.ma".
20 (* LIFT FOR PATH ************************************************************)
22 definition lift_continuation (A:Type[0]) ≝
25 rec definition lift_gen (A:Type[0]) (k:lift_continuation A) (f) (p) on p ≝
27 [ list_empty ⇒ k f (𝐞)
30 [ label_d n ⇒ lift_gen (A) (λg,p. k g (𝗱(f@⧣❨n❩)◗p)) (𝐢) q
31 | label_m ⇒ lift_gen (A) (λg,p. k g (𝗺◗p)) f q
32 | label_L ⇒ lift_gen (A) (λg,p. k g (𝗟◗p)) (⫯f) q
33 | label_A ⇒ lift_gen (A) (λg,p. k g (𝗔◗p)) f q
34 | label_S ⇒ lift_gen (A) (λg,p. k g (𝗦◗p)) f q
40 'UpArrow A k f p = (lift_gen A k f p).
42 definition proj_path: lift_continuation … ≝
45 definition proj_rmap: lift_continuation … ≝
50 'UpArrow f p = (lift_gen ? proj_path f p).
53 "lift (relocation map)"
54 'UpArrow p f = (lift_gen ? proj_rmap f p).
56 (* Basic constructions ******************************************************)
58 lemma lift_empty (A) (k) (f):
59 k f (𝐞) = ↑{A}❨k, f, 𝐞❩.
62 lemma lift_d_sn (A) (k) (p) (n) (f):
63 ↑❨(λg,p. k g (𝗱(f@⧣❨n❩)◗p)), 𝐢, p❩ = ↑{A}❨k, f, 𝗱n◗p❩.
66 lemma lift_m_sn (A) (k) (p) (f):
67 ↑❨(λg,p. k g (𝗺◗p)), f, p❩ = ↑{A}❨k, f, 𝗺◗p❩.
70 lemma lift_L_sn (A) (k) (p) (f):
71 ↑❨(λg,p. k g (𝗟◗p)), ⫯f, p❩ = ↑{A}❨k, f, 𝗟◗p❩.
74 lemma lift_A_sn (A) (k) (p) (f):
75 ↑❨(λg,p. k g (𝗔◗p)), f, p❩ = ↑{A}❨k, f, 𝗔◗p❩.
78 lemma lift_S_sn (A) (k) (p) (f):
79 ↑❨(λg,p. k g (𝗦◗p)), f, p❩ = ↑{A}❨k, f, 𝗦◗p❩.
82 (* Basic constructions with proj_path ***************************************)
84 lemma lift_path_empty (f):
88 (* Basic constructions with proj_rmap ***************************************)
90 lemma lift_rmap_empty (f):
94 lemma lift_rmap_d_sn (f) (p) (n):
98 lemma lift_rmap_m_sn (f) (p):
102 lemma lift_rmap_L_sn (f) (p):
106 lemma lift_rmap_A_sn (f) (p):
110 lemma lift_rmap_S_sn (f) (p):
114 (* Advanced cinstructionswith proj_rmap and tr_id ***************************)
116 lemma lift_rmap_id (p):
122 (* Advanced constructions with proj_rmap and path_append ********************)
124 lemma lift_rmap_append (p2) (p1) (f):
125 ↑[p2]↑[p1]f = ↑[p1●p2]f.
126 #p2 #p1 elim p1 -p1 // * [ #n ] #p1 #IH #f //
127 [ <lift_rmap_d_sn <lift_rmap_d_sn //
128 | <lift_rmap_m_sn <lift_rmap_m_sn //
129 | <lift_rmap_A_sn <lift_rmap_A_sn //
130 | <lift_rmap_S_sn <lift_rmap_S_sn //
134 (* Advanced constructions with proj_rmap and path_rcons *********************)
136 lemma lift_rmap_d_dx (f) (p) (n):
140 lemma lift_rmap_m_dx (f) (p):
144 lemma lift_rmap_L_dx (f) (p):
148 lemma lift_rmap_A_dx (f) (p):
152 lemma lift_rmap_S_dx (f) (p):
156 lemma lift_rmap_pap_d_dx (f) (p) (n) (m):