update in ground

+ WIP on subsets

diff --git a/matita/matita/contribs/lambdadelta/ground/lib/logic.ma b/matita/matita/contribs/lambdadelta/ground/lib/logic.ma
index 4cf0e0096bbbadb708bff33baedb38741354c601..8786e77aeb7556e003d1041be68190c27e7d1d10 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/lib/logic.ma
+++ b/matita/matita/contribs/lambdadelta/ground/lib/logic.ma
@@ -28,6 +28,9 @@ interpretation
 
 (* LOGIC ********************************************************************)
 
+definition negation (A:Prop): Prop ≝
+           A → ⊥.
+
 (* Constructions with land **************************************************)
 
 lemma commutative_and (A) (B):

diff --git a/matita/matita/contribs/lambdadelta/ground/lib/subset.ma b/matita/matita/contribs/lambdadelta/ground/lib/subset.ma
index 25863fe2b6f8547929aaae653dbbf0d93c5d983a..8f0154d813dd6ef8b96042b35a9b7c2915c377f1 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/lib/subset.ma
+++ b/matita/matita/contribs/lambdadelta/ground/lib/subset.ma
@@ -12,9 +12,10 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "ground/lib/relations.ma".
 include "ground/notation/functions/powerclass_1.ma".
 include "ground/notation/relations/epsilon_3.ma".
-include "ground/lib/relations.ma".
+include "ground/notation/relations/not_epsilon_3.ma".
 
 (* SUBSETS ******************************************************************)
 
@@ -31,3 +32,7 @@ definition subset_in (A): 𝒫❨A❩ → 𝒫❨A❩ ≝
 interpretation
   "membership (subset)"
   'Epsilon A a u = (subset_in A u a).
+
+interpretation
+  "negated membership (subset)"
+  'NotEpsilon A a u = (negation (subset_in A u a)).

diff --git a/matita/matita/contribs/lambdadelta/ground/lib/subset_ext.ma b/matita/matita/contribs/lambdadelta/ground/lib/subset_ext.ma
new file mode 100644 (file)
index 0000000..5d623ad
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground/lib/subset_ext.ma
@@ -0,0 +1,35 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "ground/lib/subset.ma".
+
+(* EXTENSIONS FOR SUBSETS ***************************************************)
+
+definition subset_ext_f1 (A1) (A0) (f:A1→A0): 𝒫❨A1❩ → 𝒫❨A0❩ ≝
+           λu1,a0. ∃∃a1. a1 ϵ u1 & f a1 = a0.
+
+definition subset_ext_p1 (A1) (Q:predicate A1): predicate (𝒫❨A1❩) ≝
+           λu1. ∀a1. a1 ϵ u1 → Q a1.
+
+(* Basic constructions ******************************************************)
+
+lemma subset_in_ext_f1_dx (A1) (A0) (f) (u1) (a1):
+      a1 ϵ u1 → f a1 ϵ subset_ext_f1 A1 A0 f u1.
+/2 width=3 by ex2_intro/ qed.
+
+(* Basic inversions *********************************************************)
+
+lemma subset_in_inv_ext_p1_dx (A1) (Q) (u1) (a1):
+      a1 ϵ u1 → subset_ext_p1 A1 Q u1 → Q a1.
+/2 width=1 by/ qed-.

diff --git a/matita/matita/contribs/lambdadelta/ground/lib/subset_ext_equivalence.ma b/matita/matita/contribs/lambdadelta/ground/lib/subset_ext_equivalence.ma
new file mode 100644 (file)
index 0000000..f20aca2
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground/lib/subset_ext_equivalence.ma
@@ -0,0 +1,26 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "ground/lib/subset_ext_inclusion.ma".
+include "ground/lib/subset_equivalence.ma".
+
+(* EXTENSIONS FOR SUBSETS ***************************************************)
+
+(* Constructions with subset_equivalence ************************************)
+
+lemma subset_equivalence_ext_f1_bi (A1) (A0) (f) (u1) (v1):
+      u1 ⇔ v1 → subset_ext_f1 A1 A0 f u1 ⇔ subset_ext_f1 A1 A0 f v1.
+#A1 #A0 #f #u1 #v1 * #Huv1 #Hvu1
+/3 width=3 by subset_inclusion_ext_f1_bi, conj/
+qed.

diff --git a/matita/matita/contribs/lambdadelta/ground/lib/subset_ext_inclusion.ma b/matita/matita/contribs/lambdadelta/ground/lib/subset_ext_inclusion.ma
new file mode 100644 (file)
index 0000000..7fd5fd4
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground/lib/subset_ext_inclusion.ma
@@ -0,0 +1,32 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "ground/lib/subset_inclusion.ma".
+include "ground/lib/subset_ext.ma".
+
+(* EXTENSIONS FOR SUBSETS ***************************************************)
+
+(* Constructions with subset_inclusion **************************************)
+
+lemma subset_inclusion_ext_f1_bi (A1) (A0) (f) (u1) (v1):
+      u1 ⊆ v1 → subset_ext_f1 A1 A0 f u1 ⊆ subset_ext_f1 A1 A0 f v1.
+#A1 #A0 #f #u1 #v1 #Huv1 #a0 * #a1 #Hau1 #H destruct
+/3 width=3 by subset_in_ext_f1_dx/
+qed.
+
+lemma subset_inclusion_ext_p1_trans (A1) (Q) (u1) (v1):
+      u1 ⊆ v1 → subset_ext_p1 A1 Q v1 → subset_ext_p1 A1 Q u1.
+#A1 #Q #u1 #v1 #Huv1 #Hv1
+/3 width=1 by/
+qed-.

diff --git a/matita/matita/contribs/lambdadelta/ground/notation/relations/not_epsilon_3.ma b/matita/matita/contribs/lambdadelta/ground/notation/relations/not_epsilon_3.ma
new file mode 100644 (file)
index 0000000..2bf35dc
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground/notation/relations/not_epsilon_3.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                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* GROUND NOTATION **********************************************************)
+
+notation < "hvbox( a ⧸ϵ break term 46 u )"
+  non associative with precedence 45
+  for @{ 'NotEpsilon $S $a $u }.
+
+notation > "hvbox( a ⧸ϵ break term 46 u )"
+  non associative with precedence 45
+  for @{ 'NotEpsilon ? $a $u }.
+
+notation > "hvbox( a ⧸ϵ{ break term 46 S } break term 46 u )"
+  non associative with precedence 45
+  for @{ 'NotEpsilon $S $a $u }.

diff --git a/matita/matita/predefined_virtuals.ml b/matita/matita/predefined_virtuals.ml
index cc2953e4dd28cfcf8766f7c6387485afd489374c..7656dc68c240f516dbf6ade102046239d29e2f8e 100644 (file)
--- a/matita/matita/predefined_virtuals.ml
+++ b/matita/matita/predefined_virtuals.ml
@@ -1503,6 +1503,7 @@ let load_predefined_virtuals () =
 ;;
 
 let predefined_classes = [
+ ["/"; "⧸"; ];
  ["&"; "⅋"; ];
  ["|"; "❘"; "∥"; ];
  ["!"; "¡"; "⫯"; "⫰"; "⟟"; "⫱"; ];