From: Ferruccio Guidi Date: Fri, 19 Jan 2007 14:20:38 +0000 (+0000) Subject: Unified: refactoring X-Git-Tag: make_still_working~6518 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b9d2eac98d0471eeadb6d524135bd604a9e8c757;p=helm.git Unified: refactoring --- 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 deleted file mode 100644 index 2b93d7783..000000000 --- a/helm/software/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/helm/software/matita/contribs/LAMBDA-TYPES/Unified/SUB/Context/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Unified/SUB/Context/defs.ma new file mode 100644 index 000000000..39859fc0e --- /dev/null +++ b/helm/software/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/helm/software/matita/contribs/LAMBDA-TYPES/Unified/SUB/Inc/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Unified/SUB/Inc/defs.ma index 59c085963..266e3c7b7 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Unified/SUB/Inc/defs.ma +++ b/helm/software/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/helm/software/matita/contribs/LAMBDA-TYPES/Unified/SUB/Lift/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Unified/SUB/Lift/defs.ma index a6c3345ca..dc12e8cc8 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Unified/SUB/Lift/defs.ma +++ b/helm/software/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/helm/software/matita/contribs/LAMBDA-TYPES/Unified/SUB/Switch/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Unified/SUB/Switch/defs.ma new file mode 100644 index 000000000..7a435021f --- /dev/null +++ b/helm/software/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/helm/software/matita/contribs/LAMBDA-TYPES/Unified/SUB/T/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Unified/SUB/T/defs.ma deleted file mode 100644 index df6e1945e..000000000 --- a/helm/software/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/helm/software/matita/contribs/LAMBDA-TYPES/Unified/SUB/Term/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Unified/SUB/Term/defs.ma new file mode 100644 index 000000000..d1559a40a --- /dev/null +++ b/helm/software/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/helm/software/matita/contribs/LAMBDA-TYPES/Unified/SUB/preamble.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Unified/SUB/preamble.ma new file mode 100644 index 000000000..4a348cc67 --- /dev/null +++ b/helm/software/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".