Unified: refactoring

diff --git a/matita/contribs/LAMBDA-TYPES/Unified/C/defs.ma b/matita/contribs/LAMBDA-TYPES/Unified/C/defs.ma
deleted file mode 100644 (file)
index 2c8a14f..0000000
--- a/matita/contribs/LAMBDA-TYPES/Unified/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/C/defs".
-
-(* FLAT CONTEXTS
-   - Naming policy:
-     - contexts: c d
-*)
-
-include "P/defs.ma".
-
-inductive C: Set \def
-   | top  : C
-   | entry: C \to Bind \to P \to C
-.

diff --git a/matita/contribs/LAMBDA-TYPES/Unified/Inc/defs.ma b/matita/contribs/LAMBDA-TYPES/Unified/Inc/defs.ma
deleted file mode 100644 (file)
index 59c0859..0000000
--- a/matita/contribs/LAMBDA-TYPES/Unified/Inc/defs.ma
+++ /dev/null
@@ -1,28 +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/Inc/defs".
-
-(* DISPLACEMENT INCREMENT RELATION
-*)
-
-include "logic/equality.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
-.

diff --git a/matita/contribs/LAMBDA-TYPES/Unified/Lift/defs.ma b/matita/contribs/LAMBDA-TYPES/Unified/Lift/defs.ma
deleted file mode 100644 (file)
index a6c3345..0000000
--- a/matita/contribs/LAMBDA-TYPES/Unified/Lift/defs.ma
+++ /dev/null
@@ -1,41 +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/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 "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)
-.

diff --git a/matita/contribs/LAMBDA-TYPES/Unified/P/defs.ma b/matita/contribs/LAMBDA-TYPES/Unified/P/defs.ma
deleted file mode 100644 (file)
index 798ace4..0000000
--- a/matita/contribs/LAMBDA-TYPES/Unified/P/defs.ma
+++ /dev/null
@@ -1,52 +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/P/defs".
-
-(* POLARIZED TERMS
-   - Naming policy:
-     - natural numbers      : sorts h k, local references i j, lengths l
-     - boolean values       : a b
-     - generic binding items: x
-     - generic flat items   : y
-     - generic head items   : z
-     - terms                : p q
-*)
-
-include "../../RELATIONAL/Nat/defs.ma".
-include "../../RELATIONAL/Bool/defs.ma".
-
-inductive Bind: Set \def
-   | abbr: Bind
-   | abst: Bind
-   | excl: Bind
-.
-
-inductive Flat: Set \def
-   | appl: Flat
-   | cast: Flat
-.
-
-inductive Head: Set \def
-   | bind: Bind \to Head
-   | flat: Flat \to Head
-.
-
-inductive P: Set \def
-   | sort: Nat \to P
-   | lref: Nat \to P
-   | head: Bool \to Head \to P \to P \to P
-.

diff --git a/matita/contribs/LAMBDA-TYPES/Unified/SUB/C/defs.ma b/matita/contribs/LAMBDA-TYPES/Unified/SUB/C/defs.ma
new file mode 100644 (file)
index 0000000..2c8a14f
--- /dev/null
+++ b/matita/contribs/LAMBDA-TYPES/Unified/SUB/C/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/C/defs".
+
+(* FLAT CONTEXTS
+   - Naming policy:
+     - contexts: c d
+*)
+
+include "P/defs.ma".
+
+inductive C: Set \def
+   | top  : C
+   | entry: C \to Bind \to P \to C
+.

diff --git a/matita/contribs/LAMBDA-TYPES/Unified/SUB/Inc/defs.ma b/matita/contribs/LAMBDA-TYPES/Unified/SUB/Inc/defs.ma
new file mode 100644 (file)
index 0000000..59c0859
--- /dev/null
+++ b/matita/contribs/LAMBDA-TYPES/Unified/SUB/Inc/defs.ma
@@ -0,0 +1,28 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/Inc/defs".
+
+(* DISPLACEMENT INCREMENT RELATION
+*)
+
+include "logic/equality.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
+.

diff --git a/matita/contribs/LAMBDA-TYPES/Unified/SUB/Lift/defs.ma b/matita/contribs/LAMBDA-TYPES/Unified/SUB/Lift/defs.ma
new file mode 100644 (file)
index 0000000..a6c3345
--- /dev/null
+++ b/matita/contribs/LAMBDA-TYPES/Unified/SUB/Lift/defs.ma
@@ -0,0 +1,41 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/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 "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)
+.

diff --git a/matita/contribs/LAMBDA-TYPES/Unified/SUB/P/defs.ma b/matita/contribs/LAMBDA-TYPES/Unified/SUB/P/defs.ma
new file mode 100644 (file)
index 0000000..798ace4
--- /dev/null
+++ b/matita/contribs/LAMBDA-TYPES/Unified/SUB/P/defs.ma
@@ -0,0 +1,52 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/P/defs".
+
+(* POLARIZED TERMS
+   - Naming policy:
+     - natural numbers      : sorts h k, local references i j, lengths l
+     - boolean values       : a b
+     - generic binding items: x
+     - generic flat items   : y
+     - generic head items   : z
+     - terms                : p q
+*)
+
+include "../../RELATIONAL/Nat/defs.ma".
+include "../../RELATIONAL/Bool/defs.ma".
+
+inductive Bind: Set \def
+   | abbr: Bind
+   | abst: Bind
+   | excl: Bind
+.
+
+inductive Flat: Set \def
+   | appl: Flat
+   | cast: Flat
+.
+
+inductive Head: Set \def
+   | bind: Bind \to Head
+   | flat: Flat \to Head
+.
+
+inductive P: Set \def
+   | sort: Nat \to P
+   | lref: Nat \to P
+   | head: Bool \to Head \to P \to P \to P
+.

diff --git a/matita/contribs/developments.txt b/matita/contribs/developments.txt
index 4d50449410f45fdd805fa9525b4b630ea2d1e6a1..503e8b7a2d342d6de1148aebb02dd7c16ebd41ca 100644 (file)
--- a/matita/contribs/developments.txt
+++ b/matita/contribs/developments.txt
@@ -4,7 +4,6 @@ software/matita/legacy
 software/matita/library
 software/matita/tests
 software/matita/dama
-software/matita/contribs/CoRN
 software/matita/contribs/PREDICATIVE-TOPOLOGY
 software/matita/contribs/RELATIONAL
 software/matita/contribs/LAMBDA-TYPES/Unified