From 6aab24b40d5d09561375959043ecd85c8b428d85 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 21 Apr 2014 18:35:29 +0000 Subject: [PATCH] - we introduce recursive free variables of a term in a context ... - some symbols added --- .../notation/relations/cofreestar_3.ma | 19 +++++++++++ .../basic_2/substitution/cofrees.ma | 34 +++++++++++++++++++ matita/matita/predefined_virtuals.ml | 4 +-- 3 files changed, 55 insertions(+), 2 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/notation/relations/cofreestar_3.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/substitution/cofrees.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/cofreestar_3.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/cofreestar_3.ma new file mode 100644 index 000000000..86fc1f140 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/cofreestar_3.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) + +notation "hvbox( d ~ ϵ break 𝐅 * ⦃ term 46 L, break term 46 T ⦄ )" + non associative with precedence 45 + for @{ 'CoFreeStar $d $L $T }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/cofrees.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/cofrees.ma new file mode 100644 index 000000000..daab99769 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/cofrees.ma @@ -0,0 +1,34 @@ +(**************************************************************************) +(* ___ *) +(* ||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/notation/relations/cofreestar_3.ma". +include "basic_2/substitution/cpys.ma". + +(* CONTEXT-SENSITIVE EXCLUSION FROM FREE VARIABLES **************************) + +definition cofrees: relation3 nat lenv term ≝ + λd,L,U1. ∀U2. ⦃⋆, L⦄ ⊢ U1 ▶*[d, ∞] U2 → ∃T2. ⇧[d, 1] T2 ≡ U2. + +interpretation + "context-sensitive exclusion from free variables (term)" + 'CoFreeStar d L T = (cofrees d L T). + +(* Basic forward lemmas *****************************************************) + +lemma cofrees_fwd_lift: ∀L,U,d. d ~ϵ 𝐅*⦃L, U⦄ → ∃T. ⇧[d, 1] T ≡ U. +/2 width=1 by/ qed-. + +lemma nlift_frees: ∀L,U,d. (∀T. ⇧[d, 1] T ≡ U → ⊥) → (d ~ϵ 𝐅*⦃L, U⦄ → ⊥). +#L #U #d #HnTU #H elim (cofrees_fwd_lift … H) -H /2 width=2 by/ +qed-. diff --git a/matita/matita/predefined_virtuals.ml b/matita/matita/predefined_virtuals.ml index 6311d5933..0a1135cb4 100644 --- a/matita/matita/predefined_virtuals.ml +++ b/matita/matita/predefined_virtuals.ml @@ -1518,7 +1518,7 @@ let predefined_classes = [ ["⇑"; "⇧"; "⬆"; ] ; ["⇓"; "⇩"; "⬇"; "⬊"; "➷"; ] ; ["↔"; "⇔"; "⬄"; "⬌"; ] ; - ["≤"; "≲"; "≼"; "≰"; "≴"; "⋠"; "⊑"; ]; + ["≤"; "≲"; "≼"; "≰"; "≴"; "⋠"; "⊆"; "⫃"; "⊑"; ]; ["_"; "↓"; "↙"; "⎽"; "⎼"; "⎻"; "⎺"; ]; ["<"; "≺"; "≮"; "⊀"; "〈"; "«"; "❬"; "❮"; "❰"; ] ; ["("; "❨"; "❪"; "❲"; "（"; ]; @@ -1529,7 +1529,7 @@ let predefined_classes = [ ["}"; "❵"; "⦄" ] ; ["□"; "◽"; "▪"; "◾"; ]; ["◊"; "♢"; "⧫"; "♦"; "⟐"; "⟠"; ] ; - [">"; "⭃"; "⧁"; "〉"; "»"; "❭"; "❯"; "❱"; "▸"; "►"; "▶"; ] ; + [">"; "⭃"; "⧁"; "〉"; "»"; "❭"; "❯"; "❱"; "▸"; "►"; "▶"; "⊃"; "⊐"; ] ; ["≥"; "⪀"; "≽"; "⪴"; "⥸"; "⊒"; ]; ["∨"; "⩖"; "⋓"; ] ; ["a"; "α"; "𝕒"; "𝐚"; "𝛂"; "ⓐ"; ] ; -- 2.39.2