Theory RS_Option

(***********************************************************************************
 * 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 ‹Option Type›

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

subsection ‹Restriction option type›

instantiation option :: (restriction) restriction
begin

definition restriction_option :: ‹'a option ⇒ nat ⇒ 'a option›
  where ‹x ↓ n ≡ if n = 0 then None else map_option (λa. a ↓ n) x›

instance
  by intro_classes
    (simp add: restriction_option_def option.map_comp comp_def min_def)

end

lemma restriction_option_0_is_None [simp] : ‹x ↓ 0 = None›
  by (simp add: restriction_option_def)

lemma restriction_option_None [simp] : ‹None ↓ n = None›
  by (simp add: restriction_option_def)

lemma restriction_option_Some [simp] : ‹Some x ↓ n = (if n = 0 then None else Some (x ↓ n))›
  by (simp add: restriction_option_def)

lemma restriction_option_eq_None_iff : ‹x ↓ n = None ⟷ n = 0 ∨ x = None›
  by (cases x) simp_all

lemma restriction_option_eq_Some_iff : ‹x ↓ n = Some y ⟷ n ≠ 0 ∧ x ≠ None ∧ y = the x ↓ n›
  by (cases x) auto



subsection ‹Restriction space option type›

instance option :: (restriction_space) restriction_space
proof intro_classes
  show ‹x ↓ 0 = y ↓ 0› for x y :: ‹'a option› by simp
next
  show ‹x ≠ y ⟹ ∃n. x ↓ n ≠ y ↓ n› for x y :: ‹'a option›
    by (cases x; cases y, simp_all add: gt_ex)
      (metis bot_nat_0.not_eq_extremum ex_not_restriction_related restriction_0_related)
qed



subsection ‹Complete restriction space option type›

lemma option_restriction_chainE :
  fixes σ :: ‹nat ⇒ 'a :: restriction_space option› assumes ‹chain⇩↓ σ›
  obtains ‹σ = (λn. None)›
  | σ' where ‹chain⇩↓ σ'› and ‹σ = (λn. if n = 0 then None else Some (σ' n))›
proof -
  from ‹chain⇩↓ σ› consider ‹∀n. σ n = None› | ‹∀n>0. σ n ≠ None›
    by (metis bot_nat_0.not_eq_extremum linorder_neqE_nat
        restriction_chain_def_bis restriction_option_eq_None_iff)
  thus thesis
  proof cases
    from that(1) show ‹∀n. σ n = None ⟹ thesis› by fast
  next
    define σ' where ‹σ' n ≡ if n = 0 then undefined ↓ 0 else the (σ n)› for n
    assume ‹∀n>0. σ n ≠ None›
    with ‹chain⇩↓ σ› have ‹chain⇩↓ σ'› ‹σ = (λn. if n = 0 then undefined ↓ 0 else Some (σ' n))›
      by (simp_all add: σ'_def restriction_chain_def)
        (metis option.sel restriction_option_eq_Some_iff,
          metis σ'_def bot_nat_0.not_eq_extremum option.sel restriction_option_0_is_None)
    with that(2) show thesis by force
  qed
qed


lemma non_destructive_Some : ‹non_destructive Some›
  by (simp add: non_destructiveI)

lemma restriction_cont_Some : ‹cont⇩↓ (Some :: 'a :: restriction_space ⇒ 'a option)›
  by (rule restriction_shift_imp_restriction_cont[where k = 0])
    (simp add: restriction_shiftI)


instance option :: (complete_restriction_space) complete_restriction_space
proof intro_classes
  show ‹chain⇩↓ σ ⟹ convergent⇩↓ σ› for σ :: ‹nat ⇒ 'a option›
  proof (elim option_restriction_chainE)
    show ‹σ = (λn. None) ⟹ convergent⇩↓ σ› by simp
  next
    fix σ' assume ‹chain⇩↓ σ'› and σ_def : ‹σ = (λn. if n = 0 then None else Some (σ' n))›
    from ‹chain⇩↓ σ'› have ‹convergent⇩↓ σ'› by (simp add: restriction_chain_imp_restriction_convergent)
    hence ‹convergent⇩↓ (λn. σ' (n + 1))› by (unfold restriction_convergent_shift_iff)
    then obtain Σ' where ‹(λn. σ' (n + 1)) ─↓→ Σ'› by (blast dest: restriction_convergentD')
    hence ‹(λn. Some (σ' (n + 1))) ─↓→ Some Σ'› by (fact restriction_contD[OF restriction_cont_Some])
    hence ‹convergent⇩↓ (λn. Some (σ' (n + 1)))› by (blast intro: restriction_convergentI)
    hence ‹convergent⇩↓ (λn. σ (n + 1))› by (simp add: σ_def)
    thus ‹convergent⇩↓ σ› using restriction_convergent_shift_iff by blast
  qed
qed


(*<*)
end
  (*>*)