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 "apps_2/notation/functional/blackcircle_3.ma".
16 include "apps_2/functional/mf_vlift.ma".
17 include "apps_2/functional/mf_vpush.ma".
19 (* MULTIPLE FILLING FOR TERMS ***********************************************)
21 rec definition mf gv lv T on T ≝ match T with
22 [ TAtom I ⇒ match I with
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)
33 interpretation "term filling (multiple filling)"
34 'BlackCircle gv lv T = (mf gv lv T).
36 (* Basic Properties *********************************************************)
38 lemma mf_sort: ∀gv,lv,s. ■[gv,lv]⋆s = ⋆s.
41 lemma mf_lref: ∀gv,lv,i. ■[gv,lv]#i = lv i.
44 lemma mf_gref: ∀gv,lv,l. ■[gv,lv]§l = gv l.
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.
51 lemma mf_flat (I): ∀gv,lv,V,T.
52 ■[gv,lv]ⓕ[I]V.T = ⓕ[I]■[gv,lv]V.■[gv,lv]T.