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" More_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 -
  { fix n
    have "n < LENGTH('a) ⟹ strict_part_mono {..n} (λx. (2 :: 'a :: len word) ^ x)"
    proof (induct n)
      case 0 then show ?case by simp
    next
      case (Suc n)
      from Suc.prems
      have "2 ^ n < (2 :: 'a :: len word) ^ Suc n"
        using power_strict_increasing unat_power_lower word_less_nat_alt by fastforce
      with Suc
      show ?case by (subst strict_part_mono_by_steps) simp
    qed
  }
  then show ?thesis by simp
qed

end