update in basic_2

[helm.git] / helm / software / matita / contribs / CoRN-Decl / reals / CauchySeq.ma

diff --git a/helm/software/matita/contribs/CoRN-Decl/reals/CauchySeq.ma b/helm/software/matita/contribs/CoRN-Decl/reals/CauchySeq.ma
index 56b09f62fe559a6461571014ecc4e790206d34e6..4bc6c7aa18e1185dc7bf81a0ffc891253c5e5c09 100644 (file)
--- a/helm/software/matita/contribs/CoRN-Decl/reals/CauchySeq.ma
+++ b/helm/software/matita/contribs/CoRN-Decl/reals/CauchySeq.ma
@@ -16,6 +16,8 @@
 
 set "baseuri" "cic:/matita/CoRN-Decl/reals/CauchySeq".
 
+include "CoRN.ma".
+
 (* $Id: CauchySeq.v,v 1.8 2004/04/23 10:01:04 lcf Exp $ *)
 
 (*#* printing IR %\ensuremath{\mathbb R}% *)
@@ -28,9 +30,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/reals/CauchySeq".
 
 (*#* printing AbsIR %\ensuremath{|\cdot|_{\mathbb R}}% *)
 
-(* INCLUDE
-CReals
-*)
+include "reals/CReals.ma".
 
 (*#* *Real Number Structures
 %\begin{convention}% Let [IR] be a structure for real numbers.
@@ -43,44 +43,62 @@ Definition IR : CReals := Concrete_R.
 Opaque IR.
 *)
 
-inline cic:/CoRN/reals/CauchySeq/IR.var.
+alias id "IR" = "cic:/CoRN/reals/CauchySeq/IR.var".
+
+(* NOTATION
+Notation PartIR := (PartFunct IR).
+*)
+
+(* NOTATION
+Notation ProjIR1 := (prj1 IR _ _ _).
+*)
 
-(* INCLUDE
-Transparent_algebra
+(* NOTATION
+Notation ProjIR2 := (prj2 IR _ _ _).
 *)
 
+include "tactics/Transparent_algebra.ma".
+
 (* begin hide *)
 
+(* NOTATION
+Notation ZeroR := (Zero:IR).
+*)
+
+(* NOTATION
+Notation OneR := (One:IR).
+*)
+
 (* end hide *)
 
 (* UNEXPORTED
-Section CReals_axioms.
+Section CReals_axioms
 *)
 
 (*#* ** [CReals] axioms *)
 
-inline cic:/CoRN/reals/CauchySeq/CReals_is_CReals.con.
+inline "cic:/CoRN/reals/CauchySeq/CReals_is_CReals.con".
 
 (*#* First properties which follow trivially from the axioms.  *)
 
-inline cic:/CoRN/reals/CauchySeq/Lim_Cauchy.con.
+inline "cic:/CoRN/reals/CauchySeq/Lim_Cauchy.con".
 
-inline cic:/CoRN/reals/CauchySeq/Archimedes.con.
+inline "cic:/CoRN/reals/CauchySeq/Archimedes.con".
 
-inline cic:/CoRN/reals/CauchySeq/Archimedes'.con.
+inline "cic:/CoRN/reals/CauchySeq/Archimedes'.con".
 
 (*#* A stronger version, which often comes in useful.  *)
 
-inline cic:/CoRN/reals/CauchySeq/str_Archimedes.con.
+inline "cic:/CoRN/reals/CauchySeq/str_Archimedes.con".
 
-inline cic:/CoRN/reals/CauchySeq/CauchySeqR.con.
+inline "cic:/CoRN/reals/CauchySeq/CauchySeqR.con".
 
 (* UNEXPORTED
-End CReals_axioms.
+End CReals_axioms
 *)
 
 (* UNEXPORTED
-Section Cauchy_Defs.
+Section Cauchy_Defs
 *)
 
 (*#* ** Cauchy sequences
@@ -136,124 +154,124 @@ and [[<=]] being a negative statement, this makes proofs
 sometimes easier and program extraction much more efficient.
 *)
 
-inline cic:/CoRN/reals/CauchySeq/Cauchy_prop1.con.
+inline "cic:/CoRN/reals/CauchySeq/Cauchy_prop1.con".
 
-inline cic:/CoRN/reals/CauchySeq/Cauchy_Lim_prop2.con.
+inline "cic:/CoRN/reals/CauchySeq/Cauchy_Lim_prop2.con".
 
-inline cic:/CoRN/reals/CauchySeq/Cauchy_prop2.con.
+inline "cic:/CoRN/reals/CauchySeq/Cauchy_prop2.con".
 
-inline cic:/CoRN/reals/CauchySeq/Cauchy_Lim_prop3.con.
+inline "cic:/CoRN/reals/CauchySeq/Cauchy_Lim_prop3.con".
 
-inline cic:/CoRN/reals/CauchySeq/Cauchy_prop3.con.
+inline "cic:/CoRN/reals/CauchySeq/Cauchy_prop3.con".
 
-inline cic:/CoRN/reals/CauchySeq/Cauchy_Lim_prop4.con.
+inline "cic:/CoRN/reals/CauchySeq/Cauchy_Lim_prop4.con".
 
-inline cic:/CoRN/reals/CauchySeq/Cauchy_prop4.con.
+inline "cic:/CoRN/reals/CauchySeq/Cauchy_prop4.con".
 
 (* UNEXPORTED
-End Cauchy_Defs.
+End Cauchy_Defs
 *)
 
 (* UNEXPORTED
-Section Inequalities.
+Section Inequalities
 *)
 
 (*#* *** Inequalities of Limits
 
 The next lemma is equal to lemma [Lim_Cauchy].  *)
 
-inline cic:/CoRN/reals/CauchySeq/Cauchy_complete.con.
+inline "cic:/CoRN/reals/CauchySeq/Cauchy_complete.con".
 
-inline cic:/CoRN/reals/CauchySeq/less_Lim_so_less_seq.con.
+inline "cic:/CoRN/reals/CauchySeq/less_Lim_so_less_seq.con".
 
-inline cic:/CoRN/reals/CauchySeq/Lim_less_so_seq_less.con.
+inline "cic:/CoRN/reals/CauchySeq/Lim_less_so_seq_less.con".
 
-inline cic:/CoRN/reals/CauchySeq/Lim_less_Lim_so_seq_less_seq.con.
+inline "cic:/CoRN/reals/CauchySeq/Lim_less_Lim_so_seq_less_seq.con".
 
 (*#* The next lemma follows from [less_Lim_so_less_seq] with [y := (y[+] (Lim seq)) [/]TwoNZ].  *)
 
-inline cic:/CoRN/reals/CauchySeq/less_Lim_so.con.
+inline "cic:/CoRN/reals/CauchySeq/less_Lim_so.con".
 
-inline cic:/CoRN/reals/CauchySeq/Lim_less_so.con.
+inline "cic:/CoRN/reals/CauchySeq/Lim_less_so.con".
 
-inline cic:/CoRN/reals/CauchySeq/leEq_seq_so_leEq_Lim.con.
+inline "cic:/CoRN/reals/CauchySeq/leEq_seq_so_leEq_Lim.con".
 
-inline cic:/CoRN/reals/CauchySeq/str_leEq_seq_so_leEq_Lim.con.
+inline "cic:/CoRN/reals/CauchySeq/str_leEq_seq_so_leEq_Lim.con".
 
-inline cic:/CoRN/reals/CauchySeq/Lim_leEq_Lim.con.
+inline "cic:/CoRN/reals/CauchySeq/Lim_leEq_Lim.con".
 
-inline cic:/CoRN/reals/CauchySeq/seq_leEq_so_Lim_leEq.con.
+inline "cic:/CoRN/reals/CauchySeq/seq_leEq_so_Lim_leEq.con".
 
-inline cic:/CoRN/reals/CauchySeq/str_seq_leEq_so_Lim_leEq.con.
+inline "cic:/CoRN/reals/CauchySeq/str_seq_leEq_so_Lim_leEq.con".
 
-inline cic:/CoRN/reals/CauchySeq/Limits_unique.con.
+inline "cic:/CoRN/reals/CauchySeq/Limits_unique.con".
 
-inline cic:/CoRN/reals/CauchySeq/Lim_wd.con.
+inline "cic:/CoRN/reals/CauchySeq/Lim_wd.con".
 
-inline cic:/CoRN/reals/CauchySeq/Lim_strext.con.
+inline "cic:/CoRN/reals/CauchySeq/Lim_strext.con".
 
-inline cic:/CoRN/reals/CauchySeq/Lim_ap_imp_seq_ap.con.
+inline "cic:/CoRN/reals/CauchySeq/Lim_ap_imp_seq_ap.con".
 
-inline cic:/CoRN/reals/CauchySeq/Lim_ap_imp_seq_ap'.con.
+inline "cic:/CoRN/reals/CauchySeq/Lim_ap_imp_seq_ap'.con".
 
 (* UNEXPORTED
-End Inequalities.
+End Inequalities
 *)
 
 (* UNEXPORTED
-Section Equiv_Cauchy.
+Section Equiv_Cauchy
 *)
 
 (*#* *** Equivalence of formulations of Cauchy *)
 
-inline cic:/CoRN/reals/CauchySeq/Cauchy_prop1_prop.con.
+inline "cic:/CoRN/reals/CauchySeq/Cauchy_prop1_prop.con".
 
-inline cic:/CoRN/reals/CauchySeq/Cauchy_prop2_prop.con.
+inline "cic:/CoRN/reals/CauchySeq/Cauchy_prop2_prop.con".
 
-inline cic:/CoRN/reals/CauchySeq/Cauchy_Lim_prop3_prop2.con.
+inline "cic:/CoRN/reals/CauchySeq/Cauchy_Lim_prop3_prop2.con".
 
-inline cic:/CoRN/reals/CauchySeq/Cauchy_prop3_prop2.con.
+inline "cic:/CoRN/reals/CauchySeq/Cauchy_prop3_prop2.con".
 
-inline cic:/CoRN/reals/CauchySeq/Cauchy_prop3_prop.con.
+inline "cic:/CoRN/reals/CauchySeq/Cauchy_prop3_prop.con".
 
-inline cic:/CoRN/reals/CauchySeq/Build_CauchySeq1.con.
+inline "cic:/CoRN/reals/CauchySeq/Build_CauchySeq1.con".
 
-inline cic:/CoRN/reals/CauchySeq/Cauchy_Lim_prop4_prop3.con.
+inline "cic:/CoRN/reals/CauchySeq/Cauchy_Lim_prop4_prop3.con".
 
-inline cic:/CoRN/reals/CauchySeq/Cauchy_Lim_prop4_prop2.con.
+inline "cic:/CoRN/reals/CauchySeq/Cauchy_Lim_prop4_prop2.con".
 
-inline cic:/CoRN/reals/CauchySeq/Cauchy_prop4_prop3.con.
+inline "cic:/CoRN/reals/CauchySeq/Cauchy_prop4_prop3.con".
 
-inline cic:/CoRN/reals/CauchySeq/Cauchy_prop4_prop.con.
+inline "cic:/CoRN/reals/CauchySeq/Cauchy_prop4_prop.con".
 
-inline cic:/CoRN/reals/CauchySeq/Build_CauchySeq4.con.
+inline "cic:/CoRN/reals/CauchySeq/Build_CauchySeq4.con".
 
-inline cic:/CoRN/reals/CauchySeq/Build_CauchySeq4_y.con.
+inline "cic:/CoRN/reals/CauchySeq/Build_CauchySeq4_y.con".
 
-inline cic:/CoRN/reals/CauchySeq/Lim_CauchySeq4.con.
+inline "cic:/CoRN/reals/CauchySeq/Lim_CauchySeq4.con".
 
-inline cic:/CoRN/reals/CauchySeq/Build_CauchySeq2.con.
+inline "cic:/CoRN/reals/CauchySeq/Build_CauchySeq2.con".
 
-inline cic:/CoRN/reals/CauchySeq/Build_CauchySeq2_y.con.
+inline "cic:/CoRN/reals/CauchySeq/Build_CauchySeq2_y.con".
 
-inline cic:/CoRN/reals/CauchySeq/Lim_CauchySeq2.con.
+inline "cic:/CoRN/reals/CauchySeq/Lim_CauchySeq2.con".
 
 (*#* Well definedness. *)
 
-inline cic:/CoRN/reals/CauchySeq/Cauchy_prop_wd.con.
+inline "cic:/CoRN/reals/CauchySeq/Cauchy_prop_wd.con".
 
-inline cic:/CoRN/reals/CauchySeq/Cauchy_Lim_prop2_wd.con.
+inline "cic:/CoRN/reals/CauchySeq/Cauchy_Lim_prop2_wd.con".
 
-inline cic:/CoRN/reals/CauchySeq/Lim_wd'.con.
+inline "cic:/CoRN/reals/CauchySeq/Lim_wd'.con".
 
-inline cic:/CoRN/reals/CauchySeq/Lim_unique.con.
+inline "cic:/CoRN/reals/CauchySeq/Lim_unique.con".
 
 (* UNEXPORTED
-End Equiv_Cauchy.
+End Equiv_Cauchy
 *)
 
 (* UNEXPORTED
-Section Cauchy_props.
+Section Cauchy_props
 *)
 
 (*#* *** Properties of Cauchy sequences
@@ -263,35 +281,35 @@ Some of these lemmas are now obsolete, because they were reproved for arbitrary
 We begin by defining the constant sequence and proving that it is Cauchy with the expected limit.
 *)
 
-inline cic:/CoRN/reals/CauchySeq/Cauchy_const.con.
+inline "cic:/CoRN/reals/CauchySeq/Cauchy_const.con".
 
-inline cic:/CoRN/reals/CauchySeq/Lim_const.con.
+inline "cic:/CoRN/reals/CauchySeq/Lim_const.con".
 
-inline cic:/CoRN/reals/CauchySeq/Cauchy_Lim_plus.con.
+inline "cic:/CoRN/reals/CauchySeq/Cauchy_Lim_plus.con".
 
-inline cic:/CoRN/reals/CauchySeq/Cauchy_plus.con.
+inline "cic:/CoRN/reals/CauchySeq/Cauchy_plus.con".
 
-inline cic:/CoRN/reals/CauchySeq/Lim_plus.con.
+inline "cic:/CoRN/reals/CauchySeq/Lim_plus.con".
 
-inline cic:/CoRN/reals/CauchySeq/Cauchy_Lim_inv.con.
+inline "cic:/CoRN/reals/CauchySeq/Cauchy_Lim_inv.con".
 
-inline cic:/CoRN/reals/CauchySeq/Cauchy_inv.con.
+inline "cic:/CoRN/reals/CauchySeq/Cauchy_inv.con".
 
-inline cic:/CoRN/reals/CauchySeq/Lim_inv.con.
+inline "cic:/CoRN/reals/CauchySeq/Lim_inv.con".
 
-inline cic:/CoRN/reals/CauchySeq/Cauchy_Lim_minus.con.
+inline "cic:/CoRN/reals/CauchySeq/Cauchy_Lim_minus.con".
 
-inline cic:/CoRN/reals/CauchySeq/Cauchy_minus.con.
+inline "cic:/CoRN/reals/CauchySeq/Cauchy_minus.con".
 
-inline cic:/CoRN/reals/CauchySeq/Lim_minus.con.
+inline "cic:/CoRN/reals/CauchySeq/Lim_minus.con".
 
-inline cic:/CoRN/reals/CauchySeq/Cauchy_Lim_mult.con.
+inline "cic:/CoRN/reals/CauchySeq/Cauchy_Lim_mult.con".
 
-inline cic:/CoRN/reals/CauchySeq/Cauchy_mult.con.
+inline "cic:/CoRN/reals/CauchySeq/Cauchy_mult.con".
 
-inline cic:/CoRN/reals/CauchySeq/Lim_mult.con.
+inline "cic:/CoRN/reals/CauchySeq/Lim_mult.con".
 
 (* UNEXPORTED
-End Cauchy_props.
+End Cauchy_props
 *)