# 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"
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 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 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)"
proof (rule sum_mono2)
show "finite L"
using a1.
show "K ⊆ L"
using a2.
show "0 ≤ (f b)⇧2"
if "b ∈ L - K"
for b :: 'a
using that
by simp
qed
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"

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

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 (rule filter_leI)
show "eventually P (filtermap (λF. F ∩ A) (finite_subsets_at_top B))"
if "eventually P (finite_subsets_at_top A)"
for P :: "'a set ⇒ bool"
using that unfolding eventually_filtermap
unfolding eventually_finite_subsets_at_top
by (metis Int_subset_iff assms finite_Int inf_le2 subset_trans)
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

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›

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: "enum_idx x < length (Enum.enum :: 'a list)" 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
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

(* lemma abs_summable_bdd_above:
fixes f :: ‹'a ⇒ 'b::real_normed_vector›
shows ‹f abs_summable_on A ⟷ bdd_above (sum (λx. norm (f x)) ` {F. F⊆A ∧ finite F})›
proof (rule iffI)
assume ‹f abs_summable_on A›
have ‹(∑x∈F. norm (f x)) = (∑⇩∞x∈F. norm (f x))› if ‹finite F› for F
also have ‹(∑⇩∞x∈F. norm (f x)) ≤ (∑⇩∞x∈A. norm (f x))› if ‹F ⊆ A› for F
by (smt (verit) Diff_subset ‹f abs_summable_on A› infsum_Diff infsum_nonneg norm_ge_zero summable_on_subset_banach that)
finally show ‹bdd_above (sum (λx. norm (f x)) ` {F. F ⊆ A ∧ finite F})›
by (auto intro!: bdd_aboveI)
next
assume ‹bdd_above (sum (λx. norm (f x)) ` {F. F⊆A ∧ finite F})›
then show ‹f abs_summable_on A›
qed

lemma infsum_nonneg:
fixes f :: "'a ⇒ 'b::{ordered_comm_monoid_add,linorder_topology}"
assumes "⋀x. x ∈ M ⟹ 0 ≤ f x"
shows "infsum f M ≥ 0" (is "?lhs ≥ _")
apply (cases ‹f summable_on M›)
apply (rule infsum_nonneg)
using assms by (auto simp add: infsum_not_exists)

lemma abs_summable_product:
fixes x :: "'a ⇒ 'b::{real_normed_div_algebra,banach,second_countable_topology}"
assumes x2_sum: "(λi. (x i) * (x i)) abs_summable_on A"
and y2_sum: "(λi. (y i) * (y i)) abs_summable_on A"
shows "(λi. x i * y i) abs_summable_on A"
proof (rule nonneg_bdd_above_summable_on, simp, rule bdd_aboveI2, rename_tac F)
fix F assume ‹F ∈ {F. F ⊆ A ∧ finite F}›
then have r1: "finite F" and b4: "F ⊆ A"
by auto

have a1: "(∑⇩∞i∈F. norm (x i * x i)) ≤ (∑⇩∞i∈A. norm (x i * x i))"
apply (rule infsum_mono_neutral)
using b4 r1 x2_sum by auto

have "norm (x i * y i) ≤ norm (x i * x i) + norm (y i * y i)" for i
unfolding norm_mult
by (smt mult_left_mono mult_nonneg_nonneg mult_right_mono norm_ge_zero)
hence "(∑i∈F. norm (x i * y i)) ≤ (∑i∈F. norm (x i * x i) + norm (y i * y i))"