(*********************************************************************************** * 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 ‹Booleans› (*<*) theory RS_Bool imports Restriction_Spaces begin (*>*) text ‹Restriction instance for \<^typ>‹bool›.› instantiation bool :: restriction begin definition restriction_bool :: ‹bool ⇒ nat ⇒ bool› where ‹b ↓ n ≡ if n = 0 then False else b› instance by (intro_classes) (auto simp add: restriction_bool_def) end lemma restriction_bool_0_is_False [simp] : ‹b ↓ 0 = False› by (simp add: restriction_bool_def) text ‹Restriction space instance for \<^typ>‹bool›.› instance bool :: restriction_space by intro_classes (simp_all add: restriction_bool_def gt_ex) text ‹Complete Restriction space instance for \<^typ>‹bool›.› lemma restriction_tendsto_bool_iff : ‹σ ─↓→ Σ ⟷ (∃n. ∀k≥n. σ k = Σ)› for Σ :: bool unfolding restriction_tendsto_def by (auto simp add: restriction_bool_def) instance bool :: complete_restriction_space proof intro_classes fix σ :: ‹nat ⇒ bool› assume ‹chain⇩↓ σ› hence ‹(∀n>0. ¬ σ n) ∨ (∀n>0. σ n)› by (simp add: restriction_chain_def restriction_bool_def split: if_split_asm) (metis One_nat_def Zero_not_Suc gr0_conv_Suc nat_induct_non_zero zero_induct) hence ‹σ ─↓→ False ∨ σ ─↓→ True› by (metis (full_types) gt_ex order.strict_trans2 restriction_tendsto_def) thus ‹convergent⇩↓ σ› using restriction_convergentI by blast qed lemma restriction_cont_imp_restriction_adm : ‹cont⇩↓ P ⟹ adm⇩↓ P› for P :: ‹'a :: restriction_space ⇒ bool› unfolding restriction_adm_def restriction_cont_on_def restriction_cont_at_def by (auto simp add: restriction_tendsto_bool_iff) lemma restriction_compact_bool : ‹compact⇩↓ (UNIV :: bool set)› by (simp add: finite_imp_restriction_compact) (*<*) end (*>*)