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