src/HOL/Word/Misc_Numeric.thy

tuned proofs -- clarified flow of facts wrt. calculation;

(* 
  Author:  Jeremy Dawson, NICTA
*) 

header {* Useful Numerical Lemmas *}

theory Misc_Numeric
imports Main Parity
begin

lemma zmod_zsub_self [simp]: (* FIXME move to Divides.thy *) 
  "((b :: int) - a) mod a = b mod a"
  by (simp add: mod_diff_right_eq)

declare iszero_0 [iff]

lemma min_pm [simp]: "min a b + (a - b) = (a :: nat)" by arith
  
lemmas min_pm1 [simp] = trans [OF add_commute min_pm]

lemma rev_min_pm [simp]: "min b a + (a - b) = (a::nat)" by arith

lemmas rev_min_pm1 [simp] = trans [OF add_commute rev_min_pm]

lemma min_minus [simp] : "min m (m - k) = (m - k :: nat)" by arith
  
lemmas min_minus' [simp] = trans [OF min_max.inf_commute min_minus]

lemma z1pmod2:
  "(2 * b + 1) mod 2 = (1::int)" by arith

lemma emep1:
  "even n ==> even d ==> 0 <= d ==> (n + 1) mod (d :: int) = (n mod d) + 1"
  apply (simp add: add_commute)
  apply (safe dest!: even_equiv_def [THEN iffD1])
  apply (subst pos_zmod_mult_2)
   apply arith
  apply (simp add: mod_mult_mult1)
 done

lemma int_mod_lem: 
  "(0 :: int) < n ==> (0 <= b & b < n) = (b mod n = b)"
  apply safe
    apply (erule (1) mod_pos_pos_trivial)
   apply (erule_tac [!] subst)
   apply auto
  done

lemma int_mod_ge: "a < n ==> 0 < (n :: int) ==> a <= a mod n"
  apply (cases "0 <= a")
   apply (drule (1) mod_pos_pos_trivial)
   apply simp
  apply (rule order_trans [OF _ pos_mod_sign])
   apply simp
  apply assumption
  done

lemma int_mod_ge': "b < 0 ==> 0 < (n :: int) ==> b + n <= b mod n"
  by (rule int_mod_ge [where a = "b + n" and n = n, simplified])

lemma zless2:
  "0 < (2 :: int)"
  by arith

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

lemma zle2p:
  "0 \<le> (2 ^ n :: int)"
  by arith

lemma int_mod_le': "(0::int) <= b - n ==> b mod n <= b - n"
  using zmod_le_nonneg_dividend [of "b - n" "n"] by simp

lemma diff_le_eq': "(a - b \<le> c) = (a \<le> b + (c::int))" by arith

lemma m1mod2k:
  "-1 mod 2 ^ n = (2 ^ n - 1 :: int)"
  using zless2p by (rule zmod_minus1)

lemma p1mod22k':
  fixes b :: int
  shows "(1 + 2 * b) mod (2 * 2 ^ n) = 1 + 2 * (b mod 2 ^ n)"
  using zle2p by (rule pos_zmod_mult_2) 

lemma p1mod22k:
  fixes b :: int
  shows "(2 * b + 1) mod (2 * 2 ^ n) = 2 * (b mod 2 ^ n) + 1"
  by (simp add: p1mod22k' add_commute)

lemma lrlem':
  assumes d: "(i::nat) \<le> j \<or> m < j'"
  assumes R1: "i * k \<le> j * k \<Longrightarrow> R"
  assumes R2: "Suc m * k' \<le> j' * k' \<Longrightarrow> R"
  shows "R" using d
  apply safe
   apply (rule R1, erule mult_le_mono1)
  apply (rule R2, erule Suc_le_eq [THEN iffD2 [THEN mult_le_mono1]])
  done

lemma lrlem: "(0::nat) < sc ==>
    (sc - n + (n + lb * n) <= m * n) = (sc + lb * n <= m * n)"
  apply safe
   apply arith
  apply (case_tac "sc >= n")
   apply arith
  apply (insert linorder_le_less_linear [of m lb])
  apply (erule_tac k=n and k'=n in lrlem')
   apply arith
  apply simp
  done

end