update in delayed updating

+ delayed focalized reduction

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/circled_times_1.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/circled_times_1.ma
new file mode 100644 (file)
index 0000000..ac8c482
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/circled_times_1.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 60 p )"
+  non associative with precedence 60
+  for @{ 'CircledTimes $p }.

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/pitchfork_2.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/pitchfork_2.ma
new file mode 100644 (file)
index 0000000..1cfe14b
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/pitchfork_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( t ⋔ break p )"
+  left associative with precedence 47
+  for @{ 'Pitchfork $t $p }.

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/pitchforkleftarrow_3.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/pitchforkleftarrow_3.ma
new file mode 100644 (file)
index 0000000..7ab607d
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/pitchforkleftarrow_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 DELAYED UPDATING ********************************************)
+
+notation "hvbox( t [ ⋔ break term 46 p ← break term 46 u ] )"
+  non associative with precedence 47
+  for @{ 'PitchforkLeftArrow $t $p $u }.

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/predicate_squarecap_1.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/predicate_squarecap_1.ma
new file mode 100644 (file)
index 0000000..dbe1a24
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/predicate_squarecap_1.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 p )"
+  non associative with precedence 45
+  for @{ 'PredicateSquareCap $p }.

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma
new file mode 100644 (file)
index 0000000..f0b3f5f
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.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 "ground/xoa/ex_3_1.ma".
+include "delayed_updating/syntax/path_structure.ma".
+include "delayed_updating/syntax/path_balanced.ma".
+include "delayed_updating/substitution/fsubst.ma".
+(*
+include "delayed_updating/notation/functions/pitchforkleftarrow_3.ma".
+*)
+
+(* DELAYED FOCALIZED REDUCTION **********************************************)
+
+inductive dfr (p) (q) (t): predicate preterm ≝
+| dfr_beta (b) (n):
+  let r ≝ p;;(𝗔;b;;(𝗟;q,𝗱❨n❩)) in
+  r ϵ t → ⊓⊗b → dfr p q t (t[⋔r←t⋔p,𝗦])
+.
+(*
+interpretation
+  "focalized substitution (preterm)"
+  'PitchforkLeftArrow t p u = (fsubst p u t).
+*)

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/fsubst.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/fsubst.ma
new file mode 100644 (file)
index 0000000..0ff0522
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/fsubst.ma
@@ -0,0 +1,29 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "ground/xoa/ex_3_1.ma".
+include "delayed_updating/syntax/preterm.ma".
+include "delayed_updating/notation/functions/pitchforkleftarrow_3.ma".
+
+(* FOCALIZED SUBSTITUTION ***************************************************)
+
+definition fsubst (p) (u): preterm → preterm ≝
+           λt,q.
+           ∨∨ ∃∃r. r ϵ u & p ϵ ▵t & p;;r = q
+            | ∧∧ q ϵ t & (∀r. p;;r = q → ⊥) 
+.
+
+interpretation
+  "focalized substitution (preterm)"
+  'PitchforkLeftArrow t p u = (fsubst p u t).

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/path_dephi.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/path_dephi.ma
new file mode 100644 (file)
index 0000000..f51295e
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/path_dephi.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 "ground/relocation/tr_pap.ma".
+include "delayed_updating/syntax/path.ma".
+
+(* DEPHI FOR PATH ***********************************************************)
+
+rec definition path_dephi (f) (p) on p ≝
+match p with
+[ list_empty     ⇒ 𝐞
+| list_lcons l q ⇒
+   match l with
+   [ label_node_d n ⇒ 𝗱❨f@❨n❩❩;path_dephi f q
+   | label_edge_L   ⇒ 𝗟;path_dephi (𝟏⨮f) q
+   | label_edge_A   ⇒ 𝗔;path_dephi f q
+   | label_edge_S   ⇒ 𝗦;path_dephi f q
+   ]
+].

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/preterm_dephi.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/preterm_dephi.ma
new file mode 100644 (file)
index 0000000..60c5a4a
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/preterm_dephi.ma
@@ -0,0 +1,21 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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_dephi.ma".
+include "delayed_updating/syntax/preterm_constructors.ma".
+
+(* DEPHI FOR PRETERM ********************************************************)
+
+definition preterm_dephi (f) (t): preterm ≝
+           λp. ∃∃q. q ϵ t & p = path_dephi f q. 

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_balanced.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_balanced.ma
new file mode 100644 (file)
index 0000000..3226657
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_balanced.ma
@@ -0,0 +1,29 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/relations/predicate_squarecap_1.ma".
+
+(* BALANCE CONDITION FOR PATH ***********************************************)
+
+(* This condition applies to a structural path *)
+inductive pbc: predicate path ≝
+| pbc_empty: pbc 𝐞
+| pbc_redex: ∀b. pbc b → pbc (𝗔;b,𝗟)
+| pbc_after: ∀b1,b2. pbc b1 → pbc b2 → pbc (b1;;b2)
+.
+
+interpretation
+  "balance condition (path)"
+  'PredicateSquareCap p = (pbc p).

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_dephi.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_dephi.ma
deleted file mode 100644 (file)
index f51295e..0000000
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_dephi.ma
+++ /dev/null
@@ -1,30 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||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 "ground/relocation/tr_pap.ma".
-include "delayed_updating/syntax/path.ma".
-
-(* DEPHI FOR PATH ***********************************************************)
-
-rec definition path_dephi (f) (p) on p ≝
-match p with
-[ list_empty     ⇒ 𝐞
-| list_lcons l q ⇒
-   match l with
-   [ label_node_d n ⇒ 𝗱❨f@❨n❩❩;path_dephi f q
-   | label_edge_L   ⇒ 𝗟;path_dephi (𝟏⨮f) q
-   | label_edge_A   ⇒ 𝗔;path_dephi f q
-   | label_edge_S   ⇒ 𝗦;path_dephi f q
-   ]
-].

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure.ma
new file mode 100644 (file)
index 0000000..d7608ba
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure.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 "delayed_updating/syntax/path.ma".
+include "delayed_updating/notation/functions/circled_times_1.ma".
+
+(* STRUCTURE FOR PATH *******************************************************)
+
+rec definition path_structure (p) on p ≝
+match p with
+[ list_empty     ⇒ 𝐞
+| list_lcons l q ⇒
+   match l with
+   [ label_node_d n ⇒ path_structure q
+   | label_edge_L   ⇒ 𝗟;path_structure q
+   | label_edge_A   ⇒ 𝗔;path_structure q
+   | label_edge_S   ⇒ 𝗦;path_structure q
+   ]
+].
+
+interpretation
+  "structure (path)"
+  'CircledTimes p = (path_structure p).

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm.ma
index 44d923d9bb742b2b8b49fc247031c9e8c40916d4..aabb5adae086e3bf10d98b1fe4f87783c8c3bda1 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm.ma
@@ -14,6 +14,7 @@
 
 include "ground/lib/subset.ma".
 include "delayed_updating/syntax/path.ma".
+include "delayed_updating/notation/functions/pitchfork_2.ma".
 include "delayed_updating/notation/functions/uptriangle_1.ma".
 
 (* PRETERM ******************************************************************)
@@ -21,8 +22,15 @@ include "delayed_updating/notation/functions/uptriangle_1.ma".
 (* Note: preterms are subsets of complete paths *)
 definition preterm: Type[0] ≝ 𝒫❨path❩.
 
+definition preterm_grafted: path → preterm → preterm ≝
+           λp,t,q. p;;q ϵ t.
+
+interpretation
+  "grafted (preterm)"
+  'Pitchfork t p = (preterm_grafted p t).
+
 definition preterm_root: preterm → preterm ≝
-           λt,p. ∃q. p;;q ϵ t.
+           λt,q. ∃r. q;;r ϵ t.
 
 interpretation
   "root (preterm)"

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm_dephi.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm_dephi.ma
deleted file mode 100644 (file)
index 60c5a4a..0000000
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm_dephi.ma
+++ /dev/null
@@ -1,21 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||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_dephi.ma".
-include "delayed_updating/syntax/preterm_constructors.ma".
-
-(* DEPHI FOR PRETERM ********************************************************)
-
-definition preterm_dephi (f) (t): preterm ≝
-           λp. ∃∃q. q ϵ t & p = path_dephi f q.