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›
overloading heterogenous_identity_id ≡ "heterogenous_identity :: 'a ⇒ 'a" begin
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) ≠ -∞›
    by (simp add: SUP_eq_iff assms(3))
  ultimately have Sup_bdd: ‹¦Sup (ereal ` S)¦ ≠ ∞›
    by auto
  then have ‹∃x'∈ereal ` S. Sup (ereal ` S) - ereal e < x'›
    apply (rule_tac Sup_ereal_close)
    using assms by auto
  then obtain x where ‹x ∈ S› and Sup_x: ‹Sup (ereal ` S) - ereal e < ereal x›
    by auto
  have ‹Sup (ereal ` S) = ereal (Sup S)›
    using Sup_bdd by (rule ereal_Sup[symmetric])
  with Sup_x have ‹ereal (Sup S - e) < ereal x›
    by auto
  then have ‹Sup S - e < x›
    by auto
  with ‹x ∈ S› show ?thesis
    by auto
qed

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

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

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)

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

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

subsection ‹\<^class>‹CARD_1››

context CARD_1 begin

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

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

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

end

instance unit :: CARD_1
  apply standard by auto

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

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


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



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


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

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

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


lemma finite_subsets_at_top_inter: 
  assumes "A⊆B"
  shows "filtermap (λF. F ∩ A) (finite_subsets_at_top B) ≤ finite_subsets_at_top A"
proof (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
  by (simp add: abs_complex_def)

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


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

lemma cnj_x_x_geq0[simp]: "cnj x * x ≥ 0"
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) []"
    by (simp add: map_filter_simps)
  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 []"
    by (simp add: map_filter_simps)
  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"
  by (simp add: inj_map_def)

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

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

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

end

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
    by (simp add: mult.commute)
  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)"
      by (simp add: distrib_left mult.commute)
    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))"
      by (simp add: mult.assoc)
    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
    by (simp add: sum_nonneg)
  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

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"
    by (simp add: add_mono mult_left_mono)
  with assms show ?thesis
    unfolding distrib_right[symmetric] by simp
qed

end

subclass (in linordered_semiring_1) ordered_semiring_1 ..

class ordered_semiring_strict = semiring + comm_monoid_add + ordered_cancel_ab_semigroup_add +
  ― ‹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
    by (simp add: local.mult_strict_left_mono) 
  show "a * c < b * c"
    if "a < b"
      and "0 < c"
    for a :: 'a
      and b 
      and c 
    using that
    by (simp add: local.mult_strict_right_mono) 
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
  by (simp add: local.mult_strict_left_mono)

class ordered_ring_strict = ring + ordered_semiring_strict
  + ordered_ab_group_add + partial_abs_if
  ― ‹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))"
  by (auto simp add: eq_divide_eq)

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

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"
      by (simp add: t2)      
    moreover have "0 ≤ c-b"
      by (simp add: t3)      
    ultimately have "c-a ≤ c-b ∨ c-a ≥ c-b" by (rule nn_comparable)
    hence "-a ≤ -b ∨ -a ≥ -b"
      using local.add_le_imp_le_right local.uminus_add_conv_diff by presburger
    thus ?thesis
      by (simp add: t1)
  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"
      by (simp add: t2)        
    moreover have "0 ≤ b-c"
      by (simp add: t3)      
    ultimately have "a-c ≤ b-c ∨ a-c ≥ b-c" by (rule nn_comparable)
    hence "a ≤ b ∨ a ≥ b"
      by (simp add: local.le_diff_eq)
    thus ?thesis
      by (simp add: t1)
  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"],
      simp add: nonzero_inverse_minus_eq less_imp_not_eq)

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
  from add_strict_right_mono[OF m1, where c=x]
  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
  from add_strict_right_mono[OF m1, where c=x]
  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"
  by(simp add:field_simps)

lemma divide_nonneg_pos:
  "0 ≤ x ⟹ 0 < y ⟹ 0 ≤ x / y"
  by(simp add:field_simps)

lemma divide_neg_pos:
  "x < 0 ⟹ 0 < y ⟹ x / y < 0"
  by(simp add:field_simps)

lemma divide_nonpos_pos:
  "x ≤ 0 ⟹ 0 < y ⟹ x / y ≤ 0"
  by(simp add:field_simps)

lemma divide_pos_neg:
  "0 < x ⟹ y < 0 ⟹ x / y < 0"
  by(simp add:field_simps)

lemma divide_nonneg_neg:
  "0 ≤ x ⟹ y < 0 ⟹ x / y ≤ 0"
  by(simp add:field_simps)

lemma divide_neg_neg:
  "x < 0 ⟹ y < 0 ⟹ 0 < x / y"
  by(simp add:field_simps)

lemma divide_nonpos_neg:
  "x ≤ 0 ⟹ y < 0 ⟹ 0 ≤ x / y"
  by(simp add:field_simps)

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"
  by (simp add: local.neg_less_divide_eq)

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"
  by(simp add:field_simps)

lemma mult_imp_div_pos_less: "0 < y ⟹ x < z * y ⟹ x / y < z"
  by(simp add:field_simps)

lemma mult_imp_less_div_pos: "0 < y ⟹ z * y < x ⟹ z < x / y"
  by(simp add:field_simps)

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)"
  by (metis local.add_pos_pos local.add_strict_left_mono local.mult_imp_less_div_pos local.semiring_normalization_rules(4) local.zero_less_one mult_commute)

lemma gt_half_sum: "a < b ⟹ (a+b)/(1+1) < b"
  by (metis local.add_pos_pos local.add_strict_left_mono local.mult_imp_div_pos_less local.semiring_normalization_rules(24) local.semiring_normalization_rules(4) local.zero_less_one mult_commute)

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)"
    by (rule add_strict_right_mono)
  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"
  by (simp add: local.dual_order.order_iff_strict)

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"
  by (simp add: local.dual_order.strict_iff_order)

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)"
  by (simp add: local.pos_le_divide_eq)

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)"
  by (simp add: local.dual_order.strict_iff_order)

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¦"
  by (simp add: local.abs_pos)

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
    by (simp add: field_simps)
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
    by (simp add: cmod_eq_Re complex_is_Real_iff)
  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