Theory Strict_part_mono

(*
 * Copyright Data61, CSIRO (ABN 41 687 119 230)
 *
 * SPDX-License-Identifier: BSD-2-Clause
 *)

theory Strict_part_mono
  imports "HOL-Library.Word"
begin

definition
  strict_part_mono :: "'a set ⇒ ('a :: order ⇒ 'b :: order) ⇒ bool" where
 "strict_part_mono S f ≡ ∀A∈S. ∀B∈S. A < B ⟶ f A < f B"

lemma strict_part_mono_by_steps:
  "strict_part_mono {..n :: nat} f = (n ≠ 0 ⟶ f (n - 1) < f n ∧ strict_part_mono {.. n - 1} f)"
  apply (cases n; simp add: strict_part_mono_def)
  apply (safe; clarsimp)
  apply (case_tac "B = Suc nat"; simp)
  apply (case_tac "A = nat"; clarsimp)
  apply (erule order_less_trans [rotated])
  apply simp
  done

lemma strict_part_mono_singleton[simp]:
  "strict_part_mono {x} f"
  by (simp add: strict_part_mono_def)

lemma strict_part_mono_lt:
  "⟦ x < f 0; strict_part_mono {.. n :: nat} f ⟧ ⟹ ∀m ≤ n. x < f m"
  by (auto simp add: strict_part_mono_def Ball_def intro: order.strict_trans)

lemma strict_part_mono_reverseE:
  "⟦ f n ≤ f m; strict_part_mono {.. N :: nat} f; n ≤ N ⟧ ⟹ n ≤ m"
  by (rule ccontr) (fastforce simp: linorder_not_le strict_part_mono_def)

lemma two_power_strict_part_mono:
  ‹strict_part_mono {..LENGTH('a) - 1} (λx. (2 :: 'a::len word) ^ x)›
proof -
  have ‹strict_part_mono {..n} (λx. (2 :: 'a::len word) ^ x)›
    if ‹n < LENGTH('a)› for n
  using that proof (induction n)
    case 0
    then show ?case
      by simp
  next
    case (Suc n)
    then have ‹strict_part_mono {..n} ((^) (2 :: 'a::len word))›
      by simp
    moreover have ‹2 ^ n < (2::nat) ^ Suc n›
      by simp
    with Suc.prems have ‹word_of_nat (2 ^ n) < (word_of_nat (2 ^ Suc n) :: 'a word)›
      by (simp only: of_nat_word_less_iff take_bit_of_exp) simp
    ultimately show ?case
      by (subst strict_part_mono_by_steps) simp
  qed
  then show ?thesis
    by simp
qed

end