Theory RS_Decimals

(***********************************************************************************
 * 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 ‹Decimals of a Number›

(*<*)
theory RS_Decimals
  imports Restriction_Spaces
begin
  (*>*)

typedef (overloaded) 'a :: zero decimals = ‹{σ :: nat ⇒ 'a. σ 0 = 0}›
  morphisms from_decimals to_decimals by auto

setup_lifting type_definition_decimals


declare from_decimals [simp] to_decimals_cases[simp]
  to_decimals_inject[simp] to_decimals_inverse [simp]


declare from_decimals_inject  [simp]
  from_decimals_inverse [simp]

lemmas to_decimals_inject_simplified [simp] = to_decimals_inject [simplified]
  and to_decimals_inverse_simplified[simp] = to_decimals_inverse[simplified]

(* useful ? *)
lemmas to_decimals_induct_simplified = to_decimals_induct[simplified]
  and to_decimals_cases_simplified  = to_decimals_cases [simplified]
  and from_decimals_induct_simplified = from_decimals_induct[simplified]
  and from_decimals_cases_simplified  = from_decimals_cases [simplified]



instantiation decimals :: (zero) restriction
begin

lift_definition restriction_decimals :: ‹'a decimals ⇒ nat ⇒ 'a decimals› 
  is ‹λσ m n. if n ≤ m then σ n else 0› by simp

instance by (intro_classes, transfer, rule ext, simp)

end


instance decimals :: (zero) restriction_space
  by (intro_classes; transfer, auto)
    (metis (no_types, lifting) ext order_refl)


lemma restriction_decimals_eq_iff :
  ‹x ↓ n = y ↓ n ⟷ (∀i≤n. from_decimals x i = from_decimals y i)›
  by transfer meson


lemma restriction_decimals_eqI :
  ‹(⋀i. i ≤ n ⟹ from_decimals x i = from_decimals y i) ⟹ x ↓ n = y ↓ n›
  by (simp add: restriction_decimals_eq_iff)

lemma restriction_decimals_eqD :
  ‹x ↓ n = y ↓ n ⟹ i ≤ n ⟹ from_decimals x i = from_decimals y i›
  by (simp add: restriction_decimals_eq_iff)


text ‹This space is actually complete.›

instance decimals :: (zero) complete_restriction_space
proof (intro_classes, rule restriction_convergentI)
  fix σ :: ‹nat ⇒ 'a decimals› assume ‹chain↓ σ›
  let ?Σ = ‹to_decimals (λn. from_decimals (σ n) n)›
  have ‹?Σ ↓ n = σ n› for n
  proof (subst restricted_restriction_chain_is[OF ‹chain↓ σ›, symmetric],
      rule restriction_decimals_eqI)
    fix i assume ‹i ≤ n›
    from restriction_chain_def_ter
      [THEN iffD1, OF ‹restriction_chain σ›, rule_format, OF ‹i ≤ n›]
    show ‹from_decimals ?Σ i = from_decimals (σ n) i›
      by (subst to_decimals_inverse_simplified, use from_decimals in blast)
        (metis dual_order.refl restriction_decimals.rep_eq)
  qed
  thus ‹restriction_chain σ ⟹ σ ─↓→ ?Σ› 
  proof -
    have ‹(↓) (to_decimals (λn. from_decimals (σ n) n)) = σ›
      using ‹⋀n. to_decimals (λn. from_decimals (σ n) n) ↓ n = σ n› by force
    then show ?thesis
      by (metis restriction_tendsto_restrictions)
  qed
qed




typedef nat_0_9 = ‹{0.. 9::nat}›
  morphisms from_nat_0_9 to_nat_0_9 by auto


setup_lifting type_definition_nat_0_9


instantiation nat_0_9 :: zero
begin

lift_definition zero_nat_0_9 :: nat_0_9 is 0 by simp

instance ..

end

instantiation nat_0_9 :: one
begin

lift_definition one_nat_0_9 :: nat_0_9 is 1 by simp

instance ..

end


lift_definition update_nth_decimal :: ‹[nat_0_9 decimals, nat, nat] ⇒ nat_0_9 decimals›
  is ‹λs index value.   if index = 0 ∨ 9 < value then from_decimals s
                      else (from_decimals s)(index := to_nat_0_9 value)›
  using from_decimals by auto


lemma no_update_nth_decimal [simp] :
  ‹index = 0 ⟹ update_nth_decimal s index val = s›
  ‹9 < val   ⟹ update_nth_decimal s index val = s›
  by (simp_all add: update_nth_decimal.abs_eq)


lemma non_destructive_update_nth_decimal : ‹non_destructive update_nth_decimal›
proof (rule non_destructiveI)
  show ‹update_nth_decimal x ↓ n = update_nth_decimal y ↓ n› if ‹x ↓ n = y ↓ n› for x y n
  proof (unfold restriction_fun_def, intro ext restriction_decimals_eqI)
    fix index val i assume ‹i ≤ n›
    from restriction_decimals_eqD[OF ‹x ↓ n = y ↓ n› ‹i ≤ n›]
    show ‹from_decimals (update_nth_decimal x index val) i =
          from_decimals (update_nth_decimal y index val) i›
      by (simp add: update_nth_decimal.rep_eq)
  qed
qed


lift_definition shift_decimal_right :: ‹nat_0_9 decimals ⇒ nat_0_9 decimals›
  is ‹λs n. case n of 0 ⇒ to_nat_0_9 0 | Suc n' ⇒ from_decimals s n'›
  by (simp add: zero_nat_0_9_def)


lemma constructive_shift_decimal_right : ‹constructive shift_decimal_right›
proof (rule constructiveI)
  show ‹shift_decimal_right x ↓ Suc n = shift_decimal_right y ↓ Suc n› if ‹x ↓ n = y ↓ n› for x y n
  proof (intro restriction_decimals_eqI)
    fix index val i assume ‹i ≤ Suc n›
    hence ‹i - 1 ≤ n› by simp
    from restriction_decimals_eqD[OF ‹x ↓ n = y ↓ n› ‹i - 1 ≤ n›]
    show ‹from_decimals (shift_decimal_right x) i = from_decimals (shift_decimal_right y) i›
      by (simp add: shift_decimal_right.rep_eq Nitpick.case_nat_unfold)
  qed
qed


lift_definition shift_decimal_left :: ‹nat_0_9 decimals ⇒ nat_0_9 decimals›
  is ‹λs n. if n = 0 then to_nat_0_9 0 else from_decimals s (Suc n)›
  by (simp add: zero_nat_0_9_def)

lemma non_too_destructive_shift_decimal_left : ‹non_too_destructive shift_decimal_left›
proof (rule non_too_destructiveI)
  show ‹shift_decimal_left x ↓ n = shift_decimal_left y ↓ n› if ‹x ↓ Suc n = y ↓ Suc n› for x y n
  proof (intro restriction_decimals_eqI)
    fix index val i assume ‹i ≤ n›
    hence ‹Suc i ≤ Suc n› by simp
    from restriction_decimals_eqD[OF ‹x ↓ Suc n = y ↓ Suc n› ‹Suc i ≤ Suc n›]
    show ‹from_decimals (shift_decimal_left x) i = from_decimals (shift_decimal_left y) i›
      by (simp add: shift_decimal_left.rep_eq)
  qed
qed



lemma restriction_fix_shift_decimal_right : ‹(υ x. shift_decimal_right x) = to_decimals (λ_. 0)›
proof (rule restriction_fix_unique)
  show ‹constructive shift_decimal_right› 
    by (fact constructive_shift_decimal_right)
next
  show ‹shift_decimal_right (to_decimals (λ_. 0)) = to_decimals (λ_. 0)›
    by (simp add: shift_decimal_right.abs_eq)
      (metis nat.case_eq_if to_decimals_inverse_simplified zero_nat_0_9_def)
qed



text ‹Example of a predicate that is not admissible.›

lemma one_in_decimals_not_admissible :
  defines P_def: ‹P ≡ λx. (1 :: nat_0_9) ∈ range (from_decimals x)›
  shows ‹¬ adm↓ P›
proof (rule ccontr)
  assume * : ‹¬ ¬ adm↓ P›

  define x where ‹x ≡ to_decimals (λn. if n = 0 then 0 else 1 :: nat_0_9)›

  have ‹P (υ x. shift_decimal_right x)›
  proof (induct rule: restriction_fix_ind)
    show ‹constructive shift_decimal_right› by (fact constructive_shift_decimal_right)
  next
    from "*" show ‹adm↓ P› by simp
  next
    show ‹P x› by (auto simp add: P_def x_def image_iff)
  next
    show ‹P x ⟹ P (shift_decimal_right x)› for x
      by (simp add: P_def image_def shift_decimal_right.rep_eq)
        (metis old.nat.simps(5))
  qed
  moreover have ‹¬ P (υ x. shift_decimal_right x)›
    by (simp add: P_def restriction_fix_shift_decimal_right)
      (transfer, simp)
  ultimately show False by blast
qed

(*<*)
end
  (*>*)