1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/PREDICATIVE-TOPOLOGY/domain_defs".
17 include "class_defs.ma".
19 (* QUANTIFICATION DOMAINS
20 - These are the categories on which we allow quantification
21 - We set up single quantifiers, parametric on the domain, so they
22 already have the properties that usually are axiomatized inside the
23 domain structure. This makes domains easier to use
26 record Domain: Type \def {
30 (* internal universal quantification *)
31 inductive dall (D:Domain) (P:D \to Prop) : Prop \def
32 | dall_intro: (\forall d:D. cin D d \to P d) \to dall D P.
34 (* internal existential quantification *)
35 inductive dex (D:Domain) (P:D \to Prop) : Prop \def
36 | dex_intro: \forall d:D. cin D d \land P d \to dex D P.
38 (* notations **************************************************************)
40 (*CSC: the URI must disappear: there is a bug now *)
41 interpretation "internal for all" 'iforall \eta.x =
42 (cic:/matita/PREDICATIVE-TOPOLOGY/domain_defs/dall.ind#xpointer(1/1) _ x).
44 notation > "hvbox(\iforall ident i opt (: ty) break . p)"
45 right associative with precedence 20
46 for @{ 'iforall ${default
47 @{\lambda ${ident i} : $ty. $p)}
48 @{\lambda ${ident i} . $p}}}.
50 (*CSC: the URI must disappear: there is a bug now *)
51 interpretation "internal exists" 'dexists \eta.x =
52 (cic:/matita/PREDICATIVE-TOPOLOGY/domain_defs/dex.ind#xpointer(1/1) _ x).
54 notation > "hvbox(\iexists ident i opt (: ty) break . p)"
55 right associative with precedence 20
56 for @{ 'dexists ${default
57 @{\lambda ${ident i} : $ty. $p)}
58 @{\lambda ${ident i} . $p}}}.