matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure.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/circled_times_1.ma".
  17
  18 (* STRUCTURE FOR PATH *******************************************************)
  19
  20 rec definition structure (p) on p ≝
  21 match p with
  22 [ list_empty     ⇒ 𝐞
  23 | list_lcons l q ⇒
  24    match l with
  25    [ label_d k ⇒ structure q
  26    | label_m   ⇒ structure q
  27    | label_L   ⇒ (structure q)◖𝗟
  28    | label_A   ⇒ (structure q)◖𝗔
  29    | label_S   ⇒ (structure q)◖𝗦
  30    ]
  31 ].
  32
  33 interpretation
  34   "structure (path)"
  35   'CircledTimes p = (structure p).
  36
  37 (* Basic constructions ******************************************************)
  38
  39 lemma structure_empty:
  40       𝐞 = ⊗𝐞.
  41 // qed.
  42
  43 lemma structure_d_dx (p) (k):
  44       ⊗p = ⊗(p◖𝗱k).
  45 // qed.
  46
  47 lemma structure_m_dx (p):
  48       ⊗p = ⊗(p◖𝗺).
  49 // qed.
  50
  51 lemma structure_L_dx (p):
  52       (⊗p)◖𝗟 = ⊗(p◖𝗟).
  53 // qed.
  54
  55 lemma structure_A_dx (p):
  56       (⊗p)◖𝗔 = ⊗(p◖𝗔).
  57 // qed.
  58
  59 lemma structure_S_dx (p):
  60       (⊗p)◖𝗦 = ⊗(p◖𝗦).
  61 // qed.
  62
  63 (* Main constructions *******************************************************)
  64
  65 theorem structure_idem (p):
  66         ⊗p = ⊗⊗p.
  67 #p elim p -p [| * [ #k ] #p #IH ] //
  68 qed.
  69
  70 theorem structure_append (p) (q):
  71         ⊗p●⊗q = ⊗(p●q).
  72 #p #q elim q -q [| * [ #k ] #q #IH ]
  73 [||*: <list_append_lcons_sn ] //
  74 qed.
  75
  76 (* Constructions with path_lcons ********************************************)
  77
  78 lemma structure_d_sn (p) (k):
  79       ⊗p = ⊗(𝗱k◗p).
  80 #p #n <structure_append //
  81 qed.
  82
  83 lemma structure_m_sn (p):
  84       ⊗p = ⊗(𝗺◗p).
  85 #p <structure_append //
  86 qed.
  87
  88 lemma structure_L_sn (p):
  89       (𝗟◗⊗p) = ⊗(𝗟◗p).
  90 #p <structure_append //
  91 qed.
  92
  93 lemma structure_A_sn (p):
  94       (𝗔◗⊗p) = ⊗(𝗔◗p).
  95 #p <structure_append //
  96 qed.
  97
  98 lemma structure_S_sn (p):
  99       (𝗦◗⊗p) = ⊗(𝗦◗p).
 100 #p <structure_append //
 101 qed.