# Theory Extra_General

section ‹‹Extra_General› -- General missing things›

theory Extra_General
imports
"HOL-Library.Cardinality"
"HOL-Analysis.Elementary_Topology"
Jordan_Normal_Form.Conjugate
"HOL-Analysis.Uniform_Limit"
"HOL-Library.Set_Algebras"
"HOL-Types_To_Sets.Types_To_Sets"
begin

subsection ‹Misc›

lemma reals_zero_comparable_iff:
"(x::complex)∈ℝ ⟷ x ≤ 0 ∨ x ≥ 0"
unfolding complex_is_Real_iff less_eq_complex_def
by auto

lemma reals_zero_comparable:
fixes x::complex
assumes "x∈ℝ"
shows "x ≤ 0 ∨ x ≥ 0"
using assms unfolding reals_zero_comparable_iff 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 bdd_above_image_mono:
assumes ‹⋀x. x∈S ⟹ f x ≤ g x›
assumes ‹bdd_above (g  S)›
shows ‹bdd_above (f  S)›
by (smt (verit, ccfv_threshold) assms(1) assms(2) bdd_aboveI2 bdd_above_def order_trans rev_image_eqI)

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"
proof (cases x)
show "0 ≤ cnj x * x"
if "x = Complex x1 x2"
for x1 :: real
and x2 :: real
using that by (auto simp: complex_cnj complex_mult complex_of_real_def)
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: "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

end


# Theory Extra_Vector_Spaces

section ‹‹Extra_Vector_Spaces› -- Additional facts about vector spaces›

theory Extra_Vector_Spaces
imports
"HOL-Analysis.Inner_Product"
"HOL-Analysis.Euclidean_Space"
"HOL-Library.Indicator_Function"
"HOL-Analysis.Topology_Euclidean_Space"
"HOL-Analysis.Line_Segment"
Extra_General
begin

subsection ‹Euclidean spaces›

typedef 'a euclidean_space = "UNIV :: ('a ⇒ real) set" ..
setup_lifting type_definition_euclidean_space

instantiation euclidean_space :: (type) real_vector begin
lift_definition plus_euclidean_space ::
"'a euclidean_space ⇒ 'a euclidean_space ⇒ 'a euclidean_space"
is "λf g x. f x + g x" .
lift_definition zero_euclidean_space :: "'a euclidean_space" is "λ_. 0" .
lift_definition uminus_euclidean_space ::
"'a euclidean_space ⇒ 'a euclidean_space"
is "λf x. - f x" .
lift_definition minus_euclidean_space ::
"'a euclidean_space ⇒ 'a euclidean_space ⇒ 'a euclidean_space"
is "λf g x. f x - g x".
lift_definition scaleR_euclidean_space ::
"real ⇒ 'a euclidean_space ⇒ 'a euclidean_space"
is "λc f x. c * f x" .
instance
apply intro_classes
by (transfer; auto intro: distrib_left distrib_right)+
end

instantiation euclidean_space :: (finite) real_inner begin
lift_definition inner_euclidean_space :: "'a euclidean_space ⇒ 'a euclidean_space ⇒ real"
is "λf g. ∑x∈UNIV. f x * g x :: real" .
definition "norm_euclidean_space (x::'a euclidean_space) = sqrt (inner x x)"
definition "dist_euclidean_space (x::'a euclidean_space) y = norm (x-y)"
definition "sgn x = x /⇩R norm x" for x::"'a euclidean_space"
definition "uniformity = (INF e∈{0<..}. principal {(x::'a euclidean_space, y). dist x y < e})"
definition "open U = (∀x∈U. ∀⇩F (x'::'a euclidean_space, y) in uniformity. x' = x ⟶ y ∈ U)"
instance
proof intro_classes
fix x :: "'a euclidean_space"
and y :: "'a euclidean_space"
and z :: "'a euclidean_space"
show "dist (x::'a euclidean_space) y = norm (x - y)"
and "sgn (x::'a euclidean_space) = x /⇩R norm x"
and "uniformity = (INF e∈{0<..}. principal {(x, y). dist (x::'a euclidean_space) y < e})"
and "open U = (∀x∈U. ∀⇩F (x', y) in uniformity. (x'::'a euclidean_space) = x ⟶ y ∈ U)"
and "norm x = sqrt (inner x x)" for U
unfolding dist_euclidean_space_def norm_euclidean_space_def sgn_euclidean_space_def
uniformity_euclidean_space_def open_euclidean_space_def
by simp_all

show "inner x y = inner y x"
apply transfer
show "inner (x + y) z = inner x z + inner y z"
proof transfer
fix x y z::"'a ⇒ real"
have "(∑i∈UNIV. (x i + y i) * z i) = (∑i∈UNIV. x i * z i + y i * z i)"
thus "(∑i∈UNIV. (x i + y i) * z i) = (∑j∈UNIV. x j * z j) + (∑k∈UNIV. y k * z k)"
by (subst sum.distrib[symmetric])
qed

show "inner (r *⇩R x) y = r * (inner x y)" for r
proof transfer
fix r and x y::"'a⇒real"
have "(∑i∈UNIV. r * x i * y i) = (∑i∈UNIV. r * (x i * y i))"
thus "(∑i∈UNIV. r * x i * y i) = r * (∑j∈UNIV. x j * y j)"
by (subst sum_distrib_left)
qed
show "0 ≤ inner x x"
apply transfer
show "(inner x x = 0) = (x = 0)"
proof (transfer, rule)
fix f :: "'a ⇒ real"
assume "(∑i∈UNIV. f i * f i) = 0"
hence "f x * f x = 0" for x
apply (rule_tac sum_nonneg_eq_0_iff[THEN iffD1, rule_format, where A=UNIV and x=x])
by auto
thus "f = (λ_. 0)"
by auto
qed auto
qed
end

instantiation euclidean_space :: (finite) euclidean_space begin
lift_definition euclidean_space_basis_vector :: "'a ⇒ 'a euclidean_space" is
"λx. indicator {x}" .
definition "Basis_euclidean_space == (euclidean_space_basis_vector  UNIV)"
instance
proof intro_classes
fix u :: "'a euclidean_space"
and v :: "'a euclidean_space"
show "(Basis::'a euclidean_space set) ≠ {}"
unfolding Basis_euclidean_space_def by simp
show "finite (Basis::'a euclidean_space set)"
unfolding Basis_euclidean_space_def by simp
show "inner u v = (if u = v then 1 else 0)"
if "u ∈ Basis" and "v ∈ Basis"
using that unfolding Basis_euclidean_space_def
apply transfer apply auto
by (auto simp: indicator_def)
show "(∀v∈Basis. inner u v = 0) = (u = 0)"
unfolding Basis_euclidean_space_def
apply transfer
by auto
qed
end (* euclidean_space :: (finite) euclidean_space *)

lemma closure_bounded_linear_image_subset_eq:
assumes f: "bounded_linear f"
shows "closure (f  closure S) = closure (f  S)"
by (meson closed_closure closure_bounded_linear_image_subset closure_minimal closure_mono closure_subset f image_mono subset_antisym)

lemma not_singleton_real_normed_is_perfect_space[simp]: ‹class.perfect_space (open :: 'a::{not_singleton,real_normed_vector} set ⇒ bool)›
apply standard
by (metis UNIV_not_singleton clopen closed_singleton empty_not_insert)

end


# Theory Extra_Ordered_Fields

section ‹‹Extra_Ordered_Fields› -- Additional facts about ordered fields›

theory Extra_Ordered_Fields
imports Complex_Main
Jordan_Normal_Form.Conjugate (* Defines ordering for complex. We have to use theirs, otherwise there will be conflicts *)
begin

subsection‹Ordered Fields›
text ‹In this section we introduce some type classes for ordered rings/fields/etc.
that are weakenings of existing classes. Most theorems in this section are
copies of the eponymous theorems from Isabelle/HOL, except that they are now proven
requiring weaker type classes (usually the need for a total order is removed).

Since the lemmas are identical to the originals except for weaker type constraints,
we use the same names as for the original lemmas. (In fact, the new lemmas could replace
the original ones in Isabelle/HOL with at most minor incompatibilities.›

subsection ‹Missing from Orderings.thy›

text ‹This class is analogous to \<^class>‹unbounded_dense_linorder›, except that it does not require a total order›

class unbounded_dense_order = dense_order + no_top + no_bot

instance unbounded_dense_linorder ⊆ unbounded_dense_order ..

subsection ‹Missing from Rings.thy›

text ‹The existing class \<^class>‹abs_if› requires \<^term>‹¦a¦ = (if a < 0 then - a else a)›.
However, if \<^term>‹(<)› is not a total order, this condition is too strong when \<^term>‹a›
is incomparable with \<^term>‹0›. (Namely, it requires the absolute value to be
the identity on such elements. E.g., the absolute value for complex numbers does not
satisfy this.) The following class ‹partial_abs_if› is analogous to \<^class>‹abs_if›
but does not require anything if \<^term>‹a› is incomparable with \<^term>‹0›.›

class partial_abs_if = minus + uminus + ord + zero + abs +
assumes abs_neg: "a ≤ 0 ⟹ abs a = -a"
assumes abs_pos: "a ≥ 0 ⟹ abs a = a"

class ordered_semiring_1 = ordered_semiring + semiring_1
― ‹missing class analogous to \<^class>‹linordered_semiring_1› without requiring a total order›
begin

lemma convex_bound_le:
assumes "x ≤ a" and "y ≤ a" and "0 ≤ u" and "0 ≤ v" and "u + v = 1"
shows "u * x + v * y ≤ a"
proof-
from assms have "u * x + v * y ≤ u * a + v * a"
with assms show ?thesis
unfolding distrib_right[symmetric] by simp
qed

end

subclass (in linordered_semiring_1) ordered_semiring_1 ..

― ‹missing class analogous to \<^class>‹linordered_semiring_strict› without requiring a total order›
assumes mult_strict_left_mono: "a < b ⟹ 0 < c ⟹ c * a < c * b"
assumes mult_strict_right_mono: "a < b ⟹ 0 < c ⟹ a * c < b * c"
begin

subclass semiring_0_cancel ..

subclass ordered_semiring
proof
fix a b c :: 'a
assume t1: "a ≤ b" and t2: "0 ≤ c"
thus "c * a ≤ c * b"
unfolding le_less
using mult_strict_left_mono by (cases "c = 0") auto
from t2 show "a * c ≤ b * c"
unfolding le_less
by (metis local.antisym_conv2 local.mult_not_zero local.mult_strict_right_mono t1)
qed

lemma mult_pos_pos[simp]: "0 < a ⟹ 0 < b ⟹ 0 < a * b"
using mult_strict_left_mono [of 0 b a] by simp

lemma mult_pos_neg: "0 < a ⟹ b < 0 ⟹ a * b < 0"
using mult_strict_left_mono [of b 0 a] by simp

lemma mult_neg_pos: "a < 0 ⟹ 0 < b ⟹ a * b < 0"
using mult_strict_right_mono [of a 0 b] by simp

text ‹Strict monotonicity in both arguments›
lemma mult_strict_mono:
assumes t1: "a < b" and t2: "c < d" and t3: "0 < b" and t4: "0 ≤ c"
shows "a * c < b * d"
proof-
have "a * c < b * d"
by (metis local.dual_order.order_iff_strict local.dual_order.strict_trans2
local.mult_strict_left_mono local.mult_strict_right_mono local.mult_zero_right t1 t2 t3 t4)
thus ?thesis
using assms by blast
qed

text ‹This weaker variant has more natural premises›
lemma mult_strict_mono':
assumes "a < b" and "c < d" and "0 ≤ a" and "0 ≤ c"
shows "a * c < b * d"
by (rule mult_strict_mono) (insert assms, auto)

lemma mult_less_le_imp_less:
assumes t1: "a < b" and t2: "c ≤ d" and t3: "0 ≤ a" and t4: "0 < c"
shows "a * c < b * d"
using local.mult_strict_mono' local.mult_strict_right_mono local.order.order_iff_strict
t1 t2 t3 t4 by auto

lemma mult_le_less_imp_less:
assumes "a ≤ b" and "c < d" and "0 < a" and "0 ≤ c"
shows "a * c < b * d"
by (metis assms(1) assms(2) assms(3) assms(4) local.antisym_conv2 local.dual_order.strict_trans1
local.mult_strict_left_mono local.mult_strict_mono)

end

subclass (in linordered_semiring_strict) ordered_semiring_strict
proof
show "c * a < c * b"
if "a < b"
and "0 < c"
for a :: 'a
and b
and c
using that
show "a * c < b * c"
if "a < b"
and "0 < c"
for a :: 'a
and b
and c
using that
qed

class ordered_semiring_1_strict = ordered_semiring_strict + semiring_1
― ‹missing class analogous to \<^class>‹linordered_semiring_1_strict› without requiring
a total order›
begin

subclass ordered_semiring_1 ..

lemma convex_bound_lt:
assumes "x < a" and "y < a" and "0 ≤ u" and "0 ≤ v" and "u + v = 1"
shows "u * x + v * y < a"
proof -
from assms have "u * x + v * y < u * a + v * a"
by (cases "u = 0") (auto intro!: add_less_le_mono mult_strict_left_mono mult_left_mono)
with assms show ?thesis
unfolding distrib_right[symmetric] by simp
qed

end

subclass (in linordered_semiring_1_strict) ordered_semiring_1_strict ..

class ordered_comm_semiring_strict = comm_semiring_0 + ordered_cancel_ab_semigroup_add +
― ‹missing class analogous to \<^class>‹linordered_comm_semiring_strict› without requiring a total order›
assumes comm_mult_strict_left_mono: "a < b ⟹ 0 < c ⟹ c * a < c * b"
begin

subclass ordered_semiring_strict
proof
fix a b c :: 'a
assume "a < b" and "0 < c"
thus "c * a < c * b"
by (rule comm_mult_strict_left_mono)
thus "a * c < b * c"
by (simp only: mult.commute)
qed

subclass ordered_cancel_comm_semiring
proof
fix a b c :: 'a
assume "a ≤ b" and "0 ≤ c"
thus "c * a ≤ c * b"
unfolding le_less
using mult_strict_left_mono by (cases "c = 0") auto
qed

end

subclass (in linordered_comm_semiring_strict) ordered_comm_semiring_strict
apply standard

class ordered_ring_strict = ring + ordered_semiring_strict
― ‹missing class analogous to \<^class>‹linordered_ring_strict› without requiring a total order›
begin

subclass ordered_ring ..

lemma mult_strict_left_mono_neg: "b < a ⟹ c < 0 ⟹ c * a < c * b"
using mult_strict_left_mono [of b a "- c"] by simp

lemma mult_strict_right_mono_neg: "b < a ⟹ c < 0 ⟹ a * c < b * c"
using mult_strict_right_mono [of b a "- c"] by simp

lemma mult_neg_neg: "a < 0 ⟹ b < 0 ⟹ 0 < a * b"
using mult_strict_right_mono_neg [of a 0 b] by simp

end

lemmas mult_sign_intros =
mult_nonneg_nonneg mult_nonneg_nonpos
mult_nonpos_nonneg mult_nonpos_nonpos
mult_pos_pos mult_pos_neg
mult_neg_pos mult_neg_neg

subsection ‹Ordered fields›

class ordered_field = field + order + ordered_comm_semiring_strict + ordered_ab_group_add
+ partial_abs_if
― ‹missing class analogous to \<^class>‹linordered_field› without requiring a total order›
begin

lemma frac_less_eq:
"y ≠ 0 ⟹ z ≠ 0 ⟹ x / y < w / z ⟷ (x * z - w * y) / (y * z) < 0"
by (subst less_iff_diff_less_0) (simp add: diff_frac_eq )

lemma frac_le_eq:
"y ≠ 0 ⟹ z ≠ 0 ⟹ x / y ≤ w / z ⟷ (x * z - w * y) / (y * z) ≤ 0"
by (subst le_iff_diff_le_0) (simp add: diff_frac_eq )

lemmas sign_simps = algebra_simps zero_less_mult_iff mult_less_0_iff

lemmas (in -) sign_simps = algebra_simps zero_less_mult_iff mult_less_0_iff

text‹Simplify expressions equated with 1›

lemma zero_eq_1_divide_iff [simp]: "0 = 1 / a ⟷ a = 0"
by (cases "a = 0") (auto simp: field_simps)

lemma one_divide_eq_0_iff [simp]: "1 / a = 0 ⟷ a = 0"
using zero_eq_1_divide_iff[of a] by simp

text‹Simplify expressions such as ‹0 < 1/x› to ‹0 < x››

text‹Simplify quotients that are compared with the value 1.›

text ‹Conditional Simplification Rules: No Case Splits›

lemma eq_divide_eq_1 [simp]:
"(1 = b/a) = ((a ≠ 0 & a = b))"

lemma divide_eq_eq_1 [simp]:
"(b/a = 1) = ((a ≠ 0 & a = b))"

end (* class ordered_field *)

text ‹The following type class intends to capture some important properties
that are common both to the real and the complex numbers. The purpose is
to be able to state and prove lemmas that apply both to the real and the complex
numbers without needing to state the lemma twice.
›

class nice_ordered_field = ordered_field + zero_less_one + idom_abs_sgn +
assumes positive_imp_inverse_positive: "0 < a ⟹ 0 < inverse a"
and inverse_le_imp_le: "inverse a ≤ inverse b ⟹ 0 < a ⟹ b ≤ a"
and dense_le: "(⋀x. x < y ⟹ x ≤ z) ⟹ y ≤ z"
and nn_comparable: "0 ≤ a ⟹ 0 ≤ b ⟹ a ≤ b ∨ b ≤ a"
and abs_nn: "¦x¦ ≥ 0"
begin

subclass (in linordered_field) nice_ordered_field
proof
show "¦a¦ = - a"
if "a ≤ 0"
for a :: 'a
using that
by simp
show "¦a¦ = a"
if "0 ≤ a"
for a :: 'a
using that
by simp
show "0 < inverse a"
if "0 < a"
for a :: 'a
using that
by simp
show "b ≤ a"
if "inverse a ≤ inverse b"
and "0 < a"
for a :: 'a
and b
using that
using local.inverse_le_imp_le by blast
show "y ≤ z"
if "⋀x::'a. x < y ⟹ x ≤ z"
for y
and z
using that
using local.dense_le by blast
show "a ≤ b ∨ b ≤ a"
if "0 ≤ a"
and "0 ≤ b"
for a :: 'a
and b
using that
by auto
show "0 ≤ ¦x¦"
for x :: 'a
by simp
qed

lemma comparable:
assumes h1: "a ≤ c ∨ a ≥ c"
and h2: "b ≤ c ∨ b ≥ c"
shows "a ≤ b ∨ b ≤ a"
proof-
have "a ≤ b"
if t1: "¬ b ≤ a" and t2: "a ≤ c" and t3: "b ≤ c"
proof-
have "0 ≤ c-a"
moreover have "0 ≤ c-b"
ultimately have "c-a ≤ c-b ∨ c-a ≥ c-b" by (rule nn_comparable)
hence "-a ≤ -b ∨ -a ≥ -b"
thus ?thesis
qed
moreover have "a ≤ b"
if t1: "¬ b ≤ a" and t2: "c ≤ a" and t3: "b ≤ c"
proof-
have "b ≤ a"
using local.dual_order.trans t2 t3 by blast
thus ?thesis
using t1 by auto
qed
moreover have "a ≤ b"
if t1: "¬ b ≤ a" and t2: "c ≤ a" and t3: "c ≤ b"
proof-
have "0 ≤ a-c"
moreover have "0 ≤ b-c"
ultimately have "a-c ≤ b-c ∨ a-c ≥ b-c" by (rule nn_comparable)
hence "a ≤ b ∨ a ≥ b"
thus ?thesis
qed
ultimately show ?thesis using assms by auto
qed

lemma negative_imp_inverse_negative:
"a < 0 ⟹ inverse a < 0"
by (insert positive_imp_inverse_positive [of "-a"],

lemma inverse_positive_imp_positive:
assumes inv_gt_0: "0 < inverse a" and nz: "a ≠ 0"
shows "0 < a"
proof -
have "0 < inverse (inverse a)"
using inv_gt_0 by (rule positive_imp_inverse_positive)
thus "0 < a"
using nz by (simp add: nonzero_inverse_inverse_eq)
qed

lemma inverse_negative_imp_negative:
assumes inv_less_0: "inverse a < 0" and nz: "a ≠ 0"
shows "a < 0"
proof-
have "inverse (inverse a) < 0"
using inv_less_0 by (rule negative_imp_inverse_negative)
thus "a < 0" using nz by (simp add: nonzero_inverse_inverse_eq)
qed

lemma linordered_field_no_lb:
"∀x. ∃y. y < x"
proof
fix x::'a
have m1: "- (1::'a) < 0" by simp
have "(- 1) + x < x" by simp
thus "∃y. y < x" by blast
qed

lemma linordered_field_no_ub:
"∀x. ∃y. y > x"
proof
fix x::'a
have m1: " (1::'a) > 0" by simp
have "1 + x > x" by simp
thus "∃y. y > x" by blast
qed

lemma less_imp_inverse_less:
assumes less: "a < b" and apos:  "0 < a"
shows "inverse b < inverse a"
using assms by (metis local.dual_order.strict_iff_order
local.inverse_inverse_eq local.inverse_le_imp_le local.positive_imp_inverse_positive)

lemma inverse_less_imp_less:
"inverse a < inverse b ⟹ 0 < a ⟹ b < a"
using local.inverse_le_imp_le local.order.strict_iff_order by blast

text‹Both premises are essential. Consider -1 and 1.›
lemma inverse_less_iff_less [simp]:
"0 < a ⟹ 0 < b ⟹ inverse a < inverse b ⟷ b < a"
by (blast intro: less_imp_inverse_less dest: inverse_less_imp_less)

lemma le_imp_inverse_le:
"a ≤ b ⟹ 0 < a ⟹ inverse b ≤ inverse a"
by (force simp add: le_less less_imp_inverse_less)

lemma inverse_le_iff_le [simp]:
"0 < a ⟹ 0 < b ⟹ inverse a ≤ inverse b ⟷ b ≤ a"
by (blast intro: le_imp_inverse_le dest: inverse_le_imp_le)

text‹These results refer to both operands being negative.  The opposite-sign
case is trivial, since inverse preserves signs.›
lemma inverse_le_imp_le_neg:
"inverse a ≤ inverse b ⟹ b < 0 ⟹ b ≤ a"
by (metis local.inverse_le_imp_le local.inverse_minus_eq local.neg_0_less_iff_less
local.neg_le_iff_le)

lemma inverse_less_imp_less_neg:
"inverse a < inverse b ⟹ b < 0 ⟹ b < a"
using local.dual_order.strict_iff_order local.inverse_le_imp_le_neg by blast

lemma inverse_less_iff_less_neg [simp]:
"a < 0 ⟹ b < 0 ⟹ inverse a < inverse b ⟷ b < a"
by (metis local.antisym_conv2 local.inverse_less_imp_less_neg local.negative_imp_inverse_negative
local.nonzero_inverse_inverse_eq local.order.strict_implies_order)

lemma le_imp_inverse_le_neg:
"a ≤ b ⟹ b < 0 ⟹ inverse b ≤ inverse a"
by (force simp add: le_less less_imp_inverse_less_neg)

lemma inverse_le_iff_le_neg [simp]:
"a < 0 ⟹ b < 0 ⟹ inverse a ≤ inverse b ⟷ b ≤ a"
by (blast intro: le_imp_inverse_le_neg dest: inverse_le_imp_le_neg)

lemma one_less_inverse:
"0 < a ⟹ a < 1 ⟹ 1 < inverse a"
using less_imp_inverse_less [of a 1, unfolded inverse_1] .

lemma one_le_inverse:
"0 < a ⟹ a ≤ 1 ⟹ 1 ≤ inverse a"
using le_imp_inverse_le [of a 1, unfolded inverse_1] .

lemma pos_le_divide_eq [field_simps]:
assumes "0 < c"
shows "a ≤ b / c ⟷ a * c ≤ b"
using assms by (metis local.divide_eq_imp local.divide_inverse_commute
local.dual_order.order_iff_strict local.dual_order.strict_iff_order
local.mult_right_mono local.mult_strict_left_mono local.nonzero_divide_eq_eq
local.order.strict_implies_order local.positive_imp_inverse_positive)

lemma pos_less_divide_eq [field_simps]:
assumes "0 < c"
shows "a < b / c ⟷ a * c < b"
using assms local.dual_order.strict_iff_order local.nonzero_divide_eq_eq local.pos_le_divide_eq
by auto

lemma neg_less_divide_eq [field_simps]:
assumes "c < 0"
shows "a < b / c ⟷ b < a * c"
by (metis assms local.minus_divide_divide local.mult_minus_right local.neg_0_less_iff_less
local.neg_less_iff_less local.pos_less_divide_eq)

lemma neg_le_divide_eq [field_simps]:
assumes "c < 0"
shows "a ≤ b / c ⟷ b ≤ a * c"
by (metis assms local.dual_order.order_iff_strict local.dual_order.strict_iff_order
local.neg_less_divide_eq local.nonzero_divide_eq_eq)

lemma pos_divide_le_eq [field_simps]:
assumes "0 < c"
shows "b / c ≤ a ⟷ b ≤ a * c"
by (metis assms local.dual_order.strict_iff_order local.nonzero_eq_divide_eq
local.pos_le_divide_eq)

lemma pos_divide_less_eq [field_simps]:
assumes "0 < c"
shows "b / c < a ⟷ b < a * c"
by (metis assms local.minus_divide_left local.mult_minus_left local.neg_less_iff_less
local.pos_less_divide_eq)

lemma neg_divide_le_eq [field_simps]:
assumes "c < 0"
shows "b / c ≤ a ⟷ a * c ≤ b"
by (metis assms local.minus_divide_left local.mult_minus_left local.neg_le_divide_eq
local.neg_le_iff_le)

lemma neg_divide_less_eq [field_simps]:
assumes "c < 0"
shows "b / c < a ⟷ a * c < b"
using assms local.dual_order.strict_iff_order local.neg_divide_le_eq by auto

text‹The following ‹field_simps› rules are necessary, as minus is always moved atop of
division but we want to get rid of division.›

lemma pos_le_minus_divide_eq [field_simps]: "0 < c ⟹ a ≤ - (b / c) ⟷ a * c ≤ - b"
unfolding minus_divide_left by (rule pos_le_divide_eq)

lemma neg_le_minus_divide_eq [field_simps]: "c < 0 ⟹ a ≤ - (b / c) ⟷ - b ≤ a * c"
unfolding minus_divide_left by (rule neg_le_divide_eq)

lemma pos_less_minus_divide_eq [field_simps]: "0 < c ⟹ a < - (b / c) ⟷ a * c < - b"
unfolding minus_divide_left by (rule pos_less_divide_eq)

lemma neg_less_minus_divide_eq [field_simps]: "c < 0 ⟹ a < - (b / c) ⟷ - b < a * c"
unfolding minus_divide_left by (rule neg_less_divide_eq)

lemma pos_minus_divide_less_eq [field_simps]: "0 < c ⟹ - (b / c) < a ⟷ - b < a * c"
unfolding minus_divide_left by (rule pos_divide_less_eq)

lemma neg_minus_divide_less_eq [field_simps]: "c < 0 ⟹ - (b / c) < a ⟷ a * c < - b"
unfolding minus_divide_left by (rule neg_divide_less_eq)

lemma pos_minus_divide_le_eq [field_simps]: "0 < c ⟹ - (b / c) ≤ a ⟷ - b ≤ a * c"
unfolding minus_divide_left by (rule pos_divide_le_eq)

lemma neg_minus_divide_le_eq [field_simps]: "c < 0 ⟹ - (b / c) ≤ a ⟷ a * c ≤ - b"
unfolding minus_divide_left by (rule neg_divide_le_eq)

lemma frac_less_eq:
"y ≠ 0 ⟹ z ≠ 0 ⟹ x / y < w / z ⟷ (x * z - w * y) / (y * z) < 0"
by (subst less_iff_diff_less_0) (simp add: diff_frac_eq )

lemma frac_le_eq:
"y ≠ 0 ⟹ z ≠ 0 ⟹ x / y ≤ w / z ⟷ (x * z - w * y) / (y * z) ≤ 0"
by (subst le_iff_diff_le_0) (simp add: diff_frac_eq )

text‹Lemmas ‹sign_simps› is a first attempt to automate proofs
of positivity/negativity needed for ‹field_simps›. Have not added ‹sign_simps› to ‹field_simps›
because the former can lead to case explosions.›

lemma divide_pos_pos[simp]:
"0 < x ⟹ 0 < y ⟹ 0 < x / y"

lemma divide_nonneg_pos:
"0 ≤ x ⟹ 0 < y ⟹ 0 ≤ x / y"

lemma divide_neg_pos:
"x < 0 ⟹ 0 < y ⟹ x / y < 0"

lemma divide_nonpos_pos:
"x ≤ 0 ⟹ 0 < y ⟹ x / y ≤ 0"

lemma divide_pos_neg:
"0 < x ⟹ y < 0 ⟹ x / y < 0"

lemma divide_nonneg_neg:
"0 ≤ x ⟹ y < 0 ⟹ x / y ≤ 0"

lemma divide_neg_neg:
"x < 0 ⟹ y < 0 ⟹ 0 < x / y"

lemma divide_nonpos_neg:
"x ≤ 0 ⟹ y < 0 ⟹ 0 ≤ x / y"

lemma divide_strict_right_mono:
"a < b ⟹ 0 < c ⟹ a / c < b / c"
by (simp add: less_imp_not_eq2 divide_inverse mult_strict_right_mono
positive_imp_inverse_positive)

lemma divide_strict_right_mono_neg:
"b < a ⟹ c < 0 ⟹ a / c < b / c"

text‹The last premise ensures that \<^term>‹a› and \<^term>‹b›
have the same sign›
lemma divide_strict_left_mono:
"b < a ⟹ 0 < c ⟹ 0 < a*b ⟹ c / a < c / b"
by (metis local.divide_neg_pos local.dual_order.strict_iff_order local.frac_less_eq local.less_iff_diff_less_0 local.mult_not_zero local.mult_strict_left_mono)

lemma divide_left_mono:
"b ≤ a ⟹ 0 ≤ c ⟹ 0 < a*b ⟹ c / a ≤ c / b"
using local.divide_cancel_left local.divide_strict_left_mono local.dual_order.order_iff_strict by auto

lemma divide_strict_left_mono_neg:
"a < b ⟹ c < 0 ⟹ 0 < a*b ⟹ c / a < c / b"
by (metis local.divide_strict_left_mono local.minus_divide_left local.neg_0_less_iff_less local.neg_less_iff_less mult_commute)

lemma mult_imp_div_pos_le: "0 < y ⟹ x ≤ z * y ⟹ x / y ≤ z"
by (subst pos_divide_le_eq, assumption+)

lemma mult_imp_le_div_pos: "0 < y ⟹ z * y ≤ x ⟹ z ≤ x / y"

lemma mult_imp_div_pos_less: "0 < y ⟹ x < z * y ⟹ x / y < z"

lemma mult_imp_less_div_pos: "0 < y ⟹ z * y < x ⟹ z < x / y"

lemma frac_le: "0 ≤ x ⟹ x ≤ y ⟹ 0 < w ⟹ w ≤ z  ⟹ x / z ≤ y / w"
using local.mult_imp_div_pos_le local.mult_imp_le_div_pos local.mult_mono by auto

lemma frac_less: "0 ≤ x ⟹ x < y ⟹ 0 < w ⟹ w ≤ z ⟹ x / z < y / w"
proof-
assume a1: "w ≤ z"
assume a2: "0 < w"
assume a3: "0 ≤ x"
assume a4: "x < y"
have f5: "a = 0 ∨ (b = c / a) = (b * a = c)"
for a b c::'a
by (meson local.nonzero_eq_divide_eq)
have f6: "0 < z"
using a2 a1 by (meson local.order.ordering_axioms ordering.strict_trans2)
have "z ≠ 0"
using a2 a1 by (meson local.leD)
moreover have "x / z ≠ y / w"
using a1 a2 a3 a4 local.frac_eq_eq local.mult_less_le_imp_less by fastforce
ultimately have "x / z ≠ y / w"
using f5 by (metis (no_types))
thus ?thesis
using a4 a3 a2 a1 by (meson local.frac_le local.order.not_eq_order_implies_strict
local.order.strict_implies_order)
qed

lemma frac_less2: "0 < x ⟹ x ≤ y ⟹ 0 < w ⟹ w < z  ⟹ x / z < y / w"
by (metis local.antisym_conv2 local.divide_cancel_left local.dual_order.strict_implies_order
local.frac_le local.frac_less)

lemma less_half_sum: "a < b ⟹ a < (a+b) / (1+1)"

lemma gt_half_sum: "a < b ⟹ (a+b)/(1+1) < b"

subclass unbounded_dense_order
proof
fix x y :: 'a
have less_add_one: "a < a + 1" for a::'a by auto
from less_add_one show "∃y. x < y"
by blast

from less_add_one have "x + (- 1) < (x + 1) + (- 1)"
hence "x - 1 < x + 1 - 1" by simp
hence "x - 1 < x" by (simp add: algebra_simps)
thus "∃y. y < x" ..
show "x < y ⟹ ∃z>x. z < y" by (blast intro!: less_half_sum gt_half_sum)
qed

lemma dense_le_bounded:
fixes x y z :: 'a
assumes "x < y"
and *: "⋀w. ⟦ x < w ; w < y ⟧ ⟹ w ≤ z"
shows "y ≤ z"
proof (rule dense_le)
fix w assume "w < y"
from dense[OF ‹x < y›] obtain u where "x < u" "u < y" by safe
have "u ≤ w ∨ w ≤ u"
using ‹u < y› ‹w < y› comparable local.order.strict_implies_order by blast
thus "w ≤ z"
using "*" ‹u < y› ‹w < y› ‹x < u› local.dual_order.trans local.order.strict_trans2 by blast
qed

subclass field_abs_sgn ..

lemma nonzero_abs_inverse:
"a ≠ 0 ⟹ ¦inverse a¦ = inverse ¦a¦"
by (rule abs_inverse)

lemma nonzero_abs_divide:
"b ≠ 0 ⟹ ¦a / b¦ = ¦a¦ / ¦b¦"
by (rule abs_divide)

lemma field_le_epsilon:
assumes e: "⋀e. 0 < e ⟹ x ≤ y + e"
shows "x ≤ y"
proof (rule dense_le)
fix t assume "t < x"
hence "0 < x - t" by (simp add: less_diff_eq)
from e [OF this] have "x + 0 ≤ x + (y - t)" by (simp add: algebra_simps)
hence "0 ≤ y - t" by (simp only: add_le_cancel_left)
thus "t ≤ y" by (simp add: algebra_simps)
qed

lemma inverse_positive_iff_positive [simp]:
"(0 < inverse a) = (0 < a)"
using local.positive_imp_inverse_positive by fastforce

lemma inverse_negative_iff_negative [simp]:
"(inverse a < 0) = (a < 0)"
using local.negative_imp_inverse_negative by fastforce

lemma inverse_nonnegative_iff_nonnegative [simp]:
"0 ≤ inverse a ⟷ 0 ≤ a"

lemma inverse_nonpositive_iff_nonpositive [simp]:
"inverse a ≤ 0 ⟷ a ≤ 0"
using local.inverse_nonnegative_iff_nonnegative local.neg_0_le_iff_le by fastforce

lemma one_less_inverse_iff: "1 < inverse x ⟷ 0 < x ∧ x < 1"
using less_trans[of 1 x 0 for x]
by (metis local.dual_order.strict_trans local.inverse_1 local.inverse_less_imp_less local.inverse_positive_iff_positive local.one_less_inverse local.zero_less_one)

lemma one_le_inverse_iff: "1 ≤ inverse x ⟷ 0 < x ∧ x ≤ 1"
by (metis local.dual_order.strict_trans1 local.inverse_1 local.inverse_le_imp_le local.inverse_positive_iff_positive local.one_le_inverse local.zero_less_one)

lemma inverse_less_1_iff: "inverse x < 1 ⟷ x ≤ 0 ∨ 1 < x"
proof (rule)
assume invx1: "inverse x < 1"
have "inverse x ≤ 0 ∨ inverse x ≥ 0"
using comparable invx1 local.order.strict_implies_order local.zero_less_one by blast
then consider (leq0) "inverse x ≤ 0" | (pos) "inverse x > 0" | (zero) "inverse x = 0"
using local.antisym_conv1 by blast
thus "x ≤ 0 ∨ 1 < x"
by (metis invx1 local.eq_iff local.inverse_1 local.inverse_less_imp_less
local.inverse_nonpositive_iff_nonpositive local.inverse_positive_imp_positive)
next
assume "x ≤ 0 ∨ 1 < x"
then consider (neg) "x ≤ 0" | (g1) "1 < x" by auto
thus "inverse x < 1"
by (metis local.dual_order.not_eq_order_implies_strict local.dual_order.strict_trans
local.inverse_1 local.inverse_negative_iff_negative local.inverse_zero
local.less_imp_inverse_less local.zero_less_one)
qed

lemma inverse_le_1_iff: "inverse x ≤ 1 ⟷ x ≤ 0 ∨ 1 ≤ x"
by (metis local.dual_order.order_iff_strict local.inverse_1 local.inverse_le_iff_le
local.inverse_less_1_iff local.one_le_inverse_iff)

text‹Simplify expressions such as ‹0 < 1/x› to ‹0 < x››

lemma zero_le_divide_1_iff [simp]:
"0 ≤ 1 / a ⟷ 0 ≤ a"
using local.dual_order.order_iff_strict local.inverse_eq_divide
local.inverse_positive_iff_positive by auto

lemma zero_less_divide_1_iff [simp]:
"0 < 1 / a ⟷ 0 < a"

lemma divide_le_0_1_iff [simp]:
"1 / a ≤ 0 ⟷ a ≤ 0"
by (smt local.abs_0 local.abs_1 local.abs_divide local.abs_neg local.abs_nn
local.divide_cancel_left local.le_minus_iff local.minus_divide_right local.zero_neq_one)

lemma divide_less_0_1_iff [simp]:
"1 / a < 0 ⟷ a < 0"
using local.dual_order.strict_iff_order by auto

lemma divide_right_mono:
"a ≤ b ⟹ 0 ≤ c ⟹ a/c ≤ b/c"
using local.divide_cancel_right local.divide_strict_right_mono local.dual_order.order_iff_strict by blast

lemma divide_right_mono_neg: "a ≤ b
⟹ c ≤ 0 ⟹ b / c ≤ a / c"
by (metis local.divide_cancel_right local.divide_strict_right_mono_neg local.dual_order.strict_implies_order local.eq_refl local.le_imp_less_or_eq)

lemma divide_left_mono_neg: "a ≤ b
⟹ c ≤ 0 ⟹ 0 < a * b ⟹ c / a ≤ c / b"
by (metis local.divide_left_mono local.minus_divide_left local.neg_0_le_iff_le local.neg_le_iff_le mult_commute)

lemma divide_nonneg_nonneg [simp]:
"0 ≤ x ⟹ 0 ≤ y ⟹ 0 ≤ x / y"
using local.divide_eq_0_iff local.divide_nonneg_pos local.dual_order.order_iff_strict by blast

lemma divide_nonpos_nonpos:
"x ≤ 0 ⟹ y ≤ 0 ⟹ 0 ≤ x / y"
using local.divide_nonpos_neg local.dual_order.order_iff_strict by auto

lemma divide_nonneg_nonpos:
"0 ≤ x ⟹ y ≤ 0 ⟹ x / y ≤ 0"
by (metis local.divide_eq_0_iff local.divide_nonneg_neg local.dual_order.order_iff_strict)

lemma divide_nonpos_nonneg:
"x ≤ 0 ⟹ 0 ≤ y ⟹ x / y ≤ 0"
using local.divide_nonpos_pos local.dual_order.order_iff_strict by auto

text ‹Conditional Simplification Rules: No Case Splits›

lemma le_divide_eq_1_pos [simp]:
"0 < a ⟹ (1 ≤ b/a) = (a ≤ b)"

lemma le_divide_eq_1_neg [simp]:
"a < 0 ⟹ (1 ≤ b/a) = (b ≤ a)"
by (metis local.le_divide_eq_1_pos local.minus_divide_divide local.neg_0_less_iff_less local.neg_le_iff_le)

lemma divide_le_eq_1_pos [simp]:
"0 < a ⟹ (b/a ≤ 1) = (b ≤ a)"
using local.pos_divide_le_eq by auto

lemma divide_le_eq_1_neg [simp]:
"a < 0 ⟹ (b/a ≤ 1) = (a ≤ b)"
by (metis local.divide_le_eq_1_pos local.minus_divide_divide local.neg_0_less_iff_less
local.neg_le_iff_le)

lemma less_divide_eq_1_pos [simp]:
"0 < a ⟹ (1 < b/a) = (a < b)"

lemma less_divide_eq_1_neg [simp]:
"a < 0 ⟹ (1 < b/a) = (b < a)"
using local.dual_order.strict_iff_order by auto

lemma divide_less_eq_1_pos [simp]:
"0 < a ⟹ (b/a < 1) = (b < a)"
using local.divide_le_eq_1_pos local.dual_order.strict_iff_order by auto

lemma divide_less_eq_1_neg [simp]:
"a < 0 ⟹ b/a < 1 ⟷ a < b"
using local.dual_order.strict_iff_order by auto

lemma abs_div_pos: "0 < y ⟹
¦x¦ / y = ¦x / y¦"

lemma zero_le_divide_abs_iff [simp]: "(0 ≤ a / ¦b¦) = (0 ≤ a | b = 0)"
proof
assume assm: "0 ≤ a / ¦b¦"
have absb: "abs b ≥ 0" by (fact abs_nn)
thus "0 ≤ a ∨ b = 0"
using absb assm local.abs_eq_0_iff local.mult_nonneg_nonneg by fastforce
next
assume "0 ≤ a ∨ b = 0"
then consider (a) "0 ≤ a" | (b) "b = 0" by atomize_elim auto
thus "0 ≤ a / ¦b¦"
by (metis local.abs_eq_0_iff local.abs_nn local.divide_eq_0_iff local.divide_nonneg_nonneg)
qed

lemma divide_le_0_abs_iff [simp]: "(a / ¦b¦ ≤ 0) = (a ≤ 0 | b = 0)"
by (metis local.minus_divide_left local.neg_0_le_iff_le local.zero_le_divide_abs_iff)

text‹For creating values between \<^term>‹u› and \<^term>‹v›.›
lemma scaling_mono:
assumes "u ≤ v" and "0 ≤ r" and "r ≤ s"
shows "u + r * (v - u) / s ≤ v"
proof -
have "r/s ≤ 1" using assms
by (metis local.divide_le_eq_1_pos local.division_ring_divide_zero
local.dual_order.order_iff_strict local.dual_order.trans local.zero_less_one)
hence "(r/s) * (v - u) ≤ 1 * (v - u)"
using assms(1) local.diff_ge_0_iff_ge local.mult_right_mono by blast
thus ?thesis
qed

end (* class nice_ordered_field *)

code_identifier
code_module Ordered_Fields ⇀ (SML) Arith and (OCaml) Arith and (Haskell) Arith

subsection‹Ordered Complex›

declare Conjugate.less_eq_complex_def[simp del]
declare Conjugate.less_complex_def[simp del]

subsection ‹Ordering on complex numbers›

instantiation complex :: nice_ordered_field begin
instance
proof intro_classes
note defs = less_eq_complex_def less_complex_def abs_complex_def
fix x y z a b c :: complex
show "a ≤ 0 ⟹ ¦a¦ = - a" unfolding defs
show "0 ≤ a ⟹ ¦a¦ = a"
unfolding defs
by (metis abs_of_nonneg cmod_eq_Re comp_apply complex.exhaust_sel complex_of_real_def zero_complex.simps(1) zero_complex.simps(2))
show "a < b ⟹ 0 < c ⟹ c * a < c * b" unfolding defs by auto
show "0 < (1::complex)" unfolding defs by simp
show "0 < a ⟹ 0 < inverse a" unfolding defs by auto
define ra ia rb ib rc ic where "ra = Re a" "ia = Im a" "rb = Re b" "ib = Im b" "rc = Re c" "ic = Im c"
note ri = this[symmetric]
hence "a = Complex ra ia" "b = Complex rb ib" "c = Complex rc ic" by auto
note ri = this ri
have "rb ≤ ra"
if "1 / ra ≤ (if rb = 0 then 0 else 1 / rb)"
and "ia = 0" and "0 < ra" and "ib = 0"
proof(cases "rb = 0")
case True
thus ?thesis
using that(3) by auto
next
case False
thus ?thesis
by (smt nice_ordered_field_class.frac_less2 that(1) that(3))
qed
thus "inverse a ≤ inverse b ⟹ 0 < a ⟹ b ≤ a" unfolding defs ri
by (auto simp: power2_eq_square)
show "(⋀a. a < b ⟹ a ≤ c) ⟹ b ≤ c" unfolding defs ri
by (metis complex.sel(1) complex.sel(2) dense less_le_not_le
nice_ordered_field_class.linordered_field_no_lb not_le_imp_less)
show "0 ≤ a ⟹ 0 ≤ b ⟹ a ≤ b ∨ b ≤ a" unfolding defs by auto
show "0 ≤ ¦x¦" unfolding defs by auto
qed
end

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 complex_of_real_mono:
"x ≤ y ⟹ complex_of_real x ≤ complex_of_real y"
unfolding less_eq_complex_def by auto

lemma complex_of_real_mono_iff[simp]:
"complex_of_real x ≤ complex_of_real y ⟷ x ≤ y"
unfolding less_eq_complex_def by auto

lemma complex_of_real_strict_mono_iff[simp]:
"complex_of_real x < complex_of_real y ⟷ x < y"
unfolding less_complex_def by auto

lemma complex_of_real_nn_iff[simp]:
"0 ≤ complex_of_real y ⟷ 0 ≤ y"
unfolding less_eq_complex_def by auto

lemma complex_of_real_pos_iff[simp]:
"0 < complex_of_real y ⟷ 0 < y"
unfolding less_complex_def by auto

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: assumes "x ≥ 0" shows "complex_of_real (cmod x) = x"
by (metis Reals_cases abs_of_nonneg assms comp_Im_same complex_is_Real_iff complex_of_real_nn_iff norm_of_real zero_complex.simps(2))

end


# Theory Extra_Lattice

section ‹‹Extra_Lattice› -- Additional results about lattices›

theory Extra_Lattice
imports Main
begin

subsection‹‹Lattice_Missing› -- Miscellaneous missing facts about lattices›

text ‹Two bundles to activate and deactivate lattice specific notation (e.g., ‹⊓› etc.).
Activate the notation locally via "@{theory_text ‹includes lattice_notation›}" in a lemma statement.
(Or sandwich a declaration using that notation between "@{theory_text ‹unbundle lattice_notation ... unbundle no_lattice_notation›}.)›

bundle lattice_notation begin
notation inf (infixl "⊓" 70)
notation sup (infixl "⊔" 65)
notation Inf ("⨅")
notation Sup ("⨆")
notation bot ("⊥")
notation top ("⊤")
end

bundle no_lattice_notation begin
notation inf (infixl "⊓" 70)
notation sup (infixl "⊔" 65)
notation Inf ("⨅")
notation Sup ("⨆")
notation bot ("⊥")
notation top ("⊤")
end

unbundle lattice_notation

text ‹The following class ‹complemented_lattice› describes complemented lattices (with
\<^const>‹uminus› for the complement). The definition follows
🌐‹https://en.wikipedia.org/wiki/Complemented_lattice#Definition_and_basic_properties›.
\<^const>‹minus› in terms of the complement.›

class complemented_lattice = bounded_lattice + uminus + minus +
assumes inf_compl_bot[simp]: "inf x (-x) = bot"
and sup_compl_top[simp]: "sup x (-x) = top"
and diff_eq:  "x - y = inf x (- y)" begin

lemma dual_complemented_lattice:
"class.complemented_lattice (λx y. x ⊔ (- y)) uminus sup greater_eq greater inf ⊤ ⊥"
proof (rule class.complemented_lattice.intro)
show "class.bounded_lattice (⊔) (λx y. (y::'a) ≤ x) (λx y. y < x) (⊓) ⊤ ⊥"
by (rule dual_bounded_lattice)
show "class.complemented_lattice_axioms (λx y. (x::'a) ⊔ - y) uminus (⊔) (⊓) ⊤ ⊥"
by (unfold_locales, auto simp add: diff_eq)
qed

lemma compl_inf_bot [simp]: "inf (- x) x = bot"

lemma compl_sup_top [simp]: "sup (- x) x = top"

end

class complete_complemented_lattice = complemented_lattice + complete_lattice

text ‹The following class ‹complemented_lattice› describes orthocomplemented lattices,
following   🌐‹https://en.wikipedia.org/wiki/Complemented_lattice#Orthocomplementation›.›
class orthocomplemented_lattice = complemented_lattice +
assumes ortho_involution[simp]: "- (- x) = x"
and ortho_antimono: "x ≤ y ⟹ -x ≥ -y" begin

lemma dual_orthocomplemented_lattice:
"class.orthocomplemented_lattice (λx y. x ⊔ - y) uminus sup greater_eq greater inf ⊤ ⊥"
proof (rule class.orthocomplemented_lattice.intro)
show "class.complemented_lattice (λx y. (x::'a) ⊔ - y) uminus (⊔) (λx y. y ≤ x) (λx y. y < x) (⊓) ⊤ ⊥"
by (rule dual_complemented_lattice)
show "class.orthocomplemented_lattice_axioms uminus (λx y. (y::'a) ≤ x)"
by (unfold_locales, auto simp add: diff_eq intro: ortho_antimono)
qed

lemma compl_eq_compl_iff [simp]: "- x = - y ⟷ x = y"
by (metis ortho_involution)

lemma compl_bot_eq [simp]: "- bot = top"
by (metis inf_compl_bot inf_top_left ortho_involution)

lemma compl_top_eq [simp]: "- top = bot"
using compl_bot_eq ortho_involution by blast

text ‹De Morgan's law›
(* Proof from: https://planetmath.org/orthocomplementedlattice *)
lemma compl_sup [simp]: "- (x ⊔ y) = - x ⊓ - y"
proof -
have "- (x ⊔ y) ≤ - x"
moreover have "- (x ⊔ y) ≤ - y"
ultimately have 1: "- (x ⊔ y) ≤ - x ⊓ - y"
have ‹x ≤ - (-x ⊓ -y)›
by (metis inf.cobounded1 ortho_antimono ortho_involution)
moreover have ‹y ≤ - (-x ⊓ -y)›
by (metis inf.cobounded2 ortho_antimono ortho_involution)
ultimately have ‹x ⊔ y ≤ - (-x ⊓ -y)›
by auto
hence 2: ‹-x ⊓ -y ≤ - (x ⊔ y)›
using ortho_antimono by fastforce
from 1 2 show ?thesis
qed

text ‹De Morgan's law›
lemma compl_inf [simp]: "- (x ⊓ y) = - x ⊔ - y"
using compl_sup
by (metis ortho_involution)

lemma compl_mono:
assumes "x ≤ y"
shows "- y ≤ - x"

lemma compl_le_compl_iff [simp]: "- x ≤ - y ⟷ y ≤ x"
by (auto dest: compl_mono)

lemma compl_le_swap1:
assumes "y ≤ - x"
shows "x ≤ -y"
using assms ortho_antimono by fastforce

lemma compl_le_swap2:
assumes "- y ≤ x"
shows "- x ≤ y"
using assms local.ortho_antimono by fastforce

lemma compl_less_compl_iff[simp]: "- x < - y ⟷ y < x"

lemma compl_less_swap1:
assumes "y < - x"
shows "x < - y"
using assms compl_less_compl_iff by fastforce

lemma compl_less_swap2:
assumes "- y < x"
shows "- x < y"
using assms compl_le_swap1 compl_le_swap2 less_le_not_le by auto

lemma sup_cancel_left1: "sup (sup x a) (sup (- x) b) = top"

lemma sup_cancel_left2: "sup (sup (- x) a) (sup x b) = top"

lemma inf_cancel_left1: "inf (inf x a) (inf (- x) b) = bot"

lemma inf_cancel_left2: "inf (inf (- x) a) (inf x b) = bot"
using inf.left_commute inf_commute by auto

lemma sup_compl_top_left1 [simp]: "sup (- x) (sup x y) = top"

lemma sup_compl_top_left2 [simp]: "sup x (sup (- x) y) = top"
using sup_compl_top_left1[of "- x" y] by simp

lemma inf_compl_bot_left1 [simp]: "inf (- x) (inf x y) = bot"

lemma inf_compl_bot_left2 [simp]: "inf x (inf (- x) y) = bot"
using inf_compl_bot_left1[of "- x" y] by simp

lemma inf_compl_bot_right [simp]: "inf x (inf y (- x)) = bot"
by (subst inf_left_commute) simp

end

class complete_orthocomplemented_lattice = orthocomplemented_lattice + complete_lattice

instance complete_orthocomplemented_lattice ⊆ complete_complemented_lattice
by intro_classes

text ‹The following class ‹orthomodular_lattice› describes orthomodular lattices,
following   🌐‹https://en.wikipedia.org/wiki/Complemented_lattice#Orthomodular_lattices›.›
class orthomodular_lattice = orthocomplemented_lattice +
assumes orthomodular: "x ≤ y ⟹ sup x (inf (-x) y) = y" begin

lemma dual_orthomodular_lattice:
"class.orthomodular_lattice (λx y. x ⊔ - y) uminus sup greater_eq greater inf ⊤ ⊥"
proof (rule class.orthomodular_lattice.intro)
show "class.orthocomplemented_lattice (λx y. (x::'a) ⊔ - y) uminus (⊔) (λx y. y ≤ x) (λx y. y < x) (⊓) ⊤ ⊥"
by (rule dual_orthocomplemented_lattice)
show "class.orthomodular_lattice_axioms uminus (⊔) (λx y. (y::'a) ≤ x) (⊓)"
proof (unfold_locales)
show "(x::'a) ⊓ (- x ⊔ y) = y"
if "(y::'a) ≤ x"
for x :: 'a
and y :: 'a
using that local.compl_eq_compl_iff local.ortho_antimono local.orthomodular by fastforce
qed

qed

end

class complete_orthomodular_lattice = orthomodular_lattice + complete_lattice begin

end

instance complete_orthomodular_lattice ⊆ complete_orthocomplemented_lattice
by intro_classes

instance boolean_algebra ⊆ orthomodular_lattice
proof
fix x y :: 'a
show "sup (x::'a) (inf (- x) y) = y"
if "(x::'a) ≤ y"
using that
show "x - y = inf x (- y)"
qed auto

instance complete_boolean_algebra ⊆ complete_orthomodular_lattice
by intro_classes

lemma image_of_maximum:
fixes f::"'a::order ⇒ 'b::conditionally_complete_lattice"
assumes "mono f"
and "⋀x. x:M ⟹ x≤m"
and "m:M"
shows "(SUP x∈M. f x) = f m"
by (smt (verit, ccfv_threshold) assms(1) assms(2) assms(3) cSup_eq_maximum imageE imageI monoD)

lemma cSup_eq_cSup:
fixes A B :: ‹'a::conditionally_complete_lattice set›
assumes bdd: ‹bdd_above A›
assumes B: ‹⋀a. a∈A ⟹ ∃b∈B. b ≥ a›
assumes A: ‹⋀b. b∈B ⟹ ∃a∈A. a ≥ b›
shows ‹Sup A = Sup B›
proof (cases ‹B = {}›)
case True
with A B have ‹A = {}›
by auto
with True show ?thesis by simp
next
case False
have ‹bdd_above B›
by (meson A bdd bdd_above_def order_trans)
have ‹A ≠ {}›
using A False by blast
moreover have ‹a ≤ Sup B› if ‹a ∈ A› for a
proof -
obtain b where ‹b ∈ B› and ‹b ≥ a›
using B ‹a ∈ A› by auto
then show ?thesis
apply (rule cSup_upper2)
using ‹bdd_above B› by simp
qed
moreover have ‹Sup B ≤ c› if ‹⋀a. a ∈ A ⟹ a ≤ c› for c
using False apply (rule cSup_least)
using A that by fastforce
ultimately show ?thesis
by (rule cSup_eq_non_empty)
qed

unbundle no_lattice_notation

end


# Theory Complex_Vector_Spaces0

(*  Based on HOL/Real_Vector_Spaces.thy by Brian Huffman, Johannes Hölzl
Adapted to the complex case by Dominique Unruh *)

section ‹‹Complex_Vector_Spaces0› -- Vector Spaces and Algebras over the Complex Numbers›

theory Complex_Vector_Spaces0
imports HOL.Real_Vector_Spaces HOL.Topological_Spaces HOL.Vector_Spaces
Complex_Main Jordan_Normal_Form.Conjugate
begin

(* Jordan_Normal_Form.Conjugate declares these as simps. Seems too aggressive to me. *)
declare less_complex_def[simp del]
declare less_eq_complex_def[simp del]

subsection ‹Complex vector spaces›

class scaleC = scaleR +
fixes scaleC :: "complex ⇒ 'a ⇒ 'a" (infixr "*⇩C" 75)
assumes scaleR_scaleC: "scaleR r = scaleC (complex_of_real r)"
begin

abbreviation divideC :: "'a ⇒ complex ⇒ 'a"  (infixl "'/⇩C" 70)
where "x /⇩C c ≡ inverse c *⇩C x"

end

class complex_vector = scaleC + ab_group_add +
assumes scaleC_add_right: "a *⇩C (x + y) = (a *⇩C x) + (a *⇩C y)"
and scaleC_add_left: "(a + b) *⇩C x = (a *⇩C x) + (b *⇩C x)"
and scaleC_scaleC[simp]: "a *⇩C (b *⇩C x) =  (a * b) *⇩C x"
and scaleC_one[simp]: "1 *⇩C x = x"

(* Not present in Real_Vector_Spaces *)
subclass (in complex_vector) real_vector

class complex_algebra = complex_vector + ring +
assumes mult_scaleC_left [simp]: "a *⇩C x * y = a *⇩C (x * y)"
and mult_scaleC_right [simp]: "x * a *⇩C y = a *⇩C (x * y)"

(* Not present in Real_Vector_Spaces *)
subclass (in complex_algebra) real_algebra

class complex_algebra_1 = complex_algebra + ring_1

(* Not present in Real_Vector_Spaces *)
subclass (in complex_algebra_1) real_algebra_1 ..

class complex_div_algebra = complex_algebra_1 + division_ring

(* Not present in Real_Vector_Spaces *)
subclass (in complex_div_algebra) real_div_algebra ..

class complex_field = complex_div_algebra + field

(* Not present in Real_Vector_Spaces *)
subclass (in complex_field) real_field ..

instantiation complex :: complex_field
begin

definition complex_scaleC_def [simp]: "scaleC a x = a * x"

instance
proof intro_classes
fix r :: real and a b x y :: complex
show "((*⇩R) r::complex ⇒ _) = (*⇩C) (complex_of_real r)"
show "a *⇩C (x + y) = a *⇩C x + a *⇩C y"
show "(a + b) *⇩C x = a *⇩C x + b *⇩C x"
show "a *⇩C b *⇩C x = (a * b) *⇩C x"
by simp
show "1 *⇩C x = x"
by simp
show "a *⇩C (x::complex) * y = a *⇩C (x * y)"
by simp
show "(x::complex) * a *⇩C y = a *⇩C (x * y)"
by simp
qed

end

locale clinear = Vector_Spaces.linear "scaleC::_⇒_⇒'a::complex_vector" "scaleC::_⇒_⇒'b::complex_vector"
begin

lemmas scaleC = scale

end

global_interpretation complex_vector: vector_space "scaleC :: complex ⇒ 'a ⇒ 'a :: complex_vector"
rewrites "Vector_Spaces.linear (*⇩C) (*⇩C) = clinear"
and "Vector_Spaces.linear (*) (*⇩C) = clinear"
defines cdependent_raw_def: cdependent = complex_vector.dependent
and crepresentation_raw_def: crepresentation = complex_vector.representation
and csubspace_raw_def: csubspace = complex_vector.subspace
and cspan_raw_def: cspan = complex_vector.span
and cextend_basis_raw_def: cextend_basis = complex_vector.extend_basis
and cdim_raw_def: cdim = complex_vector.dim
proof unfold_locales
show "Vector_Spaces.linear (*⇩C) (*⇩C) = clinear" "Vector_Spaces.linear (*) (*⇩C) = clinear"
by (force simp: clinear_def complex_scaleC_def[abs_def])+

(* Not needed since we did the global_interpretation with mandatory complex_vector-prefix:
hide_const (open)― ‹locale constants›
complex_vector.dependent
complex_vector.independent
complex_vector.representation
complex_vector.subspace
complex_vector.span
complex_vector.extend_basis
complex_vector.dim *)

abbreviation "cindependent x ≡ ¬ cdependent x"

global_interpretation complex_vector: vector_space_pair "scaleC::_⇒_⇒'a::complex_vector" "scaleC::_⇒_⇒'b::complex_vector"
rewrites  "Vector_Spaces.linear (*⇩C) (*⇩C) = clinear"
and "Vector_Spaces.linear (*) (*⇩C) = clinear"
defines cconstruct_raw_def: cconstruct = complex_vector.construct
proof unfold_locales
show "Vector_Spaces.linear (*) (*⇩C) = clinear"
unfolding clinear_def complex_scaleC_def by auto
qed (auto simp: clinear_def)

(* Not needed since we did the global_interpretation with mandatory complex_vector-prefix:
hide_const (open)― ‹locale constants›
complex_vector.construct *)

lemma clinear_compose: "clinear f ⟹ clinear g ⟹ clinear (g ∘ f)"
unfolding clinear_def by (rule Vector_Spaces.linear_compose)

text ‹Recover original theorem names›

lemmas scaleC_left_commute = complex_vector.scale_left_commute
lemmas scaleC_zero_left = complex_vector.scale_zero_left
lemmas scaleC_minus_left = complex_vector.scale_minus_left
lemmas scaleC_diff_left = complex_vector.scale_left_diff_distrib
lemmas scaleC_sum_left = complex_vector.scale_sum_left
lemmas scaleC_zero_right = complex_vector.scale_zero_right
lemmas scaleC_minus_right = complex_vector.scale_minus_right
lemmas scaleC_diff_right = complex_vector.scale_right_diff_distrib
lemmas scaleC_sum_right = complex_vector.scale_sum_right
lemmas scaleC_eq_0_iff = complex_vector.scale_eq_0_iff
lemmas scaleC_left_imp_eq = complex_vector.scale_left_imp_eq
lemmas scaleC_right_imp_eq = complex_vector.scale_right_imp_eq
lemmas scaleC_cancel_left = complex_vector.scale_cancel_left
lemmas scaleC_cancel_right = complex_vector.scale_cancel_right

lemma divideC_field_simps[field_simps]: (* In Real_Vector_Spaces, these lemmas are unnamed *)
"c ≠ 0 ⟹ a = b /⇩C c ⟷ c *⇩C a = b"
"c ≠ 0 ⟹ b /⇩C c = a ⟷ b = c *⇩C a"
"c ≠ 0 ⟹ a + b /⇩C c = (c *⇩C a + b) /⇩C c"
"c ≠ 0 ⟹ a /⇩C c + b = (a + c *⇩C b) /⇩C c"
"c ≠ 0 ⟹ a - b /⇩C c = (c *⇩C a - b) /⇩C c"
"c ≠ 0 ⟹ a /⇩C c - b = (a - c *⇩C b) /⇩C c"
"c ≠ 0 ⟹ - (a /⇩C c) + b = (- a + c *⇩C b) /⇩C c"
"c ≠ 0 ⟹ - (a /⇩C c) - b = (- a - c *⇩C b) /⇩C c"
for a b :: "'a :: complex_vector"

text ‹Legacy names -- omitted›

lemmas scaleC_left_diff_distrib = scaleC_diff_left
lemmas scaleC_right_diff_distrib = scaleC_diff_right *)

lemmas clinear_injective_0 = linear_inj_iff_eq_0
and clinear_injective_on_subspace_0 = linear_inj_on_iff_eq_0
and clinear_cmul = linear_scale
and clinear_scaleC = linear_scale_self
and csubspace_mul = subspace_scale
and cspan_linear_image = linear_span_image
and cspan_0 = span_zero
and cspan_mul = span_scale
and injective_scaleC = injective_scale

lemma scaleC_minus1_left [simp]: "scaleC (-1) x = - x"
for x :: "'a::complex_vector"
using scaleC_minus_left [of 1 x] by simp

lemma scaleC_2:
fixes x :: "'a::complex_vector"
shows "scaleC 2 x = x + x"

lemma scaleC_half_double [simp]:
fixes a :: "'a::complex_vector"
shows "(1 / 2) *⇩C (a + a) = a"
proof -
have "⋀r. r *⇩C (a + a) = (r * 2) *⇩C a"
by (metis scaleC_2 scaleC_scaleC)
thus ?thesis
by simp
qed

lemma clinear_scale_complex:
fixes c::complex shows "clinear f ⟹ f (c * b) = c * f b"
using complex_vector.linear_scale by fastforce

interpretation scaleC_left: additive "(λa. scaleC a x :: 'a::complex_vector)"

interpretation scaleC_right: additive "(λx. scaleC a x :: 'a::complex_vector)"

lemma nonzero_inverse_scaleC_distrib:
"a ≠ 0 ⟹ x ≠ 0 ⟹ inverse (scaleC a x) = scaleC (inverse a) (inverse x)"
for x :: "'a::complex_div_algebra"
by (rule inverse_unique) simp

lemma inverse_scaleC_distrib: "inverse (scaleC a x) = scaleC (inverse a) (inverse x)"
for x :: "'a::{complex_div_algebra,division_ring}"
by (metis inverse_zero nonzero_inverse_scaleC_distrib complex_vector.scale_eq_0_iff)

(* lemmas sum_constant_scaleC = real_vector.sum_constant_scale― ‹legacy name› *)

(* Defined in Real_Vector_Spaces:
named_theorems vector_add_divide_simps "to simplify sums of scaled vectors" *)

"v + (b / z) *⇩C w = (if z = 0 then v else (z *⇩C v + b *⇩C w) /⇩C z)"
"a *⇩C v + (b / z) *⇩C w = (if z = 0 then a *⇩C v else ((a * z) *⇩C v + b *⇩C w) /⇩C z)"
"(a / z) *⇩C v + w = (if z = 0 then w else (a *⇩C v + z *⇩C w) /⇩C z)"
"(a / z) *⇩C v + b *⇩C w = (if z = 0 then b *⇩C w else (a *⇩C v + (b * z) *⇩C w) /⇩C z)"
"v - (b / z) *⇩C w = (if z = 0 then v else (z *⇩C v - b *⇩C w) /⇩C z)"
"a *⇩C v - (b / z) *⇩C w = (if z = 0 then a *⇩C v else ((a * z) *⇩C v - b *⇩C w) /⇩C z)"
"(a / z) *⇩C v - w = (if z = 0 then -w else (a *⇩C v - z *⇩C w) /⇩C z)"
"(a / z) *⇩C v - b *⇩C w = (if z = 0 then -b *⇩C w else (a *⇩C v - (b * z) *⇩C w) /⇩C z)"
for v :: "'a :: complex_vector"

fixes x :: "'a :: complex_vector"
shows "(x = (u / v) *⇩C a) ⟷ (if v=0 then x = 0 else v *⇩C x = u *⇩C a)"
by auto (metis (no_types) divide_eq_1_iff divide_inverse_commute scaleC_one scaleC_scaleC)

fixes x :: "'a :: complex_vector"
shows "((u / v) *⇩C a = x) ⟷ (if v=0 then x = 0 else u *⇩C a = v *⇩C x)"
by (metis ceq_vector_fraction_iff)

lemma complex_vector_affinity_eq:
fixes x :: "'a :: complex_vector"
assumes m0: "m ≠ 0"
shows "m *⇩C x + c = y ⟷ x = inverse m *⇩C y - (inverse m *⇩C c)"
(is "?lhs ⟷ ?rhs")
proof
assume ?lhs
hence "m *⇩C x = y - c" by (simp add: field_simps)
hence "inverse m *⇩C (m *⇩C x) = inverse m *⇩C (y - c)" by simp
thus "x = inverse m *⇩C y - (inverse m *⇩C c)"
using m0
next
assume ?rhs
with m0 show "m *⇩C x + c = y"
qed

lemma complex_vector_eq_affinity: "m ≠ 0 ⟹ y = m *⇩C x + c ⟷ inverse m *⇩C y - (inverse m *⇩C c) = x"
for x :: "'a::complex_vector"
using complex_vector_affinity_eq[where m=m and x=x and y=y and c=c]
by metis

lemma scaleC_eq_iff [simp]: "b + u *⇩C a = a + u *⇩C b ⟷ a = b ∨ u = 1"
for a :: "'a::complex_vector"
proof (cases "u = 1")
case True
thus ?thesis by auto
next
case False
have "a = b" if "b + u *⇩C a = a + u *⇩C b"
proof -
from that have "(u - 1) *⇩C a = (u - 1) *⇩C b"
with False show ?thesis
by auto
qed
thus ?thesis by auto
qed

lemma scaleC_collapse [simp]: "(1 - u) *⇩C a + u *⇩C a = a"
for a :: "'a::complex_vector"

subsection ‹Embedding of the Complex Numbers into any ‹complex_algebra_1›: ‹of_complex››

definition of_complex :: "complex ⇒ 'a::complex_algebra_1"
where "of_complex c = scaleC c 1"

lemma scaleC_conv_of_complex: "scaleC r x = of_complex r * x"

lemma of_complex_0 [simp]: "of_complex 0 = 0"

lemma of_complex_1 [simp]: "of_complex 1 = 1"

lemma of_complex_add [simp]: "of_complex (x + y) = of_complex x + of_complex y"

lemma of_complex_minus [simp]: "of_complex (- x) = - of_complex x"

lemma of_complex_diff [simp]: "of_complex (x - y) = of_complex x - of_complex y"

lemma of_complex_mult [simp]: "of_complex (x * y) = of_complex x * of_complex y"

lemma of_complex_sum[simp]: "of_complex (sum f s) = (∑x∈s. of_complex (f x))"
by (induct s rule: infinite_finite_induct) auto

lemma of_complex_prod[simp]: "of_complex (prod f s) = (∏x∈s. of_complex (f x))"
by (induct s rule: infinite_finite_induct) auto

lemma nonzero_of_complex_inverse:
"x ≠ 0 ⟹ of_complex (inverse x) = inverse (of_complex x :: 'a::complex_div_algebra)"

lemma of_complex_inverse [simp]:
"of_complex (inverse x) = inverse (of_complex x :: 'a::{complex_div_algebra,division_ring})"

lemma nonzero_of_complex_divide:
"y ≠ 0 ⟹ of_complex (x / y) = (of_complex x / of_complex y :: 'a::complex_field)"

lemma of_complex_divide [simp]:
"of_complex (x / y) = (of_complex x / of_complex y :: 'a::complex_div_algebra)"

lemma of_complex_power [simp]:
"of_complex (x ^ n) = (of_complex x :: 'a::{complex_algebra_1}) ^ n"
by (induct n) simp_all

lemma of_complex_power_int [simp]:
"of_complex (power_int x n) = power_int (of_complex x :: 'a :: {complex_div_algebra,division_ring}) n"
by (auto simp: power_int_def)

lemma of_complex_eq_iff [simp]: "of_complex x = of_complex y ⟷ x = y"

lemma inj_of_complex: "inj of_complex"
by (auto intro: injI)

lemmas of_complex_eq_0_iff [simp] = of_complex_eq_iff [of _ 0, simplified]
lemmas of_complex_eq_1_iff [simp] = of_complex_eq_iff [of _ 1, simplified]

lemma minus_of_complex_eq_of_complex_iff [simp]: "-of_complex x = of_complex y ⟷ -x = y"
using of_complex_eq_iff[of "-x" y] by (simp only: of_complex_minus)

lemma of_complex_eq_minus_of_complex_iff [simp]: "of_complex x = -of_complex y ⟷ x = -y"
using of_complex_eq_iff[of x "-y"] by (simp only: of_complex_minus)

lemma of_complex_eq_id [simp]: "of_complex = (id :: complex ⇒ complex)"
by (rule ext) (simp add: of_complex_def)

text ‹Collapse nested embeddings.›
lemma of_complex_of_nat_eq [simp]: "of_complex (of_nat n) = of_nat n"
by (induct n) auto

lemma of_complex_of_int_eq [simp]: "of_complex (of_int z) = of_int z"
by (cases z rule: int_diff_cases) simp

lemma of_complex_numeral [simp]: "of_complex (numeral w) = numeral w"
using of_complex_of_int_eq [of "numeral w"] by simp

lemma of_complex_neg_numeral [simp]: "of_complex (- numeral w) = - numeral w"
using of_complex_of_int_eq [of "- numeral w"] by simp

lemma numeral_power_int_eq_of_complex_cancel_iff [simp]:
"power_int (numeral x) n = (of_complex y :: 'a :: {complex_div_algebra, division_ring}) ⟷
power_int (numeral x) n = y"
proof -
have "power_int (numeral x) n = (of_complex (power_int (numeral x) n) :: 'a)"
by simp
also have "… = of_complex y ⟷ power_int (numeral x) n = y"
by (subst of_complex_eq_iff) auto
finally show ?thesis .
qed

lemma of_complex_eq_numeral_power_int_cancel_iff [simp]:
"(of_complex y :: 'a :: {complex_div_algebra, division_ring}) = power_int (numeral x) n ⟷
y = power_int (numeral x) n"
by (subst (1 2) eq_commute) simp

lemma of_complex_eq_of_complex_power_int_cancel_iff [simp]:
"power_int (of_complex b :: 'a :: {complex_div_algebra, division_ring}) w = of_complex x ⟷
power_int b w = x"
by (metis of_complex_power_int of_complex_eq_iff)

lemma of_complex_in_Ints_iff [simp]: "of_complex x ∈ ℤ ⟷ x ∈ ℤ"
proof safe
fix x assume "(of_complex x :: 'a) ∈ ℤ"
then obtain n where "(of_complex x :: 'a) = of_int n"
by (auto simp: Ints_def)
also have "of_int n = of_complex (of_int n)"
by simp
finally have "x = of_int n"
by (subst (asm) of_complex_eq_iff)
thus "x ∈ ℤ"
by auto
qed (auto simp: Ints_def)

lemma Ints_of_complex [intro]: "x ∈ ℤ ⟹ of_complex x ∈ ℤ"
by simp

text ‹Every complex algebra has characteristic zero.›

(* Inherited from real_algebra_1 *)
(* instance complex_algebra_1 < ring_char_0 .. *)

lemma fraction_scaleC_times [simp]:
fixes a :: "'a::complex_algebra_1"
shows "(numeral u / numeral v) *⇩C (numeral w * a) = (numeral u * numeral w / numeral v) *⇩C a"
by (metis (no_types, lifting) of_complex_numeral scaleC_conv_of_complex scaleC_scaleC times_divide_eq_left)

lemma inverse_scaleC_times [simp]:
fixes a :: "'a::complex_algebra_1"
shows "(1 / numeral v) *⇩C (numeral w * a) = (numeral w / numeral v) *⇩C a"
by (metis divide_inverse_commute inverse_eq_divide of_complex_numeral scaleC_conv_of_complex scaleC_scaleC)

lemma scaleC_times [simp]:
fixes a :: "'a::complex_algebra_1"
shows "(numeral u) *⇩C (numeral w * a) = (numeral u * numeral w) *⇩C a"

(* Inherited from real_field *)
(* instance complex_field < field_char_0 .. *)

subsection ‹The Set of Real Numbers›

definition Complexs :: "'a::complex_algebra_1 set"  ("ℂ")
where "ℂ = range of_complex"

lemma Complexs_of_complex [simp]: "of_complex r ∈ ℂ"

lemma Complexs_of_int [simp]: "of_int z ∈ ℂ"
by (subst of_complex_of_int_eq [symmetric], rule Complexs_of_complex)

lemma Complexs_of_nat [simp]: "of_nat n ∈ ℂ"
by (subst of_complex_of_nat_eq [symmetric], rule Complexs_of_complex)

lemma Complexs_numeral [simp]: "numeral w ∈ ℂ"
by (subst of_complex_numeral [symmetric], rule Complexs_of_complex)

lemma Complexs_0 [simp]: "0 ∈ ℂ" and Complexs_1 [simp]: "1 ∈ ℂ"

lemma Complexs_add [simp]: "a ∈ ℂ ⟹ b ∈ ℂ ⟹ a + b ∈ ℂ"

lemma Complexs_minus [simp]: "a ∈ ℂ ⟹ - a ∈ ℂ"
by (auto simp: Complexs_def)

lemma Complexs_minus_iff [simp]: "- a ∈ ℂ ⟷ a ∈ ℂ"
using Complexs_minus by fastforce

lemma Complexs_diff [simp]: "a ∈ ℂ ⟹ b ∈ ℂ ⟹ a - b ∈ ℂ"

lemma Complexs_mult [simp]: "a ∈ ℂ ⟹ b ∈ ℂ ⟹ a * b ∈ ℂ"
by (metis of_complex_mult rangeI)

lemma nonzero_Complexs_inverse: "a ∈ ℂ ⟹ a ≠ 0 ⟹ inverse a ∈ ℂ"
for a :: "'a::complex_div_algebra"
by (metis of_complex_inverse range_eqI)

lemma Complexs_inverse: "a ∈ ℂ ⟹ inverse a ∈ ℂ"
for a :: "'a::{complex_div_algebra,division_ring}"
using nonzero_Complexs_inverse by fastforce

lemma Complexs_inverse_iff [simp]: "inverse x ∈ ℂ ⟷ x ∈ ℂ"
for x :: "'a::{complex_div_algebra,division_ring}"
by (metis Complexs_inverse inverse_inverse_eq)

lemma nonzero_Complexs_divide: "a ∈ ℂ ⟹ b ∈ ℂ ⟹ b ≠ 0 ⟹ a / b ∈ ℂ"
for a b :: "'a::complex_field"

lemma Complexs_divide [simp]: "a ∈ ℂ ⟹ b ∈ ℂ ⟹ a / b ∈ ℂ"
for a b :: "'a::{complex_field,field}"
using nonzero_Complexs_divide by fastforce

lemma Complexs_power [simp]: "a ∈ ℂ ⟹ a ^ n ∈ ℂ"
for a :: "'a::complex_algebra_1"
by (metis range_eqI of_complex_power[symmetric])

lemma Complexs_cases [cases set: Complexs]:
assumes "q ∈ ℂ"
obtains (of_complex) c where "q = of_complex c"
unfolding Complexs_def
proof -
from ‹q ∈ ℂ› have "q ∈ range of_complex" unfolding Complexs_def .
then obtain c where "q = of_complex c" ..
then show thesis ..
qed

lemma sum_in_Complexs [intro,simp]: "(⋀i. i ∈ s ⟹ f i ∈ ℂ) ⟹ sum f s ∈ ℂ"
proof (induct s rule: infinite_finite_induct)
case infinite
then show ?case by (metis Complexs_0 sum.infinite)
qed simp_all

lemma prod_in_Complexs [intro,simp]: "(⋀i. i ∈ s ⟹ f i ∈ ℂ) ⟹ prod f s ∈ ℂ"
proof (induct s rule: infinite_finite_induct)
case infinite
then show ?case by (metis Complexs_1 prod.infinite)
qed simp_all

lemma Complexs_induct [case_names of_complex, induct set: Complexs]:
"q ∈ ℂ ⟹ (⋀r. P (of_complex r)) ⟹ P q"
by (rule Complexs_cases) auto

subsection ‹Ordered complex vector spaces›

class ordered_complex_vector = complex_vector + ordered_ab_group_add +
assumes scaleC_left_mono: "x ≤ y ⟹ 0 ≤ a ⟹ a *⇩C x ≤ a *⇩C y"
and scaleC_right_mono: "a ≤ b ⟹ 0 ≤ x ⟹ a *⇩C x ≤ b *⇩C x"
begin

subclass (in ordered_complex_vector) ordered_real_vector
apply standard
by (auto simp add: less_eq_complex_def scaleC_left_mono scaleC_right_mono scaleR_scaleC)

lemma scaleC_mono:
"a ≤ b ⟹ x ≤ y ⟹ 0 ≤ b ⟹ 0 ≤ x ⟹ a *⇩C x ≤ b *⇩C y"
by (meson order_trans scaleC_left_mono scaleC_right_mono)

lemma scaleC_mono':
"a ≤ b ⟹ c ≤ d ⟹ 0 ≤ a ⟹ 0 ≤ c ⟹ a *⇩C c ≤ b *⇩C d"
by (rule scaleC_mono) (auto intro: order.trans)

lemma pos_le_divideC_eq [field_simps]:
"a ≤ b /⇩C c ⟷ c *⇩C a ≤ b" (is "?P ⟷ ?Q") if "0 < c"
proof
assume ?P
with scaleC_left_mono that have "c *⇩C a ≤ c *⇩C (b /⇩C c)"
using preorder_class.less_imp_le by blast
with that show ?Q
by auto
next
assume ?Q
with scaleC_left_mono that have "c *⇩C a /⇩C c ≤ b /⇩C c"
using less_complex_def less_eq_complex_def by fastforce
with that show ?P
by auto
qed

lemma pos_less_divideC_eq [field_simps]:
"a < b /⇩C c ⟷ c *⇩C a < b" if "c > 0"
using that pos_le_divideC_eq [of c a b]

lemma pos_divideC_le_eq [field_simps]:
"b /⇩C c ≤ a ⟷ b ≤ c *⇩C a" if "c > 0"
using that pos_le_divideC_eq [of "inverse c" b a]
less_complex_def by auto

lemma pos_divideC_less_eq [field_simps]:
"b /⇩C c < a ⟷ b < c *⇩C a" if "c > 0"
using that pos_less_divideC_eq [of "inverse c" b a]
by (simp add: local.less_le_not_le local.pos_divideC_le_eq local.pos_le_divideC_eq)

lemma pos_le_minus_divideC_eq [field_simps]:
"a ≤ - (b /⇩C c) ⟷ c *⇩C a ≤ - b" if "c > 0"
using that

lemma pos_less_minus_divideC_eq [field_simps]:
"a < - (b /⇩C c) ⟷ c *⇩C a < - b" if "c > 0"
using that
by (metis le_less less_le_not_le pos_divideC_le_eq pos_divideC_less_eq pos_le_minus_divideC_eq)

lemma pos_minus_divideC_le_eq [field_simps]:
"- (b /⇩C c) ≤ a ⟷ - b ≤ c *⇩C a" if "c > 0"
using that

lemma pos_minus_divideC_less_eq [field_simps]:
"- (b /⇩C c) < a ⟷ - b < c *⇩C a" if "c > 0"
using that by (simp add: less_le_not_le pos_le_minus_divideC_eq pos_minus_divideC_le_eq)

lemma scaleC_image_atLeastAtMost: "c > 0 ⟹ scaleC c  {x..y} = {c *⇩C x..c *⇩C y}"
apply (auto intro!: scaleC_left_mono simp: image_iff Bex_def)
by (meson local.eq_iff pos_divideC_le_eq pos_le_divideC_eq)

end (* class ordered_complex_vector *)

lemma neg_le_divideC_eq [field_simps]:
"a ≤ b /⇩C c ⟷ b ≤ c *⇩C a" (is "?P ⟷ ?Q") if "c < 0"
for a b :: "'a :: ordered_complex_vector"
using that pos_le_divideC_eq [of "- c" a "- b"]

lemma neg_less_divideC_eq [field_simps]:
"a < b /⇩C c ⟷ b < c *⇩C a" if "c < 0"
for a b :: "'a :: ordered_complex_vector"
using that neg_le_divideC_eq [of c a b]
by (smt (verit, ccfv_SIG) neg_le_divideC_eq antisym_conv2 complex_vector.scale_minus_right dual_order.strict_implies_order le_less_trans neg_le_iff_le scaleC_scaleC)

lemma neg_divideC_le_eq [field_simps]:
"b /⇩C c ≤ a ⟷ c *⇩C a ≤ b" if "c < 0"
for a b :: "'a :: ordered_complex_vector"
using that pos_divideC_le_eq [of "- c" "- b" a]

lemma neg_divideC_less_eq [field_simps]:
"b /⇩C c < a ⟷ c *⇩C a < b" if "c < 0"
for a b :: "'a :: ordered_complex_vector"
using that neg_divideC_le_eq [of c b a]
by (meson neg_le_divideC_eq less_le_not_le)

lemma neg_le_minus_divideC_eq [field_simps]:
"a ≤ - (b /⇩C c) ⟷ - b ≤ c *⇩C a" if "c < 0"
for a b :: "'a :: ordered_complex_vector"
using that pos_le_minus_divideC_eq [of "- c" a "- b"]
by (metis neg_le_divideC_eq complex_vector.scale_minus_right)

lemma neg_less_minus_divideC_eq [field_simps]:
"a < - (b /⇩C c) ⟷ - b < c *⇩C a" if "c < 0"
for a b :: "'a :: ordered_complex_vector"
proof -
have *: "- b = c *⇩C a ⟷ b = - (c *⇩C a)"
from that neg_le_minus_divideC_eq [of c a b]
show ?thesis by (auto simp add: le_less *)
qed

lemma neg_minus_divideC_le_eq [field_simps]:
"- (b /⇩C c) ≤ a ⟷ c *⇩C a ≤ - b" if "c < 0"
for a b :: "'a :: ordered_complex_vector"
using that pos_minus_divideC_le_eq [of "- c" "- b" a]
by (metis Complex_Vector_Spaces0.neg_divideC_le_eq complex_vector.scale_minus_right)

lemma neg_minus_divideC_less_eq [field_simps]:
"- (b /⇩C c) < a ⟷ c *⇩C a < - b" if "c < 0"
for a b :: "'a :: ordered_complex_vector"
using that by (simp add: less_le_not_le neg_le_minus_divideC_eq neg_minus_divideC_le_eq)

lemma divideC_field_splits_simps_1 [field_split_simps]: (* In Real_Vector_Spaces, these lemmas are unnamed *)
"a = b /⇩C c ⟷ (if c = 0 then a = 0 else c *⇩C a = b)"
"b /⇩C c = a ⟷ (if c = 0 then a = 0 else b = c *⇩C a)"
"a + b /⇩C c = (if c = 0 then a else (c *⇩C a + b) /⇩C c)"
"a /⇩C c + b = (if c = 0 then b else (a + c *⇩C b) /⇩C c)"
"a - b /⇩C c = (if c = 0 then a else (c *⇩C a - b) /⇩C c)"
"a /⇩C c - b = (if c = 0 then - b else (a - c *⇩C b) /⇩C c)"
"- (a /⇩C c) + b = (if c = 0 then b else (- a + c *⇩C b) /⇩C c)"
"- (a /⇩C c) - b = (if c = 0 then - b else (- a - c *⇩C b) /⇩C c)"
for a b :: "'a :: complex_vector"

lemma divideC_field_splits_simps_2 [field_split_simps]: (* In Real_Vector_Spaces, these lemmas are unnamed *)
"0 < c ⟹ a ≤ b /⇩C c ⟷ (if c > 0 then c *⇩C a ≤ b else if c < 0 then b ≤ c *⇩C a else a ≤ 0)"
"0 < c ⟹ a < b /⇩C c ⟷ (if c > 0 then c *⇩C a < b else if c < 0 then b < c *⇩C a else a < 0)"
"0 < c ⟹ b /⇩C c ≤ a ⟷ (if c > 0 then b ≤ c *⇩C a else if c < 0 then c *⇩C a ≤ b else a ≥ 0)"
"0 < c ⟹ b /⇩C c < a ⟷ (if c > 0 then b < c *⇩C a else if c < 0 then c *⇩C a < b else a > 0)"
"0 < c ⟹ a ≤ - (b /⇩C c) ⟷ (if c > 0 then c *⇩C a ≤ - b else if c < 0 then - b ≤ c *⇩C a else a ≤ 0)"
"0 < c ⟹ a < - (b /⇩C c) ⟷ (if c > 0 then c *⇩C a < - b else if c < 0 then - b < c *⇩C a else a < 0)"
"0 < c ⟹ - (b /⇩C c) ≤ a ⟷ (if c > 0 then - b ≤ c *⇩C a else if c < 0 then c *⇩C a ≤ - b else a ≥ 0)"
"0 < c ⟹ - (b /⇩C c) < a ⟷ (if c > 0 then - b < c *⇩C a else if c < 0 then c *⇩C a < - b else a > 0)"
for a b :: "'a :: ordered_complex_vector"
by (clarsimp intro!: field_simps)+

lemma scaleC_nonneg_nonneg: "0 ≤ a ⟹ 0 ≤ x ⟹ 0 ≤ a *⇩C x"
for x :: "'a::ordered_complex_vector"
using scaleC_left_mono [of 0 x a] by simp

lemma scaleC_nonneg_nonpos: "0 ≤ a ⟹ x ≤ 0 ⟹ a *⇩C x ≤ 0"
for x :: "'a::ordered_complex_vector"
using scaleC_left_mono [of x 0 a] by simp

lemma scaleC_nonpos_nonneg: "a ≤ 0 ⟹ 0 ≤ x ⟹ a *⇩C x ≤ 0"
for x :: "'a::ordered_complex_vector"
using scaleC_right_mono [of a 0 x] by simp

lemma split_scaleC_neg_le: "(0 ≤ a ∧ x ≤ 0) ∨ (a ≤ 0 ∧ 0 ≤ x) ⟹ a *⇩C x ≤ 0"
for x :: "'a::ordered_complex_vector"
by (auto simp: scaleC_nonneg_nonpos scaleC_nonpos_nonneg)

lemma cle_add_iff1: "a *⇩C e + c ≤ b *⇩C e + d ⟷ (a - b) *⇩C e + c ≤ d"
for c d e :: "'a::ordered_complex_vector"

lemma cle_add_iff2: "a *⇩C e + c ≤ b *⇩C e + d ⟷ c ≤ (b - a) *⇩C e + d"
for c d e :: "'a::ordered_complex_vector"

lemma scaleC_left_mono_neg: "b ≤ a ⟹ c ≤ 0 ⟹ c *⇩C a ≤ c *⇩C b"
for a b :: "'a::ordered_complex_vector"
by (drule scaleC_left_mono [of _ _ "- c"], simp_all add: less_eq_complex_def)

lemma scaleC_right_mono_neg: "b ≤ a ⟹ c ≤ 0 ⟹ a *⇩C c ≤ b *⇩C c"
for c :: "'a::ordered_complex_vector"
by (drule scaleC_right_mono [of _ _ "- c"], simp_all)

lemma scaleC_nonpos_nonpos: "a ≤ 0 ⟹ b ≤ 0 ⟹ 0 ≤ a *⇩C b"
for b :: "'a::ordered_complex_vector"
using scaleC_right_mono_neg [of a 0 b] by simp

lemma split_scaleC_pos_le: "(0 ≤ a ∧ 0 ≤ b) ∨ (a ≤ 0 ∧ b ≤ 0) ⟹ 0 ≤ a *⇩C b"
for b :: "'a::ordered_complex_vector"
by (auto simp: scaleC_nonneg_nonneg scaleC_nonpos_nonpos)

lemma zero_le_scaleC_iff:
fixes b :: "'a::ordered_complex_vector"
assumes "a ∈ ℝ" (* Not present in Real_Vector_Spaces.thy *)
shows "0 ≤ a *⇩C b ⟷ 0 < a ∧ 0 ≤ b ∨ a < 0 ∧ b ≤ 0 ∨ a = 0"
(is "?lhs = ?rhs")
proof (cases "a = 0")
case True
then show ?thesis by simp
next
case False
show ?thesis
proof
assume ?lhs
from ‹a ≠ 0› consider "a > 0" | "a < 0"
by (metis assms complex_is_Real_iff less_complex_def less_eq_complex_def not_le order.not_eq_order_implies_strict that(1) zero_complex.sel(2))
then show ?rhs
proof cases
case 1
with ‹?lhs› have "inverse a *⇩C 0 ≤ inverse a *⇩C (a *⇩C b)"
by (metis complex_vector.scale_zero_right ordered_complex_vector_class.pos_le_divideC_eq)
with 1 show ?thesis
by simp
next
case 2
with ‹?lhs› have "- inverse a *⇩C 0 ≤ - inverse a *⇩C (a *⇩C b)"
by (metis Complex_Vector_Spaces0.neg_le_minus_divideC_eq complex_vector.scale_zero_right neg_le_0_iff_le scaleC_left.minus)
with 2 show ?thesis
by simp
qed
next
assume ?rhs
then show ?lhs
using less_imp_le split_scaleC_pos_le by auto
qed
qed

lemma scaleC_le_0_iff:
"a *⇩C b ≤ 0 ⟷ 0 < a ∧ b ≤ 0 ∨ a < 0 ∧ 0 ≤ b ∨ a = 0"
if "a ∈ ℝ" (* Not present in Real_Vector_Spaces *)
for b::"'a::ordered_complex_vector"
apply (insert zero_le_scaleC_iff [of "-a" b])
using less_complex_def that by force

lemma scaleC_le_cancel_left: "c *⇩C a ≤ c *⇩C b ⟷ (0 < c ⟶ a ≤ b) ∧ (c < 0 ⟶ b ≤ a)"
if "c ∈ ℝ" (* Not present in Real_Vector_Spaces *)
for b :: "'a::ordered_complex_vector"
by (smt (verit, ccfv_threshold) Complex_Vector_Spaces0.neg_divideC_le_eq complex_vector.scale_cancel_left complex_vector.scale_zero_right dual_order.eq_iff dual_order.trans ordered_complex_vector_class.pos_le_divideC_eq that zero_le_scaleC_iff)

lemma scaleC_le_cancel_left_pos: "0 < c ⟹ c *⇩C a ≤ c *⇩C b ⟷ a ≤ b"
for b :: "'a::ordered_complex_vector"
by (simp add: complex_is_Real_iff less_complex_def scaleC_le_cancel_left)

lemma scaleC_le_cancel_left_neg: "c < 0 ⟹ c *⇩C a ≤ c *⇩C b ⟷ b ≤ a"
for b :: "'a::ordered_complex_vector"
by (simp add: complex_is_Real_iff less_complex_def scaleC_le_cancel_left)

lemma scaleC_left_le_one_le: "0 ≤ x ⟹ a ≤ 1 ⟹ a *⇩C x ≤ x"
for x :: "'a::ordered_complex_vector" and a :: complex
using scaleC_right_mono[of a 1 x] by simp

subsection ‹Complex normed vector spaces›

(* Classes dist, norm, sgn_div_norm, dist_norm, uniformity_dist
defined in Real_Vector_Spaces are unchanged in the complex setting.
No need to define them here. *)

class complex_normed_vector = complex_vector + sgn_div_norm + dist_norm + uniformity_dist + open_uniformity +
real_normed_vector + (* Not present in Real_Normed_Vector *)
assumes norm_scaleC [simp]: "norm (scaleC a x) = cmod a * norm x"
begin
(* lemma norm_ge_zero [simp]: "0 ≤ norm x" *) (* Not needed, included from real_normed_vector *)
end

class complex_normed_algebra = complex_algebra + complex_normed_vector +
real_normed_algebra (* Not present in Real_Normed_Vector *)
(* assumes norm_mult_ineq: "norm (x * y) ≤ norm x * norm y" *) (* Not needed, included from real_normed_algebra *)

class complex_normed_algebra_1 = complex_algebra_1 + complex_normed_algebra +
real_normed_algebra_1 (* Not present in Real_Normed_Vector *)
(* assumes norm_one [simp]: "norm 1 = 1" *) (* Not needed, included from real_normed_algebra_1 *)

lemma (in complex_normed_algebra_1) scaleC_power [simp]: "(scaleC x y) ^ n = scaleC (x^n) (y^n)"
by (induct n) (simp_all add: mult_ac)

class complex_normed_div_algebra = complex_div_algebra + complex_normed_vector +
real_normed_div_algebra (* Not present in Real_Normed_Vector *)
(* assumes norm_mult: "norm (x * y) = norm x * norm y" *) (* Not needed, included from real_normed_div_algebra *)

class complex_normed_field = complex_field + complex_normed_div_algebra

subclass (in complex_normed_field) real_normed_field ..

instance complex_normed_div_algebra < complex_normed_algebra_1 ..

context complex_normed_vector begin
(* Inherited from real_normed_vector:
lemma norm_zero [simp]: "norm (0::'a) = 0"
lemma zero_less_norm_iff [simp]: "norm x > 0 ⟷ x ≠ 0"
lemma norm_not_less_zero [simp]: "¬ norm x < 0"
lemma norm_le_zero_iff [simp]: "norm x ≤ 0 ⟷ x = 0"
lemma norm_minus_cancel [simp]: "norm (- x) = norm x"
lemma norm_minus_commute: "norm (a - b) = norm (b - a)"
lemma dist_add_cancel [simp]: "dist (a + b) (a + c) = dist b c"
lemma dist_add_cancel2 [simp]: "dist (b + a) (c + a) = dist b c"
lemma norm_uminus_minus: "norm (- x - y) = norm (x + y)"
lemma norm_triangle_ineq2: "norm a - norm b ≤ norm (a - b)"
lemma norm_triangle_ineq3: "¦norm a - norm b¦ ≤ norm (a - b)"
lemma norm_triangle_ineq4: "norm (a - b) ≤ norm a + norm b"
lemma norm_triangle_le_diff: "norm x + norm y ≤ e ⟹ norm (x - y) ≤ e"
lemma norm_diff_ineq: "norm a - norm b ≤ norm (a + b)"
lemma norm_triangle_sub: "norm x ≤ norm y + norm (x - y)"
lemma norm_triangle_le: "norm x + norm y ≤ e ⟹ norm (x + y) ≤ e"
lemma norm_triangle_lt: "norm x + norm y < e ⟹ norm (x + y) < e"
lemma norm_add_leD: "norm (a + b) ≤ c ⟹ norm b ≤ norm a + c"
lemma norm_diff_triangle_ineq: "norm ((a + b) - (c + d)) ≤ norm (a - c) + norm (b - d)"
lemma norm_diff_triangle_le: "norm (x - z) ≤ e1 + e2"
if "norm (x - y) ≤ e1"  "norm (y - z) ≤ e2"
lemma norm_diff_triangle_less: "norm (x - z) < e1 + e2"
if "norm (x - y) < e1"  "norm (y - z) < e2"
lemma norm_triangle_mono:
"norm a ≤ r ⟹ norm b ≤ s ⟹ norm (a + b) ≤ r + s"
lemma norm_sum: "norm (sum f A) ≤ (∑i∈A. norm (f i))"
for f::"'b ⇒ 'a"
lemma sum_norm_le: "norm (sum f S) ≤ sum g S"
if "⋀x. x ∈ S ⟹ norm (f x) ≤ g x"
for f::"'b ⇒ 'a"
lemma abs_norm_cancel [simp]: "¦norm a¦ = norm a"
lemma sum_norm_bound:
"norm (sum f S) ≤ of_nat (card S)*K"
if "⋀x. x ∈ S ⟹ norm (f x) ≤ K"
for f :: "'b ⇒ 'a"
lemma norm_add_less: "norm x < r ⟹ norm y < s ⟹ norm (x + y) < r + s"
*)
end

lemma dist_scaleC [simp]: "dist (x *⇩C a) (y *⇩C a) = ¦x - y¦ * norm a"
for a :: "'a::complex_normed_vector"
by (metis dist_scaleR scaleR_scaleC)

(* Inherited from real_normed_vector *)
(* lemma norm_mult_less: "norm x < r ⟹ norm y < s ⟹ norm (x * y) < r * s"
for x y :: "'a::complex_normed_algebra" *)

lemma norm_of_complex [simp]: "norm (of_complex c :: 'a::complex_normed_algebra_1) = cmod c"

(* Inherited from real_normed_vector:
lemma norm_numeral [simp]: "norm (numeral w::'a::complex_normed_algebra_1) = numeral w"
lemma norm_neg_numeral [simp]: "norm (- numeral w::'a::complex_normed_algebra_1) = numeral w"
lemma norm_of_complex_add1 [simp]: "norm (of_real x + 1 :: 'a :: complex_normed_div_algebra) = ¦x + 1¦"
"norm (of_real x + numeral b :: 'a :: complex_normed_div_algebra) = ¦x + numeral b¦"
lemma norm_of_int [simp]: "norm (of_int z::'a::complex_normed_algebra_1) = ¦of_int z¦"
lemma norm_of_nat [simp]: "norm (of_nat n::'a::complex_normed_algebra_1) = of_nat n"
lemma nonzero_norm_inverse: "a ≠ 0 ⟹ norm (inverse a) = inverse (norm a)"
for a :: "'a::complex_normed_div_algebra"
lemma norm_inverse: "norm (inverse a) = inverse (norm a)"
for a :: "'a::{complex_normed_div_algebra,division_ring}"
lemma nonzero_norm_divide: "b ≠ 0 ⟹ norm (a / b) = norm a / norm b"
for a b :: "'a::complex_normed_field"
lemma norm_divide: "norm (a / b) = norm a / norm b"
for a b :: "'a::{complex_normed_field,field}"
lemma norm_inverse_le_norm:
fixes x :: "'a::complex_normed_div_algebra"
shows "r ≤ norm x ⟹ 0 < r ⟹ norm (inverse x) ≤ inverse r"
lemma norm_power_ineq: "norm (x ^ n) ≤ norm x ^ n"
for x :: "'a::complex_normed_algebra_1"
lemma norm_power: "norm (x ^ n) = norm x ^ n"
for x :: "'a::complex_normed_div_algebra"
lemma norm_power_int: "norm (power_int x n) = power_int (norm x) n"
for x :: "'a::complex_normed_div_algebra"
lemma power_eq_imp_eq_norm:
fixes w :: "'a::complex_normed_div_algebra"
assumes eq: "w ^ n = z ^ n" and "n > 0"
shows "norm w = norm z"
lemma power_eq_1_iff:
fixes w :: "'a::complex_normed_div_algebra"
shows "w ^ n = 1 ⟹ norm w = 1 ∨ n = 0"
lemma norm_mult_numeral1 [simp]: "norm (numeral w * a) = numeral w * norm a"
for a b :: "'a::{complex_normed_field,field}"
lemma norm_mult_numeral2 [simp]: "norm (a * numeral w) = norm a * numeral w"
for a b :: "'a::{complex_normed_field,field}"
lemma norm_divide_numeral [simp]: "norm (a / numeral w) = norm a / numeral w"
for a b :: "'a::{complex_normed_field,field}"
lemma square_norm_one:
fixes x :: "'a::complex_normed_div_algebra"
assumes "x⇧2 = 1"
shows "norm x = 1"
lemma norm_less_p1: "norm x < norm (of_real (norm x) + 1 :: 'a)"
for x :: "'a::complex_normed_algebra_1"
lemma prod_norm: "prod (λx. norm (f x)) A = norm (prod f A)"
for f :: "'a ⇒ 'b::{comm_semiring_1,complex_normed_div_algebra}"
lemma norm_prod_le:
"norm (prod f A) ≤ (∏a∈A. norm (f a :: 'a :: {complex_normed_algebra_1,comm_monoid_mult}))"
lemma norm_prod_diff:
fixes z w :: "'i ⇒ 'a::{complex_normed_algebra_1, comm_monoid_mult}"
shows "(⋀i. i ∈ I ⟹ norm (z i) ≤ 1) ⟹ (⋀i. i ∈ I ⟹ norm (w i) ≤ 1) ⟹
norm ((∏i∈I. z i) - (∏i∈I. w i)) ≤ (∑i∈I. norm (z i - w i))"
lemma norm_power_diff:
fixes z w :: "'a::{complex_normed_algebra_1, comm_monoid_mult}"
assumes "norm z ≤ 1" "norm w ≤ 1"
shows "norm (z^m - w^m) ≤ m * norm (z - w)"
*)

lemma norm_of_complex_add1 [simp]: "norm (of_complex x + 1 :: 'a :: complex_normed_div_algebra) = cmod (x + 1)"

"norm (of_complex x + numeral b :: 'a :: complex_normed_div_algebra) = cmod (x + numeral b)"

lemma norm_of_complex_diff [simp]:
"norm (of_complex b - of_complex a :: 'a::complex_normed_algebra_1) ≤ cmod (b - a)"
by (metis norm_of_complex of_complex_diff order_refl)

subsection ‹Metric spaces›

(* Class metric_space is already defined in Real_Vector_Spaces and does not need changing here *)

text ‹Every normed vector space is a metric space.›
(* Already follows from complex_normed_vector < real_normed_vector < metric_space *)
(* instance complex_normed_vector < metric_space *)

subsection ‹Class instances for complex numbers›

instantiation complex :: complex_normed_field
begin

instance
apply intro_classes

end

declare uniformity_Abort[where 'a=complex, code]

lemma dist_of_complex [simp]: "dist (of_complex x :: 'a) (of_complex y) = dist x y"
for a :: "'a::complex_normed_div_algebra"
by (metis dist_norm norm_of_complex of_complex_diff)

declare [[code abort: "open :: complex set ⇒ bool"]]

(* As far as I can tell, there is no analogue to this for complex:
instance real :: order_topology
instance real :: linear_continuum_topology ..

lemmas open_complex_greaterThan = open_greaterThan[where 'a=complex]
lemmas open_complex_lessThan = open_lessThan[where 'a=complex]
lemmas open_complex_greaterThanLessThan = open_greaterThanLessThan[where 'a=complex]
*)

lemma closed_complex_atMost: ‹closed {..a::complex}›
proof -
have ‹{..a} = Im - {Im a} ∩ Re - {..Re a}›
by (auto simp: less_eq_complex_def)
also have ‹closed …›
by (auto intro!: closed_Int closed_vimage continuous_on_Im continuous_on_Re)
finally show ?thesis
by -
qed

lemma closed_complex_atLeast: ‹closed {a::complex..}›
proof -
have ‹{a..} = Im - {Im a} ∩ Re - {Re a..}›
by (auto simp: less_eq_complex_def)
also have ‹closed …›
by (auto intro!: closed_Int closed_vimage continuous_on_Im continuous_on_Re)
finally show ?thesis
by -
qed

lemma closed_complex_atLeastAtMost: ‹closed {a::complex .. b}›
proof (cases ‹Im a = Im b›)
case True
have ‹{a..b} = Im - {Im a} ∩ Re - {Re a..Re b}›
by (auto simp add: less_eq_complex_def intro!: True)
also have ‹closed …›
by (auto intro!: closed_Int closed_vimage continuous_on_Im continuous_on_Re)
finally show ?thesis
by -
next
case False
then have *: ‹{a..b} = {}›
using less_eq_complex_def by auto
show ?thesis
qed

(* As far as I can tell, there is no analogue to this for complex:
instance real :: ordered_real_vector
by standard (auto intro: mult_left_mono mult_right_mono)
*)

(* subsection ‹Extra type constraints› *)
(* Everything is commented out, so we comment out the heading, too. *)

(* These are already configured in Real_Vector_Spaces:

text ‹Only allow \<^term>‹open› in class ‹topological_space›.›
(\<^const_name>‹open›, SOME \<^typ>‹'a::topological_space set ⇒ bool›)›

text ‹Only allow \<^term>‹uniformity› in class ‹uniform_space›.›
(\<^const_name>‹uniformity›, SOME \<^typ>‹('a::uniformity × 'a) filter›)›

text ‹Only allow \<^term>‹dist› in class ‹metric_space›.›
(\<^const_name>‹dist›, SOME \<^typ>‹'a::metric_space ⇒ 'a ⇒ real›)›

text ‹Only allow \<^term>‹norm› in class ‹complex_normed_vector›.›
(\<^const_name>‹norm›, SOME \<^typ>‹'a::complex_normed_vector ⇒ real›)›
*)

subsection ‹Sign function›

(* Inherited from real_normed_vector:
lemma norm_sgn: "norm (sgn x) = (if x = 0 then 0 else 1)"
for x :: "'a::complex_normed_vector"
lemma sgn_zero [simp]: "sgn (0::'a::complex_normed_vector) = 0"
lemma sgn_zero_iff: "sgn x = 0 ⟷ x = 0"
for x :: "'a::complex_normed_vector"
lemma sgn_minus: "sgn (- x) = - sgn x"
for x :: "'a::complex_normed_vector"
lemma sgn_one [simp]: "sgn (1::'a::complex_normed_algebra_1) = 1"
lemma sgn_mult: "sgn (x * y) = sgn x * sgn y"
for x y :: "'a::complex_normed_div_algebra"
hide_fact (open) sgn_mult
lemma norm_conv_dist: "norm x = dist x 0"
declare norm_conv_dist [symmetric, simp]
lemma dist_0_norm [simp]: "dist 0 x = norm x"
for x :: "'a::complex_normed_vector"
lemma dist_diff [simp]: "dist a (a - b) = norm b"  "dist (a - b) a = norm b"
lemma dist_of_int: "dist (of_int m) (of_int n :: 'a :: complex_normed_algebra_1) = of_int ¦m - n¦"
lemma dist_of_nat:
"dist (of_nat m) (of_nat n :: 'a :: complex_normed_algebra_1) = of_int ¦int m - int n¦"
*)

lemma sgn_scaleC: "sgn (scaleC r x) = scaleC (sgn r) (sgn x)"
for x :: "'a::complex_normed_vector"
by (simp add: scaleR_scaleC sgn_div_norm ac_simps)

lemma sgn_of_complex: "sgn (of_complex r :: 'a::complex_normed_algebra_1) = of_complex (sgn r)"
unfolding of_complex_def by (simp only: sgn_scaleC sgn_one)

lemma complex_sgn_eq: "sgn x = x / ¦x¦"
for x :: complex
by (simp add: abs_complex_def scaleR_scaleC sgn_div_norm divide_inverse)

lemma czero_le_sgn_iff [simp]: "0 ≤ sgn x ⟷ 0 ≤ x"
for x :: complex
using cmod_eq_Re divide_eq_0_iff less_eq_complex_def by auto

lemma csgn_le_0_iff [simp]: "sgn x ≤ 0 ⟷ x ≤ 0"
for x :: complex
by (smt (verit, best) czero_le_sgn_iff Im_sgn Re_sgn divide_eq_0_iff dual_order.eq_iff less_eq_complex_def sgn_zero_iff zero_complex.sel(1) zero_complex.sel(2))

subsection ‹Bounded Linear and Bilinear Operators›

lemma clinearI: "clinear f"
if "⋀b1 b2. f (b1 + b2) = f b1 + f b2"
"⋀r b. f (r *⇩C b) = r *⇩C f b"
using that
by unfold_locales (auto simp: algebra_simps)

lemma clinear_iff:
"clinear f ⟷ (∀x y. f (x + y) = f x + f y) ∧ (∀c x. f (c *⇩C x) = c *⇩C f x)"
(is "clinear f ⟷ ?rhs")
proof
assume "clinear f"
then interpret f: clinear f .
show "?rhs"
next
assume "?rhs"
then show "clinear f" by (intro clinearI) auto
qed

lemmas clinear_scaleC_left = complex_vector.linear_scale_left
lemmas clinear_imp_scaleC = complex_vector.linear_imp_scale

corollary complex_clinearD:
fixes f :: "complex ⇒ complex"
assumes "clinear f" obtains c where "f = (*) c"
by (rule clinear_imp_scaleC [OF assms]) (force simp: scaleC_conv_of_complex)

lemma clinear_times_of_complex: "clinear (λx. a * of_complex x)"
by (auto intro!: clinearI simp: distrib_left)
(metis mult_scaleC_right scaleC_conv_of_complex)

locale bounded_clinear = clinear f for f :: "'a::complex_normed_vector ⇒ 'b::complex_normed_vector" +
assumes bounded: "∃K. ∀x. norm (f x) ≤ norm x * K"
begin

(* Not present in Real_Vector_Spaces *)
lemma bounded_linear: "bounded_linear f"
apply standard

lemma pos_bounded: "∃K>0. ∀x. norm (f x) ≤ norm x * K"
proof -
obtain K where K: "⋀x. norm (f x) ≤ norm x * K"
using bounded by blast
show ?thesis
proof (intro exI impI conjI allI)
show "0 < max 1 K"
by (rule order_less_le_trans [OF zero_less_one max.cobounded1])
next
fix x
have "norm (f x) ≤ norm x * K" using K .
also have "… ≤ norm x * max 1 K"
by (rule mult_left_mono [OF max.cobounded2 norm_ge_zero])
finally show "norm (f x) ≤ norm x * max 1 K" .
qed
qed

(* Inherited from bounded_linear *)
lemma nonneg_bounded: "∃K≥0. ∀x. norm (f x) ≤ norm x * K"
by (meson less_imp_le pos_bounded)

lemma clinear: "clinear f"
by (fact local.clinear_axioms)

end

lemma bounded_clinear_intro:
assumes "⋀x y. f (x + y) = f x + f y"
and "⋀r x. f (scaleC r x) = scaleC r (f x)"
and "⋀x. norm (f x) ≤ norm x * K"
shows "bounded_clinear f"
by standard (blast intro: assms)+

locale bounded_cbilinear =
fixes prod :: "'a::complex_normed_vector ⇒ 'b::complex_normed_vector ⇒ 'c::complex_normed_vector"
(infixl "**" 70)
assumes add_left: "prod (a + a') b = prod a b + prod a' b"
and add_right: "prod a (b + b') = prod a b + prod a b'"
and scaleC_left: "prod (scaleC r a) b = scaleC r (prod a b)"
and scaleC_right: "prod a (scaleC r b) = scaleC r (prod a b)"
and bounded: "∃K. ∀a b. norm (prod a b) ≤ norm a * norm b * K"
begin

(* Not present in Real_Vector_Spaces *)
lemma bounded_bilinear[simp]: "bounded_bilinear prod"
apply standard

(* Not present in Real_Vector_Spaces. Has only temporary effect (until "end") *)
interpretation bounded_bilinear prod
by simp

lemmas pos_bounded = pos_bounded (* "∃K>0. ∀a b. norm (a ** b) ≤ norm a * norm b * K" *)
lemmas nonneg_bounded = nonneg_bounded (* "∃K≥0. ∀a b. norm (a ** b) ≤ norm a * norm b * K" *)
lemmas zero_left = zero_left (* "prod 0 b = 0" *)
lemmas zero_right = zero_right (* "prod a 0 = 0" *)
lemmas minus_left = minus_left (* "prod (- a) b = - prod a b" *)
lemmas minus_right = minus_right (* "prod a (- b) = - prod a b" *)
lemmas diff_left = diff_left (* "prod (a - a') b = prod a b - prod a' b" *)
lemmas diff_right = diff_right (* "prod a (b - b') = prod a b - prod a b'" *)
lemmas sum_left = sum_left (* "prod (sum g S) x = sum ((λi. prod (g i) x)) S" *)
lemmas sum_right = sum_right (* "prod x (sum g S) = sum ((λi. (prod x (g i)))) S" *)
lemmas prod_diff_prod = prod_diff_prod (* "(x ** y - a ** b) = (x - a) ** (y - b) + (x - a) ** b + a ** (y - b)" *)

lemma bounded_clinear_left: "bounded_clinear (λa. a ** b)"
proof -
obtain K where "⋀a b. norm (a ** b) ≤ norm a * norm b * K"
using pos_bounded by blast
then show ?thesis
by (rule_tac K="norm b * K" in bounded_clinear_intro) (auto simp: algebra_simps scaleC_left add_left)
qed

lemma bounded_clinear_right: "bounded_clinear (λb. a ** b)"
proof -
obtain K where "⋀a b. norm (a ** b) ≤ norm a * norm b * K"
using pos_bounded by blast
then show ?thesis
by (rule_tac K="norm a * K" in bounded_clinear_intro) (auto simp: algebra_simps scaleC_right add_right)
qed

lemma flip: "bounded_cbilinear (λx y. y ** x)"
proof
show "∃K. ∀a b. norm (b ** a) ≤ norm a * norm b * K"
by (metis bounded mult.commute)

lemma comp1:
assumes "bounded_clinear g"
shows "bounded_cbilinear (λx. (**) (g x))"
proof
interpret g: bounded_clinear g by fact
show "⋀a a' b. g (a + a') ** b = g a ** b + g a' ** b"
"⋀a b b'. g a ** (b + b') = g a ** b + g a ** b'"
"⋀r a b. g (r *⇩C a) ** b = r *⇩C (g a ** b)"
"⋀a r b. g a ** (r *⇩C b) = r *⇩C (g a ** b)"
have "bounded_bilinear (λa b. g a ** b)"
using g.bounded_linear by (rule comp1)
then show "∃K. ∀a b. norm (g a ** b) ≤ norm a * norm b * K"
by (rule bounded_bilinear.bounded)
qed

lemma comp: "bounded_clinear f ⟹ bounded_clinear g ⟹ bounded_cbilinear (λx y. f x ** g y)"
by (rule bounded_cbilinear.flip[OF bounded_cbilinear.comp1[OF bounded_cbilinear.flip[OF comp1]]])

end (* locale bounded_cbilinear *)

lemma bounded_clinear_ident[simp]: "bounded_clinear (λx. x)"
by standard (auto intro!: exI[of _ 1])

lemma bounded_clinear_zero[simp]: "bounded_clinear (λx. 0)"
by standard (auto intro!: exI[of _ 1])

assumes "bounded_clinear f"
and "bounded_clinear g"
shows "bounded_clinear (λx. f x + g x)"
proof -
interpret f: bounded_clinear f by fact
interpret g: bounded_clinear g by fact
show ?thesis
proof
from f.bounded obtain Kf where Kf: "norm (f x) ≤ norm x * Kf" for x
by blast
from g.bounded obtain Kg where Kg: "norm (g x) ≤ norm x * Kg" for x
by blast
show "∃K. ∀x. norm (f x + g x) ≤ norm x * K"
by (intro exI[of _ "Kf + Kg"]) (auto simp: field_simps intro: norm_triangle_ineq order_trans)
qed

lemma bounded_clinear_minus:
assumes "bounded_clinear f"
shows "bounded_clinear (λx. - f x)"
proof -
interpret f: bounded_clinear f by fact
show ?thesis
qed

lemma bounded_clinear_sub: "bounded_clinear f ⟹ bounded_clinear g ⟹ bounded_clinear (λx. f x - g x)"
using bounded_clinear_add[of f "λx. - g x"] bounded_clinear_minus[of g]
by (auto simp: algebra_simps)

lemma bounded_clinear_sum:
fixes f :: "'i ⇒ 'a::complex_normed_vector ⇒ 'b::complex_normed_vector"
shows "(⋀i. i ∈ I ⟹ bounded_clinear (f i)) ⟹ bounded_clinear (λx. ∑i∈I. f i x)"
by (induct I rule: infinite_finite_induct) (auto intro!: bounded_clinear_add)

lemma bounded_clinear_compose:
assumes "bounded_clinear f"
and "bounded_clinear g"
shows "bounded_clinear (λx. f (g x))"
proof
interpret f: bounded_clinear f by fact
interpret g: bounded_clinear g by fact
show "f (g (x + y)) = f (g x) + f (g y)" for x y
show "f (g (scaleC r x)) = scaleC r (f (g x))" for r x
by (simp only: f.scaleC g.scaleC)
from f.pos_bounded obtain Kf where f: "⋀x. norm (f x) ≤ norm x * Kf" and Kf: "0 < Kf"
by blast
from g.pos_bounded obtain Kg where g: "⋀x. norm (g x) ≤ norm x * Kg"
by blast
show "∃K. ∀x. norm (f (g x)) ≤ norm x * K"
proof (intro exI allI)
fix x
have "norm (f (g x)) ≤ norm (g x) * Kf"
using f .
also have "… ≤ (norm x * Kg) * Kf"
using g Kf [THEN order_less_imp_le] by (rule mult_right_mono)
also have "(norm x * Kg) * Kf = norm x * (Kg * Kf)"
by (rule mult.assoc)
finally show "norm (f (g x)) ≤ norm x * (Kg * Kf)" .
qed
qed

lemma bounded_cbilinear_mult: "bounded_cbilinear ((*) :: 'a ⇒ 'a ⇒ 'a::complex_normed_algebra)"
proof (rule bounded_cbilinear.intro)
show "∃K. ∀a b::'a. norm (a * b) ≤ norm a * norm b * K"
by (rule_tac x=1 in exI) (simp add: norm_mult_ineq)
qed (auto simp: algebra_simps)

lemma bounded_clinear_mult_left: "bounded_clinear (λx::'a::complex_normed_algebra. x * y)"
using bounded_cbilinear_mult
by (rule bounded_cbilinear.bounded_clinear_left)

lemma bounded_clinear_mult_right: "bounded_clinear (λy::'a::complex_normed_algebra. x * y)"
using bounded_cbilinear_mult
by (rule bounded_cbilinear.bounded_clinear_right)

lemmas bounded_clinear_mult_const =
bounded_clinear_mult_left [THEN bounded_clinear_compose]

lemmas bounded_clinear_const_mult =
bounded_clinear_mult_right [THEN bounded_clinear_compose]

lemma bounded_clinear_divide: "bounded_clinear (λx. x / y)"
for y :: "'a::complex_normed_field"
unfolding divide_inverse by (rule bounded_clinear_mult_left)

lemma bounded_cbilinear_scaleC: "bounded_cbilinear scaleC"
proof (rule bounded_cbilinear.intro)
obtain K where K: ‹∀a (b::'a). norm b ≤ norm b * K›
using less_eq_real_def by auto
show "∃K. ∀a (b::'a). norm (a *⇩C b) ≤ norm a * norm b * K"
apply (rule exI[where x=K]) using K
by (metis norm_scaleC)
qed (auto simp: algebra_simps)

lemma bounded_clinear_scaleC_left: "bounded_clinear (λc. scaleC c x)"
using bounded_cbilinear_scaleC
by (rule bounded_cbilinear.bounded_clinear_left)

lemma bounded_clinear_scaleC_right: "bounded_clinear (λx. scaleC c x)"
using bounded_cbilinear_scaleC
by (rule bounded_cbilinear.bounded_clinear_right)

lemmas bounded_clinear_scaleC_const =
bounded_clinear_scaleC_left[THEN bounded_clinear_compose]

lemmas bounded_clinear_const_scaleC =
bounded_clinear_scaleC_right[THEN bounded_clinear_compose]

lemma bounded_clinear_of_complex: "bounded_clinear (λr. of_complex r)"
unfolding of_complex_def by (rule bounded_clinear_scaleC_left)

lemma complex_bounded_clinear: "bounded_clinear f ⟷ (∃c::complex. f = (λx. x * c))"
for f :: "complex ⇒ complex"
proof -
{
fix x
assume "bounded_clinear f"
then interpret bounded_clinear f .
from scaleC[of x 1] have "f x = x * f 1"
by simp
}
then show ?thesis
by (auto intro: exI[of _ "f 1"] bounded_clinear_mult_left)
qed

(* Inherited from real_normed_algebra_1 *)
(* instance complex_normed_algebra_1 ⊆ perfect_space *)

(* subsection ‹Filters and Limits on Metric Space› *)
(* Everything is commented out, so we comment out the heading, too. *)

(* Not specific to real/complex *)
(* lemma (in metric_space) nhds_metric: "nhds x = (INF e∈{0 <..}. principal {y. dist y x < e})" *)
(* lemma (in metric_space) tendsto_iff: "(f ⤏ l) F ⟷ (∀e>0. eventually (λx. dist (f x) l < e) F)" *)
(* lemma tendsto_dist_iff: "((f ⤏ l) F) ⟷ (((λx. dist (f x) l) ⤏ 0) F)" *)
(* lemma (in metric_space) tendstoI [intro?]:
"(⋀e. 0 < e ⟹ eventually (λx. dist (f x) l < e) F) ⟹ (f ⤏ l) F" *)
(* lemma (in metric_space) tendstoD: "(f ⤏ l) F ⟹ 0 < e ⟹ eventually (λx. dist (f x) l < e) F" *)
(* lemma (in metric_space) eventually_nhds_metric:
"eventually P (nhds a) ⟷ (∃d>0. ∀x. dist x a < d ⟶ P x)" *)
(* lemma eventually_at: "eventually P (at a within S) ⟷ (∃d>0. ∀x∈S. x ≠ a ∧ dist x a < d ⟶ P x)"
for a :: "'a :: metric_space" *)
(* lemma frequently_at: "frequently P (at a within S) ⟷ (∀d>0. ∃x∈S. x ≠ a ∧ dist x a < d ∧ P x)"
for a :: "'a :: metric_space" *)
(* lemma eventually_at_le: "eventually P (at a within S) ⟷ (∃d>0. ∀x∈S. x ≠ a ∧ dist x a ≤ d ⟶ P x)"
for a :: "'a::metric_space" *)

(* Does not work in complex case because it needs complex :: order_toplogy *)
(* lemma eventually_at_left_real: "a > (b :: real) ⟹ eventually (λx. x ∈ {b<..<a}) (at_left a)" *)
(* lemma eventually_at_right_real: "a < (b :: real) ⟹ eventually (λx. x ∈ {a<..<b}) (at_right a)" *)

(* Not specific to real/complex *)
(* lemma metric_tendsto_imp_tendsto:
fixes a :: "'a :: metric_space"
and b :: "'b :: metric_space"
assumes f: "(f ⤏ a) F"
and le: "eventually (λx. dist (g x) b ≤ dist (f x) a) F"
shows "(g ⤏ b) F" *)

(* Not sure if this makes sense in the complex case *)
(* lemma filterlim_complex_sequentially: "LIM x sequentially. (of_nat x :: complex) :> at_top" *)

(* Not specific to real/complex *)
(* lemma filterlim_nat_sequentially: "filterlim nat sequentially at_top" *)
(* lemma filterlim_floor_sequentially: "filterlim floor at_top at_top" *)

(* Not sure if this makes sense in the complex case *)
(* lemma filterlim_sequentially_iff_filterlim_real:
"filterlim f sequentially F ⟷ filterlim (λx. real (f x)) at_top F" (is "?lhs = ?rhs") *)

subsubsection ‹Limits of Sequences›

(* Not specific to real/complex *)
(* lemma lim_sequentially: "X ⇢ L ⟷ (∀r>0. ∃no. ∀n≥no. dist (X n) L < r)"
for L :: "'a::metric_space" *)
(* lemmas LIMSEQ_def = lim_sequentially  (*legacy binding*) *)
(* lemma LIMSEQ_iff_nz: "X ⇢ L ⟷ (∀r>0. ∃no>0. ∀n≥no. dist (X n) L < r)"
for L :: "'a::metric_space" *)
(* lemma metric_LIMSEQ_I: "(⋀r. 0 < r ⟹ ∃no. ∀n≥no. dist (X n) L < r) ⟹ X ⇢ L"
for L :: "'a::metric_space" *)
(* lemma metric_LIMSEQ_D: "X ⇢ L ⟹ 0 < r ⟹ ∃no. ∀n≥no. dist (X n) L < r"
for L :: "'a::metric_space" *)
(* lemma LIMSEQ_norm_0:
assumes  "⋀n::nat. norm (f n) < 1 / real (Suc n)"
shows "f ⇢ 0" *)

(* subsubsection ‹Limits of Functions› *)
(* Everything is commented out, so we comment out the heading, too. *)

(* Not specific to real/complex *)
(* lemma LIM_def: "f ─a→ L ⟷ (∀r > 0. ∃s > 0. ∀x. x ≠ a ∧ dist x a < s ⟶ dist (f x) L < r)"
for a :: "'a::metric_space" and L :: "'b::metric_space" *)
(* lemma metric_LIM_I:
"(⋀r. 0 < r ⟹ ∃s>0. ∀x. x ≠ a ∧ dist x a < s ⟶ dist (f x) L < r) ⟹ f ─a→ L"
for a :: "'a::metric_space" and L :: "'b::metric_space" *)
(* lemma metric_LIM_D: "f ─a→ L ⟹ 0 < r ⟹ ∃s>0. ∀x. x ≠ a ∧ dist x a < s ⟶ dist (f x) L < r"
for a :: "'a::metric_space" and L :: "'b::metric_space" *)
(* lemma metric_LIM_imp_LIM:
fixes l :: "'a::metric_space"
and m :: "'b::metric_space"
assumes f: "f ─a→ l"
and le: "⋀x. x ≠ a ⟹ dist (g x) m ≤ dist (f x) l"
shows "g ─a→ m" *)
(* lemma metric_LIM_equal2:
fixes a :: "'a::metric_space"
assumes "g ─a→ l" "0 < R"
and "⋀x. x ≠ a ⟹ dist x a < R ⟹ f x = g x"
shows "f ─a→ l" *)
(* lemma metric_LIM_compose2:
fixes a :: "'a::metric_space"
assumes f: "f ─a→ b"
and g: "g ─b→ c"
and inj: "∃d>0. ∀x. x ≠ a ∧ dist x a < d ⟶ f x ≠ b"
shows "(λx. g (f x)) ─a→ c" *)
(* lemma metric_isCont_LIM_compose2:
fixes f :: "'a :: metric_space ⇒ _"
assumes f [unfolded isCont_def]: "isCont f a"
and g: "g ─f a→ l"
and inj: "∃d>0. ∀x. x ≠ a ∧ dist x a < d ⟶ f x ≠ f a"
shows "(λx. g (f x)) ─a→ l" *)

(* subsection ‹Complete metric spaces› *)
(* Everything is commented out, so we comment out the heading, too. *)

subsection ‹Cauchy sequences›

(* Not specific to real/complex *)
(* lemma (in metric_space) Cauchy_def: "Cauchy X = (∀e>0. ∃M. ∀m≥M. ∀n≥M. dist (X m) (X n) < e)" *)
(* lemma (in metric_space) Cauchy_altdef: "Cauchy f ⟷ (∀e>0. ∃M. ∀m≥M. ∀n>m. dist (f m) (f n) < e)" *)
(* lemma (in metric_space) Cauchy_altdef2: "Cauchy s ⟷ (∀e>0. ∃N::nat. ∀n≥N. dist(s n)(s N) < e)" (is "?lhs = ?rhs") *)
(* lemma (in metric_space) metric_CauchyI:
"(⋀e. 0 < e ⟹ ∃M. ∀m≥M. ∀n≥M. dist (X m) (X n) < e) ⟹ Cauchy X" *)
(* lemma (in metric_space) CauchyI':
"(⋀e. 0 < e ⟹ ∃M. ∀m≥M. ∀n>m. dist (X m) (X n) < e) ⟹ Cauchy X" *)
(* lemma (in metric_space) metric_CauchyD:
"Cauchy X ⟹ 0 < e ⟹ ∃M. ∀m≥M. ∀n≥M. dist (X m) (X n) < e" *)
(* lemma (in metric_space) metric_Cauchy_iff2:
"Cauchy X = (∀j. (∃M. ∀m ≥ M. ∀n ≥ M. dist (X m) (X n) < inverse(real (Suc j))))" *)

lemma cCauchy_iff2: "Cauchy X ⟷ (∀j. (∃M. ∀m ≥ M. ∀n ≥ M. cmod (X m - X n) < inverse (real (Suc j))))"
by (simp only: metric_Cauchy_iff2 dist_complex_def)

(* Not specific to real/complex *)
(* lemma lim_1_over_n [tendsto_intros]: "((λn. 1 / of_nat n) ⤏ (0::'a::complex_normed_field)) sequentially" *)
(* lemma (in metric_space) complete_def:
shows "complete S = (∀f. (∀n. f n ∈ S) ∧ Cauchy f ⟶ (∃l∈S. f ⇢ l))" *)
(* lemma (in metric_space) totally_bounded_metric:
"totally_bounded S ⟷ (∀e>0. ∃k. finite k ∧ S ⊆ (⋃x∈k. {y. dist x y < e}))" *)

(* subsubsection ‹Cauchy Sequences are Convergent› *)
(* Everything is commented out, so we comment out the heading, too. *)

(* Not specific to real/complex *)
(* class complete_space *)
(* lemma Cauchy_convergent_iff: "Cauchy X ⟷ convergent X"
for X :: "nat ⇒ 'a::complete_space" *)

(* text ‹To prove that a Cauchy sequence converges, it suffices to show that a subsequence converges.› *)

(* Not specific to real/complex *)
(* lemma Cauchy_converges_subseq:
fixes u::"nat ⇒ 'a::metric_space"
assumes "Cauchy u"
"strict_mono r"
"(u ∘ r) ⇢ l"
shows "u ⇢ l" *)

subsection ‹The set of real numbers is a complete metric space›

text ‹
Proof that Cauchy sequences converge based on the one from
🌐‹http://pirate.shu.edu/~wachsmut/ira/numseq/proofs/cauconv.html›
›

text ‹
If sequence \<^term>‹X› is Cauchy, then its limit is the lub of
\<^term>‹{r::real. ∃N. ∀n≥N. r < X n}›
›

lemma complex_increasing_LIMSEQ:
fixes f :: "nat ⇒ complex"
assumes inc: "⋀n. f n ≤ f (Suc n)"
and bdd: "⋀n. f n ≤ l"
and en: "⋀e. 0 < e ⟹ ∃n. l ≤ f n + e"
shows "f ⇢ l"
proof -
have ‹(λn. Re (f n)) ⇢ Re l›
apply (rule increasing_LIMSEQ)
using assms apply (auto simp: less_eq_complex_def less_complex_def)
by (metis Im_complex_of_real Re_complex_of_real)
moreover have ‹Im (f n) = Im l› for n
using bdd by (auto simp: less_eq_complex_def)
then have ‹(λn. Im (f n)) ⇢ Im l›
by auto
ultimately show ‹f ⇢ l›
qed

lemma complex_Cauchy_convergent:
fixes X :: "nat ⇒ complex"
assumes X: "Cauchy X"
shows "convergent X"
using assms by (rule Cauchy_convergent)

instance complex :: complete_space
by intro_classes (rule complex_Cauchy_convergent)

class cbanach = complex_normed_vector + complete_space

(* Not present in Real_Vector_Spaces *)
subclass (in cbanach) banach ..

instance complex :: banach ..

(* Don't know if this holds in the complex case *)
(* lemma tendsto_at_topI_sequentially:
fixes f :: "complex ⇒ 'b::first_countable_topology"
assumes *: "⋀X. filterlim X at_top sequentially ⟹ (λn. f (X n)) ⇢ y"
shows "(f ⤏ y) at_top" *)
(* lemma tendsto_at_topI_sequentially_real:
fixes f :: "real ⇒ real"
assumes mono: "mono f"
and limseq: "(λn. f (real n)) ⇢ y"
shows "(f ⤏ y) at_top" *)

end


# Theory Complex_Vector_Spaces

section ‹‹Complex_Vector_Spaces› -- Complex Vector Spaces›

(*
Authors:

Dominique Unruh, University of Tartu, unruh@ut.ee
Jose Manuel Rodriguez Caballero, University of Tartu, jose.manuel.rodriguez.caballero@ut.ee
*)

theory Complex_Vector_Spaces
imports
"HOL-Analysis.Elementary_Topology"
"HOL-Analysis.Operator_Norm"
"HOL-Analysis.Elementary_Normed_Spaces"
"HOL-Library.Set_Algebras"
"HOL-Analysis.Starlike"
"HOL-Types_To_Sets.Types_To_Sets"

"Complex_Bounded_Operators.Extra_Vector_Spaces"
"Complex_Bounded_Operators.Extra_Ordered_Fields"
"Complex_Bounded_Operators.Extra_Lattice"
"Complex_Bounded_Operators.Extra_General"

Complex_Vector_Spaces0
begin

bundle notation_norm begin
notation norm ("∥_∥")
end

subsection ‹Misc›

lemma (in scaleC) scaleC_real: assumes "r∈ℝ" shows "r *⇩C x = Re r *⇩R x"
unfolding scaleR_scaleC using assms by simp

lemma of_complex_of_real_eq [simp]: "of_complex (of_real n) = of_real n"
unfolding of_complex_def of_real_def unfolding scaleR_scaleC by simp

lemma Complexs_of_real [simp]: "of_real r ∈ ℂ"
unfolding Complexs_def of_real_def of_complex_def
apply (subst scaleR_scaleC) by simp

lemma Reals_in_Complexs: "ℝ ⊆ ℂ"
unfolding Reals_def by auto

lemma (in clinear) "linear f"
apply standard

lemma (in bounded_clinear) bounded_linear: "bounded_linear f"

lemma clinear_times: "clinear (λx. c * x)"
for c :: "'a::complex_algebra"
by (auto simp: clinearI distrib_left)

lemma (in clinear) linear:
shows ‹linear f›

lemma bounded_clinearI:
assumes ‹⋀b1 b2. f (b1 + b2) = f b1 + f b2›
assumes ‹⋀r b. f (r *⇩C b) = r *⇩C f b›
assumes ‹∀x. norm (f x) ≤ norm x * K›
shows "bounded_clinear f"
using assms by (auto intro!: exI bounded_clinear.intro clinearI simp: bounded_clinear_axioms_def)

lemma bounded_clinear_id[simp]: ‹bounded_clinear id›

(* The following would be a natural inclusion of locales, but unfortunately it leads to
name conflicts upon interpretation of bounded_cbilinear *)
(* sublocale bounded_cbilinear ⊆ bounded_bilinear
by (rule bounded_bilinear) *)

definition cbilinear :: ‹('a::complex_vector ⇒ 'b::complex_vector ⇒ 'c::complex_vector) ⇒ bool›
where ‹cbilinear = (λ f. (∀ y. clinear (λ x. f x y)) ∧ (∀ x. clinear (λ y. f x y)) )›

assumes ‹cbilinear f›
shows ‹f (a + b) c = f a c + f b c›
by (smt (verit, del_insts) assms cbilinear_def complex_vector.linear_add)

assumes ‹cbilinear f›
shows ‹f a (b + c) = f a b + f a c›
by (smt (verit, del_insts) assms cbilinear_def complex_vector.linear_add)

lemma cbilinear_times:
fixes g' :: ‹'a::complex_vector ⇒ complex› and g :: ‹'b::complex_vector ⇒ complex›
assumes ‹⋀ x y. h x y = (g' x)*(g y)› and ‹clinear g› and ‹clinear g'›
shows ‹cbilinear h›
proof -
have w1: "h (b1 + b2) y = h b1 y + h b2 y"
for b1 :: 'a
and b2 :: 'a
and y
proof-
have ‹h (b1 + b2) y = g' (b1 + b2) * g y›
using ‹⋀ x y. h x y = (g' x)*(g y)›
by auto
also have ‹… = (g' b1 + g' b2) * g y›
using ‹clinear g'›
unfolding clinear_def
also have ‹… = g' b1 * g y + g' b2 * g y›
also have ‹… = h b1 y + h b2 y›
using assms(1) by auto
finally show ?thesis by blast
qed
have w2: "h (r *⇩C b) y = r *⇩C h b y"
for r :: complex
and b :: 'a
and y
proof-
have ‹h (r *⇩C b) y = g' (r *⇩C b) * g y›
also have ‹… = r *⇩C (g' b * g y)›
also have ‹… = r *⇩C (h b y)›
finally show ?thesis by blast
qed
have "clinear (λx. h x y)"
for y :: 'b
unfolding clinear_def
by (meson clinearI clinear_def w1 w2)
hence t2: "∀y. clinear (λx. h x y)"
by simp
have v1: "h x (b1 + b2) = h x b1 + h x b2"
for b1 :: 'b
and b2 :: 'b
and x
proof-
have ‹h x (b1 + b2)  = g' x * g (b1 + b2)›
using ‹⋀ x y. h x y = (g' x)*(g y)›
by auto
also have ‹… = g' x * (g b1 + g b2)›
using ‹clinear g'›
unfolding clinear_def
also have ‹… = g' x * g b1 + g' x * g b2›
also have ‹… = h x b1 + h x b2›
using assms(1) by auto
finally show ?thesis by blast
qed

have v2:  "h x (r *⇩C b) = r *⇩C h x b"
for r :: complex
and b :: 'b
and x
proof-
have ‹h x (r *⇩C b) =  g' x * g (r *⇩C b)›
also have ‹… = r *⇩C (g' x * g b)›
also have ‹… = r *⇩C (h x b)›
finally show ?thesis by blast
qed
have "Vector_Spaces.linear (*⇩C) (*⇩C) (h x)"
for x :: 'a
using v1 v2
by (meson clinearI clinear_def)
hence t1: "∀x. clinear (h x)"
unfolding clinear_def
by simp
show ?thesis
unfolding cbilinear_def
qed

lemma csubspace_is_subspace: "csubspace A ⟹ subspace A"
apply (rule subspaceI)
by (auto simp: complex_vector.subspace_def scaleR_scaleC)

lemma span_subset_cspan: "span A ⊆ cspan A"
unfolding span_def complex_vector.span_def

lemma cindependent_implies_independent:
assumes "cindependent (S::'a::complex_vector set)"
shows "independent S"
using assms unfolding dependent_def complex_vector.dependent_def
using span_subset_cspan by blast

lemma cspan_singleton: "cspan {x} = {α *⇩C x| α. True}"
proof -
have ‹cspan {x} = {y. y∈cspan {x}}›
by auto
also have ‹… = {α *⇩C x| α. True}›
apply (subst complex_vector.span_breakdown_eq)
by auto
finally show ?thesis
by -
qed

lemma cspan_as_span:
"cspan (B::'a::complex_vector set) = span (B ∪ scaleC 𝗂  B)"
proof auto
let ?cspan = complex_vector.span
let ?rspan = real_vector.span
fix ψ
assume cspan: "ψ ∈ ?cspan B"
have "∃B' r. finite B' ∧ B' ⊆ B ∧ ψ = (∑b∈B'. r b *⇩C b)"
using complex_vector.span_explicit[of B] cspan
by auto
then obtain B' r where "finite B'" and "B' ⊆ B" and ψ_explicit: "ψ = (∑b∈B'. r b *⇩C b)"
by atomize_elim
define R where "R = B ∪ scaleC 𝗂  B"

have x2: "(case x of (b, i) ⇒ if i
then Im (r b) *⇩R 𝗂 *⇩C b
else Re (r b) *⇩R b) ∈ span (B ∪ (*⇩C) 𝗂  B)"
if "x ∈ B' × (UNIV::bool set)"
for x :: "'a × bool"
using that ‹B' ⊆ B› by (auto simp add: real_vector.span_base real_vector.span_scale subset_iff)
have x1: "ψ = (∑x∈B'. ∑i∈UNIV. if i then Im (r x) *⇩R 𝗂 *⇩C x else Re (r x) *⇩R x)"
if "⋀b. r b *⇩C b = Re (r b) *⇩R b + Im (r b) *⇩R 𝗂 *⇩C b"
using that by (simp add: UNIV_bool ψ_explicit)
moreover have "r b *⇩C b = Re (r b) *⇩R b + Im (r b) *⇩R 𝗂 *⇩C b" for b
by (metis (no_types, lifting) complex_of_real_i i_complex_of_real)
ultimately have "ψ = (∑(b,i)∈(B'×UNIV). if i then Im (r b) *⇩R (𝗂 *⇩C b) else Re (r b) *⇩R b)"
also have "… ∈ ?rspan R"
unfolding R_def
using x2
by (rule real_vector.span_sum)
finally show "ψ ∈ ?rspan R" by -
next
let ?cspan = complex_vector.span
let ?rspan = real_vector.span
define R where "R = B ∪ scaleC 𝗂  B"
fix ψ
assume rspan: "ψ ∈ ?rspan R"
have "subspace {a. a ∈ cspan B}"
by (rule real_vector.subspaceI, auto simp add: complex_vector.span_zero
moreover have "x ∈ cspan B"
if "x ∈ R"
for x :: 'a
using that R_def complex_vector.span_base complex_vector.span_scale by fastforce
ultimately show "ψ ∈ ?cspan B"
using real_vector.span_induct rspan by blast
qed

lemma isomorphic_equal_cdim:
assumes lin_f: ‹clinear f›
assumes inj_f: ‹inj_on f (cspan S)›
assumes im_S: ‹f  S = T›
shows ‹cdim S = cdim T›
proof -
obtain SB where SB_span: "cspan SB = cspan S" and indep_SB: ‹cindependent SB›
by (metis complex_vector.basis_exists complex_vector.span_mono complex_vector.span_span subset_antisym)
with lin_f inj_f have indep_fSB: ‹cindependent (f  SB)›
apply (rule_tac complex_vector.linear_independent_injective_image)
by auto
from lin_f have ‹cspan (f  SB) = f  cspan SB›
by (meson complex_vector.linear_span_image)
also from SB_span lin_f have ‹… = cspan T›
by (metis complex_vector.linear_span_image im_S)
finally have ‹cdim T = card (f  SB)›
using indep_fSB complex_vector.dim_eq_card by blast
also have ‹… = card SB›
apply (rule card_image) using inj_f
by (metis SB_span complex_vector.linear_inj_on_span_iff_independent_image indep_fSB lin_f)
also have ‹… = cdim S›
using indep_SB SB_span
by (metis complex_vector.dim_eq_card)
finally show ?thesis by simp
qed

lemma cindependent_inter_scaleC_cindependent:
assumes a1: "cindependent (B::'a::complex_vector set)" and a3: "c ≠ 1"
shows "B ∩ (*⇩C) c  B = {}"
proof (rule classical, cases ‹c = 0›)
case True
then show ?thesis
using a1 by (auto simp add: complex_vector.dependent_zero)
next
case False
assume "¬(B ∩ (*⇩C) c  B = {})"
hence "B ∩ (*⇩C) c  B ≠ {}"
by blast
then obtain x where u1: "x ∈ B ∩ (*⇩C) c  B"
by blast
then obtain b where u2: "x = b" and u3: "b∈B"
by blast
then  obtain b' where u2': "x = c *⇩C b'" and u3': "b'∈B"
using u1
by blast
have g1: "b = c *⇩C b'"
using u2 and u2' by simp
hence "b ∈ complex_vector.span {b'}"
using False
hence "b = b'"
by (metis  u3' a1 complex_vector.dependent_def complex_vector.span_base
complex_vector.span_scale insertE insert_Diff u2 u2' u3)
hence "b' = c *⇩C b'"
using g1 by blast
thus ?thesis
by (metis a1 a3 complex_vector.dependent_zero complex_vector.scale_right_imp_eq
mult_cancel_right2 scaleC_scaleC u3')
qed

lemma real_independent_from_complex_independent:
assumes "cindependent (B::'a::complex_vector set)"
defines "B' == ((*⇩C) 𝗂  B)"
shows "independent (B ∪ B')"
proof (rule notI)
assume ‹dependent (B ∪ B')›
then obtain T f0 x where [simp]: ‹finite T› and ‹T ⊆ B ∪ B'› and f0_sum: ‹(∑v∈T. f0 v *⇩R v) = 0›
and x: ‹x ∈ T› and f0_x: ‹f0 x ≠ 0›
by (auto simp: real_vector.dependent_explicit)
define f T1 T2 T' f' x' where ‹f v = (if v ∈ T then f0 v else 0)›
and ‹T1 = T ∩ B› and ‹T2 = scaleC (-𝗂)  (T ∩ B')›
and ‹T' = T1 ∪ T2› and ‹f' v = f v + 𝗂 * f (𝗂 *⇩C v)›
and ‹x' = (if x ∈ T1 then x else -𝗂 *⇩C x)› for v
have ‹B ∩ B' = {}›
have ‹T' ⊆ B›
by (auto simp: T'_def T1_def T2_def B'_def)
have [simp]: ‹finite T'› ‹finite T1› ‹finite T2›
by (auto simp add: T'_def T1_def T2_def)
have f_sum: ‹(∑v∈T. f v *⇩R v) = 0›
unfolding f_def using f0_sum by auto
have f_x: ‹f x ≠ 0›
using f0_x x by (auto simp: f_def)
have f'_sum: ‹(∑v∈T'. f' v *⇩C v) = 0›
proof -
have ‹(∑v∈T'. f' v *⇩C v) = (∑v∈T'. complex_of_real (f v) *⇩C v) + (∑v∈T'. (𝗂 * complex_of_real (f (𝗂 *⇩C v))) *⇩C v)›
by (auto simp: f'_def sum.distrib scaleC_add_left)
also have ‹(∑v∈T'. complex_of_real (f v) *⇩C v) = (∑v∈T1. f v *⇩R v)› (is ‹_ = ?left›)
apply (auto simp: T'_def scaleR_scaleC intro!: sum.mono_neutral_cong_right)
using T'_def T1_def ‹T' ⊆ B› f_def by auto
also have ‹(∑v∈T'. (𝗂 * complex_of_real (f (𝗂 *⇩C v))) *⇩C v) = (∑v∈T2. (𝗂 * complex_of_real (f (𝗂 *⇩C v))) *⇩C v)› (is ‹_ = ?right›)
apply (auto simp: T'_def intro!: sum.mono_neutral_cong_right)
by (smt (z3) B'_def IntE IntI T1_def T2_def ‹f ≡ λv. if v ∈ T then f0 v else 0› add.inverse_inverse complex_vector.vector_space_axioms i_squared imageI mult_minus_left vector_space.vector_space_assms(3) vector_space.vector_space_assms(4))
also have ‹?right = (∑v∈T∩B'. f v *⇩R v)› (is ‹_ = ?right›)
apply (rule sum.reindex_cong[symmetric, where l=‹scaleC 𝗂›])
apply (auto simp: T2_def image_image scaleR_scaleC)
using inj_on_def by fastforce
also have ‹?left + ?right = (∑v∈T. f v *⇩R v)›
apply (subst sum.union_disjoint[symmetric])
using ‹B ∩ B' = {}› ‹T ⊆ B ∪ B'› apply (auto simp: T1_def)
by (metis Int_Un_distrib Un_Int_eq(4) sup.absorb_iff1)
also have ‹… = 0›
by (rule f_sum)
finally show ?thesis
by -
qed

have x': ‹x' ∈ T'›
using ‹T ⊆ B ∪ B'› x by (auto simp: x'_def T'_def T1_def T2_def)

have f'_x': ‹f' x' ≠ 0›
using Complex_eq Complex_eq_0 f'_def f_x x'_def by auto

from ‹finite T'› ‹T' ⊆ B› f'_sum x' f'_x'
have ‹cdependent B›
using complex_vector.independent_explicit_module by blast
with assms show False
by auto
qed

lemma crepresentation_from_representation:
assumes a1: "cindependent B" and a2: "b ∈ B" and a3: "finite B"
shows "crepresentation B ψ b = (representation (B ∪ (*⇩C) 𝗂  B) ψ b)
+ 𝗂 *⇩C (representation (B ∪ (*⇩C) 𝗂  B) ψ (𝗂 *⇩C b))"
proof (cases "ψ ∈ cspan B")
define B' where "B' = B ∪ (*⇩C) 𝗂  B"
case True
define r  where "r v = real_vector.representation B' ψ v" for v
define r' where "r' v = real_vector.representation B' ψ (𝗂 *⇩C v)" for v
define f  where "f v = r v + 𝗂 *⇩C r' v" for v
define g  where "g v = crepresentation B ψ v" for v
have "(∑v | g v ≠ 0. g v *⇩C v) = ψ"
unfolding g_def
using Collect_cong Collect_mono_iff DiffD1 DiffD2 True a1
complex_vector.finite_representation
complex_vector.sum_nonzero_representation_eq sum.mono_neutral_cong_left
by fastforce
moreover have "finite {v. g v ≠ 0}"
unfolding g_def
moreover have "v ∈ B"
if "g v ≠ 0" for v
using that unfolding g_def
ultimately have rep1: "(∑v∈B. g v *⇩C v) = ψ"
unfolding g_def
using a3 True a1 complex_vector.sum_representation_eq by blast
have l0': "inj ((*⇩C) 𝗂::'a ⇒'a)"
unfolding inj_def
by simp
have l0: "inj ((*⇩C) (- 𝗂)::'a ⇒'a)"
unfolding inj_def
by simp
have l1: "(*⇩C) (- 𝗂)  B ∩ B = {}"
using cindependent_inter_scaleC_cindependent[where B=B and c = "- 𝗂"]
by (metis Int_commute a1 add.inverse_inverse complex_i_not_one i_squared mult_cancel_left1
neg_equal_0_iff_equal)
have l2: "B ∩ (*⇩C) 𝗂  B = {}"
have rr1: "r (𝗂 *⇩C v) = r' v" for v
unfolding r_def r'_def
by simp
have k1: "independent B'"
unfolding B'_def using a1 real_independent_from_complex_independent by simp
have "ψ ∈ span B'"
using B'_def True cspan_as_span by blast
have "v ∈ B'"
if "r v ≠ 0"
for v
unfolding r_def
using r_def real_vector.representation_ne_zero that by auto
have "finite B'"
unfolding B'_def using a3
by simp
have "(∑v∈B'. r v *⇩R v) = ψ"
unfolding r_def
using True  Real_Vector_Spaces.real_vector.sum_representation_eq[where B = B' and basis = B'
and v = ψ]
by (smt Real_Vector_Spaces.dependent_raw_def ‹ψ ∈ Real_Vector_Spaces.span B'› ‹finite B'›
equalityD2 k1)
have d1: "(∑v∈B. r (𝗂 *⇩C v) *⇩R (𝗂 *⇩C v)) = (∑v∈(*⇩C) 𝗂  B. r v *⇩R v)"
using l0'
by (metis (mono_tags, lifting) inj_eq inj_on_def sum.reindex_cong)
have "(∑v∈B. (r v + 𝗂 * (r' v)) *⇩C v) = (∑v∈B. r v *⇩C v + (𝗂 * r' v) *⇩C v)"
also have "… = (∑v∈B. r v *⇩C v) + (∑v∈B. (𝗂 * r' v) *⇩C v)"
using sum.distrib by fastforce
also have "… = (∑v∈B. r v *⇩C v) + (∑v∈B. 𝗂 *⇩C (r' v *⇩C v))"
by auto
also have "… = (∑v∈B. r v *⇩R v) + (∑v∈B. 𝗂 *⇩C (r (𝗂 *⇩C v) *⇩R v))"
unfolding r'_def r_def
by (metis (mono_tags, lifting) scaleR_scaleC sum.cong)
also have "… = (∑v∈B. r v *⇩R v) + (∑v∈B. r (𝗂 *⇩C v) *⇩R (𝗂 *⇩C v))"
by (metis (no_types, lifting) complex_vector.scale_left_commute scaleR_scaleC)
also have "… = (∑v∈B. r v *⇩R v) + (∑v∈(*⇩C) 𝗂  B. r v *⇩R v)"
using d1
by simp
also have "… = ψ"
using l2 ‹(∑v∈B'. r v *⇩R v) = ψ›
unfolding B'_def
finally have "(∑v∈B. f v *⇩C v) = ψ" unfolding r'_def r_def f_def by simp
hence "0 = (∑v∈B. f v *⇩C v) - (∑v∈B. crepresentation B ψ v *⇩C v)"
using rep1
unfolding g_def
by simp
also have "… = (∑v∈B. f v *⇩C v - crepresentation B ψ v *⇩C v)"
also have "… = (∑v∈B. (f v - crepresentation B ψ v) *⇩C v)"
by (metis scaleC_left.diff)
finally have "0 = (∑v∈B. (f v - crepresentation B ψ v) *⇩C v)".
hence "(∑v∈B. (f v - crepresentation B ψ v) *⇩C v) = 0"
by simp
hence "f b - crepresentation B ψ b = 0"
using a1 a2 a3 complex_vector.independentD[where s = B and t = B
and u = "λv. f v - crepresentation B ψ v" and v = b]
order_refl  by smt
hence "crepresentation B ψ b = f b"
by simp
thus ?thesis unfolding f_def r_def r'_def B'_def by auto
next
define B' where "B' = B ∪ (*⇩C) 𝗂  B"
case False
have b2: "ψ ∉ real_vector.span B'"
unfolding B'_def
using False cspan_as_span by auto
have "ψ ∉ complex_vector.span B"
using False by blast
have "crepresentation B ψ b = 0"
unfolding complex_vector.representation_def
moreover have "real_vector.representation B' ψ b = 0"
unfolding real_vector.representation_def
moreover have "real_vector.representation B' ψ ((*⇩C) 𝗂 b) = 0"
unfolding real_vector.representation_def
ultimately show ?thesis unfolding B'_def by simp
qed

lemma CARD_1_vec_0[simp]: ‹(ψ :: _ ::{complex_vector,CARD_1}) = 0›
by auto

lemma scaleC_cindependent:
assumes a1: "cindependent (B::'a::complex_vector set)" and a3: "c ≠ 0"
shows "cindependent ((*⇩C) c  B)"
proof-
have "u y = 0"
if g1: "y∈S" and g2: "(∑x∈S. u x *⇩C x) = 0" and g3: "finite S" and g4: "S⊆(*⇩C) c  B"
for u y S
proof-
define v where "v x = u (c *⇩C x)" for x
obtain S' where "S'⊆B" and S_S': "S = (*⇩C) c  S'"
by (meson g4 subset_imageE)
have "inj ((*⇩C) c::'a⇒_)"
unfolding inj_def
using a3 by auto
hence "finite S'"
using S_S' finite_imageD g3 subset_inj_on by blast
have "t ∈ (*⇩C) (inverse c)  S"
if "t ∈ S'" for t
proof-
have "c *⇩C t ∈ S"
using ‹S = (*⇩C) c  S'› that by blast
hence "(inverse c) *⇩C (c *⇩C t) ∈ (*⇩C) (inverse c)  S"
by blast
moreover have "(inverse c) *⇩C (c *⇩C t) = t"
ultimately show ?thesis by simp
qed
moreover have "t ∈ S'"
if "t ∈ (*⇩C) (inverse c)  S" for t
proof-
obtain t' where "t = (inverse c) *⇩C t'" and "t' ∈ S"
using ‹t ∈ (*⇩C) (inverse c)  S› by auto
have "c *⇩C t = c *⇩C ((inverse c) *⇩C t')"
using ‹t = (inverse c) *⇩C t'› by simp
also have "… = (c * (inverse c)) *⇩C t'"
by simp
also have "… = t'"
finally have "c *⇩C t = t'".
thus ?thesis using ‹t' ∈ S›
using ‹S = (*⇩C) c  S'› a3 complex_vector.scale_left_imp_eq by blast
qed
ultimately have "S' = (*⇩C) (inverse c)  S"
by blast
hence "inverse c *⇩C y ∈ S'"
using that(1) by blast
have t: "inj (((*⇩C) c)::'a ⇒ _)"
using a3 complex_vector.injective_scale[where c = c]
by blast
have "0 = (∑x∈(*⇩C) c  S'. u x *⇩C x)"
using ‹S = (*⇩C) c  S'› that(2) by auto
also have "… = (∑x∈S'. v x *⇩C (c *⇩C x))"
unfolding v_def
using t Groups_Big.comm_monoid_add_class.sum.reindex[where h = "((*⇩C) c)" and A = S'
and g = "λx. u x *⇩C x"] subset_inj_on by auto
also have "… = c *⇩C (∑x∈S'. v x *⇩C x)"
by (metis (mono_tags, lifting) complex_vector.scale_left_commute scaleC_right.sum sum.cong)
finally have "0 = c *⇩C (∑x∈S'. v x *⇩C x)".
hence "(∑x∈S'. v x *⇩C x) = 0"
using a3 by auto
hence "v (inverse c *⇩C y) = 0"
using ‹inverse c *⇩C y ∈ S'› ‹finite S'› ‹S' ⊆ B› a1
complex_vector.independentD
by blast
thus "u y = 0"
unfolding v_def
qed
thus ?thesis
using complex_vector.dependent_explicit
qed

subsection ‹Antilinear maps and friends›

locale antilinear = additive f for f :: "'a::complex_vector ⇒ 'b::complex_vector" +
assumes scaleC: "f (scaleC r x) = cnj r *⇩C f x"

sublocale antilinear ⊆ linear
proof (rule linearI)
show "f (b1 + b2) = f b1 + f b2"
for b1 :: 'a
and b2 :: 'a
show "f (r *⇩R b) = r *⇩R f b"
for r :: real
and b :: 'a
unfolding scaleR_scaleC by (subst scaleC, simp)
qed

lemma antilinear_imp_scaleC:
fixes D :: "complex ⇒ 'a::complex_vector"
assumes "antilinear D"
obtains d where "D = (λx. cnj x *⇩C d)"
proof -
interpret clinear "D o cnj"
apply standard apply auto
by (rule antilinear_imp_scaleC [OF assms]) (force simp: scaleC_co`