From c5a4db6c1020488d0792cee00dcf395a0ce54735 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 20 Nov 2008 16:00:06 +0000 Subject: [PATCH] dama almost ok --- .../matita/library/dama/bishop_set.ma | 4 +- .../matita/library/dama/bishop_set_rewrite.ma | 2 +- helm/software/matita/library/dama/lebesgue.ma | 5 +-- .../dama/models/discrete_uniformity.ma | 4 +- .../models/increasing_supremum_stabilizes.ma | 6 +-- .../library/dama/models/nat_lebesgue.ma | 4 +- .../dama/models/nat_order_continuous.ma | 4 +- .../dama/models/nat_ordered_uniform.ma | 6 +-- .../matita/library/dama/models/nat_uniform.ma | 6 +-- .../matita/library/dama/nat_ordered_set.ma | 2 +- .../matita/library/dama/ordered_uniform.ma | 2 +- .../library/dama/property_exhaustivity.ma | 4 +- .../matita/library/dama/property_sigma.ma | 4 +- helm/software/matita/library/dama/sandwich.ma | 2 +- helm/software/matita/library/dama/supremum.ma | 4 +- helm/software/matita/library/dama/uniform.ma | 2 +- helm/software/matita/library/depends | 41 ++++++++++++++----- 17 files changed, 61 insertions(+), 41 deletions(-) diff --git a/helm/software/matita/library/dama/bishop_set.ma b/helm/software/matita/library/dama/bishop_set.ma index d69bb2732..3fa4eda96 100644 --- a/helm/software/matita/library/dama/bishop_set.ma +++ b/helm/software/matita/library/dama/bishop_set.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "ordered_set.ma". +include "dama/ordered_set.ma". (* Definition 2.2, setoid *) record bishop_set: Type ≝ { @@ -86,4 +86,4 @@ notation "s 2 \atop \neq" non associative with precedence 90 notation > "s 'squareB'" non associative with precedence 90 for @{ 'squareB $s }. interpretation "bishop set square" 'squareB x = (square_bishop_set x). -interpretation "bishop set square" 'square_bs x = (square_bishop_set x). \ No newline at end of file +interpretation "bishop set square" 'square_bs x = (square_bishop_set x). diff --git a/helm/software/matita/library/dama/bishop_set_rewrite.ma b/helm/software/matita/library/dama/bishop_set_rewrite.ma index ff063e29a..eaf6f65cf 100644 --- a/helm/software/matita/library/dama/bishop_set_rewrite.ma +++ b/helm/software/matita/library/dama/bishop_set_rewrite.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "bishop_set.ma". +include "dama/bishop_set.ma". coercion eq_sym. diff --git a/helm/software/matita/library/dama/lebesgue.ma b/helm/software/matita/library/dama/lebesgue.ma index f81c5ce46..1b3f5025d 100644 --- a/helm/software/matita/library/dama/lebesgue.ma +++ b/helm/software/matita/library/dama/lebesgue.ma @@ -12,9 +12,8 @@ (* *) (**************************************************************************) -(* manca un pezzo del pullback, se inverto poi non tipa *) -include "sandwich.ma". -include "property_exhaustivity.ma". +include "dama/sandwich.ma". +include "dama/property_exhaustivity.ma". (* NOT DUALIZED *) alias symbol "low" = "lower". diff --git a/helm/software/matita/library/dama/models/discrete_uniformity.ma b/helm/software/matita/library/dama/models/discrete_uniformity.ma index 76461f3f4..e3ece7df1 100644 --- a/helm/software/matita/library/dama/models/discrete_uniformity.ma +++ b/helm/software/matita/library/dama/models/discrete_uniformity.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "uniform.ma". -include "bishop_set_rewrite.ma". +include "dama/uniform.ma". +include "dama/bishop_set_rewrite.ma". definition discrete_uniform_space_of_bishop_set:bishop_set → uniform_space. intro C; apply (mk_uniform_space C); diff --git a/helm/software/matita/library/dama/models/increasing_supremum_stabilizes.ma b/helm/software/matita/library/dama/models/increasing_supremum_stabilizes.ma index 58626ff15..4f7a2f847 100644 --- a/helm/software/matita/library/dama/models/increasing_supremum_stabilizes.ma +++ b/helm/software/matita/library/dama/models/increasing_supremum_stabilizes.ma @@ -12,10 +12,10 @@ (* *) (**************************************************************************) -include "models/nat_uniform.ma". -include "supremum.ma". +include "dama/models/nat_uniform.ma". +include "dama/supremum.ma". include "nat/le_arith.ma". -include "russell_support.ma". +include "dama/russell_support.ma". lemma hint1: ∀s.sequence (Type_of_ordered_set (segment_ordered_set nat_ordered_set s)) diff --git a/helm/software/matita/library/dama/models/nat_lebesgue.ma b/helm/software/matita/library/dama/models/nat_lebesgue.ma index d5e65215e..8d563b1e3 100644 --- a/helm/software/matita/library/dama/models/nat_lebesgue.ma +++ b/helm/software/matita/library/dama/models/nat_lebesgue.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "lebesgue.ma". -include "models/nat_order_continuous.ma". +include "dama/lebesgue.ma". +include "dama/models/nat_order_continuous.ma". theorem nat_lebesgue_oc: ∀a:sequence ℕ.∀s:‡ℕ.∀H:∀i:nat.a i ∈ s. diff --git a/helm/software/matita/library/dama/models/nat_order_continuous.ma b/helm/software/matita/library/dama/models/nat_order_continuous.ma index 5f00dc338..3901c8b76 100644 --- a/helm/software/matita/library/dama/models/nat_order_continuous.ma +++ b/helm/software/matita/library/dama/models/nat_order_continuous.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "models/increasing_supremum_stabilizes.ma". -include "models/nat_ordered_uniform.ma". +include "dama/models/increasing_supremum_stabilizes.ma". +include "dama/models/nat_ordered_uniform.ma". lemma nat_us_is_oc: ∀s:‡ℕ.order_continuity (segment_ordered_uniform_space ℕ s). intros 3; split; intros 3; cases H1; cases H2; clear H2 H1; cases H; clear H; diff --git a/helm/software/matita/library/dama/models/nat_ordered_uniform.ma b/helm/software/matita/library/dama/models/nat_ordered_uniform.ma index becbab2fb..cd6ddbf79 100644 --- a/helm/software/matita/library/dama/models/nat_ordered_uniform.ma +++ b/helm/software/matita/library/dama/models/nat_ordered_uniform.ma @@ -12,9 +12,9 @@ (* *) (**************************************************************************) -include "models/nat_uniform.ma". -include "bishop_set_rewrite.ma". -include "ordered_uniform.ma". +include "dama/models/nat_uniform.ma". +include "dama/bishop_set_rewrite.ma". +include "dama/ordered_uniform.ma". definition nat_ordered_uniform_space:ordered_uniform_space. apply (mk_ordered_uniform_space (mk_ordered_uniform_space_ ℕ ℕ (refl_eq ? ℕ))); diff --git a/helm/software/matita/library/dama/models/nat_uniform.ma b/helm/software/matita/library/dama/models/nat_uniform.ma index 0b2d43563..691d15dd8 100644 --- a/helm/software/matita/library/dama/models/nat_uniform.ma +++ b/helm/software/matita/library/dama/models/nat_uniform.ma @@ -12,11 +12,11 @@ (* *) (**************************************************************************) -include "nat_ordered_set.ma". -include "models/discrete_uniformity.ma". +include "dama/nat_ordered_set.ma". +include "dama/models/discrete_uniformity.ma". definition nat_uniform_space: uniform_space. apply (discrete_uniform_space_of_bishop_set ℕ); qed. -interpretation "Uniform space N" 'N = nat_uniform_space. \ No newline at end of file +interpretation "Uniform space N" 'N = nat_uniform_space. diff --git a/helm/software/matita/library/dama/nat_ordered_set.ma b/helm/software/matita/library/dama/nat_ordered_set.ma index 26e2f0d29..a6d1ec184 100644 --- a/helm/software/matita/library/dama/nat_ordered_set.ma +++ b/helm/software/matita/library/dama/nat_ordered_set.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "nat/compare.ma". -include "bishop_set.ma". +include "dama/bishop_set.ma". definition nat_excess : nat → nat → CProp ≝ λn,m. m ordered_set; diff --git a/helm/software/matita/library/dama/property_exhaustivity.ma b/helm/software/matita/library/dama/property_exhaustivity.ma index deddf8804..4dec6442e 100644 --- a/helm/software/matita/library/dama/property_exhaustivity.ma +++ b/helm/software/matita/library/dama/property_exhaustivity.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "ordered_uniform.ma". -include "property_sigma.ma". +include "dama/ordered_uniform.ma". +include "dama/property_sigma.ma". lemma h_segment_upperbound: ∀C:half_ordered_set. diff --git a/helm/software/matita/library/dama/property_sigma.ma b/helm/software/matita/library/dama/property_sigma.ma index 74f03de4c..26ffd59bc 100644 --- a/helm/software/matita/library/dama/property_sigma.ma +++ b/helm/software/matita/library/dama/property_sigma.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "ordered_uniform.ma". -include "russell_support.ma". +include "dama/ordered_uniform.ma". +include "dama/russell_support.ma". (* Definition 3.5 *) alias num (instance 0) = "natural number". diff --git a/helm/software/matita/library/dama/sandwich.ma b/helm/software/matita/library/dama/sandwich.ma index 68bb4453c..f8aabd472 100644 --- a/helm/software/matita/library/dama/sandwich.ma +++ b/helm/software/matita/library/dama/sandwich.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "ordered_uniform.ma". +include "dama/ordered_uniform.ma". lemma le_w_plus: ∀n,m,o.n+m≤o → m ≤ o. intro; elim n; simplify; [assumption] diff --git a/helm/software/matita/library/dama/supremum.ma b/helm/software/matita/library/dama/supremum.ma index 0de61b292..be8495970 100644 --- a/helm/software/matita/library/dama/supremum.ma +++ b/helm/software/matita/library/dama/supremum.ma @@ -15,8 +15,8 @@ include "datatypes/constructors.ma". include "nat/plus.ma". -include "nat_ordered_set.ma". -include "sequence.ma". +include "dama/nat_ordered_set.ma". +include "dama/sequence.ma". (* Definition 2.4 *) definition upper_bound ≝ diff --git a/helm/software/matita/library/dama/uniform.ma b/helm/software/matita/library/dama/uniform.ma index 759037124..072849bd4 100644 --- a/helm/software/matita/library/dama/uniform.ma +++ b/helm/software/matita/library/dama/uniform.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "supremum.ma". +include "dama/supremum.ma". (* Definition 2.13 *) alias symbol "pair" = "Pair construction". diff --git a/helm/software/matita/library/depends b/helm/software/matita/library/depends index f98e795f2..d510318df 100644 --- a/helm/software/matita/library/depends +++ b/helm/software/matita/library/depends @@ -1,11 +1,14 @@ formal_topology/formal_topologies.ma formal_topology/basic_topologies.ma demo/formal_topology.ma logic/cprop_connectives.ma logic/equality.ma +dama/sandwich.ma dama/ordered_uniform.ma Q/ratio/rtimes.ma Q/fraction/ftimes.ma Q/ratio/rinv.ma demo/power_derivative.ma nat/compare.ma nat/nat.ma nat/orders.ma nat/plus.ma nat/compare.ma datatypes/bool.ma datatypes/compare.ma nat/orders.ma +dama/ordered_uniform.ma dama/uniform.ma nat/lt_arith.ma nat/div_and_mod.ma demo/propositional_sequent_calculus.ma datatypes/constructors.ma list/sort.ma nat/compare.ma nat/plus.ma Z/inversion.ma Z/dirichlet_product.ma Z/moebius.ma +dama/models/nat_order_continuous.ma dama/models/increasing_supremum_stabilizes.ma dama/models/nat_ordered_uniform.ma nat/factorial2.ma nat/exp.ma nat/factorial.ma nat/orders.ma higher_order_defs/ordering.ma logic/connectives.ma nat/nat.ma nat/sieve.ma list/sort.ma nat/primes.ma @@ -13,20 +16,24 @@ technicalities/setoids.ma datatypes/constructors.ma logic/coimplication.ma logic nat/div_and_mod_diseq.ma nat/lt_arith.ma logic/cprop_connectives.ma logic/connectives.ma algebra/groups.ma algebra/monoids.ma datatypes/bool.ma logic/connectives.ma nat/compare.ma nat/le_arith.ma -nat/chinese_reminder.ma nat/congruence.ma nat/exp.ma nat/gcd.ma nat/permutation.ma formal_topology/saturations_reductions.ma datatypes/subsets.ma +nat/chinese_reminder.ma nat/congruence.ma nat/exp.ma nat/gcd.ma nat/permutation.ma Q/q/qinv.ma Q/q/q.ma Q/ratio/rinv.ma nat/exp.ma nat/div_and_mod.ma nat/lt_arith.ma -list/in.ma datatypes/bool.ma datatypes/constructors.ma list/list.ma datatypes/compare.ma +list/in.ma datatypes/bool.ma datatypes/constructors.ma list/list.ma +dama/models/nat_uniform.ma dama/models/discrete_uniformity.ma dama/nat_ordered_set.ma didactic/exercises/substitution.ma nat/minus.ma +didactic/exercises/natural_deduction_fst_order.ma didactic/support/natural_deduction.ma nat/factorization2.ma list/list.ma nat/factorization.ma nat/sieve.ma formal_topology/basic_topologies.ma datatypes/categories.ma formal_topology/relations.ma formal_topology/saturations_reductions.ma +dama/models/increasing_supremum_stabilizes.ma dama/models/nat_uniform.ma dama/russell_support.ma dama/supremum.ma nat/le_arith.ma logic/connectives.ma Q/nat_fact/times.ma nat/factorization.ma decidable_kit/fintype.ma decidable_kit/eqtype.ma decidable_kit/list_aux.ma didactic/exercises/duality.ma nat/minus.ma nat/ord.ma datatypes/constructors.ma nat/exp.ma nat/gcd.ma nat/nth_prime.ma nat/relevant_equations.ma +dama/supremum.ma dama/nat_ordered_set.ma dama/sequence.ma datatypes/constructors.ma nat/plus.ma nat/totient1.ma nat/compare.ma nat/gcd_properties1.ma nat/iteration2.ma nat/totient.ma nat/times.ma nat/plus.ma nat/chebyshev_thm.ma nat/neper.ma @@ -35,18 +42,21 @@ demo/cantor.ma datatypes/constructors.ma demo/formal_topology.ma nat/nth_prime.ma nat/lt_arith.ma nat/primes.ma nat/le_arith.ma nat/orders.ma nat/times.ma decidable_kit/fgraph.ma decidable_kit/fintype.ma +dama/models/nat_ordered_uniform.ma dama/bishop_set_rewrite.ma dama/models/nat_uniform.ma dama/ordered_uniform.ma +dama/bishop_set.ma dama/ordered_set.ma nat/euler_theorem.ma nat/map_iter_p.ma nat/nat.ma nat/totient.ma Q/fraction/ftimes.ma Q/fraction/finv.ma Q/nat_fact/times.ma Q/ratio/ratio.ma Z/times.ma nat/factorial.ma nat/le_arith.ma Z/plus.ma Z/z.ma nat/minus.ma Q/ratio/rinv.ma Q/fraction/finv.ma Q/ratio/ratio.ma decidable_kit/streicher.ma logic/connectives.ma logic/equality.ma +dama/ordered_set.ma datatypes/constructors.ma logic/cprop_connectives.ma nat/fermat_little_theorem.ma nat/congruence.ma nat/exp.ma nat/gcd.ma nat/permutation.ma Q/q/qplus.ma nat/factorization.ma decidable_kit/list_aux.ma decidable_kit/eqtype.ma list/list.ma nat/plus.ma +Z/orders.ma Z/z.ma nat/orders.ma nat/map_iter_p.ma nat/count.ma nat/permutation.ma Q/q.ma Q/fraction/fraction.ma Z/compare.ma Z/plus.ma nat/factorization.ma -Z/orders.ma Z/z.ma nat/orders.ma nat/permutation.ma nat/compare.ma nat/sigma_and_pi.ma demo/realisability.ma datatypes/constructors.ma logic/connectives.ma list/list.ma datatypes/bool.ma higher_order_defs/functions.ma logic/equality.ma nat/nat.ma nat/orders.ma nat/plus.ma @@ -66,50 +76,61 @@ algebra/finite_groups.ma algebra/groups.ma nat/relevant_equations.ma decidable_kit/decidable.ma datatypes/bool.ma decidable_kit/streicher.ma logic/connectives.ma nat/compare.ma nat/pi_p.ma nat/generic_iter_p.ma nat/iteration2.ma nat/primes.ma algebra/semigroups.ma higher_order_defs/functions.ma +dama/models/discrete_uniformity.ma dama/bishop_set_rewrite.ma dama/uniform.ma +dama/lebesgue.ma dama/ordered_set.ma dama/property_exhaustivity.ma dama/sandwich.ma +formal_topology/relations.ma datatypes/subsets.ma higher_order_defs/relations.ma logic/connectives.ma nat/factorization.ma nat/ord.ma -formal_topology/relations.ma datatypes/subsets.ma nat/neper.ma nat/binomial.ma nat/chebyshev.ma nat/div_and_mod_diseq.ma nat/iteration2.ma nat/log.ma Z/moebius.ma Z/sigma_p.ma nat/factorization.ma demo/toolbox.ma logic/cprop_connectives.ma -logic/coimplication.ma logic/connectives.ma nat/iteration2.ma nat/count.ma nat/generic_iter_p.ma nat/ord.ma nat/primes.ma +logic/coimplication.ma logic/connectives.ma nat/minimization.ma nat/minus.ma logic/connectives2.ma higher_order_defs/relations.ma datatypes/subsets.ma datatypes/categories.ma logic/cprop_connectives.ma nat/chebyshev.ma nat/factorial2.ma nat/factorization.ma nat/log.ma nat/o.ma nat/pi_p.ma decidable_kit/eqtype.ma datatypes/constructors.ma decidable_kit/decidable.ma Q/q/q.ma Q/fraction/numerator_denominator.ma Q/ratio/ratio.ma +dama/models/nat_lebesgue.ma dama/lebesgue.ma dama/models/nat_order_continuous.ma nat/bertrand.ma list/in.ma list/sort.ma nat/chebyshev.ma nat/chebyshev_teta.ma nat/o.ma nat/sieve.ma nat/sqrt.ma nat/nat.ma higher_order_defs/functions.ma Q/Qaxioms.ma Z/compare.ma Z/times.ma nat/iteration2.ma +dama/uniform.ma dama/supremum.ma demo/natural_deduction.ma didactic/support/natural_deduction.ma higher_order_defs/ordering.ma logic/equality.ma -logic/equality.ma logic/connectives.ma higher_order_defs/relations.ma nat/congruence.ma nat/primes.ma nat/relevant_equations.ma -nat/gcd.ma nat/lt_arith.ma nat/primes.ma -datatypes/bool.ma higher_order_defs/functions.ma logic/equality.ma +logic/equality.ma logic/connectives.ma higher_order_defs/relations.ma +dama/property_exhaustivity.ma dama/ordered_uniform.ma dama/property_sigma.ma Z/compare.ma Z/orders.ma nat/compare.ma +datatypes/bool.ma higher_order_defs/functions.ma logic/equality.ma +nat/gcd.ma nat/lt_arith.ma nat/primes.ma +Z/dirichlet_product.ma Z/sigma_p.ma Z/times.ma nat/primes.ma algebra/monoids.ma algebra/semigroups.ma nat/div_and_mod.ma datatypes/constructors.ma nat/minus.ma -Z/dirichlet_product.ma Z/sigma_p.ma Z/times.ma nat/primes.ma nat/sqrt.ma nat/compare.ma nat/log.ma nat/times.ma datatypes/categories.ma logic/cprop_connectives.ma nat/relevant_equations.ma nat/gcd.ma nat/minus.ma nat/times.ma +dama/nat_ordered_set.ma nat/orders.ma dama/bishop_set.ma nat/compare.ma Q/fraction/finv.ma Q/fraction/fraction.ma Z/plus.ma +dama/russell_support.ma logic/cprop_connectives.ma nat/nat.ma nat/binomial.ma nat/factorial2.ma nat/iteration2.ma nat/log.ma datatypes/constructors.ma nat/div_and_mod_diseq.ma nat/iteration2.ma nat/minimization.ma nat/primes.ma nat/relevant_equations.ma higher_order_defs/functions.ma logic/equality.ma Q/fraction/numerator_denominator.ma Q/fraction/finv.ma -nat/generic_iter_p.ma nat/div_and_mod_diseq.ma nat/ord.ma nat/primes.ma datatypes/constructors.ma logic/equality.ma +nat/generic_iter_p.ma nat/div_and_mod_diseq.ma nat/ord.ma nat/primes.ma nat/plus.ma nat/nat.ma Q/fraction/fraction.ma Z/compare.ma nat/factorization.ma +dama/sequence.ma nat/nat.ma nat/primes.ma logic/connectives.ma nat/div_and_mod.ma nat/factorial.ma nat/minimization.ma nat/sigma_and_pi.ma nat/gcd_properties1.ma nat/gcd.ma list/sort.ma datatypes/bool.ma datatypes/constructors.ma list/in.ma didactic/exercises/natural_deduction.ma didactic/support/natural_deduction.ma +dama/models/list_support.ma nat/le_arith.ma list/list.ma logic/cprop_connectives.ma nat/minus.ma +dama/bishop_set_rewrite.ma dama/bishop_set.ma Z/times.ma Z/plus.ma nat/lt_arith.ma Z/sigma_p.ma Z/plus.ma Z/times.ma nat/generic_iter_p.ma nat/ord.ma nat/primes.ma nat/o.ma nat/binomial.ma nat/sqrt.ma +dama/property_sigma.ma dama/ordered_uniform.ma dama/russell_support.ma Q/inv.ma Q/fraction/finv.ma Q/q/q.ma Q/q.ma -- 2.39.2