+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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 "preamble.ma".
-
-(* CLASSES:
- - We use typoids with a compatible membership relation
- - The category is intended to be the domain of the membership relation
- - The membership relation is necessary because we need to regard the
- domain of a propositional function (ie a predicative subset) as a
- quantification domain and therefore as a category, but there is no
- type in CIC representing the domain of a propositional function
- - We set up a single equality predicate, parametric on the category,
- defined as the reflexive, symmetic, transitive and compatible closure
- of the "ces" (class equality step) predicate given inside the category.
-*)
-
-record Class: Type ≝ {
- class :> Type;
- cin : class → Prop;
- ces : class → class → Prop;
- ces_cin_fw: ∀c1,c2. cin c1 → ces c1 c2 → cin c2;
- ces_cin_bw: ∀c1,c2. cin c1 → ces c2 c1 → cin c2
-}.
-
-(* equality predicate *******************************************************)
-
-inductive ceq (C:Class): class C → class C → Prop ≝
- | ceq_refl : ∀c. ceq ? c c
- | ceq_trans: ∀c1,c,c2. ces ? c1 c → ceq ? c c2 → ceq ? c1 c2
- | ceq_conf : ∀c1,c,c2. ces ? c c1 → ceq ? c c2 → ceq ? c1 c2
-.
-
-(* default inhabitance predicates *******************************************)
-
-definition true_f ≝ λX:Type. λ_:X. True.
-
-definition false_f ≝ λX:Type. λ_:X. False.
-
-(* default foreward compatibilities *****************************************)
-
-theorem const_fw: ∀A:Prop. ∀X:Type. ∀P:X→X→Prop. ∀x1,x2. A → P x1 x2 → A.
-intros; autobatch.
-qed.
-
-definition true_fw ≝ const_fw True.
-
-definition false_fw ≝ const_fw False.
-
-(* default backward compatibilities *****************************************)
-
-theorem const_bw: ∀A:Prop. ∀X:Type. ∀P:X→X→Prop. ∀x1,x2. A → P x2 x1 → A.
-intros; autobatch.
-qed.
-
-definition true_bw ≝ const_bw True.
-
-definition false_bw ≝ const_bw False.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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 "Class/defs.ma".
-
-(* CLASSES:
- - Here we prove the standard properties of the equality.
-*)
-
-theorem ceq_cin_fw: ∀C,c1,c2. ceq C c1 c2 → cin ? c1 → cin ? c2.
-intros 4; elim H; clear H c1 c2; autobatch.
-qed.
-
-theorem ceq_cin_bw: ∀C,c1,c2. ceq C c1 c2 → cin ? c2 → cin ? c1.
-intros 4; elim H; clear H c1 c2; autobatch.
-qed.
-
-theorem ceq_trans: ∀C,c1,c2. ceq C c1 c2 → ∀c3. ceq ? c2 c3 → ceq ? c1 c3.
-intros 4; elim H; clear H c1 c2; autobatch.
-qed.
-
-theorem ceq_sym: ∀ C,c1,c2. ceq C c1 c2 → ceq ? c2 c1.
-intros; elim H; clear H c1 c2; autobatch.
-qed.
-
-theorem ceq_conf: ∀C,c1,c2. ceq C c1 c2 → ∀c3. ceq ? c1 c3 → ceq ? c2 c3.
-intros; autobatch.
-qed.
-
-theorem ceq_repl: ∀C,c1,c2. ceq C c1 c2 →
- ∀d1. ceq ? c1 d1 → ∀d2. ceq ? c2 d2 → ceq ? d1 d2.
-intros; autobatch.
-qed.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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 "Domain/defs.ma".
-
-(* QUANTIFICATION DOMAINS
- - Here we define some useful domains based on data types.
-*)
-
-definition DBool: Domain ≝
- mk_Domain (
- mk_Class bool (true_f ?) (eq ?) (true_fw ? ?) (true_bw ? ?)
- ).
-(*
-definition dbool_ixfam : \forall (C:Class). C \to C \to (DBool \to C) \def
- \lambda C,c0,c1,b.
- match b in bool with
- [ false \Rightarrow c0
- | true \Rightarrow c1
- ].
-*)
-definition DVoid: Domain ≝
- mk_Domain (
- mk_Class void (true_f ?) (eq ?) (true_fw ? ?) (true_bw ? ?)
- ).
-(*
-definition dvoid_ixfam : \forall (C:Class). (DVoid \to C) \def
- \lambda C,v.
- match v in void with [].
-*)
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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 "Class/defs.ma".
-
-(* QUANTIFICATION DOMAINS
- - These are the categories on which we allow quantification.
- - We set up single quantifiers, parametric on the domain.
-*)
-
-record Domain: Type ≝ {
- domain:> Class
-}.
-
-(* internal universal quantification *)
-inductive dall (D:Domain) (P:D → Prop): Prop ≝
- | dall_intro: (∀d. cin ? d → P d) → dall D P
-.
-
-interpretation "internal for all" 'iforall η.x = (dall ? x).
-
-(* internal existential quantification *)
-inductive dex (D:Domain) (P:D → Prop): Prop ≝
- | dex_intro: ∀d. cin D d → P d → dex D P
-.
-
-interpretation "internal exists" 'iexists η.x = (dex ? x).
+++ /dev/null
-include ../Makefile.defs
-
-DIR=$(shell basename $$PWD)
-
-$(DIR) all:
- $(BIN)matitac
-$(DIR).opt opt all.opt:
- $(BIN)matitac.opt
-clean:
- $(BIN)matitaclean
-clean.opt:
- $(BIN)matitaclean.opt
-depend:
- $(BIN)matitadep
-depend.opt:
- $(BIN)matitadep.opt
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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 "Domain/defs.ma".
-
-(* SUBSETS
- - We use predicative subsets encoded as propositional functions
- according to Sambin/Valentini "Toolbox".
-*)
-
-record Subset (D:Domain): Type ≝ {
- subset :1> D → Prop;
- ces_subset_fw: ∀d1,d2. subset d1 → ces ? d1 d2 → subset d2;
- ces_subset_bw: ∀d1,d2. subset d1 → ces ? d2 d1 → subset d2
-}.
-
-(* subset membership (epsilon) ********************************************)
-
-definition sin: ∀D. Subset D → D → Prop ≝
- λD. λU:Subset D. λd. cin D d ∧ U d.
-
-theorem sin_i: ∀D. ∀U:Subset D. ∀d. cin D d → U d → sin ? U d.
- unfold sin; intros; autobatch.
-qed.
-
-theorem sin_e1: ∀D. ∀U:Subset D. ∀d. sin ? U d → cin D d.
- intros; decompose; autobatch.
-qed.
-
-theorem sin_e2: ∀D. ∀U:Subset D. ∀d. sin ? U d → U d.
- intros; decompose; autobatch.
-qed.
-
-(* the domain built upon a subset *****************************************)
-
-theorem ces_sin_fw: ∀D,U,d1,d2. sin D U d1 → ces ? d1 d2 → sin D U d2.
- intros;
- apply sin_i;
- [ autobatch
- | apply (ces_subset_fw D U d1); [ apply sin_e2; autobatch | autobatch ] (**)
- ].
-qed.
-
-theorem ces_sin_bw: ∀D,U,d1,d2. sin D U d1 → ces ? d2 d1 → sin D U d2.
- intros;
- apply sin_i;
- [ autobatch
- | apply (ces_subset_bw D U d1); [ apply sin_e2; autobatch | autobatch ] (**)
- ].
-qed.
-
-definition domain_of_subset: ∀D. Subset D → Domain ≝
- λD:Domain. λU.
- mk_Domain (mk_Class D (sin D U) (ces D) (ces_sin_fw ? ?) (ces_sin_bw ? ?)).
-
-coercion domain_of_subset.
-
-(* subset top (full subset) ***********************************************)
-
-definition stop: ∀D. Subset D ≝
- λD. mk_Subset D (true_f ?) (true_fw ? ?) (true_bw ? ?).
-
-coercion stop nocomposites.
-
-(* subset bottom (empty subset) *******************************************)
-
-definition sbot: ∀D. Subset D ≝
- λD. mk_Subset D (false_f ?) (false_fw ? ?) (false_bw ? ?).
-
-(* subset and (binary intersection) ***************************************)
-
-theorem ces_sand_fw:
- ∀D. ∀U1,U2:Subset D. ∀d1,d2. U1 d1 ∧ U2 d1 → ces ? d1 d2 → U1 d2 ∧ U2 d2.
- intros; decompose; apply conj;
- [ apply (ces_subset_fw D U1 d1); autobatch (**)
- | apply (ces_subset_fw D U2 d1); autobatch
- ].
-qed.
-
-theorem ces_sand_bw:
- ∀D. ∀U1,U2:Subset D. ∀d1,d2. U1 d1 ∧ U2 d1 → ces ? d2 d1 → U1 d2 ∧ U2 d2.
- intros; decompose; apply conj;
- [ apply (ces_subset_bw D U1 d1); autobatch (**)
- | apply (ces_subset_bw D U2 d1); autobatch
- ].
-qed.
-
-definition sand: ∀D. Subset D → Subset D → Subset D ≝
- λD,U1,U2.
- mk_Subset D (λd. U1 d ∧ U2 d) (ces_sand_fw ? U1 U2) (ces_sand_bw ? U1 U2).
-
-(* subset or (binary union) ***********************************************)
-
-theorem ces_sor_fw:
- ∀D. ∀U1,U2:Subset D. ∀d1,d2. U1 d1 ∨ U2 d1 → ces ? d1 d2 → U1 d2 ∨ U2 d2.
- intros; decompose;
- [ apply or_introl; apply (ces_subset_fw D U1 d1); autobatch (**)
- | apply or_intror; apply (ces_subset_fw D U2 d1); autobatch
- ].
-qed.
-
-theorem ces_sor_bw:
- ∀D. ∀U1,U2:Subset D. ∀d1,d2. U1 d1 ∨ U2 d1 → ces ? d2 d1 → U1 d2 ∨ U2 d2.
- intros; decompose;
- [ apply or_introl; apply (ces_subset_bw D U1 d1); autobatch (**)
- | apply or_intror; apply (ces_subset_bw D U2 d1); autobatch
- ].
-qed.
-
-definition sor: ∀D. Subset D → Subset D → Subset D ≝
- λD,U1,U2.
- mk_Subset D (λd. U1 d ∨ U2 d) (ces_sor_fw ? U1 U2) (ces_sor_bw ? U1 U2).
-
-(* subset less or equal (inclusion) ***************************************)
-
-definition sle: ∀D. Subset D → Subset D → Prop ≝
- λD. λU1,U2:Subset D. \iforall d. U1 d → U2 d.
-
-(* subset overlap *********************************************************)
-
-definition sover: ∀D. Subset D → Subset D → Prop ≝
- λD. λU1,U2:Subset D. \iexists d. U1 d ∧ U2 d.
-
-(* the class of the subsets of a domain ***********************************)
-
-definition power: Domain → Class ≝
- λD. mk_Class (Subset D) (true_f ?) (sle ?) (true_fw ? ?) (true_bw ? ?).
+++ /dev/null
-preamble.ma datatypes/bool.ma datatypes/constructors.ma logic/connectives.ma
-Class/eq.ma Class/defs.ma
-Domain/defs.ma Class/defs.ma
-Domain/data.ma Domain/defs.ma
-Subset/defs.ma Domain/defs.ma
-Class/defs.ma preamble.ma
-datatypes/bool.ma
-datatypes/constructors.ma
-logic/connectives.ma
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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 "preamble.ma".
+
+(* CLASSES:
+ - We use typoids with a compatible membership relation
+ - The category is intended to be the domain of the membership relation
+ - The membership relation is necessary because we need to regard the
+ domain of a propositional function (ie a predicative subset) as a
+ quantification domain and therefore as a category, but there is no
+ type in CIC representing the domain of a propositional function
+ - We set up a single equality predicate, parametric on the category,
+ defined as the reflexive, symmetic, transitive and compatible closure
+ of the "ces" (class equality step) predicate given inside the category.
+*)
+
+record Class: Type ≝ {
+ class :> Type;
+ cin : class → Prop;
+ ces : class → class → Prop;
+ ces_cin_fw: ∀c1,c2. cin c1 → ces c1 c2 → cin c2;
+ ces_cin_bw: ∀c1,c2. cin c1 → ces c2 c1 → cin c2
+}.
+
+(* equality predicate *******************************************************)
+
+inductive ceq (C:Class): class C → class C → Prop ≝
+ | ceq_refl : ∀c. ceq ? c c
+ | ceq_trans: ∀c1,c,c2. ces ? c1 c → ceq ? c c2 → ceq ? c1 c2
+ | ceq_conf : ∀c1,c,c2. ces ? c c1 → ceq ? c c2 → ceq ? c1 c2
+.
+
+(* default inhabitance predicates *******************************************)
+
+definition true_f ≝ λX:Type. λ_:X. True.
+
+definition false_f ≝ λX:Type. λ_:X. False.
+
+(* default foreward compatibilities *****************************************)
+
+theorem const_fw: ∀A:Prop. ∀X:Type. ∀P:X→X→Prop. ∀x1,x2. A → P x1 x2 → A.
+intros; autobatch.
+qed.
+
+definition true_fw ≝ const_fw True.
+
+definition false_fw ≝ const_fw False.
+
+(* default backward compatibilities *****************************************)
+
+theorem const_bw: ∀A:Prop. ∀X:Type. ∀P:X→X→Prop. ∀x1,x2. A → P x2 x1 → A.
+intros; autobatch.
+qed.
+
+definition true_bw ≝ const_bw True.
+
+definition false_bw ≝ const_bw False.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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 "Class/defs.ma".
+
+(* CLASSES:
+ - Here we prove the standard properties of the equality.
+*)
+
+theorem ceq_cin_fw: ∀C,c1,c2. ceq C c1 c2 → cin ? c1 → cin ? c2.
+intros 4; elim H; clear H c1 c2; autobatch.
+qed.
+
+theorem ceq_cin_bw: ∀C,c1,c2. ceq C c1 c2 → cin ? c2 → cin ? c1.
+intros 4; elim H; clear H c1 c2; autobatch.
+qed.
+
+theorem ceq_trans: ∀C,c1,c2. ceq C c1 c2 → ∀c3. ceq ? c2 c3 → ceq ? c1 c3.
+intros 4; elim H; clear H c1 c2; autobatch.
+qed.
+
+theorem ceq_sym: ∀ C,c1,c2. ceq C c1 c2 → ceq ? c2 c1.
+intros; elim H; clear H c1 c2; autobatch.
+qed.
+
+theorem ceq_conf: ∀C,c1,c2. ceq C c1 c2 → ∀c3. ceq ? c1 c3 → ceq ? c2 c3.
+intros; autobatch.
+qed.
+
+theorem ceq_repl: ∀C,c1,c2. ceq C c1 c2 →
+ ∀d1. ceq ? c1 d1 → ∀d2. ceq ? c2 d2 → ceq ? d1 d2.
+intros; autobatch.
+qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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 "Domain/defs.ma".
+
+(* QUANTIFICATION DOMAINS
+ - Here we define some useful domains based on data types.
+*)
+
+definition DBool: Domain ≝
+ mk_Domain (
+ mk_Class bool (true_f ?) (eq ?) (true_fw ? ?) (true_bw ? ?)
+ ).
+(*
+definition dbool_ixfam : \forall (C:Class). C \to C \to (DBool \to C) \def
+ \lambda C,c0,c1,b.
+ match b in bool with
+ [ false \Rightarrow c0
+ | true \Rightarrow c1
+ ].
+*)
+definition DVoid: Domain ≝
+ mk_Domain (
+ mk_Class void (true_f ?) (eq ?) (true_fw ? ?) (true_bw ? ?)
+ ).
+(*
+definition dvoid_ixfam : \forall (C:Class). (DVoid \to C) \def
+ \lambda C,v.
+ match v in void with [].
+*)
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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 "Class/defs.ma".
+
+(* QUANTIFICATION DOMAINS
+ - These are the categories on which we allow quantification.
+ - We set up single quantifiers, parametric on the domain.
+*)
+
+record Domain: Type ≝ {
+ domain:> Class
+}.
+
+(* internal universal quantification *)
+inductive dall (D:Domain) (P:D → Prop): Prop ≝
+ | dall_intro: (∀d. cin ? d → P d) → dall D P
+.
+
+interpretation "internal for all" 'iforall η.x = (dall ? x).
+
+(* internal existential quantification *)
+inductive dex (D:Domain) (P:D → Prop): Prop ≝
+ | dex_intro: ∀d. cin D d → P d → dex D P
+.
+
+interpretation "internal exists" 'iexists η.x = (dex ? x).
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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 "Domain/defs.ma".
+
+(* SUBSETS
+ - We use predicative subsets encoded as propositional functions
+ according to Sambin/Valentini "Toolbox".
+*)
+
+record Subset (D:Domain): Type ≝ {
+ subset :1> D → Prop;
+ ces_subset_fw: ∀d1,d2. subset d1 → ces ? d1 d2 → subset d2;
+ ces_subset_bw: ∀d1,d2. subset d1 → ces ? d2 d1 → subset d2
+}.
+
+(* subset membership (epsilon) ********************************************)
+
+definition sin: ∀D. Subset D → D → Prop ≝
+ λD. λU:Subset D. λd. cin D d ∧ U d.
+
+theorem sin_i: ∀D. ∀U:Subset D. ∀d. cin D d → U d → sin ? U d.
+ unfold sin; intros; autobatch.
+qed.
+
+theorem sin_e1: ∀D. ∀U:Subset D. ∀d. sin ? U d → cin D d.
+ intros; decompose; autobatch.
+qed.
+
+theorem sin_e2: ∀D. ∀U:Subset D. ∀d. sin ? U d → U d.
+ intros; decompose; autobatch.
+qed.
+
+(* the domain built upon a subset *****************************************)
+
+theorem ces_sin_fw: ∀D,U,d1,d2. sin D U d1 → ces ? d1 d2 → sin D U d2.
+ intros;
+ apply sin_i;
+ [ autobatch
+ | apply (ces_subset_fw D U d1); [ apply sin_e2; autobatch | autobatch ] (**)
+ ].
+qed.
+
+theorem ces_sin_bw: ∀D,U,d1,d2. sin D U d1 → ces ? d2 d1 → sin D U d2.
+ intros;
+ apply sin_i;
+ [ autobatch
+ | apply (ces_subset_bw D U d1); [ apply sin_e2; autobatch | autobatch ] (**)
+ ].
+qed.
+
+definition domain_of_subset: ∀D. Subset D → Domain ≝
+ λD:Domain. λU.
+ mk_Domain (mk_Class D (sin D U) (ces D) (ces_sin_fw ? ?) (ces_sin_bw ? ?)).
+
+coercion domain_of_subset.
+
+(* subset top (full subset) ***********************************************)
+
+definition stop: ∀D. Subset D ≝
+ λD. mk_Subset D (true_f ?) (true_fw ? ?) (true_bw ? ?).
+
+coercion stop nocomposites.
+
+(* subset bottom (empty subset) *******************************************)
+
+definition sbot: ∀D. Subset D ≝
+ λD. mk_Subset D (false_f ?) (false_fw ? ?) (false_bw ? ?).
+
+(* subset and (binary intersection) ***************************************)
+
+theorem ces_sand_fw:
+ ∀D. ∀U1,U2:Subset D. ∀d1,d2. U1 d1 ∧ U2 d1 → ces ? d1 d2 → U1 d2 ∧ U2 d2.
+ intros; decompose; apply conj;
+ [ apply (ces_subset_fw D U1 d1); autobatch (**)
+ | apply (ces_subset_fw D U2 d1); autobatch
+ ].
+qed.
+
+theorem ces_sand_bw:
+ ∀D. ∀U1,U2:Subset D. ∀d1,d2. U1 d1 ∧ U2 d1 → ces ? d2 d1 → U1 d2 ∧ U2 d2.
+ intros; decompose; apply conj;
+ [ apply (ces_subset_bw D U1 d1); autobatch (**)
+ | apply (ces_subset_bw D U2 d1); autobatch
+ ].
+qed.
+
+definition sand: ∀D. Subset D → Subset D → Subset D ≝
+ λD,U1,U2.
+ mk_Subset D (λd. U1 d ∧ U2 d) (ces_sand_fw ? U1 U2) (ces_sand_bw ? U1 U2).
+
+(* subset or (binary union) ***********************************************)
+
+theorem ces_sor_fw:
+ ∀D. ∀U1,U2:Subset D. ∀d1,d2. U1 d1 ∨ U2 d1 → ces ? d1 d2 → U1 d2 ∨ U2 d2.
+ intros; decompose;
+ [ apply or_introl; apply (ces_subset_fw D U1 d1); autobatch (**)
+ | apply or_intror; apply (ces_subset_fw D U2 d1); autobatch
+ ].
+qed.
+
+theorem ces_sor_bw:
+ ∀D. ∀U1,U2:Subset D. ∀d1,d2. U1 d1 ∨ U2 d1 → ces ? d2 d1 → U1 d2 ∨ U2 d2.
+ intros; decompose;
+ [ apply or_introl; apply (ces_subset_bw D U1 d1); autobatch (**)
+ | apply or_intror; apply (ces_subset_bw D U2 d1); autobatch
+ ].
+qed.
+
+definition sor: ∀D. Subset D → Subset D → Subset D ≝
+ λD,U1,U2.
+ mk_Subset D (λd. U1 d ∨ U2 d) (ces_sor_fw ? U1 U2) (ces_sor_bw ? U1 U2).
+
+(* subset less or equal (inclusion) ***************************************)
+
+definition sle: ∀D. Subset D → Subset D → Prop ≝
+ λD. λU1,U2:Subset D. \iforall d. U1 d → U2 d.
+
+(* subset overlap *********************************************************)
+
+definition sover: ∀D. Subset D → Subset D → Prop ≝
+ λD. λU1,U2:Subset D. \iexists d. U1 d ∧ U2 d.
+
+(* the class of the subsets of a domain ***********************************)
+
+definition power: Domain → Class ≝
+ λD. mk_Class (Subset D) (true_f ?) (sle ?) (true_fw ? ?) (true_bw ? ?).
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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 *)
+(* *)
+(**************************************************************************)
+
+(* Project started Wed Oct 12, 2005 ***************************************)
+(* Project taken over by "formal_topology" and restarted Mon Apr 6, 2009 **)
+
+include "logic/connectives.ma".
+include "datatypes/constructors.ma".
+include "datatypes/bool.ma".
+
+(* notations **************************************************************)
+
+notation < "hvbox(\iforall ident i opt (: ty) break . p)"
+ right associative with precedence 20
+for @{ 'iforall ${ default
+ @{λ ${ident i}: $ty. $p}
+ @{λ ${ident i}. $p}
+}}.
+
+notation > "\iforall list1 ident x sep , opt (: T). term 19 Px"
+ with precedence 20
+for ${ default
+ @{ ${ fold right @{$Px} rec acc @{'iforall (λ ${ident x} :$T . $acc)} } }
+ @{ ${ fold right @{$Px} rec acc @{'iforall (λ ${ident x} . $acc)} } }
+}.
+
+notation < "hvbox(\iexists ident i opt (: ty) break . p)"
+ right associative with precedence 20
+for @{ 'iexists ${ default
+ @{λ ${ident i}: $ty. $p}
+ @{λ ${ident i}. $p}
+}}.
+
+notation > "\iexists list1 ident x sep , opt (: T). term 19 Px"
+ with precedence 20
+for ${ default
+ @{ ${ fold right @{$Px} rec acc @{'iexists (λ ${ident x}: $T. $acc)} } }
+ @{ ${ fold right @{$Px} rec acc @{'iexists (λ ${ident x}. $acc)} } }
+}.
(* Project started Wed Oct 12, 2005 ***************************************)
(* Project taken over by "formal_topology" and restarted Mon Apr 6, 2009 **)
+(* Project taken over by "lambdadelta" and restarted Sun Sept 20, 2015 ****)
-include "logic/connectives.ma".
-include "datatypes/constructors.ma".
-include "datatypes/bool.ma".
-
-(* notations **************************************************************)
-
-notation < "hvbox(\iforall ident i opt (: ty) break . p)"
- right associative with precedence 20
-for @{ 'iforall ${ default
- @{λ ${ident i}: $ty. $p}
- @{λ ${ident i}. $p}
-}}.
-
-notation > "\iforall list1 ident x sep , opt (: T). term 19 Px"
- with precedence 20
-for ${ default
- @{ ${ fold right @{$Px} rec acc @{'iforall (λ ${ident x} :$T . $acc)} } }
- @{ ${ fold right @{$Px} rec acc @{'iforall (λ ${ident x} . $acc)} } }
-}.
-
-notation < "hvbox(\iexists ident i opt (: ty) break . p)"
- right associative with precedence 20
-for @{ 'iexists ${ default
- @{λ ${ident i}: $ty. $p}
- @{λ ${ident i}. $p}
-}}.
-
-notation > "\iexists list1 ident x sep , opt (: T). term 19 Px"
- with precedence 20
-for ${ default
- @{ ${ fold right @{$Px} rec acc @{'iexists (λ ${ident x}: $T. $acc)} } }
- @{ ${ fold right @{$Px} rec acc @{'iexists (λ ${ident x}. $acc)} } }
-}.
+include "basics/logic.ma".
projects / helm.git / commitdiff