From: Ferruccio Guidi Date: Thu, 18 Jan 2007 14:49:03 +0000 (+0000) Subject: Unified: refactoring X-Git-Tag: make_still_working~6521 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=803d665cbff289f5e5340b9db137f1c4685b43f9;p=helm.git Unified: refactoring --- diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Unified/C/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Unified/C/defs.ma deleted file mode 100644 index 2c8a14ff6..000000000 --- a/helm/software/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/helm/software/matita/contribs/LAMBDA-TYPES/Unified/Inc/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Unified/Inc/defs.ma deleted file mode 100644 index 59c085963..000000000 --- a/helm/software/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/helm/software/matita/contribs/LAMBDA-TYPES/Unified/Lift/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Unified/Lift/defs.ma deleted file mode 100644 index a6c3345ca..000000000 --- a/helm/software/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/helm/software/matita/contribs/LAMBDA-TYPES/Unified/P/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Unified/P/defs.ma deleted file mode 100644 index 798ace41d..000000000 --- a/helm/software/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/helm/software/matita/contribs/LAMBDA-TYPES/Unified/SUB/C/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Unified/SUB/C/defs.ma new file mode 100644 index 000000000..2c8a14ff6 --- /dev/null +++ b/helm/software/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/helm/software/matita/contribs/LAMBDA-TYPES/Unified/SUB/Inc/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Unified/SUB/Inc/defs.ma new file mode 100644 index 000000000..59c085963 --- /dev/null +++ b/helm/software/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/helm/software/matita/contribs/LAMBDA-TYPES/Unified/SUB/Lift/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Unified/SUB/Lift/defs.ma new file mode 100644 index 000000000..a6c3345ca --- /dev/null +++ b/helm/software/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/helm/software/matita/contribs/LAMBDA-TYPES/Unified/SUB/P/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Unified/SUB/P/defs.ma new file mode 100644 index 000000000..798ace41d --- /dev/null +++ b/helm/software/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/helm/software/matita/contribs/developments.txt b/helm/software/matita/contribs/developments.txt index 4d5044941..503e8b7a2 100644 --- a/helm/software/matita/contribs/developments.txt +++ b/helm/software/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