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/relocation/tr_compose.ma".
16 include "ground/relocation/tr_uni.ma".
17 include "delayed_updating/syntax/path.ma".
18 include "delayed_updating/notation/functions/uparrow_4.ma".
19 include "delayed_updating/notation/functions/uparrow_2.ma".
21 (* LIFT FOR PATH ***********************************************************)
23 (* Note: inner numeric labels are not liftable, so they are removed *)
24 rec definition lift_gen (A:Type[0]) (k:?ā?āA) (p) (f) on p ā
26 [ list_empty ā k š f
31 [ list_empty ā lift_gen (A) (Ī»p. k (š±āØf@āØnā©ā©āp)) q f
32 | list_lcons _ _ ā lift_gen (A) k q (fāš®āØnā©)
34 | label_edge_L ā lift_gen (A) (Ī»p. k (šāp)) q (ā«Æf)
35 | label_edge_A ā lift_gen (A) (Ī»p. k (šāp)) q f
36 | label_edge_S ā lift_gen (A) (Ī»p. k (š¦āp)) q f
42 'UpArrow A k p f = (lift_gen A k p f).
44 definition proj_path (p:path) (f:tr_map) ā p.
46 definition proj_rmap (p:path) (f:tr_map) ā f.
50 'UpArrow f p = (lift_gen ? proj_path p f).
53 "lift (relocation map)"
54 'UpArrow p f = (lift_gen ? proj_rmap p f).
56 (* Basic constructions ******************************************************)
58 lemma lift_L (A) (k) (p) (f):
59 āāØ(Ī»p. k (šāp)), p, ā«Æfā© = ā{A}āØk, šāp, fā©.
62 (* Basic constructions with proj_path ***************************************)
64 lemma lift_append (p) (f) (q):
65 qāā[f]p = āāØ(Ī»p. proj_path (qāp)), p, fā©.
68 | #l #p #IH #f #q cases l
70 | <lift_L in ā¢ (???%);
71 >(list_append_rcons_sn ? q) in ā¢ (???(??(Ī»_.%)??));
77 (* Constructions with append ************************************************)
79 theorem lift_append_A (p2) (p1) (f):
80 (ā[f]p1)āšāā[ā[p1]f]p2 = ā[f](p1āšāp2).