update in ground

+ basic support for subsets as predicates

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/up_down_arrow_epsilon_2.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/up_down_arrow_epsilon_2.ma
deleted file mode 100644 (file)
index ffef611..0000000
--- a/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/up_down_arrow_epsilon_2.ma
+++ /dev/null
@@ -1,19 +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                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-(* NOTATION FOR DELAYED UPDATING ********************************************)
-
-notation "hvbox( p ϵ⬦ break term 46 t )"
-  non associative with precedence 45
-  for @{ 'UpDownArrowEpsilon $p $t }.

diff --git a/matita/matita/contribs/lambdadelta/ground/lib/subset.ma b/matita/matita/contribs/lambdadelta/ground/lib/subset.ma
new file mode 100644 (file)
index 0000000..25863fe
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground/lib/subset.ma
@@ -0,0 +1,33 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/notation/functions/powerclass_1.ma".
+include "ground/notation/relations/epsilon_3.ma".
+include "ground/lib/relations.ma".
+
+(* SUBSETS ******************************************************************)
+
+definition subset (A): Type[0] ≝
+           predicate A.
+
+interpretation
+  "power class (subset)"
+  'PowerClass A = (subset A).
+
+definition subset_in (A): 𝒫❨A❩ → 𝒫❨A❩ ≝
+           λu.u.
+
+interpretation
+  "membership (subset)"
+  'Epsilon A a u = (subset_in A u a).

diff --git a/matita/matita/contribs/lambdadelta/ground/lib/subset_equivalence.ma b/matita/matita/contribs/lambdadelta/ground/lib/subset_equivalence.ma
new file mode 100644 (file)
index 0000000..bab6b26
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground/lib/subset_equivalence.ma
@@ -0,0 +1,44 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/notation/relations/white_harrow_2.ma".
+include "ground/lib/subset_inclusion.ma".
+
+(* EQUIVALENCE FOR SUBSETS **************************************************)
+
+definition subset_eq (A): relation2 𝒫❨A❩ 𝒫❨A❩ ≝
+           λu1,u2. ∧∧ u1 ⊆ u2 & u2 ⊆ u1.
+
+interpretation
+  "equivalence (subset)"
+  'WhiteHArrow u1 u2 = (subset_eq ? u1 u2).
+
+(* Basic constructions ******************************************************)
+
+lemma subset_eq_refl (A):
+      reflexive … (subset_eq A).
+/2 width=1 by conj/ qed.
+
+lemma subset_eq_sym (A):
+      symmetric … (subset_eq A).
+#A #u1 #u2 * /2 width=1 by conj/
+qed-.
+
+(* Main constructions *******************************************************)
+
+theorem subset_eq_trans (A):
+        Transitive … (subset_eq A).
+#A #u1 #u2 * #H12 #H21 #u3 * #H23 #H32
+/3 width=5 by subset_le_trans, conj/
+qed-.

diff --git a/matita/matita/contribs/lambdadelta/ground/lib/subset_inclusion.ma b/matita/matita/contribs/lambdadelta/ground/lib/subset_inclusion.ma
new file mode 100644 (file)
index 0000000..6f2e5c9
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground/lib/subset_inclusion.ma
@@ -0,0 +1,36 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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".
+
+(* INCLUSION FOR SUBSETS ****************************************************)
+
+definition subset_le (A): relation2 𝒫❨A❩ 𝒫❨A❩ ≝
+           λu1,u2. ∀p. p ϵ u1 → p ϵ u2.
+
+interpretation
+  "inclusion (subset)"
+  'subseteq u1 u2 = (subset_le ? u1 u2).
+
+(* Basic constructions ******************************************************)
+
+lemma subset_le_refl (A):
+      reflexive … (subset_le A).
+// qed.
+
+(* Main constructions *******************************************************)
+
+theorem subset_le_trans (A):
+        Transitive … (subset_le A).
+/3 width=1 by/ qed-.

diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/powerclass_1.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/powerclass_1.ma
new file mode 100644 (file)
index 0000000..8eab6e6
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/powerclass_1.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                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* GROUND NOTATION **********************************************************)
+
+notation "hvbox( 𝒫 ❨ break term 46 S ❩ )"
+  non associative with precedence 75
+  for @{ 'PowerClass $S }.

diff --git a/matita/matita/contribs/lambdadelta/ground/notation/relations/epsilon_3.ma b/matita/matita/contribs/lambdadelta/ground/notation/relations/epsilon_3.ma
new file mode 100644 (file)
index 0000000..2f5287d
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground/notation/relations/epsilon_3.ma
@@ -0,0 +1,29 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* NOTATION FOR DELAYED UPDATING ********************************************)
+
+(* GROUND NOTATION **********************************************************)
+
+notation < "hvbox( a ϵ break term 46 u )"
+  non associative with precedence 45
+  for @{ 'Epsilon $S $a $u }.
+
+notation > "hvbox( a ϵ break term 46 u )"
+  non associative with precedence 45
+  for @{ 'Epsilon ? $a $u }.
+
+notation > "hvbox( a ϵ{ break term 46 S } break term 46 u )"
+  non associative with precedence 45
+  for @{ 'Epsilon $S $a $u }.

diff --git a/matita/matita/contribs/lambdadelta/ground/notation/relations/white_harrow_2.ma b/matita/matita/contribs/lambdadelta/ground/notation/relations/white_harrow_2.ma
new file mode 100644 (file)
index 0000000..b7130df
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground/notation/relations/white_harrow_2.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                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* GROUND NOTATION **********************************************************)
+
+notation "hvbox( a1 ⇔ break term 46 a2 )"
+  non associative with precedence 45
+  for @{ 'WhiteHArrow $a1 $a2 }.

diff --git a/matita/matita/predefined_virtuals.ml b/matita/matita/predefined_virtuals.ml
index a816099a6c901023d9b2c683d09441fdd7e2b9b3..1271e2c523bc135cc1c593d57c8456d730f73138 100644 (file)
--- a/matita/matita/predefined_virtuals.ml
+++ b/matita/matita/predefined_virtuals.ml
@@ -1565,7 +1565,7 @@ let predefined_classes = [
  ["o"; "θ"; "ϑ"; "𝕠"; "∘";  "⊚"; "ø"; "○"; "●"; "𝐨"; "𝛉"; "ⓞ"; ] ;
  ["O"; "Θ"; "𝕆"; "𝐎"; "𝚯"; "𝚹"; "Ⓞ"; ] ;
  ["p"; "π"; "𝕡"; "𝐩"; "𝛑"; "ⓟ"; ] ;
- ["P"; "Π"; "℘"; "ℙ"; "𝐏"; "𝚷"; "Ⓟ"; ] ;
+ ["P"; "Π"; "℘"; "ℙ"; "𝐏"; "𝚷"; "Ⓟ"; "𝒫"; ] ;
  ["q"; "𝕢"; "𝐪"; "ⓠ"; ] ;
  ["Q"; "ℚ"; "𝐐"; "Ⓠ"; ] ;
  ["r"; "ρ"; "ϱ"; "𝕣"; "𝐫"; "𝛒"; "𝛠"; "ⓡ"; ] ;