]> matita.cs.unibo.it Git - helm.git/commitdiff
...
authorEnrico Tassi <enrico.tassi@inria.fr>
Mon, 21 Sep 2009 19:56:38 +0000 (19:56 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Mon, 21 Sep 2009 19:56:38 +0000 (19:56 +0000)
helm/software/matita/nlibrary/topology/igft.ma

index 3e9e359d5f01109f9743e7e0f0f7d27f1c303ee3..9d61e0af603680e0ddbbc5eaf8204b549a5c35f4 100644 (file)
@@ -130,6 +130,7 @@ notation > "š term 90 a term 90 i term 90 j" non associative with precedence
 
 interpretation "D" 'D a i = (nD ? a i).
 interpretation "d" 'd a i j = (nd ? a i j).
+interpretation "new I" 'I a = (nI ? a).
 
 ndefinition image ā‰ Ī»A:nAx.Ī»a:A.Ī»i. { x | āˆƒj:šƒ a i. x = š a i j }.
 
@@ -138,6 +139,7 @@ notation "šˆš¦  [š \sub ( āØa,\emsp iā© )]" non associative with preced
 
 interpretation "image" 'Im a i = (image ? a i).
 
+(*
 ndefinition Ax_of_nAx : nAx ā†’ Ax.
 #A; @ A (nI ?); #a; #i; napply (šˆš¦ [š a i]);
 nqed.
@@ -153,16 +155,102 @@ ndefinition nAx_of_Ax : Ax ā†’ nAx.
 ##| #a; #i; *; #x; #_; napply x;
 ##]
 nqed.
+*)
 
-ninductive ord (A : nAx) : Type[0] ā‰ 
- | oO : ord A
- | oS : ord A ā†’ ord A
- | oL : āˆ€a:A.āˆ€i.āˆ€f:šƒ a i ā†’ ord A. ord A.
+ninductive Ord (A : nAx) : Type[0] ā‰ 
+ | oO : Ord A
+ | oS : Ord A ā†’ Ord A
+ | oL : āˆ€a:A.āˆ€i.āˆ€f:šƒ a i ā†’ Ord A. Ord A.
 
-nlet rec famU (A : nAx) (U : Ī©^A) (x : ord A) on x : Ī©^A ā‰ 
+notation "Ī› term 90 f" non associative with precedence 50 for @{ 'oL $f }.
+notation "x+1" non associative with precedence 50 for @{'oS $x }.
+
+interpretation "ordinals Lambda" 'oL f = (oL ? ? ? f).
+interpretation "ordinals Succ" 'oS x = (oS ? x).
+
+nlet rec famU (A : nAx) (U : Ī©^A) (x : Ord A) on x : Ī©^A ā‰ 
   match x with
   [ oO ā‡’ U
-  | oS y ā‡’ let Un ā‰ famU A U y in Un āˆŖ { x | āˆƒi.āˆ€j:šƒ x i.š x i j āˆˆ Un} 
+  | oS y ā‡’ let Un ā‰ famU A U y in Un āˆŖ { x | āˆƒi.šˆš¦[š x i] āŠ† Un} 
   | oL a i f ā‡’ { x | āˆƒj.x āˆˆ famU A U (f j) } ].
   
-ndefinition ord_coverage ā‰ Ī»A,U.{ y | āˆƒx:ord A. y āˆˆ famU ? U x }.   
+naxiom XXX : False.  
+  
+ndefinition qp_famU : āˆ€A:nAx.āˆ€U:qpowerclass A.āˆ€x:Ord A.qpowerclass A ā‰ 
+  Ī»A,U,x.?. 
+@ (famU ? (pc ? U) x); nelim x;
+##[ #a; #b; #E; nnormalize; @; #H; ##[ napply (. E^-1ā€”#); napply H; ##| napply (. Eā€”#); napply H; ##]  
+##| #o; #IH; #a; #b; #E; @; nnormalize; *; #H;
+    ##[##1,3: @1; nlapply (IH ā€¦ E); *; #G; #G'; 
+              ##[ napply G | napply G'] nassumption;
+    ##|##2,4: @2; ncases H; #i_a; #H_ia; @;
+ nelim XXX; ##]
+##| nelim XXX; 
+##]
+nqed.
+
+unification hint 0 ā‰” 
+  A,U,x; UU ā‰Ÿ (pc ? U) āŠ¢ pc ? (qp_famU A U x) ā‰” famU A UU x.
+
+notation < "term 90 U \sub (term 90 x)" non associative with precedence 50 for @{ 'famU $U $x }.
+notation > "U āŽ½ term 90 x" non associative with precedence 50 for @{ 'famU $U $x }.
+
+interpretation "famU" 'famU U x = (famU ? U x).
+  
+ndefinition ord_coverage : āˆ€A:nAx.āˆ€U:Ī©^A.Ī©^A ā‰ Ī»A,U.{ y | āˆƒx:Ord A. y āˆˆ famU ? U x }.
+
+ndefinition ord_cover_set ā‰ Ī»c:āˆ€A:nAx.Ī©^A ā†’ Ī©^A.Ī»A,C,U.
+  āˆ€y.y āˆˆ C ā†’ y āˆˆ c A U.
+
+interpretation "coverage new cover" 'coverage U = (ord_coverage ? U).
+interpretation "new covers set" 'covers a U = (ord_cover_set ord_coverage ? a U).
+interpretation "new covers" 'covers a U = (mem ? (ord_coverage ? U) a).
+
+ntheorem new_coverage_reflexive:
+  āˆ€A:nAx.āˆ€U:Ī©^A.āˆ€a. a āˆˆ U ā†’ a ā—ƒ U.
+#A; #U; #a; #H; @ (oO A); napply H;
+nqed.
+
+nlemma ord_subset:
+  āˆ€A:nAx.āˆ€a:A.āˆ€i,f,U.āˆ€j:šƒ a i.UāŽ½(f j) āŠ† UāŽ½(Ī› f).
+#A; #a; #i; #f; #U; #j; #b; #bUf; @ j; nassumption;
+nqed.
+
+naxiom AC : āˆ€A,a,i,U.(āˆ€j:šƒ a i.āˆƒx:Ord A.š a i j āˆˆ UāŽ½x) ā†’ (Ī£f.āˆ€j:šƒ a i.š a i j āˆˆ UāŽ½(f j)).
+
+naxiom setoidification :
+  āˆ€A:nAx.āˆ€a,b:A.āˆ€U.a=b ā†’ b āˆˆ U ā†’ a āˆˆ U.
+
+alias symbol "covers" = "new covers set".
+alias symbol "covers" = "new covers".
+alias symbol "covers" = "new covers set".
+alias symbol "covers" = "new covers".
+alias symbol "covers" = "new covers set".
+alias symbol "covers" = "new covers".
+ntheorem new_coverage_infinity:
+  āˆ€A:nAx.āˆ€U:Ī©^A.āˆ€a:A. (āˆƒi:šˆ a. šˆš¦[š a i] ā—ƒ U) ā†’ a ā—ƒ U.
+#A; #U; #a; *; #i; #H; nnormalize in H;
+ncut (āˆ€y:šƒ a i.āˆƒx:Ord A.š a i y āˆˆ UāŽ½x); ##[
+  #y; napply H; @ y; napply #; ##] #H'; 
+ncases (AC ā€¦ H'); #f; #Hf;
+ncut (āˆ€j.š a i j āˆˆ UāŽ½(Ī› f));
+  ##[ #j; napply (ord_subset ā€¦ f ā€¦ (Hf j));##] #Hf';
+@ ((Ī› f)+1); @2; nwhd; @i; #x; *; #d; #Hd; napply (setoidification ā€¦ Hd); napply Hf';
+nqed.
+
+(* move away *)
+nlemma subseteq_union: āˆ€A.āˆ€U,V,W:Ī©^A.U āŠ† W ā†’ V āŠ† W ā†’ U āˆŖ V āŠ† W.
+#A; #U; #V; #W; #H; #H1; #x; *; #Hx; ##[ napply H; ##| napply H1; ##] nassumption;
+nqed. 
+
+nlemma new_coverage_min :  
+  āˆ€A:nAx.āˆ€U:qpowerclass A.āˆ€V.U āŠ† V ā†’ (āˆ€a:A.āˆ€i.šˆš¦[š a i] āŠ† V ā†’ a āˆˆ V) ā†’ ā—ƒ(pc ? U) āŠ† V.
+#A; #U; #V; #HUV; #Im;  #b; *; #o; ngeneralize in match b; nchange with ((pc ? U)āŽ½o āŠ† V);
+nelim o;
+##[ #b; #bU0; napply HUV; napply bU0;
+##| #p; #IH; napply subseteq_union; ##[ nassumption; ##]
+    #x; *; #i; #H; napply (Im ? i); napply (subseteq_trans ā€¦ IH); napply H;
+##| #a; #i; #f; #IH; #x; *; #d; napply IH; ##]
+nqed.
\ No newline at end of file