Theory RS_Formal_Power_Series

(***********************************************************************************
 * Copyright (c) 2025 Université Paris-Saclay
 *
 * Author: Benoît Ballenghien, Université Paris-Saclay,
           CNRS, ENS Paris-Saclay, LMF
 * Author: Benjamin Puyobro, Université Paris-Saclay,
           IRT SystemX, CNRS, ENS Paris-Saclay, LMF
 * Author: Burkhart Wolff, Université Paris-Saclay,
           CNRS, ENS Paris-Saclay, LMF
 *
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are met:
 *
 * * Redistributions of source code must retain the above copyright notice, this
 *
 * * Redistributions in binary form must reproduce the above copyright notice,
 *   this list of conditions and the following disclaimer in the documentation
 *   and/or other materials provided with the distribution.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
 * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
 * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
 * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
 * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
 * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
 * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 *
 * SPDX-License-Identifier: BSD-2-Clause
 ***********************************************************************************)


section ‹Formal power Series›

(*<*)
theory RS_Formal_Power_Series
  imports Restriction_Spaces "HOL-Analysis.FPS_Convergence"
begin
  (*>*)

instantiation fps ::("{comm_ring_1}") restriction_space begin
definition restriction_fps :: "'a fps ⇒ nat ⇒ 'a fps"  
  where ‹restriction_fps a n ≡ ∑i<n. fps_const (fps_nth a i)*fps_X^i›

lemma intersection_equality:‹(n::nat) ≤ m ⟹ {..<m} ∩ {i. i < n} = {i. i<n}›
  by auto

lemma exist_noneq:‹x ≠ y ⟹
           ∃n. (∑i∈{x. x < n}. fps_const (fps_nth x i) * fps_X ^ i) ≠
               (∑i∈{x. x < n}. fps_const (fps_nth y i) * fps_X ^ i)› for x y::‹'a fps›
proof -
  assume ‹x≠y›
  then have ‹∃n. (n = (LEAST n. fps_nth x n ≠ fps_nth y n))› 
    using fps_nth_inject by blast
  then obtain n where ‹ (n = (LEAST n. fps_nth x n ≠ fps_nth y n))› by blast
  then have ‹∀i<n. fps_nth x i = fps_nth y i›
    using not_less_Least by blast
  then have f0:‹(∑i<n. fps_const (fps_nth x i) * fps_X ^ i) = (∑i<n. fps_const (fps_nth y i) * fps_X ^ i)›
    by(auto)
  have rule:‹a≠c ⟹ a+b ≠ c+b› for a b c::"'a fps"
    unfolding fps_plus_def using fps_ext 
    by(auto simp:fun_eq_iff fps_ext Abs_fps_inverse fps_nth_inverse Abs_fps_inject) 
  have ‹fps_nth x n ≠ fps_nth y n› 
    by (metis (mono_tags, lifting) LeastI_ex ‹n = (LEAST n. fps_nth x n ≠ fps_nth y n)› ‹x ≠ y› fps_ext)
  then have ‹ (∑i<n. fps_const (fps_nth x i) * fps_X ^ i) + fps_const (fps_nth x n) * fps_X ^ n ≠
    (∑i<n. fps_const (fps_nth y i) * fps_X ^ i) + fps_const (fps_nth y n) * fps_X ^ n›
    by (metis (no_types, lifting) f0 add_left_imp_eq fps_nth_fps_const fps_shift_times_fps_X_power') 
  moreover have ‹ (∑i∈{x. x < Suc n}. fps_const (fps_nth z i) * fps_X ^ i) 
= (∑i<n. fps_const (fps_nth z i) * fps_X ^ i) + fps_const (fps_nth z n) * fps_X ^ n› for z::"'a fps"
  proof -
    have "∀n. {..<n::nat} = {na. na < n}"
      by (simp add: lessThan_def)
    then show ?thesis
      using sum.lessThan_Suc by auto
  qed
  ultimately show ‹∃n. (∑i∈{x. x < n}. fps_const (fps_nth x i) * fps_X ^ i) ≠
               (∑i∈{x. x < n}. fps_const (fps_nth y i) * fps_X ^ i)›
    by(auto intro: exI[where x=‹Suc n›]) 
qed


instance
  using intersection_equality exist_noneq 
  by intro_classes
    (auto cong: if_cong simp add:
     Collect_mono Int_absorb2 restriction_fps_def fps_sum_nth
     if_distrib[where f=fps_const]  if_distrib[where f=‹λx. a * x› for a]
     if_distrib[where f=‹λx. x * a› for a] lessThan_def sum.If_cases min_def)

end                                                           

lemma fps_sum_rep_nthb: "fps_nth (∑i<m. fps_const(a i)*fps_X^i) n = (if n < m then a n else 0)"
  by (simp add: fps_sum_nth if_distrib cong del: if_weak_cong)

lemma restriction_eq_iff :‹a↓n = b↓n ⟷ (∀i<n. fps_nth a i = fps_nth b i)›
  by (auto simp:restriction_fps_def) 
    (metis (full_types) fps_sum_rep_nthb)


lemma restriction_eqI :
  ‹(⋀i. i < n ⟹ fps_nth x i = fps_nth y i) ⟹ x ↓ n = y ↓ n›
  by (simp add: restriction_eq_iff)

lemma restriction_eqI' :
  ‹(⋀i. i ≤ n ⟹ fps_nth x i = fps_nth y i) ⟹ x ↓ n = y ↓ n›
  by (simp add: restriction_eq_iff)

instantiation fps :: (comm_ring_1) complete_restriction_space 
begin
instance
proof (intro_classes, rule restriction_convergentI)
  fix σ :: ‹nat ⇒'a fps› assume h:‹restriction_chain σ›
  have h':‹∀n. (∑i<n. fps_const (fps_nth (σ (Suc n)) i) * fps_X ^ i) = σ n›
    using h unfolding restriction_chain_def restriction_fps_def by auto
  let ?Σ = ‹Abs_fps (λn. fps_nth (σ (Suc n)) n)›
  have ‹?Σ ↓ (n) = σ n› for n
  proof (subst restricted_restriction_chain_is[OF ‹restriction_chain σ›, symmetric],
      rule restriction_eqI)
    fix i assume ‹i < n› 
    then have ‹i ≤ n› by auto
    from restriction_chain_def_ter
      [THEN iffD1, OF ‹restriction_chain σ›, rule_format, OF ‹i ≤ n›]
    show ‹fps_nth (Abs_fps (λn. fps_nth (σ (Suc n)) n)) i = fps_nth (σ n) i›
      by (subst Abs_fps_inverse, use Abs_fps_inject restriction_fps_def in blast)
        (smt (verit, ccfv_threshold) Suc_leI ‹i < n› h le_refl lessI restriction_eq_iff 
          restriction_chain_def restriction_chain_def_ter)     
  qed
  thus ‹restriction_chain σ ⟹ σ ─↓→ ?Σ› 
  proof -
    have "(↓) (Abs_fps (λn. fps_nth (σ (Suc n)) n)) = σ"
      using ‹⋀n. Abs_fps (λn. fps_nth (σ (Suc n)) n) ↓ n = σ n› by force
    then show ?thesis
      by (metis restriction_tendsto_restrictions)
  qed
qed

end

(*<*)
end
  (*>*)