Theory Util_Nat

(*  Title:      Util_Nat.thy
    Date:       Oct 2006
    Author:     David Trachtenherz
*)

section ‹Results for natural arithmetics›

theory Util_Nat
imports Main
begin

subsection ‹Some convenience arithmetic lemmata›

lemma add_1_Suc_conv: "m + 1 = Suc m" by simp
lemma sub_Suc0_sub_Suc_conv: "b - a - Suc 0 = b - Suc a" by simp

lemma Suc_diff_Suc: "m < n ⟹ Suc (n - Suc m) = n - m"
apply (rule subst[OF sub_Suc0_sub_Suc_conv])
apply (rule Suc_pred)
apply (simp only: zero_less_diff)
done

lemma nat_grSuc0_conv: "(Suc 0 < n) = (n ≠ 0 ∧ n ≠ Suc 0)"
by fastforce

lemma nat_geSucSuc0_conv: "(Suc (Suc 0) ≤ n) = (n ≠ 0 ∧ n ≠ Suc 0)"
by fastforce

lemma nat_lessSucSuc0_conv: "(n < Suc (Suc 0)) = (n = 0 ∨ n = Suc 0)"
by fastforce

lemma nat_leSuc0_conv: "(n ≤ Suc 0) = (n = 0 ∨ n = Suc 0)"
by fastforce

lemma mult_pred: "(m - Suc 0) * n = m * n - n"
by (simp add: diff_mult_distrib)

lemma mult_pred_right: "m * (n - Suc 0) = m * n - m"
by (simp add: diff_mult_distrib2)

lemma gr_implies_gr0: "m < (n::nat) ⟹ 0 < n" by simp

corollary mult_cancel1_gr0: "
  (0::nat) < k ⟹ (k * m = k * n) = (m = n)" by simp
corollary mult_cancel2_gr0: "
  (0::nat) < k ⟹ (m * k = n * k) = (m = n)" by simp

corollary mult_le_cancel1_gr0: "
  (0::nat) < k ⟹ (k * m ≤ k * n) = (m ≤ n)" by simp
corollary mult_le_cancel2_gr0: "
  (0::nat) < k ⟹ (m * k ≤ n * k) = (m ≤ n)" by simp

lemma gr0_imp_self_le_mult1: "0 < (k::nat) ⟹ m ≤ m * k"
by (drule Suc_leI, drule mult_le_mono[OF order_refl], simp)

lemma gr0_imp_self_le_mult2: "0 < (k::nat) ⟹ m ≤ k * m"
by (subst mult.commute, rule gr0_imp_self_le_mult1)

lemma less_imp_Suc_mult_le: "m < n ⟹ Suc m * k ≤ n * k"
by (rule mult_le_mono1, simp)

lemma less_imp_Suc_mult_pred_less: "⟦ m < n; 0 < k ⟧ ⟹ Suc m * k - Suc 0 < n * k"
apply (rule Suc_le_lessD)
apply (simp only: Suc_pred[OF nat_0_less_mult_iff[THEN iffD2, OF conjI, OF zero_less_Suc]])
apply (rule less_imp_Suc_mult_le, assumption)
done

lemma ord_zero_less_diff: "(0 < (b::'a::ordered_ab_group_add) - a) = (a < b)"
by (simp add: less_diff_eq)

lemma ord_zero_le_diff: "(0 ≤ (b::'a::ordered_ab_group_add) - a) = (a ≤ b)"
by (simp add: le_diff_eq)

text ‹‹diff_diff_right› in rule format›
lemmas diff_diff_right = Nat.diff_diff_right[rule_format]


lemma less_add1: "(0::nat) < j ⟹ i < i + j" by simp
lemma less_add2: "(0::nat) < j ⟹ i < j + i" by simp

lemma add_lessD2: "i + j < (k::nat) ⟹ j < k" by simp

lemma add_le_mono2: "i ≤ (j::nat) ⟹ k + i ≤ k + j" by simp

lemma add_less_mono2: "i < (j::nat) ⟹ k + i < k + j" by simp


lemma diff_less_self: "⟦ (0::nat) < i;  0 < j ⟧ ⟹ i - j < i" by simp

lemma
  ge_less_neq_conv: "((a::'a::linorder) ≤ n) = (∀x. x < a ⟶ n ≠ x)" and
  le_greater_neq_conv: "(n ≤ (a::'a::linorder)) = (∀x. a < x ⟶ n ≠ x)"
by (subst linorder_not_less[symmetric], blast)+
lemma
  greater_le_neq_conv: "((a::'a::linorder) < n) = (∀x. x ≤ a ⟶ n ≠ x)" and
  less_ge_neq_conv: "(n < (a::'a::linorder)) = (∀x. a ≤ x ⟶ n ≠ x)"
by (subst linorder_not_le[symmetric], blast)+



text ‹Lemmas for @term{abs} function›

lemma leq_pos_imp_abs_leq: "⟦ 0 ≤ (a::'a::ordered_ab_group_add_abs); a ≤ b ⟧ ⟹ ¦a¦ ≤ ¦b¦"
by simp
lemma leq_neg_imp_abs_geq: "⟦ (a::'a::ordered_ab_group_add_abs) ≤ 0; b ≤ a ⟧ ⟹ ¦a¦ ≤ ¦b¦"
by simp
lemma abs_range: "⟦ 0 ≤ (a::'a::{ordered_ab_group_add_abs,abs_if}); -a ≤ x; x ≤ a ⟧ ⟹ ¦x¦ ≤ a"
apply (clarsimp simp: abs_if)
apply (rule neg_le_iff_le[THEN iffD1], simp)
done



text ‹Lemmas for @term{sgn} function›

lemma sgn_abs:"(x::'a::linordered_idom) ≠ 0 ⟹ ¦sgn x¦ = 1"
by (case_tac "x < 0", simp+)
lemma sgn_mult_abs:"¦x¦ * ¦sgn (a::'a::linordered_idom)¦ = ¦x * sgn a¦"
by (fastforce simp add: sgn_if abs_if)
lemma abs_imp_sgn_abs: "¦a¦ = ¦b¦ ⟹ ¦sgn (a::'a::linordered_idom)¦ = ¦sgn b¦"
by (fastforce simp add: abs_if)
lemma sgn_mono: "a ≤ b ⟹ sgn (a::'a::{linordered_idom,linordered_semidom}) ≤ sgn b"
by (auto simp add: sgn_if)


subsection ‹Additional facts about inequalities›

lemma add_diff_le: "k ≤ n ⟹ m + k - n ≤ (m::nat)"
by (case_tac "m + k < n", simp_all)

lemma less_add_diff: "k < (n::nat) ⟹ m < n + m - k"

by (rule add_less_imp_less_right[of _ k], simp)

lemma add_diff_less: "⟦ k < n; 0 < m ⟧ ⟹ m + k - n < (m::nat)"
by (case_tac "m + k < n", simp_all)


lemma add_le_imp_le_diff1: "i + k ≤ j ⟹ i ≤ j - (k::nat)"
by (case_tac "k ≤ j", simp_all)

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

lemma diff_less_imp_less_add: "j - (k::nat) < i ⟹ j < i + k" by simp

lemma diff_less_conv: "0 < i ⟹ (j - (k::nat) < i) = (j < i + k)"
by (safe, simp_all)

lemma le_diff_swap: "⟦ i ≤ (k::nat); j ≤ k ⟧ ⟹ (k - j ≤ i) = (k - i ≤ j)"
by (safe, simp_all)

lemma diff_less_imp_swap: "⟦ 0 < (i::nat); k - i < j ⟧ ⟹ (k - j < i)" by simp
lemma diff_less_swap: "⟦ 0 < (i::nat); 0 < j ⟧ ⟹ (k - j < i) = (k - i < j)"
by (blast intro: diff_less_imp_swap)

lemma less_diff_imp_less: "(i::nat) < j - m ⟹ i < j" by simp
lemma le_diff_imp_le: "(i::nat) ≤ j - m ⟹ i ≤ j" by simp

lemma less_diff_le_imp_less: "⟦ (i::nat) < j - m; n ≤ m ⟧ ⟹ i < j - n" by simp
lemma le_diff_le_imp_le: "⟦ (i::nat) ≤ j - m; n ≤ m ⟧ ⟹ i ≤ j - n" by simp

lemma le_imp_diff_le: "(j::nat) ≤ k ⟹ j - n ≤ k" by simp


subsection ‹Inequalities for Suc and pred›

corollary less_eq_le_pred: "0 < (n::nat) ⟹ (m < n) = (m ≤ n - Suc 0)"
by (safe, simp_all)

corollary less_imp_le_pred: "m < n ⟹ m ≤ n - Suc 0" by simp
corollary le_pred_imp_less: "⟦ 0 < n; m ≤ n - Suc 0 ⟧ ⟹ m < n" by simp

corollary pred_less_eq_le: "0 < m ⟹ (m - Suc 0 < n) = (m ≤ n)"
by (safe, simp_all)
corollary pred_less_imp_le: "m - Suc 0 < n ⟹ m ≤ n" by simp
corollary le_imp_pred_less: "⟦ 0 < m; m ≤ n ⟧ ⟹ m - Suc 0 < n" by simp

lemma diff_add_inverse_Suc: "n < m ⟹ n + (m - Suc n) = m - Suc 0" by simp

lemma pred_mono: "⟦ m < n; 0 < m ⟧ ⟹ m - Suc 0 < n - Suc 0" by simp
corollary pred_Suc_mono: "⟦ m < Suc n; 0 < m ⟧ ⟹ m - Suc 0 < n" by simp

lemma Suc_less_pred_conv: "(Suc m < n) = (m < n - Suc 0)" by (safe, simp_all)
lemma Suc_le_pred_conv: "0 < n ⟹ (Suc m ≤ n) = (m ≤ n - Suc 0)" by (safe, simp_all)
lemma Suc_le_imp_le_pred: "Suc m ≤ n ⟹ m ≤ n - Suc 0" by simp


subsection ‹Additional facts about cancellation in (in-)equalities›

lemma diff_cancel_imp_eq: "⟦ 0 < (n::nat);  n + i - j = n ⟧ ⟹ i = j" by simp

lemma nat_diff_left_cancel_less: "k - m < k - (n::nat) ⟹ n < m" by simp
lemma nat_diff_right_cancel_less: "n - k < (m::nat) - k ⟹ n < m" by simp

lemma nat_diff_left_cancel_le1: "⟦ k - m ≤ k - (n::nat); m < k ⟧ ⟹ n ≤ m" by simp
lemma nat_diff_left_cancel_le2: "⟦ k - m ≤ k - (n::nat); n ≤ k ⟧ ⟹ n ≤ m" by simp

lemma nat_diff_right_cancel_le1: "⟦ m - k ≤ n - (k::nat); k < m ⟧ ⟹ m ≤ n" by simp
lemma nat_diff_right_cancel_le2: "⟦ m - k ≤ n - (k::nat); k ≤ n ⟧ ⟹ m ≤ n" by simp

lemma nat_diff_left_cancel_eq1: "⟦ k - m = k - (n::nat); m < k ⟧ ⟹ m = n" by simp
lemma nat_diff_left_cancel_eq2: "⟦ k - m = k - (n::nat); n < k ⟧ ⟹ m = n" by simp

lemma nat_diff_right_cancel_eq1: "⟦ m - k = n - (k::nat); k < m ⟧ ⟹ m = n" by simp
lemma nat_diff_right_cancel_eq2: "⟦ m - k = n - (k::nat); k < n ⟧ ⟹ m = n" by simp

lemma eq_diff_left_iff: "⟦ (m::nat) ≤ k; n ≤ k⟧ ⟹ (k - m = k - n) = (m = n)"
by (safe, simp_all)

lemma eq_imp_diff_eq: "m = (n::nat) ⟹ m - k = n - k" by simp


text ‹List of definitions and lemmas›

thm
  Nat.add_Suc_right
  add_1_Suc_conv
  sub_Suc0_sub_Suc_conv

thm
  Nat.mult_cancel1
  Nat.mult_cancel2
  mult_cancel1_gr0
  mult_cancel2_gr0

thm
  Nat.add_lessD1
  add_lessD2

thm
  Nat.zero_less_diff
  ord_zero_less_diff
  ord_zero_le_diff

thm
  le_add_diff
  add_diff_le
  less_add_diff
  add_diff_less

thm
  Nat.le_diff_conv le_diff_conv2
  Nat.less_diff_conv
  diff_less_imp_less_add
  diff_less_conv

thm
  le_diff_swap
  diff_less_imp_swap
  diff_less_swap

thm
  less_diff_imp_less
  le_diff_imp_le

thm
  less_diff_le_imp_less
  le_diff_le_imp_le

thm
  Nat.less_imp_diff_less
  le_imp_diff_le

thm
  Nat.less_Suc_eq_le
  less_eq_le_pred
  less_imp_le_pred
  le_pred_imp_less

thm
  Nat.Suc_le_eq
  pred_less_eq_le
  pred_less_imp_le
  le_imp_pred_less

thm
  diff_cancel_imp_eq
thm
  diff_add_inverse_Suc
thm
  Nat.nat_add_left_cancel_less
  Nat.nat_add_left_cancel_le
  add_right_cancel
  add_left_cancel
  Nat.eq_diff_iff
  Nat.less_diff_iff
  Nat.le_diff_iff
thm
  nat_diff_left_cancel_less
  nat_diff_right_cancel_less
thm
  nat_diff_left_cancel_le1
  nat_diff_left_cancel_le2
  nat_diff_right_cancel_le1
  nat_diff_right_cancel_le2
thm
  nat_diff_left_cancel_eq1
  nat_diff_left_cancel_eq2
  nat_diff_right_cancel_eq1
  nat_diff_right_cancel_eq2

thm
  Nat.eq_diff_iff
  eq_diff_left_iff

thm
  add_right_cancel add_left_cancel
  Nat.diff_le_mono
  eq_imp_diff_eq

end