Theory Restriction_Spaces.Restriction_Spaces_Fun

(***********************************************************************************
 * 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 ‹Functions towards a Restriction Space›

subsection ‹Restriction Space›

(*<*)
theory Restriction_Spaces_Fun
  imports Restriction_Spaces_Classes
begin
  (*>*)

instantiation ‹fun› :: (type, restriction) restriction
begin

definition restriction_fun :: ‹['a ⇒ 'b, nat, 'a] ⇒ 'b›
  where ‹f ↓ n ≡ (λx. f x ↓ n)›

instance by intro_classes (simp add: restriction_fun_def)

end 


instance ‹fun› :: (type, restriction_space) restriction_space
proof (intro_classes, unfold restriction_fun_def)
  show ‹(λx. f x ↓ 0) = (λx. g x ↓ 0)›
    for f g :: ‹'a ⇒ 'b› by (rule ext) simp
next
  fix f g :: ‹'a ⇒ 'b› assume ‹f ≠ g›
  then obtain x where ‹f x ≠ g x› by fast
  with ex_not_restriction_related obtain n
    where ‹f x ↓ n ≠ g x ↓ n› by blast
  hence ‹(λx. f x ↓ n) ≠ (λx. g x ↓ n)› by meson
  thus ‹∃n. (λx. f x ↓ n) ≠ (λx. g x ↓ n)› ..
qed


instance ‹fun› :: (type, preorder_restriction_space) preorder_restriction_space
proof intro_classes
  show ‹f ↓ 0 ≤ g ↓ 0› for f g :: ‹'a ⇒ 'b›
    by (simp add: le_fun_def restriction_fun_def)
next
  show ‹f ≤ g ⟹ f ↓ n ≤ g ↓ n› for f g :: ‹'a ⇒ 'b› and n
    by (simp add: restriction_fun_def le_fun_def mono_restriction_less_eq)
next
  show ‹¬ f ≤ g ⟹ ∃n. ¬ f ↓ n ≤ g ↓ n› for f g :: ‹'a ⇒ 'b›
    by (metis ex_not_restriction_less_eq le_funD le_funI restriction_fun_def)
qed

instance ‹fun› :: (type, order_restriction_space) order_restriction_space ..




subsection ‹Restriction shift Maps›

lemma restriction_shift_on_fun_iff :
  ‹restriction_shift_on f k A ⟷ (∀z. restriction_shift_on (λx. f x z) k A)›
proof (intro iffI allI)
  show ‹restriction_shift_on (λx. f x z) k A› if ‹restriction_shift_on f k A› for z
  proof (rule restriction_shift_onI)
    fix x y n assume ‹x ∈ A› ‹y ∈ A› ‹x ↓ n = y ↓ n›
    from restriction_shift_onD[OF ‹restriction_shift_on f k A› this]
    show ‹f x z ↓ nat (int n + k) = f y z ↓ nat (int n + k)›
      by (unfold restriction_fun_def) (blast dest!: fun_cong)
  qed
next
  show ‹restriction_shift_on f k A› if ‹∀z. restriction_shift_on (λx. f x z) k A›
  proof (rule restriction_shift_onI)
    fix x y n assume ‹x ∈ A› ‹y ∈ A› ‹x ↓ n = y ↓ n›
    with ‹∀z. restriction_shift_on (λx. f x z) k A› restriction_shift_onD
    have ‹f x z ↓ nat (int n + k) = f y z ↓ nat (int n + k)› for z by blast
    thus ‹f x ↓ nat (int n + k) = f y ↓ nat (int n + k)›
      by (simp add: restriction_fun_def)
  qed
qed

lemma restriction_shift_fun_iff : ‹restriction_shift f k ⟷ (∀z. restriction_shift (λx. f x z) k)›
  by (unfold restriction_shift_def, fact restriction_shift_on_fun_iff)


lemma non_too_destructive_on_fun_iff:
  ‹non_too_destructive_on f A ⟷ (∀z. non_too_destructive_on (λx. f x z) A)›
  by (simp add: non_too_destructive_on_def restriction_shift_on_fun_iff)

lemma non_too_destructive_fun_iff:
  ‹non_too_destructive f ⟷ (∀z. non_too_destructive (λx. f x z))›
  by (unfold restriction_shift_def non_too_destructive_def)
    (fact non_too_destructive_on_fun_iff)


lemma non_destructive_on_fun_iff:
  ‹non_destructive_on f A ⟷ (∀z. non_destructive_on (λx. f x z) A)›
  by (simp add: non_destructive_on_def restriction_shift_on_fun_iff)

lemma non_destructive_fun_iff:
  ‹non_destructive f ⟷ (∀z. non_destructive (λx. f x z))›
  unfolding non_destructive_def by (fact non_destructive_on_fun_iff)


lemma constructive_on_fun_iff:
  ‹constructive_on f A ⟷ (∀z. constructive_on (λx. f x z) A)›
  by (simp add: constructive_on_def restriction_shift_on_fun_iff)

lemma constructive_fun_iff:
  ‹constructive f ⟷ (∀z. constructive (λx. f x z))›
  unfolding constructive_def by (fact constructive_on_fun_iff)



lemma restriction_shift_fun [restriction_shift_simpset, restriction_shift_introset] :
  ‹(⋀z. restriction_shift (λx. f x z) k) ⟹ restriction_shift f k›
  and non_too_destructive_fun [restriction_shift_simpset, restriction_shift_introset] :
  ‹(⋀z. non_too_destructive (λx. f x z)) ⟹ non_too_destructive f›
  and non_destructive_fun [restriction_shift_simpset, restriction_shift_introset] :
  ‹(⋀z. non_destructive (λx. f x z)) ⟹ non_destructive f›
  and constructive_fun [restriction_shift_simpset, restriction_shift_introset] :
  ‹(⋀z. constructive (λx. f x z)) ⟹ constructive f›
  by (simp_all add: restriction_shift_fun_iff non_too_destructive_fun_iff
      non_destructive_fun_iff constructive_fun_iff)



subsection ‹Limits and Convergence›

lemma reached_dist_funE :
  fixes f g :: ‹'a ⇒ 'b :: restriction_space› assumes ‹f ≠ g›
  obtains x where ‹f x ≠ g x› ‹Sup (restriction_related_set f g) = Sup (restriction_related_set (f x) (g x))›
    ―‹Morally, we say here that the distance between two functions is reached.
   But we did not introduce the concept of distance.›
proof -
  let ?n = ‹Sup (restriction_related_set f g)›
  from Sup_in_restriction_related_set[OF ‹f ≠ g›]
  have ‹?n ∈ restriction_related_set f g› .
  with restriction_related_le have ‹∀m≤?n. f ↓ m = g ↓ m› by blast
  moreover have ‹f ↓ Suc ?n ≠ g ↓ Suc ?n›
    using cSup_upper[OF _ bdd_above_restriction_related_set_iff[THEN iffD2, OF ‹f ≠ g›], of ‹Suc ?n›]
    by (metis (mono_tags, lifting) dual_order.refl mem_Collect_eq not_less_eq_eq restriction_related_le)
  ultimately obtain x where * : ‹∀m≤?n. f x ↓ m = g x ↓ m› ‹f x ↓ Suc ?n ≠ g x ↓ Suc ?n›
    unfolding restriction_fun_def by meson
  from "*"(2) have ‹f x ≠ g x› by auto
  moreover from "*" have ‹?n = Sup (restriction_related_set (f x) (g x))›
    by (metis (no_types, lifting) ‹∀m≤?n. f ↓ m = g ↓ m›
        ‹f ↓ Suc ?n ≠ g ↓ Suc ?n› not_less_eq_eq restriction_related_le)
  ultimately show thesis using that by blast
qed


lemma reached_restriction_related_set_funE : 
  fixes f g :: ‹'a ⇒ 'b :: restriction_space›
  obtains x where ‹restriction_related_set f g = restriction_related_set (f x) (g x)›
proof (cases ‹f = g›)
  from that show ‹f = g ⟹ thesis› by simp
next
  from that show ‹f ≠ g ⟹ thesis›
    by (elim reached_dist_funE) (metis (full_types) restriction_related_set_is_atMost)
qed



lemma restriction_chain_fun_iff :
  ‹restriction_chain σ ⟷ (∀z. restriction_chain (λn. σ n z))›
proof (intro iffI allI)
  show ‹restriction_chain σ ⟹ restriction_chain (λn. σ n z)› for z
    by (auto simp add: restriction_chain_def restriction_fun_def dest!: fun_cong)
next
  show ‹∀z. restriction_chain (λn. σ n z) ⟹ restriction_chain σ›
    by (simp add: restriction_chain_def restriction_fun_def)
qed



lemma restriction_tendsto_fun_imp : ‹σ ─↓→ Σ ⟹ (λn. σ n z) ─↓→ Σ z›
  by (simp add: restriction_tendsto_def restriction_fun_def) meson


lemma restriction_convergent_fun_imp :
  ‹restriction_convergent σ ⟹ restriction_convergent (λn. σ n z)›
  by (metis restriction_convergent_def restriction_tendsto_fun_imp)


subsection ‹Completeness›

instance ‹fun› :: (type, complete_restriction_space) complete_restriction_space
proof intro_classes
  fix σ :: ‹nat ⇒ 'a ⇒ 'b :: complete_restriction_space›
  assume ‹restriction_chain σ›
  hence * : ‹restriction_chain (λn. σ n x)› for x
    by (simp add: restriction_chain_fun_iff)
  from restriction_chain_imp_restriction_convergent[OF this]
  have ** : ‹restriction_convergent (λn. σ n x)› for x .
  then obtain Σ where *** : ‹(λn. σ n x) ─↓→ Σ x› for x
    by (meson restriction_convergent_def)
  from "*" have **** : ‹(λn. σ n x ↓ n) = (λn. σ n x)› for x
    by (simp add: restricted_restriction_chain_is)
  have ‹σ ─↓→ Σ›
  proof (rule restriction_tendstoI)
    fix n
    have ‹∀k≥n. Σ x ↓ n = σ k x ↓ n› for x
      by (metis "*" "**" "***" "****" restriction_related_le restriction_chain_is(1)
          restriction_tendsto_of_restriction_convergent restriction_tendsto_unique)
    hence ‹∀k≥n. Σ ↓ n = σ k ↓ n› by (simp add: restriction_fun_def)
    thus ‹∃n0. ∀k≥n0. Σ ↓ n = σ k ↓ n› by blast
  qed

  thus ‹restriction_convergent σ› by (fact restriction_convergentI)
qed



(*<*)
end
  (*>*)