Theory Example_Euclidean_Space

section ‹‹Example_Euclidean_Space› -- Example: compactness of the sphere›

theory Example_Euclidean_Space
  imports With_Type "HOL-Analysis.Euclidean_Space" "HOL-Analysis.Topology_Euclidean_Space"
begin

subsection ‹Setting up type class \<^class>‹finite› for \<^const>‹with_type››

definition ‹WITH_TYPE_CLASS_finite S u ⟷ finite S›
  for S :: ‹'rep set› and u :: unit
definition ‹WITH_TYPE_REL_finite r = (rel_unit_itself :: _ ⇒ 'abs itself ⇒ _)›
  for r :: ‹'rep ⇒ 'abs ⇒ bool›

lemma [with_type_intros]: ‹finite S ⟹ WITH_TYPE_CLASS_finite S x›
  using WITH_TYPE_CLASS_finite_def by blast

lemma with_type_wellformed_finite[with_type_intros]:
  ‹with_type_wellformed WITH_TYPE_CLASS_finite S WITH_TYPE_REL_finite›
  by (simp add: with_type_wellformed_def WITH_TYPE_REL_finite_def)

lemma with_type_transfer_finite:
  includes lifting_syntax
  fixes r :: ‹'rep ⇒ 'abs ⇒ bool›
  assumes [transfer_rule]: ‹bi_unique r› ‹right_total r›
  shows ‹(WITH_TYPE_REL_finite r ===> (⟷))
         (WITH_TYPE_CLASS_finite (Collect (Domainp r))) class.finite›
  unfolding WITH_TYPE_REL_finite_def
proof (rule rel_funI)
  fix x :: unit and y :: ‹'abs itself›
  assume ‹rel_unit_itself x y›
  then have [simp]: ‹y = TYPE('abs)›
    by simp
  note right_total_UNIV_transfer[transfer_rule]
  show ‹WITH_TYPE_CLASS_finite (Collect (Domainp r)) x ⟷ class.finite y›
    apply (simp add: WITH_TYPE_CLASS_finite_def class.finite_def)
    apply transfer
    by simp
qed

setup ‹
With_Type.add_with_type_info_global {
  class = \<^class>‹finite›,
  param_names = [],
  rep_class = \<^const_name>‹WITH_TYPE_CLASS_finite›,
  rep_rel = \<^const_name>‹WITH_TYPE_REL_finite›,
  with_type_wellformed = @{thm with_type_wellformed_finite},
  transfer = SOME @{thm with_type_transfer_finite},
  rep_rel_itself = SOME @{lemma ‹bi_unique r ⟹ right_total r ⟹ (WITH_TYPE_REL_finite r) p TYPE('abs2)›
      by (simp add: WITH_TYPE_REL_finite_def rel_unit_itself.simps Transfer.Rel_def)}
}
›

subsection ‹Vector space over a given basis›

text ‹‹'a vs_over› is defined to be the vector space with an orthonormal basis enumerated by
  elements of \<^typ>‹'a›, in other words $\mathbb R^\mathtt{'a}$. We require \<^typ>‹'a› to be finite.›
typedef 'a vs_over = ‹UNIV :: ('a::finite⇒real) set›
  by (rule exI[of _ ‹λ_. 0›], auto)
setup_lifting type_definition_vs_over


instantiation vs_over :: (finite) real_vector begin
lift_definition plus_vs_over :: ‹'a vs_over ⇒ 'a vs_over ⇒ 'a vs_over› is ‹λx y a. x a + y a›.
lift_definition minus_vs_over :: ‹'a vs_over ⇒ 'a vs_over ⇒ 'a vs_over› is ‹λx y a. x a - y a›.
lift_definition uminus_vs_over :: ‹'a vs_over ⇒ 'a vs_over› is ‹λx a. - x a›.
lift_definition zero_vs_over :: ‹'a vs_over› is ‹λ_. 0›.
lift_definition scaleR_vs_over :: ‹real ⇒ 'a vs_over ⇒ 'a vs_over› is ‹λr x a. r * x a›.
instance
  apply (intro_classes; transfer)
  by (auto intro!: ext simp: distrib_right distrib_left)
end

instantiation vs_over :: (finite) real_normed_vector begin
lift_definition norm_vs_over :: ‹'a vs_over ⇒ real› is ‹λx. L2_set x UNIV›.
definition dist_vs_over :: ‹'a vs_over ⇒ 'a vs_over ⇒ real› where ‹dist_vs_over x y = norm (x - y)›
definition uniformity_vs_over :: ‹('a vs_over × 'a vs_over) filter› where ‹uniformity_vs_over = (INF e∈{0<..}. principal {(x, y). dist x y < e})›
definition sgn_vs_over :: ‹'a vs_over ⇒ 'a vs_over› where ‹sgn_vs_over x = x /⇩R norm x›
definition open_vs_over :: ‹'a vs_over set ⇒ bool› where ‹open_vs_over U = (∀x∈U. ∀⇩F (x', y) in uniformity. x' = x ⟶ y ∈ U)›
instance
proof intro_classes
  fix x y :: ‹'a vs_over›
  show ‹dist x y = norm (x - y)›
  using dist_vs_over_def by presburger
  show ‹sgn x = x /⇩R norm x›
  using sgn_vs_over_def by blast
  show ‹(uniformity :: ('a vs_over × 'a vs_over) filter) = (INF e∈{0<..}. principal {(x, y). dist x y < e})›
  using uniformity_vs_over_def by blast
  show ‹(norm x = 0) = (x = 0)›
    apply transfer
    by (auto simp: L2_set_eq_0_iff)
  show ‹norm (x + y) ≤ norm x + norm y›
    apply transfer
    by (rule L2_set_triangle_ineq)
  show ‹norm (a *⇩R x) = ¦a¦ * norm x› for a
    apply transfer
    by (simp add: L2_set_def power_mult_distrib real_sqrt_mult flip: sum_distrib_left)
  show ‹open U = (∀x∈U. ∀⇩F (x', y) in uniformity. x' = x ⟶ y ∈ U)› for U :: ‹'a vs_over set›
    by (simp add: open_vs_over_def)
qed
end

instantiation vs_over :: (finite) real_inner begin
lift_definition inner_vs_over :: ‹'a vs_over ⇒ 'a vs_over ⇒ real› is ‹λx y. ∑a∈UNIV. x a * y a›.
instance
  apply (intro_classes; transfer)
  by (auto intro!: sum_nonneg sum.cong simp: mult.commute sum_nonneg_eq_0_iff L2_set_def
      power2_eq_square sum_distrib_left mult_ac distrib_left simp flip: sum.distrib)
end

instantiation vs_over :: (finite) euclidean_space begin
text ‹Returns the basis vector corresponding to \<^typ>‹'a›.›
lift_definition basis_vec :: ‹'a ⇒ 'a vs_over› is ‹λa::'a. indicator {a}›.
definition Basis_vs_over :: ‹'a vs_over set› where ‹Basis = range basis_vec›
instance
  apply (intro_classes; unfold Basis_vs_over_def; transfer)
  by (auto intro!: simp: indicator_def)
end


subsection ‹Compactness of the sphere.›

text ‹@{thm compact_sphere} shows that a sphere in an Euclidean vector space
  (type class \<^class>‹euclidean_space›) is compact. We wish to transfer this result to
  any space with a finite orthonormal basis. Mathematically, this is the same statement,
  but the conversion between a statement based on type classes and one based on predicates
  about bases is non-trivial in Isabelle.›

lemma compact_sphere_onb:
  fixes B :: ‹'a::real_inner set›
  assumes ‹finite B› and ‹span B = UNIV› and onb: ‹∀b∈B. ∀c∈B. inner b c = of_bool (b=c)›
  shows ‹compact (sphere (0::'a) r)›
proof (cases ‹B = {}›)
  case True
  with assms have all_0: ‹(x :: 'a) = 0› for x
    by auto
  then have ‹sphere (0::'a) r = {0} ∨ sphere (0::'a) r = {}›
    by (auto simp add: sphere_def)
  then show ?thesis
    by fastforce
next
  case False
  have ‹let 't::finite = B in compact (sphere (0::'t vs_over) r)›
  proof with_type_intro
    from False show ‹B ≠ {}› by -
    from assms show ‹finite B› by -
    fix rep :: ‹'t ⇒ _›
    assume ‹bij_betw rep UNIV B›
    from compact_sphere[where 'a=‹'t vs_over›]
    show ‹compact (sphere (0::'t vs_over) r)›
      by simp
  qed
  then have ‹let 't::finite = B in compact (sphere (0::'a) r)›
  proof with_type_mp
    with_type_case

    define f :: ‹'t vs_over ⇒ 'a› where ‹f x = (∑t∈UNIV. Rep_vs_over x t *⇩R rep_t t)› for x
    have ‹linear f›
      by (auto intro!: linearI sum.distrib simp: f_def plus_vs_over.rep_eq scaleR_vs_over.rep_eq
          scaleR_add_left scaleR_right.sum simp flip: scaleR_scaleR)
    then have ‹continuous_on X f› for X
      using linear_continuous_on linear_linear by blast
    moreover from with_type_mp.premise have ‹compact (sphere (0::'t vs_over) r)›
      by -
    ultimately have compact_fsphere: ‹compact (f ` sphere 0 r)›
      using compact_continuous_image by blast
    have ‹surj f›
    proof (unfold surj_def, rule allI)
      fix y :: 'a
      from assms have ‹y ∈ span B›
        by auto
      then show ‹∃x. y = f x›
      proof (induction rule: span_induct_alt)
        case base
        then show ?case
          by (auto intro!: exI[of _ 0] simp: f_def zero_vs_over.rep_eq)
      next
        case (step c b y)
        from step.IH
        obtain x where yfx: ‹y = f x›
          by auto
        have ‹b = f (basis_vec (inv rep_t b))›
          by (simp add: f_def basis_vec.rep_eq step.hyps type_definition_t.Abs_inverse)
        then have ‹c *⇩R b + y = f (c *⇩R basis_vec (inv rep_t b) + x)›
          using ‹linear f›
          by (simp add: linear_add linear_scale yfx)
        then show ?case
          by auto
      qed
    qed
    have ‹norm (f x) = norm x› for x
    proof -
      have aux1: ‹(a, b) ∉ range (λt. (t, t)) ⟹ rep_t a ∙ rep_t b ≠ 0 ⟹ Rep_vs_over x b = 0› for a b
        by (metis (mono_tags, lifting) of_bool_eq(1) onb range_eqI type_definition_t.Rep type_definition_t.Rep_inverse)
      have rep_inner: ‹inner (rep_t t) (rep_t u) = of_bool (t=u)› for t u
        by (simp add: onb type_definition_t.Rep type_definition_t.Rep_inject)
      have ‹(norm (f x))⇧2 = inner (f x) (f x)›
        by (simp add: dot_square_norm)
      also have ‹… = (∑(t,t')∈UNIV. (Rep_vs_over x t * Rep_vs_over x t') * inner (rep_t t) (rep_t t'))›
        by (auto intro!: simp: f_def inner_sum_right inner_sum_left sum_distrib_left sum.cartesian_product
            case_prod_beta inner_commute mult_ac)
      also have ‹… = (∑(t,t')∈(λt. (t,t))`UNIV. (Rep_vs_over x t * Rep_vs_over x t') * inner (rep_t t) (rep_t t'))›
        by (auto intro!: sum.mono_neutral_cong_right simp: aux1)
      also have ‹… = (∑t∈UNIV. (Rep_vs_over x t)⇧2)›
        apply (subst sum.reindex)
        by (auto intro!: injI simp: rep_inner power2_eq_square)
      also have ‹… = (norm x)⇧2›
        by (simp add: norm_vs_over_def L2_set_def sum_nonneg)
      finally show ?thesis
        by simp
    qed
    then have ‹f ` sphere 0 r = sphere 0 r›
      using ‹surj f›
      by (fastforce simp: sphere_def)
    with compact_fsphere
    show ‹compact (sphere (0::'a) r)›
      by simp
  qed
  from this[cancel_with_type]
  show ‹compact (sphere (0::'a) r)›
    by -
qed

end