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 085e35dac7d0e8b484c8f5a9bf0cc79ea792d973..3e899a82986846d577da2853611171c5fb3923a4 100644 (file)
--- 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 *)
 (* 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)"
 .
 
 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)"
 
 interpretation "abbreviation (global environment)"

-   'DxAbbr G T = (GBind G Abbr T).
+   'DxAbbr G T = (GPair G Abbr T).

 
 interpretation "abstraction (global environment)"
 
 interpretation "abstraction (global environment)"

-   'DxAbst G T = (GBind G Abst T).
+   'DxAbst G T = (GPair G Abst T).

 
 (* Basic properties *********************************************************)
 
 
 (* 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 15244609af5af016dbde569c9bb02d0ce25b4dc1..bda7b391e767c9b2b9a04a8be5ac859cfb11b172 100644 (file)
--- 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
 
 rec definition glength G on G ≝ match G with
 [ GAtom       ⇒ 0

-| GBind G _ _ ⇒ ↑(glength G)
+| GPair G _ _ ⇒ ↑(glength G)

 ].
 
 interpretation "length (global environment)"
 ].
 
 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 (file)
index 0000000..632fdc8
--- /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 46ccf13b99b4808aa41ca19d54bbf7b05d9b4c5e..ff9b216278ece0c67338780b15bda9f3916708f4 100644 (file)
--- 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" + "( |?| )" * ]
         ]
         [ { "global environments" * } {
              [ [ "" ] "genv_length" + "( |?| )" * ]

+             [ [ "" ] "genv_weight" + "( ♯{?} )" * ]

              [ [ "" ] "genv" * ]
           }
         ]
              [ [ "" ] "genv" * ]
           }
         ]