Theory Restriction_Spaces_Locales

(***********************************************************************************
 * 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 ‹Locales factorizing the proof Work›

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

named_theorems restriction_shift_simpset
named_theorems restriction_shift_introset ― ‹Useful for future automation.›


text ‹In order to factorize the proof work, we first work with locales and then with classes.›


subsection ‹Basic Notions for Restriction›

locale Restriction =
  fixes restriction :: ‹['a, nat] ⇒ 'a›  (infixl ‹↓› 60)
    and relation    :: ‹['a, 'a] ⇒ bool› (infixl ‹⪅› 50)
  assumes restriction_restriction [simp] : ‹x ↓ n ↓ m = x ↓ min n m›
begin


abbreviation restriction_related_set  :: ‹'a ⇒ 'a ⇒ nat set›
  where ‹restriction_related_set x y  ≡ {n. x ↓ n ⪅ y ↓ n}›

abbreviation restriction_not_related_set :: ‹'a ⇒ 'a ⇒ nat set›
  where ‹restriction_not_related_set x y ≡ {n. ¬ x ↓ n ⪅ y ↓ n}›

lemma restriction_related_set_Un_restriction_not_related_set :
  ‹restriction_related_set x y ∪ restriction_not_related_set x y = UNIV› by blast

lemma disjoint_restriction_related_set_restriction_not_related_set :
  ‹restriction_related_set x y ∩ restriction_not_related_set x y = {}› by blast

lemma ‹bdd_below (restriction_related_set x y)› by (fact bdd_below_bot)

lemma ‹bdd_below (restriction_not_related_set x y)› by (fact bdd_below_bot)


end


locale PreorderRestrictionSpace = Restriction +
  assumes restriction_0_related   [simp] : ‹x ↓ 0 ⪅ y ↓ 0›
    and mono_restriction_related   : ‹  x ⪅ y ⟹ x ↓ n ⪅ y ↓ n›
    and ex_not_restriction_related : ‹¬ x ⪅ y ⟹ ∃n. ¬ x ↓ n ⪅ y ↓ n›
    and related_trans : ‹x ⪅ y ⟹ y ⪅ z ⟹ x ⪅ z›
begin

lemma exists_restriction_related [simp] : ‹∃n. x ↓ n ⪅ y ↓ n›
  using restriction_0_related by blast

lemma all_restriction_related_iff_related : ‹(∀n. x ↓ n ⪅ y ↓ n) ⟷ x ⪅ y›
  using mono_restriction_related ex_not_restriction_related by blast

lemma restriction_related_le : ‹x ↓ n ⪅ y ↓ n› if ‹n ≤ m› and ‹x ↓ m ⪅ y ↓ m›
proof -
  from mono_restriction_related[OF ‹x ↓ m ⪅ y ↓ m›] have ‹x ↓ m ↓ n ⪅ y ↓ m ↓ n› .
  also have ‹(λx. x ↓ m ↓ n) = (λx. x ↓ n)› by (simp add: ‹n ≤ m›)
  finally show ‹x ↓ n ⪅ y ↓ n› .
qed

corollary restriction_related_pred : ‹x ↓ Suc n ⪅ y ↓ Suc n ⟹ x ↓ n ⪅ y ↓ n›
  by (metis le_add2 plus_1_eq_Suc restriction_related_le)

lemma all_ge_restriction_related_iff_related : ‹(∀n≥m. x ↓ n ⪅ y ↓ n) ⟷ x ⪅ y›
  by (metis all_restriction_related_iff_related nle_le restriction_related_le)


lemma take_lemma_restriction : ‹x ⪅ y›
  if ‹⋀n. ⟦⋀k. k ≤ n ⟹ x ↓ k ⪅ y ↓ k⟧ ⟹ x ↓ Suc n ⪅ y ↓ Suc n›
proof (subst all_restriction_related_iff_related[symmetric], intro allI)
  show ‹x ↓ n ⪅ y ↓ n› for n
    by (induct n rule: full_nat_induct)
      (metis not_less_eq_eq restriction_0_related restriction_related_le that zero_induct)
qed

lemma ex_not_restriction_related_optimized :
  ‹∃!n. ¬ x ↓ Suc n ⪅ y ↓ Suc n ∧ (∀m≤n. x ↓ m ⪅ y ↓ m)› if ‹¬ x ⪅ y›
proof (rule ex1I)
  let ?S = ‹{n. ¬ x ↓ Suc n ⪅ y ↓ Suc n ∧ (∀m≤n. x ↓ m ⪅ y ↓ m)}›
  let ?n = ‹Inf {n. ¬ x ↓ Suc n ⪅ y ↓ Suc n ∧ (∀m≤n. x ↓ m ⪅ y ↓ m)}›
  from restriction_related_le[of _ _ x y] take_lemma_restriction[of x y] ‹¬ x ⪅ y›
  have ‹?S ≠ {}› by auto
  from Inf_nat_def1[OF this] have ‹?n ∈ ?S› .
  thus ‹¬ x ↓ Suc ?n ⪅ y ↓ Suc ?n ∧ (∀m≤?n. x ↓ m ⪅ y ↓ m)› by blast
  thus ‹¬ x ↓ Suc n ⪅ y ↓ Suc n ∧ (∀m≤n. x ↓ m ⪅ y ↓ m) ⟹ n = ?n› for n
    by (meson not_less_eq_eq order_antisym_conv)
qed




lemma nonempty_restriction_related_set : ‹restriction_related_set x y ≠ {}›
  using restriction_0_related by blast

lemma non_UNIV_restriction_not_related_set : ‹restriction_not_related_set x y ≠ UNIV›
  using restriction_0_related by blast

lemma UNIV_restriction_related_set_iff : ‹restriction_related_set x y = UNIV ⟷ x ⪅ y›
  using all_restriction_related_iff_related by blast

lemma empty_restriction_not_related_set_iff: ‹restriction_not_related_set x y = {} ⟷ x ⪅ y›
  by (simp add: all_restriction_related_iff_related)


lemma finite_restriction_related_set_iff :
  ‹finite (restriction_related_set x y) ⟷ ¬ x ⪅ y›
proof (rule iffI)
  assume ‹finite (restriction_related_set x y)›
  obtain n where ‹¬ x ↓ n ⪅ y ↓ n› 
    using ‹finite (restriction_related_set x y)› by fastforce
  with mono_restriction_related show ‹¬ x ⪅ y› by blast
next
  assume ‹¬ x ⪅ y›
  then obtain n where ‹∀m>n. ¬ x ↓ m ⪅ y ↓ m›
    by (meson all_restriction_related_iff_related less_le_not_le restriction_related_le)
  hence ‹restriction_related_set x y ⊆ {0..n}›
    by (simp add: subset_iff) (meson linorder_not_le)
  thus ‹finite (restriction_related_set x y)›
    by (simp add: subset_eq_atLeast0_atMost_finite)
qed

lemma infinite_restriction_not_related_set_iff :
  ‹infinite (restriction_not_related_set x y) ⟷ ¬ x ⪅ y›
  by (metis empty_restriction_not_related_set_iff finite_restriction_related_set_iff
      finite.emptyI finite_Collect_not infinite_UNIV_char_0)

lemma bdd_above_restriction_related_set_iff :
  ‹bdd_above (restriction_related_set x y) ⟷ ¬ x ⪅ y›
  by (simp add: bdd_above_nat finite_restriction_related_set_iff)



context fixes x y assumes ‹¬ x ⪅ y› begin

lemma Sup_in_restriction_related_set :
  ‹Sup (restriction_related_set x y) ∈ restriction_related_set x y›
  using Max_in[OF finite_restriction_related_set_iff[THEN iffD2, OF ‹¬ x ⪅ y›]
      nonempty_restriction_related_set]
    cSup_eq_Max[OF finite_restriction_related_set_iff[THEN iffD2, OF ‹¬ x ⪅ y›]
      nonempty_restriction_related_set]
  by argo

lemma Inf_in_restriction_not_related_set :
  ‹Inf (restriction_not_related_set x y) ∈ restriction_not_related_set x y›
  by (metis ‹¬ x ⪅ y› Inf_nat_def1 finite.emptyI infinite_restriction_not_related_set_iff)

lemma Inf_restriction_not_related_set_eq_Suc_Sup_restriction_related_set :
  ‹Inf (restriction_not_related_set x y) = Suc (Sup (restriction_related_set x y))›
proof -
  let ?S_eq  = ‹restriction_related_set  x y›
  let ?S_neq = ‹restriction_not_related_set x y›
  from Inf_in_restriction_not_related_set have ‹Inf ?S_neq ∈ ?S_neq› by blast
  from Sup_in_restriction_related_set have ‹Sup ?S_eq ∈ ?S_eq› by blast
  hence ‹Suc (Sup ?S_eq) ∉ ?S_eq›
    by (metis Suc_n_not_le_n ‹¬ x ⪅ y› bdd_above_restriction_related_set_iff cSup_upper)
  with restriction_related_set_Un_restriction_not_related_set
  have ‹Suc (Sup ?S_eq) ∈ ?S_neq› by auto
  show ‹Inf ?S_neq = Suc (Sup ?S_eq)›
  proof (rule order_antisym)
    show ‹Inf ?S_neq ≤ Suc (Sup ?S_eq)›
      by (fact wellorder_Inf_le1[OF ‹Suc (Sup ?S_eq) ∈ ?S_neq›])
  next
    from ‹Inf ?S_neq ∈ ?S_neq› ‹Sup ?S_eq ∈ ?S_eq› show ‹Suc (Sup ?S_eq) ≤ Inf ?S_neq›
      by (metis (mono_tags, lifting) mem_Collect_eq not_less_eq_eq restriction_related_le)
  qed
qed

end


lemma restriction_related_set_is_atMost :
  ‹restriction_related_set x y =
   (if x ⪅ y then UNIV else {..Sup (restriction_related_set x y)})›
proof (split if_split, intro conjI impI)
  show ‹x ⪅ y ⟹ restriction_related_set x y = UNIV› 
    by (simp add: UNIV_restriction_related_set_iff)
next
  assume ‹¬ x ⪅ y›
  hence * : ‹Sup (restriction_related_set x y) ∈ restriction_related_set x y›
    by (fact Sup_in_restriction_related_set)
  show ‹restriction_related_set x y = {..Sup (restriction_related_set x y)} ›
  proof (intro subset_antisym subsetI)
    show ‹n ∈ restriction_related_set x y ⟹ n ∈ {..Sup (restriction_related_set x y)}› for n
      by (simp add: ‹¬ x ⪅ y› finite_restriction_related_set_iff le_cSup_finite)
  next
    from "*" show ‹n ∈ {..Sup (restriction_related_set x y)} ⟹
                   n ∈ restriction_related_set x y› for n
      by simp (meson mem_Collect_eq restriction_related_le)
  qed
qed

lemma restriction_not_related_set_is_atLeast :
  ‹restriction_not_related_set x y =
   (if x ⪅ y then {} else {Inf (restriction_not_related_set x y)..})›
proof (split if_split, intro conjI impI)
  from empty_restriction_not_related_set_iff
  show ‹x ⪅ y ⟹ restriction_not_related_set x y = {}› by blast
next
  assume ‹¬ x ⪅ y›
  have ‹restriction_not_related_set x y = UNIV - restriction_related_set x y› by auto
  also have ‹… = UNIV - {..Sup (restriction_related_set x y)}›
    by (subst restriction_related_set_is_atMost) (simp add: ‹¬ x ⪅ y›)
  also have ‹… = {Suc (Sup (restriction_related_set x y))..}› by auto
  also have ‹Suc (Sup (restriction_related_set x y)) = Inf (restriction_not_related_set x y)›
    by (simp add: ‹¬ x ⪅ y› flip: Inf_restriction_not_related_set_eq_Suc_Sup_restriction_related_set)
  finally show ‹restriction_not_related_set x y = {Inf (restriction_not_related_set x y)..}› .
qed


end




subsection ‹Restriction shift Maps›

locale Restriction_2_PreorderRestrictionSpace =
  R1 : Restriction ‹(↓⇩1)› ‹(⪅⇩1)› +
  PRS2 : PreorderRestrictionSpace ‹(↓⇩2)› ‹(⪅⇩2)›
  for restriction⇩1 :: ‹'a ⇒ nat ⇒ 'a›  (infixl ‹↓⇩1› 60)
    and relation⇩1    :: ‹'a ⇒ 'a ⇒ bool› (infixl ‹⪅⇩1› 50)
    and restriction⇩2 :: ‹'b ⇒ nat ⇒ 'b›  (infixl ‹↓⇩2› 60)
    and relation⇩2    :: ‹'b ⇒ 'b ⇒ bool› (infixl ‹⪅⇩2› 50)
begin

subsubsection ‹Definition›

text ‹This notion is a generalization of constructive map and non-destructive map.›

definition restriction_shift_on :: ‹['a ⇒ 'b, int, 'a set] ⇒ bool›
  where ‹restriction_shift_on f k A ≡
         ∀x∈A. ∀y∈A. ∀n. x ↓⇩1 n ⪅⇩1 y ↓⇩1 n ⟶ f x ↓⇩2 nat (int n + k) ⪅⇩2 f y ↓⇩2 nat (int n + k)›

definition restriction_shift :: ‹['a ⇒ 'b, int] ⇒ bool›
  where ‹restriction_shift f k ≡ restriction_shift_on f k UNIV›


lemma restriction_shift_onI :
  ‹(⋀x y n. ⟦x ∈ A; y ∈ A; ¬ f x ⪅⇩2 f y; x ↓⇩1 n ⪅⇩1 y ↓⇩1 n⟧ ⟹
             f x ↓⇩2 nat (int n + k) ⪅⇩2 f y ↓⇩2 nat (int n + k))
   ⟹ restriction_shift_on f k A›
  unfolding restriction_shift_on_def
  by (metis PRS2.all_restriction_related_iff_related)

corollary restriction_shiftI :
  ‹(⋀x y n. ⟦¬ f x ⪅⇩2 f y; x ↓⇩1 n ⪅⇩1 y ↓⇩1 n⟧ ⟹
             f x ↓⇩2 nat (int n + k) ⪅⇩2 f y ↓⇩2 nat (int n + k))
   ⟹ restriction_shift f k›
  by (unfold restriction_shift_def, rule restriction_shift_onI)



lemma restriction_shift_onD :
  ‹⟦restriction_shift_on f k A; x ∈ A; y ∈ A; x ↓⇩1 n ⪅⇩1 y ↓⇩1 n⟧
   ⟹ f x ↓⇩2 nat (int n + k) ⪅⇩2 f y ↓⇩2 nat (int n + k)›
  by (unfold restriction_shift_on_def) blast

lemma restriction_shiftD :
  ‹⟦restriction_shift f k; x ↓⇩1 n ⪅⇩1 y ↓⇩1 n⟧ ⟹ f x ↓⇩2 nat (int n + k) ⪅⇩2 f y ↓⇩2 nat (int n + k)›
  unfolding restriction_shift_def using restriction_shift_onD by blast

lemma restriction_shift_on_subset :
  ‹restriction_shift_on f k B ⟹ A ⊆ B ⟹ restriction_shift_on f k A›
  by (simp add: restriction_shift_on_def subset_iff)

lemma restriction_shift_imp_restriction_shift_on [restriction_shift_simpset] :
  ‹restriction_shift f k ⟹ restriction_shift_on f k A›
  unfolding restriction_shift_def using restriction_shift_on_subset by blast


lemma restriction_shift_on_imp_restriction_shift_on_le [restriction_shift_simpset] :
  ‹restriction_shift_on f l A› if ‹l ≤ k› and ‹restriction_shift_on f k A›
proof (rule restriction_shift_onI)
  fix x y n assume ‹x ∈ A› ‹y ∈ A› ‹x ↓⇩1 n ⪅⇩1 y ↓⇩1 n›
  from ‹restriction_shift_on f k A›[THEN restriction_shift_onD, OF this]
  have ‹f x ↓⇩2 nat (int n + k) ⪅⇩2 f y ↓⇩2 nat (int n + k)› .
  moreover have ‹nat (int n + l) ≤ nat (int n + k)› by (simp add: nat_mono ‹l ≤ k›)
  ultimately show ‹f x ↓⇩2 nat (int n + l) ⪅⇩2 f y ↓⇩2 nat (int n + l)›
    using PRS2.restriction_related_le by blast
qed

corollary restriction_shift_imp_restriction_shift_le [restriction_shift_simpset] :
  ‹l ≤ k ⟹ restriction_shift f k ⟹ restriction_shift f l›
  unfolding restriction_shift_def
  by (fact restriction_shift_on_imp_restriction_shift_on_le)



lemma restriction_shift_on_if_then_else [restriction_shift_simpset, restriction_shift_introset] :
  ‹⟦⋀x. P x ⟹ restriction_shift_on (f x) k A;
    ⋀x. ¬ P x ⟹ restriction_shift_on (g x) k A⟧ ⟹
    restriction_shift_on (λy. if P x then f x y else g x y) k A›
  by (rule restriction_shift_onI) (auto dest: restriction_shift_onD)

corollary restriction_shift_if_then_else [restriction_shift_simpset, restriction_shift_introset] :
  ‹⟦⋀x. P x ⟹ restriction_shift (f x) k;
    ⋀x. ¬ P x ⟹ restriction_shift (g x) k⟧ ⟹
    restriction_shift (λy. if P x then f x y else g x y) k›
  unfolding restriction_shift_def by (fact restriction_shift_on_if_then_else)



subsubsection ‹Three particular Cases›

text ‹The shift is most often equal to \<^term>‹0 :: int›, \<^term>‹1 :: int› or \<^term>‹- 1 :: int›.
      We provide extra support in these three cases.›

paragraph ‹Non-too-destructive Map›

definition non_too_destructive_on :: ‹['a ⇒ 'b, 'a set] ⇒ bool›
  where ‹non_too_destructive_on f A ≡ restriction_shift_on f (- 1) A›

definition non_too_destructive :: ‹['a ⇒ 'b] ⇒ bool›
  where ‹non_too_destructive f ≡ non_too_destructive_on f UNIV›


lemma non_too_destructive_onI :
  ‹non_too_destructive_on f A›
  if ‹⋀n x y. ⟦x ∈ A; y ∈ A; ¬ f x ⪅⇩2 f y; x ↓⇩1 Suc n ⪅⇩1 y ↓⇩1 Suc n⟧ ⟹ f x ↓⇩2 n ⪅⇩2 f y ↓⇩2 n›
proof (unfold non_too_destructive_on_def, rule restriction_shift_onI)
  fix x y n
  show ‹⟦x ∈ A; y ∈ A; ¬ f x ⪅⇩2 f y; x ↓⇩1 n ⪅⇩1 y ↓⇩1 n⟧
        ⟹ f x ↓⇩2 nat (int n + - 1) ⪅⇩2 f y ↓⇩2 nat (int n + - 1)›
    by (cases ‹n < 1›) (simp_all add: Suc_nat_eq_nat_zadd1 that)
qed

lemma non_too_destructiveI :
  ‹⟦⋀n x y. ⟦¬ f x ⪅⇩2 f y; x ↓⇩1 Suc n ⪅⇩1 y ↓⇩1 Suc n⟧ ⟹ f x ↓⇩2 n ⪅⇩2 f y ↓⇩2 n⟧
   ⟹ non_too_destructive f›
  by (unfold non_too_destructive_def, rule non_too_destructive_onI)

lemma non_too_destructive_onD :
  ‹⟦non_too_destructive_on f A; x ∈ A; y ∈ A; x ↓⇩1 Suc n ⪅⇩1 y ↓⇩1 Suc n⟧ ⟹ f x ↓⇩2 n ⪅⇩2 f y ↓⇩2 n›
  unfolding non_too_destructive_on_def using restriction_shift_onD by fastforce

lemma non_too_destructiveD :
  ‹⟦non_too_destructive f; x ↓⇩1 Suc n ⪅⇩1 y ↓⇩1 Suc n⟧ ⟹ f x ↓⇩2 n ⪅⇩2 f y ↓⇩2 n›
  unfolding non_too_destructive_def using non_too_destructive_onD by simp

lemma non_too_destructive_on_subset :
  ‹non_too_destructive_on f B ⟹ A ⊆ B ⟹ non_too_destructive_on f A›
  by (meson non_too_destructive_on_def restriction_shift_on_subset)

lemma non_too_destructive_imp_non_too_destructive_on [restriction_shift_simpset] :
  ‹non_too_destructive f ⟹ non_too_destructive_on f A›
  unfolding non_too_destructive_def using non_too_destructive_on_subset by auto


corollary non_too_destructive_on_if_then_else [restriction_shift_simpset, restriction_shift_introset]:
  ‹⟦⋀x. P x ⟹ non_too_destructive_on (f x) A; ⋀x. ¬ P x ⟹ non_too_destructive_on (g x) A⟧
     ⟹ non_too_destructive_on (λy. if P x then f x y else g x y) A›
  and non_too_destructive_if_then_else [restriction_shift_simpset, restriction_shift_introset] :
  ‹⟦⋀x. P x ⟹ non_too_destructive (f x); ⋀x. ¬ P x ⟹ non_too_destructive (g x)⟧
     ⟹ non_too_destructive (λy. if P x then f x y else g x y)›
  by (auto simp add: non_too_destructive_def non_too_destructive_on_def
      intro: restriction_shift_on_if_then_else)



paragraph ‹Non-destructive Map›

definition non_destructive_on :: ‹['a ⇒ 'b, 'a set] ⇒ bool›
  where ‹non_destructive_on f A ≡ restriction_shift_on f 0 A›

definition non_destructive :: ‹['a ⇒ 'b] ⇒ bool›
  where ‹non_destructive f ≡ non_destructive_on f UNIV›


lemma non_destructive_onI :
  ‹⟦⋀n x y. ⟦n ≠ 0; x ∈ A; y ∈ A; ¬ f x ⪅⇩2 f y; x ↓⇩1 n ⪅⇩1 y ↓⇩1 n⟧ ⟹ f x ↓⇩2 n ⪅⇩2 f y ↓⇩2 n⟧
   ⟹ non_destructive_on f A›
  by (unfold non_destructive_on_def, rule restriction_shift_onI)
    (metis PRS2.restriction_0_related add.right_neutral nat_int)

lemma non_destructiveI :
  ‹⟦⋀n x y. ⟦n ≠ 0; ¬ f x ⪅⇩2 f y; x ↓⇩1 n ⪅⇩1 y ↓⇩1 n⟧ ⟹ f x ↓⇩2 n ⪅⇩2 f y ↓⇩2 n⟧
   ⟹ non_destructive f› by (unfold non_destructive_def, rule non_destructive_onI)

lemma non_destructive_onD :
  ‹⟦non_destructive_on f A; x ∈ A; y ∈ A; ¬ f x ⪅⇩2 f y; x ↓⇩1 n ⪅⇩1 y ↓⇩1 n⟧ ⟹ f x ↓⇩2 n ⪅⇩2 f y ↓⇩2 n›
  by (simp add: non_destructive_on_def restriction_shift_on_def)

lemma non_destructiveD : ‹⟦non_destructive f; x ↓⇩1 n ⪅⇩1 y ↓⇩1 n⟧ ⟹ f x ↓⇩2 n ⪅⇩2 f y ↓⇩2 n›
  by (simp add: non_destructive_def non_destructive_on_def restriction_shift_on_def)

lemma non_destructive_on_subset :
  ‹non_destructive_on f B ⟹ A ⊆ B ⟹ non_destructive_on f A›
  by (meson non_destructive_on_def restriction_shift_on_subset)

lemma non_destructive_imp_non_destructive_on [restriction_shift_simpset] :
  ‹non_destructive f ⟹ non_destructive_on f A›
  unfolding non_destructive_def using non_destructive_on_subset by auto

lemma non_destructive_on_imp_non_too_destructive_on [restriction_shift_simpset] :
  ‹non_destructive_on f A ⟹ non_too_destructive_on f A›
  unfolding non_destructive_on_def non_too_destructive_on_def
  by (rule restriction_shift_on_imp_restriction_shift_on_le[of ‹- 1› 0 f A, simplified])

corollary non_destructive_imp_non_too_destructive [restriction_shift_simpset] :
  ‹non_destructive f ⟹ non_too_destructive f›
  by (unfold non_destructive_def non_too_destructive_def)
    (fact non_destructive_on_imp_non_too_destructive_on)


corollary non_destructive_on_if_then_else [restriction_shift_simpset, restriction_shift_introset] :
  ‹⟦⋀x. P x ⟹ non_destructive_on (f x) A; ⋀x. ¬ P x ⟹ non_destructive_on (g x) A⟧
     ⟹ non_destructive_on (λy. if P x then f x y else g x y) A›
  and non_destructive_if_then_else [restriction_shift_simpset, restriction_shift_introset] :
  ‹⟦⋀x. P x ⟹ non_destructive (f x); ⋀x. ¬ P x ⟹ non_destructive (g x)⟧
     ⟹ non_destructive (λy. if P x then f x y else g x y)›
  by (auto simp add: non_destructive_def non_destructive_on_def
      intro: restriction_shift_on_if_then_else)



paragraph ‹Constructive Map›

definition constructive_on :: ‹['a ⇒ 'b, 'a set] ⇒ bool›
  where ‹constructive_on f A ≡ restriction_shift_on f 1 A›

definition constructive :: ‹['a ⇒ 'b] ⇒ bool›
  where ‹constructive f ≡ constructive_on f UNIV›


lemma constructive_onI :
  ‹⟦⋀n x y. ⟦x ∈ A; y ∈ A; ¬ f x ⪅⇩2 f y; x ↓⇩1 n ⪅⇩1 y ↓⇩1 n⟧ ⟹ f x ↓⇩2 Suc n ⪅⇩2 f y ↓⇩2 Suc n⟧
   ⟹ constructive_on f A›
  by (simp add: Suc_as_int constructive_on_def restriction_shift_onI)

lemma constructiveI :
  ‹⟦⋀n x y. ⟦¬ f x ⪅⇩2 f y; x ↓⇩1 n ⪅⇩1 y ↓⇩1 n⟧ ⟹ f x ↓⇩2 Suc n ⪅⇩2 f y ↓⇩2 Suc n⟧
   ⟹ constructive f› by (unfold constructive_def, rule constructive_onI)

lemma constructive_onD :
  ‹⟦constructive_on f A; x ∈ A; y ∈ A; x ↓⇩1 n ⪅⇩1 y ↓⇩1 n⟧ ⟹ f x ↓⇩2 Suc n ⪅⇩2 f y ↓⇩2 Suc n›
  unfolding constructive_on_def by (metis Suc_as_int restriction_shift_onD)

lemma constructiveD : ‹⟦constructive f; x ↓⇩1 n ⪅⇩1 y ↓⇩1 n⟧ ⟹ f x ↓⇩2 Suc n ⪅⇩2 f y ↓⇩2 Suc n›
  unfolding constructive_def using constructive_onD by blast

lemma constructive_on_subset :
  ‹constructive_on f B ⟹ A ⊆ B ⟹ constructive_on f A›
  by (meson constructive_on_def restriction_shift_on_subset)

lemma constructive_imp_constructive_on [restriction_shift_simpset] :
  ‹constructive f ⟹ constructive_on f A›
  unfolding constructive_def using constructive_on_subset by auto


lemma constructive_on_imp_non_destructive_on [restriction_shift_simpset] :
  ‹constructive_on f A ⟹ non_destructive_on f A›
  by (rule non_destructive_onI)
    (meson PRS2.restriction_related_pred constructive_onD)

corollary constructive_imp_non_destructive [restriction_shift_simpset] :
  ‹constructive f ⟹ non_destructive f›
  unfolding constructive_def non_destructive_def
  by (fact constructive_on_imp_non_destructive_on)


corollary constructive_on_if_then_else [restriction_shift_simpset, restriction_shift_introset] :
  ‹⟦⋀x. P x ⟹ constructive_on (f x) A; ⋀x. ¬ P x ⟹ constructive_on (g x) A⟧
     ⟹ constructive_on (λy. if P x then f x y else g x y) A›
  and constructive_if_then_else [restriction_shift_simpset, restriction_shift_introset] :
  ‹⟦⋀x. P x ⟹ constructive (f x); ⋀x. ¬ P x ⟹ constructive (g x)⟧
     ⟹ constructive (λy. if P x then f x y else g x y)›
  by (auto simp add: constructive_def constructive_on_def
      intro: restriction_shift_on_if_then_else)


end



subsubsection ‹Properties›

locale PreorderRestrictionSpace_2_PreorderRestrictionSpace =
  PRS1 : PreorderRestrictionSpace ‹(↓⇩1)› ‹(⪅⇩1)› +
  PRS2 : PreorderRestrictionSpace ‹(↓⇩2)› ‹(⪅⇩2)›
  for restriction⇩1 :: ‹'a ⇒ nat ⇒ 'a›  (infixl ‹↓⇩1› 60)
    and relation⇩1    :: ‹'a ⇒ 'a ⇒ bool› (infixl ‹⪅⇩1› 50)
    and restriction⇩2 :: ‹'b ⇒ nat ⇒ 'b›  (infixl ‹↓⇩2› 60)
    and relation⇩2    :: ‹'b ⇒ 'b ⇒ bool› (infixl ‹⪅⇩2› 50)
begin

sublocale Restriction_2_PreorderRestrictionSpace by unfold_locales

lemma restriction_shift_on_restriction_restriction :
  ‹f (x ↓⇩1 n) ↓⇩2 nat (int n + k) ⪅⇩2 f x ↓⇩2 nat (int n + k)›
  if ‹restriction_shift_on f k A› ‹x ↓⇩1 n ∈ A› ‹x ∈ A› ‹x ↓⇩1 n ⪅⇩1 x ↓⇩1 n›
    ―‹the last assumption is trivial if \<^term>‹(⪅⇩1)› is reflexive›
  by (rule restriction_shift_onD
      [OF ‹restriction_shift_on f k A› ‹x ↓⇩1 n ∈ A› ‹x ∈ A›])
    (simp add: ‹x ↓⇩1 n ⪅⇩1 x ↓⇩1 n›)

corollary restriction_shift_restriction_restriction :
  ‹f (x ↓⇩1 n) ↓⇩2 nat (int n + k) ⪅⇩2 f x ↓⇩2 nat (int n + k)›
  if ‹restriction_shift f k› and ‹x ↓⇩1 n ⪅⇩1 x ↓⇩1 n›
  by (rule restriction_shiftD[OF ‹restriction_shift f k›])
    (simp add: ‹x ↓⇩1 n ⪅⇩1 x ↓⇩1 n›)


corollary constructive_on_restriction_restriction :
  ‹⟦constructive_on f A; x ↓⇩1 n ∈ A; x ∈ A; x ↓⇩1 n ⪅⇩1 x ↓⇩1 n⟧
   ⟹ f (x ↓⇩1 n) ↓⇩2 Suc n ⪅⇩2 f x ↓⇩2 Suc n›
  using restriction_shift_on_restriction_restriction
    restriction_shift_restriction_restriction Suc_as_int
  unfolding constructive_on_def by presburger

corollary constructive_restriction_restriction :
  ‹constructive f ⟹ x ↓⇩1 n ⪅⇩1 x ↓⇩1 n ⟹ f (x ↓⇩1 n) ↓⇩2 Suc n ⪅⇩2 f x ↓⇩2 Suc n›
  by (simp add: constructive_def constructive_on_restriction_restriction)


corollary non_destructive_on_restriction_restriction :
  ‹⟦non_destructive_on f A; x ↓⇩1 n ∈ A; x ∈ A; x ↓⇩1 n ⪅⇩1 x ↓⇩1 n⟧
   ⟹ f (x ↓⇩1 n) ↓⇩2 n ⪅⇩2 f x ↓⇩2 n›
  using restriction_shift_on_restriction_restriction
    restriction_shift_restriction_restriction
  unfolding non_destructive_on_def by (metis add.commute add_0 nat_int)

corollary non_destructive_restriction_restriction :
  ‹non_destructive f ⟹ x ↓⇩1 n ⪅⇩1 x ↓⇩1 n ⟹ f (x ↓⇩1 n) ↓⇩2 n ⪅⇩2 f x ↓⇩2 n›
  by (simp add: non_destructive_def non_destructive_on_restriction_restriction)


corollary non_too_destructive_on_restriction_restriction :
  ‹⟦non_too_destructive_on f A; x ↓⇩1 Suc n ∈ A; x ∈ A; x ↓⇩1 Suc n ⪅⇩1 x ↓⇩1 Suc n⟧
   ⟹ f (x ↓⇩1 Suc n) ↓⇩2 n ⪅⇩2 f x ↓⇩2 n›
  using restriction_shift_on_restriction_restriction
    restriction_shift_restriction_restriction
  unfolding non_too_destructive_on_def by fastforce

corollary non_too_destructive_restriction_restriction :
  ‹non_too_destructive f ⟹ x ↓⇩1 Suc n ⪅⇩1 x ↓⇩1 Suc n ⟹ f (x ↓⇩1 Suc n) ↓⇩2 n ⪅⇩2 f x ↓⇩2 n›
  by (simp add: non_too_destructive_def non_too_destructive_on_restriction_restriction)


end


locale Restriction_2_PreorderRestrictionSpace_2_PreorderRestrictionSpace =
  R2PRS1 : Restriction_2_PreorderRestrictionSpace ‹(↓⇩1)› ‹(⪅⇩1)› ‹(↓⇩2)› ‹(⪅⇩2)› +
  PRS2 : PreorderRestrictionSpace ‹(↓⇩3)› ‹(⪅⇩3)›
  for restriction⇩1 :: ‹'a ⇒ nat ⇒ 'a›  (infixl ‹↓⇩1› 60)
    and relation⇩1    :: ‹'a ⇒ 'a ⇒ bool› (infixl ‹⪅⇩1› 50)
    and restriction⇩2 :: ‹'b ⇒ nat ⇒ 'b›  (infixl ‹↓⇩2› 60)
    and relation⇩2    :: ‹'b ⇒ 'b ⇒ bool› (infixl ‹⪅⇩2› 50)
    and restriction⇩3 :: ‹'c ⇒ nat ⇒ 'c›  (infixl ‹↓⇩3› 60)
    and relation⇩3    :: ‹'c ⇒ 'c ⇒ bool› (infixl ‹⪅⇩3› 50)
begin

interpretation R2PRS2 : Restriction_2_PreorderRestrictionSpace ‹(↓⇩1)› ‹(⪅⇩1)› ‹(↓⇩3)› ‹(⪅⇩3)›
  by unfold_locales

interpretation PRS2PRS3 : PreorderRestrictionSpace_2_PreorderRestrictionSpace ‹(↓⇩2)› ‹(⪅⇩2)› ‹(↓⇩3)› ‹(⪅⇩3)›
  by unfold_locales



theorem restriction_shift_on_comp_restriction_shift_on [restriction_shift_simpset] :
  ‹R2PRS2.restriction_shift_on (λx. g (f x)) (k + l) A›
  if ‹f ` A ⊆ B› ‹PRS2PRS3.restriction_shift_on g l B› ‹R2PRS1.restriction_shift_on f k A›
proof (rule R2PRS2.restriction_shift_onI)
  fix x y n assume ‹x ∈ A› ‹y ∈ A› ‹x ↓⇩1 n ⪅⇩1 y ↓⇩1 n›
  from ‹R2PRS1.restriction_shift_on f k A›[THEN R2PRS1.restriction_shift_onD, OF this]
  have ‹f x ↓⇩2 nat (int n + k) ⪅⇩2 f y ↓⇩2 nat (int n + k)› .
  moreover from ‹x ∈ A› ‹y ∈ A› ‹f ` A ⊆ B› have ‹f x ∈ B› ‹f y ∈ B› by auto
  ultimately have ‹g (f x) ↓⇩3 nat (int (nat (int n + k)) + l) ⪅⇩3
                   g (f y) ↓⇩3 nat (int (nat (int n + k)) + l)›
    using ‹PRS2PRS3.restriction_shift_on g l B›[THEN PRS2PRS3.restriction_shift_onD] by blast
  moreover have ‹nat (int n + (k + l)) ≤ nat (int (nat (int n + k)) + l)›
    by (simp add: nat_mono)
  ultimately show ‹g (f x) ↓⇩3 nat (int n + (k + l)) ⪅⇩3 g (f y) ↓⇩3 nat (int n + (k + l))›
    by (metis PRS2.restriction_related_le)
qed

corollary restriction_shift_comp_restriction_shift_on [restriction_shift_simpset] :
  ‹PRS2PRS3.restriction_shift g l ⟹ R2PRS1.restriction_shift_on f k A ⟹
   R2PRS2.restriction_shift_on (λx. g (f x)) (k + l) A›
  using PRS2PRS3.restriction_shift_imp_restriction_shift_on
    restriction_shift_on_comp_restriction_shift_on by blast

corollary restriction_shift_comp_restriction_shift [restriction_shift_simpset] :
  ‹PRS2PRS3.restriction_shift g l ⟹ R2PRS1.restriction_shift f k ⟹
   R2PRS2.restriction_shift (λx. g (f x)) (k + l)›
  by (simp add: R2PRS1.restriction_shift_imp_restriction_shift_on
      R2PRS2.restriction_shift_def restriction_shift_comp_restriction_shift_on)



corollary non_destructive_on_comp_non_destructive_on [restriction_shift_simpset] :
  ‹⟦f ` A ⊆ B; PRS2PRS3.non_destructive_on g B; R2PRS1.non_destructive_on f A⟧ ⟹
    R2PRS2.non_destructive_on (λx. g (f x)) A›
  by (simp add: R2PRS1.non_destructive_on_def R2PRS2.non_destructive_on_def
      R2PRS2.restriction_shift_on_def R2PRS1.restriction_shift_on_def)
    (meson PRS2.mono_restriction_related PRS2PRS3.non_destructive_onD image_subset_iff)

corollary non_destructive_comp_non_destructive_on [restriction_shift_simpset] :
  ‹PRS2PRS3.non_destructive g ⟹ R2PRS1.non_destructive_on f A ⟹
   R2PRS2.non_destructive_on (λx. g (f x)) A›
  by (simp add: PRS2PRS3.non_destructiveD R2PRS1.non_destructive_on_def
      R2PRS2.non_destructive_on_def R2PRS2.restriction_shift_on_def
      R2PRS1.restriction_shift_on_def)

corollary non_destructive_comp_non_destructive [restriction_shift_simpset] :
  ‹PRS2PRS3.non_destructive g ⟹ R2PRS1.non_destructive f ⟹
   R2PRS2.non_destructive (λx. g (f x))›
  by (simp add: PRS2PRS3.non_destructiveD R2PRS1.non_destructiveD
      R2PRS2.non_destructive_def R2PRS2.non_destructive_onI)


corollary constructive_on_comp_non_destructive_on [restriction_shift_simpset] :
  ‹⟦f ` A ⊆ B; PRS2PRS3.constructive_on g B; R2PRS1.non_destructive_on f A⟧ ⟹
    R2PRS2.constructive_on (λx. g (f x)) A›
  by (metis PRS2PRS3.constructive_on_def R2PRS1.non_destructive_on_def
      R2PRS2.constructive_on_def add.commute add_cancel_left_right
      restriction_shift_on_comp_restriction_shift_on)

corollary constructive_comp_non_destructive_on [restriction_shift_simpset] :
  ‹PRS2PRS3.constructive g ⟹ R2PRS1.non_destructive_on f A ⟹
   R2PRS2.constructive_on (λx. g (f x)) A›
  by (simp add: R2PRS1.Restriction_2_PreorderRestrictionSpace_axioms
      PRS2PRS3.constructiveD R2PRS1.non_destructive_on_def R2PRS2.constructive_onI
      Restriction_2_PreorderRestrictionSpace.restriction_shift_on_def)

corollary constructive_comp_non_destructive [restriction_shift_simpset] :
  ‹PRS2PRS3.constructive g ⟹ R2PRS1.non_destructive f ⟹
   R2PRS2.constructive (λx. g (f x))›
  by (simp add: PRS2PRS3.constructiveD R2PRS1.non_destructiveD R2PRS2.constructiveI)


corollary non_destructive_on_comp_constructive_on [restriction_shift_simpset] :
  ‹⟦f ` A ⊆ B; PRS2PRS3.non_destructive_on g B; R2PRS1.constructive_on f A⟧ ⟹
    R2PRS2.constructive_on (λx. g (f x)) A›
  by (simp add: PRS2PRS3.non_destructive_onD R2PRS1.constructive_onD
      R2PRS2.constructive_onI image_subset_iff)

corollary non_destructive_comp_constructive_on [restriction_shift_simpset] :
  ‹PRS2PRS3.non_destructive g ⟹ R2PRS1.constructive_on f A ⟹
   R2PRS2.constructive_on (λx. g (f x)) A›
  using PRS2PRS3.non_destructive_def non_destructive_on_comp_constructive_on by blast

corollary non_destructive_comp_constructive [restriction_shift_simpset] :
  ‹PRS2PRS3.non_destructive g ⟹ R2PRS1.constructive f ⟹
   R2PRS2.constructive (λx. g (f x))›
  using PRS2PRS3.non_destructiveD R2PRS1.constructiveD R2PRS2.constructiveI by presburger


corollary non_too_destructive_on_comp_non_destructive_on [restriction_shift_simpset] :
  ‹⟦f ` A ⊆ B; PRS2PRS3.non_too_destructive_on g B; R2PRS1.non_destructive_on f A⟧ ⟹
    R2PRS2.non_too_destructive_on (λx. g (f x)) A›
  by (metis PRS2PRS3.non_too_destructive_on_def R2PRS1.non_destructive_on_def
      R2PRS2.non_too_destructive_on_def add.commute
      add.right_neutral restriction_shift_on_comp_restriction_shift_on)

corollary non_too_destructive_comp_non_destructive_on [restriction_shift_simpset] :
  ‹PRS2PRS3.non_too_destructive g ⟹ R2PRS1.non_destructive_on f A ⟹
   R2PRS2.non_too_destructive_on (λx. g (f x)) A›
  by (metis PRS2PRS3.non_too_destructive_imp_non_too_destructive_on
      non_too_destructive_on_comp_non_destructive_on top_greatest)

corollary non_too_destructive_comp_non_destructive [restriction_shift_simpset] :
  ‹PRS2PRS3.non_too_destructive g ⟹ R2PRS1.non_destructive f ⟹
   R2PRS2.non_too_destructive (λx. g (f x))›
  by (simp add: PRS2PRS3.non_too_destructiveD R2PRS1.non_destructiveD R2PRS2.non_too_destructiveI)


corollary non_destructive_on_comp_non_too_destructive_on [restriction_shift_simpset] :
  ‹⟦f ` A ⊆ B; PRS2PRS3.non_destructive_on g B; R2PRS1.non_too_destructive_on f A⟧ ⟹
    R2PRS2.non_too_destructive_on (λx. g (f x)) A›
  by (simp add: PRS2PRS3.non_destructive_onD R2PRS1.non_too_destructive_onD
      R2PRS2.non_too_destructive_onI image_subset_iff)

corollary non_destructive_comp_non_too_destructive_on [restriction_shift_simpset] :
  ‹PRS2PRS3.non_destructive g ⟹ R2PRS1.non_too_destructive_on f A ⟹
   R2PRS2.non_too_destructive_on (λx. g (f x)) A›
  by (simp add: PRS2PRS3.non_destructiveD R2PRS1.non_too_destructive_onD R2PRS2.non_too_destructive_onI)

corollary non_destructive_comp_non_too_destructive [restriction_shift_simpset] :
  ‹PRS2PRS3.non_destructive g ⟹ R2PRS1.non_too_destructive f ⟹
   R2PRS2.non_too_destructive (λx. g (f x))›
  using R2PRS1.non_too_destructive_imp_non_too_destructive_on R2PRS2.non_too_destructive_def
    non_destructive_comp_non_too_destructive_on by blast


corollary non_too_destructive_on_comp_constructive_on [restriction_shift_simpset] :
  ‹⟦f ` A ⊆ B; PRS2PRS3.non_too_destructive_on g B; R2PRS1.constructive_on f A⟧ ⟹
    R2PRS2.non_destructive_on (λx. g (f x)) A›
  using restriction_shift_on_comp_restriction_shift_on[of f A B g ‹- 1› 1]
  by (simp add: PRS2PRS3.non_too_destructive_on_def
      R2PRS2.non_destructive_on_def R2PRS1.constructive_on_def )

corollary non_too_destructive_comp_constructive_on [restriction_shift_simpset] :
  ‹PRS2PRS3.non_too_destructive g ⟹ R2PRS1.constructive_on f A ⟹
   R2PRS2.non_destructive_on (λx. g (f x)) A›
  by (metis PRS2PRS3.non_too_destructive_imp_non_too_destructive_on
      non_too_destructive_on_comp_constructive_on top_greatest)

corollary non_too_destructive_comp_constructive [restriction_shift_simpset] :
  ‹PRS2PRS3.non_too_destructive g ⟹ R2PRS1.constructive f ⟹
   R2PRS2.non_destructive (λx. g (f x))›
  by (simp add: PRS2PRS3.non_too_destructiveD R2PRS1.constructiveD R2PRS2.non_destructiveI)


corollary constructive_on_comp_non_too_destructive_on [restriction_shift_simpset] :
  ‹⟦f ` A ⊆ B; PRS2PRS3.constructive_on g B; R2PRS1.non_too_destructive_on f A⟧ ⟹
    R2PRS2.non_destructive_on (λx. g (f x)) A›
  using restriction_shift_on_comp_restriction_shift_on[of f A B g 1 ‹- 1›] 
  by (simp add: R2PRS1.non_too_destructive_on_def
      PRS2PRS3.constructive_on_def R2PRS2.non_destructive_on_def)

corollary constructive_comp_non_too_destructive_on [restriction_shift_simpset] :
  ‹PRS2PRS3.constructive g ⟹ R2PRS1.non_too_destructive_on f A ⟹
   R2PRS2.non_destructive_on (λx. g (f x)) A›
  using PRS2PRS3.constructive_imp_constructive_on constructive_on_comp_non_too_destructive_on by blast

corollary constructive_comp_non_too_destructive [restriction_shift_simpset] :
  ‹PRS2PRS3.constructive g ⟹ R2PRS1.non_too_destructive f ⟹
   R2PRS2.non_destructive (λx. g (f x))›
  by (metis R2PRS1.non_too_destructive_imp_non_too_destructive_on R2PRS2.non_destructiveI
      R2PRS2.non_destructive_onD UNIV_I constructive_comp_non_too_destructive_on)



end



(*<*)
end
  (*>*)