(*  Title:      HOL/Topological_Spaces.thy

    Author:     Brian Huffman

    Author:     Johannes Hölzl

*)

header {* Topological Spaces *}

theory Topological_Spaces

imports Main Conditionally_Complete_Lattices

begin

subsection {* Topological space *}

class "open" =

  fixes "open" :: "'a set \<Rightarrow> bool"

class topological_space = "open" +

  assumes open_UNIV [simp, intro]: "open UNIV"

  assumes open_Int [intro]: "open S \<Longrightarrow> open T \<Longrightarrow> open (S \<inter> T)"

  assumes open_Union [intro]: "\<forall>S\<in>K. open S \<Longrightarrow> open (\<Union> K)"

begin

definition

  closed :: "'a set \<Rightarrow> bool" where

  "closed S \<longleftrightarrow> open (- S)"

lemma open_empty [intro, simp]: "open {}"

  using open_Union [of "{}"] by simp

lemma open_Un [intro]: "open S \<Longrightarrow> open T \<Longrightarrow> open (S \<union> T)"

  using open_Union [of "{S, T}"] by simp

lemma open_UN [intro]: "\<forall>x\<in>A. open (B x) \<Longrightarrow> open (\<Union>x\<in>A. B x)"

  unfolding SUP_def by (rule open_Union) auto

lemma open_Inter [intro]: "finite S \<Longrightarrow> \<forall>T\<in>S. open T \<Longrightarrow> open (\<Inter>S)"

  by (induct set: finite) auto

lemma open_INT [intro]: "finite A \<Longrightarrow> \<forall>x\<in>A. open (B x) \<Longrightarrow> open (\<Inter>x\<in>A. B x)"

  unfolding INF_def by (rule open_Inter) auto

lemma openI:

  assumes "\<And>x. x \<in> S \<Longrightarrow> \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> S"

  shows "open S"

proof -

  have "open (\<Union>{T. open T \<and> T \<subseteq> S})" by auto

  moreover have "\<Union>{T. open T \<and> T \<subseteq> S} = S" by (auto dest!: assms)

  ultimately show "open S" by simp

qed

lemma closed_empty [intro, simp]:  "closed {}"

  unfolding closed_def by simp

lemma closed_Un [intro]: "closed S \<Longrightarrow> closed T \<Longrightarrow> closed (S \<union> T)"

  unfolding closed_def by auto

lemma closed_UNIV [intro, simp]: "closed UNIV"

  unfolding closed_def by simp

lemma closed_Int [intro]: "closed S \<Longrightarrow> closed T \<Longrightarrow> closed (S \<inter> T)"

  unfolding closed_def by auto

lemma closed_INT [intro]: "\<forall>x\<in>A. closed (B x) \<Longrightarrow> closed (\<Inter>x\<in>A. B x)"

  unfolding closed_def by auto

lemma closed_Inter [intro]: "\<forall>S\<in>K. closed S \<Longrightarrow> closed (\<Inter> K)"

  unfolding closed_def uminus_Inf by auto

lemma closed_Union [intro]: "finite S \<Longrightarrow> \<forall>T\<in>S. closed T \<Longrightarrow> closed (\<Union>S)"

  by (induct set: finite) auto

lemma closed_UN [intro]: "finite A \<Longrightarrow> \<forall>x\<in>A. closed (B x) \<Longrightarrow> closed (\<Union>x\<in>A. B x)"

  unfolding SUP_def by (rule closed_Union) auto

lemma open_closed: "open S \<longleftrightarrow> closed (- S)"

  unfolding closed_def by simp

lemma closed_open: "closed S \<longleftrightarrow> open (- S)"

  unfolding closed_def by simp

lemma open_Diff [intro]: "open S \<Longrightarrow> closed T \<Longrightarrow> open (S - T)"

  unfolding closed_open Diff_eq by (rule open_Int)

lemma closed_Diff [intro]: "closed S \<Longrightarrow> open T \<Longrightarrow> closed (S - T)"

  unfolding open_closed Diff_eq by (rule closed_Int)

lemma open_Compl [intro]: "closed S \<Longrightarrow> open (- S)"

  unfolding closed_open .

lemma closed_Compl [intro]: "open S \<Longrightarrow> closed (- S)"

  unfolding open_closed .

end

subsection{* Hausdorff and other separation properties *}

class t0_space = topological_space +

  assumes t0_space: "x \<noteq> y \<Longrightarrow> \<exists>U. open U \<and> \<not> (x \<in> U \<longleftrightarrow> y \<in> U)"

class t1_space = topological_space +

  assumes t1_space: "x \<noteq> y \<Longrightarrow> \<exists>U. open U \<and> x \<in> U \<and> y \<notin> U"

instance t1_space \<subseteq> t0_space

proof qed (fast dest: t1_space)

lemma separation_t1:

  fixes x y :: "'a::t1_space"

  shows "x \<noteq> y \<longleftrightarrow> (\<exists>U. open U \<and> x \<in> U \<and> y \<notin> U)"

  using t1_space[of x y] by blast

lemma closed_singleton:

  fixes a :: "'a::t1_space"

  shows "closed {a}"

proof -

  let ?T = "\<Union>{S. open S \<and> a \<notin> S}"

  have "open ?T" by (simp add: open_Union)

  also have "?T = - {a}"

    by (simp add: set_eq_iff separation_t1, auto)

  finally show "closed {a}" unfolding closed_def .

qed

lemma closed_insert [simp]:

  fixes a :: "'a::t1_space"

  assumes "closed S" shows "closed (insert a S)"

proof -

  from closed_singleton assms

  have "closed ({a} \<union> S)" by (rule closed_Un)

  thus "closed (insert a S)" by simp

qed

lemma finite_imp_closed:

  fixes S :: "'a::t1_space set"

  shows "finite S \<Longrightarrow> closed S"

by (induct set: finite, simp_all)

text {* T2 spaces are also known as Hausdorff spaces. *}

class t2_space = topological_space +

  assumes hausdorff: "x \<noteq> y \<Longrightarrow> \<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {}"

instance t2_space \<subseteq> t1_space

proof qed (fast dest: hausdorff)

lemma separation_t2:

  fixes x y :: "'a::t2_space"

  shows "x \<noteq> y \<longleftrightarrow> (\<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {})"

  using hausdorff[of x y] by blast

lemma separation_t0:

  fixes x y :: "'a::t0_space"

  shows "x \<noteq> y \<longleftrightarrow> (\<exists>U. open U \<and> ~(x\<in>U \<longleftrightarrow> y\<in>U))"

  using t0_space[of x y] by blast

text {* A perfect space is a topological space with no isolated points. *}

class perfect_space = topological_space +

  assumes not_open_singleton: "\<not> open {x}"

subsection {* Generators for toplogies *}

inductive generate_topology for S where

  UNIV: "generate_topology S UNIV"

| Int: "generate_topology S a \<Longrightarrow> generate_topology S b \<Longrightarrow> generate_topology S (a \<inter> b)"

| UN: "(\<And>k. k \<in> K \<Longrightarrow> generate_topology S k) \<Longrightarrow> generate_topology S (\<Union>K)"

| Basis: "s \<in> S \<Longrightarrow> generate_topology S s"

hide_fact (open) UNIV Int UN Basis 

lemma generate_topology_Union: 

  "(\<And>k. k \<in> I \<Longrightarrow> generate_topology S (K k)) \<Longrightarrow> generate_topology S (\<Union>k\<in>I. K k)"

  unfolding SUP_def by (intro generate_topology.UN) auto

lemma topological_space_generate_topology:

  "class.topological_space (generate_topology S)"

  by default (auto intro: generate_topology.intros)

subsection {* Order topologies *}

class order_topology = order + "open" +

  assumes open_generated_order: "open = generate_topology (range (\<lambda>a. {..< a}) \<union> range (\<lambda>a. {a <..}))"

begin

subclass topological_space

  unfolding open_generated_order

  by (rule topological_space_generate_topology)

lemma open_greaterThan [simp]: "open {a <..}"

  unfolding open_generated_order by (auto intro: generate_topology.Basis)

lemma open_lessThan [simp]: "open {..< a}"

  unfolding open_generated_order by (auto intro: generate_topology.Basis)

lemma open_greaterThanLessThan [simp]: "open {a <..< b}"

   unfolding greaterThanLessThan_eq by (simp add: open_Int)

end

class linorder_topology = linorder + order_topology

lemma closed_atMost [simp]: "closed {.. a::'a::linorder_topology}"

  by (simp add: closed_open)

lemma closed_atLeast [simp]: "closed {a::'a::linorder_topology ..}"

  by (simp add: closed_open)

lemma closed_atLeastAtMost [simp]: "closed {a::'a::linorder_topology .. b}"

proof -

  have "{a .. b} = {a ..} \<inter> {.. b}"

    by auto

  then show ?thesis

    by (simp add: closed_Int)

qed

lemma (in linorder) less_separate:

  assumes "x < y"

  shows "\<exists>a b. x \<in> {..< a} \<and> y \<in> {b <..} \<and> {..< a} \<inter> {b <..} = {}"

proof (cases "\<exists>z. x < z \<and> z < y")

  case True

  then obtain z where "x < z \<and> z < y" ..

  then have "x \<in> {..< z} \<and> y \<in> {z <..} \<and> {z <..} \<inter> {..< z} = {}"

    by auto

  then show ?thesis by blast

next

  case False

  with `x < y` have "x \<in> {..< y} \<and> y \<in> {x <..} \<and> {x <..} \<inter> {..< y} = {}"

    by auto

  then show ?thesis by blast

qed

instance linorder_topology \<subseteq> t2_space

proof

  fix x y :: 'a

  from less_separate[of x y] less_separate[of y x]

  show "x \<noteq> y \<Longrightarrow> \<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {}"

    by (elim neqE) (metis open_lessThan open_greaterThan Int_commute)+

qed

lemma (in linorder_topology) open_right:

  assumes "open S" "x \<in> S" and gt_ex: "x < y" shows "\<exists>b>x. {x ..< b} \<subseteq> S"

  using assms unfolding open_generated_order

proof induction

  case (Int A B)

  then obtain a b where "a > x" "{x ..< a} \<subseteq> A"  "b > x" "{x ..< b} \<subseteq> B" by auto

  then show ?case by (auto intro!: exI[of _ "min a b"])

next

  case (Basis S) then show ?case by (fastforce intro: exI[of _ y] gt_ex)

qed blast+

lemma (in linorder_topology) open_left:

  assumes "open S" "x \<in> S" and lt_ex: "y < x" shows "\<exists>b<x. {b <.. x} \<subseteq> S"

  using assms unfolding open_generated_order

proof induction

  case (Int A B)

  then obtain a b where "a < x" "{a <.. x} \<subseteq> A"  "b < x" "{b <.. x} \<subseteq> B" by auto

  then show ?case by (auto intro!: exI[of _ "max a b"])

next

  case (Basis S) then show ?case by (fastforce intro: exI[of _ y] lt_ex)

qed blast+

subsection {* Filters *}

text {*

  This definition also allows non-proper filters.

*}

locale is_filter =

  fixes F :: "('a \<Rightarrow> bool) \<Rightarrow> bool"

  assumes True: "F (\<lambda>x. True)"

  assumes conj: "F (\<lambda>x. P x) \<Longrightarrow> F (\<lambda>x. Q x) \<Longrightarrow> F (\<lambda>x. P x \<and> Q x)"

  assumes mono: "\<forall>x. P x \<longrightarrow> Q x \<Longrightarrow> F (\<lambda>x. P x) \<Longrightarrow> F (\<lambda>x. Q x)"

typedef 'a filter = "{F :: ('a \<Rightarrow> bool) \<Rightarrow> bool. is_filter F}"

proof

  show "(\<lambda>x. True) \<in> ?filter" by (auto intro: is_filter.intro)

qed

lemma is_filter_Rep_filter: "is_filter (Rep_filter F)"

  using Rep_filter [of F] by simp

lemma Abs_filter_inverse':

  assumes "is_filter F" shows "Rep_filter (Abs_filter F) = F"

  using assms by (simp add: Abs_filter_inverse)

subsubsection {* Eventually *}

definition eventually :: "('a \<Rightarrow> bool) \<Rightarrow> 'a filter \<Rightarrow> bool"

  where "eventually P F \<longleftrightarrow> Rep_filter F P"

lemma eventually_Abs_filter:

  assumes "is_filter F" shows "eventually P (Abs_filter F) = F P"

  unfolding eventually_def using assms by (simp add: Abs_filter_inverse)

lemma filter_eq_iff:

  shows "F = F' \<longleftrightarrow> (\<forall>P. eventually P F = eventually P F')"

  unfolding Rep_filter_inject [symmetric] fun_eq_iff eventually_def ..

lemma eventually_True [simp]: "eventually (\<lambda>x. True) F"

  unfolding eventually_def

  by (rule is_filter.True [OF is_filter_Rep_filter])

lemma always_eventually: "\<forall>x. P x \<Longrightarrow> eventually P F"

proof -

  assume "\<forall>x. P x" hence "P = (\<lambda>x. True)" by (simp add: ext)

  thus "eventually P F" by simp

qed

lemma eventually_mono:

  "(\<forall>x. P x \<longrightarrow> Q x) \<Longrightarrow> eventually P F \<Longrightarrow> eventually Q F"

  unfolding eventually_def

  by (rule is_filter.mono [OF is_filter_Rep_filter])

lemma eventually_conj:

  assumes P: "eventually (\<lambda>x. P x) F"

  assumes Q: "eventually (\<lambda>x. Q x) F"

  shows "eventually (\<lambda>x. P x \<and> Q x) F"

  using assms unfolding eventually_def

  by (rule is_filter.conj [OF is_filter_Rep_filter])

lemma eventually_Ball_finite:

  assumes "finite A" and "\<forall>y\<in>A. eventually (\<lambda>x. P x y) net"

  shows "eventually (\<lambda>x. \<forall>y\<in>A. P x y) net"

using assms by (induct set: finite, simp, simp add: eventually_conj)

lemma eventually_all_finite:

  fixes P :: "'a \<Rightarrow> 'b::finite \<Rightarrow> bool"

  assumes "\<And>y. eventually (\<lambda>x. P x y) net"

  shows "eventually (\<lambda>x. \<forall>y. P x y) net"

using eventually_Ball_finite [of UNIV P] assms by simp

lemma eventually_mp:

  assumes "eventually (\<lambda>x. P x \<longrightarrow> Q x) F"

  assumes "eventually (\<lambda>x. P x) F"

  shows "eventually (\<lambda>x. Q x) F"

proof (rule eventually_mono)

  show "\<forall>x. (P x \<longrightarrow> Q x) \<and> P x \<longrightarrow> Q x" by simp

  show "eventually (\<lambda>x. (P x \<longrightarrow> Q x) \<and> P x) F"

    using assms by (rule eventually_conj)

qed

lemma eventually_rev_mp:

  assumes "eventually (\<lambda>x. P x) F"

  assumes "eventually (\<lambda>x. P x \<longrightarrow> Q x) F"

  shows "eventually (\<lambda>x. Q x) F"

using assms(2) assms(1) by (rule eventually_mp)

lemma eventually_conj_iff:

  "eventually (\<lambda>x. P x \<and> Q x) F \<longleftrightarrow> eventually P F \<and> eventually Q F"

  by (auto intro: eventually_conj elim: eventually_rev_mp)

lemma eventually_elim1:

  assumes "eventually (\<lambda>i. P i) F"

  assumes "\<And>i. P i \<Longrightarrow> Q i"

  shows "eventually (\<lambda>i. Q i) F"

  using assms by (auto elim!: eventually_rev_mp)

lemma eventually_elim2:

  assumes "eventually (\<lambda>i. P i) F"

  assumes "eventually (\<lambda>i. Q i) F"

  assumes "\<And>i. P i \<Longrightarrow> Q i \<Longrightarrow> R i"

  shows "eventually (\<lambda>i. R i) F"

  using assms by (auto elim!: eventually_rev_mp)

lemma eventually_subst:

  assumes "eventually (\<lambda>n. P n = Q n) F"

  shows "eventually P F = eventually Q F" (is "?L = ?R")

proof -

  from assms have "eventually (\<lambda>x. P x \<longrightarrow> Q x) F"

      and "eventually (\<lambda>x. Q x \<longrightarrow> P x) F"

    by (auto elim: eventually_elim1)

  then show ?thesis by (auto elim: eventually_elim2)

qed

ML {*

  fun eventually_elim_tac ctxt thms thm =

    let

      val thy = Proof_Context.theory_of ctxt

      val mp_thms = thms RL [@{thm eventually_rev_mp}]

      val raw_elim_thm =

        (@{thm allI} RS @{thm always_eventually})

        |> fold (fn thm1 => fn thm2 => thm2 RS thm1) mp_thms

        |> fold (fn _ => fn thm => @{thm impI} RS thm) thms

      val cases_prop = prop_of (raw_elim_thm RS thm)

      val cases = (Rule_Cases.make_common (thy, cases_prop) [(("elim", []), [])])

    in

      CASES cases (rtac raw_elim_thm 1) thm

    end

*}

method_setup eventually_elim = {*

  Scan.succeed (fn ctxt => METHOD_CASES (eventually_elim_tac ctxt))

*} "elimination of eventually quantifiers"

subsubsection {* Finer-than relation *}

text {* @{term "F \<le> F'"} means that filter @{term F} is finer than

filter @{term F'}. *}

instantiation filter :: (type) complete_lattice

begin

definition le_filter_def:

  "F \<le> F' \<longleftrightarrow> (\<forall>P. eventually P F' \<longrightarrow> eventually P F)"

definition

  "(F :: 'a filter) < F' \<longleftrightarrow> F \<le> F' \<and> \<not> F' \<le> F"

definition

  "top = Abs_filter (\<lambda>P. \<forall>x. P x)"

definition

  "bot = Abs_filter (\<lambda>P. True)"

definition

  "sup F F' = Abs_filter (\<lambda>P. eventually P F \<and> eventually P F')"

definition

  "inf F F' = Abs_filter

      (\<lambda>P. \<exists>Q R. eventually Q F \<and> eventually R F' \<and> (\<forall>x. Q x \<and> R x \<longrightarrow> P x))"

definition

  "Sup S = Abs_filter (\<lambda>P. \<forall>F\<in>S. eventually P F)"

definition

  "Inf S = Sup {F::'a filter. \<forall>F'\<in>S. F \<le> F'}"

lemma eventually_top [simp]: "eventually P top \<longleftrightarrow> (\<forall>x. P x)"

  unfolding top_filter_def

  by (rule eventually_Abs_filter, rule is_filter.intro, auto)

lemma eventually_bot [simp]: "eventually P bot"

  unfolding bot_filter_def

  by (subst eventually_Abs_filter, rule is_filter.intro, auto)

lemma eventually_sup:

  "eventually P (sup F F') \<longleftrightarrow> eventually P F \<and> eventually P F'"

  unfolding sup_filter_def

  by (rule eventually_Abs_filter, rule is_filter.intro)

     (auto elim!: eventually_rev_mp)

lemma eventually_inf:

  "eventually P (inf F F') \<longleftrightarrow>

   (\<exists>Q R. eventually Q F \<and> eventually R F' \<and> (\<forall>x. Q x \<and> R x \<longrightarrow> P x))"

  unfolding inf_filter_def

  apply (rule eventually_Abs_filter, rule is_filter.intro)

  apply (fast intro: eventually_True)

  apply clarify

  apply (intro exI conjI)

  apply (erule (1) eventually_conj)

  apply (erule (1) eventually_conj)

  apply simp

  apply auto

  done

lemma eventually_Sup:

  "eventually P (Sup S) \<longleftrightarrow> (\<forall>F\<in>S. eventually P F)"

  unfolding Sup_filter_def

  apply (rule eventually_Abs_filter, rule is_filter.intro)

  apply (auto intro: eventually_conj elim!: eventually_rev_mp)

  done

instance proof

  fix F F' F'' :: "'a filter" and S :: "'a filter set"

  { show "F < F' \<longleftrightarrow> F \<le> F' \<and> \<not> F' \<le> F"

    by (rule less_filter_def) }

  { show "F \<le> F"

    unfolding le_filter_def by simp }

  { assume "F \<le> F'" and "F' \<le> F''" thus "F \<le> F''"

    unfolding le_filter_def by simp }

  { assume "F \<le> F'" and "F' \<le> F" thus "F = F'"

    unfolding le_filter_def filter_eq_iff by fast }

  { show "inf F F' \<le> F" and "inf F F' \<le> F'"

    unfolding le_filter_def eventually_inf by (auto intro: eventually_True) }

  { assume "F \<le> F'" and "F \<le> F''" thus "F \<le> inf F' F''"

    unfolding le_filter_def eventually_inf

    by (auto elim!: eventually_mono intro: eventually_conj) }

  { show "F \<le> sup F F'" and "F' \<le> sup F F'"

    unfolding le_filter_def eventually_sup by simp_all }

  { assume "F \<le> F''" and "F' \<le> F''" thus "sup F F' \<le> F''"

    unfolding le_filter_def eventually_sup by simp }

  { assume "F'' \<in> S" thus "Inf S \<le> F''"

    unfolding le_filter_def Inf_filter_def eventually_Sup Ball_def by simp }

  { assume "\<And>F'. F' \<in> S \<Longrightarrow> F \<le> F'" thus "F \<le> Inf S"

    unfolding le_filter_def Inf_filter_def eventually_Sup Ball_def by simp }

  { assume "F \<in> S" thus "F \<le> Sup S"

    unfolding le_filter_def eventually_Sup by simp }

  { assume "\<And>F. F \<in> S \<Longrightarrow> F \<le> F'" thus "Sup S \<le> F'"

    unfolding le_filter_def eventually_Sup by simp }

  { show "Inf {} = (top::'a filter)"

    by (auto simp: top_filter_def Inf_filter_def Sup_filter_def)

      (metis (full_types) top_filter_def always_eventually eventually_top) }

  { show "Sup {} = (bot::'a filter)"

    by (auto simp: bot_filter_def Sup_filter_def) }

qed

end

lemma filter_leD:

  "F \<le> F' \<Longrightarrow> eventually P F' \<Longrightarrow> eventually P F"

  unfolding le_filter_def by simp

lemma filter_leI:

  "(\<And>P. eventually P F' \<Longrightarrow> eventually P F) \<Longrightarrow> F \<le> F'"

  unfolding le_filter_def by simp

lemma eventually_False:

  "eventually (\<lambda>x. False) F \<longleftrightarrow> F = bot"

  unfolding filter_eq_iff by (auto elim: eventually_rev_mp)

abbreviation (input) trivial_limit :: "'a filter \<Rightarrow> bool"

  where "trivial_limit F \<equiv> F = bot"

lemma trivial_limit_def: "trivial_limit F \<longleftrightarrow> eventually (\<lambda>x. False) F"

  by (rule eventually_False [symmetric])

lemma eventually_const: "\<not> trivial_limit net \<Longrightarrow> eventually (\<lambda>x. P) net \<longleftrightarrow> P"

  by (cases P) (simp_all add: eventually_False)

subsubsection {* Map function for filters *}

definition filtermap :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a filter \<Rightarrow> 'b filter"

  where "filtermap f F = Abs_filter (\<lambda>P. eventually (\<lambda>x. P (f x)) F)"

lemma eventually_filtermap:

  "eventually P (filtermap f F) = eventually (\<lambda>x. P (f x)) F"

  unfolding filtermap_def

  apply (rule eventually_Abs_filter)

  apply (rule is_filter.intro)

  apply (auto elim!: eventually_rev_mp)

  done

lemma filtermap_ident: "filtermap (\<lambda>x. x) F = F"

  by (simp add: filter_eq_iff eventually_filtermap)

lemma filtermap_filtermap:

  "filtermap f (filtermap g F) = filtermap (\<lambda>x. f (g x)) F"

  by (simp add: filter_eq_iff eventually_filtermap)

lemma filtermap_mono: "F \<le> F' \<Longrightarrow> filtermap f F \<le> filtermap f F'"

  unfolding le_filter_def eventually_filtermap by simp

lemma filtermap_bot [simp]: "filtermap f bot = bot"

  by (simp add: filter_eq_iff eventually_filtermap)

lemma filtermap_sup: "filtermap f (sup F1 F2) = sup (filtermap f F1) (filtermap f F2)"

  by (auto simp: filter_eq_iff eventually_filtermap eventually_sup)

subsubsection {* Order filters *}

definition at_top :: "('a::order) filter"

  where "at_top = Abs_filter (\<lambda>P. \<exists>k. \<forall>n\<ge>k. P n)"

lemma eventually_at_top_linorder: "eventually P at_top \<longleftrightarrow> (\<exists>N::'a::linorder. \<forall>n\<ge>N. P n)"

  unfolding at_top_def

proof (rule eventually_Abs_filter, rule is_filter.intro)

  fix P Q :: "'a \<Rightarrow> bool"

  assume "\<exists>i. \<forall>n\<ge>i. P n" and "\<exists>j. \<forall>n\<ge>j. Q n"

  then obtain i j where "\<forall>n\<ge>i. P n" and "\<forall>n\<ge>j. Q n" by auto

  then have "\<forall>n\<ge>max i j. P n \<and> Q n" by simp

  then show "\<exists>k. \<forall>n\<ge>k. P n \<and> Q n" ..

qed auto

lemma eventually_ge_at_top:

  "eventually (\<lambda>x. (c::_::linorder) \<le> x) at_top"

  unfolding eventually_at_top_linorder by auto

lemma eventually_at_top_dense: "eventually P at_top \<longleftrightarrow> (\<exists>N::'a::unbounded_dense_linorder. \<forall>n>N. P n)"

  unfolding eventually_at_top_linorder

proof safe

  fix N assume "\<forall>n\<ge>N. P n"

  then show "\<exists>N. \<forall>n>N. P n" by (auto intro!: exI[of _ N])

next

  fix N assume "\<forall>n>N. P n"

  moreover obtain y where "N < y" using gt_ex[of N] ..

  ultimately show "\<exists>N. \<forall>n\<ge>N. P n" by (auto intro!: exI[of _ y])

qed

lemma eventually_gt_at_top:

  "eventually (\<lambda>x. (c::_::unbounded_dense_linorder) < x) at_top"

  unfolding eventually_at_top_dense by auto

definition at_bot :: "('a::order) filter"

  where "at_bot = Abs_filter (\<lambda>P. \<exists>k. \<forall>n\<le>k. P n)"

lemma eventually_at_bot_linorder:

  fixes P :: "'a::linorder \<Rightarrow> bool" shows "eventually P at_bot \<longleftrightarrow> (\<exists>N. \<forall>n\<le>N. P n)"

  unfolding at_bot_def

proof (rule eventually_Abs_filter, rule is_filter.intro)

  fix P Q :: "'a \<Rightarrow> bool"

  assume "\<exists>i. \<forall>n\<le>i. P n" and "\<exists>j. \<forall>n\<le>j. Q n"

  then obtain i j where "\<forall>n\<le>i. P n" and "\<forall>n\<le>j. Q n" by auto

  then have "\<forall>n\<le>min i j. P n \<and> Q n" by simp

  then show "\<exists>k. \<forall>n\<le>k. P n \<and> Q n" ..

qed auto

lemma eventually_le_at_bot:

  "eventually (\<lambda>x. x \<le> (c::_::linorder)) at_bot"

  unfolding eventually_at_bot_linorder by auto

lemma eventually_at_bot_dense:

  fixes P :: "'a::unbounded_dense_linorder \<Rightarrow> bool" shows "eventually P at_bot \<longleftrightarrow> (\<exists>N. \<forall>n<N. P n)"

  unfolding eventually_at_bot_linorder

proof safe

  fix N assume "\<forall>n\<le>N. P n" then show "\<exists>N. \<forall>n<N. P n" by (auto intro!: exI[of _ N])

next

  fix N assume "\<forall>n<N. P n" 

  moreover obtain y where "y < N" using lt_ex[of N] ..

  ultimately show "\<exists>N. \<forall>n\<le>N. P n" by (auto intro!: exI[of _ y])

qed

lemma eventually_gt_at_bot:

  "eventually (\<lambda>x. x < (c::_::unbounded_dense_linorder)) at_bot"

  unfolding eventually_at_bot_dense by auto

subsection {* Sequentially *}

abbreviation sequentially :: "nat filter"

  where "sequentially == at_top"

lemma sequentially_def: "sequentially = Abs_filter (\<lambda>P. \<exists>k. \<forall>n\<ge>k. P n)"

  unfolding at_top_def by simp

lemma eventually_sequentially:

  "eventually P sequentially \<longleftrightarrow> (\<exists>N. \<forall>n\<ge>N. P n)"

  by (rule eventually_at_top_linorder)

lemma sequentially_bot [simp, intro]: "sequentially \<noteq> bot"

  unfolding filter_eq_iff eventually_sequentially by auto

lemmas trivial_limit_sequentially = sequentially_bot

lemma eventually_False_sequentially [simp]:

  "\<not> eventually (\<lambda>n. False) sequentially"

  by (simp add: eventually_False)

lemma le_sequentially:

  "F \<le> sequentially \<longleftrightarrow> (\<forall>N. eventually (\<lambda>n. N \<le> n) F)"

  unfolding le_filter_def eventually_sequentially

  by (safe, fast, drule_tac x=N in spec, auto elim: eventually_rev_mp)

lemma eventually_sequentiallyI:

  assumes "\<And>x. c \<le> x \<Longrightarrow> P x"

  shows "eventually P sequentially"

using assms by (auto simp: eventually_sequentially)

lemma eventually_sequentially_seg:

  "eventually (\<lambda>n. P (n + k)) sequentially \<longleftrightarrow> eventually P sequentially"

  unfolding eventually_sequentially

  apply safe

   apply (rule_tac x="N + k" in exI)

   apply rule

   apply (erule_tac x="n - k" in allE)

   apply auto []

  apply (rule_tac x=N in exI)

  apply auto []

  done

subsubsection {* Standard filters *}

definition principal :: "'a set \<Rightarrow> 'a filter" where

  "principal S = Abs_filter (\<lambda>P. \<forall>x\<in>S. P x)"

lemma eventually_principal: "eventually P (principal S) \<longleftrightarrow> (\<forall>x\<in>S. P x)"

  unfolding principal_def

  by (rule eventually_Abs_filter, rule is_filter.intro) auto

lemma eventually_inf_principal: "eventually P (inf F (principal s)) \<longleftrightarrow> eventually (\<lambda>x. x \<in> s \<longrightarrow> P x) F"

  unfolding eventually_inf eventually_principal by (auto elim: eventually_elim1)

lemma principal_UNIV[simp]: "principal UNIV = top"

  by (auto simp: filter_eq_iff eventually_principal)

lemma principal_empty[simp]: "principal {} = bot"

  by (auto simp: filter_eq_iff eventually_principal)

lemma principal_le_iff[iff]: "principal A \<le> principal B \<longleftrightarrow> A \<subseteq> B"

  by (auto simp: le_filter_def eventually_principal)

lemma le_principal: "F \<le> principal A \<longleftrightarrow> eventually (\<lambda>x. x \<in> A) F"

  unfolding le_filter_def eventually_principal

  apply safe

  apply (erule_tac x="\<lambda>x. x \<in> A" in allE)

  apply (auto elim: eventually_elim1)

  done

lemma principal_inject[iff]: "principal A = principal B \<longleftrightarrow> A = B"

  unfolding eq_iff by simp

lemma sup_principal[simp]: "sup (principal A) (principal B) = principal (A \<union> B)"

  unfolding filter_eq_iff eventually_sup eventually_principal by auto

lemma inf_principal[simp]: "inf (principal A) (principal B) = principal (A \<inter> B)"

  unfolding filter_eq_iff eventually_inf eventually_principal

  by (auto intro: exI[of _ "\<lambda>x. x \<in> A"] exI[of _ "\<lambda>x. x \<in> B"])

lemma SUP_principal[simp]: "(SUP i : I. principal (A i)) = principal (\<Union>i\<in>I. A i)"

  unfolding filter_eq_iff eventually_Sup SUP_def by (auto simp: eventually_principal)

lemma filtermap_principal[simp]: "filtermap f (principal A) = principal (f ` A)"

  unfolding filter_eq_iff eventually_filtermap eventually_principal by simp

subsubsection {* Topological filters *}

definition (in topological_space) nhds :: "'a \<Rightarrow> 'a filter"

  where "nhds a = Abs_filter (\<lambda>P. \<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x))"

definition (in topological_space) at_within :: "'a \<Rightarrow> 'a set \<Rightarrow> 'a filter" ("at (_) within (_)" [1000, 60] 60)

  where "at a within s = inf (nhds a) (principal (s - {a}))"

abbreviation (in topological_space) at :: "'a \<Rightarrow> 'a filter" ("at") where

  "at x \<equiv> at x within (CONST UNIV)"

abbreviation (in order_topology) at_right :: "'a \<Rightarrow> 'a filter" where

  "at_right x \<equiv> at x within {x <..}"

abbreviation (in order_topology) at_left :: "'a \<Rightarrow> 'a filter" where

  "at_left x \<equiv> at x within {..< x}"

lemma (in topological_space) eventually_nhds:

  "eventually P (nhds a) \<longleftrightarrow> (\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x))"

  unfolding nhds_def

proof (rule eventually_Abs_filter, rule is_filter.intro)

  have "open UNIV \<and> a \<in> UNIV \<and> (\<forall>x\<in>UNIV. True)" by simp

  thus "\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. True)" ..

next

  fix P Q

  assume "\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x)"

     and "\<exists>T. open T \<and> a \<in> T \<and> (\<forall>x\<in>T. Q x)"

  then obtain S T where

    "open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x)"

    "open T \<and> a \<in> T \<and> (\<forall>x\<in>T. Q x)" by auto

  hence "open (S \<inter> T) \<and> a \<in> S \<inter> T \<and> (\<forall>x\<in>(S \<inter> T). P x \<and> Q x)"

    by (simp add: open_Int)

  thus "\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x \<and> Q x)" ..

qed auto

lemma nhds_neq_bot [simp]: "nhds a \<noteq> bot"

  unfolding trivial_limit_def eventually_nhds by simp

lemma eventually_at_filter:

  "eventually P (at a within s) \<longleftrightarrow> eventually (\<lambda>x. x \<noteq> a \<longrightarrow> x \<in> s \<longrightarrow> P x) (nhds a)"

  unfolding at_within_def eventually_inf_principal by (simp add: imp_conjL[symmetric] conj_commute)

lemma at_le: "s \<subseteq> t \<Longrightarrow> at x within s \<le> at x within t"

  unfolding at_within_def by (intro inf_mono) auto

lemma eventually_at_topological:

  "eventually P (at a within s) \<longleftrightarrow> (\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. x \<noteq> a \<longrightarrow> x \<in> s \<longrightarrow> P x))"

  unfolding eventually_nhds eventually_at_filter by simp

lemma at_within_open: "a \<in> S \<Longrightarrow> open S \<Longrightarrow> at a within S = at a"

  unfolding filter_eq_iff eventually_at_topological by (metis open_Int Int_iff UNIV_I)

lemma at_within_empty [simp]: "at a within {} = bot"

  unfolding at_within_def by simp

lemma at_within_union: "at x within (S \<union> 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 at_eq_bot_iff: "at a = bot \<longleftrightarrow> open {a}"

  unfolding trivial_limit_def eventually_at_topological

  by (safe, case_tac "S = {a}", simp, fast, fast)

lemma at_neq_bot [simp]: "at (a::'a::perfect_space) \<noteq> bot"

  by (simp add: at_eq_bot_iff not_open_singleton)

lemma eventually_at_right:

  fixes x :: "'a :: {no_top, linorder_topology}"

  shows "eventually P (at_right x) \<longleftrightarrow> (\<exists>b. x < b \<and> (\<forall>z. x < z \<and> z < b \<longrightarrow> P z))"

  unfolding eventually_at_topological

proof safe

  obtain y where "x < y" using gt_ex[of x] ..

  moreover fix S assume "open S" "x \<in> S" note open_right[OF this, of y]

  moreover note gt_ex[of x]

  moreover assume "\<forall>s\<in>S. s \<noteq> x \<longrightarrow> s \<in> {x<..} \<longrightarrow> P s"

  ultimately show "\<exists>b>x. \<forall>z. x < z \<and> z < b \<longrightarrow> P z"

    by (auto simp: subset_eq Ball_def)

next

  fix b assume "x < b" "\<forall>z. x < z \<and> z < b \<longrightarrow> P z"

  then show "\<exists>S. open S \<and> x \<in> S \<and> (\<forall>xa\<in>S. xa \<noteq> x \<longrightarrow> xa \<in> {x<..} \<longrightarrow> P xa)"

    by (intro exI[of _ "{..< b}"]) auto

qed

lemma eventually_at_left:

  fixes x :: "'a :: {no_bot, linorder_topology}"

  shows "eventually P (at_left x) \<longleftrightarrow> (\<exists>b. x > b \<and> (\<forall>z. b < z \<and> z < x \<longrightarrow> P z))"

  unfolding eventually_at_topological

proof safe

  obtain y where "y < x" using lt_ex[of x] ..

  moreover fix S assume "open S" "x \<in> S" note open_left[OF this, of y]

  moreover assume "\<forall>s\<in>S. s \<noteq> x \<longrightarrow> s \<in> {..<x} \<longrightarrow> P s"

  ultimately show "\<exists>b<x. \<forall>z. b < z \<and> z < x \<longrightarrow> P z"

    by (auto simp: subset_eq Ball_def)

next

  fix b assume "b < x" "\<forall>z. b < z \<and> z < x \<longrightarrow> P z"

  then show "\<exists>S. open S \<and> x \<in> S \<and> (\<forall>s\<in>S. s \<noteq> x \<longrightarrow> s \<in> {..<x} \<longrightarrow> P s)"

    by (intro exI[of _ "{b <..}"]) auto

qed

lemma trivial_limit_at_left_real [simp]:

  "\<not> trivial_limit (at_left (x::'a::{no_bot, unbounded_dense_linorder, linorder_topology}))"

  unfolding trivial_limit_def eventually_at_left by (auto dest: dense)

lemma trivial_limit_at_right_real [simp]:

  "\<not> trivial_limit (at_right (x::'a::{no_top, unbounded_dense_linorder, linorder_topology}))"

  unfolding trivial_limit_def eventually_at_right by (auto dest: dense)

lemma at_eq_sup_left_right: "at (x::'a::linorder_topology) = sup (at_left x) (at_right x)"

  by (auto simp: eventually_at_filter filter_eq_iff eventually_sup 

           elim: eventually_elim2 eventually_elim1)

lemma eventually_at_split:

  "eventually P (at (x::'a::linorder_topology)) \<longleftrightarrow> eventually P (at_left x) \<and> eventually P (at_right x)"

  by (subst at_eq_sup_left_right) (simp add: eventually_sup)

subsection {* Limits *}

definition filterlim :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b filter \<Rightarrow> 'a filter \<Rightarrow> bool" where

  "filterlim f F2 F1 \<longleftrightarrow> filtermap f F1 \<le> F2"

syntax

  "_LIM" :: "pttrns \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> bool" ("(3LIM (_)/ (_)./ (_) :> (_))" [1000, 10, 0, 10] 10)

translations

  "LIM x F1. f :> F2"   == "CONST filterlim (%x. f) F2 F1"

lemma filterlim_iff:

  "(LIM x F1. f x :> F2) \<longleftrightarrow> (\<forall>P. eventually P F2 \<longrightarrow> eventually (\<lambda>x. P (f x)) F1)"

  unfolding filterlim_def le_filter_def eventually_filtermap ..

lemma filterlim_compose:

  "filterlim g F3 F2 \<Longrightarrow> filterlim f F2 F1 \<Longrightarrow> filterlim (\<lambda>x. g (f x)) F3 F1"

  unfolding filterlim_def filtermap_filtermap[symmetric] by (metis filtermap_mono order_trans)

lemma filterlim_mono:

  "filterlim f F2 F1 \<Longrightarrow> F2 \<le> F2' \<Longrightarrow> F1' \<le> F1 \<Longrightarrow> filterlim f F2' F1'"

  unfolding filterlim_def by (metis filtermap_mono order_trans)

lemma filterlim_ident: "LIM x F. x :> F"

  by (simp add: filterlim_def filtermap_ident)

lemma filterlim_cong:

  "F1 = F1' \<Longrightarrow> F2 = F2' \<Longrightarrow> eventually (\<lambda>x. f x = g x) F2 \<Longrightarrow> filterlim f F1 F2 = filterlim g F1' F2'"

  by (auto simp: filterlim_def le_filter_def eventually_filtermap elim: eventually_elim2)

lemma filterlim_principal:

  "(LIM x F. f x :> principal S) \<longleftrightarrow> (eventually (\<lambda>x. f x \<in> S) F)"

  unfolding filterlim_def eventually_filtermap le_principal ..

lemma filterlim_inf:

  "(LIM x F1. f x :> inf F2 F3) \<longleftrightarrow> ((LIM x F1. f x :> F2) \<and> (LIM x F1. f x :> F3))"

  unfolding filterlim_def by simp

lemma filterlim_filtermap: "filterlim f F1 (filtermap g F2) = filterlim (\<lambda>x. f (g x)) F1 F2"

  unfolding filterlim_def filtermap_filtermap ..

lemma filterlim_sup:

  "filterlim f F F1 \<Longrightarrow> filterlim f F F2 \<Longrightarrow> filterlim f F (sup F1 F2)"

  unfolding filterlim_def filtermap_sup by auto

lemma filterlim_Suc: "filterlim Suc sequentially sequentially"

  by (simp add: filterlim_iff eventually_sequentially) (metis le_Suc_eq)

subsubsection {* Tendsto *}

abbreviation (in topological_space)

  tendsto :: "('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b filter \<Rightarrow> bool" (infixr "--->" 55) where

  "(f ---> l) F \<equiv> filterlim f (nhds l) F"

definition (in t2_space) Lim :: "'f filter \<Rightarrow> ('f \<Rightarrow> 'a) \<Rightarrow> 'a" where

  "Lim A f = (THE l. (f ---> l) A)"

lemma tendsto_eq_rhs: "(f ---> x) F \<Longrightarrow> x = y \<Longrightarrow> (f ---> y) F"

  by simp

ML {*

structure Tendsto_Intros = Named_Thms

(

  val name = @{binding tendsto_intros}

  val description = "introduction rules for tendsto"

)

*}

setup {*

  Tendsto_Intros.setup #>

  Global_Theory.add_thms_dynamic (@{binding tendsto_eq_intros},

    map_filter (try (fn thm => @{thm tendsto_eq_rhs} OF [thm])) o Tendsto_Intros.get o Context.proof_of);

*}

lemma (in topological_space) tendsto_def:

   "(f ---> l) F \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) F)"

  unfolding filterlim_def

proof safe

  fix S assume "open S" "l \<in> S" "filtermap f F \<le> nhds l"

  then show "eventually (\<lambda>x. f x \<in> S) F"

    unfolding eventually_nhds eventually_filtermap le_filter_def

    by (auto elim!: allE[of _ "\<lambda>x. x \<in> S"] eventually_rev_mp)

qed (auto elim!: eventually_rev_mp simp: eventually_nhds eventually_filtermap le_filter_def)

lemma tendsto_mono: "F \<le> F' \<Longrightarrow> (f ---> l) F' \<Longrightarrow> (f ---> l) F"

  unfolding tendsto_def le_filter_def by fast

lemma tendsto_within_subset: "(f ---> l) (at x within S) \<Longrightarrow> T \<subseteq> S \<Longrightarrow> (f ---> l) (at x within T)"

  by (blast intro: tendsto_mono at_le)

lemma filterlim_at:

  "(LIM x F. f x :> at b within s) \<longleftrightarrow> (eventually (\<lambda>x. f x \<in> s \<and> f x \<noteq> b) F \<and> (f ---> b) F)"

  by (simp add: at_within_def filterlim_inf filterlim_principal conj_commute)

lemma (in topological_space) topological_tendstoI:

  "(\<And>S. open S \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>x. f x \<in> S) F) \<Longrightarrow> (f ---> l) F"

  unfolding tendsto_def by auto

lemma (in topological_space) topological_tendstoD:

  "(f ---> l) F \<Longrightarrow> open S \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>x. f x \<in> S) F"

  unfolding tendsto_def by auto

lemma order_tendstoI:

  fixes y :: "_ :: order_topology"

  assumes "\<And>a. a < y \<Longrightarrow> eventually (\<lambda>x. a < f x) F"

  assumes "\<And>a. y < a \<Longrightarrow> eventually (\<lambda>x. f x < a) F"

  shows "(f ---> y) F"

proof (rule topological_tendstoI)

  fix S assume "open S" "y \<in> S"

  then show "eventually (\<lambda>x. f x \<in> S) F"

    unfolding open_generated_order

  proof induct

    case (UN K)

    then obtain k where "y \<in> k" "k \<in> K" by auto

    with UN(2)[of k] show ?case

      by (auto elim: eventually_elim1)

  qed (insert assms, auto elim: eventually_elim2)

qed

lemma order_tendstoD:

  fixes y :: "_ :: order_topology"

  assumes y: "(f ---> y) F"

  shows "a < y \<Longrightarrow> eventually (\<lambda>x. a < f x) F"

    and "y < a \<Longrightarrow> eventually (\<lambda>x. f x < a) F"

  using topological_tendstoD[OF y, of "{..< a}"] topological_tendstoD[OF y, of "{a <..}"] by auto

lemma order_tendsto_iff: 

  fixes f :: "_ \<Rightarrow> 'a :: order_topology"

  shows "(f ---> x) F \<longleftrightarrow>(\<forall>l<x. eventually (\<lambda>x. l < f x) F) \<and> (\<forall>u>x. eventually (\<lambda>x. f x < u) F)"

  by (metis order_tendstoI order_tendstoD)

lemma tendsto_bot [simp]: "(f ---> a) bot"

  unfolding tendsto_def by simp

lemma tendsto_ident_at [tendsto_intros]: "((\<lambda>x. x) ---> a) (at a within s)"

  unfolding tendsto_def eventually_at_topological by auto

lemma (in topological_space) tendsto_const [tendsto_intros]: "((\<lambda>x. k) ---> k) F"

  by (simp add: tendsto_def)

lemma (in t2_space) tendsto_unique:

  assumes "\<not> trivial_limit F" and "(f ---> a) F" and "(f ---> b) F"

  shows "a = b"

proof (rule ccontr)

  assume "a \<noteq> b"

  obtain U V where "open U" "open V" "a \<in> U" "b \<in> V" "U \<inter> V = {}"

    using hausdorff [OF `a \<noteq> b`] by fast

  have "eventually (\<lambda>x. f x \<in> U) F"

    using `(f ---> a) F` `open U` `a \<in> U` by (rule topological_tendstoD)

  moreover

  have "eventually (\<lambda>x. f x \<in> V) F"

    using `(f ---> b) F` `open V` `b \<in> V` by (rule topological_tendstoD)

  ultimately

  have "eventually (\<lambda>x. False) F"

  proof eventually_elim

    case (elim x)

    hence "f x \<in> U \<inter> V" by simp

    with `U \<inter> V = {}` show ?case by simp

  qed

  with `\<not> trivial_limit F` show "False"

    by (simp add: trivial_limit_def)

qed

lemma (in t2_space) tendsto_const_iff:

  assumes "\<not> trivial_limit F" shows "((\<lambda>x. a :: 'a) ---> b) F \<longleftrightarrow> a = b"

  by (safe intro!: tendsto_const tendsto_unique [OF assms tendsto_const])

lemma increasing_tendsto:

  fixes f :: "_ \<Rightarrow> 'a::order_topology"

  assumes bdd: "eventually (\<lambda>n. f n \<le> l) F"

      and en: "\<And>x. x < l \<Longrightarrow> eventually (\<lambda>n. x < f n) F"

  shows "(f ---> l) F"

  using assms by (intro order_tendstoI) (auto elim!: eventually_elim1)