Theory Topological_Spaces

(*  Title:      HOL/Topological_Spaces.thy
    Author:     Brian Huffman
    Author:     Johannes Hölzl
*)

section ‹Topological Spaces›

theory Topological_Spaces
  imports Main
begin

named_theorems continuous_intros "structural introduction rules for continuity"

subsection ‹Topological space›

class "open" =
  fixes "open" :: "'a set  bool"

class topological_space = "open" +
  assumes open_UNIV [simp, intro]: "open UNIV"
  assumes open_Int [intro]: "open S  open T  open (S  T)"
  assumes open_Union [intro]: "SK. open S  open (K)"
begin

definition closed :: "'a set  bool"
  where "closed S  open (- S)"

lemma open_empty [continuous_intros, intro, simp]: "open {}"
  using open_Union [of "{}"] by simp

lemma open_Un [continuous_intros, intro]: "open S  open T  open (S  T)"
  using open_Union [of "{S, T}"] by simp

lemma open_UN [continuous_intros, intro]: "xA. open (B x)  open (xA. B x)"
  using open_Union [of "B ` A"] by simp

lemma open_Inter [continuous_intros, intro]: "finite S  TS. open T  open (S)"
  by (induction set: finite) auto

lemma open_INT [continuous_intros, intro]: "finite A  xA. open (B x)  open (xA. B x)"
  using open_Inter [of "B ` A"] by simp

lemma openI:
  assumes "x. x  S  T. open T  x  T  T  S"
  shows "open S"
proof -
  have "open ({T. open T  T  S})" by auto
  moreover have "{T. open T  T  S} = S" by (auto dest!: assms)
  ultimately show "open S" by simp
qed

lemma open_subopen: "open S  (xS. T. open T  x  T  T  S)"
by (auto intro: openI)

lemma closed_empty [continuous_intros, intro, simp]: "closed {}"
  unfolding closed_def by simp

lemma closed_Un [continuous_intros, intro]: "closed S  closed T  closed (S  T)"
  unfolding closed_def by auto

lemma closed_UNIV [continuous_intros, intro, simp]: "closed UNIV"
  unfolding closed_def by simp

lemma closed_Int [continuous_intros, intro]: "closed S  closed T  closed (S  T)"
  unfolding closed_def by auto

lemma closed_INT [continuous_intros, intro]: "xA. closed (B x)  closed (xA. B x)"
  unfolding closed_def by auto

lemma closed_Inter [continuous_intros, intro]: "SK. closed S  closed (K)"
  unfolding closed_def uminus_Inf by auto

lemma closed_Union [continuous_intros, intro]: "finite S  TS. closed T  closed (S)"
  by (induct set: finite) auto

lemma closed_UN [continuous_intros, intro]:
  "finite A  xA. closed (B x)  closed (xA. B x)"
  using closed_Union [of "B ` A"] by simp

lemma open_closed: "open S  closed (- S)"
  by (simp add: closed_def)

lemma closed_open: "closed S  open (- S)"
  by (rule closed_def)

lemma open_Diff [continuous_intros, intro]: "open S  closed T  open (S - T)"
  by (simp add: closed_open Diff_eq open_Int)

lemma closed_Diff [continuous_intros, intro]: "closed S  open T  closed (S - T)"
  by (simp add: open_closed Diff_eq closed_Int)

lemma open_Compl [continuous_intros, intro]: "closed S  open (- S)"
  by (simp add: closed_open)

lemma closed_Compl [continuous_intros, intro]: "open S  closed (- S)"
  by (simp add: open_closed)

lemma open_Collect_neg: "closed {x. P x}  open {x. ¬ P x}"
  unfolding Collect_neg_eq by (rule open_Compl)

lemma open_Collect_conj:
  assumes "open {x. P x}" "open {x. Q x}"
  shows "open {x. P x  Q x}"
  using open_Int[OF assms] by (simp add: Int_def)

lemma open_Collect_disj:
  assumes "open {x. P x}" "open {x. Q x}"
  shows "open {x. P x  Q x}"
  using open_Un[OF assms] by (simp add: Un_def)

lemma open_Collect_ex: "(i. open {x. P i x})  open {x. i. P i x}"
  using open_UN[of UNIV "λi. {x. P i x}"] unfolding Collect_ex_eq by simp

lemma open_Collect_imp: "closed {x. P x}  open {x. Q x}  open {x. P x  Q x}"
  unfolding imp_conv_disj by (intro open_Collect_disj open_Collect_neg)

lemma open_Collect_const: "open {x. P}"
  by (cases P) auto

lemma closed_Collect_neg: "open {x. P x}  closed {x. ¬ P x}"
  unfolding Collect_neg_eq by (rule closed_Compl)

lemma closed_Collect_conj:
  assumes "closed {x. P x}" "closed {x. Q x}"
  shows "closed {x. P x  Q x}"
  using closed_Int[OF assms] by (simp add: Int_def)

lemma closed_Collect_disj:
  assumes "closed {x. P x}" "closed {x. Q x}"
  shows "closed {x. P x  Q x}"
  using closed_Un[OF assms] by (simp add: Un_def)

lemma closed_Collect_all: "(i. closed {x. P i x})  closed {x. i. P i x}"
  using closed_INT[of UNIV "λi. {x. P i x}"] by (simp add: Collect_all_eq)

lemma closed_Collect_imp: "open {x. P x}  closed {x. Q x}  closed {x. P x  Q x}"
  unfolding imp_conv_disj by (intro closed_Collect_disj closed_Collect_neg)

lemma closed_Collect_const: "closed {x. P}"
  by (cases P) auto

end


subsection ‹Hausdorff and other separation properties›

class t0_space = topological_space +
  assumes t0_space: "x  y  U. open U  ¬ (x  U  y  U)"

class t1_space = topological_space +
  assumes t1_space: "x  y  U. open U  x  U  y  U"

instance t1_space  t0_space
  by standard (fast dest: t1_space)

context t1_space begin

lemma separation_t1: "x  y  (U. open U  x  U  y  U)"
  using t1_space[of x y] by blast

lemma closed_singleton [iff]: "closed {a}"
proof -
  let ?T = "{S. open S  a  S}"
  have "open ?T"
    by (simp add: open_Union)
  also have "?T = - {a}"
    by (auto simp add: set_eq_iff separation_t1)
  finally show "closed {a}"
    by (simp only: closed_def)
qed

lemma closed_insert [continuous_intros, simp]:
  assumes "closed S"
  shows "closed (insert a S)"
proof -
  from closed_singleton assms have "closed ({a}  S)"
    by (rule closed_Un)
  then show "closed (insert a S)"
    by simp
qed

lemma finite_imp_closed: "finite S  closed S"
  by (induct pred: finite) simp_all

end

text ‹T2 spaces are also known as Hausdorff spaces.›

class t2_space = topological_space +
  assumes hausdorff: "x  y  U V. open U  open V  x  U  y  V  U  V = {}"

instance t2_space  t1_space
  by standard (fast dest: hausdorff)

lemma (in t2_space) separation_t2: "x  y  (U V. open U  open V  x  U  y  V  U  V = {})"
  using hausdorff [of x y] by blast

lemma (in t0_space) separation_t0: "x  y  (U. open U  ¬ (x  U  y  U))"
  using t0_space [of x y] by blast


text ‹A classical separation axiom for topological space, the T3 axiom -- also called regularity:
if a point is not in a closed set, then there are open sets separating them.›

class t3_space = t2_space +
  assumes t3_space: "closed S  y  S  U V. open U  open V  y  U  S  V  U  V = {}"

text ‹A classical separation axiom for topological space, the T4 axiom -- also called normality:
if two closed sets are disjoint, then there are open sets separating them.›

class t4_space = t2_space +
  assumes t4_space: "closed S  closed T  S  T = {}  U V. open U  open V  S  U  T  V  U  V = {}"

text ‹T4 is stronger than T3, and weaker than metric.›

instance t4_space  t3_space
proof
  fix S and y::'a assume "closed S" "y  S"
  then show "U V. open U  open V  y  U  S  V  U  V = {}"
    using t4_space[of "{y}" S] by auto
qed

text ‹A perfect space is a topological space with no isolated points.›

class perfect_space = topological_space +
  assumes not_open_singleton: "¬ open {x}"

lemma (in perfect_space) UNIV_not_singleton: "UNIV  {x}"
  for x::'a
  by (metis (no_types) open_UNIV not_open_singleton)


subsection ‹Generators for toplogies›

inductive generate_topology :: "'a set set  'a set  bool" for S :: "'a set set"
  where
    UNIV: "generate_topology S UNIV"
  | Int: "generate_topology S (a  b)" if "generate_topology S a" and "generate_topology S b"
  | UN: "generate_topology S (K)" if "(k. k  K  generate_topology S k)"
  | Basis: "generate_topology S s" if "s  S"

hide_fact (open) UNIV Int UN Basis

lemma generate_topology_Union:
  "(k. k  I  generate_topology S (K k))  generate_topology S (kI. K k)"
  using generate_topology.UN [of "K ` I"] by auto

lemma topological_space_generate_topology: "class.topological_space (generate_topology S)"
  by standard (auto intro: generate_topology.intros)


subsection ‹Order topologies›

class order_topology = order + "open" +
  assumes open_generated_order: "open = generate_topology (range (λa. {..< a})  range (λa. {a <..}))"
begin

subclass topological_space
  unfolding open_generated_order
  by (rule topological_space_generate_topology)

lemma open_greaterThan [continuous_intros, simp]: "open {a <..}"
  unfolding open_generated_order by (auto intro: generate_topology.Basis)

lemma open_lessThan [continuous_intros, simp]: "open {..< a}"
  unfolding open_generated_order by (auto intro: generate_topology.Basis)

lemma open_greaterThanLessThan [continuous_intros, simp]: "open {a <..< b}"
   unfolding greaterThanLessThan_eq by (simp add: open_Int)

end

class linorder_topology = linorder + order_topology

lemma closed_atMost [continuous_intros, simp]: "closed {..a}"
  for a :: "'a::linorder_topology"
  by (simp add: closed_open)

lemma closed_atLeast [continuous_intros, simp]: "closed {a..}"
  for a :: "'a::linorder_topology"
  by (simp add: closed_open)

lemma closed_atLeastAtMost [continuous_intros, simp]: "closed {a..b}"
  for a b :: "'a::linorder_topology"
proof -
  have "{a .. b} = {a ..}  {.. b}"
    by auto
  then show ?thesis
    by (simp add: closed_Int)
qed

lemma (in order) less_separate:
  assumes "x < y"
  shows "a b. x  {..< a}  y  {b <..}  {..< a}  {b <..} = {}"
proof (cases "z. x < z  z < y")
  case True
  then obtain z where "x < z  z < y" ..
  then have "x  {..< z}  y  {z <..}  {z <..}  {..< z} = {}"
    by auto
  then show ?thesis by blast
next
  case False
  with x < y have "x  {..< y}" "y  {x <..}" "{x <..}  {..< y} = {}"
    by auto
  then show ?thesis by blast
qed

instance linorder_topology  t2_space
proof
  fix x y :: 'a
  show "x  y  U V. open U  open V  x  U  y  V  U  V = {}"
    using less_separate [of x y] less_separate [of y x]
    by (elim neqE; metis open_lessThan open_greaterThan Int_commute)
qed

lemma (in linorder_topology) open_right:
  assumes "open S" "x  S"
    and gt_ex: "x < y"
  shows "b>x. {x ..< b}  S"
  using assms unfolding open_generated_order
proof induct
  case UNIV
  then show ?case by blast
next
  case (Int A B)
  then obtain a b where "a > x" "{x ..< a}  A"  "b > x" "{x ..< b}  B"
    by auto
  then show ?case
    by (auto intro!: exI[of _ "min a b"])
next
  case UN
  then show ?case by blast
next
  case Basis
  then show ?case
    by (fastforce intro: exI[of _ y] gt_ex)
qed

lemma (in linorder_topology) open_left:
  assumes "open S" "x  S"
    and lt_ex: "y < x"
  shows "b<x. {b <.. x}  S"
  using assms unfolding open_generated_order
proof induction
  case UNIV
  then show ?case by blast
next
  case (Int A B)
  then obtain a b where "a < x" "{a <.. x}  A"  "b < x" "{b <.. x}  B"
    by auto
  then show ?case
    by (auto intro!: exI[of _ "max a b"])
next
  case UN
  then show ?case by blast
next
  case Basis
  then show ?case
    by (fastforce intro: exI[of _ y] lt_ex)
qed


subsection ‹Setup some topologies›

subsubsection ‹Boolean is an order topology›

class discrete_topology = topological_space +
  assumes open_discrete: "A. open A"

instance discrete_topology < t2_space
proof
  fix x y :: 'a
  assume "x  y"
  then show "U V. open U  open V  x  U  y  V  U  V = {}"
    by (intro exI[of _ "{_}"]) (auto intro!: open_discrete)
qed

instantiation bool :: linorder_topology
begin

definition open_bool :: "bool set  bool"
  where "open_bool = generate_topology (range (λa. {..< a})  range (λa. {a <..}))"

instance
  by standard (rule open_bool_def)

end

instance bool :: discrete_topology
proof
  fix A :: "bool set"
  have *: "{False <..} = {True}" "{..< True} = {False}"
    by auto
  have "A = UNIV  A = {}  A = {False <..}  A = {..< True}"
    using subset_UNIV[of A] unfolding UNIV_bool * by blast
  then show "open A"
    by auto
qed

instantiation nat :: linorder_topology
begin

definition open_nat :: "nat set  bool"
  where "open_nat = generate_topology (range (λa. {..< a})  range (λa. {a <..}))"

instance
  by standard (rule open_nat_def)

end

instance nat :: discrete_topology
proof
  fix A :: "nat set"
  have "open {n}" for n :: nat
  proof (cases n)
    case 0
    moreover have "{0} = {..<1::nat}"
      by auto
    ultimately show ?thesis
       by auto
  next
    case (Suc n')
    then have "{n} = {..<Suc n}  {n' <..}"
      by auto
    with Suc show ?thesis
      by (auto intro: open_lessThan open_greaterThan)
  qed
  then have "open (aA. {a})"
    by (intro open_UN) auto
  then show "open A"
    by simp
qed

instantiation int :: linorder_topology
begin

definition open_int :: "int set  bool"
  where "open_int = generate_topology (range (λa. {..< a})  range (λa. {a <..}))"

instance
  by standard (rule open_int_def)

end

instance int :: discrete_topology
proof
  fix A :: "int set"
  have "{..<i + 1}  {i-1 <..} = {i}" for i :: int
    by auto
  then have "open {i}" for i :: int
    using open_Int[OF open_lessThan[of "i + 1"] open_greaterThan[of "i - 1"]] by auto
  then have "open (aA. {a})"
    by (intro open_UN) auto
  then show "open A"
    by simp
qed


subsubsection ‹Topological filters›

definition (in topological_space) nhds :: "'a  'a filter"
  where "nhds a = (INF S{S. open S  a  S}. principal S)"

definition (in topological_space) at_within :: "'a  'a set  'a filter"
    (at (_)/ within (_) [1000, 60] 60)
  where "at a within s = inf (nhds a) (principal (s - {a}))"

abbreviation (in topological_space) at :: "'a  'a filter"  (at)
  where "at x  at x within (CONST UNIV)"

abbreviation (in order_topology) at_right :: "'a  'a filter"
  where "at_right x  at x within {x <..}"

abbreviation (in order_topology) at_left :: "'a  'a filter"
  where "at_left x  at x within {..< x}"

lemma (in topological_space) nhds_generated_topology:
  "open = generate_topology T  nhds x = (INF S{ST. x  S}. principal S)"
  unfolding nhds_def
proof (safe intro!: antisym INF_greatest)
  fix S
  assume "generate_topology T S" "x  S"
  then show "(INF S{S  T. x  S}. principal S)  principal S"
    by induct
      (auto intro: INF_lower order_trans simp: inf_principal[symmetric] simp del: inf_principal)
qed (auto intro!: INF_lower intro: generate_topology.intros)

lemma (in topological_space) eventually_nhds:
  "eventually P (nhds a)  (S. open S  a  S  (xS. P x))"
  unfolding nhds_def by (subst eventually_INF_base) (auto simp: eventually_principal)

lemma eventually_eventually:
  "eventually (λy. eventually P (nhds y)) (nhds x) = eventually P (nhds x)"
  by (auto simp: eventually_nhds)

lemma (in topological_space) eventually_nhds_in_open:
  "open s  x  s  eventually (λy. y  s) (nhds x)"
  by (subst eventually_nhds) blast

lemma (in topological_space) eventually_nhds_x_imp_x: "eventually P (nhds x)  P x"
  by (subst (asm) eventually_nhds) blast

lemma (in topological_space) nhds_neq_bot [simp]: "nhds a  bot"
  by (simp add: trivial_limit_def eventually_nhds)

lemma (in t1_space) t1_space_nhds: "x  y  (F x in nhds x. x  y)"
  by (drule t1_space) (auto simp: eventually_nhds)

lemma (in topological_space) nhds_discrete_open: "open {x}  nhds x = principal {x}"
  by (auto simp: nhds_def intro!: antisym INF_greatest INF_lower2[of "{x}"])

lemma (in discrete_topology) nhds_discrete: "nhds x = principal {x}"
  by (simp add: nhds_discrete_open open_discrete)

lemma (in discrete_topology) at_discrete: "at x within S = bot"
  unfolding at_within_def nhds_discrete by simp

lemma (in discrete_topology) tendsto_discrete:
  "filterlim (f :: 'b  'a) (nhds y) F  eventually (λx. f x = y) F"
  by (auto simp: nhds_discrete filterlim_principal)

lemma (in topological_space) at_within_eq:
  "at x within s = (INF S{S. open S  x  S}. principal (S  s - {x}))"
  unfolding nhds_def at_within_def
  by (subst INF_inf_const2[symmetric]) (auto simp: Diff_Int_distrib)

lemma (in topological_space) eventually_at_filter:
  "eventually P (at a within s)  eventually (λx. x  a  x  s  P x) (nhds a)"
  by (simp add: at_within_def eventually_inf_principal imp_conjL[symmetric] conj_commute)

lemma (in topological_space) at_le: "s  t  at x within s  at x within t"
  unfolding at_within_def by (intro inf_mono) auto

lemma (in topological_space) eventually_at_topological:
  "eventually P (at a within s)  (S. open S  a  S  (xS. x  a  x  s  P x))"
  by (simp add: eventually_nhds eventually_at_filter)

lemma eventually_nhds_conv_at:
  "eventually P (nhds x)  eventually P (at x)  P x"
  unfolding eventually_at_topological eventually_nhds by fast

lemma eventually_at_in_open:
  assumes "open A" "x  A"
  shows   "eventually (λy. y  A - {x}) (at x)"
  using assms eventually_at_topological by blast

lemma eventually_at_in_open':
  assumes "open A" "x  A"
  shows   "eventually (λy. y  A) (at x)"
  using assms eventually_at_topological by blast

lemma (in topological_space) at_within_open: "a  S  open S  at a within S = at a"
  unfolding filter_eq_iff eventually_at_topological by (metis open_Int Int_iff UNIV_I)

lemma (in topological_space) at_within_open_NO_MATCH:
  "a  s  open s  NO_MATCH UNIV s  at a within s = at a"
  by (simp only: at_within_open)

lemma (in topological_space) at_within_open_subset:
  "a  S  open S  S  T  at a within T = at a"
  by (metis at_le at_within_open dual_order.antisym subset_UNIV)

lemma (in topological_space) at_within_nhd:
  assumes "x  S" "open S" "T  S - {x} = U  S - {x}"
  shows "at x within T = at x within U"
  unfolding filter_eq_iff eventually_at_filter
proof (intro allI eventually_subst)
  have "eventually (λx. x  S) (nhds x)"
    using x  S open S by (auto simp: eventually_nhds)
  then show "F n in nhds x. (n  x  n  T  P n) = (n  x  n  U  P n)" for P
    by eventually_elim (insert T  S - {x} = U  S - {x}, blast)
qed

lemma (in topological_space) at_within_empty [simp]: "at a within {} = bot"
  unfolding at_within_def by simp

lemma (in topological_space) at_within_union:
  "at x within (S  T) = sup (at x within S) (at x within T)"
  unfolding filter_eq_iff eventually_sup eventually_at_filter
  by (auto elim!: eventually_rev_mp)

lemma (in topological_space) at_eq_bot_iff: "at a = bot  open {a}"
  unfolding trivial_limit_def eventually_at_topological
  by (metis UNIV_I empty_iff is_singletonE is_singletonI' singleton_iff)

lemma (in t1_space) eventually_neq_at_within:
  "eventually (λw. w  x) (at z within A)"
  by (smt (verit, ccfv_threshold) eventually_True eventually_at_topological separation_t1)

lemma (in perfect_space) at_neq_bot [simp]: "at a  bot"
  by (simp add: at_eq_bot_iff not_open_singleton)

lemma (in order_topology) nhds_order:
  "nhds x = inf (INF a{x <..}. principal {..< a}) (INF a{..< x}. principal {a <..})"
proof -
  have 1: "{S  range lessThan  range greaterThan. x  S} =
      (λa. {..< a}) ` {x <..}  (λa. {a <..}) ` {..< x}"
    by auto
  show ?thesis
    by (simp only: nhds_generated_topology[OF open_generated_order] INF_union 1 INF_image comp_def)
qed

lemma (in topological_space) filterlim_at_within_If:
  assumes "filterlim f G (at x within (A  {x. P x}))"
    and "filterlim g G (at x within (A  {x. ¬P x}))"
  shows "filterlim (λx. if P x then f x else g x) G (at x within A)"
proof (rule filterlim_If)
  note assms(1)
  also have "at x within (A  {x. P x}) = inf (nhds x) (principal (A  Collect P - {x}))"
    by (simp add: at_within_def)
  also have "A  Collect P - {x} = (A - {x})  Collect P"
    by blast
  also have "inf (nhds x) (principal ) = inf (at x within A) (principal (Collect P))"
    by (simp add: at_within_def inf_assoc)
  finally show "filterlim f G (inf (at x within A) (principal (Collect P)))" .
next
  note assms(2)
  also have "at x within (A  {x. ¬ P x}) = inf (nhds x) (principal (A  {x. ¬ P x} - {x}))"
    by (simp add: at_within_def)
  also have "A  {x. ¬ P x} - {x} = (A - {x})  {x. ¬ P x}"
    by blast
  also have "inf (nhds x) (principal ) = inf (at x within A) (principal {x. ¬ P x})"
    by (simp add: at_within_def inf_assoc)
  finally show "filterlim g G (inf (at x within A) (principal {x. ¬ P x}))" .
qed

lemma (in topological_space) filterlim_at_If:
  assumes "filterlim f G (at x within {x. P x})"
    and "filterlim g G (at x within {x. ¬P x})"
  shows "filterlim (λx. if P x then f x else g x) G (at x)"
  using assms by (intro filterlim_at_within_If) simp_all
lemma (in linorder_topology) at_within_order:
  assumes "UNIV  {x}"
  shows "at x within s =
    inf (INF a{x <..}. principal ({..< a}  s - {x}))
        (INF a{..< x}. principal ({a <..}  s - {x}))"
proof (cases "{x <..} = {}" "{..< x} = {}" rule: case_split [case_product case_split])
  case True_True
  have "UNIV = {..< x}  {x}  {x <..}"
    by auto
  with assms True_True show ?thesis
    by auto
qed (auto simp del: inf_principal simp: at_within_def nhds_order Int_Diff
      inf_principal[symmetric] INF_inf_const2 inf_sup_aci[where 'a="'a filter"])

lemma (in linorder_topology) at_left_eq:
  "y < x  at_left x = (INF a{..< x}. principal {a <..< x})"
  by (subst at_within_order)
     (auto simp: greaterThan_Int_greaterThan greaterThanLessThan_eq[symmetric] min.absorb2 INF_constant
           intro!: INF_lower2 inf_absorb2)

lemma (in linorder_topology) eventually_at_left:
  "y < x  eventually P (at_left x)  (b<x. y>b. y < x  P y)"
  unfolding at_left_eq
  by (subst eventually_INF_base) (auto simp: eventually_principal Ball_def)

lemma (in linorder_topology) at_right_eq:
  "x < y  at_right x = (INF a{x <..}. principal {x <..< a})"
  by (subst at_within_order)
     (auto simp: lessThan_Int_lessThan greaterThanLessThan_eq[symmetric] max.absorb2 INF_constant Int_commute
           intro!: INF_lower2 inf_absorb1)

lemma (in linorder_topology) eventually_at_right:
  "x < y  eventually P (at_right x)  (b>x. y>x. y < b  P y)"
  unfolding at_right_eq
  by (subst eventually_INF_base) (auto simp: eventually_principal Ball_def)

lemma eventually_at_right_less: "F y in at_right (x::'a::{linorder_topology, no_top}). x < y"
  using gt_ex[of x] eventually_at_right[of x] by auto

lemma trivial_limit_at_right_top: "at_right (top::_::{order_top,linorder_topology}) = bot"
  by (auto simp: filter_eq_iff eventually_at_topological)

lemma trivial_limit_at_left_bot: "at_left (bot::_::{order_bot,linorder_topology}) = bot"
  by (auto simp: filter_eq_iff eventually_at_topological)

lemma trivial_limit_at_left_real [simp]: "¬ trivial_limit (at_left x)"
  for x :: "'a::{no_bot,dense_order,linorder_topology}"
  using lt_ex [of x]
  by safe (auto simp add: trivial_limit_def eventually_at_left dest: dense)

lemma trivial_limit_at_right_real [simp]: "¬ trivial_limit (at_right x)"
  for x :: "'a::{no_top,dense_order,linorder_topology}"
  using gt_ex[of x]
  by safe (auto simp add: trivial_limit_def eventually_at_right dest: dense)

lemma (in linorder_topology) at_eq_sup_left_right: "at x = sup (at_left x) (at_right x)"
  by (auto simp: eventually_at_filter filter_eq_iff eventually_sup
      elim: eventually_elim2 eventually_mono)

lemma (in linorder_topology) eventually_at_split:
  "eventually P (at x)  eventually P (at_left x)  eventually P (at_right x)"
  by (subst at_eq_sup_left_right) (simp add: eventually_sup)

lemma (in order_topology) eventually_at_leftI:
  assumes "x. x  {a<..<b}  P x" "a < b"
  shows   "eventually P (at_left b)"
  using assms unfolding eventually_at_topological by (intro exI[of _ "{a<..}"]) auto

lemma (in order_topology) eventually_at_rightI:
  assumes "x. x  {a<..<b}  P x" "a < b"
  shows   "eventually P (at_right a)"
  using assms unfolding eventually_at_topological by (intro exI[of _ "{..<b}"]) auto

lemma eventually_filtercomap_nhds:
  "eventually P (filtercomap f (nhds x))  (S. open S  x  S  (x. f x  S  P x))"
  unfolding eventually_filtercomap eventually_nhds by auto

lemma eventually_filtercomap_at_topological:
  "eventually P (filtercomap f (at A within B))  
     (S. open S  A  S  (x. f x  S  B - {A}  P x))" (is "?lhs = ?rhs")
  unfolding at_within_def filtercomap_inf eventually_inf_principal filtercomap_principal 
          eventually_filtercomap_nhds eventually_principal by blast

lemma eventually_at_right_field:
  "eventually P (at_right x)  (b>x. y>x. y < b  P y)"
  for x :: "'a::{linordered_field, linorder_topology}"
  using linordered_field_no_ub[rule_format, of x]
  by (auto simp: eventually_at_right)

lemma eventually_at_left_field:
  "eventually P (at_left x)  (b<x. y>b. y < x  P y)"
  for x :: "'a::{linordered_field, linorder_topology}"
  using linordered_field_no_lb[rule_format, of x]
  by (auto simp: eventually_at_left)

lemma filtermap_nhds_eq_imp_filtermap_at_eq: 
  assumes "filtermap f (nhds z) = nhds (f z)"
  assumes "eventually (λx. f x = f z  x = z) (at z)"
  shows   "filtermap f (at z) = at (f z)"
proof (rule filter_eqI)
  fix P :: "'a  bool"
  have "eventually P (filtermap f (at z))  (F x in nhds z. x  z  P (f x))"
    by (simp add: eventually_filtermap eventually_at_filter)
  also have "  (F x in nhds z. f x  f z  P (f x))"
    by (rule eventually_cong [OF assms(2)[unfolded eventually_at_filter]]) auto
  also have "  (F x in filtermap f (nhds z). x  f z  P x)"
    by (simp add: eventually_filtermap)
  also have "filtermap f (nhds z) = nhds (f z)"
    by (rule assms)
  also have "(F x in nhds (f z). x  f z  P x)  (F x in at (f z). P x)"
    by (simp add: eventually_at_filter)
  finally show "eventually P (filtermap f (at z)) = eventually P (at (f z))" .
qed

subsubsection ‹Tendsto›

abbreviation (in topological_space)
  tendsto :: "('b  'a)  'a  'b filter  bool"  (infixr  55)
  where "(f  l) F  filterlim f (nhds l) F"

definition (in t2_space) Lim :: "'f filter  ('f  'a)  'a"
  where "Lim A f = (THE l. (f  l) A)"

lemma (in topological_space) tendsto_eq_rhs: "(f  x) F  x = y  (f  y) F"
  by simp

named_theorems tendsto_intros "introduction rules for tendsto"
setup Global_Theory.add_thms_dynamic (bindingtendsto_eq_intros,
    fn context =>
      Named_Theorems.get (Context.proof_of context) named_theorems‹tendsto_intros›
      |> map_filter (try (fn thm => @{thm tendsto_eq_rhs} OF [thm])))

context topological_space begin

lemma tendsto_def:
   "(f  l) F  (S. open S  l  S  eventually (λx. f x  S) F)"
   unfolding nhds_def filterlim_INF filterlim_principal by auto

lemma tendsto_cong: "(f  c) F  (g  c) F" if "eventually (λx. f x = g x) F"
  by (rule filterlim_cong [OF refl refl that])

lemma tendsto_mono: "F  F'  (f  l) F'  (f  l) F"
  unfolding tendsto_def le_filter_def by fast

lemma tendsto_ident_at [tendsto_intros, simp, intro]: "((λx. x)  a) (at a within s)"
  by (auto simp: tendsto_def eventually_at_topological)

lemma tendsto_const [tendsto_intros, simp, intro]: "((λx. k)  k) F"
  by (simp add: tendsto_def)

lemma filterlim_at:
  "(LIM x F. f x :> at b within s)  eventually (λx. f x  s  f x  b) F  (f  b) F"
  by (simp add: at_within_def filterlim_inf filterlim_principal conj_commute)

lemma (in -)
  assumes "filterlim f (nhds L) F"
  shows tendsto_imp_filterlim_at_right:
          "eventually (λx. f x > L) F  filterlim f (at_right L) F"
    and tendsto_imp_filterlim_at_left:
          "eventually (λx. f x < L) F  filterlim f (at_left L) F"
  using assms by (auto simp: filterlim_at elim: eventually_mono)

lemma  filterlim_at_withinI:
  assumes "filterlim f (nhds c) F"
  assumes "eventually (λx. f x  A - {c}) F"
  shows   "filterlim f (at c within A) F"
  using assms by (simp add: filterlim_at)

lemma filterlim_atI:
  assumes "filterlim f (nhds c) F"
  assumes "eventually (λx. f x  c) F"
  shows   "filterlim f (at c) F"
  using assms by (intro filterlim_at_withinI) simp_all

lemma topological_tendstoI:
  "(S. open S  l  S  eventually (λx. f x  S) F)  (f  l) F"
  by (auto simp: tendsto_def)

lemma topological_tendstoD:
  "(f  l) F  open S  l  S  eventually (λx. f x  S) F"
  by (auto simp: tendsto_def)

lemma tendsto_bot [simp]: "(f  a) bot"
  by (simp add: tendsto_def)

lemma tendsto_eventually: "eventually (λx. f x = l) net  ((λx. f x)  l) net"
  by (rule topological_tendstoI) (auto elim: eventually_mono)

(* Contributed by Dominique Unruh *)
lemma tendsto_principal_singleton[simp]:
  shows "(f  f x) (principal {x})"
  unfolding tendsto_def eventually_principal by simp

end

lemma (in topological_space) filterlim_within_subset:
  "filterlim f l (at x within S)  T  S  filterlim f l (at x within T)"
  by (blast intro: filterlim_mono at_le)

lemmas tendsto_within_subset = filterlim_within_subset

lemma (in order_topology) order_tendsto_iff:
  "(f  x) F  (l<x. eventually (λx. l < f x) F)  (u>x. eventually (λx. f x < u) F)"
  by (auto simp: nhds_order filterlim_inf filterlim_INF filterlim_principal)

lemma (in order_topology) order_tendstoI:
  "(a. a < y  eventually (λx. a < f x) F)  (a. y < a  eventually (λx. f x < a) F) 
    (f  y) F"
  by (auto simp: order_tendsto_iff)

lemma (in order_topology) order_tendstoD:
  assumes "(f  y) F"
  shows "a < y  eventually (λx. a < f x) F"
    and "y < a  eventually (λx. f x < a) F"
  using assms by (auto simp: order_tendsto_iff)

lemma (in linorder_topology) tendsto_max[tendsto_intros]:
  assumes X: "(X  x) net"
    and Y: "(Y  y) net"
  shows "((λx. max (X x) (Y x))  max x y) net"
proof (rule order_tendstoI)
  fix a
  assume "a < max x y"
  then show "eventually (λx. a < max (X x) (Y x)) net"
    using order_tendstoD(1)[OF X, of a] order_tendstoD(1)[OF Y, of a]
    by (auto simp: less_max_iff_disj elim: eventually_mono)
next
  fix a
  assume "max x y < a"
  then show "eventually (λx. max (X x) (Y x) < a) net"
    using order_tendstoD(2)[OF X, of a] order_tendstoD(2)[OF Y, of a]
    by (auto simp: eventually_conj_iff)
qed

lemma (in linorder_topology) tendsto_min[tendsto_intros]:
  assumes X: "(X  x) net"
    and Y: "(Y  y) net"
  shows "((λx. min (X x) (Y x))  min x y) net"
proof (rule order_tendstoI)
  fix a
  assume "a < min x y"
  then show "eventually (λx. a < min (X x) (Y x)) net"
    using order_tendstoD(1)[OF X, of a] order_tendstoD(1)[OF Y, of a]
    by (auto simp: eventually_conj_iff)
next
  fix a
  assume "min x y < a"
  then show "eventually (λx. min (X x) (Y x) < a) net"
    using order_tendstoD(2)[OF X, of a] order_tendstoD(2)[OF Y, of a]
    by (auto simp: min_less_iff_disj elim: eventually_mono)
qed

lemma (in order_topology)
  assumes "a < b"
  shows at_within_Icc_at_right: "at a within {a..b} = at_right a"
    and at_within_Icc_at_left:  "at b within {a..b} = at_left b"
  using order_tendstoD(2)[OF tendsto_ident_at assms, of "{a<..}"]
  using order_tendstoD(1)[OF tendsto_ident_at assms, of "{..<b}"]
  by (auto intro!: order_class.order_antisym filter_leI
      simp: eventually_at_filter less_le
      elim: eventually_elim2)

lemma (in order_topology)
  shows at_within_Ici_at_right: "at a within {a..} = at_right a"
    and at_within_Iic_at_left:  "at a within {..a} = at_left a"
  using order_tendstoD(2)[OF tendsto_ident_at [where s = "{a<..}"]]
  using order_tendstoD(1)[OF tendsto_ident_at[where s = "{..<a}"]]
  by (auto intro!: order_class.order_antisym filter_leI
      simp: eventually_at_filter less_le
      elim: eventually_elim2)

lemma (in order_topology) at_within_Icc_at: "a < x  x < b  at x within {a..b} = at x"
  by (rule at_within_open_subset[where S="{a<..<b}"]) auto

lemma (in t2_space) tendsto_unique:
  assumes "F  bot"
    and "(f  a) F"
    and "(f  b) F"
  shows "a = b"
proof (rule ccontr)
  assume "a  b"
  obtain U V where "open U" "open V" "a  U" "b  V" "U  V = {}"
    using hausdorff [OF a  b] by fast
  have "eventually (λx. f x  U) F"
    using (f  a) F open U a  U by (rule topological_tendstoD)
  moreover
  have "eventually (λx. f x  V) F"
    using (f  b) F open V b  V by (rule topological_tendstoD)
  ultimately
  have "eventually (λx. False) F"
  proof eventually_elim
    case (elim x)
    then have "f x  U  V" by simp
    with U  V = {} show ?case by simp
  qed
  with ¬ trivial_limit F show "False"
    by (simp add: trivial_limit_def)
qed

lemma (in t2_space) tendsto_const_iff:
  fixes a b :: 'a
  assumes "¬ trivial_limit F"
  shows "((λx. a)  b) F  a = b"
  by (auto intro!: tendsto_unique [OF assms tendsto_const])

lemma (in t2_space) tendsto_unique':
 assumes "F  bot"
 shows "1l. (f  l) F"
 using Uniq_def assms local.tendsto_unique by fastforce

lemma Lim_in_closed_set:
  assumes "closed S" "eventually (λx. f(x)  S) F" "F  bot" "(f  l) F"
  shows "l  S"
proof (rule ccontr)
  assume "l  S"
  with closed S have "open (- S)" "l  - S"
    by (simp_all add: open_Compl)
  with assms(4) have "eventually (λx. f x  - S) F"
    by (rule topological_tendstoD)
  with assms(2) have "eventually (λx. False) F"
    by (rule eventually_elim2) simp
  with assms(3) show "False"
    by (simp add: eventually_False)
qed

lemma (in t3_space) nhds_closed:
  assumes "x  A" and "open A"
  shows   "A'. x  A'  closed A'  A'  A  eventually (λy. y  A') (nhds x)"
proof -
  from assms have "U V. open U  open V  x  U  - A  V  U  V = {}"
    by (intro t3_space) auto
  then obtain U V where UV: "open U" "open V" "x  U" "-A  V" "U  V = {}"
    by auto
  have "eventually (λy. y  U) (nhds x)"
    using open U and x  U by (intro eventually_nhds_in_open)
  hence "eventually (λy. y  -V) (nhds x)"
    by eventually_elim (use UV in auto)
  with UV show ?thesis by (intro exI[of _ "-V"]) auto
qed

lemma (in order_topology) increasing_tendsto:
  assumes bdd: "eventually (λn. f n  l) F"
    and en: "x. x < l  eventually (λn. x < f n) F"
  shows "(f  l) F"
  using assms by (intro order_tendstoI) (auto elim!: eventually_mono)

lemma (in order_topology) decreasing_tendsto:
  assumes bdd: "eventually (λn. l  f n) F"
    and en: "x. l < x  eventually (λn. f n < x) F"
  shows "(f  l) F"
  using assms by (intro order_tendstoI) (auto elim!: eventually_mono)

lemma (in order_topology) tendsto_sandwich:
  assumes ev: "eventually (λn. f n  g n) net" "eventually (λn. g n  h n) net"
  assumes lim: "(f  c) net" "(h  c) net"
  shows "(g  c) net"
proof (rule order_tendstoI)
  fix a
  show "a < c  eventually (λx. a < g x) net"
    using order_tendstoD[OF lim(1), of a] ev by (auto elim: eventually_elim2)
next
  fix a
  show "c < a  eventually (λx. g x < a) net"
    using order_tendstoD[OF lim(2), of a] ev by (auto elim: eventually_elim2)
qed

lemma (in t1_space) limit_frequently_eq:
  assumes "F  bot"
    and "frequently (λx. f x = c) F"
    and "(f  d) F"
  shows "d = c"
proof (rule ccontr)
  assume "d  c"
  from t1_space[OF this] obtain U where "open U" "d  U" "c  U"
    by blast
  with assms have "eventually (λx. f x  U) F"
    unfolding tendsto_def by blast
  then have "eventually (λx. f x  c) F"
    by eventually_elim (insert c  U, blast)
  with assms(2) show False
    unfolding frequently_def by contradiction
qed

lemma (in t1_space) tendsto_imp_eventually_ne:
  assumes  "(f  c) F" "c  c'"
  shows "eventually (λz. f z  c') F"
proof (cases "F=bot")
  case True
  thus ?thesis by auto
next
  case False
  show ?thesis
  proof (rule ccontr)
    assume "¬ eventually (λz. f z  c') F"
    then have "frequently (λz. f z = c') F"
      by (simp add: frequently_def)
    from limit_frequently_eq[OF False this (f  c) F] and c  c' show False
      by contradiction
  qed
qed

lemma (in linorder_topology) tendsto_le:
  assumes F: "¬ trivial_limit F"
    and x: "(f  x) F"
    and y: "(g  y) F"
    and ev: "eventually (λx. g x  f x) F"
  shows "y  x"
proof (rule ccontr)
  assume "¬ y  x"
  with less_separate[of x y] obtain a b where xy: "x < a" "b < y" "{..<a}  {b<..} = {}"
    by (auto simp: not_le)
  then have "eventually (λx. f x < a) F" "eventually (λx. b < g x) F"
    using x y by (auto intro: order_tendstoD)
  with ev have "eventually (λx. False) F"
    by eventually_elim (insert xy, fastforce)
  with F show False
    by (simp add: eventually_False)
qed

lemma (in linorder_topology) tendsto_lowerbound:
  assumes x: "(f  x) F"
      and ev: "eventually (λi. a  f i) F"
      and F: "¬ trivial_limit F"
  shows "a  x"
  using F x tendsto_const ev by (rule tendsto_le)

lemma (in linorder_topology) tendsto_upperbound:
  assumes x: "(f  x) F"
      and ev: "eventually (λi. a  f i) F"
      and F: "¬ trivial_limit F"
  shows "a  x"
  by (rule tendsto_le [OF F tendsto_const x ev])

lemma filterlim_at_within_not_equal:
  fixes f::"'a  'b::t2_space"
  assumes "filterlim f (at a within s) F"
  shows "eventually (λw. f ws  f w b) F"
proof (cases "a=b")
  case True
  then show ?thesis using assms by (simp add: filterlim_at)
next
  case False
  from hausdorff[OF this] obtain U V where UV:"open U" "open V" "a  U" "b  V" "U  V = {}"
    by auto  
  have "(f  a) F" using assms filterlim_at by auto
  then have "F x in F. f x  U" using UV unfolding tendsto_def by auto
  moreover have  "F x in F. f x  s  f xa" using assms filterlim_at by auto
  ultimately show ?thesis 
    apply eventually_elim
    using UV by auto
qed

subsubsection ‹Rules about constLim

lemma tendsto_Lim: "¬ trivial_limit net  (f  l) net  Lim net f = l"
  unfolding Lim_def using tendsto_unique [of net f] by auto

lemma Lim_ident_at: "¬ trivial_limit (at x within s)  Lim (at x within s) (λx. x) = x"
  by (simp add: tendsto_Lim)

lemma Lim_cong:
  assumes "F x in F. f x = g x" "F = G"
  shows "Lim F f = Lim F g"
  unfolding t2_space_class.Lim_def using tendsto_cong assms by fastforce

lemma eventually_Lim_ident_at:
  "(F y in at x within X. P (Lim (at x within X) (λx. x)) y) 
    (F y in at x within X. P x y)" for x::"'a::t2_space"
  by (cases "at x within X = bot") (auto simp: Lim_ident_at)

lemma filterlim_at_bot_at_right:
  fixes f :: "'a::linorder_topology  'b::linorder"
  assumes mono: "x y. Q x  Q y  x  y  f x  f y"
    and bij: "x. P x  f (g x) = x" "x. P x  Q (g x)"
    and Q: "eventually Q (at_right a)"
    and bound: "b. Q b  a < b"
    and P: "eventually P at_bot"
  shows "filterlim f at_bot (at_right a)"
proof -
  from P obtain x where x: "y. y  x  P y"
    unfolding eventually_at_bot_linorder by auto
  show ?thesis
  proof (intro filterlim_at_bot_le[THEN iffD2] allI impI)
    fix z
    assume "z  x"
    with x have "P z" by auto
    have "eventually (λx. x  g z) (at_right a)"
      using bound[OF bij(2)[OF P z]]
      unfolding eventually_at_right[OF bound[OF bij(2)[OF P z]]]
      by (auto intro!: exI[of _ "g z"])
    with Q show "eventually (λx. f x  z) (at_right a)"
      by eventually_elim (metis bij P z mono)
  qed
qed

lemma filterlim_at_top_at_left:
  fixes f :: "'a::linorder_topology  'b::linorder"
  assumes mono: "x y. Q x  Q y  x  y  f x  f y"
    and bij: "x. P x  f (g x) = x" "x. P x  Q (g x)"
    and Q: "eventually Q (at_left a)"
    and bound: "b. Q b  b < a"
    and P: "eventually P at_top"
  shows "filterlim f at_top (at_left a)"
proof -
  from P obtain x where x: "y. x  y  P y"
    unfolding eventually_at_top_linorder by auto
  show ?thesis
  proof (intro filterlim_at_top_ge[THEN iffD2] allI impI)
    fix z
    assume "x  z"
    with x have "P z" by auto
    have "eventually (λx. g z  x) (at_left a)"
      using bound[OF bij(2)[OF P z]]
      unfolding eventually_at_left[OF bound[OF bij(2)[OF P z]]]
      by (auto intro!: exI[of _ "g z"])
    with Q show "eventually (λx. z  f x) (at_left a)"
      by eventually_elim (metis bij P z mono)
  qed
qed

lemma filterlim_split_at:
  "filterlim f F (at_left x)  filterlim f F (at_right x) 
    filterlim f F (at x)"
  for x :: "'a::linorder_topology"
  by (subst at_eq_sup_left_right) (rule filterlim_sup)

lemma filterlim_at_split:
  "filterlim f F (at x)  filterlim f F (at_left x)  filterlim f F (at_right x)"
  for x :: "'a::linorder_topology"
  by (subst at_eq_sup_left_right) (simp add: filterlim_def filtermap_sup)

lemma eventually_nhds_top:
  fixes P :: "'a :: {order_top,linorder_topology}  bool"
    and b :: 'a
  assumes "b < top"
  shows "eventually P (nhds top)  (b<top. (z. b < z  P z))"
  unfolding eventually_nhds
proof safe
  fix S :: "'a set"
  assume "open S" "top  S"
  note open_left[OF this b < top]
  moreover assume "sS. P s"
  ultimately show "b<top. z>b. P z"
    by (auto simp: subset_eq Ball_def)
next
  fix b
  assume "b < top" "z>b. P z"
  then show "S. open S  top  S  (xaS. P xa)"
    by (intro exI[of _ "{b <..}"]) auto
qed

lemma tendsto_at_within_iff_tendsto_nhds:
  "(g  g l) (at l within S)  (g  g l) (inf (nhds l) (principal S))"
  unfolding tendsto_def eventually_at_filter eventually_inf_principal
  by (intro ext all_cong imp_cong) (auto elim!: eventually_mono)


subsection ‹Limits on sequences›

abbreviation (in topological_space)
  LIMSEQ :: "[nat  'a, 'a]  bool"  ((‹notation=‹infix LIMSEQ››(_)/  (_)) [60, 60] 60)
  where "X  L  (X  L) sequentially"

abbreviation (in t2_space) lim :: "(nat  'a)  'a"
  where "lim X  Lim sequentially X"

definition (in topological_space) convergent :: "(nat  'a)  bool"
  where "convergent X = (L. X  L)"

lemma lim_def: "lim X = (THE L. X  L)"
  unfolding Lim_def ..

lemma lim_explicit:
  "f  f0  (S. open S  f0  S  (N. nN. f n  S))"
  unfolding tendsto_def eventually_sequentially by auto

lemma closed_sequentially:
  assumes "closed S" and "n. f n  S" and "f  l"
  shows "l  S"
  by (metis Lim_in_closed_set assms eventually_sequentially trivial_limit_sequentially)


subsection ‹Monotone sequences and subsequences›

text ‹
  Definition of monotonicity.
  The use of disjunction here complicates proofs considerably.
  One alternative is to add a Boolean argument to indicate the direction.
  Another is to develop the notions of increasing and decreasing first.
›
definition monoseq :: "(nat  'a::order)  bool"
  where "monoseq X  (m. nm. X m  X n)  (m. nm. X n  X m)"

abbreviation incseq :: "(nat  'a::order)  bool"
  where "incseq X  mono X"

lemma incseq_def: "incseq X  (m. nm. X n  X m)"
  unfolding mono_def ..

abbreviation decseq :: "(nat  'a::order)  bool"
  where "decseq X  antimono X"

lemma decseq_def: "decseq X  (m. nm. X n  X m)"
  unfolding antimono_def ..

subsubsection ‹Definition of subsequence.›

(* For compatibility with the old "subseq" *)
lemma strict_mono_leD: "strict_mono r  m  n  r m  r n"
  by (erule (1) monoD [OF strict_mono_mono])

lemma strict_mono_id: "strict_mono id"
  by (simp add: strict_mono_def)

lemma incseq_SucI: "(n. X n  X (Suc n))  incseq X"
  by (simp add: mono_iff_le_Suc)

lemma incseqD: "incseq f  i  j  f i  f j"
  by (auto simp: incseq_def)

lemma incseq_SucD: "incseq A  A i  A (Suc i)"
  using incseqD[of A i "Suc i"] by auto

lemma incseq_Suc_iff: "incseq f  (n. f n  f (Suc n))"
  by (auto intro: incseq_SucI dest: incseq_SucD)

lemma incseq_const[simp, intro]: "incseq (λx. k)"
  unfolding incseq_def by auto

lemma decseq_SucI: "(n. X (Suc n)  X n)  decseq X"
  by (simp add: antimono_iff_le_Suc)

lemma decseqD: "decseq f  i  j  f j  f i"
  by (auto simp: decseq_def)

lemma decseq_SucD: "decseq A  A (Suc i)  A i"
  using decseqD[of A i "Suc i"] by auto

lemma decseq_Suc_iff: "decseq f  (n. f (Suc n)  f n)"
  by (auto intro: decseq_SucI dest: decseq_SucD)

lemma decseq_const[simp, intro]: "decseq (λx. k)"
  unfolding decseq_def by auto

lemma monoseq_iff: "monoseq X  incseq X  decseq X"
  unfolding monoseq_def incseq_def decseq_def ..

lemma monoseq_Suc: "monoseq X  (n. X n  X (Suc n))  (n. X (Suc n)  X n)"
  unfolding monoseq_iff incseq_Suc_iff decseq_Suc_iff ..

lemma monoI1: "m. n  m. X m  X n  monoseq X"
  by (simp add: monoseq_def)

lemma monoI2: "m. n  m. X n  X m  monoseq X"
  by (simp add: monoseq_def)

lemma mono_SucI1: "n. X n  X (Suc n)  monoseq X"
  by (simp add: monoseq_Suc)

lemma mono_SucI2: "n. X (Suc n)  X n  monoseq X"
  by (simp add: monoseq_Suc)

lemma monoseq_minus:
  fixes a :: "nat  'a::ordered_ab_group_add"
  assumes "monoseq a"
  shows "monoseq (λ n. - a n)"
proof (cases "m. n  m. a m  a n")
  case True
  then have "m. n  m. - a n  - a m" by auto
  then show ?thesis by (rule monoI2)
next
  case False
  then have "m. n  m. - a m  - a n"
    using monoseq a[unfolded monoseq_def] by auto
  then show ?thesis by (rule monoI1)
qed


subsubsection ‹Subsequence (alternative definition, (e.g. Hoskins)›

text ‹For any sequence, there is a monotonic subsequence.›
lemma seq_monosub:
  fixes s :: "nat  'a::linorder"
  shows "f. strict_mono f  monoseq (λn. (s (f n)))"
proof (cases "n. p>n. mp. s m  s p")
  case True
  then have "f. n. (mf n. s m  s (f n))  f n < f (Suc n)"
    by (intro dependent_nat_choice) (auto simp: conj_commute)
  then obtain f :: "nat  nat" 
    where f: "strict_mono f" and mono: "n m. f n  m  s m  s (f n)"
    by (auto simp: strict_mono_Suc_iff)
  then have "incseq f"
    unfolding strict_mono_Suc_iff incseq_Suc_iff by (auto intro: less_imp_le)
  then have "monoseq (λn. s (f n))"
    by (auto simp add: incseq_def intro!: mono monoI2)
  with f show ?thesis
    by auto
next
  case False
  then obtain N where N: "p > N  m>p. s p < s m" for p
    by (force simp: not_le le_less)
  have "f. n. N < f n  f n < f (Suc n)  s (f n)  s (f (Suc n))"
  proof (intro dependent_nat_choice)
    fix x
    assume "N < x" with N[of x]
    show "y>N. x < y  s x  s y"
      by (auto intro: less_trans)
  qed auto
  then show ?thesis
    by (auto simp: monoseq_iff incseq_Suc_iff strict_mono_Suc_iff)
qed

lemma seq_suble:
  assumes sf: "strict_mono (f :: nat  nat)"
  shows "n  f n"
proof (induct n)
  case 0
  show ?case by simp
next
  case (Suc n)
  with sf [unfolded strict_mono_Suc_iff, rule_format, of n] have "n < f (Suc n)"
     by arith
  then show ?case by arith
qed

lemma eventually_subseq:
  "strict_mono r  eventually P sequentially  eventually (λn. P (r n)) sequentially"
  unfolding eventually_sequentially by (metis seq_suble le_trans)

lemma not_eventually_sequentiallyD:
  assumes "¬ eventually P sequentially"
  shows "r::natnat. strict_mono r  (n. ¬ P (r n))"
proof -
  from assms have "n. mn. ¬ P m"
    unfolding eventually_sequentially by (simp add: not_less)
  then obtain r where "n. r n  n" "n. ¬ P (r n)"
    by (auto simp: choice_iff)
  then show ?thesis
    by (auto intro!: exI[of _ "λn. r (((Suc  r) ^^ Suc n) 0)"]
             simp: less_eq_Suc_le strict_mono_Suc_iff)
qed

lemma sequentially_offset: 
  assumes "eventually (λi. P i) sequentially"
  shows "eventually (λi. P (i + k)) sequentially"
  using assms by (rule eventually_sequentially_seg [THEN iffD2])

lemma seq_offset_neg: 
  "(f  l) sequentially  ((λi. f(i - k))  l) sequentially"
  apply (erule filterlim_compose)
  apply (simp add: filterlim_def le_sequentially eventually_filtermap eventually_sequentially, arith)
  done

lemma