From: Ferruccio Guidi Date: Mon, 6 Apr 2009 14:20:51 +0000 (+0000) Subject: - external quantification removed (will be reintroduced when needed) X-Git-Tag: make_still_working~4118 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=bf8fe5331d6e6d2dfe955efa54b1ffdafaae8429;p=helm.git - external quantification removed (will be reintroduced when needed) - preamble added (was missing) --- diff --git a/helm/software/matita/contribs/limits/Class/defs.ma b/helm/software/matita/contribs/limits/Class/defs.ma index a0b07ccee..bbb071b50 100644 --- a/helm/software/matita/contribs/limits/Class/defs.ma +++ b/helm/software/matita/contribs/limits/Class/defs.ma @@ -14,7 +14,7 @@ include "preamble.ma". -(* ACZEL CATEGORIES: +(* ACZEL CATEGORIES - 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 @@ -42,41 +42,4 @@ inductive ceq (C:Class): class C → class C → Prop ≝ | ceq_trans: ∀c1,c,c2. cin ? c1 → ces ? c1 c → ceq ? c c2 → ceq ? c1 c2 | ceq_conf : ∀c1,c,c2. cin ? c1 → ces ? c c1 → ceq ? c c2 → ceq ? c1 c2 . -(* -(* external universal quantification *) -inductive call (C:Class) (P:C \to Prop) : Prop ≝ - | call_intro: (\forall c. cin ? c \to P c) \to call C P. -inductive call2 (C1,C2:Class) (P:C1 \to C2 \to Prop) : Prop \def - | call2_intro: - (\forall c1,c2. cin ? c1 \to cin ? c2 \to P c1 c2) \to call2 C1 C2 P. -*) -(* notations **************************************************************) -(* -(*CSC: the URI must disappear: there is a bug now *) -interpretation "external for all" 'xforall \eta.x = - (cic:/matita/limits/Class/defs/call.ind#xpointer(1/1) _ x). - -notation < "hvbox(\xforall ident i opt (: ty) break . p)" - right associative with precedence 20 -for @{ 'xforall ${default - @{\lambda ${ident i} : $ty. $p} - @{\lambda ${ident i} . $p}}}. - -notation > "\forall list1 ident x sep , opt (: T). term 19 Px" - with precedence 20 - for ${ default - @{ ${ fold right @{$Px} rec acc @{'xforall (λ${ident x}:$T.$acc)} } } - @{ ${ fold right @{$Px} rec acc @{'xforall (λ${ident x}.$acc)} } } - }. - -(*CSC: the URI must disappear: there is a bug now *) -interpretation "external for all 2" 'xforall2 \eta.x \eta.y = - (cic:/matita/limits/Class/defs/call2.ind#xpointer(1/1) _ _ x y). - -notation > "hvbox(\xforall ident i1 opt (: ty1) ident i2 opt (: ty2) break . p)" - with precedence 20 -for @{ 'xforall2 ${default - @{\lambda ${ident i1} : $ty1. \lambda ${ident i2} : $ty2. $p} - @{\lambda ${ident i1}, ${ident i2}. $p}}}. -*) diff --git a/helm/software/matita/contribs/limits/Domain/defs.ma b/helm/software/matita/contribs/limits/Domain/defs.ma index 2250e811c..f73f1aca0 100644 --- a/helm/software/matita/contribs/limits/Domain/defs.ma +++ b/helm/software/matita/contribs/limits/Domain/defs.ma @@ -25,44 +25,14 @@ record Domain: Type ≝ { (* internal universal quantification *) inductive dall (D:Domain) (P:D → Prop): Prop ≝ - | dall_intro: (∀d. cin ? d → P d) → dall D P. + | 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. - -(* notations **************************************************************) - -(*CSC: the URI must disappear: there is a bug now *) -interpretation "internal for all" 'iforall η.x = - (cic:/matita/limits/Domain/defs/dall.ind#xpointer(1/1) _ x). + | dex_intro: ∀d. cin D d → P d → dex D P +. -notation < "hvbox(\iforall ident i opt (: ty) break . p)" - right associative with precedence 20 -for @{ 'iforall ${default - @{\lambda ${ident i} : $ty. $p} - @{\lambda ${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)} } } -}. - -(*CSC: the URI must disappear: there is a bug now *) -interpretation "internal exists" 'iexists η.x = - (cic:/matita/limits/Domain/defs/dex.ind#xpointer(1/1) _ x). - -notation < "hvbox(\iexists ident i opt (: ty) break . p)" - right associative with precedence 20 -for @{ 'iexists ${default - @{\lambda ${ident i} : $ty. $p} - @{\lambda ${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)} } } -}. +interpretation "internal exists" 'iexists η.x = (dex _ x). diff --git a/helm/software/matita/contribs/limits/Subset/defs.ma b/helm/software/matita/contribs/limits/Subset/defs.ma index ed5c8a47e..6dbab4b39 100644 --- a/helm/software/matita/contribs/limits/Subset/defs.ma +++ b/helm/software/matita/contribs/limits/Subset/defs.ma @@ -28,6 +28,8 @@ definition sin : ∀D. Subset D → D → Prop ≝ (* subset top (full subset) *) definition stop ≝ λD:Domain. true_f D. +coercion stop. + (* subset bottom (empty subset) *) definition sbot ≝ λD:Domain. false_f D. @@ -47,17 +49,10 @@ definition sle: ∀D. Subset D → Subset D → Prop ≝ definition sover: ∀D. Subset D → Subset D → Prop ≝ λD,U1,U2. \iexists d. U1 d ∧ U2 d. -(* coercions **************************************************************) - -(* -(* the class of the subsets of a domain (not an implicit coercion) *) -definition class_of_subsets_of \def - \lambda D. mk_Class (Subset D) (true_f ?) (sle ?). -*) +(* the class of the subsets of a domain *) +definition subsets_of_domain ≝ + λD. mk_Class (Subset D) (true_f ?) (sle ?). -(* the domain built upon a subset (not an implicit coercion) *) -definition domain_of_subset: ∀D. Subset D \to Domain ≝ +(* the domain built upon a subset *) +definition domain_of_subset: ∀D. Subset D → Domain ≝ λD:Domain. λU. mk_Domain (mk_Class D (sin D U) (ces D)). - -(* the full subset of a domain *) -coercion stop. diff --git a/helm/software/matita/contribs/limits/preamble.ma b/helm/software/matita/contribs/limits/preamble.ma new file mode 100644 index 000000000..80713e416 --- /dev/null +++ b/helm/software/matita/contribs/limits/preamble.ma @@ -0,0 +1,50 @@ +(**************************************************************************) +(* ___ *) +(* ||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)} } } +}.