Theory Extra_General

section Extra_General› -- General missing things

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

subsection Misc

lemma reals_zero_comparable:
  fixes x::complex
  assumes "x"
  shows "x  0  x  0"
  using assms unfolding complex_is_real_iff_compare0 by assumption

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

lemma sum_single: 
  assumes "finite A"
  assumes "j. j  i  jA  f j = 0"
  shows "sum f A = (if iA 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 L2_set_mono2:
  assumes a1: "finite L" and a2: "K  L"
  shows "L2_set f K  L2_set f L"
proof-
  have "(iK. (f i)2)  (iL. (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 (iK. (f i)2)  sqrt (iL. (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 "xS. 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 classCARD_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 "AB"
  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="YX"] 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 "AB"
  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
  by (simp add: less_eq_complex_def)


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

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

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

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

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

  have "norm (x i * y i) ≤ norm (x i * x i) + norm (y i * y i)" for i
    unfolding norm_mult
    by (smt mult_left_mono mult_nonneg_nonneg mult_right_mono norm_ge_zero)
  hence "(∑i∈F. norm (x i * y i)) ≤ (∑i∈F. norm (x i * x i) + norm (y i * y i))"
    by (simp add: sum_mono)
  also have "… = (∑i∈F. norm (x i * x i)) + (∑i∈F. norm (y i * y i))"
    by (simp add: sum.distrib)
  also have "… = (∑i∈F. norm (x i * x i)) + (∑i∈F. norm (y i * y i))"
    by (simp add: ‹finite F›)
  also have "… ≤ (∑i∈A. norm (x i * x i)) + (∑i∈A. norm (y i * y i))" 
    by (smt (verit, del_insts) a1 Diff_iff Infinite_Sum.infsum_nonneg assms(2) b4 infsum_def infsum_mono_neutral norm_ge_zero subset_eq)
  finally show ‹(∑xa∈F. norm (x xa * y xa)) ≤ (∑i∈A. norm (x i * x i)) + (∑i∈A. norm (y i * y i))›
    by simp
qed *)

end