Theory Restriction_Spaces_Classes

(***********************************************************************************
 * 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 ‹Class Implementation›

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


subsection ‹Preliminaries›

text ‹Small lemma from ▩‹HOL-Library.Infinite_Set› to avoid dependency.›

lemma INFM_nat_le: ‹(∃⇩∞n :: nat. P n) ⟷ (∀m. ∃n≥m. P n)›
  unfolding cofinite_eq_sequentially frequently_sequentially by simp

text ‹We need to be able to extract a subsequence verifying a predicate.›


fun extraction_subseq :: ‹[nat ⇒ 'a, 'a ⇒ bool] ⇒ nat ⇒ nat›
  where ‹extraction_subseq σ P 0 = (LEAST k. P (σ k))›
  | ‹extraction_subseq σ P (Suc n) = (LEAST k. extraction_subseq σ P n < k ∧ P (σ k))›


lemma exists_extraction_subseq :
  assumes ‹∃⇩∞k. P (σ k)›
  defines f_def : ‹f ≡ extraction_subseq σ P›
  shows ‹strict_mono f› and ‹P (σ (f k))›
proof -
  have ‹f n < f (Suc n) ∧ P (σ (f n))› for n
    by (cases n, simp_all add: f_def)
      (metis (mono_tags, lifting) ‹∃⇩∞k. P (σ k)›[unfolded INFM_nat_le] LeastI_ex Suc_le_eq)+
  thus ‹strict_mono f› and ‹P (σ (f k))›
    by (simp_all add: strict_mono_Suc_iff)
qed


lemma extraction_subseqD :
  ‹∃f :: nat ⇒ nat. strict_mono f ∧ (∀k. P (σ (f k)))› if ‹∃⇩∞k. P (σ k)›
proof (rule exI)
  show ‹strict_mono (extraction_subseq σ P) ∧ (∀k. P (σ ((extraction_subseq σ P) k)))›
    by (simp add: ‹∃⇩∞k. P (σ k)› exists_extraction_subseq)
qed

lemma extraction_subseqE :
  ― ‹The idea is to abstract the concrete construction of this extraction function,
      we only need the fact that there is one.›
  ‹∃⇩∞k. P (σ k) ⟹ (⋀f :: nat ⇒ nat. strict_mono f ⟹ (⋀k. P (σ (f k))) ⟹ thesis) ⟹ thesis›
  by (blast dest: extraction_subseqD) 



subsection ‹Basic Notions for Restriction›

class restriction = 
  fixes restriction :: ‹['a, nat] ⇒ 'a›  (infixl ‹↓› 60)
  assumes [simp] : ‹x ↓ n ↓ m = x ↓ min n m›
begin

sublocale Restriction ‹(↓)› ‹(=)› by unfold_locales simp
    ― ‹Just to recover \<^const>‹restriction_related_set› and \<^const>‹restriction_not_related_set›.›
end

class restriction_space = restriction +
  assumes [simp] : ‹x ↓ 0 = y ↓ 0›
    and ex_not_restriction_eq : ‹x ≠ y ⟹ ∃n. x ↓ n ≠ y ↓ n›
begin

sublocale PreorderRestrictionSpace ‹(↓)› ‹(=)›
  by unfold_locales (simp_all add: ex_not_restriction_eq)



lemma restriction_related_set_commute :
  ‹restriction_related_set x y = restriction_related_set y x› by auto

lemma restriction_not_related_set_commute :
  ‹restriction_not_related_set x y = restriction_not_related_set y x› by auto

end

context restriction_space begin

sublocale Restriction_2_PreorderRestrictionSpace
  ‹(↓) :: 'b :: restriction ⇒ nat ⇒ 'b› ‹(=)›
  ‹(↓) :: 'a ⇒ nat ⇒ 'a› ‹(=)› ..

text ‹With this we recover constants like \<^const>‹restriction_shift_on›.›

sublocale PreorderRestrictionSpace_2_PreorderRestrictionSpace
  ‹(↓) :: 'b :: restriction_space ⇒ nat ⇒ 'b› ‹(=)›
  ‹(↓) :: 'a ⇒ nat ⇒ 'a› ‹(=)› ..

text ‹With that we recover theorems like @{thm constructive_restriction_restriction}.›

sublocale Restriction_2_PreorderRestrictionSpace_2_PreorderRestrictionSpace
  ‹(↓) :: 'c :: restriction ⇒ nat ⇒ 'c› ‹(=)›
  ‹(↓) :: 'b :: restriction_space ⇒ nat ⇒ 'b› ‹(=)›
  ‹(↓) :: 'a ⇒ nat ⇒ 'a› ‹(=)› ..

text ‹And with that we recover theorems like @{thm constructive_on_comp_non_destructive_on}.›



lemma restriction_shift_const [restriction_shift_simpset] :
  ‹restriction_shift (λx. c) k› by (simp add: restriction_shiftI)

lemma constructive_const [restriction_shift_simpset] :
  ‹constructive (λx. c)› by (simp add: constructiveI)




end

lemma restriction_shift_on_restricted [restriction_shift_simpset] :
  ‹restriction_shift_on (λx. f x ↓ n) k A› if ‹restriction_shift_on f k A›
proof (rule restriction_shift_onI)
  fix x y m assume ‹x ∈ A› ‹y ∈ A› ‹x ↓ m = y ↓ m›
  from restriction_shift_onD[OF ‹restriction_shift_on f k A› this]
  have ‹f x ↓ nat (int m + k) = f y ↓ nat (int m + k)› .
  hence ‹f x ↓ nat (int m + k) ↓ n = f y ↓ nat (int m + k) ↓ n› by argo
  thus ‹f x ↓ n ↓ nat (int m + k) = f y ↓ n ↓ nat (int m + k)›
    by (simp add: min.commute)
qed

lemma restriction_shift_restricted [restriction_shift_simpset] :
  ‹restriction_shift f k ⟹ restriction_shift (λx. f x ↓ n) k›
  using restriction_shift_def restriction_shift_on_restricted by blast

corollary constructive_restricted [restriction_shift_simpset] :
  ‹constructive f ⟹ constructive (λx. f x ↓ n)›
  by (simp add: constructive_def constructive_on_def restriction_shift_on_restricted)

corollary non_destructive_restricted [restriction_shift_simpset] :
  ‹non_destructive f ⟹ non_destructive (λx. f x ↓ n)›
  by (simp add: non_destructive_def non_destructive_on_def restriction_shift_on_restricted)


lemma non_destructive_id [restriction_shift_simpset] :
  ‹non_destructive id› ‹non_destructive (λx. x)›
  by (simp_all add: id_def non_destructiveI)



interpretation less_eqRS : Restriction ‹(↓)› ‹(≤)› by unfold_locales
    ― ‹Just to recover \<^const>‹less_eqRS.restriction_related_set› and
   \<^const>‹less_eqRS.restriction_not_related_set›.›


class preorder_restriction_space = restriction + preorder +
  assumes restriction_0_less_eq [simp] : ‹x ↓ 0 ≤ y ↓ 0›
    and mono_restriction_less_eq     : ‹x ≤ y ⟹ x ↓ n ≤ y ↓ n›
    and ex_not_restriction_less_eq   : ‹¬ x ≤ y ⟹ ∃n. ¬ x ↓ n ≤ y ↓ n›
begin

sublocale less_eqRS : PreorderRestrictionSpace ‹(↓) :: 'a ⇒ nat ⇒ 'a› ‹(≤)›
proof unfold_locales
  show ‹x ↓ 0 ≤ y ↓ 0› for x y :: 'a by simp
next
  show ‹x ≤ y ⟹ x ↓ n ≤ y ↓ n› for x y :: 'a and n
    by (fact mono_restriction_less_eq)
next
  show ‹¬ x ≤ y ⟹ ∃n. ¬ x ↓ n ≤ y ↓ n› for x y :: 'a
    by (simp add: ex_not_restriction_less_eq)
next
  show ‹x ≤ y ⟹ y ≤ z ⟹ x ≤ z› for x y z :: 'a by (fact order_trans)
qed

end


class order_restriction_space = preorder_restriction_space + order
begin

subclass restriction_space
proof unfold_locales
  show ‹x ↓ 0 = y ↓ 0› for x y :: 'a by (rule order_antisym) simp_all
next
  show ‹x ≠ y ⟹ ∃n. x ↓ n ≠ y ↓ n› for x y :: 'a
    by (metis ex_not_restriction_less_eq order.eq_iff)
qed

end


context preorder_restriction_space begin

sublocale less_eqRS : Restriction_2_PreorderRestrictionSpace
  ‹(↓) :: 'b :: {restriction, ord} ⇒ nat ⇒ 'b› ‹(≤)›
  ‹(↓) :: 'a ⇒ nat ⇒ 'a› ‹(≤)› ..

text ‹With this we recover constants like \<^const>‹less_eqRS.restriction_shift_on›.›

sublocale less_eqRS : PreorderRestrictionSpace_2_PreorderRestrictionSpace
  ‹(↓) :: 'b :: preorder_restriction_space ⇒ nat ⇒ 'b› ‹(≤)›
  ‹(↓) :: 'a ⇒ nat ⇒ 'a› ‹(≤)› ..

text ‹With that we recover theorems like @{thm less_eqRS.constructive_restriction_restriction}.›

sublocale less_eqRS : Restriction_2_PreorderRestrictionSpace_2_PreorderRestrictionSpace
  ‹(↓) :: 'c :: restriction ⇒ nat ⇒ 'c› ‹(=)›
  ‹(↓) :: 'b :: preorder_restriction_space ⇒ nat ⇒ 'b› ‹(≤)›
  ‹(↓) :: 'a ⇒ nat ⇒ 'a› ‹(≤)› ..

text ‹And with that we recover theorems like @{thm less_eqRS.constructive_on_comp_non_destructive_on}.›

end


context order_restriction_space begin

text ‹From @{thm order_antisym} we can obtain stronger lemmas.›

corollary order_restriction_shift_onI :
  ‹(⋀x y n. ⟦x ∈ A; y ∈ A; f x ≠ f y; x ↓ n = y ↓ n⟧ ⟹
             f x ↓ nat (int n + k) ≤ f y ↓ nat (int n + k))
   ⟹ restriction_shift_on f k A›
  by (simp add: order_antisym restriction_shift_onI)

corollary order_restriction_shiftI :
  ‹(⋀x y n. ⟦f x ≠ f y; x ↓ n = y ↓ n⟧ ⟹
             f x ↓ nat (int n + k) ≤ f y ↓ nat (int n + k))
   ⟹ restriction_shift f k›
  by (simp add: order_antisym restriction_shiftI)

corollary order_non_too_destructive_onI :
  ‹(⋀x y n. ⟦x ∈ A; y ∈ A; f x ≠ f y; x ↓ Suc n = y ↓ Suc n⟧ ⟹
             f x ↓ n ≤ f y ↓ n)
   ⟹ non_too_destructive_on f A›
  by (simp add: order_antisym non_too_destructive_onI)

corollary order_non_too_destructiveI :
  ‹(⋀x y n. ⟦f x ≠ f y; x ↓ Suc n = y ↓ Suc n⟧ ⟹ f x ↓ n ≤ f y ↓ n)
   ⟹ non_too_destructive f›
  by (simp add: order_antisym non_too_destructiveI)

corollary order_non_destructive_onI :
  ‹(⋀x y n. ⟦n ≠ 0; x ∈ A; y ∈ A; f x ≠ f y; x ↓ n = y ↓ n⟧ ⟹ f x ↓ n ≤ f y ↓ n)
   ⟹ non_destructive_on f A›
  by (simp add: order_antisym non_destructive_onI)

corollary order_non_destructiveI :
  ‹(⋀x y n. ⟦n ≠ 0; f x ≠ f y; x ↓ n = y ↓ n⟧ ⟹ f x ↓ n ≤ f y ↓ n)
   ⟹ non_destructive f›
  by (simp add: order_antisym non_destructiveI)

corollary order_constructive_onI :
  ‹(⋀x y n. ⟦x ∈ A; y ∈ A; f x ≠ f y; x ↓ n = y ↓ n⟧ ⟹ f x ↓ Suc n ≤ f y ↓ Suc n)
   ⟹ constructive_on f A›
  by (simp add: order_antisym constructive_onI)

corollary order_constructiveI :
  ‹(⋀x y n. ⟦f x ≠ f y; x ↓ n = y ↓ n⟧ ⟹ f x ↓ Suc n ≤ f y ↓ Suc n)
   ⟹ constructive f›
  by (simp add: order_antisym constructiveI)


end




subsection ‹Definition of the Fixed-Point Operator›

subsubsection ‹Preliminaries›

paragraph ‹Chain›

context restriction begin

definition restriction_chain :: ‹[nat ⇒ 'a] ⇒ bool› (‹chain⇩↓›)
  where ‹restriction_chain σ ≡ ∀n. σ (Suc n) ↓ n = σ n›

lemma restriction_chainI : ‹(⋀n. σ (Suc n) ↓ n = σ n) ⟹ restriction_chain σ›
  and restriction_chainD : ‹restriction_chain σ ⟹ σ (Suc n) ↓ n = σ n›
  by (simp_all add: restriction_chain_def)

end


context restriction_space begin

lemma (in restriction_space) restriction_chain_def_bis:
  ‹restriction_chain σ ⟷ (∀n m. n < m ⟶ σ m ↓ n = σ n)›
proof (rule iffI)
  show ‹∀n m. n < m ⟶ σ m ↓ n = σ n ⟹ restriction_chain σ›
    by (simp add: restriction_chainI)
next
  show ‹restriction_chain σ ⟹ ∀n m. n < m ⟶ σ m ↓ n = σ n›
  proof (intro allI impI)
    fix n m
    assume restriction : ‹restriction_chain σ›
    show ‹n < m ⟹ σ m ↓ n = σ n›
    proof (induct ‹m - n› arbitrary: m)
      fix m
      assume ‹0 = m - n› and ‹n < m›
      hence False by simp
      thus ‹σ m ↓ n = σ n› by simp
    next
      fix x m
      assume prems : ‹Suc x = m - n› ‹n < m›
      assume hyp : ‹x = m' - n ⟹ n < m' ⟹ σ m' ↓ n = σ n› for m'
      obtain m' where ‹m = Suc m'› by (meson less_imp_Suc_add prems(2))
      from prems(2) ‹m = Suc m'› consider ‹n = m'› | ‹n < m'› by linarith
      thus ‹σ m ↓ n = σ n›
      proof cases
        show ‹n = m' ⟹ σ m ↓ n = σ n› 
          by (simp add: ‹m = Suc m'› restriction restriction_chainD)
      next
        assume ‹n < m'›
        have * : ‹σ (Suc m') ↓ n = σ (Suc m') ↓ m' ↓ n› by (simp add: ‹n < m'›)
        from ‹m = Suc m'› prems(1) have ** : ‹x = m' - n› by linarith
        show ‹σ m ↓ n = σ n›
          by (simp add: "*" "**" ‹m = Suc m'› ‹n < m'› hyp restriction restriction_chainD)
      qed
    qed
  qed
qed


lemma restricted_restriction_chain_is :
  ‹restriction_chain σ ⟹ (λn. σ n ↓ n) = σ›
  by (rule ext) (metis min.idem restriction_chainD restriction_restriction)

lemma restriction_chain_def_ter:
  ‹restriction_chain σ ⟷ (∀n m. n ≤ m ⟶ σ m ↓ n = σ n)›
  by (metis le_eq_less_or_eq restricted_restriction_chain_is restriction_chain_def_bis)

lemma restriction_chain_restrictions : ‹restriction_chain ((↓) x)›
  by (simp add: restriction_chainI)

end



paragraph ‹Iterations›

text ‹The sequence of restricted images of powers of a constructive function
      is a \<^const>‹restriction_chain›.›

context fixes f :: ‹'a ⇒ 'a :: restriction_space› begin

lemma restriction_chain_funpow_restricted [simp]:
  ‹restriction_chain (λn. (f ^^ n) x ↓ n)› if ‹constructive f›
proof (rule restriction_chainI)
  show ‹(f ^^ Suc n) x ↓ Suc n ↓ n = (f ^^ n) x ↓ n› for n
  proof (induct n)
    show ‹(f ^^ Suc 0) x ↓ Suc 0 ↓ 0 = (f ^^ 0) x ↓ 0› by simp
  next
    fix n assume ‹(f ^^ Suc n) x ↓ Suc n ↓ n = (f ^^ n) x ↓ n›
    from ‹constructive f›[THEN constructiveD, OF this[simplified]]
    show ‹(f ^^ Suc (Suc n)) x ↓ Suc (Suc n) ↓ Suc n = (f ^^ Suc n) x ↓ Suc n› by simp
  qed
qed

lemma constructive_imp_eq_funpow_restricted :
  ‹n ≤ k ⟹ n ≤ l ⟹ (f ^^ k) x ↓ n = (f ^^ l) y ↓ n› if ‹constructive f›
proof (induct n arbitrary: k l)
  show ‹(f ^^ k) x ↓ 0 = (f ^^ l) y ↓ 0› for k l by simp
next
  fix n k l assume hyp : ‹n ≤ k ⟹ n ≤ l ⟹ (f ^^ k) x ↓ n = (f ^^ l) y ↓ n› for k l
  assume ‹Suc n ≤ k› ‹Suc n ≤ l›
  then obtain k' l' where ‹k = Suc k'› ‹n ≤ k'› ‹l = Suc l'› ‹n ≤ l'›
    by (metis Suc_le_D not_less_eq_eq)
  from ‹constructive f›[THEN constructiveD, OF hyp[OF ‹n ≤ k'› ‹n ≤ l'›]]
  show ‹(f ^^ k) x ↓ Suc n = (f ^^ l) y ↓ Suc n›
    by (simp add: ‹k = Suc k'› ‹l = Suc l'›)
qed

end



paragraph ‹Limits and Convergence›

context restriction begin

definition restriction_tendsto :: ‹[nat ⇒ 'a, 'a] ⇒ bool› (‹((_)/ ─↓→ (_))› [59, 59] 59)
  where ‹σ ─↓→ Σ ≡ ∀n. ∃n0. ∀k≥n0. Σ ↓ n = σ k ↓ n›

lemma restriction_tendstoI : ‹(⋀n. ∃n0. ∀k≥n0. Σ ↓ n = σ k ↓ n) ⟹ σ ─↓→ Σ›
  by (simp add: restriction_tendsto_def)

lemma restriction_tendstoD : ‹σ ─↓→ Σ ⟹ ∃n0. ∀k≥n0. Σ ↓ n = σ k ↓ n›
  by (simp add: restriction_tendsto_def) 

lemma restriction_tendstoE :
  ‹σ ─↓→ Σ ⟹ (⋀n0. (⋀k. n0 ≤ k ⟹ Σ ↓ n = σ k ↓ n) ⟹ thesis) ⟹ thesis›
  using restriction_tendstoD by blast

end


lemma (in restriction_space) restriction_tendsto_unique :
  ‹σ ─↓→ Σ ⟹ σ ─↓→ Σ' ⟹ Σ = Σ'›
  by (metis ex_not_restriction_eq restriction_tendstoD nat_le_linear)


context restriction begin

lemma restriction_tendsto_const_restricted :
  ‹σ ─↓→ Σ ⟹ (λn. σ n ↓ k) ─↓→ Σ ↓ k›
  unfolding restriction_tendsto_def by metis

lemma restriction_tendsto_iff_eventually_in_restriction_eq_set :
  ‹σ ─↓→ Σ ⟷ (∀n. ∃n0. ∀k≥n0. n ∈ restriction_related_set Σ (σ k))›
  by (simp add: restriction_tendsto_def)


lemma restriction_tendsto_const : ‹(λn. Σ) ─↓→ Σ›
  by (simp add: restriction_tendstoI)

lemma (in restriction_space) restriction_tendsto_restrictions : ‹(λn. Σ ↓ n) ─↓→ Σ›
  by (metis restriction_tendstoI restriction_chain_def_ter restriction_chain_restrictions)

lemma restriction_tendsto_shift_iff : ‹(λn. σ (n + l)) ─↓→ Σ ⟷ σ ─↓→ Σ›
proof (rule iffI)
  show ‹(λn. σ (n + l)) ─↓→ Σ› if ‹σ ─↓→ Σ›
  proof (rule restriction_tendstoI)
    from ‹σ ─↓→ Σ›[THEN restriction_tendstoD]
    show ‹∃n0. ∀k≥n0. Σ ↓ n = σ (k + l) ↓ n› for n by (meson trans_le_add1)
  qed
next
  show ‹σ ─↓→ Σ› if ‹(λn. σ (n + l)) ─↓→ Σ›
  proof (rule restriction_tendstoI)
    fix n
    from ‹(λn. σ (n + l)) ─↓→ Σ›[THEN restriction_tendstoD]
    obtain n0 where ‹∀k≥n0. Σ ↓ n = σ (k + l) ↓ n› ..
    hence ‹∀k≥n0 + l. Σ ↓ n = σ k ↓ n›
      by (metis add.commute add_leD2 add_le_imp_le_left le_iff_add)
    thus ‹∃n1. ∀k≥n1. Σ ↓ n = σ k ↓ n› ..
  qed
qed


lemma restriction_tendsto_shiftI : ‹σ ─↓→ Σ ⟹ (λn. σ (n + l)) ─↓→ Σ›
  by (simp add: restriction_tendsto_shift_iff)

lemma restriction_tendsto_shiftD : ‹(λn. σ (n + l)) ─↓→ Σ ⟹ σ ─↓→ Σ›
  by (simp add: restriction_tendsto_shift_iff)


lemma (in restriction_space) restriction_tendsto_restricted_iff_restriction_tendsto :
  ‹(λn. σ n ↓ n) ─↓→ Σ ⟷ σ ─↓→ Σ›
proof (rule iffI)
  assume * : ‹(λn. σ n ↓ n) ─↓→ Σ›
  show ‹σ ─↓→ Σ›
  proof (rule restriction_tendstoI)
    fix n
    from "*" restriction_tendstoE obtain n0 where ‹n0 ≤ k ⟹ Σ ↓ n = σ k ↓ k ↓ n› for k by blast
    hence ‹max n0 n ≤ k ⟹ Σ ↓ n = σ k ↓ n› for k by auto
    thus ‹∃n0. ∀k≥n0. Σ ↓ n = σ k ↓ n› by blast
  qed
next
  assume * : ‹σ ─↓→ Σ›
  show ‹(λn. σ n ↓ n) ─↓→ Σ›
  proof (rule restriction_tendstoI)
    fix n
    from "*" restriction_tendstoE obtain n0 where ‹n0 ≤ k ⟹ Σ ↓ n = σ k ↓ n› for k by blast
    hence ‹max n0 n ≤ k ⟹ Σ ↓ n = σ k ↓ k ↓ n› for k by auto
    thus ‹∃n0. ∀k≥n0. Σ ↓ n = σ k ↓ k ↓ n› by blast
  qed
qed

lemma restriction_tendsto_subseq :
  ‹(σ ∘ f) ─↓→ Σ› if ‹strict_mono f› and ‹σ ─↓→ Σ›
proof (rule restriction_tendstoI)
  fix n
  have ‹n ≤ f n› by (simp add: strict_mono_imp_increasing ‹strict_mono f›)
  moreover from ‹σ ─↓→ Σ› restriction_tendstoE obtain n0 where ‹n0 ≤ k ⟹ Σ ↓ n = σ k ↓ n› for k by blast
  ultimately have ‹∀k≥n0. Σ ↓ n = σ (f k) ↓ n›
    by (metis le_trans strict_mono_imp_increasing that(1))
  thus ‹∃n0. ∀k≥n0. Σ ↓ n = (σ ∘ f) k ↓ n› by auto
qed

end


context restriction begin

definition restriction_convergent :: ‹(nat ⇒ 'a) ⇒ bool› (‹convergent⇩↓›)
  where ‹restriction_convergent σ ≡ ∃Σ. σ ─↓→ Σ›

lemma restriction_convergentI : ‹σ ─↓→ Σ ⟹ restriction_convergent σ›
  by (auto simp add: restriction_convergent_def)

lemma restriction_convergentD' : ‹restriction_convergent σ ⟹ ∃Σ. σ ─↓→ Σ›
  by (simp add: restriction_convergent_def)

end


context restriction_space begin

lemma restriction_convergentD :
  ‹restriction_convergent σ ⟹ ∃!Σ. σ ─↓→ Σ›
  unfolding restriction_convergent_def using restriction_tendsto_unique by blast

lemma restriction_convergentE : 
  ‹restriction_convergent σ ⟹
   (⋀Σ. σ ─↓→ Σ ⟹ (⋀Σ'. σ ─↓→ Σ' ⟹ Σ' = Σ) ⟹ thesis) ⟹ thesis›
  using restriction_convergentD by blast

lemma restriction_tendsto_of_restriction_convergent :
  ‹restriction_convergent σ ⟹ σ ─↓→ (THE Σ. σ ─↓→ Σ)›
  by (simp add: restriction_convergentD the1I2)

end



context restriction begin

lemma restriction_convergent_const [simp] : ‹convergent⇩↓ (λn. Σ)›
  unfolding restriction_convergent_def restriction_tendsto_def by blast

lemma (in restriction_space) restriction_convergent_restrictions [simp] :
  ‹convergent⇩↓ (λn. Σ ↓ n)›
  using restriction_convergent_def restriction_tendsto_restrictions by blast

lemma restriction_convergent_shift_iff :
  ‹convergent⇩↓ (λn. σ (n + l)) ⟷ convergent⇩↓ σ›
  by (simp add: restriction_convergent_def restriction_tendsto_shift_iff)


lemma restriction_convergent_shift_shiftI :
  ‹convergent⇩↓ σ ⟹ convergent⇩↓ (λn. σ (n + l))›
  by (simp add: restriction_convergent_shift_iff)

lemma restriction_convergent_shift_shiftD :
  ‹convergent⇩↓ (λn. σ (n + l)) ⟹ convergent⇩↓ σ›
  by (simp add: restriction_convergent_shift_iff)


lemma (in restriction_space) restriction_convergent_restricted_iff_restriction_convergent :
  ‹convergent⇩↓ (λn. σ n ↓ n) ⟷ convergent⇩↓ σ›
  by (simp add: restriction_convergent_def
      restriction_tendsto_restricted_iff_restriction_tendsto)


lemma restriction_convergent_subseq :
  ‹strict_mono f ⟹ restriction_convergent σ ⟹ restriction_convergent (σ ∘ f)›
  unfolding restriction_convergent_def using restriction_tendsto_subseq by blast

lemma (in restriction_space)
  convergent_restriction_chain_imp_ex1 : ‹∃!Σ. ∀n. Σ ↓ n = σ n›
  and restriction_tendsto_of_convergent_restriction_chain : ‹σ ─↓→ (THE Σ. ∀n. Σ ↓ n = σ n)›
  if ‹restriction_convergent σ› and ‹restriction_chain σ›
proof -
  from ‹restriction_convergent σ› restriction_convergentE obtain Σ
    where ‹σ ─↓→ Σ› ‹⋀Σ'. σ ─↓→ Σ' ⟹ Σ' = Σ› by blast

  have * : ‹Σ ↓ n = σ n› for n
  proof -
    from ‹σ ─↓→ Σ› restriction_tendstoE obtain n0 where ‹n0 ≤ k ⟹ Σ ↓ n = σ k ↓ n› for k by blast
    hence ‹Σ ↓ n = σ (max n0 n) ↓ n› by simp
    thus ‹Σ ↓ n = σ n›
      by (simp add: restriction_chain_def_ter[THEN iffD1, OF ‹restriction_chain σ›])
  qed
  have ** : ‹∀n. Σ' ↓ n = σ n ⟹ Σ' = Σ› for Σ'
    by (metis "*" ex_not_restriction_eq)
  from "*" "**" show ‹∃!Σ. ∀n. Σ ↓ n = σ n› by blast
  from theI'[OF this] "**" have ‹Σ = (THE Σ. ∀n. Σ ↓ n = σ n)› by simp
  with ‹σ ─↓→ Σ› show ‹σ ─↓→ (THE Σ. ∀n. Σ ↓ n = σ n)› by simp
qed

end



subsubsection ‹Fixed-Point Operator›

text ‹Our definition only makes sense if such a fixed point exists and is unique.
      We will therefore directly add a completeness assumption,
      and define the fixed-point operator within this context.
      It will only be valid when the function \<^term>‹f› is \<^const>‹constructive›.›

class complete_restriction_space = restriction_space +
  assumes restriction_chain_imp_restriction_convergent : ‹chain⇩↓ σ ⟹ convergent⇩↓ σ›

definition (in complete_restriction_space)
  restriction_fix :: ‹('a ⇒ 'a) ⇒ 'a› (* (binder ‹υ › 10) *)
  ― ‹We will use a syntax rather than a binder to be compatible with the product.›
  where ‹restriction_fix (λx. f x) ≡ THE Σ. (λn. (f ^^ n) undefined) ─↓→ Σ›

syntax "_restriction_fix" :: ‹[pttrn, 'a ⇒ 'a] ⇒ 'a›
  (‹(‹indent=3 notation=‹binder restriction_fix››υ _./ _)› [0, 10] 10)
syntax_consts "_restriction_fix" ⇌ restriction_fix
translations "υ x. f" ⇌ "CONST restriction_fix (λx. f)"
print_translation ‹
  [(\<^const_syntax>‹restriction_fix›, fn ctxt => fn [Abs abs] =>
      let val (x, t) = Syntax_Trans.atomic_abs_tr' ctxt abs
      in Syntax.const \<^syntax_const>‹_restriction_fix› $ x $ t end)]
›  ― ‹To avoid eta-contraction of body›


context complete_restriction_space begin

text ‹The following result is quite similar to the Banach's fixed point theorem.›

lemma restriction_chain_imp_ex1 : ‹∃!Σ. ∀n. Σ ↓ n = σ n›
  and restriction_tendsto_of_restriction_chain : ‹σ ─↓→ (THE Σ. ∀n. Σ ↓ n = σ n)›
  if ‹restriction_chain σ›
  by (simp_all add: convergent_restriction_chain_imp_ex1
      restriction_tendsto_of_convergent_restriction_chain
      restriction_chain_imp_restriction_convergent ‹restriction_chain σ›)



lemma restriction_chain_is :
  ‹σ = (↓) (THE Σ. σ ─↓→ Σ)›
  ‹σ = (↓) (THE Σ. ∀n. Σ ↓ n = σ n)› if ‹restriction_chain σ›
proof -
  from restriction_tendsto_of_restriction_chain[OF ‹restriction_chain σ›]
  have ‹σ ─↓→ (THE Σ. ∀n. Σ ↓ n = σ n)› .
  with restriction_tendsto_of_restriction_convergent
    restriction_convergentI restriction_tendsto_unique
  have * : ‹(THE Σ. ∀n. Σ ↓ n = σ n) = (THE Σ. σ ─↓→ Σ)› by blast

  from theI'[OF restriction_chain_imp_ex1, OF ‹restriction_chain σ›]
  show ‹σ = (↓) (THE Σ. ∀n. Σ ↓ n = σ n)› by (intro ext) simp
  with "*" show ‹σ = (↓) (THE Σ. σ ─↓→ Σ)› by auto
qed

end


context 
  fixes f :: ‹'a ⇒ 'a :: complete_restriction_space›
  assumes ‹constructive f›
begin

lemma ex1_restriction_fix :
  ‹∃!Σ. ∀x. (λn. (f ^^ n) x) ─↓→ Σ›
proof -
  let ?σ = ‹λx n. (f ^^ n) x ↓ n›
  from constructive_imp_eq_funpow_restricted[OF ‹constructive f›]
  have ‹?σ x = ?σ y› for x y by blast
  moreover have ‹restriction_chain (?σ x)› for x by (simp add: ‹constructive f›)
  ultimately obtain Σ where ‹∀x. ?σ x ─↓→ Σ›
    by (metis (full_types) restriction_chain_is(1) restriction_tendsto_restrictions)
  with restriction_tendsto_unique have ‹∃!Σ. ∀x. ?σ x ─↓→ Σ› by blast
  thus ‹∃!Σ. ∀x. (λn. (f ^^ n) x) ─↓→ Σ›
    by (simp add: restriction_tendsto_restricted_iff_restriction_tendsto)
qed

lemma ex1_restriction_fix_bis :
  ‹∃!Σ. (λn. (f ^^ n) x) ─↓→ Σ›
  using ex1_restriction_fix restriction_tendsto_unique by blast


lemma restriction_fix_def_bis :
  ‹(υ x. f x) = (THE Σ. (λn. (f ^^ n) x) ─↓→ Σ)›
proof -
  have ‹(λΣ. (λn. (f ^^ n) undefined) ─↓→ Σ) = (λΣ. (λn. (f ^^ n) x) ─↓→ Σ)›
    by (metis ex1_restriction_fix restriction_tendsto_unique)
  from arg_cong[where f = The, OF this, folded restriction_fix_def]
  show ‹(υ x. f x) = (THE Σ. (λn. (f ^^ n) x) ─↓→ Σ)› .
qed


lemma funpow_restriction_tendsto_restriction_fix : ‹(λn. (f ^^ n) x) ─↓→ (υ x. f x)›
  by (metis ex1_restriction_fix restriction_convergentI
      restriction_fix_def_bis restriction_tendsto_of_restriction_convergent)


lemma restriction_restriction_fix_is : ‹(υ x. f x) ↓ n = (f ^^ n) x ↓ n›
proof (rule restriction_tendsto_unique)
  from funpow_restriction_tendsto_restriction_fix
  show ‹(λk. (f ^^ k) x ↓ n) ─↓→ (υ x. f x) ↓ n›
    by (simp add: restriction_tendsto_def)
next
  from restriction_tendsto_restrictions
  have ‹(λk. (f ^^ n) x ↓ n ↓ k) ─↓→ (f ^^ n) x ↓ n› .
  then obtain n0 where * : ‹∀k≥n0. (f ^^ n) x ↓ n = (f ^^ n) x ↓ n ↓ k›
    by (metis restriction_restriction min_def)
  show ‹(λk. (f ^^ k) x ↓ n) ─↓→ (f ^^ n) x ↓ n›
  proof (rule restriction_tendstoI)
    fix m
    from * have ‹∀k≥n + n0 + m. (f ^^ n) x ↓ n ↓ m = (f ^^ k) x ↓ n ↓ m›
      by (simp add: ‹constructive f› constructive_imp_eq_funpow_restricted)
    thus ‹∃n0. ∀k≥n0. (f ^^ n) x ↓ n ↓ m = (f ^^ k) x ↓ n ↓ m› ..
  qed
qed


lemma restriction_fix_eq : ‹(υ x. f x) = f (υ x. f x)›
proof (subst restriction_fix_def, intro the1_equality restriction_tendstoI)
  show ‹∃!Σ. (λn. (f ^^ n) undefined) ─↓→ Σ›
    by (simp add: ex1_restriction_fix_bis)
next
  have ‹n ≤ k ⟹ f (restriction_fix f) ↓ n = (f ^^ k) undefined ↓ n› for n k
    by (cases n, simp, cases k, simp_all)
      (meson ‹constructive f›[THEN constructiveD] restriction_related_le
        restriction_restriction_fix_is)
  thus ‹∃n0. ∀k≥n0. f (restriction_fix f) ↓ n = (f ^^ k) undefined ↓ n› for n by blast
qed


lemma restriction_fix_unique : ‹f x = x ⟹ (υ x. f x) = x›
  by (metis (no_types, opaque_lifting) restriction_fix_eq ‹constructive f›
      constructiveD dual_order.refl take_lemma_restriction)


lemma restriction_fix_def_ter : ‹(υ x. f x) = (THE x. f x = x)›
  by (metis (mono_tags, lifting) restriction_fix_eq restriction_fix_unique the_equality)




end



(*<*)
end
  (*>*)