From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 8 Jul 2009 02:13:35 +0000 (+0000)
Subject: ...
X-Git-Tag: make_still_working~3739
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=sidebyside;h=9a7ec6adbfd12e5305800a033d1b471afe316abd;p=helm.git

...
---

diff --git a/helm/software/matita/nlibrary/algebra/magmas.ma b/helm/software/matita/nlibrary/algebra/magmas.ma
new file mode 100644
index 000000000..de8e3ba22
--- /dev/null
+++ b/helm/software/matita/nlibrary/algebra/magmas.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                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "sets/sets.ma".
+
+nrecord magma (A: Type) : Type ≝
+ { carr: Ω \sup A(*;
+   op: A → A → A;
+   op_closed: ∀x,y. x ∈ carr → y ∈ carr → op x y ∈ carr*)
+ }.
\ No newline at end of file
diff --git a/helm/software/matita/nlibrary/depends b/helm/software/matita/nlibrary/depends
index 857215f68..1b7a60cdb 100644
--- a/helm/software/matita/nlibrary/depends
+++ b/helm/software/matita/nlibrary/depends
@@ -1,3 +1,5 @@
-sets/sets.ma logic/connectives.ma
+sets/sets.ma logic/equality.ma
+logic/equality.ma logic/connectives.ma
 logic/connectives.ma logic/pts.ma
+algebra/magmas.ma sets/sets.ma
 logic/pts.ma 
diff --git a/helm/software/matita/nlibrary/depends.dot b/helm/software/matita/nlibrary/depends.dot
index 710415825..eb6855410 100644
--- a/helm/software/matita/nlibrary/depends.dot
+++ b/helm/software/matita/nlibrary/depends.dot
@@ -1,8 +1,12 @@
 digraph g {
   "sets/sets.ma" [];
-  "sets/sets.ma" -> "logic/connectives.ma" [];
+  "sets/sets.ma" -> "logic/equality.ma" [];
+  "logic/equality.ma" [];
+  "logic/equality.ma" -> "logic/connectives.ma" [];
   "logic/connectives.ma" [];
   "logic/connectives.ma" -> "logic/pts.ma" [];
+  "algebra/magmas.ma" [];
+  "algebra/magmas.ma" -> "sets/sets.ma" [];
   "logic/pts.ma" [];
   
   }
\ No newline at end of file
diff --git a/helm/software/matita/nlibrary/depends.png b/helm/software/matita/nlibrary/depends.png
index 631218af1..31bab1539 100644
Binary files a/helm/software/matita/nlibrary/depends.png and b/helm/software/matita/nlibrary/depends.png differ
diff --git a/helm/software/matita/nlibrary/logic/equality.ma b/helm/software/matita/nlibrary/logic/equality.ma
new file mode 100644
index 000000000..d940b97c0
--- /dev/null
+++ b/helm/software/matita/nlibrary/logic/equality.ma
@@ -0,0 +1,22 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "logic/connectives.ma".
+
+ninductive eq (A: Type) (a: A) : A → Prop ≝
+ refl: eq A a a.
+ 
+interpretation "leibnitz's equality" 'eq t x y = (eq t x y).
+
+interpretation "leibnitz's non-equality" 'neq t x y = (Not (eq t x y)).
\ No newline at end of file
diff --git a/helm/software/matita/nlibrary/sets/sets.ma b/helm/software/matita/nlibrary/sets/sets.ma
index 5ba0b08a6..a12f1fc5c 100644
--- a/helm/software/matita/nlibrary/sets/sets.ma
+++ b/helm/software/matita/nlibrary/sets/sets.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "logic/connectives.ma".
+include "logic/equality.ma".
 
 nrecord powerset (A: Type) : Type[1] ≝ { mem: A → CProp }.
 (* This is a projection! *)
@@ -49,8 +49,6 @@ ndefinition union ≝ λA.λU,V:Ω \sup A. {x | x ∈ U ∨ x ∈ V }.
 
 interpretation "union" 'union U V = (union ? U V).
 
-(*
 ndefinition singleton ≝ λA.λa:A.{b | a=b}.
 
 interpretation "singleton" 'singl a = (singleton ? a).
-*)
\ No newline at end of file