Unified: refactoring

diff --git a/matita/contribs/LAMBDA-TYPES/Unified/SUB/C/defs.ma b/matita/contribs/LAMBDA-TYPES/Unified/SUB/C/defs.ma
deleted file mode 100644 (file)
index 2b93d77..0000000
--- a/matita/contribs/LAMBDA-TYPES/Unified/SUB/C/defs.ma
+++ /dev/null
@@ -1,27 +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                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified/SUB/Context/defs".
-
-(* FLAT CONTEXTS
-   - Naming policy:
-     - contexts: c d
-*)
-
-include "SUB/T/defs.ma".
-
-inductive Context: Set \def
-   | top  : Context
-   | entry: Context \to Bind \to Term \to Context
-.

diff --git a/matita/contribs/LAMBDA-TYPES/Unified/SUB/Context/defs.ma b/matita/contribs/LAMBDA-TYPES/Unified/SUB/Context/defs.ma
new file mode 100644 (file)
index 0000000..39859fc
--- /dev/null
+++ b/matita/contribs/LAMBDA-TYPES/Unified/SUB/Context/defs.ma
@@ -0,0 +1,27 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified/SUB/Context/defs".
+
+(* FLAT CONTEXTS
+   - Naming policy:
+     - contexts: c d
+*)
+
+include "SUB/Term/defs.ma".
+
+inductive Context: Set \def
+   | leaf: Context
+   | head: Context \to Bind \to Term \to Context
+.

diff --git a/matita/contribs/LAMBDA-TYPES/Unified/SUB/Inc/defs.ma b/matita/contribs/LAMBDA-TYPES/Unified/SUB/Inc/defs.ma
index 59c085963d749b3999a4f8d6e47fa63a4a40e1da..266e3c7b7605a7a313510111ba779e7fdf34dfaa 100644 (file)
--- a/matita/contribs/LAMBDA-TYPES/Unified/SUB/Inc/defs.ma
+++ b/matita/contribs/LAMBDA-TYPES/Unified/SUB/Inc/defs.ma
@@ -12,17 +12,16 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified/Inc/defs".
+set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified/SUB/Inc/defs".
 
 (* DISPLACEMENT INCREMENT RELATION
 *)
 
-include "logic/equality.ma".
+include "SUB/Term/defs.ma".
 
-include "P/defs.ma".
-
-inductive Inc (i:Nat): Bool \to Head \to Nat \to Prop \def
-   | inc_bind: \forall x. Inc i true (bind x) (succ i)
-   | inc_flat: \forall y. Inc i true (flat y) i   
-   | inc_neg : \forall z. Inc i false z i
+inductive Inc (q:Bool) (i:Nat): Head \to Nat \to Prop \def
+   | inc_bind: \forall r. Inc q i (bind q r) (succ i)
+   | inc_skip: \forall p. (q = p \to False) \to
+               \forall r. Inc q i (bind p r) i
+   | inc_flat: \forall p,r. Inc q i (flat p r) i   
 .

diff --git a/matita/contribs/LAMBDA-TYPES/Unified/SUB/Lift/defs.ma b/matita/contribs/LAMBDA-TYPES/Unified/SUB/Lift/defs.ma
index a6c3345caa4be6dd7e7863a4e66999eec3345a50..dc12e8cc81d667600085e43354b7edcb39b0c7c5 100644 (file)
--- a/matita/contribs/LAMBDA-TYPES/Unified/SUB/Lift/defs.ma
+++ b/matita/contribs/LAMBDA-TYPES/Unified/SUB/Lift/defs.ma
@@ -12,30 +12,28 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified/Lift/defs".
+set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified/SUB/Lift/defs".
 
 (* LIFT RELATION
    - Usage: invoke with positive polarity
 *)
 
-include "logic/equality.ma".
-include "../../RELATIONAL/NPlus/defs.ma".
-include "../../RELATIONAL/NLE/defs.ma".
-include "../../RELATIONAL/BEq/defs.ma".
+include "SUB/Switch/defs.ma".
+include "SUB/Inc/defs.ma".
 
-include "P/defs.ma".
-include "Inc/defs.ma".
-
-inductive Lift (l: Nat): Nat \to Bool \to P \to P \to Prop \def
-   | lift_sort    : \forall i,a,h. Lift l i a (sort h) (sort h)
-   | lift_lref_neg: \forall i,j. Lift l i false (lref j) (lref j)
-   | lift_lref_lt : \forall i,j. 
-                    j < i \to Lift l i true (lref j) (lref j)
-   | lift_lref_ge : \forall i,j1,j2.
-                    i <= j1 \to (j1 + l == j2) \to
-                    Lift l i true (lref j1) (lref j2)
-   | lift_head    : \forall i,i',a,b,a',z,q1,q2,p1,p2. 
-                    (a * b == a') \to Inc i a' z i' \to
-                    Lift l i a' q1 q2 \to Lift l i' a p1 p2 \to 
-                    Lift l i a (head b z q1 p1) (head b z q2 p2)
+inductive Lift: Bool \to Nat \to Nat \to Term \to Term \to Prop \def
+   | lift_sort   : \forall l,q,i,h. 
+                   Lift q l i (leaf (sort h)) (leaf (sort h))
+   | lift_skip   : \forall l,i,j. 
+                   Lift false l i (leaf (lref j)) (leaf (lref j))
+   | lift_lref_lt: \forall l,i,j. j < i \to 
+                   Lift true l i (leaf (lref j)) (leaf (lref j))
+   | lift_lref_ge: \forall l,i,j1. i <= j1 \to
+                   \forall j2. (j1 + l == j2) \to
+                   Lift true l i (leaf (lref j1)) (leaf (lref j2))
+   | lift_head   : \forall l,qt,qu,z. Switch qt z qu \to
+                   \forall iu,it. Inc qt iu z it \to
+                   \forall u1,u2. Lift qu l iu u1 u2 \to
+                   \forall t1,t2. Lift qt l it t1 t2 \to 
+                   Lift qt l iu (head z u1 t1) (head z u2 t2)
 .

diff --git a/matita/contribs/LAMBDA-TYPES/Unified/SUB/Switch/defs.ma b/matita/contribs/LAMBDA-TYPES/Unified/SUB/Switch/defs.ma
new file mode 100644 (file)
index 0000000..7a43502
--- /dev/null
+++ b/matita/contribs/LAMBDA-TYPES/Unified/SUB/Switch/defs.ma
@@ -0,0 +1,27 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified/SUB/Switch/defs".
+
+(* POLARITY SWITCH RELATION
+*)
+
+include "SUB/Term/defs.ma".
+
+inductive Switch (q1:Bool): Head \to Bool \to Prop \def
+   | switch_bind: \forall q2,p. (p -- q1 == q2) \to
+                  \forall r. Switch q1 (bind p r) q2 
+   | switch_flat: \forall q2,p. (p -- q1 == q2) \to
+                  \forall r. Switch q1 (flat p r) q2 
+.

diff --git a/matita/contribs/LAMBDA-TYPES/Unified/SUB/T/defs.ma b/matita/contribs/LAMBDA-TYPES/Unified/SUB/T/defs.ma
deleted file mode 100644 (file)
index df6e194..0000000
--- a/matita/contribs/LAMBDA-TYPES/Unified/SUB/T/defs.ma
+++ /dev/null
@@ -1,57 +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                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-(* Project started Tue Aug 22, 2006 ***************************************)
-
-set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified/SUB/Term/defs".
-
-(* POLARIZED TERMS
-   - Naming policy:
-     - natural numbers      : sorts h k, local references i j, lengths l o
-     - boolean values       : p q
-     - generic leaf items   : m n
-     - generic binding items: r s 
-     - generic flat items   : r s
-     - generic head items   : m n
-     - terms                : t u
-*)
-
-include "../../RELATIONAL/Nat/defs.ma".
-include "../../RELATIONAL/Bool/defs.ma".
-
-inductive Leaf: Set \def
-   | sort: Nat \to Leaf
-   | lref: Nat \to Leaf
-.
-
-inductive Bind: Set \def
-   | abbr: Bind
-   | abst: Bind
-   | excl: Bind
-.
-
-inductive Flat: Set \def
-   | appl: Flat
-   | cast: Flat
-.
-
-inductive Head: Set \def
-   | bind: Bool \to Bind \to Head
-   | flat: Bool \to Flat \to Head
-.
-
-inductive Term: Set \def
-   | leaf: Leaf \to Term
-   | head: Head \to Term \to Term \to Term
-.

diff --git a/matita/contribs/LAMBDA-TYPES/Unified/SUB/Term/defs.ma b/matita/contribs/LAMBDA-TYPES/Unified/SUB/Term/defs.ma
new file mode 100644 (file)
index 0000000..d1559a4
--- /dev/null
+++ b/matita/contribs/LAMBDA-TYPES/Unified/SUB/Term/defs.ma
@@ -0,0 +1,54 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified/SUB/Term/defs".
+
+(* POLARIZED TERMS
+   - Naming policy:
+     - natural numbers      : sorts h k, local references i j, lengths l o
+     - boolean values       : p q
+     - generic leaf items   : m n
+     - generic binding items: r s 
+     - generic flat items   : r s
+     - generic head items   : m n
+     - terms                : t u
+*)
+
+include "SUB/preamble.ma".
+
+inductive Leaf: Set \def
+   | sort: Nat \to Leaf
+   | lref: Nat \to Leaf
+.
+
+inductive Bind: Set \def
+   | abbr: Bind
+   | abst: Bind
+   | excl: Bind
+.
+
+inductive Flat: Set \def
+   | appl: Flat
+   | cast: Flat
+.
+
+inductive Head: Set \def
+   | bind: Bool \to Bind \to Head
+   | flat: Bool \to Flat \to Head
+.
+
+inductive Term: Set \def
+   | leaf: Leaf \to Term
+   | head: Head \to Term \to Term \to Term
+.

diff --git a/matita/contribs/LAMBDA-TYPES/Unified/SUB/preamble.ma b/matita/contribs/LAMBDA-TYPES/Unified/SUB/preamble.ma
new file mode 100644 (file)
index 0000000..4a348cc
--- /dev/null
+++ b/matita/contribs/LAMBDA-TYPES/Unified/SUB/preamble.ma
@@ -0,0 +1,27 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* Project started Tue Aug 22, 2006 ***************************************)
+
+set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified/SUB/preamble".
+
+(* PREAMBLE
+*)
+
+include "logic/equality.ma".
+include "../../RELATIONAL/NPlus/defs.ma".
+include "../../RELATIONAL/NLE/defs.ma".
+include "../../RELATIONAL/BEq/defs.ma".
+include "../../RELATIONAL/Nat/defs.ma".
+include "../../RELATIONAL/Bool/defs.ma".