matita/matita/contribs/lambdadelta/apps_2/functional/mf.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 "apps_2/notation/functional/blackcircle_3.ma".
  16 include "apps_2/functional/mf_vlift.ma".
  17 include "apps_2/functional/mf_vpush.ma".
  18
  19 (* MULTIPLE FILLING FOR TERMS ***********************************************)
  20
  21 rec definition mf gv lv T on T ≝ match T with
  22 [ TAtom I     ⇒ match I with
  23   [ Sort _ ⇒ T
  24   | LRef i ⇒ lv i
  25   | GRef l ⇒ gv l
  26   ]
  27 | TPair I V T ⇒ match I with
  28   [ Bind2 _ _ ⇒ TPair I (mf gv lv V) (mf (⇡[0]gv) (⇡[0←#0]lv) T)
  29   | Flat2 _   ⇒ TPair I (mf gv lv V) (mf gv lv T)
  30   ]
  31 ].
  32
  33 interpretation "term filling (multiple filling)"
  34   'BlackCircle gv lv T = (mf gv lv T).
  35
  36 (* Basic Properties *********************************************************)
  37
  38 lemma mf_sort: ∀gv,lv,s. ●[gv,lv]⋆s = ⋆s.
  39 // qed.
  40
  41 lemma mf_lref: ∀gv,lv,i. ●[gv,lv]#i = lv i.
  42 // qed.
  43
  44 lemma mf_gref: ∀gv,lv,l. ●[gv,lv]§l = gv l.
  45 // qed.
  46
  47 lemma mf_bind (p) (I): ∀gv,lv,V,T.
  48                        ●[gv,lv]ⓑ{p,I}V.T = ⓑ{p,I}●[gv,lv]V.●[⇡[0]gv,⇡[0←#0]lv]T.
  49 // qed.
  50
  51 lemma mf_flat (I): ∀gv,lv,V,T.
  52                    ●[gv,lv]ⓕ{I}V.T = ⓕ{I}●[gv,lv]V.●[gv,lv]T.
  53 // qed.