From 2d4205b85b48a73d5b708a9dfa7bca9dcab664ca Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sun, 20 Aug 2006 19:44:22 +0000 Subject: [PATCH] new definitions --- .../contribs/RELATIONAL-ARITHMETICS/BEq.ma | 23 +++++++++++++++++++ .../contribs/RELATIONAL-ARITHMETICS/BNot.ma | 21 +++++++++++++++++ .../contribs/RELATIONAL-ARITHMETICS/Bool.ma | 19 +++++++++++++++ .../contribs/RELATIONAL-ARITHMETICS/NLE.ma | 21 +++++++++++++++++ .../contribs/RELATIONAL-ARITHMETICS/Nat.ma | 2 -- .../RELATIONAL-ARITHMETICS/Nat_fwd.ma | 2 ++ .../contribs/RELATIONAL-ARITHMETICS/Plus.ma | 2 ++ 7 files changed, 88 insertions(+), 2 deletions(-) create mode 100644 helm/software/matita/contribs/RELATIONAL-ARITHMETICS/BEq.ma create mode 100644 helm/software/matita/contribs/RELATIONAL-ARITHMETICS/BNot.ma create mode 100644 helm/software/matita/contribs/RELATIONAL-ARITHMETICS/Bool.ma create mode 100644 helm/software/matita/contribs/RELATIONAL-ARITHMETICS/NLE.ma diff --git a/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/BEq.ma b/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/BEq.ma new file mode 100644 index 000000000..cf837aee7 --- /dev/null +++ b/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/BEq.ma @@ -0,0 +1,23 @@ +(**************************************************************************) +(* ___ *) +(* ||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-ARITHMETICS/BEq". + +include "logic/equality.ma". + +include "BNot.ma". + +inductive BEq (b1:Bool): Bool \to Bool \to Prop \def + | BEq_false: \forall b2. BNot b1 b2 \to BEq b1 false b2 + | BEq_true : BEq b1 true b1. diff --git a/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/BNot.ma b/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/BNot.ma new file mode 100644 index 000000000..8d6405407 --- /dev/null +++ b/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/BNot.ma @@ -0,0 +1,21 @@ +(**************************************************************************) +(* ___ *) +(* ||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-ARITHMETICS/BNot". + +include "Bool.ma". + +inductive BNot: Bool \to Bool \to Prop \def + | BNot_false: BNot false true + | BNot_true : BNot true false. diff --git a/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/Bool.ma b/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/Bool.ma new file mode 100644 index 000000000..1d7b343fc --- /dev/null +++ b/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/Bool.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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-ARITHMETICS/Bool". + +inductive Bool: Set \def + | false: Bool + | true: Bool. diff --git a/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/NLE.ma b/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/NLE.ma new file mode 100644 index 000000000..8e9c492c8 --- /dev/null +++ b/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/NLE.ma @@ -0,0 +1,21 @@ +(**************************************************************************) +(* ___ *) +(* ||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-ARITHMETICS/NLE". + +include "Nat.ma". + +inductive NLE: Nat \to Nat \to Prop \def + | NLE_zero: \forall q. NLE zero q + | NLE_succ: \forall p,q. NLE p q \to NLE (succ p) (succ q). diff --git a/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/Nat.ma b/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/Nat.ma index bc0624140..e3721fcd4 100644 --- a/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/Nat.ma +++ b/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/Nat.ma @@ -14,8 +14,6 @@ set "baseuri" "cic:/matita/RELATIONAL-ARITHMETICS/Nat". -include "logic/equality.ma". - inductive Nat: Set \def | zero: Nat | succ: Nat \to Nat. diff --git a/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/Nat_fwd.ma b/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/Nat_fwd.ma index ede85286a..adfdcace4 100644 --- a/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/Nat_fwd.ma +++ b/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/Nat_fwd.ma @@ -14,6 +14,8 @@ set "baseuri" "cic:/matita/RELATIONAL-ARITHMETICS/Nat_fwd". +include "logic/equality.ma". + include "Nat.ma". theorem eq_gen_zero_succ: \forall (P:Prop). \forall m2. zero = succ m2 \to P. diff --git a/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/Plus.ma b/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/Plus.ma index 5d8f4f3ec..5b86bf749 100644 --- a/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/Plus.ma +++ b/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/Plus.ma @@ -14,6 +14,8 @@ set "baseuri" "cic:/matita/RELATIONAL-ARITHMETICS/Plus". +include "logic/equality.ma". + include "Nat.ma". inductive Plus (p:Nat): Nat \to Nat \to Prop \def -- 2.39.2