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  AS. BS. 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