From 7ea8b1445c01013b270607d2182d506702646bf2 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sun, 11 Feb 2007 12:46:45 +0000 Subject: [PATCH] Unified: INC and BEq removed contribs: added dependence to ../legacy in the Makefile --- .../LAMBDA-TYPES/Unified-Sub/Inc/defs.ma | 26 --------------- .../LAMBDA-TYPES/Unified-Sub/Lift/defs.ma | 22 +++++++++---- .../LAMBDA-TYPES/Unified-Sub/preamble.ma | 1 - helm/software/matita/contribs/Makefile | 2 +- .../matita/contribs/RELATIONAL/BEq/defs.ma | 32 ------------------- 5 files changed, 16 insertions(+), 67 deletions(-) delete mode 100644 helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/Inc/defs.ma delete mode 100644 helm/software/matita/contribs/RELATIONAL/BEq/defs.ma 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 deleted file mode 100644 index d36f86abd..000000000 --- a/helm/software/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 "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/helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/defs.ma index cf29a3562..af573d360 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 @@ -18,21 +18,29 @@ set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified-Sub/Lift/defs". - Usage: invoke with positive polarity *) -include "Inc/defs.ma". +include "Term/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_lref : \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) + | lift_bind : \forall l,i,u1,u2. Lift true l i u1 u2 \to + \forall q,t1,t2. Lift q l (succ i) t1 t2 \to + \forall r. + Lift q l i (head q (bind r) u1 t1) (head q (bind r) u2 t2) + | lift_flat : \forall l,i,u1,u2. Lift true l i u1 u2 \to + \forall q,t1,t2. Lift q l i t1 t2 \to + \forall r. + Lift q l i (head q (flat r) u1 t1) (head q (flat r) u2 t2) + | lift_head : \forall l,qt,q. (qt = q \to False) \to + \forall i,u1,u2. Lift false l i u1 u2 \to + \forall t1,t2. Lift qt l i t1 t2 \to + \forall z. + Lift qt l i (head q z u1 t1) (head q z u2 t2) . diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/preamble.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/preamble.ma index 21afc1d99..45f2fb182 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/preamble.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/preamble.ma @@ -22,6 +22,5 @@ set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified-Sub/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/helm/software/matita/contribs/Makefile b/helm/software/matita/contribs/Makefile index 8dc8c4626..4fb6a0f11 100644 --- a/helm/software/matita/contribs/Makefile +++ b/helm/software/matita/contribs/Makefile @@ -1,6 +1,6 @@ GOALS = all opt clean clean.opt -DEVELS = ../library RELATIONAL LAMBDA-TYPES +DEVELS = ../library ../legacy RELATIONAL LAMBDA-TYPES $(GOALS): @$(foreach DEVEL, $(DEVELS), $(MAKE) -C $(DEVEL) $@;) diff --git a/helm/software/matita/contribs/RELATIONAL/BEq/defs.ma b/helm/software/matita/contribs/RELATIONAL/BEq/defs.ma deleted file mode 100644 index 3ab3b002e..000000000 --- a/helm/software/matita/contribs/RELATIONAL/BEq/defs.ma +++ /dev/null @@ -1,32 +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/RELATIONAL/BEq/defs". - -include "logic/equality.ma". - -include "Bool/defs.ma". - -inductive BEq (A:Type) (a1:A): A \to Bool \to Prop \def - | beq_true : BEq A a1 a1 true - | beq_false: \forall a2. (a1 = a2 -> False) \to BEq A a1 a2 false -. - -(*CSC: the URI must disappear: there is a bug now *) -interpretation "boolean equality" 'beq x y z = - (cic:/matita/RELATIONAL/BEq/defs/BEq.ind#xpointer(1/1) _ x y z). - -notation "hvbox(a break -- b break == c)" - non associative with precedence 95 -for @{ 'beq $a $b $c}. -- 2.39.2