matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "delayed_updating/syntax/path.ma".
  16 include "delayed_updating/notation/functions/black_diamond_2.ma".
  17 include "ground/relocation/tr_pap.ma".
  18
  19 (* GENERIC UNWIND FOR PATH **************************************************)
  20
  21 rec definition unwind_gen (f) (p) on p ≝
  22 match p with
  23 [ list_empty     ⇒ 𝐞
  24 | list_lcons l q ⇒
  25   match l with
  26   [ label_d n ⇒
  27     match q with
  28     [ list_empty     ⇒ 𝗱((f n)＠⧣❨n❩)◗(unwind_gen f q)
  29     | list_lcons _ _ ⇒ unwind_gen f q
  30     ]
  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)
  35   ]
  36 ].
  37
  38 interpretation
  39   "generic unwind (path)"
  40   'BlackDiamond f p = (unwind_gen f p).
  41
  42 (* Basic constructions ******************************************************)
  43
  44 lemma unwind_gen_empty (f):
  45       (𝐞) = ◆[f]𝐞.
  46 // qed.
  47
  48 lemma unwind_gen_d_empty (f) (n):
  49       𝗱((f n)＠⧣❨n❩)◗𝐞 = ◆[f](𝗱n◗𝐞).
  50 // qed.
  51
  52 lemma unwind_gen_d_lcons (f) (p) (l) (n):
  53       ◆[f](l◗p) = ◆[f](𝗱n◗l◗p).
  54 // qed.
  55
  56 lemma unwind_gen_m_sn (f) (p):
  57       ◆[f]p = ◆[f](𝗺◗p).
  58 // qed.
  59
  60 lemma unwind_gen_L_sn (f) (p):
  61       (𝗟◗◆[f]p) = ◆[f](𝗟◗p).
  62 // qed.
  63
  64 lemma unwind_gen_A_sn (f) (p):
  65       (𝗔◗◆[f]p) = ◆[f](𝗔◗p).
  66 // qed.
  67
  68 lemma unwind_gen_S_sn (f) (p):
  69       (𝗦◗◆[f]p) = ◆[f](𝗦◗p).
  70 // qed.
  71
  72 (* Advanced eliminations with path ******************************************)
  73
  74 lemma path_ind_unwind (Q:predicate …):
  75       Q (𝐞) →
  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)) →
  82       ∀p. Q p.
  83 #Q #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #IH7 #p
  84 elim p -p [| * [ #n * ] ]
  85 /2 width=1 by/
  86 qed-.