From d59f1c74c62ad3706d50707bb68758d88fbed006 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 9 May 2022 21:08:36 +0200 Subject: [PATCH] update in delayed_updating + main function to locate the referred binder + update function for unfold --- .../notation/functions/downarrowright_2.ma | 19 +++++ .../notation/functions/power_2.ma | 19 +++++ .../delayed_updating/syntax/path_labels.ma | 42 ++++++++++ .../delayed_updating/syntax/path_reverse.ma | 53 ++++++++++++ .../delayed_updating/syntax/path_tail.ma | 73 +++++++++++++++++ .../{path_closed.ma => path_tail_depth.ma} | 60 +++++++------- .../delayed_updating/unwind/unwind1_rmap.ma | 63 ++++++++++++++ .../unwind/unwind1_rmap_tail.ma | 82 +++++++++++++++++++ .../ground/notation/functions/applysucc_2.ma | 19 +++++ matita/matita/predefined_virtuals.ml | 3 +- 10 files changed, 400 insertions(+), 33 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/downarrowright_2.ma create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/power_2.ma create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_labels.ma create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_reverse.ma create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_tail.ma rename matita/matita/contribs/lambdadelta/delayed_updating/syntax/{path_closed.ma => path_tail_depth.ma} (58%) create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind1_rmap.ma create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind1_rmap_tail.ma create mode 100644 matita/matita/contribs/lambdadelta/ground/notation/functions/applysucc_2.ma diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/downarrowright_2.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/downarrowright_2.ma new file mode 100644 index 000000000..7531c6bcc --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/downarrowright_2.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 DELAYED UPDATING ********************************************) + +notation "hvbox( ↳[ term 46 n ] break term 70 p )" + non associative with precedence 70 + for @{ 'DownArrowRight $n $p }. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/power_2.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/power_2.ma new file mode 100644 index 000000000..bed0c7fe5 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/power_2.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 DELAYED UPDATING ********************************************) + +notation "hvbox( a ∗∗ break b )" + left associative with precedence 65 + for @{ 'Power $a $b }. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_labels.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_labels.ma new file mode 100644 index 000000000..a01c225ee --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_labels.ma @@ -0,0 +1,42 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "delayed_updating/syntax/path.ma". +include "delayed_updating/notation/functions/power_2.ma". +include "ground/arith/nat_succ_iter.ma". + +(* *) + +definition labels (l) (n:nat): path ≝ + ((list_lcons ? l)^n) (𝐞). + +interpretation + "labels (path)" + 'Power l n = (labels l n). + +(* Basic constructions ******************************************************) + +lemma labels_unfold (l) (n): + ((list_lcons ? l)^n) (𝐞) = l∗∗n. +// qed. + +lemma labels_zero (l): + (𝐞) = l∗∗𝟎. +// qed. + +lemma labels_succ (l) (n): + l◗(l∗∗n) = l∗∗(↑n). +#l #n +IH -IH