Theory Misc_Tensor_Product_TTS

section ‹‹Misc_Tensor_Product_TTS› -- Miscelleanous results missing from \<^session>‹Complex_Bounded_Operators››

text ‹Here specifically results obtained from lifting existing results using the types to sets mechanism (\<^cite>‹"types-to-sets"›).›

theory Misc_Tensor_Product_TTS
  imports
    Complex_Bounded_Operators.Complex_L2

    Misc_Tensor_Product
    With_Type.With_Type
begin

unbundle lattice_syntax and cblinfun_syntax

subsection ‹Retrieving axioms›

attribute_setup axiom = ‹Scan.lift Parse.name_position >> (fn name_pos => Thm.rule_attribute [] 
    (fn context => fn _ =>
       let val thy = Context.theory_of context
           val (full_name, _) = Name_Space.check context (Theory.axiom_table thy) name_pos
       in Thm.axiom thy full_name end))› 
  ‹Retrieve an axiom by name. E.g., write @{thm [source] [[axiom HOL.refl]]}.›

subsection ‹Auxiliary lemmas›

named_theorems unoverload_def

locale local_typedef = fixes S ::"'b set" and s::"'s itself"
  assumes Ex_type_definition_S: "∃(Rep::'s ⇒ 'b) (Abs::'b ⇒ 's). type_definition Rep Abs S"
begin
definition "Rep = fst (SOME (Rep::'s ⇒ 'b, Abs). type_definition Rep Abs S)"
definition "Abs = snd (SOME (Rep::'s ⇒ 'b, Abs). type_definition Rep Abs S)"
lemma type_definition_S: "type_definition Rep Abs S"
  unfolding Abs_def Rep_def split_beta'
  by (rule someI_ex) (use Ex_type_definition_S in auto)
lemma rep_in_S[simp]: "Rep x ∈ S"
  and rep_inverse[simp]: "Abs (Rep x) = x"
  and Abs_inverse[simp]: "y ∈ S ⟹ Rep (Abs y) = y"
  using type_definition_S
  unfolding type_definition_def by auto
definition cr_S where "cr_S ≡ λs b. s = Rep b"
lemma Domainp_cr_S[transfer_domain_rule]: "Domainp cr_S = (λx. x ∈ S)"
  by (metis Abs_inverse Domainp.simps cr_S_def rep_in_S)
lemma right_total_cr_S[transfer_rule]: "right_total cr_S"
  by (rule typedef_right_total[OF type_definition_S cr_S_def])
lemma bi_unique_cr_S[transfer_rule]: "bi_unique cr_S"
  by (rule typedef_bi_unique[OF type_definition_S cr_S_def])
lemma left_unique_cr_S[transfer_rule]: "left_unique cr_S"
  by (rule typedef_left_unique[OF type_definition_S cr_S_def])
lemma right_unique_cr_S[transfer_rule]: "right_unique cr_S"
  by (rule typedef_right_unique[OF type_definition_S cr_S_def])
lemma cr_S_Rep[intro, simp]: "cr_S (Rep a) a" by (simp add: cr_S_def)
lemma cr_S_Abs[intro, simp]: "a∈S ⟹ cr_S a (Abs a)" by (simp add: cr_S_def)
lemma UNIV_transfer[transfer_rule]: ‹rel_set cr_S S UNIV›
  using Domainp_cr_S right_total_cr_S right_total_UNIV_transfer by fastforce
end

lemma complete_space_as_set[simp]: ‹complete (space_as_set V)› for V :: ‹_::cbanach ccsubspace›
  by (simp add: complete_eq_closed)

definition ‹transfer_ball_range A P ⟷ (∀f. range f ⊆ A ⟶ P f)›

lemma transfer_ball_range_parametric'[transfer_rule]:
  includes lifting_syntax
  assumes [transfer_rule, simp]: ‹right_unique T› ‹bi_total T› ‹bi_unique U›
  shows ‹(rel_set U ===> ((T ===> U) ===> (⟶)) ===> (⟶)) transfer_ball_range transfer_ball_range›
proof (intro rel_funI impI, rename_tac A B P Q)
  fix A B P Q
  assume [transfer_rule]: ‹rel_set U A B›
  assume TUPQ[transfer_rule]: ‹((T ===> U) ===> (⟶)) P Q›
  assume ‹transfer_ball_range A P›
  then have Pf: ‹P f› if ‹range f ⊆ A› for f
    unfolding transfer_ball_range_def using that by auto
  have ‹Q g› if ‹range g ⊆ B› for g
  proof -
    from that ‹rel_set U A B›
    have ‹Rangep (T ===> U) g›
      apply (auto simp add: conversep_rel_fun Domainp_pred_fun_eq simp flip: Domainp_conversep)
      apply (simp add: Domainp_conversep)
      by (metis Rangep.simps range_subsetD rel_setD2)
    then obtain f where TUfg[transfer_rule]: ‹(T ===> U) f g›
      by blast
    from that have ‹range f ⊆ A›
      by transfer
    then have ‹P f›
      by (simp add: Pf)
    then show ‹Q g›
      by (metis TUfg TUPQ rel_funD)
  qed
  then show ‹transfer_ball_range B Q›
  by (simp add: transfer_ball_range_def)
qed

lemma transfer_ball_range_parametric[transfer_rule]:
  includes lifting_syntax
  assumes [transfer_rule, simp]: ‹bi_unique T› ‹bi_total T› ‹bi_unique U›
  shows ‹(rel_set U ===> ((T ===> U) ===> (⟷)) ===> (⟷)) transfer_ball_range transfer_ball_range›
proof -
  have ‹(rel_set U ===> ((T ===> U) ===> (⟶)) ===> (⟶)) transfer_ball_range transfer_ball_range›
    using assms(1) assms(2) assms(3) bi_unique_alt_def transfer_ball_range_parametric' by blast
  then have 1: ‹(rel_set U ===> ((T ===> U) ===> (⟷)) ===> (⟶)) transfer_ball_range transfer_ball_range›
    apply (rule rev_mp)
    apply (intro rel_fun_mono')
    by auto

  have ‹(rel_set (U¯¯) ===> ((T¯¯ ===> U¯¯) ===> (⟶)) ===> (⟶)) transfer_ball_range transfer_ball_range›
    apply (rule transfer_ball_range_parametric')
    using assms(1) bi_unique_alt_def bi_unique_conversep apply blast
    by auto
  then have ‹(rel_set U ===> ((T ===> U) ===> (⟶)¯¯) ===> (⟶)¯¯) transfer_ball_range transfer_ball_range›
    apply (rule_tac conversepD[where r=‹(rel_set U ===> ((T ===> U) ===> (⟶)¯¯) ===> (⟶)¯¯)›])
    by (simp add: conversep_rel_fun del: conversep_iff)
  then have 2: ‹(rel_set U ===> ((T ===> U) ===> (⟷)) ===> (⟶)¯¯) transfer_ball_range transfer_ball_range›
    apply (rule rev_mp)
    apply (intro rel_fun_mono')
    by (auto simp: rev_implies_def)

  from 1 2 show ?thesis
    apply (auto intro!: rel_funI simp: conversep_iff[abs_def])
     apply (smt (z3) rel_funE)
    by (smt (verit) rel_funE rev_implies_def)
qed

definition ‹transfer_Times A B = A × B›

lemma transfer_Times_parametricity[transfer_rule]:
  includes lifting_syntax
  shows ‹(rel_set T ===> rel_set U ===> rel_set (rel_prod T U)) transfer_Times transfer_Times›
  by (auto intro!: rel_funI simp add: transfer_Times_def rel_set_def)


lemma csubspace_nonempty: ‹csubspace X ⟹ X ≠ {}›
  using complex_vector.subspace_0 by auto


definition ‹transfer_vimage_into f U s = (f -` U) ∩ s›

lemma transfer_vimage_into_parametric[transfer_rule]:
  includes lifting_syntax
  assumes [transfer_rule]: ‹bi_unique A› ‹bi_unique B›
  shows ‹((A ===> B) ===> rel_set B ===> rel_set A ===> rel_set A) transfer_vimage_into transfer_vimage_into›
  unfolding transfer_vimage_into_def
  apply (auto intro!: rel_funI simp: rel_set_def)
  by (metis Int_iff apply_rsp' assms bi_unique_def vimage_eq)+

(* Simplify with these theorems to (try to) change all ‹∀x. ...› into ‹∀x∈S. ...› (and similar)
  to enable automated creation of parametricity rules without `bi_total` assumptions. *)
lemma make_parametricity_proof_friendly:
  shows ‹(∀x. P ⟶ Q x) ⟷ (P ⟶ (∀x. Q x))›
    and ‹(∀x. x ∈ S ⟶ Q x) ⟷ (∀x∈S. Q x)›
    and ‹(∀x⊆S. R x) ⟷ (∀x∈Pow S. R x)›
    and ‹{x∈S. Q x} = Set.filter Q S›
    and ‹{x. x ⊆ S ∧ R x} = Set.filter R (Pow S)›
    and ‹⋀P. (∀f. range f ⊆ A ⟶ P f) = transfer_ball_range A P›
    and ‹⋀A B. A × B = transfer_Times A B›
    and ‹⋀B P. (∃A⊆B. P A) ⟷ (∃A∈Pow B. P A)›
    and ‹⋀f U s. (f -` U) ∩ s = transfer_vimage_into f U s›
    and ‹⋀M B. ⨅M ⊓ principal B = transfer_bounded_filter_Inf B M›
    and ‹⋀F M. F ⊓ principal M = transfer_inf_principal F M›
  by (auto simp: transfer_ball_range_def transfer_Times_def transfer_vimage_into_def
      transfer_bounded_filter_Inf_def transfer_inf_principal_def)

subsection ‹\<^class>‹plus››

locale plus_ow =
  fixes U plus
  assumes ‹∀x∈U. ∀y∈U. plus x y ∈ U›
lemma plus_ow_parametricity[transfer_rule]:
  includes lifting_syntax
  assumes [transfer_rule]: ‹bi_unique A›
  shows ‹(rel_set A ===> (A ===> A ===> A) ===> (=)) 
     plus_ow plus_ow›
  unfolding plus_ow_def
  by transfer_prover

subsubsection ‹\<^class>‹minus››

locale minus_ow = fixes U minus assumes ‹∀x∈U. ∀y∈U. minus x y ∈ U›

lemma minus_ow_parametricity[transfer_rule]:
  includes lifting_syntax
  assumes [transfer_rule]: ‹bi_unique A›
  shows ‹(rel_set A ===> (A ===> A ===> A) ===> (=)) 
     minus_ow minus_ow›
  unfolding minus_ow_def
  by transfer_prover

subsubsection ‹\<^class>‹uminus››

locale uminus_ow = fixes U uminus assumes ‹∀x∈U. uminus x ∈ U›

lemma uminus_ow_parametricity[transfer_rule]:
  includes lifting_syntax
  assumes [transfer_rule]: ‹bi_unique A›
  shows ‹(rel_set A ===> (A ===> A) ===> (=)) 
     uminus_ow uminus_ow›
  unfolding uminus_ow_def
  by transfer_prover

subsection ‹\<^locale>‹semigroup››

locale semigroup_ow = plus_ow U plus for U plus +
  assumes ‹∀x∈U. ∀y∈U. ∀z∈U. plus x (plus y z) = plus (plus x y) z›

lemma semigroup_ow_parametricity[transfer_rule]:
  includes lifting_syntax
  assumes [transfer_rule]: ‹bi_unique A›
  shows ‹(rel_set A ===> (A ===> A ===> A) ===> (=)) 
     semigroup_ow semigroup_ow›
  unfolding semigroup_ow_def semigroup_ow_axioms_def
  by transfer_prover

lemma semigroup_ow_typeclass[simp, iff]: ‹semigroup_ow V (+)›
  if ‹⋀x y. x∈V ⟹ y∈V ⟹ x + y ∈ V› for V :: ‹'a :: semigroup_add set›
  by (auto intro!: plus_ow.intro semigroup_ow.intro semigroup_ow_axioms.intro simp: Groups.add_ac that)

lemma class_semigroup_add_ud[unoverload_def]: ‹class.semigroup_add = semigroup_ow UNIV›
  by (auto intro!: ext plus_ow.intro simp: class.semigroup_add_def semigroup_ow_def semigroup_ow_axioms_def)

subsection ‹\<^locale>‹abel_semigroup››

locale abel_semigroup_ow = semigroup_ow U plus for U plus +
  assumes ‹∀x∈U. ∀y∈U. plus x y = plus y x›

lemma abel_semigroup_ow_parametric[transfer_rule]:
  includes lifting_syntax
  assumes [transfer_rule]: ‹bi_unique A›
  shows ‹(rel_set A ===> (A ===> A ===> A) ===> (=))
     abel_semigroup_ow abel_semigroup_ow›
  unfolding abel_semigroup_ow_def abel_semigroup_ow_axioms_def make_parametricity_proof_friendly
  by transfer_prover

lemma abel_semigroup_ow_typeclass[simp, iff]: ‹abel_semigroup_ow V (+)›
  if ‹⋀x y. x∈V ⟹ y∈V ⟹ x + y ∈ V› for V :: ‹'a :: ab_semigroup_add set›
  by (auto simp: abel_semigroup_ow_def abel_semigroup_ow_axioms_def Groups.add_ac that)

lemma class_ab_semigroup_add_ud[unoverload_def]: ‹class.ab_semigroup_add = abel_semigroup_ow UNIV›
  by (auto intro!: ext simp: class.ab_semigroup_add_def abel_semigroup_ow_def 
      class_semigroup_add_ud abel_semigroup_ow_axioms_def class.ab_semigroup_add_axioms_def)

subsection ‹\<^locale>‹comm_monoid››

locale comm_monoid_ow = abel_semigroup_ow U plus for U plus +
  fixes zero
  assumes ‹zero ∈ U›
  assumes ‹∀x∈U. plus x zero = x›

lemma comm_monoid_ow_parametric[transfer_rule]:
  includes lifting_syntax
  assumes [transfer_rule]: ‹bi_unique A›
  shows ‹(rel_set A ===> (A ===> A ===> A) ===> A ===> (=))
     comm_monoid_ow comm_monoid_ow›
  unfolding comm_monoid_ow_def comm_monoid_ow_axioms_def make_parametricity_proof_friendly
  by transfer_prover

lemma comm_monoid_ow_typeclass[simp, iff]: ‹comm_monoid_ow V (+) 0›
  if ‹0 ∈ V› and ‹⋀x y. x∈V ⟹ y∈V ⟹ x + y ∈ V› for V :: ‹'a :: comm_monoid_add set›
  by (auto simp: comm_monoid_ow_def comm_monoid_ow_axioms_def that)

lemma class_comm_monoid_add_ud[unoverload_def]: ‹class.comm_monoid_add = comm_monoid_ow UNIV›
  apply (auto intro!: ext simp: class.comm_monoid_add_def comm_monoid_ow_def
      class_ab_semigroup_add_ud class.comm_monoid_add_axioms_def comm_monoid_ow_axioms_def)
  by (simp_all add: abel_semigroup_ow_def abel_semigroup_ow_axioms_def)

subsection ‹\<^class>‹topological_space››

locale topological_space_ow = 
  fixes U "open"
  assumes ‹open U›
  assumes ‹∀S⊆U. ∀T⊆U. open S ⟶ open T ⟶ open (S ∩ T)›
  assumes "∀K⊆Pow U. (∀S∈K. open S) ⟶ open (⋃K)"

lemma topological_space_ow_parametricity[transfer_rule]:
  includes lifting_syntax
  assumes [transfer_rule]: ‹bi_unique A›
  shows ‹(rel_set A ===> (rel_set A ===> (=)) ===> (=)) 
     topological_space_ow topological_space_ow›
  unfolding topological_space_ow_def make_parametricity_proof_friendly
  by transfer_prover

lemma class_topological_space_ud[unoverload_def]: ‹class.topological_space = topological_space_ow UNIV›
  by (auto intro!: ext simp: class.topological_space_def topological_space_ow_def)

lemma topological_space_ow_from_topology[simp]: ‹topological_space_ow (topspace T) (openin T)›
  by (auto intro!: topological_space_ow.intro)

subsection ‹\<^const>‹sum››

definition ‹sum_ow z plus f S = 
  (if finite S then the_default z (Collect (fold_graph (plus o f) z S)) else z)›
  for U z plus S

lemma sum_ow_parametric[transfer_rule]:
  includes lifting_syntax
  assumes [transfer_rule]: ‹bi_unique T› ‹bi_unique U›
  shows ‹(T ===> (V ===> T ===> T) ===> (U ===> V) ===> rel_set U ===> T)
            sum_ow sum_ow›
  unfolding sum_ow_def
  by transfer_prover

lemma (in comm_monoid_set) comp_fun_commute_onI: ‹Finite_Set.comp_fun_commute_on UNIV ((❙*) ∘ g)›
  apply (rule Finite_Set.comp_fun_commute_on.intro)
  by (simp add: o_def left_commute)

lemma (in comm_monoid_set) F_via_the_default: ‹F g A = the_default def (Collect (fold_graph ((❙*) ∘ g) ❙1 A))›
  if ‹finite A›
proof -
  have ‹y = x› if ‹fold_graph ((❙*) ∘ g) ❙1 A x› and ‹fold_graph ((❙*) ∘ g) ❙1 A y› for x y
    using that apply (rule Finite_Set.comp_fun_commute_on.fold_graph_determ[rotated 2, where S=UNIV])
    by (simp_all add: comp_fun_commute_onI)
  then have ‹Ex1 (fold_graph ((❙*) ∘ g) ❙1 A)›
    by (meson finite_imp_fold_graph that)
  then have ‹card (Collect (fold_graph ((❙*) ∘ g) ❙1 A)) = 1›
    using card_eq_Suc_0_ex1 by fastforce
  then show ?thesis
    using that by (auto simp add: the_default_The eq_fold Finite_Set.fold_def)
qed

lemma sum_ud[unoverload_def]: ‹sum = sum_ow 0 plus›
  apply (auto intro!: ext simp: sum_def sum_ow_def comm_monoid_set.F_via_the_default)
   apply (subst comm_monoid_set.F_via_the_default)
    apply (auto simp add: sum.comm_monoid_set_axioms)
  by (metis comm_monoid_add_class.sum_def sum.infinite)

(* declare sum_with[unoverload_def del] *)

subsection ‹\<^class>‹t2_space››

locale t2_space_ow = topological_space_ow +
  assumes ‹∀x∈U. ∀y∈U. x ≠ y ⟶ (∃S⊆U. ∃T⊆U. open S ∧ open T ∧ x ∈ S ∧ y ∈ T ∧ S ∩ T = {})›

lemma t2_space_ow_parametric[transfer_rule]:
  includes lifting_syntax
  assumes [transfer_rule]: ‹bi_unique A›
  shows ‹(rel_set A ===> (rel_set A ===> (=)) ===> (=)) 
     t2_space_ow t2_space_ow›
  unfolding t2_space_ow_def t2_space_ow_axioms_def make_parametricity_proof_friendly
  by transfer_prover

lemma class_t2_space_ud[unoverload_def]: ‹class.t2_space = t2_space_ow UNIV›
  by (auto intro!: ext simp: class.t2_space_def class.t2_space_axioms_def t2_space_ow_def
      t2_space_ow_axioms_def class_topological_space_ud)

lemma t2_space_ow_from_topology[simp, iff]: ‹t2_space_ow (topspace T) (openin T)› if ‹Hausdorff_space T›
  using that
  apply (auto intro!: t2_space_ow.intro simp: t2_space_ow_axioms_def Hausdorff_space_def disjnt_def)
  by (metis openin_subset)

subsubsection ‹\<^const>‹continuous_on››

definition continuous_on_ow where ‹continuous_on_ow A B opnA opnB s f 
  ⟷ (∀U⊆B. opnB U ⟶ (∃V⊆A. opnA V ∧ (V ∩ s) = (f -` U) ∩ s))›
  for f :: ‹'a ⇒ 'b›

lemma continuous_on_ud[unoverload_def]: ‹continuous_on s f ⟷ continuous_on_ow UNIV UNIV open open s f›
  for f :: ‹'a::topological_space ⇒ 'b::topological_space›
  unfolding continuous_on_ow_def continuous_on_open_invariant by auto

lemma continuous_on_ow_parametric[transfer_rule]:
  includes lifting_syntax
  assumes [transfer_rule]: ‹bi_unique A› ‹bi_unique B›
  shows ‹(rel_set A ===> rel_set B ===> (rel_set A ===> (⟷)) ===> (rel_set B ===> (⟷)) ===> rel_set A ===> (A ===> B) ===> (⟷)) continuous_on_ow continuous_on_ow›
  unfolding continuous_on_ow_def make_parametricity_proof_friendly
  by transfer_prover


subsection ‹\<^class>‹scaleR››

locale scaleR_ow = 
  fixes U and scaleR :: ‹real ⇒ 'a ⇒ 'a›
  assumes scaleR_closed: ‹∀a ∈ U. scaleR r a ∈ U›

lemma scaleR_ow_typeclass[simp]: ‹scaleR_ow UNIV scaleR› for scaleR
  by (simp add: scaleR_ow_def)

lemma scaleR_ow_parametric[transfer_rule]:
  includes lifting_syntax
  assumes [transfer_rule]: ‹bi_unique A›
  shows ‹(rel_set A ===> ((=) ===> A ===> A) ===> (=))
     scaleR_ow scaleR_ow›
  unfolding scaleR_ow_def make_parametricity_proof_friendly
  by transfer_prover

subsection ‹\<^class>‹scaleC››

locale scaleC_ow = scaleR_ow +
  fixes scaleC
  assumes scaleC_closed: ‹∀a∈U. scaleC c a ∈ U›
  assumes ‹∀a∈U. scaleR r a = scaleC (complex_of_real r) a›

lemma scaleC_ow_parametric[transfer_rule]:
  includes lifting_syntax
  assumes [transfer_rule]: ‹bi_unique A›
  shows ‹(rel_set A ===> ((=) ===> A ===> A) ===> ((=) ===> A ===> A) ===> (=))
     scaleC_ow scaleC_ow›
  unfolding scaleC_ow_def scaleC_ow_axioms_def make_parametricity_proof_friendly
  by transfer_prover

lemma class_scaleC_ud[unoverload_def]: ‹class.scaleC = scaleC_ow UNIV›
  by (auto intro!: ext simp: class.scaleC_def scaleC_ow_def scaleR_ow_def scaleC_ow_axioms_def)

subsection ‹\<^class>‹ab_group_add››

locale ab_group_add_ow = comm_monoid_ow U plus zero + minus_ow U minus + uminus_ow U uminus
  for U plus zero minus uminus +
  assumes ‹∀a∈U. uminus a ∈ U›
  assumes "∀a∈U. plus (uminus a) a = zero"
  assumes "∀a∈U. ∀b∈U. minus a b = plus a (uminus b)"

lemma ab_group_add_ow_parametric[transfer_rule]:
  includes lifting_syntax
  assumes [transfer_rule]: ‹bi_unique A›
  shows ‹(rel_set A ===> (A ===> A ===> A) ===> A ===> (A ===> A ===> A) ===> (A ===> A) ===> (=)) 
     ab_group_add_ow ab_group_add_ow›
  unfolding ab_group_add_ow_def ab_group_add_ow_axioms_def
  apply transfer_prover_start
  apply transfer_step+
  by transfer_prover

lemma ab_group_add_ow_typeclass[simp]: 
  ‹ab_group_add_ow V (+) 0 (-) uminus› 
  if ‹0 ∈ V› ‹∀x∈V. -x ∈ V› ‹∀x∈V. ∀y∈V. x + y ∈ V›
  for V :: ‹_ :: ab_group_add set›
  using that
  apply (auto intro!: ab_group_add_ow.intro ab_group_add_ow_axioms.intro comm_monoid_ow_typeclass
      minus_ow.intro uminus_ow.intro)
  by force

lemma class_ab_group_add_ud[unoverload_def]: ‹class.ab_group_add = ab_group_add_ow UNIV›
  by (auto intro!: ext simp: class.ab_group_add_def ab_group_add_ow_def class_comm_monoid_add_ud
      minus_ow_def uminus_ow_def ab_group_add_ow_axioms_def class.ab_group_add_axioms_def)

subsection ‹\<^locale>‹vector_space››

locale vector_space_ow = ab_group_add_ow U plus zero minus uminus
  for U plus zero minus uminus +
  fixes scale :: "'f::field ⇒ 'a ⇒ 'a"
  assumes
    ‹∀x∈U. scale a x ∈ U›
    "∀x∈U. ∀y∈U. scale a (plus x y) = plus (scale a x) (scale a y)"
    "∀x∈U. scale (a + b) x = plus (scale a x) (scale b x)"
    "∀x∈U. scale a (scale b x) = scale (a * b) x"
    "∀x∈U. scale 1 x = x"

lemma vector_space_ow_parametric[transfer_rule]:
  includes lifting_syntax
  assumes [transfer_rule]: ‹bi_unique A›
  shows ‹(rel_set A ===> (A ===> A ===> A) ===> A ===> (A ===> A ===> A) ===> (A ===> A) ===> ((=) ===> A ===> A) ===> (=)) 
     vector_space_ow vector_space_ow›
  unfolding vector_space_ow_def vector_space_ow_axioms_def
  apply transfer_prover_start
                      apply transfer_step+
  by simp

subsection ‹\<^class>‹complex_vector››

locale complex_vector_ow = vector_space_ow U plus zero minus uminus scaleC + scaleC_ow U scaleR scaleC
  for U scaleR scaleC plus zero minus uminus

lemma complex_vector_ow_parametric[transfer_rule]:
  includes lifting_syntax
  assumes [transfer_rule]: ‹bi_unique A›
  shows ‹(rel_set A ===> ((=) ===> A ===> A) ===> ((=) ===> A ===> A) ===> (A ===> A ===> A) ===>
     A ===> (A ===> A ===> A) ===> (A ===> A) ===> (=))
     complex_vector_ow complex_vector_ow›
  unfolding complex_vector_ow_def make_parametricity_proof_friendly
  by transfer_prover

lemma class_complex_vector_ud[unoverload_def]: ‹class.complex_vector = complex_vector_ow UNIV›
  by (auto intro!: ext simp: class.complex_vector_def vector_space_ow_def vector_space_ow_axioms_def
      class.complex_vector_axioms_def class.scaleC_def complex_vector_ow_def
      class_scaleC_ud class_ab_group_add_ud)

lemma vector_space_ow_typeclass[simp]: 
  ‹vector_space_ow V (+) 0 (-) uminus (*⇩C)› 
  if [simp]: ‹csubspace V›
  for V :: ‹_::complex_vector set›
  by (auto intro!: vector_space_ow.intro ab_group_add_ow_typeclass scaleC_left.add
      vector_space_ow_axioms.intro complex_vector.subspace_neg scaleC_add_right
      complex_vector.subspace_add complex_vector.subspace_scale complex_vector.subspace_0)

lemma complex_vector_ow_typeclass[simp]:
  ‹complex_vector_ow V (*⇩R) (*⇩C) (+) 0 (-) uminus› if [simp]: ‹csubspace V›
  by (auto intro!: scaleC_ow_def simp add: complex_vector_ow_def scaleC_ow_def 
      scaleC_ow_axioms_def scaleR_ow_def scaleR_scaleC complex_vector.subspace_scale)


subsection ‹\<^class>‹open_uniformity››

locale open_uniformity_ow = "open" "open" + uniformity uniformity
  for A "open" uniformity +
  assumes open_uniformity:
    "⋀U. U ⊆ A ⟹ open U ⟷ (∀x∈U. eventually (λ(x', y). x' = x ⟶ y ∈ U) uniformity)"

lemma open_uniformity_ow_parametric[transfer_rule]:
  includes lifting_syntax
  assumes [transfer_rule]: ‹bi_unique A›
  shows ‹(rel_set A ===> (rel_set A ===> (=)) ===> rel_filter (rel_prod A A) ===> (=)) 
     open_uniformity_ow open_uniformity_ow›
  unfolding open_uniformity_ow_def make_parametricity_proof_friendly
  by transfer_prover

lemma class_open_uniformity_ud[unoverload_def]: ‹class.open_uniformity = open_uniformity_ow UNIV›
  by (auto intro!: ext simp: class.open_uniformity_def open_uniformity_ow_def)

lemma open_uniformity_on_typeclass[simp]: 
  fixes V :: ‹_::open_uniformity set›
  assumes ‹closed V›
  shows ‹open_uniformity_ow V (openin (top_of_set V)) (uniformity_on V)›
proof (rule open_uniformity_ow.intro, intro allI impI iffI ballI)
  fix U assume ‹U ⊆ V›
  assume ‹openin (top_of_set V) U›
  then obtain T where ‹U = T ∩ V› and ‹open T›
    by (metis Int_ac(3) openin_open)
  with open_uniformity 
  have *: ‹∀⇩F (x', y) in uniformity. x' = x ⟶ y ∈ T› if ‹x ∈ T› for x
    using that by blast
  have ‹∀⇩F (x', y) in uniformity_on V. x' = x ⟶ y ∈ U› if ‹x ∈ U› for x
    apply (rule eventually_inf_principal[THEN iffD2])
    using *[of x] apply (rule eventually_rev_mp)
    using ‹U = T ∩ V› that by (auto intro!: always_eventually)
  then show ‹∀⇩F (x', y) in uniformity_on V. x' = x ⟶ y ∈ U› if ‹x ∈ U› for x
    using that by blast
next
  fix U assume ‹U ⊆ V›
  assume asm: ‹∀x∈U. ∀⇩F (x', y) in uniformity_on V. x' = x ⟶ y ∈ U›
  from asm[rule_format]
  have ‹∀⇩F (x', y) in uniformity. x' ∈ V ∧ y ∈ V ∧ x' = x ⟶ y ∈ U ∪ -V› if ‹x ∈ U› for x
    unfolding eventually_inf_principal
    apply (rule eventually_rev_mp)
    using that by (auto intro!: always_eventually)
  then have xU: ‹∀⇩F (x', y) in uniformity. x' = x ⟶ y ∈ U ∪ -V› if ‹x ∈ U› for x
    apply (rule eventually_rev_mp)
    using that ‹U ⊆ V› by (auto intro!: always_eventually)
  have ‹open (-V)›
    using assms by auto
  with open_uniformity
  have ‹∀⇩F (x', y) in uniformity. x' = x ⟶ y ∈ -V› if ‹x ∈ -V› for x
    using that by blast
  then have xV: ‹∀⇩F (x', y) in uniformity. x' = x ⟶ y ∈ U ∪ -V› if ‹x ∈ -V› for x
    apply (rule eventually_rev_mp)
     apply (rule that)
    apply (rule always_eventually)
    by auto
  have ‹∀⇩F (x', y) in uniformity. x' = x ⟶ y ∈ U ∪ -V› if ‹x ∈ U ∪ -V› for x
    using xV[of x] xU[of x] that
    by auto
  then have ‹open (U ∪ -V)›
    using open_uniformity by blast
  then show ‹openin (top_of_set V) U›
    using ‹U ⊆ V›
    by (auto intro!: exI simp: openin_open)
qed

subsection ‹\<^class>‹uniformity_dist››

locale uniformity_dist_ow = dist dist + uniformity uniformity for U dist uniformity +
  assumes uniformity_dist: "uniformity = (⨅e∈{0<..}. principal {(x, y)∈U×U. dist x y < e})"

lemma class_uniformity_dist_ud[unoverload_def]: ‹class.uniformity_dist = uniformity_dist_ow UNIV›
  by (auto intro!: ext simp: class.uniformity_dist_def uniformity_dist_ow_def)

lemma uniformity_dist_ow_parametric[transfer_rule]:
  includes lifting_syntax
  assumes [transfer_rule]: ‹bi_unique A›
  shows ‹(rel_set A ===> (A ===> A ===> (=)) ===> rel_filter (rel_prod A A) ===> (=))
     uniformity_dist_ow uniformity_dist_ow›
proof -
  have *: "uniformity_dist_ow U dist uniformity ⟷ 
          uniformity = transfer_bounded_filter_Inf (transfer_Times U U)
              ((λe. principal (Set.filter (λ(x,y). dist x y < e) (transfer_Times U U))) ` {0<..})"
  for  U dist uniformity
    unfolding uniformity_dist_ow_def make_parametricity_proof_friendly case_prod_unfold
      prod.collapse
    apply (subst Inf_bounded_transfer_bounded_filter_Inf[where B=‹U×U›])
    by (auto simp: transfer_Times_def)
  show ?thesis
    unfolding *[abs_def]
    by transfer_prover
qed

lemma uniformity_dist_on_typeclass[simp]: ‹uniformity_dist_ow V dist (uniformity_on V)› for V :: ‹_::uniformity_dist set›
  apply (auto simp add: uniformity_dist_ow_def uniformity_dist simp flip: INF_inf_const2)
  apply (subst asm_rl[of ‹⋀x. Restr {(xa, y). dist xa y < x} V = {(xa, y). xa ∈ V ∧ y ∈ V ∧ dist xa y < x}›, rule_format])
  by auto

subsection ‹\<^class>‹sgn››

locale sgn_ow =
  fixes U and sgn :: ‹'a ⇒ 'a›
  assumes sgn_closed: ‹∀a∈U. sgn a ∈ U›

lemma sgn_ow_parametric[transfer_rule]:
  includes lifting_syntax
  assumes [transfer_rule]: ‹bi_unique A›
  shows ‹(rel_set A ===> (A ===> A) ===> (=)) 
     sgn_ow sgn_ow›
  unfolding sgn_ow_def
  by transfer_prover

subsection ‹\<^class>‹sgn_div_norm››

locale sgn_div_norm_ow = scaleR_ow U scaleR + norm norm + sgn_ow U sgn for U sgn norm scaleR +
  assumes "∀x∈U. sgn x = scaleR (inverse (norm x)) x"

lemma class_sgn_div_norm_ud[unoverload_def]: ‹class.sgn_div_norm = sgn_div_norm_ow UNIV›
  by (auto intro!: ext simp: class.sgn_div_norm_def sgn_div_norm_ow_def sgn_div_norm_ow_axioms_def unoverload_def sgn_ow_def)

lemma sgn_div_norm_ow_parametric[transfer_rule]:
  includes lifting_syntax
  assumes [transfer_rule]: ‹bi_unique A›
  shows ‹(rel_set A ===> (A ===> A) ===> (A ===> (=)) ===> ((=) ===> A ===> A) ===> (=)) 
     sgn_div_norm_ow sgn_div_norm_ow›
  unfolding sgn_div_norm_ow_def sgn_div_norm_ow_axioms_def make_parametricity_proof_friendly
  by transfer_prover

lemma sgn_div_norm_on_typeclass[simp]: 
  fixes V :: ‹_::sgn_div_norm set›
  assumes ‹⋀v r. v∈V ⟹ scaleR r v ∈ V›
  shows ‹sgn_div_norm_ow V sgn norm (*⇩R)› 
  using assms 
  by (auto simp add: sgn_ow_def sgn_div_norm_ow_axioms_def scaleR_ow_def sgn_div_norm_ow_def sgn_div_norm)

subsection ‹\<^class>‹dist_norm››

locale dist_norm_ow = dist dist + norm norm + minus_ow U minus for U minus dist norm +
  assumes dist_norm: "∀x∈U. ∀y∈U. dist x y = norm (minus x y)"

lemma dist_norm_ud[unoverload_def]: ‹class.dist_norm = dist_norm_ow UNIV›
  by (auto intro!: ext simp: class.dist_norm_def dist_norm_ow_def dist_norm_ow_axioms_def
      minus_ow_def unoverload_def)

lemma dist_norm_ow_parametric[transfer_rule]:
  includes lifting_syntax
  assumes [transfer_rule]: ‹bi_unique A›
  shows ‹(rel_set A ===> (A ===> A ===> A) ===> (A ===> A ===> (=)) ===> (A ===> (=)) ===> (=))
     dist_norm_ow dist_norm_ow›
  unfolding dist_norm_ow_def dist_norm_ow_axioms_def make_parametricity_proof_friendly
  by transfer_prover

lemma dist_norm_ow_typeclass[simp]: 
  fixes A :: ‹_::dist_norm set›
  assumes ‹⋀a b. ⟦ a ∈ A; b ∈ A ⟧ ⟹ a - b ∈ A›
  shows ‹dist_norm_ow A (-) dist norm› 
  by (auto simp add: assms dist_norm_ow_def minus_ow_def dist_norm_ow_axioms_def dist_norm)

subsection ‹\<^class>‹complex_inner››

locale complex_inner_ow = complex_vector_ow U scaleR scaleC plus zero minus uminus
  + dist_norm_ow U minus dist norm + sgn_div_norm_ow U sgn norm scaleR
  + uniformity_dist_ow U dist uniformity
  + open_uniformity_ow U "open" uniformity
  for U scaleR scaleC plus zero minus uminus dist norm sgn uniformity "open" +
  fixes cinner :: "'a ⇒ 'a ⇒ complex"
  assumes "∀x∈U. ∀y∈U. cinner x y = cnj (cinner y x)"
    and "∀x∈U. ∀y∈U. ∀z∈U. cinner (plus x y) z = cinner x z + cinner y z"
    and "∀x∈U. ∀y∈U. cinner (scaleC r x) y = cnj r * cinner x y"
    and "∀x∈U. 0 ≤ cinner x x"
    and "∀x∈U. cinner x x = 0 ⟷ x = zero"
    and "∀x∈U. norm x = sqrt (cmod (cinner x x))"

lemma class_complex_inner_ud[unoverload_def]: ‹class.complex_inner = complex_inner_ow UNIV›
  apply (intro ext)
  by (simp add: class.complex_inner_def class.complex_inner_axioms_def complex_inner_ow_def complex_inner_ow_axioms_def unoverload_def)

lemma complex_inner_ow_parametricity[transfer_rule]:
  includes lifting_syntax
  assumes [transfer_rule]: ‹bi_unique T›
  shows ‹(rel_set T ===> ((=) ===> T ===> T) ===> ((=) ===> T ===> T) ===> (T ===> T ===> T) ===> T 
          ===> (T ===> T ===> T) ===> (T ===> T) ===> (T ===> T ===> (=)) ===> (T ===> (=))
          ===> (T ===> T) ===> rel_filter (rel_prod T T) ===> (rel_set T ===> (=))
          ===> (T ===> T ===> (=)) ===> (=)) complex_inner_ow complex_inner_ow›
  unfolding complex_inner_ow_def complex_inner_ow_axioms_def
  by transfer_prover

lemma complex_inner_ow_typeclass[simp]:
  fixes V :: ‹_::complex_inner set›
  assumes [simp]: ‹closed V› ‹csubspace V›
  shows ‹complex_inner_ow V (*⇩R) (*⇩C) (+) 0 (-) uminus dist norm sgn (uniformity_on V) (openin (top_of_set V)) (∙⇩C)›
  apply (auto intro!: complex_vector_ow_typeclass dist_norm_ow_typeclass sgn_div_norm_on_typeclass
      simp: complex_inner_ow_def cinner_simps complex_vector.subspace_diff complex_inner_ow_axioms_def
      scaleR_scaleC complex_vector.subspace_scale 
      simp flip: norm_eq_sqrt_cinner)
  by -

subsection ‹\<^const>‹is_ortho_set››

definition is_ortho_set_ow where ‹is_ortho_set_ow zero cinner S ⟷ 
  ((∀x∈S. ∀y∈S. x ≠ y ⟶ cinner x y = 0) ∧ zero ∉ S)›
  for zero cinner

lemma is_ortho_set_ow_parametric[transfer_rule]:
  includes lifting_syntax
  assumes [transfer_rule]: ‹bi_unique A›
  shows ‹(A ===> (A ===> A ===> (=)) ===> rel_set A ===> (=))
     is_ortho_set_ow is_ortho_set_ow›
  unfolding is_ortho_set_ow_def make_parametricity_proof_friendly
  by transfer_prover

lemma is_ortho_set_ud[unoverload_def]: ‹is_ortho_set = is_ortho_set_ow 0 cinner›
  by (auto simp: is_ortho_set_ow_def is_ortho_set_def)

subsection ‹\<^class>‹metric_space››

locale metric_space_ow = uniformity_dist_ow U dist uniformity + open_uniformity_ow U "open" uniformity
  for U dist uniformity "open" +
  assumes "∀x ∈ U. ∀y ∈ U. dist x y = 0 ⟷ x = y"
    and "∀x∈U. ∀y∈U. ∀z∈U. dist x y ≤ dist x z + dist y z"

lemma metric_space_ow_parametric[transfer_rule]:
  includes lifting_syntax
  assumes [transfer_rule]: ‹bi_unique A›
  shows ‹(rel_set A ===> (A ===> A ===> (=)) ===> rel_filter (rel_prod A A) ===>
            (rel_set A ===> (=)) ===> (=))
     metric_space_ow metric_space_ow›
  unfolding metric_space_ow_def metric_space_ow_axioms_def make_parametricity_proof_friendly
  by transfer_prover

lemma class_metric_space_ud[unoverload_def]: ‹class.metric_space = metric_space_ow UNIV›
  by (auto intro!: ext simp: class.metric_space_def class.metric_space_axioms_def metric_space_ow_def metric_space_ow_axioms_def unoverload_def)

lemma metric_space_ow_typeclass[simp]:
  fixes V :: ‹_::metric_space set›
  assumes ‹closed V›
  shows ‹metric_space_ow V dist (uniformity_on V) (openin (top_of_set V))›
  by (auto simp: assms metric_space_ow_def metric_space_ow_axioms_def class.metric_space_axioms_def dist_triangle2)

subsection ‹\<^const>‹nhds››

definition nhds_ow where ‹nhds_ow U open a = (INF S∈{S. S ⊆ U ∧ open S ∧ a ∈ S}. principal S) ⊓ principal U›
  for U "open"

lemma nhds_ow_parametric[transfer_rule]:
  includes lifting_syntax
  assumes [transfer_rule]: ‹bi_unique A›
  shows ‹(rel_set A ===> (rel_set A ===> (=)) ===> A ===> rel_filter A) 
     nhds_ow nhds_ow›
  unfolding nhds_ow_def[folded transfer_bounded_filter_Inf_def] make_parametricity_proof_friendly
  by transfer_prover

lemma topological_space_nhds_ud[unoverload_def]: ‹topological_space.nhds = nhds_ow UNIV›
  by (auto intro!: ext simp add: nhds_ow_def [[axiom topological_space.nhds_def_raw]])

lemma nhds_ud[unoverload_def]: ‹nhds = nhds_ow UNIV open›
  by (auto intro!: ext simp add: nhds_ow_def nhds_def)

lemma nhds_ow_topology[simp]: ‹nhds_ow (topspace T) (openin T) x = nhdsin T x› if ‹x ∈ topspace T›
  using that apply (auto intro!: ext simp add: nhds_ow_def nhdsin_def[abs_def])
   apply (subst INF_inf_const2[symmetric])
  using openin_subset by (auto intro!: INF_cong)

subsection ‹\<^const>‹at_within››

definition ‹at_within_ow U open a s = nhds_ow U open a ⊓ principal (s - {a})›
  for U "open" a s

lemma at_within_ow_parametric[transfer_rule]:
  includes lifting_syntax
  assumes [transfer_rule]: ‹bi_unique T›
  shows ‹((rel_set T) ===> (rel_set T ===> (=)) ===> T ===> rel_set T ===> rel_filter T)
            at_within_ow at_within_ow›
  unfolding at_within_ow_def make_parametricity_proof_friendly transfer_inf_principal_def[symmetric]
  by transfer_prover

lemma at_within_ud[unoverload_def]: ‹at_within = at_within_ow UNIV open›
  by (auto intro!: ext simp: at_within_def at_within_ow_def unoverload_def)

lemma at_within_ow_topology:
  ‹at_within_ow (topspace T) (openin T) a S = nhdsin T a ⊓ principal (S - {a})› 
  if ‹a ∈ topspace T›
  using that unfolding at_within_ow_def by (simp add: nhds_ow_topology)


subsection ‹\<^const>‹has_sum››

definition ‹has_sum_ow U plus zero open f A x =
        filterlim (sum_ow zero plus f) (nhds_ow U (λS. open S) x)
         (finite_subsets_at_top A)›
  for U plus zero "open" f A x

lemma has_sum_ow_parametric[transfer_rule]:
  includes lifting_syntax
  assumes [transfer_rule]: ‹bi_unique T› ‹bi_unique U›
  shows ‹(rel_set T ===> (V ===> T ===> T) ===> T ===> (rel_set T ===> (=)) ===> (U ===> V) ===> rel_set U ===> T ===> (=))
            has_sum_ow has_sum_ow›
  unfolding has_sum_ow_def
  by transfer_prover

lemma has_sum_ud[unoverload_def]: ‹HAS_SUM = has_sum_ow UNIV plus (0::'a::{comm_monoid_add,topological_space}) open›
  by (auto intro!: ext simp: has_sum_def has_sum_ow_def unoverload_def)

lemma has_sum_ow_topology:
  assumes ‹l ∈ topspace T›
  assumes ‹0 ∈ topspace T›
  assumes ‹⋀x y. x ∈ topspace T ⟹ y ∈ topspace T ⟹ x + y ∈ topspace T›
  shows ‹has_sum_ow (topspace T) (+) 0 (openin T) f S l ⟷ has_sum_in T f S l›
  using assms apply (simp add: has_sum_ow_def has_sum_in_def nhds_ow_topology sum_ud[symmetric])
  by (metis filterlim_nhdsin_iff_limitin)

subsection ‹\<^const>‹filterlim››

subsection ‹\<^const>‹convergent››

definition convergent_ow where
  ‹convergent_ow U open X ⟷ (∃L∈U. filterlim X (nhds_ow U open L) sequentially)›
for U "open"

lemma convergent_ow_parametric[transfer_rule]:
  includes lifting_syntax
  assumes [transfer_rule]: ‹bi_unique T›
  shows ‹(rel_set T ===> (rel_set T ===> (=)) ===> ((=) ===> T) ===> (⟷))
           convergent_ow convergent_ow›
  unfolding convergent_ow_def
  by transfer_prover

lemma convergent_ud[unoverload_def]: ‹convergent = convergent_ow UNIV open›
  by (auto simp: convergent_ow_def[abs_def] convergent_def[abs_def] unoverload_def)

lemma topological_space_convergent_ud[unoverload_def]: ‹topological_space.convergent = convergent_ow UNIV›
  by (auto intro!: ext simp: [[axiom topological_space.convergent_def_raw]]
      convergent_ow_def unoverload_def)

lemma convergent_ow_topology[simp]:
  ‹convergent_ow (topspace T) (openin T) f ⟷ (∃l. limitin T f l sequentially)›
  by (auto simp: convergent_ow_def simp flip: filterlim_nhdsin_iff_limitin)

lemma convergent_ow_typeclass[simp]:
  ‹convergent_ow V (openin (top_of_set V)) f ⟷ (∃l. limitin (top_of_set V) f l sequentially)›
  by (simp flip: convergent_ow_topology)

subsection ‹\<^const>‹uniform_space.cauchy_filter››

lemma cauchy_filter_parametric[transfer_rule]:
  includes lifting_syntax
  assumes [transfer_rule]: "bi_unique T"
  shows "(rel_filter (rel_prod T T) ===> rel_filter T ===> (=)) 
    uniform_space.cauchy_filter
    uniform_space.cauchy_filter"
  unfolding [[axiom uniform_space.cauchy_filter_def_raw]]
  by transfer_prover

subsection ‹\<^const>‹uniform_space.Cauchy››

lemma uniform_space_Cauchy_parametric[transfer_rule]:
  includes lifting_syntax
  assumes [transfer_rule]: "bi_unique T"
  shows "(rel_filter (rel_prod T T) ===> ((=) ===> T) ===> (=)) 
    uniform_space.Cauchy
    uniform_space.Cauchy"
  unfolding [[axiom uniform_space.Cauchy_uniform_raw]]
  using filtermap_parametric[transfer_rule] apply fail?
  by transfer_prover

subsection ‹\<^class>‹complete_space››

locale complete_space_ow = metric_space_ow U dist uniformity "open"
  for U dist uniformity "open" +
  assumes ‹range X ⊆ U ⟶ uniform_space.Cauchy uniformity X ⟶ convergent_ow U open X›

lemma class_complete_space_ud[unoverload_def]: ‹class.complete_space = complete_space_ow UNIV›
  by (auto intro!: ext simp: class.complete_space_def class.complete_space_axioms_def complete_space_ow_def complete_space_ow_axioms_def unoverload_def)

lemma complete_space_ow_parametric[transfer_rule]:
  includes lifting_syntax
  assumes [transfer_rule]: "bi_unique T"
  shows "(rel_set T ===> (T ===> T ===> (=)) ===> rel_filter (rel_prod T T) ===> (rel_set T ===> (=)) ===> (=)) 
    complete_space_ow complete_space_ow"
  unfolding complete_space_ow_def complete_space_ow_axioms_def make_parametricity_proof_friendly
  by transfer_prover

lemma complete_space_ow_typeclass[simp]:
  fixes V :: ‹_::uniform_space set›
  assumes ‹complete V›
  shows ‹complete_space_ow V dist (uniformity_on V) (openin (top_of_set V))›
proof (rule complete_space_ow.intro)
  show ‹metric_space_ow V dist (uniformity_on V) (openin (top_of_set V))›
    apply (rule metric_space_ow_typeclass)
    by (simp add: assms complete_imp_closed)
  have ‹∃l. limitin (top_of_set V) X l sequentially›
    if XV: ‹⋀n. X n ∈ V› and cauchy: ‹uniform_space.Cauchy (uniformity_on V) X› for X
  proof -
    from cauchy
    have ‹uniform_space.cauchy_filter (uniformity_on V) (filtermap X sequentially)›
      by (simp add: [[axiom uniform_space.Cauchy_uniform_raw]])
    then have ‹cauchy_filter (filtermap X sequentially)›
      by (auto simp: cauchy_filter_def [[axiom uniform_space.cauchy_filter_def_raw]])
    then have ‹Cauchy X›
      by (simp add: Cauchy_uniform)
    with ‹complete V› XV obtain l where l: ‹X ⇢ l› ‹l ∈ V›
      apply atomize_elim
      by (meson completeE)
    with XV l show ?thesis
      by (auto intro!: exI[of _ l] simp: convergent_def limitin_subtopology)
  qed
  then show ‹complete_space_ow_axioms V (uniformity_on V) (openin (top_of_set V))›
    apply (auto simp: complete_space_ow_axioms_def complete_imp_closed assms)
    by blast
qed

subsection ‹\<^class>‹chilbert_space››

locale chilbert_space_ow = complex_inner_ow + complete_space_ow

lemma chilbert_space_ow_parametric[transfer_rule]:
  includes lifting_syntax
  assumes [transfer_rule]: ‹bi_unique A›
  shows ‹(rel_set A ===> ((=) ===> A ===> A) ===> ((=) ===> A ===> A) ===> (A ===> A ===> A) ===>
     A ===> (A ===> A ===> A) ===> (A ===> A) ===> (A ===> A ===> (=)) ===> (A ===> (=)) ===>
     (A ===> A) ===> rel_filter (rel_prod A A) ===> (rel_set A ===> (=)) ===> (A ===> A ===> (=)) ===> (=))
     chilbert_space_ow chilbert_space_ow›
  unfolding chilbert_space_ow_def make_parametricity_proof_friendly
  by transfer_prover

lemma chilbert_space_on_typeclass[simp]:
  fixes V :: ‹_::complex_inner set›
  assumes ‹complete V› ‹csubspace V›
  shows ‹chilbert_space_ow V (*⇩R) (*⇩C) (+) 0 (-) uminus dist norm sgn
     (uniformity_on V) (openin (top_of_set V)) (∙⇩C)›
  by (auto intro!: chilbert_space_ow.intro complex_inner_ow_typeclass
      simp: assms complete_imp_closed)

lemma class_chilbert_space_ud[unoverload_def]:
  ‹class.chilbert_space = chilbert_space_ow UNIV›
  by (auto intro!: ext simp add: class.chilbert_space_def chilbert_space_ow_def unoverload_def)

subsection ‹\<^const>‹hull››

definition ‹hull_ow A S s = ((λx. S x ∧ x ⊆ A) hull s) ∩ A›

lemma hull_ow_nondegenerate: ‹hull_ow A S s = ((λx. S x ∧ x ⊆ A) hull s)› if ‹x ⊆ A› and ‹s ⊆ x› and ‹S x›
proof -
  have ‹((λx. S x ∧ x ⊆ A) hull s) ⊆ x›
    apply (rule hull_minimal)
    using that by auto
  also note ‹x ⊆ A›
  finally show ?thesis
    unfolding hull_ow_def by auto
qed

definition ‹transfer_bounded_Inf B M = Inf M ⊓ B›

lemma transfer_bounded_Inf_parametric[transfer_rule]:
  includes lifting_syntax
  assumes ‹bi_unique T›
  shows ‹(rel_set T ===> rel_set (rel_set T) ===> rel_set T) transfer_bounded_Inf transfer_bounded_Inf›
  apply (auto intro!: rel_funI simp: transfer_bounded_Inf_def rel_set_def Bex_def)
  apply (metis (full_types) assms bi_uniqueDr)
  by (metis (full_types) assms bi_uniqueDl)

lemma hull_ow_parametric[transfer_rule]:
  includes lifting_syntax
  assumes [transfer_rule]: "bi_unique T"
  shows "(rel_set T ===> (rel_set T ===> (=)) ===> rel_set T ===> rel_set T) 
    hull_ow hull_ow"
proof -
  have *: ‹hull_ow A S s = transfer_bounded_Inf A (Set.filter (λx. S x ∧ s ⊆ x) (Pow A))› for A S s
    by (auto simp add: hull_ow_def hull_def transfer_bounded_Inf_def)
  show ?thesis
    unfolding *
    by transfer_prover      
qed

lemma hull_ow_ud[unoverload_def]: ‹(hull) = hull_ow UNIV›
  unfolding hull_def hull_ow_def by auto

subsection ‹\<^const>‹csubspace››

definition
  ‹subspace_ow plus zero scale S = (zero ∈ S ∧ (∀x∈S. ∀y∈S. plus x y ∈ S) ∧ (∀c. ∀x∈S. scale c x ∈ S))›
  for plus zero scale S

lemma subspace_ow_parametric[transfer_rule]:
  includes lifting_syntax
  assumes [transfer_rule]: ‹bi_unique T›
  shows ‹((T ===> T ===> T) ===> T ===> ((=) ===> T ===> T) ===> rel_set T ===> (=))
           subspace_ow subspace_ow›
  unfolding subspace_ow_def
  by transfer_prover

lemma module_subspace_ud[unoverload_def]: ‹module.subspace = subspace_ow plus 0›
  by (auto intro!: ext simp: [[axiom module.subspace_def_raw]] subspace_ow_def)

lemma csubspace_ud[unoverload_def]: ‹csubspace = subspace_ow (+) 0 (*⇩C)›
  by (simp add: csubspace_raw_def module_subspace_ud)

subsection ‹\<^const>‹cspan››

definition 
  ‹span_ow U plus zero scale b = hull_ow U (subspace_ow plus zero scale) b›
  for U plus zero scale b

lemma span_ow_on_typeclass: 
  assumes ‹csubspace U›
  assumes ‹B ⊆ U›
  shows ‹span_ow U plus 0 scaleC B = cspan B›
proof -
  have ‹span_ow U plus 0 scaleC B = (λx. csubspace x ∧ x ⊆ U) hull B›
    using assms 
    by (auto simp add: span_ow_def hull_ow_nondegenerate[where x=U] csubspace_raw_def 
        simp flip: csubspace_ud)
  also have ‹(λx. csubspace x ∧ x ⊆ U) hull B = cspan B›
    apply (rule hull_unique)
    using assms(2) complex_vector.span_superset apply force
    by (simp_all add: assms complex_vector.span_minimal)
  finally show ?thesis
    by -
qed

lemma (in Modules.module) span_ud[unoverload_def]: ‹span = span_ow UNIV plus 0 scale›
  by (auto intro!: ext simp: span_def span_ow_def
      module_subspace_ud hull_ow_ud)

lemmas cspan_ud[unoverload_def] = complex_vector.span_ud

lemma span_ow_parametric[transfer_rule]:
  includes lifting_syntax
  assumes [transfer_rule]: ‹bi_unique T›
  shows ‹(rel_set T ===> (T ===> T ===> T) ===> T ===> ((=) ===> T ===> T) ===> rel_set T ===> rel_set T)
           span_ow span_ow›
  unfolding span_ow_def
  by transfer_prover

subsubsection ‹\<^const>‹islimpt››

definition ‹islimpt_ow U open x S ⟷ (∀T⊆U. x∈T ⟶ open T ⟶ (∃y∈S. y∈T ∧ y≠x))› for "open"

lemma islimpt_ow_parametric[transfer_rule]:
  includes lifting_syntax
  assumes [transfer_rule]: ‹bi_unique T›
  shows ‹(rel_set T ===> (rel_set T ===> (=)) ===> T ===> rel_set T ===> (⟷)) islimpt_ow islimpt_ow›
  unfolding islimpt_ow_def make_parametricity_proof_friendly
  by transfer_prover

definition ‹islimptin T x S ⟷ x ∈ topspace T ∧ (∀V. x ∈ V ⟶ openin T V ⟶ (∃y∈S. y ∈ V ∧ y ≠ x))›

lemma islimpt_ow_from_topology: ‹islimpt_ow (topspace T) (openin T) x S ⟷ islimptin T x S ∨ x ∉ topspace T›
  apply (cases ‹x ∈ topspace T›)
   apply (simp_all add: islimpt_ow_def islimptin_def Pow_def)
  by blast+

subsubsection ‹\<^const>‹closure››

definition ‹closure_ow U open S = S ∪ {x∈U. islimpt_ow U open x S}› for "open"

lemma closure_ow_with_typeclass[simp]: 
  ‹closure_ow X (openin (top_of_set X)) S = (X ∩ closure (X ∩ S)) ∪ S›
proof -
  have ‹closure_ow X (openin (top_of_set X)) S = (top_of_set X) closure_of S ∪ S›
    apply (simp add: closure_ow_def islimpt_ow_def closure_of_def)
    apply safe
     apply (meson PowI openin_imp_subset)
    by auto
  also have ‹… = (X ∩ closure (X ∩ S)) ∪ S›
    by (simp add: closure_of_subtopology)
  finally show ?thesis
    by -
qed

lemma closure_ow_parametric[transfer_rule]:
  includes lifting_syntax
  assumes [transfer_rule]: ‹bi_unique T›
  shows ‹(rel_set T ===> (rel_set T ===> (=)) ===> rel_set T ===> rel_set T) closure_ow closure_ow›
  unfolding closure_ow_def make_parametricity_proof_friendly
  by transfer_prover

lemma closure_ow_from_topology: ‹closure_ow (topspace T) (openin T) S = T closure_of S› if ‹S ⊆ topspace T›
  using that apply (auto simp: closure_ow_def islimpt_ow_from_topology in_closure_of)
  apply (meson in_closure_of islimptin_def)
  by (metis islimptin_def)

lemma closure_ud[unoverload_def]: ‹closure = closure_ow UNIV open›
  unfolding closure_def closure_ow_def islimpt_def islimpt_ow_def by auto

subsection ‹\<^const>‹continuous››

lemma continuous_on_ow_from_topology: ‹continuous_on_ow (topspace T) (topspace U) (openin T) (openin U) (topspace T) f ⟷ continuous_map T U f›
  if ‹f ` topspace T ⊆ topspace U›
  apply (simp add: continuous_on_ow_def continuous_map_def)
  apply safe
    apply (meson image_subset_iff that)
   apply (smt (verit) Collect_mono_iff Int_def inf_absorb1 mem_Collect_eq openin_subopen openin_subset vimage_eq)
  by blast

subsection ‹\<^const>‹is_onb››

definition
  ‹is_onb_ow U scaleC plus zero norm open cinner E ⟷ is_ortho_set_ow zero cinner E ∧ (∀b∈E. norm b = 1) ∧ 
    closure_ow U open (span_ow U plus zero scaleC E) = U›
  for U scaleC plus zero norm "open" cinner

lemma is_onb_ow_parametric[transfer_rule]:
  includes lifting_syntax
  assumes [transfer_rule]: ‹bi_unique A›
  shows ‹(rel_set A ===>
     ((=) ===> A ===> A) ===>
     (A ===> A ===> A) ===>
     A ===>
     (A ===> (=)) ===> (rel_set A ===> (=)) ===> (A ===> A ===> (=)) ===> rel_set A ===> (=))
     is_onb_ow is_onb_ow›
  unfolding is_onb_ow_def
  by transfer_prover

lemma is_onb_ud[unoverload_def]:
  ‹is_onb = is_onb_ow UNIV scaleC plus 0 norm open cinner›
  unfolding is_onb_def is_onb_ow_def
  apply (subst asm_rl[of ‹⋀E. ccspan E = ⊤ ⟷ closure (cspan E) = UNIV›, rule_format])
   apply (transfer, rule)
  unfolding unoverload_def
  apply transfer by auto


subsection ‹Transferring theorems›

lemma closure_of_eqI:
  fixes f g :: ‹'a ⇒ 'b› and T :: ‹'a topology› and U :: ‹'b topology›
  assumes hausdorff: ‹Hausdorff_space U›
  assumes f_eq_g: ‹⋀x. x ∈ S ⟹ f x = g x›
  assumes x: ‹x ∈ T closure_of S›
  assumes f: ‹continuous_map T U f› and g: ‹continuous_map T U g›
  shows ‹f x = g x›
proof -
  have ‹topspace T ≠ {}›
    by (metis assms(3) equals0D in_closure_of)
  have ‹topspace U ≠ {}›
    using ‹topspace T ≠ {}› assms(5) continuous_map_image_subset_topspace by blast

  {
    assume "∃(Rep :: 't ⇒ 'a) Abs. type_definition Rep Abs (topspace T)"
    then interpret T: local_typedef ‹topspace T› ‹TYPE('t)›
      by unfold_locales
    assume "∃(Rep :: 'u ⇒ 'b) Abs. type_definition Rep Abs (topspace U)"
    then interpret U: local_typedef ‹topspace U› ‹TYPE('u)›
      by unfold_locales

    note on_closure_eqI
    note this[unfolded unoverload_def]
    note this[unoverload_type 'b, unoverload_type 'a]
    note this[unfolded unoverload_def]
    note this[where 'a='t and 'b='u]
    note this[untransferred]
    note this[where f=f and g=g and S=‹S ∩ topspace T› and x=x and ?open="openin T" and opena=‹openin U›]
    note this[simplified]
  }
  note * = this[cancel_type_definition, OF ‹topspace T ≠ {}›, cancel_type_definition, OF ‹topspace U ≠ {}›]

  have 2: ‹f ` topspace T ⊆ topspace U›
  by (meson assms(4) continuous_map_image_subset_topspace)
  have 3: ‹g ` topspace T ⊆ topspace U›
    by (simp add: continuous_map_image_subset_topspace g)
  have 4: ‹x ∈ topspace T›
    by (meson assms(3) in_closure_of)
  have 5: ‹topological_space_ow (topspace T) (openin T)›
    by simp
  have 6: ‹t2_space_ow (topspace U) (openin U)›
    by (simp add: hausdorff)
  from x have ‹x ∈ T closure_of (S ∩ topspace T)›
    by (metis closure_of_restrict inf_commute)
  then have 7: ‹x ∈ closure_ow (topspace T) (openin T) (S ∩ topspace T)›
    by (simp add: closure_ow_from_topology)
  have 8: ‹continuous_on_ow (topspace T) (topspace U) (openin T) (openin U) (topspace T) f›
     by (meson "2" continuous_on_ow_from_topology f)
  have 9: ‹continuous_on_ow (topspace T) (topspace U) (openin T) (openin U) (topspace T) g›
    by (simp add: "3" continuous_on_ow_from_topology g)

  show ?thesis
    apply (rule * )
    using 2 3 4 5 6 f_eq_g 7 8 9 by auto
qed


lemma orthonormal_subspace_basis_exists:
  fixes S :: ‹'a::chilbert_space set›
  assumes ‹is_ortho_set S› and norm: ‹⋀x. x∈S ⟹ norm x = 1› and ‹S ⊆ space_as_set V›
  shows ‹∃B. B ⊇ S ∧ is_ortho_set B ∧ (∀x∈B. norm x = 1) ∧ ccspan B = V›
proof -
  {
    assume "∃(Rep :: 't ⇒ 'a) Abs. type_definition Rep Abs (space_as_set V)"
    then interpret T: local_typedef ‹space_as_set V› ‹TYPE('t)›
      by unfold_locales

    note orthonormal_basis_exists
    note this[unfolded unoverload_def]
    note this[unoverload_type 'a]
    note this[unfolded unoverload_def]
    note this[where 'a='t]
    note this[untransferred]
    note this[where plus=plus and scaleC=scaleC and scaleR=scaleR and zero=0 and minus=minus
        and uminus=uminus and sgn=sgn and S=S and norm=norm and cinner=cinner and dist=dist
        and ?open=‹openin (top_of_set (space_as_set V))›
        and uniformity=‹uniformity_on (space_as_set V)›]
    note this[simplified Domainp_rel_filter prod.Domainp_rel T.Domainp_cr_S]
  }    
  note * = this[cancel_type_definition]
  have 1: ‹uniformity_on (space_as_set V)
    ≤ principal (Collect (pred_prod (λx. x ∈ space_as_set V) (λx. x ∈ space_as_set V)))›
    by (auto simp: uniformity_dist intro!: le_infI2)
  have ‹∃B∈{A. ∀x∈A. x ∈ space_as_set V}.
     S ⊆ B ∧ is_onb_ow (space_as_set V) (*⇩C) (+) 0 norm (openin (top_of_set (space_as_set V))) (∙⇩C) B›
    apply (rule * )
    using ‹S ⊆ space_as_set V› ‹is_ortho_set S›
    by (auto simp flip: unoverload_def
        intro!: complex_vector.subspace_scale real_vector.subspace_scale csubspace_is_subspace
        csubspace_nonempty complex_vector.subspace_add complex_vector.subspace_diff
        complex_vector.subspace_neg sgn_in_spaceI 1 norm)

  then obtain B where ‹B ⊆ space_as_set V› and ‹S ⊆ B›
    and is_onb: ‹is_onb_ow (space_as_set V) (*⇩C) (+) 0 norm (openin (top_of_set (space_as_set V))) (∙⇩C) B›
    by auto

  from ‹B ⊆ space_as_set V›
  have [simp]: ‹cspan B ∩ space_as_set V = cspan B›
    by (smt (verit) basic_trans_rules(8) ccspan.rep_eq ccspan_leqI ccspan_superset complex_vector.span_span inf_absorb1 less_eq_ccsubspace.rep_eq)
  then have [simp]: ‹space_as_set V ∩ cspan B = cspan B›
    by blast
  from ‹B ⊆ space_as_set V›
  have [simp]: ‹space_as_set V ∩ closure (cspan B) = closure (cspan B)›
    by (metis Int_absorb1 ccspan.rep_eq ccspan_leqI less_eq_ccsubspace.rep_eq)
  have [simp]: ‹closure X ∪ X = closure X› for X :: ‹'z::topological_space set›
    using closure_subset by blast

  from is_onb have ‹is_ortho_set B›
    by (auto simp: is_onb_ow_def unoverload_def)

  moreover from is_onb have ‹norm x = 1› if ‹x ∈ B› for x
    by (auto simp: is_onb_ow_def that)

  moreover from is_onb have ‹closure (cspan B) = space_as_set V›
    by (simp add: is_onb_ow_def ‹B ⊆ space_as_set V›
        closure_ow_with_typeclass span_ow_on_typeclass flip: unoverload_def)
  then have ‹ccspan B = V›
    by (simp add: ccspan.abs_eq space_as_set_inverse)

  ultimately show ?thesis
    using ‹S ⊆ B› by auto
qed

lemma has_sum_in_comm_additive_general:
  fixes f :: ‹'a ⇒ 'b :: comm_monoid_add›
    and g :: ‹'b ⇒ 'c :: comm_monoid_add›
  assumes T0[simp]: ‹0 ∈ topspace T› and Tplus[simp]: ‹⋀x y. x ∈ topspace T ⟹ y ∈ topspace T ⟹ x+y ∈ topspace T›
  assumes Uplus[simp]: ‹⋀x y. x ∈ topspace U ⟹ y ∈ topspace U ⟹ x+y ∈ topspace U›
  assumes grange: ‹g ` topspace T ⊆ topspace U›
  assumes g0: ‹g 0 = 0›
  assumes frange: ‹f ` S ⊆ topspace T›
  assumes gcont: ‹filterlim g (nhdsin U (g l)) (atin T l)›
  assumes gadd: ‹⋀x y. x ∈ topspace T ⟹ y ∈ topspace T ⟹ g (x+y) = g x + g y›
  assumes sumf: ‹has_sum_in T f S l›
  shows ‹has_sum_in U (g o f) S (g l)›
proof -
  define f' where ‹f' x = (if x ∈ S then f x else 0)› for x
  have ‹topspace T ≠ {}›
    using T0 by blast
  then have ‹topspace U ≠ {}›
    using grange by blast
  {
    assume "∃(Rep :: 't ⇒ 'b) Abs. type_definition Rep Abs (topspace T)"
    then interpret T: local_typedef ‹topspace T› ‹TYPE('t)›
      by unfold_locales
    assume "∃(Rep :: 'u ⇒ 'c) Abs. type_definition Rep Abs (topspace U)"
    then interpret U: local_typedef ‹topspace U› ‹TYPE('u)›
      by unfold_locales

    note [[show_types]]
    note has_sum_comm_additive_general
    note this[unfolded unoverload_def]
    note this[unoverload_type 'b, unoverload_type 'c]
    note this[where 'b='t and 'c='u and 'a='a]
    note this[unfolded unoverload_def]
    thm this[no_vars]
    note this[untransferred]
    note this[where f=g and g=f' and zero=0 and zeroa=0 and plus=plus and plusa=plus
        and ?open=‹openin U› and opena=‹openin T› and x=l and S=S and T=‹topspace T›]
    note this[simplified]
  }
  note * = this[cancel_type_definition, OF ‹topspace T ≠ {}›, cancel_type_definition, OF ‹topspace U ≠ {}›]

  have f'T[simp]: ‹f' x ∈ topspace T› for x
    using frange f'_def by force
  have [simp]: ‹l ∈ topspace T›
    using sumf has_sum_in_topspace by blast
  have [simp]: ‹x ∈ topspace T ⟹ g x ∈ topspace U› for x
    using grange by auto
  have sumf'T: ‹(∑x∈F. f' x) ∈ topspace T› if ‹finite F› for F
    using that apply induction
    by auto
  have [simp]: ‹(∑x∈F. f x) ∈ topspace T› if ‹F ⊆ S› for F
    using that apply (induction F rule:infinite_finite_induct)
      apply auto
    by (metis Tplus f'T f'_def)
  have sum_gf: ‹(∑x∈F. g (f' x)) = g (∑x∈F. f' x)› 
    if ‹finite F› and ‹F ⊆ S› for F
  proof -
    have ‹(∑x∈F. g (f' x)) = (∑x∈F. g (f x))›
      apply (rule sum.cong)
      using frange that by (auto simp: f'_def)
    also have ‹… = g (∑x∈F. f x)›
      using ‹finite F› ‹F ⊆ S› apply induction
      using g0 frange apply auto
      apply (subst gadd)
      by (auto simp: f'_def)
    also have ‹… = g (∑x∈F. f' x)›
      apply (rule arg_cong[where f=g])
      apply (rule sum.cong)
      using that by (auto simp: f'_def)
    finally show ?thesis
      by -
  qed
  from sumf have sumf': ‹has_sum_in T f' S l›
    apply (rule has_sum_in_cong[THEN iffD2, rotated])
    unfolding f'_def by auto
  have [simp]: ‹g l ∈ topspace U›
    using grange by auto
  from gcont have contg': ‹filterlim g (nhdsin U (g l)) (nhdsin T l ⊓ principal (topspace T - {l}))›
    apply (rule filterlim_cong[THEN iffD1, rotated -1])
      apply (rule refl)
     apply (simp add: atin_def)
    by (auto intro!: exI simp add: eventually_atin)
  from T0 grange g0 have [simp]: ‹0 ∈ topspace U›
    by auto

  have [simp]: 
    ‹comm_monoid_ow (topspace T) (+) 0›
    ‹comm_monoid_ow (topspace U) (+) 0›
    by (simp_all add: comm_monoid_ow_def abel_semigroup_ow_def
        semigroup_ow_def plus_ow_def semigroup_ow_axioms_def
        comm_monoid_ow_axioms_def Groups.add_ac abel_semigroup_ow_axioms_def)

  have ‹has_sum_ow (topspace U) (+) 0 (openin U) (g ∘ f') S (g l)›
    apply (rule *)
    by (auto simp: topological_space_ow_from_topology sum_gf sumf'
        sum_ud[symmetric] at_within_ow_topology has_sum_ow_topology
        contg' sumf'T)

  then have ‹has_sum_in U (g ∘ f') S (g l)›
    apply (rule has_sum_ow_topology[THEN iffD1, rotated -1])
    by simp_all
  then have ‹has_sum_in U (g ∘ f') S (g l)›
    by simp
  then show ?thesis
    apply (rule has_sum_in_cong[THEN iffD1, rotated])
    unfolding f'_def using frange grange by auto
qed

lemma has_sum_in_comm_additive:
  fixes f :: ‹'a ⇒ 'b :: ab_group_add›
    and g :: ‹'b ⇒ 'c :: ab_group_add›
  assumes ‹topspace T = UNIV› and ‹topspace U = UNIV›
  assumes ‹Modules.additive g›
  assumes gcont: ‹continuous_map T U g›
  assumes sumf: ‹has_sum_in T f S l›
  shows ‹has_sum_in U (g o f) S (g l)›
  apply (rule has_sum_in_comm_additive_general[where T=T and U=U])
  using assms
  by (auto simp: additive.zero Modules.additive_def intro!: continuous_map_is_continuous_at_point)


section ‹Stuff relying on the above lifting›

(* TODO: Migrate this into Bounded_Operators session,
   and change "some_chilbert_basis" there to to abbreviate "some_onb_of UNIV" *)
definition ‹some_onb_of X = (SOME B. is_ortho_set B ∧ (∀b∈B. norm b = 1) ∧ ccspan B = X)›

lemma
  fixes X :: ‹'a::chilbert_space ccsubspace›
  shows some_onb_of_is_ortho_set[iff]: ‹is_ortho_set (some_onb_of X)›
    and some_onb_of_norm1: ‹b ∈ some_onb_of X ⟹ norm b = 1›
    and some_onb_of_ccspan[simp]: ‹ccspan (some_onb_of X) = X›
proof -
  let ?P = ‹λB. is_ortho_set B ∧ (∀b∈B. norm b = 1) ∧ ccspan B = X›
  have ‹Ex ?P›
    using orthonormal_subspace_basis_exists[where S=‹{}› and V=X]
    by auto
  then have ‹?P (some_onb_of X)›
    by (simp add: some_onb_of_def verit_sko_ex)
  then show is_ortho_set_some_onb_of: ‹is_ortho_set (some_onb_of X)›
    and ‹b ∈ some_onb_of X ⟹ norm b = 1›
    and ‹ccspan (some_onb_of X) = X›
    by auto
qed

lemma ccsubspace_as_whole_type:
  fixes X :: ‹'a::chilbert_space ccsubspace›
  assumes ‹X ≠ 0›
  shows ‹let 'b::type = some_onb_of X in
         ∃U::'b ell2 ⇒⇩C⇩L 'a. isometry U ∧ U *⇩S ⊤ = X›
proof with_type_intro
  show ‹some_onb_of X ≠ {}›
    using some_onb_of_ccspan[of X] assms
    by (auto simp del: some_onb_of_ccspan)
  fix Rep :: ‹'b ⇒ 'a› and Abs
  assume ‹bij_betw Rep UNIV (some_onb_of X)›
  then interpret type_definition Rep ‹inv Rep› ‹some_onb_of X›
    by (simp add: type_definition_bij_betw_iff)
  define U where ‹U = cblinfun_extension (range ket) (Rep o inv ket)›
  have [simp]: ‹Rep i ∙⇩C Rep j = 0› if ‹i ≠ j› for i j
    using Rep some_onb_of_is_ortho_set[unfolded is_ortho_set_def] that
    by (smt (verit) Rep_inverse)
  moreover have [simp]: ‹norm (Rep i) = 1› for i
    using Rep[of i] some_onb_of_norm1
    by auto
  ultimately have ‹cblinfun_extension_exists (range ket) (Rep o inv ket)›
    apply (rule_tac cblinfun_extension_exists_ortho)
    by auto
  then have U_ket[simp]: ‹U (ket i) = Rep i› for i
    by (auto simp: cblinfun_extension_apply U_def)
  have ‹isometry U›
    apply (rule orthogonal_on_basis_is_isometry[where B=‹range ket›])
    by (auto simp: cinner_ket simp flip: cnorm_eq_1)
  moreover have ‹U *⇩S ccspan (range ket) = X›
    apply (subst cblinfun_image_ccspan)
    by (simp add: Rep_range image_image)
  ultimately show ‹∃U :: 'b ell2 ⇒⇩C⇩L 'a. isometry U ∧ U *⇩S ⊤ = X›
    by auto
qed

lemma some_onb_of_0[simp]: ‹some_onb_of (0 :: 'a::chilbert_space ccsubspace) = {}›
proof -
  have no0: ‹0 ∉ some_onb_of (0 :: 'a ccsubspace)›
    using some_onb_of_norm1
    by fastforce
  have ‹ccspan (some_onb_of 0) = (0 :: 'a ccsubspace)›
    by simp
  then have ‹some_onb_of 0 ⊆ space_as_set (0 :: 'a ccsubspace)›
    by (metis ccspan_superset)
  also have ‹… = {0}›
    by simp
  finally show ?thesis
    using no0
    by blast
qed

lemma some_onb_of_finite_dim:
  fixes S :: ‹'a::chilbert_space ccsubspace›
  assumes ‹finite_dim_ccsubspace S›
  shows ‹finite (some_onb_of S)›
proof -
  from assms obtain C where CS: ‹cspan C = space_as_set S› and ‹finite C›
    by (meson cfinite_dim_subspace_has_basis csubspace_space_as_set finite_dim_ccsubspace.rep_eq)
  then show ‹finite (some_onb_of S)›
    using ccspan_superset complex_vector.independent_span_bound is_ortho_set_cindependent by fastforce
qed

lemma some_onb_of_in_space[iff]:
  fixes S :: ‹'a::chilbert_space ccsubspace›
  shows ‹some_onb_of S ⊆ space_as_set S›
  using ccspan_superset by fastforce



lemma sum_some_onb_of_butterfly:
  fixes S :: ‹'a::chilbert_space ccsubspace›
  assumes ‹finite_dim_ccsubspace S›
  shows ‹(∑x∈some_onb_of S. butterfly x x) = Proj S›
proof -
  obtain B where onb_S_in_B: ‹some_onb_of S ⊆ B› and ‹is_onb B›
    apply atomize_elim
    apply (rule orthonormal_basis_exists)
    by (simp_all add: some_onb_of_norm1)
  have S_ccspan: ‹S = ccspan (some_onb_of S)›
    by simp

  show ?thesis
  proof (rule cblinfun_eq_gen_eqI[where G=B])
    show ‹ccspan B = ⊤›
      using ‹is_onb B› is_onb_def by blast
    fix b assume ‹b ∈ B›
    show ‹(∑x∈some_onb_of S. selfbutter x) *⇩V b = Proj S *⇩V b›
    proof (cases ‹b ∈ some_onb_of S›)
      case True
      have ‹(∑x∈some_onb_of S. selfbutter x) *⇩V b = (∑x∈some_onb_of S. selfbutter x *⇩V b)›
        using cblinfun.sum_left by blast
      also have ‹… = b›
        apply (subst sum_single[where i=b])
        using True apply (auto intro!: simp add: assms some_onb_of_finite_dim) 
        using is_ortho_set_def apply fastforce
        using cnorm_eq_1 some_onb_of_norm1 by force
      also have ‹… = Proj S *⇩V b›
        apply (rule Proj_fixes_image[symmetric])
        using True some_onb_of_in_space by blast
      finally show ?thesis
        by -
    next
      case False
      have *: ‹is_orthogonal x b› if ‹x ∈ some_onb_of S› and ‹x ≠ 0› for x
      proof -
        have ‹x ∈ B›
          using onb_S_in_B that(1) by fastforce
        moreover note ‹b ∈ B›
        moreover have ‹x ≠ b›
          using False that(1) by blast
        moreover note ‹is_onb B›
        ultimately show ‹is_orthogonal x b›
          by (simp add: is_onb_def is_ortho_set_def)
      qed
      have ‹(∑x∈some_onb_of S. selfbutter x) *⇩V b = (∑x∈some_onb_of S. selfbutter x *⇩V b)›
        using cblinfun.sum_left by blast
      also have ‹… = 0›
        by (auto intro!: sum.neutral simp: * )
      also have ‹… = Proj S *⇩V b›
        apply (rule Proj_0_compl[symmetric])
        apply (subst S_ccspan)
        apply (rule mem_ortho_ccspanI)
        using "*" cinner_zero_right is_orthogonal_sym by blast
      finally show ?thesis 
        by -
    qed
  qed
qed


lemma cdim_infinite_0:
  assumes ‹¬ cfinite_dim S›
  shows ‹cdim S = 0›
proof -
  from assms have not_fin_cspan: ‹¬ cfinite_dim (cspan S)›
    using cfinite_dim_def cfinite_dim_subspace_has_basis complex_vector.span_superset by fastforce
  obtain B where ‹cindependent B› and ‹cspan S = cspan B›
    using csubspace_has_basis by blast
  with not_fin_cspan have ‹infinite B›
    by auto
  then have ‹card B = 0›
    by force
  have ‹cdim (cspan S) = 0› 
    apply (rule complex_vector.dim_unique[of B])
       apply (auto intro!: simp add: ‹cspan S = cspan B› complex_vector.span_superset)
    using ‹cindependent B› ‹card B = 0› by auto
  then show ?thesis
    by simp
qed


lemma some_onb_of_card:
  fixes S :: ‹'a::chilbert_space ccsubspace›
  shows ‹card (some_onb_of S) = cdim (space_as_set S)›
proof (cases ‹finite_dim_ccsubspace S›)
  case True
  show ?thesis
    apply (rule complex_vector.dim_eq_card[symmetric])
     apply (auto simp: is_ortho_set_cindependent)
     apply (metis True ccspan_finite some_onb_of_ccspan complex_vector.span_clauses(1) some_onb_of_finite_dim)
    by (metis True ccspan_finite some_onb_of_ccspan complex_vector.span_eq_iff csubspace_space_as_set some_onb_of_finite_dim)
next
  case False
  then have ‹cdim (space_as_set S) = 0›
    by (simp add: cdim_infinite_0 finite_dim_ccsubspace.rep_eq)
  moreover from False have ‹infinite (some_onb_of S)›
    using ccspan_finite_dim by fastforce
  ultimately show ?thesis 
    by simp
qed

unbundle no lattice_syntax and no cblinfun_syntax

end