Theory Restriction_Spaces_Prod

(***********************************************************************************
 * 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 ‹Product over Restriction Spaces›

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

subsection ‹Restriction Space›

instantiation prod :: (restriction, restriction) restriction
begin

definition restriction_prod :: ‹'a × 'b ⇒ nat ⇒ 'a × 'b›
  where ‹p ↓ n ≡ (fst p ↓ n, snd p ↓ n)›

instance by intro_classes (simp add: restriction_prod_def)

end



instance prod :: (restriction_space, restriction_space) restriction_space
proof intro_classes
  show ‹p ↓ 0 = q ↓ 0› for p q :: ‹'a × 'b›
    by (simp add: restriction_prod_def)
next
  show ‹p ≠ q ⟹ ∃n. p ↓ n ≠ q ↓ n› for p q :: ‹'a × 'b›
    by (simp add: restriction_prod_def)
      (meson ex_not_restriction_related prod.expand)
qed



instantiation prod :: (preorder_restriction_space, preorder_restriction_space) preorder_restriction_space
begin

text ‹
We might want to use lexicographic order :
  ▪ \<^term>‹p ≤ q ≡ fst p < fst q ∨ fst p = fst q ∧ snd p ≤ snd q›
  ▪ \<^term>‹p < q ≡ fst p < fst q ∨ (fst p = fst q ∧ snd p < snd q)›

but this is wrong since it is incompatible with \<^term>‹p ↓ 0 ≤ q ↓ 0›,
\<^term>‹¬ p ≤ q ⟹ ∃n. ¬ p ↓ n ≤ q ↓ n› and \<^term>‹p ≤ q ⟹ p ↓ n ≤ q ↓ n›.›

definition less_eq_prod :: ‹'a × 'b ⇒ 'a × 'b ⇒ bool›
  where ‹p ≤ q ≡ fst p ≤ fst q ∧ snd p ≤ snd q›

definition less_prod :: ‹'a × 'b ⇒ 'a × 'b ⇒ bool›
  where ‹p < q ≡ fst p ≤ fst q ∧ snd p < snd q ∨ fst p < fst q ∧ snd p ≤ snd q›

instance
proof intro_classes
  show ‹p < q ⟷ p ≤ q ∧ ¬ q ≤ p› for p q :: ‹'a × 'b›
    by (auto simp add: less_eq_prod_def less_prod_def less_le_not_le)
next
  show ‹p ≤ p› for p :: ‹'a × 'b›
    by (simp add: less_eq_prod_def)
next
  show ‹p ≤ q ⟹ q ≤ r ⟹ p ≤ r› for p q r :: ‹'a × 'b›
    by (auto simp add: less_eq_prod_def intro: order_trans)
next
  show ‹p ↓ 0 ≤ q ↓ 0› for p q :: ‹'a × 'b›
    by (simp add: less_eq_prod_def restriction_prod_def)
next
  show ‹p ≤ q ⟹ p ↓ n ≤ q ↓ n› for p q :: ‹'a × 'b› and n
    by (simp add: less_eq_prod_def restriction_prod_def mono_restriction_less_eq)
next
  show ‹¬ p ≤ q ⟹ ∃n. ¬ p ↓ n ≤ q ↓ n› for p q :: ‹'a × 'b›
    by (simp add: less_eq_prod_def restriction_prod_def)
      (meson ex_not_restriction_less_eq)
qed

end


instance prod :: (order_restriction_space, order_restriction_space) order_restriction_space
  by intro_classes (simp add: less_eq_prod_def order_antisym prod.expand)



subsection ‹Restriction shift Maps›

subsubsection ‹Domain is a Product›

lemma restriction_shift_on_prod_domain_iff : 
  ‹restriction_shift_on f k (A × B) ⟷ (∀x∈A. restriction_shift_on (λy. f (x, y)) k B) ∧
                                         (∀y∈B. restriction_shift_on (λx. f (x, y)) k A)›
proof (intro iffI conjI ballI)
  show ‹restriction_shift_on (λy. f (x, y)) k B›
    if ‹restriction_shift_on f k (A × B)› and ‹x ∈ A› for x
  proof (rule restriction_shift_onI)
    show ‹y1 ∈ B ⟹ y2 ∈ B ⟹ y1 ↓ n = y2 ↓ n ⟹
          f (x, y1) ↓ nat (int n + k) = f (x, y2) ↓ nat (int n + k)› for y1 y2 n
      by (rule that(1)[THEN restriction_shift_onD])
        (use that(2) in ‹simp_all add: restriction_prod_def›)
  qed
next
  show ‹restriction_shift_on (λx. f (x, y)) k A›
    if ‹restriction_shift_on f k (A × B)› and ‹y ∈ B› for y
  proof (rule restriction_shift_onI)
    show ‹x1 ∈ A ⟹ x2 ∈ A ⟹ x1 ↓ n = x2 ↓ n ⟹
          f (x1, y) ↓ nat (int n + k) = f (x2, y) ↓ nat (int n + k)› for x1 x2 n
      by (rule that(1)[THEN restriction_shift_onD])
        (use that(2) in ‹simp_all add: restriction_prod_def›)
  qed
next
  assume assm : ‹(∀x∈A. restriction_shift_on (λy. f (x, y)) k B) ∧
                 (∀y∈B. restriction_shift_on (λx. f (x, y)) k A)›
  show ‹restriction_shift_on f k (A × B)›
  proof (rule restriction_shift_onI)
    fix p q n assume ‹p ∈ A × B› ‹q ∈ A × B› ‹p ↓ n = q ↓ n›
    then obtain x1 y1 x2 y2
      where ‹p = (x1, y1)› ‹q = (x2, y2)› ‹x1 ∈ A› ‹y1 ∈ B›
        ‹x2 ∈ A› ‹y2 ∈ B› ‹x1 ↓ n = x2 ↓ n› ‹y1 ↓ n = y2 ↓ n›
      by (cases p, cases q, simp add: restriction_prod_def)
    have ‹p = (x1, y1)› by (fact ‹p = (x1, y1)›)
    also have ‹f (x1, y1) ↓ nat (int n + k) = f (x1, y2) ↓ nat (int n + k)›
      by (rule assm[THEN conjunct1, rule_format, OF ‹x1 ∈ A›, THEN restriction_shift_onD])
        (fact ‹y1 ∈ B› ‹y2 ∈ B› ‹y1 ↓ n = y2 ↓ n›)+
    also have ‹f (x1, y2) ↓ nat (int n + k) = f (x2, y2) ↓ nat (int n + k)›
      by (rule assm[THEN conjunct2, rule_format, OF ‹y2 ∈ B›, THEN restriction_shift_onD])
        (fact ‹x1 ∈ A› ‹x2 ∈ A› ‹x1 ↓ n = x2 ↓ n›)+
    also have ‹(x2, y2) = q› by (simp add: ‹q = (x2, y2)›)
    finally show ‹f p ↓ nat (int n + k) = f q ↓ nat (int n + k)› .
  qed
qed

lemma restriction_shift_prod_domain_iff:
  ‹restriction_shift f k ⟷ (∀x. restriction_shift (λy. f (x, y)) k) ∧
                             (∀y. restriction_shift (λx. f (x, y)) k)›
  unfolding restriction_shift_def
  by (metis UNIV_I UNIV_Times_UNIV restriction_shift_on_prod_domain_iff)


lemma non_too_destructive_on_prod_domain_iff :
  ‹non_too_destructive_on f (A × B) ⟷ (∀x∈A. non_too_destructive_on (λy. f (x, y)) B) ∧
                                        (∀y∈B. non_too_destructive_on (λx. f (x, y)) A)›
  by (simp add: non_too_destructive_on_def restriction_shift_on_prod_domain_iff)

lemma non_too_destructive_prod_domain_iff :
  ‹non_too_destructive f ⟷ (∀x. non_too_destructive (λy. f (x, y))) ∧
                             (∀y. non_too_destructive (λx. f (x, y)))›
  unfolding non_too_destructive_def
  by (metis UNIV_I UNIV_Times_UNIV non_too_destructive_on_prod_domain_iff)


lemma non_destructive_on_prod_domain_iff :
  ‹non_destructive_on f (A × B) ⟷ (∀x∈A. non_destructive_on (λy. f (x, y)) B) ∧
                                    (∀y∈B. non_destructive_on (λx. f (x, y)) A)›
  by (simp add: non_destructive_on_def restriction_shift_on_prod_domain_iff)

lemma non_destructive_prod_domain_iff :
  ‹non_destructive f ⟷ (∀x. non_destructive (λy. f (x, y))) ∧
                         (∀y. non_destructive (λx. f (x, y)))›
  unfolding non_destructive_def
  by (metis UNIV_I UNIV_Times_UNIV non_destructive_on_prod_domain_iff)


lemma constructive_on_prod_domain_iff :
  ‹constructive_on f (A × B) ⟷ (∀x∈A. constructive_on (λy. f (x, y)) B) ∧
                                 (∀y∈B. constructive_on (λx. f (x, y)) A)›
  by (simp add: constructive_on_def restriction_shift_on_prod_domain_iff)

lemma constructive_prod_domain_iff :
  ‹constructive f ⟷ (∀x. constructive (λy. f (x, y))) ∧
                      (∀y. constructive (λx. f (x, y)))›
  unfolding constructive_def
  by (metis UNIV_I UNIV_Times_UNIV constructive_on_prod_domain_iff)



lemma restriction_shift_prod_domain [restriction_shift_simpset, restriction_shift_introset] :
  ‹⟦⋀x. restriction_shift (λy. f (x, y)) k;
    ⋀y. restriction_shift (λx. f (x, y)) k⟧ ⟹ restriction_shift f k›
  and non_too_destructive_prod_domain [restriction_shift_simpset, restriction_shift_introset] :
  ‹⟦⋀x. non_too_destructive (λy. f (x, y));
    ⋀y. non_too_destructive (λx. f (x, y))⟧ ⟹ non_too_destructive f›
  and non_destructive_prod_domain [restriction_shift_simpset, restriction_shift_introset] :
  ‹⟦⋀x. non_destructive (λy. f (x, y));
    ⋀y. non_destructive (λx. f (x, y))⟧ ⟹ non_destructive f›
  and constructive_prod_domain [restriction_shift_simpset, restriction_shift_introset] :
  ‹⟦⋀x. constructive (λy. f (x, y));
    ⋀y. constructive (λx. f (x, y))⟧ ⟹ constructive f›
  by (simp_all add: restriction_shift_prod_domain_iff non_too_destructive_prod_domain_iff
      non_destructive_prod_domain_iff constructive_prod_domain_iff)



subsubsection ‹Codomain is a Product›

lemma restriction_shift_on_prod_codomain_iff : 
  ‹restriction_shift_on f k A ⟷ (restriction_shift_on (λx. fst (f x)) k A) ∧
                                  (restriction_shift_on (λx. snd (f x)) k A)›
  by (simp add: restriction_shift_on_def restriction_prod_def) blast


lemma restriction_shift_prod_codomain_iff:
  ‹restriction_shift f k ⟷ (restriction_shift (λx. fst (f x)) k) ∧
                             (restriction_shift (λx. snd (f x)) k)›
  unfolding restriction_shift_def
  by (fact restriction_shift_on_prod_codomain_iff)


lemma non_too_destructive_on_prod_codomain_iff :
  ‹non_too_destructive_on f A ⟷ (non_too_destructive_on (λx. fst (f x)) A) ∧
                                  (non_too_destructive_on (λx. snd (f x)) A)›
  by (simp add: non_too_destructive_on_def restriction_shift_on_prod_codomain_iff)

lemma non_too_destructive_prod_codomain_iff :
  ‹non_too_destructive f ⟷ (non_too_destructive (λx. fst (f x))) ∧
                             (non_too_destructive (λx. snd (f x)))›
  by (simp add: non_too_destructive_def non_too_destructive_on_prod_codomain_iff)


lemma non_destructive_on_prod_codomain_iff :
  ‹non_destructive_on f A ⟷ (non_destructive_on (λx. fst (f x)) A) ∧
                              (non_destructive_on (λx. snd (f x)) A)›

  by (simp add: non_destructive_on_def restriction_shift_on_prod_codomain_iff)

lemma non_destructive_prod_codomain_iff :
  ‹non_destructive f ⟷ (non_destructive (λx. fst (f x))) ∧
                         (non_destructive (λx. snd (f x)))›
  by (simp add: non_destructive_def non_destructive_on_prod_codomain_iff)


lemma constructive_on_prod_codomain_iff :
  ‹constructive_on f A ⟷ (constructive_on (λx. fst (f x)) A) ∧
                           (constructive_on (λx. snd (f x)) A)›
  by (simp add: constructive_on_def restriction_shift_on_prod_codomain_iff)

lemma constructive_prod_codomain_iff :
  ‹constructive f ⟷ (constructive (λx. fst (f x))) ∧
                      (constructive (λx. snd (f x)))›
  by (simp add: constructive_def constructive_on_prod_codomain_iff)


lemma restriction_shift_prod_codomain [restriction_shift_simpset, restriction_shift_introset] :
  ‹⟦restriction_shift f k; restriction_shift g k⟧ ⟹
   restriction_shift (λx. (f x, g x)) k›
  and non_too_destructive_prod_codomain [restriction_shift_simpset, restriction_shift_introset] :
  ‹⟦non_too_destructive f; non_too_destructive g⟧ ⟹ non_too_destructive (λx. (f x, g x))›
  and non_destructive_prod_codomain [restriction_shift_simpset, restriction_shift_introset] :
  ‹⟦non_destructive f; non_destructive g⟧ ⟹ non_destructive (λx. (f x, g x))›
  and constructive_prod_codomain [restriction_shift_simpset, restriction_shift_introset] :
  ‹⟦constructive f; constructive g⟧ ⟹ constructive (λx. (f x, g x))›
  by (simp_all add: restriction_shift_prod_codomain_iff non_too_destructive_prod_codomain_iff
      non_destructive_prod_codomain_iff constructive_prod_codomain_iff)



subsection ‹Limits and Convergence›

lemma restriction_chain_prod_iff :
  ‹restriction_chain σ ⟷ restriction_chain (λn. fst (σ n)) ∧
                           restriction_chain (λn. snd (σ n))›
  by (simp add: restriction_chain_def restriction_prod_def)
    (metis fst_conv prod.collapse snd_conv)

lemma restriction_tendsto_prod_iff :
  ‹σ ─↓→ Σ ⟷ (λn. fst (σ n)) ─↓→ fst Σ ∧ (λn. snd (σ n)) ─↓→ snd Σ›
  by (simp add: restriction_tendsto_def restriction_prod_def)
    (meson nle_le order_trans)

lemma restriction_convergent_prod_iff :
  ‹restriction_convergent σ ⟷ restriction_convergent (λn. fst (σ n)) ∧
                                restriction_convergent (λn. snd (σ n))›
  by (simp add: restriction_convergent_def restriction_tendsto_prod_iff)

lemma funpow_indep_prod_is :
  ‹((λ(x, y). (f x, g y)) ^^ n) (x, y) = ((f ^^ n) x, (g ^^ n) y)›
  for f g :: ‹'a ⇒ 'a›
  by (induct n) simp_all



subsection ‹Completeness›

instance prod :: (complete_restriction_space, complete_restriction_space) complete_restriction_space
proof intro_classes
  fix σ :: ‹nat ⇒ 'a :: complete_restriction_space × 'b :: complete_restriction_space›
  assume ‹chain⇩↓ σ›
  hence ‹chain⇩↓ (λn. fst (σ n))› ‹chain⇩↓ (λn. snd (σ n))›
    by (simp_all add: restriction_chain_prod_iff)
  hence ‹convergent⇩↓ (λn. fst (σ n))› ‹convergent⇩↓ (λn. snd (σ n))›
    by (simp_all add: restriction_chain_imp_restriction_convergent)
  thus ‹convergent⇩↓ σ›
    by (simp add: restriction_convergent_prod_iff)
qed    



subsection ‹Fixed Point›

lemma restriction_fix_indep_prod_is :
  ‹(υ (x, y). (f x, g y)) = (υ x. f x, υ y. g y)›
  if contructive : ‹constructive f› ‹constructive g›
  for f :: ‹'a ⇒ 'a :: complete_restriction_space›
    and g :: ‹'b ⇒ 'b :: complete_restriction_space›
proof (rule restriction_fix_unique)
  from contructive show ‹constructive (λ(x, y). (f x, g y))›
    by (simp add: constructive_prod_domain_iff constructive_prod_codomain_iff constructive_const)
next
  show ‹(case (υ x. f x, υ y. g y) of (x, y) ⇒ (f x, g y)) = (υ x. f x, υ y. g y)›
    by simp (metis restriction_fix_eq contructive)
qed



lemma non_destructive_fst : ‹non_destructive fst›
  by (rule non_destructiveI) (simp add: restriction_prod_def)

lemma non_destructive_snd : ‹non_destructive snd›
  by (rule non_destructiveI) (simp add: restriction_prod_def)




lemma constructive_restriction_fix_right :
  ‹constructive (λx. υ y. f (x, y))› if ‹constructive f›
for f :: ‹'a :: complete_restriction_space × 'b :: complete_restriction_space ⇒ 'b›
proof (rule constructiveI)
  fix n and x x' :: 'a assume ‹x ↓ n = x' ↓ n›
  show ‹(υ y. f (x, y)) ↓ Suc n = (υ y. f (x', y)) ↓ Suc n›
  proof (subst (1 2) restriction_restriction_fix_is)
    show ‹constructive (λy. f (x', y))› and ‹constructive (λy. f (x, y))›
      using ‹constructive f› constructive_prod_domain_iff by blast+
  next
    from ‹x ↓ n = x' ↓ n› show ‹((λy. f (x, y)) ^^ Suc n) undefined ↓ Suc n =
                                ((λy. f (x', y)) ^^ Suc n) undefined ↓ Suc n›
      by (induct n, simp_all)
        (use ‹constructive f› constructiveD restriction_0_related in blast,
          metis (no_types, lifting) ‹constructive f› constructiveD prod.sel
          restriction_related_pred restriction_prod_def)
  qed
qed


lemma constructive_restriction_fix_left :
  ‹constructive (λy. υ x. f (x, y))› if ‹constructive f›
for f :: ‹'a :: complete_restriction_space × 'b :: complete_restriction_space ⇒ 'a›
proof (rule constructiveI)
  fix n and y y' :: 'b assume ‹y ↓ n = y' ↓ n›
  show ‹(υ x. f (x, y)) ↓ Suc n = (υ x. f (x, y')) ↓ Suc n›
  proof (subst (1 2) restriction_restriction_fix_is)
    show ‹constructive (λx. f (x, y'))› and ‹constructive (λx. f (x, y))›
      using ‹constructive f› constructive_prod_domain_iff by blast+
  next
    from ‹y ↓ n = y' ↓ n› show ‹((λx. f (x, y)) ^^ Suc n) undefined ↓ Suc n =
                                ((λx. f (x, y')) ^^ Suc n) undefined ↓ Suc n›
      by (induct n, simp_all)
        (use restriction_0_related ‹constructive f› constructiveD in blast,
          metis (no_types, lifting) ‹constructive f› constructiveD prod.sel
          restriction_related_pred restriction_prod_def)
  qed
qed



― ‹``Bekic's Theorem'' in HOLCF›

lemma restriction_fix_prod_is :
  ‹(υ p. f p) = (υ x. fst (f (x, υ y. snd (f (x, y)))),
                 υ y. snd (f (υ x. fst (f (x, υ y. snd (f (x, y)))), y)))›
  (is ‹(υ p. f p) = (?x, ?y)›) if ‹constructive f›
for f :: ‹'a :: complete_restriction_space × 'b :: complete_restriction_space ⇒ 'a × 'b›
proof (rule restriction_fix_unique[OF ‹constructive f›])
  have ‹constructive (λp. snd (f p))›
    by (fact non_destructive_comp_constructive[OF non_destructive_snd ‹constructive f›])
  hence ‹constructive (λx. υ y. snd (f (x, y)))›
    by (fact constructive_restriction_fix_right)
  hence ‹non_destructive (λx. υ y. snd (f (x, y)))›
    by (fact constructive_imp_non_destructive)
  hence ‹non_destructive (λx. (x, υ y. snd (f (x, y))))›
    by (fact non_destructive_prod_codomain[OF non_destructive_id(2)])
  hence ‹constructive (λx. f (x, υ y. snd (f (x, y))))›
    by (fact constructive_comp_non_destructive[OF ‹constructive f›])
  hence * : ‹constructive (λx. fst (f (x, υ y. snd (f (x, y)))))›
    by (fact non_destructive_comp_constructive[OF non_destructive_fst])

  have ‹non_destructive (λx. υ x. fst (f (x, υ y. snd (f (x, y)))))›
    by (fact constructive_imp_non_destructive[OF constructive_const])
  hence ‹non_destructive (Pair (υ x. fst (f (x, υ y. snd (f (x, y))))))›
    by (fact non_destructive_prod_codomain[OF _ non_destructive_id(2)])
  hence ‹constructive (λx. f (υ x. fst (f (x, υ y. snd (f (x, y)))), x))›
    by (fact constructive_comp_non_destructive[OF ‹constructive f›])
  hence ** : ‹constructive (λx. snd (f (υ x. fst (f (x, υ y. snd (f (x, y)))), x)))›
    by (fact non_destructive_comp_constructive[OF non_destructive_snd])

  have ‹fst (f (?x, ?y)) = ?x›
    by (rule trans [symmetric, OF restriction_fix_eq[OF "*"]]) simp
  moreover have ‹snd (f (?x, ?y)) = ?y›
    by (rule trans [symmetric, OF restriction_fix_eq[OF "**"]]) simp
  ultimately show ‹f (?x, ?y) = (?x, ?y)› by (cases ‹f (?x, ?y)›) simp
qed 


(*<*)
end
  (*>*)