Theory List-Infinite.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