From 48c011f52853dd106dbf9cbbd1b9da61277fba3b Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 9 May 2018 20:29:59 +0200 Subject: [PATCH] update in basic_2 + weight of a global environment + renaming --- .../lambdadelta/basic_2/syntax/genv.ma | 8 ++--- .../lambdadelta/basic_2/syntax/genv_length.ma | 2 +- .../lambdadelta/basic_2/syntax/genv_weight.ma | 30 +++++++++++++++++++ .../lambdadelta/basic_2/web/basic_2_src.tbl | 1 + 4 files changed, 36 insertions(+), 5 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/syntax/genv_weight.ma 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" * ] } ] -- 2.39.2