From 1f32c644494bdd49b455501f3f797f781a1bd24a Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 19 Jan 2007 14:20:38 +0000 Subject: [PATCH] Unified: refactoring --- .../Unified/SUB/{C => Context}/defs.ma | 6 +-- .../LAMBDA-TYPES/Unified/SUB/Inc/defs.ma | 15 ++++---- .../LAMBDA-TYPES/Unified/SUB/Lift/defs.ma | 38 +++++++++---------- .../LAMBDA-TYPES/Unified/SUB/Switch/defs.ma | 27 +++++++++++++ .../Unified/SUB/{T => Term}/defs.ma | 5 +-- .../LAMBDA-TYPES/Unified/SUB/preamble.ma | 27 +++++++++++++ 6 files changed, 83 insertions(+), 35 deletions(-) rename matita/contribs/LAMBDA-TYPES/Unified/SUB/{C => Context}/defs.ma (92%) create mode 100644 matita/contribs/LAMBDA-TYPES/Unified/SUB/Switch/defs.ma rename matita/contribs/LAMBDA-TYPES/Unified/SUB/{T => Term}/defs.ma (91%) create mode 100644 matita/contribs/LAMBDA-TYPES/Unified/SUB/preamble.ma diff --git a/matita/contribs/LAMBDA-TYPES/Unified/SUB/C/defs.ma b/matita/contribs/LAMBDA-TYPES/Unified/SUB/Context/defs.ma similarity index 92% rename from matita/contribs/LAMBDA-TYPES/Unified/SUB/C/defs.ma rename to matita/contribs/LAMBDA-TYPES/Unified/SUB/Context/defs.ma index 2b93d7783..39859fc0e 100644 --- a/matita/contribs/LAMBDA-TYPES/Unified/SUB/C/defs.ma +++ b/matita/contribs/LAMBDA-TYPES/Unified/SUB/Context/defs.ma @@ -19,9 +19,9 @@ set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified/SUB/Context/defs". - contexts: c d *) -include "SUB/T/defs.ma". +include "SUB/Term/defs.ma". inductive Context: Set \def - | top : Context - | entry: Context \to Bind \to Term \to Context + | 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 59c085963..266e3c7b7 100644 --- 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 a6c3345ca..dc12e8cc8 100644 --- 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 index 000000000..7a435021f --- /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/Term/defs.ma similarity index 91% rename from matita/contribs/LAMBDA-TYPES/Unified/SUB/T/defs.ma rename to matita/contribs/LAMBDA-TYPES/Unified/SUB/Term/defs.ma index df6e1945e..d1559a40a 100644 --- a/matita/contribs/LAMBDA-TYPES/Unified/SUB/T/defs.ma +++ b/matita/contribs/LAMBDA-TYPES/Unified/SUB/Term/defs.ma @@ -12,8 +12,6 @@ (* *) (**************************************************************************) -(* Project started Tue Aug 22, 2006 ***************************************) - set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified/SUB/Term/defs". (* POLARIZED TERMS @@ -27,8 +25,7 @@ set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified/SUB/Term/defs". - terms : t u *) -include "../../RELATIONAL/Nat/defs.ma". -include "../../RELATIONAL/Bool/defs.ma". +include "SUB/preamble.ma". inductive Leaf: Set \def | sort: Nat \to Leaf diff --git a/matita/contribs/LAMBDA-TYPES/Unified/SUB/preamble.ma b/matita/contribs/LAMBDA-TYPES/Unified/SUB/preamble.ma new file mode 100644 index 000000000..4a348cc67 --- /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". -- 2.39.2