(*********************************************************************************** * 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 ‹Naturals› (*<*) theory RS_Nat imports Restriction_Spaces begin (*>*) text ‹Restriction instance for \<^typ>‹nat›.› instantiation nat :: restriction begin definition restriction_nat :: ‹nat ⇒ nat ⇒ nat› where ‹x ↓ n ≡ if x ≤ n then x else n› instance by intro_classes (simp add: restriction_nat_def) end lemma restriction_nat_0_is_0 [simp] : ‹x ↓ 0 = (0 :: nat)› by (simp add: restriction_nat_def) text ‹Restriction Space instance for \<^typ>‹nat›.› instance nat :: restriction_space by intro_classes (use nat_le_linear in ‹auto simp add: restriction_nat_def›) text ‹Constructive Suc› lemma constructive_Suc : ‹constructive Suc› proof (rule constructiveI) show ‹x ↓ n = y ↓ n ⟹ Suc x ↓ Suc n = Suc y ↓ Suc n› for x y n by (simp add: restriction_nat_def split: if_split_asm) qed text ‹Non too destructive pred› lemma non_too_destructive_pred : ‹non_too_destructive nat.pred› proof (rule non_too_destructiveI) show ‹x ↓ Suc n = y ↓ Suc n ⟹ nat.pred x ↓ n = nat.pred y ↓ n› for x y n by (cases x; cases y) (simp_all add: restriction_nat_def split: if_split_asm) qed text ‹Restriction shift plus› lemma restriction_shift_plus : ‹restriction_shift (λx. x + k) (int k)› proof (intro restriction_shiftI) show ‹x ↓ n = y ↓ n ⟹ x + k ↓ nat (int n + int k) = y + k ↓ nat (int n + int k)› for x y n by (simp add: restriction_nat_def nat_int_add split: if_split_asm) qed lemma ‹restriction_shift (λx. k + x) (int k)› by (simp add: add.commute restriction_shift_plus) ― ‹In particular, constructive if \<^term>‹1 < k›.› (*<*) end (*>*)