Structure netsTheory

signature netsTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val at_def : thm
    val at_infinity : thm
    val at_neginfinity : thm
    val at_posinfinity : thm
    val bounded : thm
    val dorder : thm
    val eventually : thm
    val in_direction : thm
    val isnet : thm
    val limit : thm
    val net_TY_DEF : thm
    val netlimit : thm
    val sequentially : thm
    val tends : thm
    val tendsto : thm
    val trivial_limit : thm
    val within : thm
  
  (*  Theorems  *)
    val ALWAYS_EVENTUALLY : thm
    val AT : thm
    val AT_INFINITY : thm
    val AT_NEGINFINITY : thm
    val AT_POSINFINITY : thm
    val DORDER_LEMMA : thm
    val DORDER_NET : thm
    val DORDER_NGE : thm
    val DORDER_TENDSTO : thm
    val EVENTUALLY_AND : thm
    val EVENTUALLY_AT_INFINITY : thm
    val EVENTUALLY_AT_INFINITY_POS : thm
    val EVENTUALLY_AT_NEGINFINITY : thm
    val EVENTUALLY_AT_POSINFINITY : thm
    val EVENTUALLY_FALSE : thm
    val EVENTUALLY_FORALL : thm
    val EVENTUALLY_HAPPENS : thm
    val EVENTUALLY_MONO : thm
    val EVENTUALLY_MP : thm
    val EVENTUALLY_SEQUENTIALLY : thm
    val EVENTUALLY_TRUE : thm
    val FORALL_EVENTUALLY : thm
    val IN_DIRECTION : thm
    val LIM_TENDS : thm
    val LIM_TENDS2 : thm
    val MR1_BOUNDED : thm
    val MTOP_TENDS : thm
    val MTOP_TENDS_UNIQ : thm
    val NET : thm
    val NETLIMIT_WITHIN : thm
    val NET_ABS : thm
    val NET_ADD : thm
    val NET_CONV_BOUNDED : thm
    val NET_CONV_IBOUNDED : thm
    val NET_CONV_NZ : thm
    val NET_DILEMMA : thm
    val NET_DIV : thm
    val NET_INV : thm
    val NET_LE : thm
    val NET_MUL : thm
    val NET_NEG : thm
    val NET_NULL : thm
    val NET_NULL_ADD : thm
    val NET_NULL_CMUL : thm
    val NET_NULL_MUL : thm
    val NET_SUB : thm
    val NONTRIVIAL_LIMIT_WITHIN : thm
    val NOT_EVENTUALLY : thm
    val OLDNET : thm
    val REAL_CHOOSE_SIZE : thm
    val SEQUENTIALLY : thm
    val SEQ_TENDS : thm
    val TRIVIAL_LIMIT_AT_INFINITY : thm
    val TRIVIAL_LIMIT_AT_NEGINFINITY : thm
    val TRIVIAL_LIMIT_AT_POSINFINITY : thm
    val TRIVIAL_LIMIT_SEQUENTIALLY : thm
    val WITHIN : thm
    val WITHIN_UNIV : thm
    val WITHIN_WITHIN : thm
    val at : thm
    val limit_alt_tends : thm
    val net_tybij : thm
    val tends_imp_limit : thm
    val tendsto_mr1 : thm
    val trivial_limit_def : thm
(*
   [metric] Parent theory of "nets"
   
   [at_def]  Definition
      
      ⊢ ∀z. at z = mk_net (tendsto (mr1,z))
   
   [at_infinity]  Definition
      
      ⊢ at_infinity = mk_net (λx y. abs x ≥ abs y)
   
   [at_neginfinity]  Definition
      
      ⊢ at_neginfinity = mk_net (λx y. x ≤ y)
   
   [at_posinfinity]  Definition
      
      ⊢ at_posinfinity = mk_net (λx y. x ≥ y)
   
   [bounded]  Definition
      
      ⊢ ∀m g f.
          bounded (m,g) f ⇔ ∃k x N. g N N ∧ ∀n. g n N ⇒ dist m (f n,x) < k
   
   [dorder]  Definition
      
      ⊢ ∀g. dorder g ⇔
            ∀x y. g x x ∧ g y y ⇒ ∃z. g z z ∧ ∀w. g w z ⇒ g w x ∧ g w y
   
   [eventually]  Definition
      
      ⊢ ∀p net.
          eventually p net ⇔
          trivial_limit net ∨
          ∃y. (∃x. netord net x y) ∧ ∀x. netord net x y ⇒ p x
   
   [in_direction]  Definition
      
      ⊢ ∀a v.
          (a in_direction v) =
          (at a within {b | ∃c. 0 ≤ c ∧ b − a = c * v})
   
   [isnet]  Definition
      
      ⊢ ∀g. isnet g ⇔ ∀x y. (∀z. g z x ⇒ g z y) ∨ ∀z. g z y ⇒ g z x
   
   [limit]  Definition
      
      ⊢ ∀top f l net.
          limit top f l net ⇔
          l ∈ topspace top ∧
          ∀u. open_in top u ∧ l ∈ u ⇒ eventually (λx. f x ∈ u) net
   
   [net_TY_DEF]  Definition
      
      ⊢ ∃rep. TYPE_DEFINITION isnet rep
   
   [netlimit]  Definition
      
      ⊢ ∀net. netlimit net = @a. ∀x. ¬netord net x a
   
   [sequentially]  Definition
      
      ⊢ sequentially = mk_net (λm n. m ≥ n)
   
   [tends]  Definition
      
      ⊢ ∀s l top g.
          (s tends l) (top,g) ⇔
          ∀N. neigh top (N,l) ⇒ ∃n. g n n ∧ ∀m. g m n ⇒ N (s m)
   
   [tendsto]  Definition
      
      ⊢ ∀m x y z.
          tendsto (m,x) y z ⇔
          0 < dist m (x,y) ∧ dist m (x,y) ≤ dist m (x,z)
   
   [trivial_limit]  Definition
      
      ⊢ ∀net.
          trivial_limit net ⇔
          (∀a b. a = b) ∨
          ∃a b. a ≠ b ∧ ∀x. ¬netord net x a ∧ ¬netord net x b
   
   [within]  Definition
      
      ⊢ ∀net s. (net within s) = mk_net (λx y. netord net x y ∧ x ∈ s)
   
   [ALWAYS_EVENTUALLY]  Theorem
      
      ⊢ ∀net p. (∀x. p x) ⇒ eventually p net
   
   [AT]  Theorem
      
      ⊢ ∀a x y.
          netord (at a) x y ⇔ 0 < dist (x,a) ∧ dist (x,a) ≤ dist (y,a)
   
   [AT_INFINITY]  Theorem
      
      ⊢ ∀x y. netord at_infinity x y ⇔ abs x ≥ abs y
   
   [AT_NEGINFINITY]  Theorem
      
      ⊢ ∀x y. netord at_neginfinity x y ⇔ x ≤ y
   
   [AT_POSINFINITY]  Theorem
      
      ⊢ ∀x y. netord at_posinfinity x y ⇔ x ≥ y
   
   [DORDER_LEMMA]  Theorem
      
      ⊢ ∀g. dorder g ⇒
            ∀P Q.
              (∃n. g n n ∧ ∀m. g m n ⇒ P m) ∧ (∃n. g n n ∧ ∀m. g m n ⇒ Q m) ⇒
              ∃n. g n n ∧ ∀m. g m n ⇒ P m ∧ Q m
   
   [DORDER_NET]  Theorem
      
      ⊢ ∀n. dorder (netord n)
   
   [DORDER_NGE]  Theorem
      
      ⊢ dorder $>=
   
   [DORDER_TENDSTO]  Theorem
      
      ⊢ ∀m x. dorder (tendsto (m,x))
   
   [EVENTUALLY_AND]  Theorem
      
      ⊢ ∀net p q.
          eventually (λx. p x ∧ q x) net ⇔
          eventually p net ∧ eventually q net
   
   [EVENTUALLY_AT_INFINITY]  Theorem
      
      ⊢ ∀p. eventually p at_infinity ⇔ ∃b. ∀x. abs x ≥ b ⇒ p x
   
   [EVENTUALLY_AT_INFINITY_POS]  Theorem
      
      ⊢ ∀p. eventually p at_infinity ⇔ ∃b. 0 < b ∧ ∀x. abs x ≥ b ⇒ p x
   
   [EVENTUALLY_AT_NEGINFINITY]  Theorem
      
      ⊢ ∀p. eventually p at_neginfinity ⇔ ∃b. ∀x. x ≤ b ⇒ p x
   
   [EVENTUALLY_AT_POSINFINITY]  Theorem
      
      ⊢ ∀p. eventually p at_posinfinity ⇔ ∃b. ∀x. x ≥ b ⇒ p x
   
   [EVENTUALLY_FALSE]  Theorem
      
      ⊢ ∀net. eventually (λx. F) net ⇔ trivial_limit net
   
   [EVENTUALLY_FORALL]  Theorem
      
      ⊢ ∀net p s.
          FINITE s ∧ s ≠ ∅ ⇒
          (eventually (λx. ∀a. a ∈ s ⇒ p a x) net ⇔
           ∀a. a ∈ s ⇒ eventually (p a) net)
   
   [EVENTUALLY_HAPPENS]  Theorem
      
      ⊢ ∀net p. eventually p net ⇒ trivial_limit net ∨ ∃x. p x
   
   [EVENTUALLY_MONO]  Theorem
      
      ⊢ ∀net p q. (∀x. p x ⇒ q x) ∧ eventually p net ⇒ eventually q net
   
   [EVENTUALLY_MP]  Theorem
      
      ⊢ ∀net p q.
          eventually (λx. p x ⇒ q x) net ∧ eventually p net ⇒
          eventually q net
   
   [EVENTUALLY_SEQUENTIALLY]  Theorem
      
      ⊢ ∀p. eventually p sequentially ⇔ ∃N. ∀n. N ≤ n ⇒ p n
   
   [EVENTUALLY_TRUE]  Theorem
      
      ⊢ ∀net. eventually (λx. T) net ⇔ T
   
   [FORALL_EVENTUALLY]  Theorem
      
      ⊢ ∀net p s.
          FINITE s ∧ s ≠ ∅ ⇒
          ((∀a. a ∈ s ⇒ eventually (p a) net) ⇔
           eventually (λx. ∀a. a ∈ s ⇒ p a x) net)
   
   [IN_DIRECTION]  Theorem
      
      ⊢ ∀a v x y.
          netord (a in_direction v) x y ⇔
          0 < dist (x,a) ∧ dist (x,a) ≤ dist (y,a) ∧
          ∃c. 0 ≤ c ∧ x − a = c * v
   
   [LIM_TENDS]  Theorem
      
      ⊢ ∀m1 m2 f x0 y0.
          limpt (mtop m1) x0 𝕌(:α) ⇒
          ((f tends y0) (mtop m2,tendsto (m1,x0)) ⇔
           ∀e. 0 < e ⇒
               ∃d. 0 < d ∧
                   ∀x. 0 < dist m1 (x,x0) ∧ dist m1 (x,x0) ≤ d ⇒
                       dist m2 (f x,y0) < e)
   
   [LIM_TENDS2]  Theorem
      
      ⊢ ∀m1 m2 f x0 y0.
          limpt (mtop m1) x0 𝕌(:α) ⇒
          ((f tends y0) (mtop m2,tendsto (m1,x0)) ⇔
           ∀e. 0 < e ⇒
               ∃d. 0 < d ∧
                   ∀x. 0 < dist m1 (x,x0) ∧ dist m1 (x,x0) < d ⇒
                       dist m2 (f x,y0) < e)
   
   [MR1_BOUNDED]  Theorem
      
      ⊢ ∀g f. bounded (mr1,g) f ⇔ ∃k N. g N N ∧ ∀n. g n N ⇒ abs (f n) < k
   
   [MTOP_TENDS]  Theorem
      
      ⊢ ∀d g x x0.
          (x tends x0) (mtop d,g) ⇔
          ∀e. 0 < e ⇒ ∃n. g n n ∧ ∀m. g m n ⇒ dist d (x m,x0) < e
   
   [MTOP_TENDS_UNIQ]  Theorem
      
      ⊢ ∀g d.
          dorder g ⇒
          (x tends x0) (mtop d,g) ∧ (x tends x1) (mtop d,g) ⇒
          x0 = x1
   
   [NET]  Theorem
      
      ⊢ ∀n x y.
          (∀z. netord n z x ⇒ netord n z y) ∨
          ∀z. netord n z y ⇒ netord n z x
   
   [NETLIMIT_WITHIN]  Theorem
      
      ⊢ ∀a s. ¬trivial_limit (at a within s) ⇒ netlimit (at a within s) = a
   
   [NET_ABS]  Theorem
      
      ⊢ ∀g x x0.
          (x tends x0) (mtop mr1,g) ⇒
          ((λn. abs (x n)) tends abs x0) (mtop mr1,g)
   
   [NET_ADD]  Theorem
      
      ⊢ ∀g. dorder g ⇒
            ∀x x0 y y0.
              (x tends x0) (mtop mr1,g) ∧ (y tends y0) (mtop mr1,g) ⇒
              ((λn. x n + y n) tends (x0 + y0)) (mtop mr1,g)
   
   [NET_CONV_BOUNDED]  Theorem
      
      ⊢ ∀g x x0. (x tends x0) (mtop mr1,g) ⇒ bounded (mr1,g) x
   
   [NET_CONV_IBOUNDED]  Theorem
      
      ⊢ ∀g x x0.
          (x tends x0) (mtop mr1,g) ∧ x0 ≠ 0 ⇒
          bounded (mr1,g) (λn. (x n)⁻¹)
   
   [NET_CONV_NZ]  Theorem
      
      ⊢ ∀g x x0.
          (x tends x0) (mtop mr1,g) ∧ x0 ≠ 0 ⇒
          ∃N. g N N ∧ ∀n. g n N ⇒ x n ≠ 0
   
   [NET_DILEMMA]  Theorem
      
      ⊢ ∀net.
          (∃a. (∃x. netord net x a) ∧ ∀x. netord net x a ⇒ P x) ∧
          (∃b. (∃x. netord net x b) ∧ ∀x. netord net x b ⇒ Q x) ⇒
          ∃c. (∃x. netord net x c) ∧ ∀x. netord net x c ⇒ P x ∧ Q x
   
   [NET_DIV]  Theorem
      
      ⊢ ∀g. dorder g ⇒
            ∀x x0 y y0.
              (x tends x0) (mtop mr1,g) ∧ (y tends y0) (mtop mr1,g) ∧
              y0 ≠ 0 ⇒
              ((λn. x n / y n) tends (x0 / y0)) (mtop mr1,g)
   
   [NET_INV]  Theorem
      
      ⊢ ∀g. dorder g ⇒
            ∀x x0.
              (x tends x0) (mtop mr1,g) ∧ x0 ≠ 0 ⇒
              ((λn. (x n)⁻¹) tends x0⁻¹) (mtop mr1,g)
   
   [NET_LE]  Theorem
      
      ⊢ ∀g. dorder g ⇒
            ∀x x0 y y0.
              (x tends x0) (mtop mr1,g) ∧ (y tends y0) (mtop mr1,g) ∧
              (∃N. g N N ∧ ∀n. g n N ⇒ x n ≤ y n) ⇒
              x0 ≤ y0
   
   [NET_MUL]  Theorem
      
      ⊢ ∀g. dorder g ⇒
            ∀x y x0 y0.
              (x tends x0) (mtop mr1,g) ∧ (y tends y0) (mtop mr1,g) ⇒
              ((λn. x n * y n) tends (x0 * y0)) (mtop mr1,g)
   
   [NET_NEG]  Theorem
      
      ⊢ ∀g. dorder g ⇒
            ∀x x0.
              (x tends x0) (mtop mr1,g) ⇔
              ((λn. -x n) tends -x0) (mtop mr1,g)
   
   [NET_NULL]  Theorem
      
      ⊢ ∀g x x0.
          (x tends x0) (mtop mr1,g) ⇔ ((λn. x n − x0) tends 0) (mtop mr1,g)
   
   [NET_NULL_ADD]  Theorem
      
      ⊢ ∀g. dorder g ⇒
            ∀x y.
              (x tends 0) (mtop mr1,g) ∧ (y tends 0) (mtop mr1,g) ⇒
              ((λn. x n + y n) tends 0) (mtop mr1,g)
   
   [NET_NULL_CMUL]  Theorem
      
      ⊢ ∀g k x.
          (x tends 0) (mtop mr1,g) ⇒ ((λn. k * x n) tends 0) (mtop mr1,g)
   
   [NET_NULL_MUL]  Theorem
      
      ⊢ ∀g. dorder g ⇒
            ∀x y.
              bounded (mr1,g) x ∧ (y tends 0) (mtop mr1,g) ⇒
              ((λn. x n * y n) tends 0) (mtop mr1,g)
   
   [NET_SUB]  Theorem
      
      ⊢ ∀g. dorder g ⇒
            ∀x x0 y y0.
              (x tends x0) (mtop mr1,g) ∧ (y tends y0) (mtop mr1,g) ⇒
              ((λn. x n − y n) tends (x0 − y0)) (mtop mr1,g)
   
   [NONTRIVIAL_LIMIT_WITHIN]  Theorem
      
      ⊢ ∀net s. trivial_limit net ⇒ trivial_limit (net within s)
   
   [NOT_EVENTUALLY]  Theorem
      
      ⊢ ∀net p. (∀x. ¬p x) ∧ ¬trivial_limit net ⇒ ¬eventually p net
   
   [OLDNET]  Theorem
      
      ⊢ ∀n x y.
          netord n x x ∧ netord n y y ⇒
          ∃z. netord n z z ∧ ∀w. netord n w z ⇒ netord n w x ∧ netord n w y
   
   [REAL_CHOOSE_SIZE]  Theorem
      
      ⊢ ∀c. 0 ≤ c ⇒ ∃x. abs x = c
   
   [SEQUENTIALLY]  Theorem
      
      ⊢ ∀m n. netord sequentially m n ⇔ m ≥ n
   
   [SEQ_TENDS]  Theorem
      
      ⊢ ∀d x x0.
          (x tends x0) (mtop d,$>=) ⇔
          ∀e. 0 < e ⇒ ∃N. ∀n. n ≥ N ⇒ dist d (x n,x0) < e
   
   [TRIVIAL_LIMIT_AT_INFINITY]  Theorem
      
      ⊢ ¬trivial_limit at_infinity
   
   [TRIVIAL_LIMIT_AT_NEGINFINITY]  Theorem
      
      ⊢ ¬trivial_limit at_neginfinity
   
   [TRIVIAL_LIMIT_AT_POSINFINITY]  Theorem
      
      ⊢ ¬trivial_limit at_posinfinity
   
   [TRIVIAL_LIMIT_SEQUENTIALLY]  Theorem
      
      ⊢ ¬trivial_limit sequentially
   
   [WITHIN]  Theorem
      
      ⊢ ∀n s x y. netord (n within s) x y ⇔ netord n x y ∧ x ∈ s
   
   [WITHIN_UNIV]  Theorem
      
      ⊢ ∀x. (at x within 𝕌(:real)) = at x
   
   [WITHIN_WITHIN]  Theorem
      
      ⊢ ∀net s t. ((net within s) within t) = (net within s ∩ t)
   
   [at]  Theorem
      
      ⊢ ∀a. at a = mk_net (λx y. 0 < dist (x,a) ∧ dist (x,a) ≤ dist (y,a))
   
   [limit_alt_tends]  Theorem
      
      ⊢ ∀top f l net.
          ¬trivial_limit net ∧ l ∈ topspace top ∧
          (∀x y. netord net x y ⇒ netord net y y) ⇒
          (limit top f l net ⇔ (f tends l) (top,netord net))
   
   [net_tybij]  Theorem
      
      ⊢ (∀a. mk_net (netord a) = a) ∧
        ∀r. (∀x y. (∀z. r z x ⇒ r z y) ∨ ∀z. r z y ⇒ r z x) ⇔
            netord (mk_net r) = r
   
   [tends_imp_limit]  Theorem
      
      ⊢ ∀top f l net.
          ¬trivial_limit net ∧ l ∈ topspace top ⇒
          (f tends l) (top,netord net) ⇒
          limit top f l net
   
   [tendsto_mr1]  Theorem
      
      ⊢ ∀m a. tendsto (mr1,a) = netord (at a)
   
   [trivial_limit_def]  Theorem
      
      ⊢ ∀net. trivial_limit net ⇔ eventually (λx. F) net
   
   
*)
end

HOL 4, Trindemossen-2