Theory Extra_General

section ‹‹Extra_General› -- General missing things›

theory Extra_General
  imports
    "HOL-Library.Cardinality"
    "HOL-Analysis.Elementary_Topology"
    "HOL-Analysis.Uniform_Limit"
    "HOL-Library.Set_Algebras"
    "HOL-Types_To_Sets.Types_To_Sets"
    "HOL-Library.Complex_Order"
    "HOL-Analysis.Infinite_Sum"
    "HOL-Cardinals.Cardinals"
    "HOL-Library.Complemented_Lattices"
    "HOL-Analysis.Abstract_Topological_Spaces"
begin

subsection ‹Misc›

lemma reals_zero_comparable:
  fixes x::complex
  assumes "x∈ℝ"
  shows "x ≤ 0 ∨ x ≥ 0"
  using assms unfolding complex_is_real_iff_compare0 by assumption

lemma unique_choice: "∀x. ∃!y. Q x y ⟹ ∃!f. ∀x. Q x (f x)"
  apply (auto intro!: choice ext) by metis

lemma image_set_plus: 
  assumes ‹linear U›
  shows ‹U ` (A + B) = U ` A + U ` B›
  unfolding image_def set_plus_def
  using assms by (force simp: linear_add)

consts heterogenous_identity :: ‹'a ⇒ 'b›
overloading heterogenous_identity_id ≡ "heterogenous_identity :: 'a ⇒ 'a" begin
definition heterogenous_identity_def[simp]: ‹heterogenous_identity_id = id›
end

lemma L2_set_mono2:
  assumes a1: "finite L" and a2: "K ≤ L"
  shows "L2_set f K ≤ L2_set f L"
proof-
  have "(∑i∈K. (f i)⇧2) ≤ (∑i∈L. (f i)⇧2)"
    apply (rule sum_mono2) 
    using assms by auto
  hence "sqrt (∑i∈K. (f i)⇧2) ≤ sqrt (∑i∈L. (f i)⇧2)"
    by (rule real_sqrt_le_mono)
  thus ?thesis
    unfolding L2_set_def.
qed

lemma Sup_real_close:
  fixes e :: real
  assumes "0 < e"
    and S: "bdd_above S" "S ≠ {}"
  shows "∃x∈S. Sup S - e < x"
proof -
  have ‹Sup (ereal ` S) ≠ ∞›
    by (metis assms(2) bdd_above_def ereal_less_eq(3) less_SUP_iff less_ereal.simps(4) not_le)
  moreover have ‹Sup (ereal ` S) ≠ -∞›
    by (simp add: SUP_eq_iff assms(3))
  ultimately have Sup_bdd: ‹¦Sup (ereal ` S)¦ ≠ ∞›
    by auto
  then have ‹∃x'∈ereal ` S. Sup (ereal ` S) - ereal e < x'›
    apply (rule_tac Sup_ereal_close)
    using assms by auto
  then obtain x where ‹x ∈ S› and Sup_x: ‹Sup (ereal ` S) - ereal e < ereal x›
    by auto
  have ‹Sup (ereal ` S) = ereal (Sup S)›
    using Sup_bdd by (rule ereal_Sup[symmetric])
  with Sup_x have ‹ereal (Sup S - e) < ereal x›
    by auto
  then have ‹Sup S - e < x›
    by auto
  with ‹x ∈ S› show ?thesis
    by auto
qed

text ‹Improved version of @{attribute internalize_sort}: It is not necessary to specify the sort of the type variable.›
attribute_setup internalize_sort' = ‹let
fun find_tvar thm v = let
  val tvars = Term.add_tvars (Thm.prop_of thm) []
  val tv = case find_first (fn (n,sort) => n=v) tvars of
              SOME tv => tv | NONE => raise THM ("Type variable " ^ string_of_indexname v ^ " not found", 0, [thm])
in 
TVar tv
end

fun internalize_sort_attr (tvar:indexname) =
  Thm.rule_attribute [] (fn context => fn thm =>
    (snd (Internalize_Sort.internalize_sort (Thm.ctyp_of (Context.proof_of context) (find_tvar thm tvar)) thm)));
in
  Scan.lift Args.var >> internalize_sort_attr
end›
  "internalize a sort"

lemma card_prod_omega: ‹X *c natLeq =o X› if ‹Cinfinite X›
  by (simp add: Cinfinite_Cnotzero cprod_infinite1' natLeq_Card_order natLeq_cinfinite natLeq_ordLeq_cinfinite that)

lemma countable_leq_natLeq: ‹|X| ≤o natLeq› if ‹countable X›
  using subset_range_from_nat_into[OF that]
  by (meson card_of_nat ordIso_iff_ordLeq ordLeq_transitive surj_imp_ordLeq)

lemma set_Times_plus_distrib: ‹(A × B) + (C × D) = (A + C) × (B + D)›
  by (auto simp: Sigma_def set_plus_def)

definition (in order) ‹is_Sup X s ⟷ (∀x∈X. x ≤ s) ∧ (∀y. (∀x∈X. x ≤ y) ⟶ s ≤ y)›
definition (in order) ‹has_Sup X ⟷ (∃s. is_Sup X s)›

lemma (in order) is_SupI:
  assumes ‹⋀x. x ∈ X ⟹ x ≤ s›
  assumes ‹⋀y. (⋀x. x ∈ X ⟹ x ≤ y) ⟹ s ≤ y›
  shows ‹is_Sup X s›
  using assms by (auto simp add: is_Sup_def)

lemma is_Sup_approx_below:
  fixes b :: ‹'a::linordered_ab_group_add›
  assumes ‹is_Sup A b›
  assumes ‹ε > 0›
  shows ‹∃x∈A. b - ε ≤ x›
proof (rule ccontr)
  assume ‹¬ (∃x∈A. b - ε ≤ x)›
  then have ‹b - ε ≥ x› if ‹x ∈ A› for x
    using that by auto
  with assms
  have ‹b ≤ b - ε›
    by (simp add: is_Sup_def)
  with ‹ε > 0›
  show False
    by simp
qed

subsection ‹Not singleton›

class not_singleton =
  assumes not_singleton_card: "∃x y. x ≠ y"

lemma not_singleton_existence[simp]:
  ‹∃ x::('a::not_singleton). x ≠ t›
  using not_singleton_card[where ?'a = 'a] by (metis (full_types))

lemma not_not_singleton_zero: 
  ‹x = 0› if ‹¬ class.not_singleton TYPE('a)› for x :: ‹'a::zero›
  using that unfolding class.not_singleton_def by auto

lemma UNIV_not_singleton[simp]: "(UNIV::_::not_singleton set) ≠ {x}"
  using not_singleton_existence[of x] by blast

lemma UNIV_not_singleton_converse: 
  assumes"⋀x::'a. UNIV ≠ {x}"
  shows "∃x::'a. ∃y. x ≠ y"
  using assms
  by fastforce 

subclass (in card2) not_singleton
  apply standard using two_le_card
  by (meson card_2_iff' obtain_subset_with_card_n)

subclass (in perfect_space) not_singleton
  apply intro_classes
  by (metis (mono_tags) Collect_cong Collect_mem_eq UNIV_I local.UNIV_not_singleton local.not_open_singleton local.open_subopen)

lemma class_not_singletonI_monoid_add:
  assumes "(UNIV::'a set) ≠ {0}"
  shows "class.not_singleton TYPE('a::monoid_add)"
proof intro_classes
  let ?univ = "UNIV :: 'a set"
  from assms obtain x::'a where "x ≠ 0"
    by auto
  thus "∃x y :: 'a. x ≠ y"
    by auto
qed

lemma not_singleton_vs_CARD_1:
  assumes ‹¬ class.not_singleton TYPE('a)›
  shows ‹class.CARD_1 TYPE('a)›
  using assms unfolding class.not_singleton_def class.CARD_1_def
  by (metis (full_types) One_nat_def UNIV_I card.empty card.insert empty_iff equalityI finite.intros(1) insert_iff subsetI)

subsection ‹\<^class>‹CARD_1››

context CARD_1 begin

lemma everything_the_same[simp]: "(x::'a)=y"
  by (metis (full_types) UNIV_I card_1_singletonE empty_iff insert_iff local.CARD_1)

lemma CARD_1_UNIV: "UNIV = {x::'a}"
  by (metis (full_types) UNIV_I card_1_singletonE local.CARD_1 singletonD)

lemma CARD_1_ext: "x (a::'a) = y b ⟹ x = y"
proof (rule ext)
  show "x t = y t"
    if "x a = y b"
    for t :: 'a
    using that  apply (subst (asm) everything_the_same[where x=a])
    apply (subst (asm) everything_the_same[where x=b])
    by simp
qed 

end

instance unit :: CARD_1
  apply standard by auto

instance prod :: (CARD_1, CARD_1) CARD_1
  apply intro_classes
  by (simp add: CARD_1)

instance "fun" :: (CARD_1, CARD_1) CARD_1
  apply intro_classes
  by (auto simp add: card_fun CARD_1)


lemma enum_CARD_1: "(Enum.enum :: 'a::{CARD_1,enum} list) = [a]"
proof -
  let ?enum = "Enum.enum :: 'a::{CARD_1,enum} list"
  have "length ?enum = 1"
    apply (subst card_UNIV_length_enum[symmetric])
    by (rule CARD_1)
  then obtain b where "?enum = [b]"
    apply atomize_elim
    apply (cases ?enum, auto)
    by (metis length_0_conv length_Cons nat.inject)
  thus "?enum = [a]"
    by (subst everything_the_same[of _ b], simp)
qed

lemma card_not_singleton: ‹CARD('a::not_singleton) ≠ 1›
  by (simp add: card_1_singleton_iff)


subsection ‹Topology›

lemma cauchy_filter_metricI:
  fixes F :: "'a::metric_space filter"
  assumes "⋀e. e>0 ⟹ ∃P. eventually P F ∧ (∀x y. P x ∧ P y ⟶ dist x y < e)"
  shows "cauchy_filter F"
proof (unfold cauchy_filter_def le_filter_def, auto)
  fix P :: "'a × 'a ⇒ bool"
  assume "eventually P uniformity"
  then obtain e where e: "e > 0" and P: "dist x y < e ⟹ P (x, y)" for x y
    unfolding eventually_uniformity_metric by auto

  obtain P' where evP': "eventually P' F" and P'_dist: "P' x ∧ P' y ⟹ dist x y < e" for x y
    apply atomize_elim using assms e by auto

  from evP' P'_dist P
  show "eventually P (F ×⇩F F)"
    unfolding eventually_uniformity_metric eventually_prod_filter eventually_filtermap by metis
qed

lemma cauchy_filter_metric_filtermapI:
  fixes F :: "'a filter" and f :: "'a⇒'b::metric_space"
  assumes "⋀e. e>0 ⟹ ∃P. eventually P F ∧ (∀x y. P x ∧ P y ⟶ dist (f x) (f y) < e)"
  shows "cauchy_filter (filtermap f F)"
proof (rule cauchy_filter_metricI)
  fix e :: real assume e: "e > 0"
  with assms obtain P where evP: "eventually P F" and dist: "P x ∧ P y ⟹ dist (f x) (f y) < e" for x y
    by atomize_elim auto
  define P' where "P' y = (∃x. P x ∧ y = f x)" for y
  have "eventually P' (filtermap f F)"
    unfolding eventually_filtermap P'_def 
    using evP
    by (smt (z3) eventually_mono) 
  moreover have "P' x ∧ P' y ⟶ dist x y < e" for x y
    unfolding P'_def using dist by metis
  ultimately show "∃P. eventually P (filtermap f F) ∧ (∀x y. P x ∧ P y ⟶ dist x y < e)"
    by auto
qed


lemma tendsto_add_const_iff:
  ― ‹This is a generalization of ‹Limits.tendsto_add_const_iff›, 
      the only difference is that the sort here is more general.›
  "((λx. c + f x :: 'a::topological_group_add) ⤏ c + d) F ⟷ (f ⤏ d) F"
  using tendsto_add[OF tendsto_const[of c], of f d]
    and tendsto_add[OF tendsto_const[of "-c"], of "λx. c + f x" "c + d"] by auto

lemma finite_subsets_at_top_minus: 
  assumes "A⊆B"
  shows "finite_subsets_at_top (B - A) ≤ filtermap (λF. F - A) (finite_subsets_at_top B)"
proof (rule filter_leI)
  fix P assume "eventually P (filtermap (λF. F - A) (finite_subsets_at_top B))"
  then obtain X where "finite X" and "X ⊆ B" 
    and P: "finite Y ∧ X ⊆ Y ∧ Y ⊆ B ⟶ P (Y - A)" for Y
    unfolding eventually_filtermap eventually_finite_subsets_at_top by auto

  hence "finite (X-A)" and "X-A ⊆ B - A"
    by auto
  moreover have "finite Y ∧ X-A ⊆ Y ∧ Y ⊆ B - A ⟶ P Y" for Y
    using P[where Y="Y∪X"] ‹finite X› ‹X ⊆ B›
    by (metis Diff_subset Int_Diff Un_Diff finite_Un inf.orderE le_sup_iff sup.orderE sup_ge2)
  ultimately show "eventually P (finite_subsets_at_top (B - A))"
    unfolding eventually_finite_subsets_at_top by meson
qed

lemma finite_subsets_at_top_inter: 
  assumes "A⊆B"
  shows "filtermap (λF. F ∩ A) (finite_subsets_at_top B) = finite_subsets_at_top A"
proof (subst filter_eq_iff, intro allI iffI)
  fix P :: "'a set ⇒ bool"
  assume "eventually P (finite_subsets_at_top A)"
  then show "eventually P (filtermap (λF. F ∩ A) (finite_subsets_at_top B))"
    unfolding eventually_filtermap
    unfolding eventually_finite_subsets_at_top
    by (metis Int_subset_iff assms finite_Int inf_le2 subset_trans)
next
  fix P :: "'a set ⇒ bool"
  assume "eventually P (filtermap (λF. F ∩ A) (finite_subsets_at_top B))"
  then obtain X where ‹finite X› ‹X ⊆ B› and P: ‹finite Y ⟹ X ⊆ Y ⟹ Y ⊆ B ⟹ P (Y ∩ A)› for Y
    unfolding eventually_filtermap eventually_finite_subsets_at_top by metis
  have *: ‹finite Y ⟹ X ∩ A ⊆ Y ⟹ Y ⊆ A ⟹ P Y› for Y
    using P[where Y=‹Y ∪ (B-A)›]
    apply (subgoal_tac ‹(Y ∪ (B - A)) ∩ A = Y›)
    apply (smt (verit, best) Int_Un_distrib2 Int_Un_eq(4) P Un_subset_iff ‹X ⊆ B› ‹finite X› assms finite_UnI inf.orderE sup_ge2)
    by auto
  show "eventually P (finite_subsets_at_top A)"
    unfolding eventually_finite_subsets_at_top
    apply (rule exI[of _ ‹X∩A›])
    by (auto simp: ‹finite X› intro!: *)
qed

lemma tendsto_principal_singleton:
  shows "(f ⤏ f x) (principal {x})"
  unfolding tendsto_def eventually_principal by simp

lemma complete_singleton: 
  "complete {s::'a::uniform_space}"
proof-
  have "F ≤ principal {s} ⟹
         F ≠ bot ⟹ cauchy_filter F ⟹ F ≤ nhds s" for F
    by (metis eventually_nhds eventually_principal le_filter_def singletonD)
  thus ?thesis
    unfolding complete_uniform
    by simp
qed

lemma on_closure_eqI:
  fixes f g :: ‹'a::topological_space ⇒ 'b::t2_space›
  assumes eq: ‹⋀x. x ∈ S ⟹ f x = g x›
  assumes xS: ‹x ∈ closure S›
  assumes cont: ‹continuous_on UNIV f› ‹continuous_on UNIV g›
  shows ‹f x = g x›
proof -
  define X where ‹X = {x. f x = g x}›
  have ‹closed X›
    using cont by (simp add: X_def closed_Collect_eq)
  moreover have ‹S ⊆ X›
    by (simp add: X_def eq subsetI)
  ultimately have ‹closure S ⊆ X›
    using closure_minimal by blast
  with xS have ‹x ∈ X›
    by auto
  then show ?thesis
    using X_def by blast
qed

lemma on_closure_leI:
  fixes f g :: ‹'a::topological_space ⇒ 'b::linorder_topology›
  assumes eq: ‹⋀x. x ∈ S ⟹ f x ≤ g x›
  assumes xS: ‹x ∈ closure S›
  assumes cont: ‹continuous_on UNIV f› ‹continuous_on UNIV g› (* Is "isCont f x" "isCont g x" sufficient? *)
  shows ‹f x ≤ g x›
proof -
  define X where ‹X = {x. f x ≤ g x}›
  have ‹closed X›
    using cont by (simp add: X_def closed_Collect_le)
  moreover have ‹S ⊆ X›
    by (simp add: X_def eq subsetI)
  ultimately have ‹closure S ⊆ X›
    using closure_minimal by blast
  with xS have ‹x ∈ X›
    by auto
  then show ?thesis
    using X_def by blast
qed


lemma tendsto_compose_at_within:
  assumes f: "(f ⤏ y) F" and g: "(g ⤏ z) (at y within S)" 
    and fg: "eventually (λw. f w = y ⟶ g y = z) F"
    and fS: ‹∀⇩F w in F. f w ∈ S›
  shows "((g ∘ f) ⤏ z) F"
proof (cases ‹g y = z›)
  case False
  then have 1: "(∀⇩F a in F. f a ≠ y)"
    using fg by force
  have 2: "(g ⤏ z) (filtermap f F) ∨ ¬ (∀⇩F a in F. f a ≠ y)"
    by (smt (verit, best) eventually_elim2 f fS filterlim_at filterlim_def g tendsto_mono)
  show ?thesis
    using "1" "2" tendsto_compose_filtermap by blast
next
  case True
  have *: ?thesis if ‹(g ⤏ z) (filtermap f F)›
    using that by (simp add: tendsto_compose_filtermap)
  from g
  have ‹(g ⤏ g y) (inf (nhds y) (principal (S-{y})))›
    by (simp add: True at_within_def)
  then have g': ‹(g ⤏ g y) (inf (nhds y) (principal S))›
    using True g tendsto_at_iff_tendsto_nhds_within by blast
  from f have ‹filterlim f (nhds y) F›
    by -
  then have f': ‹filterlim f (inf (nhds y) (principal S)) F›
    using fS
    by (simp add: filterlim_inf filterlim_principal)
  from f' g' show ?thesis
    by (simp add: * True filterlim_compose filterlim_filtermap)
qed

subsection ‹Sums›

lemma sum_single: 
  assumes "finite A"
  assumes "⋀j. j ≠ i ⟹ j∈A ⟹ f j = 0"
  shows "sum f A = (if i∈A then f i else 0)"
  apply (subst sum.mono_neutral_cong_right[where S=‹A ∩ {i}› and h=f])
  using assms by auto

lemma has_sum_comm_additive_general: 
  ― ‹This is a strengthening of @{thm [source] has_sum_comm_additive_general}.›
  fixes f :: ‹'b :: {comm_monoid_add,topological_space} ⇒ 'c :: {comm_monoid_add,topological_space}›
  assumes f_sum: ‹⋀F. finite F ⟹ F ⊆ S ⟹ sum (f o g) F = f (sum g F)›
      ― ‹Not using \<^const>‹additive› because it would add sort constraint \<^class>‹ab_group_add››
  assumes inS: ‹⋀F. finite F ⟹ sum g F ∈ T›
  assumes cont: ‹(f ⤏ f x) (at x within T)›
    ― ‹For \<^class>‹t2_space› and \<^term>‹T=UNIV›, this is equivalent to ‹isCont f x› by @{thm [source] isCont_def}.›
  assumes infsum: ‹(g has_sum x) S›
  shows ‹((f o g) has_sum (f x)) S› 
proof -
  have ‹(sum g ⤏ x) (finite_subsets_at_top S)›
    using infsum has_sum_def by blast
  then have ‹((f o sum g) ⤏ f x) (finite_subsets_at_top S)›
    apply (rule tendsto_compose_at_within[where S=T])
    using assms by auto
  then have ‹(sum (f o g) ⤏ f x) (finite_subsets_at_top S)›
    apply (rule tendsto_cong[THEN iffD1, rotated])
    using f_sum by fastforce
  then show ‹((f o g) has_sum (f x)) S›
    using has_sum_def by blast 
qed

lemma summable_on_comm_additive_general:
  ― ‹This is a strengthening of @{thm [source] summable_on_comm_additive_general}.›
  fixes g :: ‹'a ⇒ 'b :: {comm_monoid_add,topological_space}› and f :: ‹'b ⇒ 'c :: {comm_monoid_add,topological_space}›
  assumes ‹⋀F. finite F ⟹ F ⊆ S ⟹ sum (f o g) F = f (sum g F)›
    ― ‹Not using \<^const>‹additive› because it would add sort constraint \<^class>‹ab_group_add››
  assumes inS: ‹⋀F. finite F ⟹ sum g F ∈ T›
  assumes cont: ‹⋀x. (g has_sum x) S ⟹ (f ⤏ f x) (at x within T)›
    ― ‹For \<^class>‹t2_space› and \<^term>‹T=UNIV›, this is equivalent to ‹isCont f x› by @{thm [source] isCont_def}.›
  assumes ‹g summable_on S›
  shows ‹(f o g) summable_on S›
  by (meson assms summable_on_def has_sum_comm_additive_general has_sum_def infsum_tendsto)

lemma has_sum_metric:
  fixes l :: ‹'a :: {metric_space, comm_monoid_add}›
  shows ‹(f has_sum l) A ⟷ (∀e. e > 0 ⟶ (∃X. finite X ∧ X ⊆ A ∧ (∀Y. finite Y ∧ X ⊆ Y ∧ Y ⊆ A ⟶ dist (sum f Y) l < e)))›
  unfolding has_sum_def
  apply (subst tendsto_iff)
  unfolding eventually_finite_subsets_at_top
  by simp

lemma summable_on_product_finite_left:
  fixes f :: ‹'a×'b ⇒ 'c::{topological_comm_monoid_add}›
  assumes sum: ‹⋀x. x∈X ⟹ (λy. f(x,y)) summable_on Y›
  assumes ‹finite X›
  shows ‹f summable_on (X×Y)›
  using ‹finite X› subset_refl[of X]
proof (induction rule: finite_subset_induct')
  case empty
  then show ?case
    by simp
next
  case (insert x F)
  have *: ‹bij_betw (Pair x) Y ({x} × Y)›
    apply (rule bij_betwI')
    by auto
  from sum[of x]
  have ‹f summable_on {x} × Y›
    apply (rule summable_on_reindex_bij_betw[THEN iffD1, rotated])
    by (simp_all add: * insert.hyps(2))
  then have ‹f summable_on {x} × Y ∪ F × Y›
    apply (rule summable_on_Un_disjoint)
    using insert by auto
  then show ?case
    by (metis Sigma_Un_distrib1 insert_is_Un)
qed

lemma summable_on_product_finite_right:
  fixes f :: ‹'a×'b ⇒ 'c::{topological_comm_monoid_add}›
  assumes sum: ‹⋀y. y∈Y ⟹ (λx. f(x,y)) summable_on X›
  assumes ‹finite Y›
  shows ‹f summable_on (X×Y)›
proof -
  have ‹(λ(y,x). f(x,y)) summable_on (Y×X)›
    apply (rule summable_on_product_finite_left)
    using assms by auto
  then show ?thesis
    apply (subst summable_on_reindex_bij_betw[where g=prod.swap and A=‹Y×X›, symmetric])
    apply (simp add: bij_betw_def product_swap)
    by (metis (mono_tags, lifting) case_prod_unfold prod.swap_def summable_on_cong)
qed



subsection ‹Complex numbers›

lemma cmod_Re:
  assumes "x ≥ 0"
  shows "cmod x = Re x"
  using assms unfolding less_eq_complex_def cmod_def
  by auto

lemma abs_complex_real[simp]: "abs x ∈ ℝ" for x :: complex
  by (simp add: abs_complex_def)

lemma Im_abs[simp]: "Im (abs x) = 0"
  using abs_complex_real complex_is_Real_iff by blast


lemma cnj_x_x: "cnj x * x = (abs x)⇧2"
proof (cases x)
  show "cnj x * x = ¦x¦⇧2"
    if "x = Complex x1 x2"
    for x1 :: real
      and x2 :: real
    using that
    by (auto simp: complex_cnj complex_mult abs_complex_def
        complex_norm power2_eq_square complex_of_real_def)
qed

lemma cnj_x_x_geq0[simp]: ‹cnj x * x ≥ 0›
  by (simp add: less_eq_complex_def)

lemma complex_of_real_leq_1_iff[iff]: ‹complex_of_real x ≤ 1 ⟷ x ≤ 1›
  by (simp add: less_eq_complex_def)

lemma x_cnj_x: ‹x * cnj x = (abs x)⇧2›
  by (metis cnj_x_x mult.commute)

lemma has_sum_mono_neutral_complex:
  fixes f :: "'a ⇒ complex"
  assumes ‹(f has_sum a) A› and "(g has_sum b) B"
  assumes ‹⋀x. x ∈ A∩B ⟹ f x ≤ g x›
  assumes ‹⋀x. x ∈ A-B ⟹ f x ≤ 0›
  assumes ‹⋀x. x ∈ B-A ⟹ g x ≥ 0›
  shows "a ≤ b"
proof -
  have ‹((λx. Re (f x)) has_sum Re a) A›
    using assms(1) has_sum_Re has_sum_cong by blast
  moreover have ‹((λx. Re (g x)) has_sum Re b) B›
    using assms(2) has_sum_Re has_sum_cong by blast
  ultimately have Re: ‹Re a ≤ Re b›
    apply (rule has_sum_mono_neutral)
    using assms(3-5) by (simp_all add: less_eq_complex_def)
  have ‹((λx. Im (f x)) has_sum Im a) A›
    using assms(1) has_sum_Im has_sum_cong by blast
  then have ‹((λx. Im (f x)) has_sum Im a) (A ∩ B)›
    apply (rule has_sum_cong_neutral[THEN iffD1, rotated -1])
    using assms(3-5) by (auto simp add: less_eq_complex_def)
  moreover have ‹((λx. Im (g x)) has_sum Im b) B›
    using assms(2) has_sum_Im has_sum_cong by blast
  then have ‹((λx. Im (f x)) has_sum Im b) (A ∩ B)›
    apply (rule has_sum_cong_neutral[THEN iffD1, rotated -1])
    using assms(3-5) by (auto simp add: less_eq_complex_def)
  ultimately have Im: ‹Im a = Im b›
    by (rule has_sum_unique)
  from Re Im show ?thesis
    using less_eq_complex_def by blast
qed

lemma Re_mono: "x ≤ y ⟹ Re x ≤ Re y"
  unfolding less_eq_complex_def by simp

lemma comp_Im_same: "x ≤ y ⟹ Im x = Im y"
  unfolding less_eq_complex_def by simp

lemma Re_strict_mono: "x < y ⟹ Re x < Re y"
  unfolding less_complex_def by simp

lemma complex_of_real_cmod: ‹complex_of_real (cmod x) = abs x›
  by (simp add: abs_complex_def)

lemma less_eq_complexI: "Re x ≤ Re y ⟹ Im x = Im y ⟹ x≤y" unfolding less_eq_complex_def
  by simp
lemma less_complexI: "Re x < Re y ⟹ Im x = Im y ⟹ x<y" unfolding less_complex_def
  by simp

lemma sums_le_complex: 
  fixes f g :: "nat ⇒ complex"
  assumes ‹⋀n. f n ≤ g n›
  assumes ‹f sums s›
  assumes ‹g sums t›
  shows ‹s ≤ t›
proof -
  have ‹Re (f n) ≤ Re (g n)› for n
    by (simp add: Re_mono assms(1)) 
  moreover have ‹(λn. Re (f n)) sums Re s›
    using assms(2) sums_Re by auto 
  moreover have ‹(λn. Re (g n)) sums Re t›
    using assms(3) sums_Re by auto 
  ultimately have re: ‹Re s ≤ Re t›
    by (rule sums_le)
  have ‹Im (f n) = Im (g n)› for n
    by (simp add: assms(1) comp_Im_same) 
  moreover have ‹(λn. Im (f n)) sums Im s›
    using assms(2) sums_Im by auto 
  moreover have ‹(λn. Im (g n)) sums Im t›
    using assms(3) sums_Im by auto 
  ultimately have im: ‹Im s = Im t›
    using sums_unique2 by auto 
  from re im show ‹s ≤ t›
    using less_eq_complexI by auto 
qed

subsection ‹List indices and enum›

fun index_of where
  "index_of x [] = (0::nat)"
| "index_of x (y#ys) = (if x=y then 0 else (index_of x ys + 1))"

definition "enum_idx (x::'a::enum) = index_of x (enum_class.enum :: 'a list)"

lemma index_of_length: "index_of x y ≤ length y"
  apply (induction y) by auto

lemma index_of_correct:
  assumes "x ∈ set y"
  shows "y ! index_of x y = x"
  using assms apply (induction y arbitrary: x)
  by auto

lemma enum_idx_correct: 
  "Enum.enum ! enum_idx i = i"
proof-
  have "i ∈ set enum_class.enum"
    using UNIV_enum by blast 
  thus ?thesis
    unfolding enum_idx_def
    using index_of_correct by metis
qed

lemma index_of_bound: 
  assumes "y ≠ []" and "x ∈ set y"
  shows "index_of x y < length y"
  using assms proof(induction y arbitrary: x)
  case Nil
  thus ?case by auto
next
  case (Cons a y)
  show ?case 
  proof(cases "a = x")
    case True
    thus ?thesis by auto
  next
    case False
    moreover have "a ≠ x ⟹ index_of x y < length y"
      using Cons.IH Cons.prems(2) by fastforce      
    ultimately show ?thesis by auto
  qed
qed

lemma enum_idx_bound[simp]: "enum_idx x < CARD('a)" for x :: "'a::enum"
proof-
  have p1: "False"
    if "(Enum.enum :: 'a list) = []"
  proof-
    have "(UNIV::'a set) = set ([]::'a list)"
      using that UNIV_enum by metis
    also have "… = {}"
      by blast
    finally have "(UNIV::'a set) = {}".
    thus ?thesis by simp
  qed    
  have p2: "x ∈ set (Enum.enum :: 'a list)"
    using UNIV_enum by auto
  moreover have "(enum_class.enum::'a list) ≠ []"
    using p2 by auto
  ultimately show ?thesis
    unfolding enum_idx_def card_UNIV_length_enum
    using index_of_bound [where x = x and y = "(Enum.enum :: 'a list)"]
    by auto   
qed

lemma index_of_nth:
  assumes "distinct xs"
  assumes "i < length xs"
  shows "index_of (xs ! i) xs = i"
  using assms
  by (metis gr_implies_not_zero index_of_bound index_of_correct length_0_conv nth_eq_iff_index_eq nth_mem)

lemma enum_idx_enum: 
  assumes ‹i < CARD('a::enum)›
  shows ‹enum_idx (enum_class.enum ! i :: 'a) = i›
  unfolding enum_idx_def apply (rule index_of_nth)
  using assms by (simp_all add: card_UNIV_length_enum enum_distinct)

subsection ‹Filtering lists/sets›

lemma map_filter_map: "List.map_filter f (map g l) = List.map_filter (f o g) l"
  by (induction l) (simp_all split: option.split)

lemma map_filter_Some [simp]: "List.map_filter (λx. Some (f x)) l = map f l"
  by (simp add: List.map_filter_def)

lemma filter_Un: "Set.filter f (x ∪ y) = Set.filter f x ∪ Set.filter f y"
  by auto

lemma Set_filter_unchanged: "Set.filter P X = X" if "⋀x. x∈X ⟹ P x" for P and X :: "'z set"
  using that by auto

subsection ‹Maps›

definition "inj_map π = (∀x y. π x = π y ∧ π x ≠ None ⟶ x = y)"

definition "inv_map π = (λy. if Some y ∈ range π then Some (inv π (Some y)) else None)"

lemma inj_map_total[simp]: "inj_map (Some o π) = inj π"
  unfolding inj_map_def inj_def by simp

lemma inj_map_Some[simp]: "inj_map Some"
  by (simp add: inj_map_def)

lemma inv_map_total: 
  assumes "surj π"
  shows "inv_map (Some o π) = Some o inv π"
proof-
  have "(if Some y ∈ range (λx. Some (π x))
          then Some (SOME x. Some (π x) = Some y)
          else None) =
         Some (SOME b. π b = y)"
    if "surj π"
    for y
    using that by auto
  hence  "surj π ⟹
    (λy. if Some y ∈ range (λx. Some (π x))
         then Some (SOME x. Some (π x) = Some y) else None) =
    (λx. Some (SOME xa. π xa = x))"
    by (rule ext) 
  thus ?thesis 
    unfolding inv_map_def o_def inv_def
    using assms by linarith
qed

lemma inj_map_map_comp[simp]: 
  assumes a1: "inj_map f" and a2: "inj_map g" 
  shows "inj_map (f ∘⇩m g)"
  using a1 a2
  unfolding inj_map_def
  by (metis (mono_tags, lifting) map_comp_def option.case_eq_if option.expand)

lemma inj_map_inv_map[simp]: "inj_map (inv_map π)"
proof (unfold inj_map_def, rule allI, rule allI, rule impI, erule conjE)
  fix x y
  assume same: "inv_map π x = inv_map π y"
    and pix_not_None: "inv_map π x ≠ None"
  have x_pi: "Some x ∈ range π" 
    using pix_not_None unfolding inv_map_def apply auto
    by (meson option.distinct(1))
  have y_pi: "Some y ∈ range π" 
    using pix_not_None unfolding same unfolding inv_map_def apply auto
    by (meson option.distinct(1))
  have "inv_map π x = Some (Hilbert_Choice.inv π (Some x))"
    unfolding inv_map_def using x_pi by simp
  moreover have "inv_map π y = Some (Hilbert_Choice.inv π (Some y))"
    unfolding inv_map_def using y_pi by simp
  ultimately have "Hilbert_Choice.inv π (Some x) = Hilbert_Choice.inv π (Some y)"
    using same by simp
  thus "x = y"
    by (meson inv_into_injective option.inject x_pi y_pi)
qed

subsection ‹Lattices›

unbundle lattice_syntax

text ‹The following lemma is identical to @{thm [source] Complete_Lattices.uminus_Inf} 
  except for the more general sort.›
lemma uminus_Inf: "- (⨅A) = ⨆(uminus ` A)" for A :: ‹'a::complete_orthocomplemented_lattice set›
proof (rule order.antisym)
  show "- ⨅A ≤ ⨆(uminus ` A)"
    by (rule compl_le_swap2, rule Inf_greatest, rule compl_le_swap2, rule Sup_upper) simp
  show "⨆(uminus ` A) ≤ - ⨅A"
    by (rule Sup_least, rule compl_le_swap1, rule Inf_lower) auto
qed

text ‹The following lemma is identical to @{thm [source] Complete_Lattices.uminus_INF}
  except for the more general sort.›
lemma uminus_INF: "- (INF x∈A. B x) = (SUP x∈A. - B x)" for B :: ‹'a ⇒ 'b::complete_orthocomplemented_lattice›
  by (simp add: uminus_Inf image_image)

text ‹The following lemma is identical to @{thm [source] Complete_Lattices.uminus_Sup}
  except for the more general sort.›
lemma uminus_Sup: "- (⨆A) = ⨅(uminus ` A)" for A :: ‹'a::complete_orthocomplemented_lattice set›
  by (metis (no_types, lifting) uminus_INF image_cong image_ident ortho_involution)

text ‹The following lemma is identical to @{thm [source] Complete_Lattices.uminus_SUP}
  except for the more general sort.›
lemma uminus_SUP: "- (SUP x∈A. B x) = (INF x∈A. - B x)" for B :: ‹'a ⇒ 'b::complete_orthocomplemented_lattice›
  by (simp add: uminus_Sup image_image)

lemma has_sumI_metric:
  fixes l :: ‹'a :: {metric_space, comm_monoid_add}›
  assumes ‹⋀e. e > 0 ⟹ ∃X. finite X ∧ X ⊆ A ∧ (∀Y. finite Y ∧ X ⊆ Y ∧ Y ⊆ A ⟶ dist (sum f Y) l < e)›
  shows ‹(f has_sum l) A›
  unfolding has_sum_metric using assms by simp

lemma limitin_pullback_topology: 
  ‹limitin (pullback_topology A g T) f l F ⟷ l∈A ∧ (∀⇩F x in F. f x ∈ A) ∧ limitin T (g o f) (g l) F›
  apply (simp add: topspace_pullback_topology limitin_def openin_pullback_topology imp_ex flip: ex_simps(1))
  apply rule
   apply simp
   apply safe
  using eventually_mono apply fastforce
   apply (simp add: eventually_conj_iff)
  by (simp add: eventually_conj_iff)

lemma tendsto_coordinatewise: ‹(f ⤏ l) F ⟷ (∀x. ((λi. f i x) ⤏ l x) F)›
proof (intro iffI allI)
  assume asm: ‹(f ⤏ l) F›
  then show ‹((λi. f i x) ⤏ l x) F› for x
    apply (rule continuous_on_tendsto_compose[where s=UNIV, rotated])
    by auto
next
  assume asm: ‹(∀x. ((λi. f i x) ⤏ l x) F)›
  show ‹(f ⤏ l) F›
  proof (unfold tendsto_def, intro allI impI)
    fix S assume ‹open S› and ‹l ∈ S›
    from product_topology_open_contains_basis[OF ‹open S›[unfolded open_fun_def] ‹l ∈ S›]
    obtain U where lU: ‹l ∈ Pi UNIV U› and openU: ‹⋀x. open (U x)› and finiteD: ‹finite {x. U x ≠ UNIV}› and US: ‹Pi UNIV U ⊆ S›
      by (auto simp add: PiE_UNIV_domain)

    define D where ‹D = {x. U x ≠ UNIV}›
    with finiteD have finiteD: ‹finite D›
      by simp
    have PiUNIV: ‹t ∈ Pi UNIV U ⟷ (∀x∈D. t x ∈ U x)› for t
      using D_def by blast

    have f_Ui: ‹∀⇩F i in F. f i x ∈ U x› for x
      using asm[rule_format, of x] openU[of x]
      using lU topological_tendstoD by fastforce

    have ‹∀⇩F x in F. ∀i∈D. f x i ∈ U i›
      using finiteD
    proof induction
      case empty
      then show ?case
        by simp
    next
      case (insert x F)
      with f_Ui show ?case
        by (simp add: eventually_conj_iff)
    qed

    then show ‹∀⇩F x in F. f x ∈ S›
      using US by (simp add: PiUNIV eventually_mono in_mono)
  qed
qed

lemma limitin_closure_of:
  assumes limit: ‹limitin T f c F›
  assumes in_S: ‹∀⇩F x in F. f x ∈ S›
  assumes nontrivial: ‹¬ trivial_limit F›
  shows ‹c ∈ T closure_of S›
proof (intro in_closure_of[THEN iffD2] conjI impI allI)
  from limit show ‹c ∈ topspace T›
    by (simp add: limitin_topspace)
  fix U
  assume ‹c ∈ U ∧ openin T U›
  with limit have ‹∀⇩F x in F. f x ∈ U›
    by (simp add: limitin_def)
  with in_S have ‹∀⇩F x in F. f x ∈ U ∧ f x ∈ S›
    by (simp add: eventually_frequently_simps)
  with nontrivial
  show ‹∃y. y ∈ S ∧ y ∈ U›
    using eventually_happens' by blast
qed

subsection ‹Separating sets›

definition separating_set :: ‹(('a ⇒ 'b) ⇒ bool) ⇒ 'a set ⇒ bool› where
  ‹separating_set P S ⟷ (∀f g. P f ⟶ P g ⟶ (∀x∈S. f x = g x) ⟶ f = g)›

lemma separating_set_mono: ‹S ⊆ T ⟹ separating_set P S ⟹ separating_set P T›
  unfolding separating_set_def by fast

lemma separating_set_UNIV[simp]: ‹separating_set P UNIV›
  by (auto intro!: ext simp: separating_set_def)

lemma eq_from_separatingI:
  assumes ‹separating_set P S›
  assumes ‹P f› and ‹P g›
  assumes ‹⋀x. x ∈ S ⟹ f x = g x›
  shows ‹f = g›
  using assms by (simp add: separating_set_def)

lemma eq_from_separatingIx:
  ― ‹When using this as a rule, best instantiate \<^term>‹x› explicitly.›
  assumes ‹separating_set P S›
  assumes ‹P f› and ‹P g›
  assumes ‹⋀x. x ∈ S ⟹ f x = g x›
  shows ‹f x = g x›
  using assms eq_from_separatingI by blast

lemma eq_from_separatingI2:
  assumes ‹separating_set P ((λ(x,y). h x y) ` (S×T))›
  assumes ‹P f› and ‹P g›
  assumes ‹⋀x y. x ∈ S ⟹ y ∈ T ⟹ f (h x y) = g (h x y)›
  shows ‹f = g›
  apply (rule eq_from_separatingI[OF assms(1)])
  using assms(2-4) by auto

lemma eq_from_separatingI2x:
  ― ‹When using this as a rule, best instantiate \<^term>‹x› explicitly.›
  assumes ‹separating_set P ((λ(x,y). h x y) ` (S×T))›
  assumes ‹P f› and ‹P g›
  assumes ‹⋀x y. x ∈ S ⟹ y ∈ T ⟹ f (h x y) = g (h x y)›
  shows ‹f x = g x›
  using assms eq_from_separatingI2 by blast

lemma separating_setI:
  assumes ‹⋀f g. P f ⟹ P g ⟹ (⋀x. x∈S ⟹ f x = g x) ⟹ f = g›
  shows ‹separating_set P S›
  by (simp add: assms separating_set_def)

end