helm/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 set "baseuri" "cic:/matita/PREDICATIVE-TOPOLOGY/domain_defs".
  16
  17 include "class_defs.ma".
  18
  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
  24 *)
  25
  26 record Domain: Type \def {
  27    qd:> Class
  28 }.
  29
  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.
  33
  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.
  37
  38 (* notations **************************************************************)
  39
  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).
  43
  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}}}.
  49
  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).
  53
  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}}}.