# Theory Word_Lib.Many_More

```(*
* Copyright Data61, CSIRO (ABN 41 687 119 230)
*
*)

theory Many_More
imports
Main
"HOL-Library.Word"
More_Word
Even_More_List
begin

lemma nat_less_mult_monoish: "⟦ a < b; c < (d :: nat) ⟧ ⟹ (a + 1) * (c + 1) <= b * d"
apply (drule Suc_leI)+
apply (drule(1) mult_le_mono)
apply simp
done

context
includes bit_operations_syntax
begin

lemma if_and_helper:
"(If x v v') AND v'' = If x (v AND v'') (v' AND v'')"
by (rule if_distrib)

end

lemma eq_eqI:
"a = b ⟹ (a = x) = (b = x)"
by simp

lemma map2_Cons_2_3:
"(map2 f xs (y # ys) = (z # zs)) = (∃x xs'. xs = x # xs' ∧ f x y = z ∧ map2 f xs' ys = zs)"
by (case_tac xs, simp_all)

lemma map2_xor_replicate_False:
"map2 (λx y. x ⟷ ¬ y) xs (replicate n False) = take n xs"
apply (induct xs arbitrary: n, simp)
apply (case_tac n; simp)
done

lemma plus_Collect_helper:
"(+) x ` {xa. P (xa :: 'a :: len word)} = {xa. P (xa - x)}"

lemma plus_Collect_helper2:
"(+) (- x) ` {xa. P (xa :: 'a :: len word)} = {xa. P (x + xa)}"
using plus_Collect_helper [of "- x" P] by (simp add: ac_simps)

lemma range_subset_eq2:
"{a :: 'a :: len word .. b} ≠ {} ⟹ ({a .. b} ⊆ {c .. d}) = (c ≤ a ∧ b ≤ d)"
by simp

lemma nat_mod_power_lem:
fixes a :: nat
shows "1 < a ⟹ a ^ n mod a ^ m = (if m ≤ n then 0 else a ^ n)"
apply (clarsimp)
done

lemma i_hate_words_helper:
"i ≤ (j - k :: nat) ⟹ i ≤ j"
by simp

lemma i_hate_words:
"unat (a :: 'a word) ≤ unat (b :: 'a :: len word) - Suc 0
⟹ a ≠ -1"
apply (frule i_hate_words_helper)
apply (subst(asm) word_le_nat_alt[symmetric])
apply (clarsimp simp only: word_minus_one_le)
apply (simp only: linorder_not_less[symmetric])
apply (erule notE)
apply (rule diff_Suc_less)
apply (subst neq0_conv[symmetric])
apply (subst unat_eq_0)
apply (rule notI, drule arg_cong[where f="(+) 1"])
apply simp
done

lemma If_eq_obvious:
"x ≠ z ⟹ ((if P then x else y) = z) = (¬ P ∧ y = z)"
by simp

lemma Some_to_the:
"v = Some x ⟹ x = the v"
by simp

lemma dom_if_Some:
"dom (λx. if P x then Some (f x) else g x) = {x. P x} ∪ dom g"
by fastforce

lemma dom_insert_absorb:
"x ∈ dom f ⟹ insert x (dom f) = dom f"
by (fact insert_absorb)

lemma emptyE2:
"⟦ S = {}; x ∈ S ⟧ ⟹ P"
by simp

"⟦ ⋀x y. (x * val = y * val') = (x * val'' = y); x * val'' ∈ S ⟧ ⟹
ptr_add ptr (x * val) ∈ (λp. ptr_add ptr (p * val')) ` S"
by (auto simp add: image_iff) metis

lemmas map_prod_split_imageI'
= map_prod_imageI[where f="case_prod f" and g="case_prod g"
and a="(a, b)" and b="(c, d)" for a b c d f g]
lemmas map_prod_split_imageI = map_prod_split_imageI'[simplified]

lemma dom_if:
"dom (λa. if a ∈ addrs then Some (f a) else g a)  = addrs ∪ dom g"
by (auto simp: dom_def split: if_split)

lemmas arg_cong_Not = arg_cong [where f=Not]

lemma drop_append_miracle:
"n = length xs ⟹ drop n (xs @ ys) = ys"
by simp

lemma foldr_does_nothing_to_xf:
"⟦ ⋀x s. x ∈ set xs ⟹ xf (f x s) = xf s ⟧ ⟹ xf (foldr f xs s) = xf s"
by (induct xs, simp_all)

lemma mod_mod_power_int:
fixes k :: int
shows "k mod 2 ^ m mod 2 ^ n = k mod 2 ^ (min m n)"
by (fact mod_exp_eq)

lemma le_step_down_nat:"⟦(i::nat) ≤ n; i = n ⟶ P; i ≤ n - 1 ⟶ P⟧ ⟹ P"
by arith

lemma le_step_down_int:"⟦(i::int) ≤ n; i = n ⟶ P; i ≤ n - 1 ⟶ P⟧ ⟹ P"
by arith

lemma replicate_numeral [simp]: "replicate (numeral k) x = x # replicate (pred_numeral k) x"

lemma list_exhaust_size_gt0:
assumes "⋀a list. y = a # list ⟹ P"
shows "0 < length y ⟹ P"
apply (cases y)
apply simp
apply (rule assms)
apply fastforce
done

lemma list_exhaust_size_eq0:
assumes "y = [] ⟹ P"
shows "length y = 0 ⟹ P"
apply (cases y)
apply (rule assms)
apply simp
apply simp
done

lemma size_Cons_lem_eq: "y = xa # list ⟹ size y = Suc k ⟹ size list = k"
by auto

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_empty:
"¬ f x ⟹ takeWhile f (replicate len x) = []"
by simp

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

lemma takeWhile_all:
"length (takeWhile P xs) = length xs ⟹ ∀x ∈ set xs. P x"
by (induct xs) (auto split: if_split_asm)

lemma nth_rev: "n < length xs ⟹ rev xs ! n = xs ! (length xs - 1 - n)"
using rev_nth by simp

lemma nth_rev_alt: "n < length ys ⟹ ys ! n = rev ys ! (length ys - Suc n)"

lemma hd_butlast: "length xs > 1 ⟹ hd (butlast xs) = hd xs"
by (cases xs) auto

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_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 drop_Suc_nth:
"n < length xs ⟹ drop n xs = xs!n # drop (Suc n) xs"

lemma and_len: "xs = ys ⟹ xs = ys ∧ length xs = length ys"
by auto

lemma tl_if: "tl (if p then xs else ys) = (if p then tl xs else tl ys)"
by auto

lemma hd_if: "hd (if p then xs else ys) = (if p then hd xs else hd ys)"
by auto

lemma if_single: "(if xc then [xab] else [an]) = [if xc then xab else an]"
by auto

― ‹note -- ‹if_Cons› can cause blowup in the size, if ‹p› is complex, so make a simproc›
lemma if_Cons: "(if p then x # xs else y # ys) = If p x y # If p xs ys"
by auto

lemma list_of_false:
"True ∉ set xs ⟹ xs = replicate (length xs) False"
by (induct xs, simp_all)

lemma list_all2_induct [consumes 1, case_names Nil Cons]:
assumes lall: "list_all2 Q xs ys"
and     nilr: "P [] []"
and    consr: "⋀x xs y ys. ⟦list_all2 Q xs ys; Q x y; P xs ys⟧ ⟹ P (x # xs) (y # ys)"
shows  "P xs ys"
using lall
proof (induct rule: list_induct2 [OF list_all2_lengthD [OF lall]])
case 1 then show ?case by auto fact+
next
case (2 x xs y ys)

show ?case
proof (rule consr)
from "2.prems" show "list_all2 Q xs ys" and "Q x y" by simp_all
then show "P xs ys" by (intro "2.hyps")
qed
qed

lemma replicate_minus:
"k < n ⟹ replicate n False = replicate (n - k) False @ replicate k False"

lemma cart_singleton_empty:
"(S × {e} = {}) = (S = {})"
by blast

lemma MinI:
assumes fa: "finite A"
and     ne: "A ≠ {}"
and     xv: "m ∈ A"
and    min: "∀y ∈ A. m ≤ y"
shows "Min A = m" using fa ne xv min
proof (induct A arbitrary: m rule: finite_ne_induct)
case singleton then show ?case by simp
next
case (insert y F)

from insert.prems have yx: "m ≤ y" and fx: "∀y ∈ F. m ≤ y" by auto
have "m ∈ insert y F" by fact
then show ?case
proof
assume mv: "m = y"

have mlt: "m ≤ Min F"
by (rule iffD2 [OF Min_ge_iff [OF insert.hyps(1) insert.hyps(2)] fx])

show ?case
apply (subst Min_insert [OF insert.hyps(1) insert.hyps(2)])
apply (subst mv [symmetric])
apply (auto simp: min_def mlt)
done
next
assume "m ∈ F"
then have mf: "Min F = m"
by (rule insert.hyps(4) [OF _ fx])

show ?case
apply (subst Min_insert [OF insert.hyps(1) insert.hyps(2)])
apply (subst mf)
apply (rule iffD2 [OF _ yx])
apply (auto simp: min_def)
done
qed
qed

lemma power_numeral: "a ^ numeral k = a * a ^ (pred_numeral k)"

lemma funpow_numeral [simp]: "f ^^ numeral k = f ∘ f ^^ (pred_numeral k)"

lemma funpow_minus_simp: "0 < n ⟹ f ^^ n = f ∘ f ^^ (n - 1)"
by (auto dest: gr0_implies_Suc)

lemma rco_alt: "(f ∘ g) ^^ n ∘ f = f ∘ (g ∘ f) ^^ n"
apply (rule ext)
apply (induct n)
done

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 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 if_f:
"(if a then f b else f c) = f (if a then b else c)"
by simp

lemma size_if: "size (if p then xs else ys) = (if p then size xs else size ys)"
by (fact if_distrib)

lemma if_Not_x: "(if p then ¬ x else x) = (p = (¬ x))"
by auto

lemma if_x_Not: "(if p then x else ¬ x) = (p = x)"
by auto

lemma if_same_and: "(If p x y ∧ If p u v) = (if p then x ∧ u else y ∧ v)"
by auto

lemma if_same_eq: "(If p x y  = (If p u v)) = (if p then x = u else y = v)"
by auto

lemma if_same_eq_not: "(If p x y = (¬ If p u v)) = (if p then x = (¬ u) else y = (¬ v))"
by auto

lemma the_elemI: "y = {x} ⟹ the_elem y = x"
by simp

lemma nonemptyE: "S ≠ {} ⟹ (⋀x. x ∈ S ⟹ R) ⟹ R"
by auto

lemmas xtr1 = xtrans(1)
lemmas xtr2 = xtrans(2)
lemmas xtr3 = xtrans(3)
lemmas xtr4 = xtrans(4)
lemmas xtr5 = xtrans(5)
lemmas xtr6 = xtrans(6)
lemmas xtr7 = xtrans(7)
lemmas xtr8 = xtrans(8)

lemmas if_fun_split = if_apply_def2

lemma not_empty_eq:
"(S ≠ {}) = (∃x. x ∈ S)"
by auto

lemma range_subset_lower:
fixes c :: "'a ::linorder"
shows "⟦ {a..b} ⊆ {c..d}; x ∈ {a..b} ⟧ ⟹ c ≤ a"
apply (frule (1) subsetD)
apply (rule classical)
apply clarsimp
done

lemma range_subset_upper:
fixes c :: "'a ::linorder"
shows "⟦ {a..b} ⊆ {c..d}; x ∈ {a..b} ⟧ ⟹ b ≤ d"
apply (frule (1) subsetD)
apply (rule classical)
apply clarsimp
done

lemma range_subset_eq:
fixes a::"'a::linorder"
assumes non_empty: "a ≤ b"
shows "({a..b} ⊆ {c..d}) = (c ≤ a ∧ b ≤ d)"
apply (insert non_empty)
apply (rule iffI)
apply (frule range_subset_lower [where x=a], simp)
apply (drule range_subset_upper [where x=a], simp)
apply simp
apply auto
done

lemma range_eq:
fixes a::"'a::linorder"
assumes non_empty: "a ≤ b"
shows "({a..b} = {c..d}) = (a = c ∧ b = d)"
by (metis atLeastatMost_subset_iff eq_iff non_empty)

lemma range_strict_subset_eq:
fixes a::"'a::linorder"
assumes non_empty: "a ≤ b"
shows "({a..b} ⊂ {c..d}) = (c ≤ a ∧ b ≤ d ∧ (a = c ⟶ b ≠ d))"
apply (insert non_empty)
apply (subst psubset_eq)
apply (subst range_subset_eq, assumption+)
apply (subst range_eq, assumption+)
apply simp
done

lemma range_subsetI:
fixes x :: "'a :: order"
assumes xX: "X ≤ x"
and     yY: "y ≤ Y"
shows   "{x .. y} ⊆ {X .. Y}"
using xX yY by auto

lemma set_False [simp]:
"(set bs ⊆ {False}) = (True ∉ set bs)" by auto

lemma int_not_emptyD:
"A ∩ B ≠ {} ⟹ ∃x. x ∈ A ∧ x ∈ B"
by (erule contrapos_np, clarsimp simp: disjoint_iff_not_equal)

definition
sum_map :: "('a ⇒ 'b) ⇒ ('c ⇒ 'd) ⇒ 'a + 'c ⇒ 'b + 'd" where
"sum_map f g x ≡ case x of Inl v ⇒ Inl (f v) | Inr v' ⇒ Inr (g v')"

lemma sum_map_simps[simp]:
"sum_map f g (Inl v) = Inl (f v)"
"sum_map f g (Inr w) = Inr (g w)"

lemma if_Some_None_eq_None:
"((if P then Some v else None) = None) = (¬ P)"
by simp

lemma CollectPairFalse [iff]:
"{(a,b). False} = {}"

lemma if_conj_dist:
"((if b then w else x) ∧ (if b then y else z) ∧ X) =
((if b then w ∧ y else x ∧ z) ∧ X)"
by simp

lemma if_P_True1:
"Q ⟹ (if P then True else Q)"
by simp

lemma if_P_True2:
"Q ⟹ (if P then Q else True)"
by simp

lemma nat_min_simps:
"(a::nat) ≤ b ⟹ min b a = a"
"a ≤ b ⟹ min a b = a"
by simp_all

lemmas mcl = mult_cancel_left [THEN iffD1, THEN make_pos_rule]

lemma pl_pl_rels: "a + b = c + d ⟹ a ≥ c ∧ b ≤ d ∨ a ≤ c ∧ b ≥ d"
for a b c d :: nat
by arith

lemmas pl_pl_rels' = add.commute [THEN [2] trans, THEN pl_pl_rels]

lemma iszero_minus:
‹iszero (- z) ⟷ iszero z›

lemma diff_le_eq': "a - b ≤ c ⟷ a ≤ b + c"
for a b c :: int
by arith

lemma zless2: "0 < (2 :: int)"
by (fact zero_less_numeral)

lemma zless2p: "0 < (2 ^ n :: int)"
by arith

lemma zle2p: "0 ≤ (2 ^ n :: int)"
by arith

lemma ex_eq_or: "(∃m. n = Suc m ∧ (m = k ∨ P m)) ⟷ n = Suc k ∨ (∃m. n = Suc m ∧ P m)"
by auto

lemma power_minus_simp: "0 < n ⟹ a ^ n = a * a ^ (n - 1)"
by (auto dest: gr0_implies_Suc)

lemma n2s_ths:
‹2 + n = Suc (Suc n)›
‹n + 2 = Suc (Suc n)›

lemma s2n_ths:
‹Suc (Suc n) = 2 + n›
‹Suc (Suc n) = n + 2›
by simp_all

lemma gt_or_eq_0: "0 < y ∨ 0 = y"
for y :: nat
by arith

lemma sum_imp_diff: "j = k + i ⟹ j - i = k"
for k :: nat
by simp

lemma le_diff_eq': "a ≤ c - b ⟷ b + a ≤ c"
for a b c :: int
by arith

lemma less_diff_eq': "a < c - b ⟷ b + a < c"
for a b c :: int
by arith

lemma diff_less_eq': "a - b < c ⟷ a < b + c"
for a b c :: int
by arith

lemma axxbyy: "a + m + m = b + n + n ⟹ a = 0 ∨ a = 1 ⟹ b = 0 ∨ b = 1 ⟹ a = b ∧ m = n"
for a b m n :: int
by arith

lemma minus_eq: "m - k = m ⟷ k = 0 ∨ m = 0"
for k m :: nat
by arith

lemma pl_pl_mm: "a + b = c + d ⟹ a - c = d - b"
for a b c d :: nat
by arith

lemmas pl_pl_mm' = add.commute [THEN [2] trans, THEN pl_pl_mm]

lemma less_le_mult': "w * c < b * c ⟹ 0 ≤ c ⟹ (w + 1) * c ≤ b * c"
for b c w :: int
apply (rule mult_right_mono)
apply (erule (1) mult_right_less_imp_less)
apply assumption
done

lemma less_le_mult: "w * c < b * c ⟹ 0 ≤ c ⟹ w * c + c ≤ b * c"
for b c w :: int
using less_le_mult' [of w c b] by (simp add: algebra_simps)

lemmas less_le_mult_minus = iffD2 [OF le_diff_eq less_le_mult,
simplified left_diff_distrib]

lemma gen_minus: "0 < n ⟹ f n = f (Suc (n - 1))"
by auto

lemma mpl_lem: "j ≤ i ⟹ k < j ⟹ i - j + k < i"
for i j k :: nat
by arith

lemmas dme = div_mult_mod_eq
lemmas dtle = div_times_less_eq_dividend
lemmas th2 = order_trans [OF order_refl [THEN [2] mult_le_mono] div_times_less_eq_dividend]

lemmas sdl = div_nat_eqI

lemma given_quot: "f > 0 ⟹ (f * l + (f - 1)) div f = l"
for f l :: nat
by (rule div_nat_eqI) (simp_all)

lemma given_quot_alt: "f > 0 ⟹ (l * f + f - Suc 0) div f = l"
for f l :: nat
apply (frule given_quot)
apply (rule trans)
prefer 2
apply (erule asm_rl)
apply (rule_tac f="λn. n div f" in arg_cong)
done

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

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 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 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 power_sub_int:
"⟦ m ≤ n; 0 < b ⟧ ⟹ b ^ n div b ^ m = (b ^ (n - m) :: int)"
apply (subgoal_tac "∃n'. n = m + n'")
apply (rule exI[where x="n - m"])
apply simp
done

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

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

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

lemma less_le_mult_nat':
"w * c < b * c ==> 0 ≤ c ==> Suc w * c ≤ b * (c::nat)"
apply (rule mult_right_mono)
apply (rule Suc_leI)
apply (erule (1) mult_right_less_imp_less)
apply assumption
done

lemma less_le_mult_nat:
‹0 < c ∧ w < b ⟹ c + w * c ≤ b * c› for b c w :: nat
using less_le_mult_nat' [of w c b] by simp

lemma p_assoc_help:
fixes p :: "'a::{ring,power,numeral,one}"
shows "p + 2^sz - 1 = p + (2^sz - 1)"
by simp

lemma pow_mono_leq_imp_lt:
"x ≤ y ⟹ x < 2 ^ y"

lemma small_powers_of_2:
"x ≥ 3 ⟹ x < 2 ^ (x - 1)"
by (induct x; simp add: suc_le_pow_2)

lemma nat_less_power_trans2:
fixes n :: nat
shows "⟦n < 2 ^ (m - k); k ≤ m⟧ ⟹ n * 2 ^ k  < 2 ^ m"
by (subst mult.commute, erule (1) nat_less_power_trans)

lemma nat_move_sub_le: "(a::nat) + b ≤ c ⟹ a ≤ c - b"
by arith

lemma plus_minus_one_rewrite:
"v + (- 1 :: ('a :: {ring, one, uminus})) ≡ v - 1"