# 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›
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) ≠ -∞›
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)

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)

assumes "(UNIV::'a set) ≠ {0}"
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

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›

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 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

― ‹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})))›
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
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

― ‹This is a strengthening of @{thm [source] has_sum_comm_additive_general}.›
assumes f_sum: ‹⋀F. finite F ⟹ F ⊆ S ⟹ sum (f o g) F = f (sum g F)›
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

― ‹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)›
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])
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])
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

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›

lemma complex_of_real_leq_1_iff[iff]: ‹complex_of_real x ≤ 1 ⟷ x ≤ 1›

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

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"
proof (induction l)
show "List.map_filter f (map g []) = List.map_filter (f ∘ g) []"
show "List.map_filter f (map g (a # l)) = List.map_filter (f ∘ g) (a # l)"
if "List.map_filter f (map g l) = List.map_filter (f ∘ g) l"
for a :: 'c
and l :: "'c list"
using that  map_filter_simps(1)
by (metis comp_eq_dest_lhs list.simps(9))
qed

lemma map_filter_Some[simp]: "List.map_filter (λx. Some (f x)) l = map f l"
proof (induction l)
show "List.map_filter (λx. Some (f x)) [] = map f []"
show "List.map_filter (λx. Some (f x)) (a # l) = map f (a # l)"
if "List.map_filter (λx. Some (f x)) l = map f l"
for a :: 'b
and l :: "'b list"
using that by (simp add: map_filter_simps(1))
qed

lemma filter_Un: "Set.filter f (x ∪ y) = Set.filter f x ∪ Set.filter f y"
unfolding Set.filter_def 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 unfolding Set.filter_def 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"

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›

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›

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

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›

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
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›
fix U
assume ‹c ∈ U ∧ openin T U›
with limit have ‹∀⇩F x in F. f x ∈ U›