From d1cf044d3f19bc9397872cc827cc77097fcc5b25 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sun, 21 Apr 2013 15:52:11 +0000 Subject: [PATCH] one file was missing --- .../lambdadelta/basic_2/reduction/chnf.ma | 36 +++++++++++++++++++ 1 file changed, 36 insertions(+) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/reduction/chnf.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/chnf.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/chnf.ma new file mode 100644 index 000000000..839450da3 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/chnf.ma @@ -0,0 +1,36 @@ +(**************************************************************************) +(* ___ *) +(* ||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/reduction/cpr_tshf.ma". + +(* CONTEXT-SENSITIVE WEAK HEAD NORMAL TERMS *********************************) + +definition chnf: lenv → predicate term ≝ λL. NF … (cpr L) tshf. + +interpretation + "context-sensitive head normality (term)" + 'HdNormal L T = (chnf L T). + +(* Basic inversion lemmas ***************************************************) + +lemma chnf_inv_tshf: ∀L,T. L ⊢ 𝐇𝐍⦃T⦄ → T ≈ T. +normalize /2 width=1/ +qed-. + +(* Basic properties *********************************************************) + +lemma tshf_thnf: ∀T. T ≈ T → ⋆ ⊢ 𝐇𝐍⦃T⦄. +#T #HT #T2 #H elim (cpr_fwd_tshf1 … H) -H // +#H elim H // +qed. -- 2.39.2