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/syntax/path.ma".
16 include "delayed_updating/notation/functions/black_diamond_2.ma".
17 include "ground/relocation/tr_pap.ma".
19 (* GENERIC UNWIND FOR PATH **************************************************)
21 rec definition unwind_gen (f) (p) on p ā
28 [ list_empty ā š±((f n)@āØnā©)ā(unwind_gen f q)
29 | list_lcons _ _ ā unwind_gen f q
31 | label_m ā unwind_gen f q
32 | label_L ā lā(unwind_gen f q)
33 | label_A ā lā(unwind_gen f q)
34 | label_S ā lā(unwind_gen f q)
39 "generic unwind (path)"
40 'BlackDiamond f p = (unwind_gen f p).
42 (* Basic constructions ******************************************************)
44 lemma unwind_gen_empty (f):
48 lemma unwind_gen_d_empty (f) (n):
49 š±((f n)@āØnā©)āš = ā[f](š±nāš).
52 lemma unwind_gen_d_lcons (f) (p) (l) (n):
53 ā[f](lāp) = ā[f](š±nālāp).
56 lemma unwind_gen_m_sn (f) (p):
57 ā[f]p = ā[f](šŗāp).
60 lemma unwind_gen_L_sn (f) (p):
61 (šāā[f]p) = ā[f](šāp).
64 lemma unwind_gen_A_sn (f) (p):
65 (šāā[f]p) = ā[f](šāp).
68 lemma unwind_gen_S_sn (f) (p):
69 (š¦āā[f]p) = ā[f](š¦āp).
72 (* Advanced eliminations with path ******************************************)
74 lemma path_ind_unwind (Q:predicate ā¦):
76 (ān. Q (š) ā Q (š±nāš)) ā
77 (ān,l,p. Q (lāp) ā Q (š±nālāp)) ā
78 (āp. Q p ā Q (šŗāp)) ā
79 (āp. Q p ā Q (šāp)) ā
80 (āp. Q p ā Q (šāp)) ā
81 (āp. Q p ā Q (š¦āp)) ā
83 #Q #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #IH7 #p
84 elim p -p [| * [ #n * ] ]