From: Ferruccio Guidi <fguidi@maelstrom.helm.cs.unibo.it>
Date: Wed, 9 May 2018 18:29:59 +0000 (+0200)
Subject: update in basic_2
X-Git-Tag: make_still_working~326
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=48c011f52853dd106dbf9cbbd1b9da61277fba3b;p=helm.git

update in basic_2

+ weight of a global environment
+ renaming
---

diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/genv.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/genv.ma
index 085e35dac..3e899a829 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/syntax/genv.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/genv.ma
@@ -23,20 +23,20 @@ include "basic_2/syntax/term.ma".
 (* global environments *)
 inductive genv: Type[0] ≝
 | GAtom: genv                       (* empty *)
-| GBind: genv → bind2 → term → genv (* binding construction *)
+| GPair: genv → bind2 → term → genv (* binary binding construction *)
 .
 
 interpretation "sort (global environment)"
    'Star = (GAtom).
 
 interpretation "global environment binding construction (binary)"
-   'DxBind2 G I T = (GBind G I T).
+   'DxBind2 G I T = (GPair G I T).
 
 interpretation "abbreviation (global environment)"
-   'DxAbbr G T = (GBind G Abbr T).
+   'DxAbbr G T = (GPair G Abbr T).
 
 interpretation "abstraction (global environment)"
-   'DxAbst G T = (GBind G Abst T).
+   'DxAbst G T = (GPair G Abst T).
 
 (* Basic properties *********************************************************)
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/genv_length.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/genv_length.ma
index 15244609a..bda7b391e 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/syntax/genv_length.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/genv_length.ma
@@ -18,7 +18,7 @@ include "basic_2/syntax/genv.ma".
 
 rec definition glength G on G ≝ match G with
 [ GAtom       ⇒ 0
-| GBind G _ _ ⇒ ↑(glength G)
+| GPair G _ _ ⇒ ↑(glength G)
 ].
 
 interpretation "length (global environment)"
diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/genv_weight.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/genv_weight.ma
new file mode 100644
index 000000000..632fdc8e5
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/genv_weight.ma
@@ -0,0 +1,30 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/syntax/term_weight.ma".
+include "basic_2/syntax/genv.ma".
+
+(* WEIGHT OF A GLOBAL ENVIRONMENT *******************************************)
+
+rec definition gw G ≝ match G with
+[ GAtom       ⇒ 0
+| GPair G I T ⇒ gw G + ♯{T}
+].
+
+interpretation "weight (global environment)" 'Weight G = (gw G).
+
+(* Basic properties *********************************************************)
+
+lemma gw_pair: ∀I,G,T. ♯{G} < ♯{G.ⓑ{I}T}.
+normalize /2 width=1 by monotonic_le_plus_r/ qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
index 46ccf13b9..ff9b21627 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
+++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
@@ -251,6 +251,7 @@ table {
         ]
         [ { "global environments" * } {
              [ [ "" ] "genv_length" + "( |?| )" * ]
+             [ [ "" ] "genv_weight" + "( ♯{?} )" * ]
              [ [ "" ] "genv" * ]
           }
         ]