Theory HOL_Lemmas

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

section "Generic Lemmas used in the Word Library"

theory HOL_Lemmas
imports Main
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 (metis atMost_iff le_0_eq le_cases neq0_conv order.strict_trans strict_part_mono_def)

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 takeWhile_take_has_property:
  "n ≤ length (takeWhile P xs) ⟹ ∀x ∈ set (take n xs). P x"
  by (induct xs arbitrary: n; simp split: if_split_asm) (case_tac n, simp_all)

lemma takeWhile_take_has_property_nth:
  "⟦ n < length (takeWhile P xs) ⟧ ⟹ P (xs ! n)"
  by (induct xs arbitrary: n; simp split: if_split_asm) (case_tac n, simp_all)

lemma takeWhile_replicate:
  "takeWhile f (replicate len x) = (if f x then replicate len x else [])"
  by (induct_tac len) auto

lemma takeWhile_replicate_empty:
  "¬ f x ⟹ takeWhile f (replicate len x) = []"
  by (simp add: takeWhile_replicate)

lemma takeWhile_replicate_id:
  "f x ⟹ takeWhile f (replicate len x) = replicate len x"
  by (simp add: takeWhile_replicate)

lemma power_sub:
  fixes a :: nat
  assumes lt: "n ≤ m"
  and     av: "0 < a"
  shows "a ^ (m - n) = a ^ m div a ^ n"
proof (subst nat_mult_eq_cancel1 [symmetric])
  show "(0::nat) < a ^ n" using av by simp
next
  from lt obtain q where mv: "n + q = m"
    by (auto simp: le_iff_add)

  have "a ^ n * (a ^ m div a ^ n) = a ^ m"
  proof (subst mult.commute)
    have "a ^ m = (a ^ m div a ^ n) * a ^ n + a ^ m mod a ^ n"
      by (rule  div_mult_mod_eq [symmetric])

    moreover have "a ^ m mod a ^ n = 0"
      by (subst mod_eq_0_iff_dvd, subst dvd_def, rule exI [where x = "a ^ q"],
      (subst power_add [symmetric] mv)+, rule refl)

    ultimately show "(a ^ m div a ^ n) * a ^ n = a ^ m" by simp
  qed

  then show "a ^ n * a ^ (m - n) = a ^ n * (a ^ m div a ^ n)" using lt
    by (simp add: power_add [symmetric])
qed


lemma union_sub:
  "⟦B ⊆ A; C ⊆ B⟧ ⟹ (A - B) ∪ (B - C) = (A - C)"
  by fastforce

lemma insert_sub:
  "x ∈ xs ⟹ (insert x (xs - ys)) = (xs - (ys - {x}))"
  by blast

lemma ran_upd:
  "⟦ inj_on f (dom f); f y = Some z ⟧ ⟹ ran (λx. if x = y then None else f x) = ran f - {z}"
  unfolding ran_def
  apply (rule set_eqI)
  apply simp
  by (metis domI inj_on_eq_iff option.sel)

lemma nat_less_power_trans:
  fixes n :: nat
  assumes nv: "n < 2 ^ (m - k)"
  and     kv: "k ≤ m"
  shows "2 ^ k * n < 2 ^ m"
proof (rule order_less_le_trans)
  show "2 ^ k * n < 2 ^ k * 2 ^ (m - k)"
    by (rule mult_less_mono2 [OF nv zero_less_power]) simp

  show "(2::nat) ^ k * 2 ^ (m - k) ≤ 2 ^ m" using nv kv
    by (subst power_add [symmetric]) simp
qed

lemma nat_le_power_trans:
  fixes n :: nat
  shows "⟦n ≤ 2 ^ (m - k); k ≤ m⟧ ⟹ 2 ^ k * n ≤ 2 ^ m"
  by (metis le_add_diff_inverse mult_le_mono2 semiring_normalization_rules(26))

lemma x_power_minus_1:
  fixes x :: "'a :: {ab_group_add, power, numeral, one}"
  shows "x + (2::'a) ^ n - (1::'a) = x + (2 ^ n - 1)" by simp

lemma nat_diff_add:
  fixes i :: nat
  shows "⟦ i + j = k ⟧ ⟹ i = k - j"
  by arith

lemma pow_2_gt: "n ≥ 2 ⟹ (2::int) < 2 ^ n"
  by (induct n) auto

lemma if_apply_def2:
  "(if P then F else G) = (λx. (P ⟶ F x) ∧ (¬ P ⟶ G x))"
  by simp

lemma case_bool_If:
  "case_bool P Q b = (if b then P else Q)"
  by simp

lemma sum_to_zero:
  "(a :: 'a :: ring) + b = 0 ⟹ a = (- b)"
  by (drule arg_cong[where f="λ x. x - a"], simp)

lemma arith_is_1:
  "⟦ x ≤ Suc 0; x > 0 ⟧ ⟹ x = 1"
  by arith

lemma if_f:
  "(if a then f b else f c) = f (if a then b else c)"
  by simp

lemma upt_add_eq_append':
  assumes "i ≤ j" and "j ≤ k"
  shows "[i..<k] = [i..<j] @ [j..<k]"
  using assms le_Suc_ex upt_add_eq_append by blast

lemma split_upt_on_n:
  "n < m ⟹ [0 ..< m] = [0 ..< n] @ [n] @ [Suc n ..< m]"
  by (metis append_Cons append_Nil less_Suc_eq_le less_imp_le_nat upt_add_eq_append'
            upt_rec zero_less_Suc)

lemma drop_Suc_nth:
  "n < length xs ⟹ drop n xs = xs!n # drop (Suc n) xs"
  by (simp add: Cons_nth_drop_Suc)

lemma n_less_equal_power_2 [simp]:
  "n < 2 ^ n"
  by (induct n; simp)

lemma nat_min_simps [simp]:
  "(a::nat) ≤ b ⟹ min b a = a"
  "a ≤ b ⟹ min a b = a"
  by auto

lemma power_sub_int:
  "⟦ m ≤ n; 0 < b ⟧ ⟹ b ^ n div b ^ m = (b ^ (n - m) :: int)"
  apply (subgoal_tac "∃n'. n = m + n'")
   apply (clarsimp simp: power_add)
  apply (rule exI[where x="n - m"])
  apply simp
  done

lemma suc_le_pow_2:
  "1 < (n::nat) ⟹ Suc n < 2 ^ n"
  by (induct n; clarsimp)
     (case_tac "n = 1"; clarsimp)

lemma nat_le_Suc_less_imp:
  "x < y ⟹ x ≤ y - Suc 0"
  by arith

lemma length_takeWhile_less:
  "∃x∈set xs. ¬ P x ⟹ length (takeWhile P xs) < length xs"
  by (induct xs) (auto split: if_splits)

lemma drop_eq_mono:
  assumes le: "m ≤ n"
  assumes drop: "drop m xs = drop m ys"
  shows "drop n xs = drop n ys"
proof -
  have ex: "∃p. n = p + m" by (rule exI[of _ "n - m"]) (simp add: le)
  then obtain p where p: "n = p + m" by blast
  show ?thesis unfolding p drop_drop[symmetric] drop by simp
qed

lemma nat_Suc_less_le_imp:
  "(k::nat) < Suc n ⟹ k ≤ n"
  by auto

lemma nat_add_less_by_max:
  "⟦ (x::nat) ≤ xmax ; y < k - xmax ⟧ ⟹ x + y < k"
  by simp

lemma mod_lemma: "[| (0::nat) < c; r < b |] ==> b * (q mod c) + r < b * c"
  apply (cut_tac m = q and n = c in mod_less_divisor)
  apply (drule_tac [2] m = "q mod c" in less_imp_Suc_add, auto)
  apply (erule_tac P = "%x. lhs < rhs x" for lhs rhs in ssubst)
  apply (simp add: add_mult_distrib2)
  done

lemma nat_le_Suc_less:
  "0 < y ⟹ (x ≤ y - Suc 0) = (x < y)"
  by arith

lemma nat_power_minus_less:
  "a < 2 ^ (x - n) ⟹ (a :: nat) < 2 ^ x"
  by (erule order_less_le_trans) simp

end