Theory Restriction_Spaces.Restriction_Spaces_Induction

(***********************************************************************************
 * 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 ‹Induction in Restriction Space›

(*<*)
theory  Restriction_Spaces_Induction
  imports Restriction_Spaces_Topology
begin
  (*>*)

subsection ‹Admissibility›

named_theorems restriction_adm_simpset ― ‹For future automation.›

subsubsection ‹Definition›

text ‹We start by defining the notion of admissible predicate.
      The idea is that if this predicates holds for each value
      of a convergent sequence, it also holds for its limit.›

context restriction begin

definition restriction_adm :: ‹('a ⇒ bool) ⇒ bool› (‹adm⇩↓›)
  where ‹restriction_adm P ≡ ∀σ Σ. σ ─↓→ Σ ⟶ (∀n. P (σ n)) ⟶ P Σ›

lemma restriction_admI :
  ‹(⋀σ Σ. σ ─↓→ Σ ⟹ (⋀n. P (σ n)) ⟹ P Σ) ⟹ restriction_adm P›
  by (simp add: restriction_adm_def)

lemma restriction_admD :
  ‹⟦restriction_adm P; σ ─↓→ Σ; ⋀n. P (σ n)⟧ ⟹ P Σ›
  by (simp add: restriction_adm_def)


subsubsection ‹Properties›

lemma restriction_adm_const [restriction_adm_simpset] :
  ‹adm⇩↓ (λx. t)›
  by (simp add: restriction_admI)

lemma restriction_adm_conj [restriction_adm_simpset] :
  ‹adm⇩↓ (λx. P x) ⟹ adm⇩↓ (λx. Q x) ⟹ adm⇩↓ (λx. P x ∧ Q x)›
  by (fast intro: restriction_admI elim: restriction_admD)

lemma restriction_adm_all [restriction_adm_simpset] :
  ‹(⋀y. adm⇩↓ (λx. P x y)) ⟹ adm⇩↓ (λx. ∀y. P x y)›
  by (fast intro: restriction_admI elim: restriction_admD)

lemma restriction_adm_ball [restriction_adm_simpset] :
  ‹(⋀y. y ∈ A ⟹ adm⇩↓ (λx. P x y)) ⟹ adm⇩↓ (λx. ∀y∈A. P x y)›
  by (fast intro: restriction_admI elim: restriction_admD)

lemma restriction_adm_disj [restriction_adm_simpset] :
  ‹adm⇩↓ (λx. P x ∨ Q x)› if ‹adm⇩↓ (λx. P x)› ‹adm⇩↓ (λx. Q x)›
proof (rule restriction_admI)
  fix σ Σ
  assume * : ‹σ ─↓→ Σ› ‹⋀n. P (σ n) ∨ Q (σ n)›
  from "*"(2) have ** : ‹(∀i. ∃j≥i. P (σ j)) ∨ (∀i. ∃j≥i. Q (σ j))›
    by (meson nat_le_linear)

  { fix P assume $ : ‹adm⇩↓ (λx. P x)› ‹∀i. ∃j≥i. P (σ j)›
    define f where ‹f i = (LEAST j. i ≤ j ∧ P (σ j))› for i 
    have f1: ‹⋀i. i ≤ f i› and f2: ‹⋀i. P (σ (f i))›
      using LeastI_ex [OF "$"(2)[rule_format]] by (simp_all add: f_def)
    have f3 : ‹(λn. σ (f n)) ─↓→ Σ›
    proof (rule restriction_tendstoI)
      fix n
      from ‹σ ─↓→ Σ› restriction_tendstoD obtain n0 where ‹∀k≥n0. Σ ↓ n = σ k ↓ n› by blast
      hence ‹∀k≥max n0 n. Σ ↓ n = σ (f k) ↓ n› by (meson f1 le_trans max.boundedE)
      thus ‹∃n0. ∀k≥n0. Σ ↓ n = σ (f k) ↓ n› by blast
    qed
    have ‹P Σ› by (fact restriction_admD[OF "$"(1) f3 f2])
  }

  with "**" ‹adm⇩↓ (λx. P x)› ‹adm⇩↓ (λx. Q x)› show ‹P Σ ∨ Q Σ› by blast
qed

lemma restriction_adm_imp [restriction_adm_simpset] :
  ‹adm⇩↓ (λx. ¬ P x) ⟹ adm⇩↓ (λx. Q x) ⟹ adm⇩↓ (λx. P x ⟶ Q x)›
  by (subst imp_conv_disj) (rule restriction_adm_disj)


lemma restriction_adm_iff [restriction_adm_simpset] :
  ‹adm⇩↓ (λx. P x ⟶ Q x) ⟹ adm⇩↓ (λx. Q x ⟶ P x) ⟹ adm⇩↓ (λx. P x ⟷ Q x)›
  by (subst iff_conv_conj_imp) (rule restriction_adm_conj)

lemma restriction_adm_if_then_else [restriction_adm_simpset]:
  ‹⟦P ⟹ adm⇩↓ (λx. Q x); ¬ P ⟹ adm⇩↓ (λx. R x)⟧ ⟹
   adm⇩↓ (λx. if P then Q x else R x)›
  by (simp add: restriction_adm_def)

end



text ‹The notion of continuity is of course strongly related to the notion of admissibility.›

lemma restriction_adm_eq [restriction_adm_simpset] :
  ‹adm⇩↓ (λx. f x = g x)› if ‹cont⇩↓ f› and ‹cont⇩↓ g›
for f g :: ‹'a :: restriction ⇒ 'b :: restriction_space›
proof (rule restriction_admI)
  fix σ Σ assume ‹σ ─↓→ Σ› and ‹⋀n. f (σ n) = g (σ n)›
  from restriction_contD[OF ‹cont⇩↓ f› ‹σ ─↓→ Σ›] have ‹(λn. f (σ n)) ─↓→ f Σ› .
  hence ‹(λn. g (σ n)) ─↓→ f Σ› by (unfold ‹⋀n. f (σ n) = g (σ n)›)
  moreover from restriction_contD[OF ‹cont⇩↓ g› ‹σ ─↓→ Σ›] have ‹(λn. g (σ n)) ─↓→ g Σ› .
  ultimately show ‹f Σ = g Σ› by (fact restriction_tendsto_unique)
qed

lemma restriction_adm_subst [restriction_adm_simpset] :
  ‹adm⇩↓ (λx. P (t x))› if ‹cont⇩↓ (λx. t x)› and ‹adm⇩↓ P›
proof (rule restriction_admI)
  fix σ Σ assume ‹σ ─↓→ Σ› ‹⋀n. P (t (σ n))›
  from restriction_contD[OF ‹cont⇩↓ (λx. t x)› ‹σ ─↓→ Σ›]
  have ‹(λn. t (σ n)) ─↓→ t Σ› .
  from restriction_admD[OF ‹restriction_adm P› ‹(λn. t (σ n)) ─↓→ t Σ› ‹⋀n. P (t (σ n))›]
  show ‹P (t Σ)› .
qed



lemma restriction_adm_prod_domainD [restriction_adm_simpset] :
  ‹adm⇩↓ (λx. P (x, y))› and ‹adm⇩↓ (λy. P (x, y))› if ‹adm⇩↓ P›
proof -
  show ‹adm⇩↓ (λx. P (x, y))›
  proof (rule restriction_admI)
    show ‹P (Σ, y)› if ‹σ ─↓→ Σ› ‹⋀n. P (σ n, y)› for σ Σ
    proof (rule restriction_admD[OF ‹adm⇩↓ P› _ ‹⋀n. P (σ n, y)›])
      show ‹(λn. (σ n, y)) ─↓→ (Σ, y)›
        by (simp add: restriction_tendsto_prod_iff restriction_tendsto_const ‹σ ─↓→ Σ›)
    qed
  qed
next
  show ‹adm⇩↓ (λy. P (x, y))›
  proof (rule restriction_admI)
    show ‹P (x, Σ)› if ‹σ ─↓→ Σ› ‹⋀n. P (x, σ n)› for σ Σ
    proof (rule restriction_admD[OF ‹adm⇩↓ P› _ ‹⋀n. P (x, σ n)›])
      show ‹(λn. (x, σ n)) ─↓→ (x, Σ)›
        by (simp add: restriction_tendsto_prod_iff restriction_tendsto_const ‹σ ─↓→ Σ›)
    qed
  qed
qed



lemma restriction_adm_restriction_shift_on [restriction_adm_simpset] :
  ‹adm⇩↓ (λf. restriction_shift_on f k A)›
proof (rule restriction_admI)
  fix σ :: ‹nat ⇒ 'a ⇒ 'b› and Σ :: ‹'a ⇒ 'b›
  assume ‹σ ─↓→ Σ› and hyp : ‹restriction_shift_on (σ n) k A› for n
  show ‹restriction_shift_on Σ k A›
  proof (rule restriction_shift_onI)
    fix x y n assume ‹x ∈ A› ‹y ∈ A› ‹x ↓ n = y ↓ n›
    from hyp[THEN restriction_shift_onD, OF this]
    have * : ‹σ m x ↓ nat (int n + k) = σ m y ↓ nat (int n + k)› for m .
    show ‹Σ x ↓ nat (int n + k) = Σ y ↓ nat (int n + k)›
    proof (rule restriction_tendsto_unique)
      show ‹(λm. σ m x ↓ nat (int n + k)) ─↓→ Σ x ↓ nat (int n + k)›
        by (simp add: ‹σ ─↓→ Σ› restriction_tendsto_const_restricted restriction_tendsto_fun_imp)
    next
      show ‹(λm. σ m x ↓ nat (int n + k)) ─↓→ Σ y ↓ nat (int n + k)›
        by (simp add: "*" ‹σ ─↓→ Σ› restriction_tendsto_const_restricted restriction_tendsto_fun_imp)
    qed
  qed
qed

lemma restriction_adm_constructive_on [restriction_adm_simpset] :
  ‹adm⇩↓ (λf. constructive_on f A)›
  by (simp add: constructive_on_def restriction_adm_restriction_shift_on)

lemma restriction_adm_non_destructive_on [restriction_adm_simpset] :
  ‹adm⇩↓ (λf. non_destructive_on f A)›
  by (simp add: non_destructive_on_def restriction_adm_restriction_shift_on)


lemma restriction_adm_restriction_cont_at [restriction_adm_simpset] :
  ‹adm⇩↓ (λf. cont⇩↓ f at a)›
proof (rule restriction_admI)
  fix σ :: ‹nat ⇒ 'a ⇒ 'b› and Σ :: ‹'a ⇒ 'b›
  assume ‹σ ─↓→ Σ› and hyp : ‹cont⇩↓ (σ n) at a› for n
  show ‹cont⇩↓ Σ at a›
  proof (rule restriction_cont_atI)
    fix γ assume ‹γ ─↓→ a›
    from hyp[THEN restriction_cont_atD, OF this, THEN restriction_tendstoD]
    have ‹∃n0. ∀k≥n0. σ m a ↓ n = σ m (γ k) ↓ n› for m n .
    moreover from ‹σ ─↓→ Σ›[THEN restriction_tendstoD]
    have ‹∃n0. ∀k≥n0. Σ ↓ n = σ k ↓ n› for n .
    ultimately show ‹(λn. Σ (γ n)) ─↓→ Σ a›
      by (intro restriction_tendstoI) (metis restriction_fun_def)
  qed
qed

lemma restriction_adm_restriction_cont_on [restriction_adm_simpset] :
  ‹adm⇩↓ (λf. cont⇩↓ f on A)›
  unfolding restriction_cont_on_def
  by (intro restriction_adm_ball restriction_adm_restriction_cont_at)



corollary restriction_adm_restriction_shift [restriction_adm_simpset] :
  ‹adm⇩↓ (λf. restriction_shift f k)›
  and    restriction_adm_constructive [restriction_adm_simpset] :
  ‹adm⇩↓ (λf. constructive f)›
  and    restriction_adm_non_destructive [restriction_adm_simpset] :
  ‹adm⇩↓ (λf. non_destructive f)›
  and    restriction_adm_restriction_cont [restriction_adm_simpset] :
  ‹adm⇩↓ (λf. cont⇩↓ f)›
  by (simp_all add: restriction_adm_simpset restriction_shift_def
      constructive_def non_destructive_def)



lemma (in restriction) restriction_adm_mem_restriction_closed [restriction_adm_simpset] :
  ‹closed⇩↓ K ⟹ adm⇩↓ (λx. x ∈ K)›
  by (auto intro!: restriction_admI dest: restriction_closed_sequentialD)

lemma (in restriction_space) restriction_adm_mem_restriction_compact [restriction_adm_simpset] :
  ‹compact⇩↓ K ⟹ adm⇩↓ (λx. x ∈ K)›
  by (simp add: restriction_adm_mem_restriction_closed restriction_compact_imp_restriction_closed)

lemma (in restriction_space) restriction_adm_mem_finite [restriction_adm_simpset] :
  ‹finite S ⟹ adm⇩↓ (λx. x ∈ S)›
  by (simp add: finite_imp_restriction_compact restriction_adm_mem_restriction_compact)


lemma restriction_adm_restriction_tendsto [restriction_adm_simpset] :
  ‹adm⇩↓ (λσ. σ ─↓→ Σ)›
  by (intro restriction_admI restriction_tendstoI)
    (metis (no_types, opaque_lifting) restriction_fun_def restriction_tendsto_def)

lemma restriction_adm_lim [restriction_adm_simpset] :
  ‹adm⇩↓ (λΣ. σ ─↓→ Σ)›
  by (metis restriction_admI restriction_openD restriction_open_restriction_cball
      restriction_tendsto_iff_restriction_cball_characterization)


lemma restriction_restriction_cont_on [restriction_cont_simpset] :
  ‹cont⇩↓ f on A ⟹ cont⇩↓ (λx. f x ↓ n) on A›
  by (rule restriction_cont_onI)
    (simp add: restriction_cont_onD restriction_tendsto_const_restricted)

lemma restriction_cont_on_id [restriction_cont_simpset] : ‹cont⇩↓ (λx. x) on A›
  by (simp add: restriction_cont_onI)

lemma restriction_cont_on_const [restriction_cont_simpset] : ‹cont⇩↓ (λx. c) on A›
  by (simp add: restriction_cont_onI restriction_tendstoI)

lemma restriction_cont_on_fun [restriction_cont_simpset] : ‹cont⇩↓ (λf. f x) on A›
  by (rule restriction_cont_onI) (simp add: restriction_tendsto_fun_imp)

lemma restriction_cont2cont_on_fun [restriction_cont_simpset] :
  ‹cont⇩↓ f on A ⟹ cont⇩↓ (λx. f x y) on A›
  by (rule restriction_cont_onI)
    (metis restriction_cont_onD restriction_tendsto_fun_imp)







subsection ‹Induction›

text ‹Now that we have the concept of admissibility,
      we can formalize an induction rule for fixed points.
      Considering a \<^const>‹constructive› function \<^term>‹f› of type \<^typ>‹'a ⇒ 'a›
      (where \<^typ>‹'a› is instance of the class \<^class>‹complete_restriction_space›)
      and a predicate \<^term>‹P› which is admissible, and assuming that :
      ▪ \<^term>‹P› holds for a certain element \<^term>‹x›
      ▪ for any element \<^term>‹x›, if \<^term>‹P› holds for \<^term>‹x› then it still holds for \<^term>‹f x›
      
      we can have that \<^term>‹P› holds for the fixed point \<^term>‹υ x. P x›.›

lemma restriction_fix_ind' [case_names constructive adm steps] :
  ‹constructive f ⟹ adm⇩↓ P ⟹ (⋀n. P ((f ^^ n) x)) ⟹ P (υ x. f x)›
  using restriction_admD funpow_restriction_tendsto_restriction_fix by blast

lemma restriction_fix_ind [case_names constructive adm base step] :
  ‹P (υ x. f x)› if ‹constructive f› ‹adm⇩↓ P› ‹P x› ‹⋀x. P x ⟹ P (f x)›
proof (induct rule: restriction_fix_ind')
  show ‹constructive f› by (fact ‹constructive f›)
next
  show ‹restriction_adm P› by (fact ‹restriction_adm P›)
next
  show ‹P ((f ^^ n) x)› for n
    by (induct n) (simp_all add: ‹P x› ‹⋀x. P x ⟹ P (f x)›)
qed

lemma restriction_fix_ind2 [case_names constructive adm base0 base1 step] :
  ‹P (υ x. f x)› if ‹constructive f› ‹adm⇩↓ P› ‹P x› ‹P (f x)›
  ‹⋀x. ⟦P x; P (f x)⟧ ⟹ P (f (f x))›
proof (induct rule: restriction_fix_ind')
  show ‹constructive f› by (fact ‹constructive f›)
next
  show ‹restriction_adm P› by (fact ‹restriction_adm P›)
next
  show ‹P ((f ^^ n) x)› for n
    by (induct n rule: induct_nat_012) (simp_all add: that(3-5))
qed


text ‹We can rewrite the fixed point over a product to
      obtain this parallel fixed point induction rule. ›

lemma parallel_restriction_fix_ind [case_names constructiveL constructiveR adm base step] :
  fixes f :: ‹'a :: complete_restriction_space ⇒ 'a›
    and g :: ‹'b :: complete_restriction_space ⇒ 'b›
  assumes constructive : ‹constructive f› ‹constructive g›
    and adm  : ‹restriction_adm (λp. P (fst p) (snd p))›
    and base : ‹P x y› and step : ‹⋀x y. P x y ⟹ P (f x) (g y)›
  shows ‹P (υ x. f x) (υ y. g y)›
proof -
  define F where ‹F ≡ λ(x, y). (f x, g y)›
  define Q where ‹Q ≡ λ(x, y). P x y›

  have ‹P (υ x. f x) (υ y. g y) = Q (υ p. F p)›
    by (simp add: F_def Q_def constructive restriction_fix_indep_prod_is)
  also have ‹Q (υ p. F p)› 
  proof (induct F rule : restriction_fix_ind)
    show ‹constructive F›
      by (simp add: F_def constructive_prod_codomain_iff constructive_prod_domain_iff constructive constructive_const)
  next
    show ‹restriction_adm Q›
      by (unfold Q_def) (metis (mono_tags, lifting) adm case_prod_beta restriction_adm_def)
  next
    show ‹Q (x, y)› by (simp add: Q_def base)
  next
    show ‹Q p ⟹ Q (F p)› for p by (simp add: Q_def F_def step split_beta)
  qed
  finally show ‹P (υ x. f x) (υ y. g y)› .
qed


text ‹k-steps induction›

lemma restriction_fix_ind_k_steps [case_names constructive adm base_k_steps step] :
  assumes ‹constructive f›
    and ‹adm⇩↓ P›
    and ‹∀i < k. P ((f ^^ i) x)›
    and ‹⋀x. ∀i < k. P ((f ^^ i) x) ⟹ P ((f ^^ k) x)›
  shows ‹P (υ x. f x)›
proof (rule restriction_fix_ind')
  show ‹constructive f› by (fact ‹constructive f›)
next
  show ‹adm⇩↓ P› by (fact ‹adm⇩↓ P›)
next
  have nat_k_induct :
    ‹P n› if ‹∀i<k. P i› and ‹∀n⇩0. (∀i<k. P (n⇩0 + i)) ⟶ P (n⇩0 + k)› for k n :: nat and P
  proof (induct rule: nat_less_induct)
    fix n assume ‹∀m<n. P m›
    show ‹P n›
    proof (cases ‹n < k›)
      from that(1) show ‹n < k ⟹ P n› by blast
    next
      from ‹∀m<n. P m› that(2)[rule_format, of ‹n - k›]
      show ‹¬ n < k ⟹ P n› by auto
    qed
  qed
  show ‹P ((f ^^ i) x)› for i
  proof (induct rule: nat_k_induct)
    show ‹∀i<k. P ((f ^^ i) x)› by (simp add: assms(3))
  next
    show ‹∀n⇩0. (∀i<k. P ((f ^^ (n⇩0 + i)) x)) ⟶ P ((f ^^ (n⇩0 + k)) x)›
      by (smt (verit, del_insts) add.commute assms(4) funpow_add o_apply)
  qed
qed



(*<*)
end
  (*>*)