Unified refactored

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..7aca13a
--- /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 "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
new file mode 100644 (file)
index 0000000..d36f86a
--- /dev/null
+++ b/matita/contribs/LAMBDA-TYPES/Unified-Sub/Inc/defs.ma
@@ -0,0 +1,26 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/Inc/defs".
+
+(* DISPLACEMENT INCREMENT RELATION
+*)
+
+include "Term/defs.ma".
+
+inductive Inc (i:Nat): Bool \to Head \to Nat \to Prop \def
+   | inc_bind: \forall r. Inc i true (bind r) (succ i)
+   | inc_skip: \forall r. Inc i false (bind r) i
+   | inc_flat: \forall r,q. Inc i q (flat r) 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..cf29a35
--- /dev/null
+++ b/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/defs.ma
@@ -0,0 +1,38 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/Lift/defs".
+
+(* LIFT RELATION
+   - Usage: invoke with positive polarity
+*)
+
+include "Inc/defs.ma".
+
+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,q. (qt -- q == qu) \to
+                   \forall z,iu,it. Inc iu qu 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 q z u1 t1) (head q z u2 t2)
+.

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..e082096
--- /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 "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: Bind \to Head
+   | flat: Flat \to Head
+.
+
+inductive Term: Set \def
+   | leaf: Leaf \to Term
+   | head: Bool \to Head \to Term \to Term \to Term
+.

diff --git a/matita/contribs/LAMBDA-TYPES/Unified-Sub/makefile b/matita/contribs/LAMBDA-TYPES/Unified-Sub/makefile
new file mode 100644 (file)
index 0000000..489485e
--- /dev/null
+++ b/matita/contribs/LAMBDA-TYPES/Unified-Sub/makefile
@@ -0,0 +1,39 @@
+H=@
+
+RT_BASEDIR=/home/fguidi/svn/software/matita/
+OPTIONS=-bench
+MMAKE=$(RT_BASEDIR)matitamake $(OPTIONS)
+CLEAN=$(RT_BASEDIR)matitaclean $(OPTIONS) 
+MMAKEO=$(RT_BASEDIR)matitamake.opt $(OPTIONS)
+CLEANO=$(RT_BASEDIR)matitaclean.opt $(OPTIONS) 
+
+devel:=$(shell basename `pwd`)
+
+ifneq "$(SRC)" ""
+  XXX="SRC=$(SRC)"
+endif
+
+all: preall
+       $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) build $(devel)
+clean: preall
+       $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) clean $(devel)
+cleanall: preall
+       $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MCLEAN) all
+
+all.opt opt: preall.opt
+       $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) build $(devel)
+clean.opt: preall.opt
+       $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) clean $(devel)
+cleanall.opt: preall.opt
+       $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MCLEANO) all
+
+%.mo: preall
+       $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) $@
+%.mo.opt: preall.opt
+       $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) $@
+       
+preall:
+       $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) init $(devel)
+
+preall.opt:
+       $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) init $(devel)

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..21afc1d
--- /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".

diff --git a/matita/contribs/LAMBDA-TYPES/Unified/SUB/Context/defs.ma b/matita/contribs/LAMBDA-TYPES/Unified/SUB/Context/defs.ma
deleted file mode 100644 (file)
index 22763dd..0000000
--- a/matita/contribs/LAMBDA-TYPES/Unified/SUB/Context/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/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
deleted file mode 100644 (file)
index 4c4c996..0000000
--- a/matita/contribs/LAMBDA-TYPES/Unified/SUB/Inc/defs.ma
+++ /dev/null
@@ -1,26 +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/Inc/defs".
-
-(* DISPLACEMENT INCREMENT RELATION
-*)
-
-include "SUB/Term/defs.ma".
-
-inductive Inc (i:Nat): Bool \to Head \to Nat \to Prop \def
-   | inc_bind: \forall r. Inc i true (bind r) (succ i)
-   | inc_skip: \forall r. Inc i false (bind r) i
-   | inc_flat: \forall r,q. Inc i q (flat r) i   
-.

diff --git a/matita/contribs/LAMBDA-TYPES/Unified/SUB/Lift/defs.ma b/matita/contribs/LAMBDA-TYPES/Unified/SUB/Lift/defs.ma
deleted file mode 100644 (file)
index a653404..0000000
--- a/matita/contribs/LAMBDA-TYPES/Unified/SUB/Lift/defs.ma
+++ /dev/null
@@ -1,38 +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/Lift/defs".
-
-(* LIFT RELATION
-   - Usage: invoke with positive polarity
-*)
-
-include "SUB/Inc/defs.ma".
-
-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,q. (qt -- q == qu) \to
-                   \forall z,iu,it. Inc iu qu 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 q z u1 t1) (head q z u2 t2)
-.

diff --git a/matita/contribs/LAMBDA-TYPES/Unified/SUB/Term/defs.ma b/matita/contribs/LAMBDA-TYPES/Unified/SUB/Term/defs.ma
deleted file mode 100644 (file)
index b73935a..0000000
--- a/matita/contribs/LAMBDA-TYPES/Unified/SUB/Term/defs.ma
+++ /dev/null
@@ -1,54 +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/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: Bind \to Head
-   | flat: Flat \to Head
-.
-
-inductive Term: Set \def
-   | leaf: Leaf \to Term
-   | head: Bool \to 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
deleted file mode 100644 (file)
index 21afc1d..0000000
--- a/matita/contribs/LAMBDA-TYPES/Unified/SUB/preamble.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                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-(* 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".

diff --git a/matita/contribs/LAMBDA-TYPES/Unified/makefile b/matita/contribs/LAMBDA-TYPES/Unified/makefile
deleted file mode 100644 (file)
index d53547f..0000000
--- a/matita/contribs/LAMBDA-TYPES/Unified/makefile
+++ /dev/null
@@ -1,39 +0,0 @@
-H=@
-
-RT_BASEDIR=../../../
-OPTIONS=-bench
-MMAKE=$(RT_BASEDIR)matitamake $(OPTIONS)
-CLEAN=$(RT_BASEDIR)matitaclean $(OPTIONS) 
-MMAKEO=$(RT_BASEDIR)matitamake.opt $(OPTIONS)
-CLEANO=$(RT_BASEDIR)matitaclean.opt $(OPTIONS) 
-
-devel:=$(shell basename `pwd`)
-
-ifneq "$(SRC)" ""
-  XXX="SRC=$(SRC)"
-endif
-
-all: preall
-       $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) build $(devel)
-clean: preall
-       $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) clean $(devel)
-cleanall: preall
-       $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MCLEAN) all
-
-all.opt opt: preall.opt
-       $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) build $(devel)
-clean.opt: preall.opt
-       $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) clean $(devel)
-cleanall.opt: preall.opt
-       $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MCLEANO) all
-
-%.mo: preall
-       $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) $@
-%.mo.opt: preall.opt
-       $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) $@
-       
-preall:
-       $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) init $(devel)
-
-preall.opt:
-       $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) init $(devel)