helm/software/matita/contribs/dama/dama/models/uniformnat.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 include "datatypes/constructors.ma".
  16 include "nat_ordered_set.ma".
  17 include "bishop_set_rewrite.ma".
  18 include "uniform.ma".
  19
  20 definition discrete_uniform_space_of_bishop_set:bishop_set → uniform_space.
  21 intro C; apply (mk_uniform_space C);
  22 [1: intro; apply (∃_:unit.∀n:C square.(fst n ≈ snd n → P n) ∧ (P n → fst n ≈ snd n));
  23 |2: intros 4 (U H x Hx); unfold in Hx;
  24     cases H (_ H1); cases (H1 x); apply H2; apply Hx;
  25 |3: intros; cases H (_ PU); cases H1 (_ PV);
  26     exists[apply (λx.U x ∧ V x)] split;
  27     [1: exists[apply something] intro; cases (PU n); cases (PV n);
  28         split; intros; try split;[apply H2;|apply H4] try assumption;
  29         apply H3; cases H6; assumption;
  30     |2: simplify; unfold mk_set; intros; assumption;]
  31 |4: intros; cases H (_ PU); exists [apply U] split;
  32     [1: exists [apply something] intro n; cases (PU n);
  33         split; intros; try split;[apply H1;|apply H2] assumption;
  34     |2: intros 2 (x Hx); cases Hx; cases H1; clear H1;
  35         cases (PU 〈(fst x),x1〉); lapply (H4 H2) as H5; simplify in H5;
  36         cases (PU 〈x1,(snd x)〉); lapply (H7 H3) as H8; simplify in H8;
  37         generalize in match H5; generalize in match H8;
  38         generalize in match (PU x); clear H6 H7 H1 H4 H2 H3 H5 H8;
  39         cases x; simplify; intros; cases H1; clear H1; apply H4;
  40         apply (eq_trans ???? H3 H2);]
  41 |5: intros; cases H (_ H1); split; cases x;
  42     [2: cases (H1 〈b,b1〉); intro; apply H2; cases (H1 〈b1,b〉);
  43         lapply (H6 H4) as H7; apply eq_sym; apply H7;
  44     |1: cases (H1 〈b1,b〉); intro; apply H2; cases (H1 〈b,b1〉);
  45         lapply (H6 H4) as H7; apply eq_sym; apply H7;]]
  46 qed.
  47
  48 definition nat_uniform_space: uniform_space.
  49 apply (discrete_uniform_space_of_bishop_set nat_ordered_set);
  50 qed.