prefer one theory for misc material
authorhaftmann
Tue Apr 16 19:50:05 2019 +0000 (7 days ago)
changeset 7017056727602d0a5
parent 70169 8bb835f10a39
child 70171 3173d7878274
prefer one theory for misc material
src/HOL/Word/Bit_Representation.thy
src/HOL/Word/Bits_Int.thy
src/HOL/Word/Misc_Arithmetic.thy
src/HOL/Word/Misc_Numeric.thy
src/HOL/Word/Word.thy
src/HOL/Word/Word_Miscellaneous.thy
     1.1 --- a/src/HOL/Word/Bit_Representation.thy	Tue Apr 16 19:50:03 2019 +0000
     1.2 +++ b/src/HOL/Word/Bit_Representation.thy	Tue Apr 16 19:50:05 2019 +0000
     1.3 @@ -5,9 +5,37 @@
     1.4  section \<open>Integers as implicit bit strings\<close>
     1.5  
     1.6  theory Bit_Representation
     1.7 -  imports Misc_Numeric
     1.8 +  imports Main
     1.9  begin
    1.10  
    1.11 +lemma int_mod_lem: "0 < n \<Longrightarrow> 0 \<le> b \<and> b < n \<longleftrightarrow> b mod n = b"
    1.12 +  for b n :: int
    1.13 +  apply safe
    1.14 +    apply (erule (1) mod_pos_pos_trivial)
    1.15 +   apply (erule_tac [!] subst)
    1.16 +   apply auto
    1.17 +  done
    1.18 +
    1.19 +lemma int_mod_ge: "a < n \<Longrightarrow> 0 < n \<Longrightarrow> a \<le> a mod n"
    1.20 +  for a n :: int
    1.21 +  by (metis dual_order.trans le_cases mod_pos_pos_trivial pos_mod_conj)
    1.22 +
    1.23 +lemma int_mod_ge': "b < 0 \<Longrightarrow> 0 < n \<Longrightarrow> b + n \<le> b mod n"
    1.24 +  for b n :: int
    1.25 +  by (metis add_less_same_cancel2 int_mod_ge mod_add_self2)
    1.26 +
    1.27 +lemma int_mod_le': "0 \<le> b - n \<Longrightarrow> b mod n \<le> b - n"
    1.28 +  for b n :: int
    1.29 +  by (metis minus_mod_self2 zmod_le_nonneg_dividend)
    1.30 +
    1.31 +lemma emep1: "even n \<Longrightarrow> even d \<Longrightarrow> 0 \<le> d \<Longrightarrow> (n + 1) mod d = (n mod d) + 1"
    1.32 +  for n d :: int
    1.33 +  by (auto simp add: pos_zmod_mult_2 add.commute dvd_def)
    1.34 +
    1.35 +lemma m1mod2k: "- 1 mod 2 ^ n = (2 ^ n - 1 :: int)"
    1.36 +  by (rule zmod_minus1) simp
    1.37 +
    1.38 +
    1.39  subsection \<open>Constructors and destructors for binary integers\<close>
    1.40  
    1.41  definition Bit :: "int \<Rightarrow> bool \<Rightarrow> int"  (infixl "BIT" 90)
    1.42 @@ -563,7 +591,9 @@
    1.43    apply (unfold no_bintr_alt1)
    1.44    apply (auto simp add: image_iff)
    1.45    apply (rule exI)
    1.46 -  apply (auto intro: int_mod_lem [THEN iffD1, symmetric])
    1.47 +  apply (rule sym)
    1.48 +  using int_mod_lem [symmetric, of "2 ^ n"]
    1.49 +  apply auto
    1.50    done
    1.51  
    1.52  lemma no_sbintr_alt2: "sbintrunc n = (\<lambda>w. (w + 2 ^ n) mod 2 ^ Suc n - 2 ^ n :: int)"
    1.53 @@ -572,15 +602,15 @@
    1.54  lemma range_sbintrunc: "range (sbintrunc n) = {i. - (2 ^ n) \<le> i \<and> i < 2 ^ n}"
    1.55    apply (unfold no_sbintr_alt2)
    1.56    apply (auto simp add: image_iff eq_diff_eq)
    1.57 +
    1.58    apply (rule exI)
    1.59    apply (auto intro: int_mod_lem [THEN iffD1, symmetric])
    1.60    done
    1.61  
    1.62  lemma sb_inc_lem: "a + 2^k < 0 \<Longrightarrow> a + 2^k + 2^(Suc k) \<le> (a + 2^k) mod 2^(Suc k)"
    1.63    for a :: int
    1.64 -  apply (erule int_mod_ge' [where n = "2 ^ (Suc k)" and b = "a + 2 ^ k", simplified zless2p])
    1.65 -  apply (rule TrueI)
    1.66 -  done
    1.67 +  using int_mod_ge' [where n = "2 ^ (Suc k)" and b = "a + 2 ^ k"]
    1.68 +  by simp
    1.69  
    1.70  lemma sb_inc_lem': "a < - (2^k) \<Longrightarrow> a + 2^k + 2^(Suc k) \<le> (a + 2^k) mod 2^(Suc k)"
    1.71    for a :: int
    1.72 @@ -600,8 +630,6 @@
    1.73  lemma sbintrunc_dec: "x \<ge> (2 ^ n) \<Longrightarrow> x - 2 ^ (Suc n) >= sbintrunc n x"
    1.74    unfolding no_sbintr_alt2 by (drule sb_dec_lem') simp
    1.75  
    1.76 -lemmas m2pths = pos_mod_sign pos_mod_bound [OF zless2p]
    1.77 -
    1.78  lemma bintr_ge0: "0 \<le> bintrunc n w"
    1.79    by (simp add: bintrunc_mod2p)
    1.80  
    1.81 @@ -815,7 +843,7 @@
    1.82    apply (simp add: bin_rest_def zdiv_zmult2_eq)
    1.83    apply (case_tac b rule: bin_exhaust)
    1.84    apply simp
    1.85 -  apply (simp add: Bit_def mod_mult_mult1 p1mod22k)
    1.86 +  apply (simp add: Bit_def mod_mult_mult1 pos_zmod_mult_2 add.commute)
    1.87    done
    1.88  
    1.89  end
     2.1 --- a/src/HOL/Word/Bits_Int.thy	Tue Apr 16 19:50:03 2019 +0000
     2.2 +++ b/src/HOL/Word/Bits_Int.thy	Tue Apr 16 19:50:05 2019 +0000
     2.3 @@ -370,7 +370,7 @@
     2.4    have "2 * (bin mod 2 ^ n) + 1 = (2 * bin mod 2 ^ Suc n) + 1"
     2.5      by (simp add: mod_mult_mult1)
     2.6    also have "\<dots> = ((2 * bin mod 2 ^ Suc n) + 1) mod 2 ^ Suc n"
     2.7 -    by (simp add: ac_simps p1mod22k')
     2.8 +    by (simp add: ac_simps pos_zmod_mult_2)
     2.9    also have "\<dots> = (2 * bin + 1) mod 2 ^ Suc n"
    2.10      by (simp only: mod_simps)
    2.11    finally show ?thesis
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Word/Misc_Arithmetic.thy	Tue Apr 16 19:50:05 2019 +0000
     3.3 @@ -0,0 +1,433 @@
     3.4 +(*  Title:      HOL/Word/Misc_Arithmetic.thy  *)
     3.5 +
     3.6 +section \<open>Miscellaneous lemmas, mostly for arithmetic\<close>
     3.7 +
     3.8 +theory Misc_Arithmetic
     3.9 +  imports "HOL-Library.Bit" Bit_Representation
    3.10 +begin
    3.11 +
    3.12 +lemma one_mod_exp_eq_one [simp]:
    3.13 +  "1 mod (2 * 2 ^ n) = (1::int)"
    3.14 +  using power_gt1 [of 2 n] by (auto intro: mod_pos_pos_trivial)
    3.15 +  
    3.16 +lemma mod_2_neq_1_eq_eq_0: "k mod 2 \<noteq> 1 \<longleftrightarrow> k mod 2 = 0"
    3.17 +  for k :: int
    3.18 +  by (fact not_mod_2_eq_1_eq_0)
    3.19 +
    3.20 +lemma z1pmod2: "(2 * b + 1) mod 2 = (1::int)"
    3.21 +  for b :: int
    3.22 +  by arith
    3.23 +
    3.24 +lemma diff_le_eq': "a - b \<le> c \<longleftrightarrow> a \<le> b + c"
    3.25 +  for a b c :: int
    3.26 +  by arith
    3.27 +
    3.28 +lemma zless2: "0 < (2 :: int)"
    3.29 +  by (fact zero_less_numeral)
    3.30 +
    3.31 +lemma zless2p: "0 < (2 ^ n :: int)"
    3.32 +  by arith
    3.33 +
    3.34 +lemma zle2p: "0 \<le> (2 ^ n :: int)"
    3.35 +  by arith
    3.36 +
    3.37 +lemma p1mod22k': "(1 + 2 * b) mod (2 * 2 ^ n) = 1 + 2 * (b mod 2 ^ n)"
    3.38 +  for b :: int
    3.39 +  using zle2p by (rule pos_zmod_mult_2)
    3.40 +
    3.41 +lemma p1mod22k: "(2 * b + 1) mod (2 * 2 ^ n) = 2 * (b mod 2 ^ n) + 1"
    3.42 +  for b :: int
    3.43 +  by (simp add: p1mod22k' add.commute)
    3.44 +
    3.45 +lemma ex_eq_or: "(\<exists>m. n = Suc m \<and> (m = k \<or> P m)) \<longleftrightarrow> n = Suc k \<or> (\<exists>m. n = Suc m \<and> P m)"
    3.46 +  by auto
    3.47 +
    3.48 +lemma power_minus_simp: "0 < n \<Longrightarrow> a ^ n = a * a ^ (n - 1)"
    3.49 +  by (auto dest: gr0_implies_Suc)
    3.50 +
    3.51 +lemma funpow_minus_simp: "0 < n \<Longrightarrow> f ^^ n = f \<circ> f ^^ (n - 1)"
    3.52 +  by (auto dest: gr0_implies_Suc)
    3.53 +
    3.54 +lemma power_numeral: "a ^ numeral k = a * a ^ (pred_numeral k)"
    3.55 +  by (simp add: numeral_eq_Suc)
    3.56 +
    3.57 +lemma funpow_numeral [simp]: "f ^^ numeral k = f \<circ> f ^^ (pred_numeral k)"
    3.58 +  by (simp add: numeral_eq_Suc)
    3.59 +
    3.60 +lemma replicate_numeral [simp]: "replicate (numeral k) x = x # replicate (pred_numeral k) x"
    3.61 +  by (simp add: numeral_eq_Suc)
    3.62 +
    3.63 +lemma rco_alt: "(f \<circ> g) ^^ n \<circ> f = f \<circ> (g \<circ> f) ^^ n"
    3.64 +  apply (rule ext)
    3.65 +  apply (induct n)
    3.66 +   apply (simp_all add: o_def)
    3.67 +  done
    3.68 +
    3.69 +lemma list_exhaust_size_gt0:
    3.70 +  assumes "\<And>a list. y = a # list \<Longrightarrow> P"
    3.71 +  shows "0 < length y \<Longrightarrow> P"
    3.72 +  apply (cases y)
    3.73 +   apply simp
    3.74 +  apply (rule assms)
    3.75 +  apply fastforce
    3.76 +  done
    3.77 +
    3.78 +lemma list_exhaust_size_eq0:
    3.79 +  assumes "y = [] \<Longrightarrow> P"
    3.80 +  shows "length y = 0 \<Longrightarrow> P"
    3.81 +  apply (cases y)
    3.82 +   apply (rule assms)
    3.83 +   apply simp
    3.84 +  apply simp
    3.85 +  done
    3.86 +
    3.87 +lemma size_Cons_lem_eq: "y = xa # list \<Longrightarrow> size y = Suc k \<Longrightarrow> size list = k"
    3.88 +  by auto
    3.89 +
    3.90 +lemmas ls_splits = prod.split prod.split_asm if_split_asm
    3.91 +
    3.92 +\<comment> \<open>simplifications for specific word lengths\<close>
    3.93 +lemmas n2s_ths [THEN eq_reflection] = add_2_eq_Suc add_2_eq_Suc'
    3.94 +
    3.95 +lemmas s2n_ths = n2s_ths [symmetric]
    3.96 +
    3.97 +lemma and_len: "xs = ys \<Longrightarrow> xs = ys \<and> length xs = length ys"
    3.98 +  by auto
    3.99 +
   3.100 +lemma size_if: "size (if p then xs else ys) = (if p then size xs else size ys)"
   3.101 +  by auto
   3.102 +
   3.103 +lemma tl_if: "tl (if p then xs else ys) = (if p then tl xs else tl ys)"
   3.104 +  by auto
   3.105 +
   3.106 +lemma hd_if: "hd (if p then xs else ys) = (if p then hd xs else hd ys)"
   3.107 +  by auto
   3.108 +
   3.109 +lemma if_Not_x: "(if p then \<not> x else x) = (p = (\<not> x))"
   3.110 +  by auto
   3.111 +
   3.112 +lemma if_x_Not: "(if p then x else \<not> x) = (p = x)"
   3.113 +  by auto
   3.114 +
   3.115 +lemma if_same_and: "(If p x y \<and> If p u v) = (if p then x \<and> u else y \<and> v)"
   3.116 +  by auto
   3.117 +
   3.118 +lemma if_same_eq: "(If p x y  = (If p u v)) = (if p then x = u else y = v)"
   3.119 +  by auto
   3.120 +
   3.121 +lemma if_same_eq_not: "(If p x y = (\<not> If p u v)) = (if p then x = (\<not> u) else y = (\<not> v))"
   3.122 +  by auto
   3.123 +
   3.124 +\<comment> \<open>note -- \<open>if_Cons\<close> can cause blowup in the size, if \<open>p\<close> is complex, so make a simproc\<close>
   3.125 +lemma if_Cons: "(if p then x # xs else y # ys) = If p x y # If p xs ys"
   3.126 +  by auto
   3.127 +
   3.128 +lemma if_single: "(if xc then [xab] else [an]) = [if xc then xab else an]"
   3.129 +  by auto
   3.130 +
   3.131 +lemma if_bool_simps:
   3.132 +  "If p True y = (p \<or> y) \<and> If p False y = (\<not> p \<and> y) \<and>
   3.133 +    If p y True = (p \<longrightarrow> y) \<and> If p y False = (p \<and> y)"
   3.134 +  by auto
   3.135 +
   3.136 +lemmas if_simps =
   3.137 +  if_x_Not if_Not_x if_cancel if_True if_False if_bool_simps
   3.138 +
   3.139 +lemmas seqr = eq_reflection [where x = "size w"] for w (* FIXME: delete *)
   3.140 +
   3.141 +lemma the_elemI: "y = {x} \<Longrightarrow> the_elem y = x"
   3.142 +  by simp
   3.143 +
   3.144 +lemma nonemptyE: "S \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> S \<Longrightarrow> R) \<Longrightarrow> R"
   3.145 +  by auto
   3.146 +
   3.147 +lemma gt_or_eq_0: "0 < y \<or> 0 = y"
   3.148 +  for y :: nat
   3.149 +  by arith
   3.150 +
   3.151 +lemmas xtr1 = xtrans(1)
   3.152 +lemmas xtr2 = xtrans(2)
   3.153 +lemmas xtr3 = xtrans(3)
   3.154 +lemmas xtr4 = xtrans(4)
   3.155 +lemmas xtr5 = xtrans(5)
   3.156 +lemmas xtr6 = xtrans(6)
   3.157 +lemmas xtr7 = xtrans(7)
   3.158 +lemmas xtr8 = xtrans(8)
   3.159 +
   3.160 +lemmas nat_simps = diff_add_inverse2 diff_add_inverse
   3.161 +lemmas nat_iffs = le_add1 le_add2
   3.162 +
   3.163 +lemma sum_imp_diff: "j = k + i \<Longrightarrow> j - i = k"
   3.164 +  for k :: nat
   3.165 +  by arith
   3.166 +
   3.167 +lemmas pos_mod_sign2 = zless2 [THEN pos_mod_sign [where b = "2::int"]]
   3.168 +lemmas pos_mod_bound2 = zless2 [THEN pos_mod_bound [where b = "2::int"]]
   3.169 +
   3.170 +lemma nmod2: "n mod 2 = 0 \<or> n mod 2 = 1"
   3.171 +  for n :: int
   3.172 +  by arith
   3.173 +
   3.174 +lemmas eme1p = emep1 [simplified add.commute]
   3.175 +
   3.176 +lemma le_diff_eq': "a \<le> c - b \<longleftrightarrow> b + a \<le> c"
   3.177 +  for a b c :: int
   3.178 +  by arith
   3.179 +
   3.180 +lemma less_diff_eq': "a < c - b \<longleftrightarrow> b + a < c"
   3.181 +  for a b c :: int
   3.182 +  by arith
   3.183 +
   3.184 +lemma diff_less_eq': "a - b < c \<longleftrightarrow> a < b + c"
   3.185 +  for a b c :: int
   3.186 +  by arith
   3.187 +
   3.188 +lemmas m1mod22k = mult_pos_pos [OF zless2 zless2p, THEN zmod_minus1]
   3.189 +
   3.190 +lemma z1pdiv2: "(2 * b + 1) div 2 = b"
   3.191 +  for b :: int
   3.192 +  by arith
   3.193 +
   3.194 +lemmas zdiv_le_dividend = xtr3 [OF div_by_1 [symmetric] zdiv_mono2,
   3.195 +  simplified int_one_le_iff_zero_less, simplified]
   3.196 +
   3.197 +lemma axxbyy: "a + m + m = b + n + n \<Longrightarrow> a = 0 \<or> a = 1 \<Longrightarrow> b = 0 \<or> b = 1 \<Longrightarrow> a = b \<and> m = n"
   3.198 +  for a b m n :: int
   3.199 +  by arith
   3.200 +
   3.201 +lemma axxmod2: "(1 + x + x) mod 2 = 1 \<and> (0 + x + x) mod 2 = 0"
   3.202 +  for x :: int
   3.203 +  by arith
   3.204 +
   3.205 +lemma axxdiv2: "(1 + x + x) div 2 = x \<and> (0 + x + x) div 2 = x"
   3.206 +  for x :: int
   3.207 +  by arith
   3.208 +
   3.209 +lemmas iszero_minus =
   3.210 +  trans [THEN trans, OF iszero_def neg_equal_0_iff_equal iszero_def [symmetric]]
   3.211 +
   3.212 +lemmas zadd_diff_inverse =
   3.213 +  trans [OF diff_add_cancel [symmetric] add.commute]
   3.214 +
   3.215 +lemmas add_diff_cancel2 =
   3.216 +  add.commute [THEN diff_eq_eq [THEN iffD2]]
   3.217 +
   3.218 +lemmas rdmods [symmetric] = mod_minus_eq
   3.219 +  mod_diff_left_eq mod_diff_right_eq mod_add_left_eq
   3.220 +  mod_add_right_eq mod_mult_right_eq mod_mult_left_eq
   3.221 +
   3.222 +lemma mod_plus_right: "(a + x) mod m = (b + x) mod m \<longleftrightarrow> a mod m = b mod m"
   3.223 +  for a b m x :: nat
   3.224 +  by (induct x) (simp_all add: mod_Suc, arith)
   3.225 +
   3.226 +lemma nat_minus_mod: "(n - n mod m) mod m = 0"
   3.227 +  for m n :: nat
   3.228 +  by (induct n) (simp_all add: mod_Suc)
   3.229 +
   3.230 +lemmas nat_minus_mod_plus_right =
   3.231 +  trans [OF nat_minus_mod mod_0 [symmetric],
   3.232 +    THEN mod_plus_right [THEN iffD2], simplified]
   3.233 +
   3.234 +lemmas push_mods' = mod_add_eq
   3.235 +  mod_mult_eq mod_diff_eq
   3.236 +  mod_minus_eq
   3.237 +
   3.238 +lemmas push_mods = push_mods' [THEN eq_reflection]
   3.239 +lemmas pull_mods = push_mods [symmetric] rdmods [THEN eq_reflection]
   3.240 +
   3.241 +lemma nat_mod_eq: "b < n \<Longrightarrow> a mod n = b mod n \<Longrightarrow> a mod n = b"
   3.242 +  for a b n :: nat
   3.243 +  by (induct a) auto
   3.244 +
   3.245 +lemmas nat_mod_eq' = refl [THEN [2] nat_mod_eq]
   3.246 +
   3.247 +lemma nat_mod_lem: "0 < n \<Longrightarrow> b < n \<longleftrightarrow> b mod n = b"
   3.248 +  for b n :: nat
   3.249 +  apply safe
   3.250 +   apply (erule nat_mod_eq')
   3.251 +  apply (erule subst)
   3.252 +  apply (erule mod_less_divisor)
   3.253 +  done
   3.254 +
   3.255 +lemma mod_nat_add: "x < z \<Longrightarrow> y < z \<Longrightarrow> (x + y) mod z = (if x + y < z then x + y else x + y - z)"
   3.256 +  for x y z :: nat
   3.257 +  apply (rule nat_mod_eq)
   3.258 +   apply auto
   3.259 +  apply (rule trans)
   3.260 +   apply (rule le_mod_geq)
   3.261 +   apply simp
   3.262 +  apply (rule nat_mod_eq')
   3.263 +  apply arith
   3.264 +  done
   3.265 +
   3.266 +lemma mod_nat_sub: "x < z \<Longrightarrow> (x - y) mod z = x - y"
   3.267 +  for x y :: nat
   3.268 +  by (rule nat_mod_eq') arith
   3.269 +
   3.270 +lemma int_mod_eq: "0 \<le> b \<Longrightarrow> b < n \<Longrightarrow> a mod n = b mod n \<Longrightarrow> a mod n = b"
   3.271 +  for a b n :: int
   3.272 +  by (metis mod_pos_pos_trivial)
   3.273 +
   3.274 +lemmas int_mod_eq' = mod_pos_pos_trivial (* FIXME delete *)
   3.275 +
   3.276 +lemmas int_mod_le = zmod_le_nonneg_dividend (* FIXME: delete *)
   3.277 +
   3.278 +lemma mod_add_if_z:
   3.279 +  "x < z \<Longrightarrow> y < z \<Longrightarrow> 0 \<le> y \<Longrightarrow> 0 \<le> x \<Longrightarrow> 0 \<le> z \<Longrightarrow>
   3.280 +    (x + y) mod z = (if x + y < z then x + y else x + y - z)"
   3.281 +  for x y z :: int
   3.282 +  by (auto intro: int_mod_eq)
   3.283 +
   3.284 +lemma mod_sub_if_z:
   3.285 +  "x < z \<Longrightarrow> y < z \<Longrightarrow> 0 \<le> y \<Longrightarrow> 0 \<le> x \<Longrightarrow> 0 \<le> z \<Longrightarrow>
   3.286 +    (x - y) mod z = (if y \<le> x then x - y else x - y + z)"
   3.287 +  for x y z :: int
   3.288 +  by (auto intro: int_mod_eq)
   3.289 +
   3.290 +lemmas zmde = mult_div_mod_eq [symmetric, THEN diff_eq_eq [THEN iffD2], symmetric]
   3.291 +lemmas mcl = mult_cancel_left [THEN iffD1, THEN make_pos_rule]
   3.292 +
   3.293 +(* already have this for naturals, div_mult_self1/2, but not for ints *)
   3.294 +lemma zdiv_mult_self: "m \<noteq> 0 \<Longrightarrow> (a + m * n) div m = a div m + n"
   3.295 +  for a m n :: int
   3.296 +  apply (rule mcl)
   3.297 +   prefer 2
   3.298 +   apply (erule asm_rl)
   3.299 +  apply (simp add: zmde ring_distribs)
   3.300 +  done
   3.301 +
   3.302 +lemma mod_power_lem: "a > 1 \<Longrightarrow> a ^ n mod a ^ m = (if m \<le> n then 0 else a ^ n)"
   3.303 +  for a :: int
   3.304 +  by (simp add: mod_eq_0_iff_dvd le_imp_power_dvd)
   3.305 +
   3.306 +lemma pl_pl_rels: "a + b = c + d \<Longrightarrow> a \<ge> c \<and> b \<le> d \<or> a \<le> c \<and> b \<ge> d"
   3.307 +  for a b c d :: nat
   3.308 +  by arith
   3.309 +
   3.310 +lemmas pl_pl_rels' = add.commute [THEN [2] trans, THEN pl_pl_rels]
   3.311 +
   3.312 +lemma minus_eq: "m - k = m \<longleftrightarrow> k = 0 \<or> m = 0"
   3.313 +  for k m :: nat
   3.314 +  by arith
   3.315 +
   3.316 +lemma pl_pl_mm: "a + b = c + d \<Longrightarrow> a - c = d - b"
   3.317 +  for a b c d :: nat
   3.318 +  by arith
   3.319 +
   3.320 +lemmas pl_pl_mm' = add.commute [THEN [2] trans, THEN pl_pl_mm]
   3.321 +
   3.322 +lemmas dme = div_mult_mod_eq
   3.323 +lemmas dtle = div_times_less_eq_dividend
   3.324 +lemmas th2 = order_trans [OF order_refl [THEN [2] mult_le_mono] div_times_less_eq_dividend]
   3.325 +
   3.326 +lemma td_gal: "0 < c \<Longrightarrow> a \<ge> b * c \<longleftrightarrow> a div c \<ge> b"
   3.327 +  for a b c :: nat
   3.328 +  apply safe
   3.329 +   apply (erule (1) xtr4 [OF div_le_mono div_mult_self_is_m])
   3.330 +  apply (erule th2)
   3.331 +  done
   3.332 +
   3.333 +lemmas td_gal_lt = td_gal [simplified not_less [symmetric], simplified]
   3.334 +
   3.335 +lemmas div_mult_le = div_times_less_eq_dividend
   3.336 +
   3.337 +lemmas sdl = div_nat_eqI
   3.338 +
   3.339 +lemma given_quot: "f > 0 \<Longrightarrow> (f * l + (f - 1)) div f = l"
   3.340 +  for f l :: nat
   3.341 +  by (rule div_nat_eqI) (simp_all)
   3.342 +
   3.343 +lemma given_quot_alt: "f > 0 \<Longrightarrow> (l * f + f - Suc 0) div f = l"
   3.344 +  for f l :: nat
   3.345 +  apply (frule given_quot)
   3.346 +  apply (rule trans)
   3.347 +   prefer 2
   3.348 +   apply (erule asm_rl)
   3.349 +  apply (rule_tac f="\<lambda>n. n div f" in arg_cong)
   3.350 +  apply (simp add : ac_simps)
   3.351 +  done
   3.352 +
   3.353 +lemma diff_mod_le: "a < d \<Longrightarrow> b dvd d \<Longrightarrow> a - a mod b \<le> d - b"
   3.354 +  for a b d :: nat
   3.355 +  apply (unfold dvd_def)
   3.356 +  apply clarify
   3.357 +  apply (case_tac k)
   3.358 +   apply clarsimp
   3.359 +  apply clarify
   3.360 +  apply (cases "b > 0")
   3.361 +   apply (drule mult.commute [THEN xtr1])
   3.362 +   apply (frule (1) td_gal_lt [THEN iffD1])
   3.363 +   apply (clarsimp simp: le_simps)
   3.364 +   apply (rule minus_mod_eq_mult_div [symmetric, THEN [2] xtr4])
   3.365 +   apply (rule mult_mono)
   3.366 +      apply auto
   3.367 +  done
   3.368 +
   3.369 +lemma less_le_mult': "w * c < b * c \<Longrightarrow> 0 \<le> c \<Longrightarrow> (w + 1) * c \<le> b * c"
   3.370 +  for b c w :: int
   3.371 +  apply (rule mult_right_mono)
   3.372 +   apply (rule zless_imp_add1_zle)
   3.373 +   apply (erule (1) mult_right_less_imp_less)
   3.374 +  apply assumption
   3.375 +  done
   3.376 +
   3.377 +lemma less_le_mult: "w * c < b * c \<Longrightarrow> 0 \<le> c \<Longrightarrow> w * c + c \<le> b * c"
   3.378 +  for b c w :: int
   3.379 +  using less_le_mult' [of w c b] by (simp add: algebra_simps)
   3.380 +
   3.381 +lemmas less_le_mult_minus = iffD2 [OF le_diff_eq less_le_mult,
   3.382 +  simplified left_diff_distrib]
   3.383 +
   3.384 +lemma gen_minus: "0 < n \<Longrightarrow> f n = f (Suc (n - 1))"
   3.385 +  by auto
   3.386 +
   3.387 +lemma mpl_lem: "j \<le> i \<Longrightarrow> k < j \<Longrightarrow> i - j + k < i"
   3.388 +  for i j k :: nat
   3.389 +  by arith
   3.390 +
   3.391 +lemma nonneg_mod_div: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> (a mod b) \<and> 0 \<le> a div b"
   3.392 +  for a b :: int
   3.393 +  by (cases "b = 0") (auto intro: pos_imp_zdiv_nonneg_iff [THEN iffD2])
   3.394 +
   3.395 +declare iszero_0 [intro]
   3.396 +
   3.397 +lemma min_pm [simp]: "min a b + (a - b) = a"
   3.398 +  for a b :: nat
   3.399 +  by arith
   3.400 +
   3.401 +lemma min_pm1 [simp]: "a - b + min a b = a"
   3.402 +  for a b :: nat
   3.403 +  by arith
   3.404 +
   3.405 +lemma rev_min_pm [simp]: "min b a + (a - b) = a"
   3.406 +  for a b :: nat
   3.407 +  by arith
   3.408 +
   3.409 +lemma rev_min_pm1 [simp]: "a - b + min b a = a"
   3.410 +  for a b :: nat
   3.411 +  by arith
   3.412 +
   3.413 +lemma min_minus [simp]: "min m (m - k) = m - k"
   3.414 +  for m k :: nat
   3.415 +  by arith
   3.416 +
   3.417 +lemma min_minus' [simp]: "min (m - k) m = m - k"
   3.418 +  for m k :: nat
   3.419 +  by arith
   3.420 +
   3.421 +lemmas m2pths = pos_mod_sign pos_mod_bound [OF zless2p]
   3.422 +
   3.423 +lemma not_B1_is_B0: "y \<noteq> 1 \<Longrightarrow> y = 0"
   3.424 +  for y :: bit
   3.425 +  by (cases y) auto
   3.426 +
   3.427 +lemma B1_ass_B0:
   3.428 +  fixes y :: bit
   3.429 +  assumes y: "y = 0 \<Longrightarrow> y = 1"
   3.430 +  shows "y = 1"
   3.431 +  apply (rule classical)
   3.432 +  apply (drule not_B1_is_B0)
   3.433 +  apply (erule y)
   3.434 +  done
   3.435 +
   3.436 +end
     4.1 --- a/src/HOL/Word/Misc_Numeric.thy	Tue Apr 16 19:50:03 2019 +0000
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,71 +0,0 @@
     4.4 -(*  Title:      HOL/Word/Misc_Numeric.thy
     4.5 -    Author:     Jeremy Dawson, NICTA
     4.6 -*)
     4.7 -
     4.8 -section \<open>Useful Numerical Lemmas\<close>
     4.9 -
    4.10 -theory Misc_Numeric
    4.11 -  imports Main
    4.12 -begin
    4.13 -
    4.14 -lemma one_mod_exp_eq_one [simp]:
    4.15 -  "1 mod (2 * 2 ^ n) = (1::int)"
    4.16 -  using power_gt1 [of 2 n] by (auto intro: mod_pos_pos_trivial)
    4.17 -  
    4.18 -lemma mod_2_neq_1_eq_eq_0: "k mod 2 \<noteq> 1 \<longleftrightarrow> k mod 2 = 0"
    4.19 -  for k :: int
    4.20 -  by (fact not_mod_2_eq_1_eq_0)
    4.21 -
    4.22 -lemma z1pmod2: "(2 * b + 1) mod 2 = (1::int)"
    4.23 -  for b :: int
    4.24 -  by arith
    4.25 -
    4.26 -lemma diff_le_eq': "a - b \<le> c \<longleftrightarrow> a \<le> b + c"
    4.27 -  for a b c :: int
    4.28 -  by arith
    4.29 -
    4.30 -lemma emep1: "even n \<Longrightarrow> even d \<Longrightarrow> 0 \<le> d \<Longrightarrow> (n + 1) mod d = (n mod d) + 1"
    4.31 -  for n d :: int
    4.32 -  by (auto simp add: pos_zmod_mult_2 add.commute dvd_def)
    4.33 -
    4.34 -lemma int_mod_ge: "a < n \<Longrightarrow> 0 < n \<Longrightarrow> a \<le> a mod n"
    4.35 -  for a n :: int
    4.36 -  by (metis dual_order.trans le_cases mod_pos_pos_trivial pos_mod_conj)
    4.37 -
    4.38 -lemma int_mod_ge': "b < 0 \<Longrightarrow> 0 < n \<Longrightarrow> b + n \<le> b mod n"
    4.39 -  for b n :: int
    4.40 -  by (metis add_less_same_cancel2 int_mod_ge mod_add_self2)
    4.41 -
    4.42 -lemma int_mod_le': "0 \<le> b - n \<Longrightarrow> b mod n \<le> b - n"
    4.43 -  for b n :: int
    4.44 -  by (metis minus_mod_self2 zmod_le_nonneg_dividend)
    4.45 -
    4.46 -lemma zless2: "0 < (2 :: int)"
    4.47 -  by (fact zero_less_numeral)
    4.48 -
    4.49 -lemma zless2p: "0 < (2 ^ n :: int)"
    4.50 -  by arith
    4.51 -
    4.52 -lemma zle2p: "0 \<le> (2 ^ n :: int)"
    4.53 -  by arith
    4.54 -
    4.55 -lemma m1mod2k: "- 1 mod 2 ^ n = (2 ^ n - 1 :: int)"
    4.56 -  using zless2p by (rule zmod_minus1)
    4.57 -
    4.58 -lemma p1mod22k': "(1 + 2 * b) mod (2 * 2 ^ n) = 1 + 2 * (b mod 2 ^ n)"
    4.59 -  for b :: int
    4.60 -  using zle2p by (rule pos_zmod_mult_2)
    4.61 -
    4.62 -lemma p1mod22k: "(2 * b + 1) mod (2 * 2 ^ n) = 2 * (b mod 2 ^ n) + 1"
    4.63 -  for b :: int
    4.64 -  by (simp add: p1mod22k' add.commute)
    4.65 -
    4.66 -lemma int_mod_lem: "0 < n \<Longrightarrow> 0 \<le> b \<and> b < n \<longleftrightarrow> b mod n = b"
    4.67 -  for b n :: int
    4.68 -  apply safe
    4.69 -    apply (erule (1) mod_pos_pos_trivial)
    4.70 -   apply (erule_tac [!] subst)
    4.71 -   apply auto
    4.72 -  done
    4.73 -
    4.74 -end
     5.1 --- a/src/HOL/Word/Word.thy	Tue Apr 16 19:50:03 2019 +0000
     5.2 +++ b/src/HOL/Word/Word.thy	Tue Apr 16 19:50:05 2019 +0000
     5.3 @@ -11,7 +11,7 @@
     5.4    Bits_Bit
     5.5    Bits_Int
     5.6    Misc_Typedef
     5.7 -  Word_Miscellaneous
     5.8 +  Misc_Arithmetic
     5.9  begin
    5.10  
    5.11  text \<open>See \<^file>\<open>WordExamples.thy\<close> for examples.\<close>
     6.1 --- a/src/HOL/Word/Word_Miscellaneous.thy	Tue Apr 16 19:50:03 2019 +0000
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,398 +0,0 @@
     6.4 -(*  Title:      HOL/Word/Word_Miscellaneous.thy  *)
     6.5 -
     6.6 -section \<open>Miscellaneous lemmas, of at least doubtful value\<close>
     6.7 -
     6.8 -theory Word_Miscellaneous
     6.9 -  imports "HOL-Library.Bit" Misc_Numeric
    6.10 -begin
    6.11 -
    6.12 -lemma ex_eq_or: "(\<exists>m. n = Suc m \<and> (m = k \<or> P m)) \<longleftrightarrow> n = Suc k \<or> (\<exists>m. n = Suc m \<and> P m)"
    6.13 -  by auto
    6.14 -
    6.15 -lemma power_minus_simp: "0 < n \<Longrightarrow> a ^ n = a * a ^ (n - 1)"
    6.16 -  by (auto dest: gr0_implies_Suc)
    6.17 -
    6.18 -lemma funpow_minus_simp: "0 < n \<Longrightarrow> f ^^ n = f \<circ> f ^^ (n - 1)"
    6.19 -  by (auto dest: gr0_implies_Suc)
    6.20 -
    6.21 -lemma power_numeral: "a ^ numeral k = a * a ^ (pred_numeral k)"
    6.22 -  by (simp add: numeral_eq_Suc)
    6.23 -
    6.24 -lemma funpow_numeral [simp]: "f ^^ numeral k = f \<circ> f ^^ (pred_numeral k)"
    6.25 -  by (simp add: numeral_eq_Suc)
    6.26 -
    6.27 -lemma replicate_numeral [simp]: "replicate (numeral k) x = x # replicate (pred_numeral k) x"
    6.28 -  by (simp add: numeral_eq_Suc)
    6.29 -
    6.30 -lemma rco_alt: "(f \<circ> g) ^^ n \<circ> f = f \<circ> (g \<circ> f) ^^ n"
    6.31 -  apply (rule ext)
    6.32 -  apply (induct n)
    6.33 -   apply (simp_all add: o_def)
    6.34 -  done
    6.35 -
    6.36 -lemma list_exhaust_size_gt0:
    6.37 -  assumes "\<And>a list. y = a # list \<Longrightarrow> P"
    6.38 -  shows "0 < length y \<Longrightarrow> P"
    6.39 -  apply (cases y)
    6.40 -   apply simp
    6.41 -  apply (rule assms)
    6.42 -  apply fastforce
    6.43 -  done
    6.44 -
    6.45 -lemma list_exhaust_size_eq0:
    6.46 -  assumes "y = [] \<Longrightarrow> P"
    6.47 -  shows "length y = 0 \<Longrightarrow> P"
    6.48 -  apply (cases y)
    6.49 -   apply (rule assms)
    6.50 -   apply simp
    6.51 -  apply simp
    6.52 -  done
    6.53 -
    6.54 -lemma size_Cons_lem_eq: "y = xa # list \<Longrightarrow> size y = Suc k \<Longrightarrow> size list = k"
    6.55 -  by auto
    6.56 -
    6.57 -lemmas ls_splits = prod.split prod.split_asm if_split_asm
    6.58 -
    6.59 -lemma not_B1_is_B0: "y \<noteq> 1 \<Longrightarrow> y = 0"
    6.60 -  for y :: bit
    6.61 -  by (cases y) auto
    6.62 -
    6.63 -lemma B1_ass_B0:
    6.64 -  fixes y :: bit
    6.65 -  assumes y: "y = 0 \<Longrightarrow> y = 1"
    6.66 -  shows "y = 1"
    6.67 -  apply (rule classical)
    6.68 -  apply (drule not_B1_is_B0)
    6.69 -  apply (erule y)
    6.70 -  done
    6.71 -
    6.72 -\<comment> \<open>simplifications for specific word lengths\<close>
    6.73 -lemmas n2s_ths [THEN eq_reflection] = add_2_eq_Suc add_2_eq_Suc'
    6.74 -
    6.75 -lemmas s2n_ths = n2s_ths [symmetric]
    6.76 -
    6.77 -lemma and_len: "xs = ys \<Longrightarrow> xs = ys \<and> length xs = length ys"
    6.78 -  by auto
    6.79 -
    6.80 -lemma size_if: "size (if p then xs else ys) = (if p then size xs else size ys)"
    6.81 -  by auto
    6.82 -
    6.83 -lemma tl_if: "tl (if p then xs else ys) = (if p then tl xs else tl ys)"
    6.84 -  by auto
    6.85 -
    6.86 -lemma hd_if: "hd (if p then xs else ys) = (if p then hd xs else hd ys)"
    6.87 -  by auto
    6.88 -
    6.89 -lemma if_Not_x: "(if p then \<not> x else x) = (p = (\<not> x))"
    6.90 -  by auto
    6.91 -
    6.92 -lemma if_x_Not: "(if p then x else \<not> x) = (p = x)"
    6.93 -  by auto
    6.94 -
    6.95 -lemma if_same_and: "(If p x y \<and> If p u v) = (if p then x \<and> u else y \<and> v)"
    6.96 -  by auto
    6.97 -
    6.98 -lemma if_same_eq: "(If p x y  = (If p u v)) = (if p then x = u else y = v)"
    6.99 -  by auto
   6.100 -
   6.101 -lemma if_same_eq_not: "(If p x y = (\<not> If p u v)) = (if p then x = (\<not> u) else y = (\<not> v))"
   6.102 -  by auto
   6.103 -
   6.104 -\<comment> \<open>note -- \<open>if_Cons\<close> can cause blowup in the size, if \<open>p\<close> is complex, so make a simproc\<close>
   6.105 -lemma if_Cons: "(if p then x # xs else y # ys) = If p x y # If p xs ys"
   6.106 -  by auto
   6.107 -
   6.108 -lemma if_single: "(if xc then [xab] else [an]) = [if xc then xab else an]"
   6.109 -  by auto
   6.110 -
   6.111 -lemma if_bool_simps:
   6.112 -  "If p True y = (p \<or> y) \<and> If p False y = (\<not> p \<and> y) \<and>
   6.113 -    If p y True = (p \<longrightarrow> y) \<and> If p y False = (p \<and> y)"
   6.114 -  by auto
   6.115 -
   6.116 -lemmas if_simps =
   6.117 -  if_x_Not if_Not_x if_cancel if_True if_False if_bool_simps
   6.118 -
   6.119 -lemmas seqr = eq_reflection [where x = "size w"] for w (* FIXME: delete *)
   6.120 -
   6.121 -lemma the_elemI: "y = {x} \<Longrightarrow> the_elem y = x"
   6.122 -  by simp
   6.123 -
   6.124 -lemma nonemptyE: "S \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> S \<Longrightarrow> R) \<Longrightarrow> R"
   6.125 -  by auto
   6.126 -
   6.127 -lemma gt_or_eq_0: "0 < y \<or> 0 = y"
   6.128 -  for y :: nat
   6.129 -  by arith
   6.130 -
   6.131 -lemmas xtr1 = xtrans(1)
   6.132 -lemmas xtr2 = xtrans(2)
   6.133 -lemmas xtr3 = xtrans(3)
   6.134 -lemmas xtr4 = xtrans(4)
   6.135 -lemmas xtr5 = xtrans(5)
   6.136 -lemmas xtr6 = xtrans(6)
   6.137 -lemmas xtr7 = xtrans(7)
   6.138 -lemmas xtr8 = xtrans(8)
   6.139 -
   6.140 -lemmas nat_simps = diff_add_inverse2 diff_add_inverse
   6.141 -lemmas nat_iffs = le_add1 le_add2
   6.142 -
   6.143 -lemma sum_imp_diff: "j = k + i \<Longrightarrow> j - i = k"
   6.144 -  for k :: nat
   6.145 -  by arith
   6.146 -
   6.147 -lemmas pos_mod_sign2 = zless2 [THEN pos_mod_sign [where b = "2::int"]]
   6.148 -lemmas pos_mod_bound2 = zless2 [THEN pos_mod_bound [where b = "2::int"]]
   6.149 -
   6.150 -lemma nmod2: "n mod 2 = 0 \<or> n mod 2 = 1"
   6.151 -  for n :: int
   6.152 -  by arith
   6.153 -
   6.154 -lemmas eme1p = emep1 [simplified add.commute]
   6.155 -
   6.156 -lemma le_diff_eq': "a \<le> c - b \<longleftrightarrow> b + a \<le> c"
   6.157 -  for a b c :: int
   6.158 -  by arith
   6.159 -
   6.160 -lemma less_diff_eq': "a < c - b \<longleftrightarrow> b + a < c"
   6.161 -  for a b c :: int
   6.162 -  by arith
   6.163 -
   6.164 -lemma diff_less_eq': "a - b < c \<longleftrightarrow> a < b + c"
   6.165 -  for a b c :: int
   6.166 -  by arith
   6.167 -
   6.168 -lemmas m1mod22k = mult_pos_pos [OF zless2 zless2p, THEN zmod_minus1]
   6.169 -
   6.170 -lemma z1pdiv2: "(2 * b + 1) div 2 = b"
   6.171 -  for b :: int
   6.172 -  by arith
   6.173 -
   6.174 -lemmas zdiv_le_dividend = xtr3 [OF div_by_1 [symmetric] zdiv_mono2,
   6.175 -  simplified int_one_le_iff_zero_less, simplified]
   6.176 -
   6.177 -lemma axxbyy: "a + m + m = b + n + n \<Longrightarrow> a = 0 \<or> a = 1 \<Longrightarrow> b = 0 \<or> b = 1 \<Longrightarrow> a = b \<and> m = n"
   6.178 -  for a b m n :: int
   6.179 -  by arith
   6.180 -
   6.181 -lemma axxmod2: "(1 + x + x) mod 2 = 1 \<and> (0 + x + x) mod 2 = 0"
   6.182 -  for x :: int
   6.183 -  by arith
   6.184 -
   6.185 -lemma axxdiv2: "(1 + x + x) div 2 = x \<and> (0 + x + x) div 2 = x"
   6.186 -  for x :: int
   6.187 -  by arith
   6.188 -
   6.189 -lemmas iszero_minus =
   6.190 -  trans [THEN trans, OF iszero_def neg_equal_0_iff_equal iszero_def [symmetric]]
   6.191 -
   6.192 -lemmas zadd_diff_inverse =
   6.193 -  trans [OF diff_add_cancel [symmetric] add.commute]
   6.194 -
   6.195 -lemmas add_diff_cancel2 =
   6.196 -  add.commute [THEN diff_eq_eq [THEN iffD2]]
   6.197 -
   6.198 -lemmas rdmods [symmetric] = mod_minus_eq
   6.199 -  mod_diff_left_eq mod_diff_right_eq mod_add_left_eq
   6.200 -  mod_add_right_eq mod_mult_right_eq mod_mult_left_eq
   6.201 -
   6.202 -lemma mod_plus_right: "(a + x) mod m = (b + x) mod m \<longleftrightarrow> a mod m = b mod m"
   6.203 -  for a b m x :: nat
   6.204 -  by (induct x) (simp_all add: mod_Suc, arith)
   6.205 -
   6.206 -lemma nat_minus_mod: "(n - n mod m) mod m = 0"
   6.207 -  for m n :: nat
   6.208 -  by (induct n) (simp_all add: mod_Suc)
   6.209 -
   6.210 -lemmas nat_minus_mod_plus_right =
   6.211 -  trans [OF nat_minus_mod mod_0 [symmetric],
   6.212 -    THEN mod_plus_right [THEN iffD2], simplified]
   6.213 -
   6.214 -lemmas push_mods' = mod_add_eq
   6.215 -  mod_mult_eq mod_diff_eq
   6.216 -  mod_minus_eq
   6.217 -
   6.218 -lemmas push_mods = push_mods' [THEN eq_reflection]
   6.219 -lemmas pull_mods = push_mods [symmetric] rdmods [THEN eq_reflection]
   6.220 -
   6.221 -lemma nat_mod_eq: "b < n \<Longrightarrow> a mod n = b mod n \<Longrightarrow> a mod n = b"
   6.222 -  for a b n :: nat
   6.223 -  by (induct a) auto
   6.224 -
   6.225 -lemmas nat_mod_eq' = refl [THEN [2] nat_mod_eq]
   6.226 -
   6.227 -lemma nat_mod_lem: "0 < n \<Longrightarrow> b < n \<longleftrightarrow> b mod n = b"
   6.228 -  for b n :: nat
   6.229 -  apply safe
   6.230 -   apply (erule nat_mod_eq')
   6.231 -  apply (erule subst)
   6.232 -  apply (erule mod_less_divisor)
   6.233 -  done
   6.234 -
   6.235 -lemma mod_nat_add: "x < z \<Longrightarrow> y < z \<Longrightarrow> (x + y) mod z = (if x + y < z then x + y else x + y - z)"
   6.236 -  for x y z :: nat
   6.237 -  apply (rule nat_mod_eq)
   6.238 -   apply auto
   6.239 -  apply (rule trans)
   6.240 -   apply (rule le_mod_geq)
   6.241 -   apply simp
   6.242 -  apply (rule nat_mod_eq')
   6.243 -  apply arith
   6.244 -  done
   6.245 -
   6.246 -lemma mod_nat_sub: "x < z \<Longrightarrow> (x - y) mod z = x - y"
   6.247 -  for x y :: nat
   6.248 -  by (rule nat_mod_eq') arith
   6.249 -
   6.250 -lemma int_mod_eq: "0 \<le> b \<Longrightarrow> b < n \<Longrightarrow> a mod n = b mod n \<Longrightarrow> a mod n = b"
   6.251 -  for a b n :: int
   6.252 -  by (metis mod_pos_pos_trivial)
   6.253 -
   6.254 -lemmas int_mod_eq' = mod_pos_pos_trivial (* FIXME delete *)
   6.255 -
   6.256 -lemmas int_mod_le = zmod_le_nonneg_dividend (* FIXME: delete *)
   6.257 -
   6.258 -lemma mod_add_if_z:
   6.259 -  "x < z \<Longrightarrow> y < z \<Longrightarrow> 0 \<le> y \<Longrightarrow> 0 \<le> x \<Longrightarrow> 0 \<le> z \<Longrightarrow>
   6.260 -    (x + y) mod z = (if x + y < z then x + y else x + y - z)"
   6.261 -  for x y z :: int
   6.262 -  by (auto intro: int_mod_eq)
   6.263 -
   6.264 -lemma mod_sub_if_z:
   6.265 -  "x < z \<Longrightarrow> y < z \<Longrightarrow> 0 \<le> y \<Longrightarrow> 0 \<le> x \<Longrightarrow> 0 \<le> z \<Longrightarrow>
   6.266 -    (x - y) mod z = (if y \<le> x then x - y else x - y + z)"
   6.267 -  for x y z :: int
   6.268 -  by (auto intro: int_mod_eq)
   6.269 -
   6.270 -lemmas zmde = mult_div_mod_eq [symmetric, THEN diff_eq_eq [THEN iffD2], symmetric]
   6.271 -lemmas mcl = mult_cancel_left [THEN iffD1, THEN make_pos_rule]
   6.272 -
   6.273 -(* already have this for naturals, div_mult_self1/2, but not for ints *)
   6.274 -lemma zdiv_mult_self: "m \<noteq> 0 \<Longrightarrow> (a + m * n) div m = a div m + n"
   6.275 -  for a m n :: int
   6.276 -  apply (rule mcl)
   6.277 -   prefer 2
   6.278 -   apply (erule asm_rl)
   6.279 -  apply (simp add: zmde ring_distribs)
   6.280 -  done
   6.281 -
   6.282 -lemma mod_power_lem: "a > 1 \<Longrightarrow> a ^ n mod a ^ m = (if m \<le> n then 0 else a ^ n)"
   6.283 -  for a :: int
   6.284 -  by (simp add: mod_eq_0_iff_dvd le_imp_power_dvd)
   6.285 -
   6.286 -lemma pl_pl_rels: "a + b = c + d \<Longrightarrow> a \<ge> c \<and> b \<le> d \<or> a \<le> c \<and> b \<ge> d"
   6.287 -  for a b c d :: nat
   6.288 -  by arith
   6.289 -
   6.290 -lemmas pl_pl_rels' = add.commute [THEN [2] trans, THEN pl_pl_rels]
   6.291 -
   6.292 -lemma minus_eq: "m - k = m \<longleftrightarrow> k = 0 \<or> m = 0"
   6.293 -  for k m :: nat
   6.294 -  by arith
   6.295 -
   6.296 -lemma pl_pl_mm: "a + b = c + d \<Longrightarrow> a - c = d - b"
   6.297 -  for a b c d :: nat
   6.298 -  by arith
   6.299 -
   6.300 -lemmas pl_pl_mm' = add.commute [THEN [2] trans, THEN pl_pl_mm]
   6.301 -
   6.302 -lemmas dme = div_mult_mod_eq
   6.303 -lemmas dtle = div_times_less_eq_dividend
   6.304 -lemmas th2 = order_trans [OF order_refl [THEN [2] mult_le_mono] div_times_less_eq_dividend]
   6.305 -
   6.306 -lemma td_gal: "0 < c \<Longrightarrow> a \<ge> b * c \<longleftrightarrow> a div c \<ge> b"
   6.307 -  for a b c :: nat
   6.308 -  apply safe
   6.309 -   apply (erule (1) xtr4 [OF div_le_mono div_mult_self_is_m])
   6.310 -  apply (erule th2)
   6.311 -  done
   6.312 -
   6.313 -lemmas td_gal_lt = td_gal [simplified not_less [symmetric], simplified]
   6.314 -
   6.315 -lemmas div_mult_le = div_times_less_eq_dividend
   6.316 -
   6.317 -lemmas sdl = div_nat_eqI
   6.318 -
   6.319 -lemma given_quot: "f > 0 \<Longrightarrow> (f * l + (f - 1)) div f = l"
   6.320 -  for f l :: nat
   6.321 -  by (rule div_nat_eqI) (simp_all)
   6.322 -
   6.323 -lemma given_quot_alt: "f > 0 \<Longrightarrow> (l * f + f - Suc 0) div f = l"
   6.324 -  for f l :: nat
   6.325 -  apply (frule given_quot)
   6.326 -  apply (rule trans)
   6.327 -   prefer 2
   6.328 -   apply (erule asm_rl)
   6.329 -  apply (rule_tac f="\<lambda>n. n div f" in arg_cong)
   6.330 -  apply (simp add : ac_simps)
   6.331 -  done
   6.332 -
   6.333 -lemma diff_mod_le: "a < d \<Longrightarrow> b dvd d \<Longrightarrow> a - a mod b \<le> d - b"
   6.334 -  for a b d :: nat
   6.335 -  apply (unfold dvd_def)
   6.336 -  apply clarify
   6.337 -  apply (case_tac k)
   6.338 -   apply clarsimp
   6.339 -  apply clarify
   6.340 -  apply (cases "b > 0")
   6.341 -   apply (drule mult.commute [THEN xtr1])
   6.342 -   apply (frule (1) td_gal_lt [THEN iffD1])
   6.343 -   apply (clarsimp simp: le_simps)
   6.344 -   apply (rule minus_mod_eq_mult_div [symmetric, THEN [2] xtr4])
   6.345 -   apply (rule mult_mono)
   6.346 -      apply auto
   6.347 -  done
   6.348 -
   6.349 -lemma less_le_mult': "w * c < b * c \<Longrightarrow> 0 \<le> c \<Longrightarrow> (w + 1) * c \<le> b * c"
   6.350 -  for b c w :: int
   6.351 -  apply (rule mult_right_mono)
   6.352 -   apply (rule zless_imp_add1_zle)
   6.353 -   apply (erule (1) mult_right_less_imp_less)
   6.354 -  apply assumption
   6.355 -  done
   6.356 -
   6.357 -lemma less_le_mult: "w * c < b * c \<Longrightarrow> 0 \<le> c \<Longrightarrow> w * c + c \<le> b * c"
   6.358 -  for b c w :: int
   6.359 -  using less_le_mult' [of w c b] by (simp add: algebra_simps)
   6.360 -
   6.361 -lemmas less_le_mult_minus = iffD2 [OF le_diff_eq less_le_mult,
   6.362 -  simplified left_diff_distrib]
   6.363 -
   6.364 -lemma gen_minus: "0 < n \<Longrightarrow> f n = f (Suc (n - 1))"
   6.365 -  by auto
   6.366 -
   6.367 -lemma mpl_lem: "j \<le> i \<Longrightarrow> k < j \<Longrightarrow> i - j + k < i"
   6.368 -  for i j k :: nat
   6.369 -  by arith
   6.370 -
   6.371 -lemma nonneg_mod_div: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> (a mod b) \<and> 0 \<le> a div b"
   6.372 -  for a b :: int
   6.373 -  by (cases "b = 0") (auto intro: pos_imp_zdiv_nonneg_iff [THEN iffD2])
   6.374 -
   6.375 -declare iszero_0 [intro]
   6.376 -
   6.377 -lemma min_pm [simp]: "min a b + (a - b) = a"
   6.378 -  for a b :: nat
   6.379 -  by arith
   6.380 -
   6.381 -lemma min_pm1 [simp]: "a - b + min a b = a"
   6.382 -  for a b :: nat
   6.383 -  by arith
   6.384 -
   6.385 -lemma rev_min_pm [simp]: "min b a + (a - b) = a"
   6.386 -  for a b :: nat
   6.387 -  by arith
   6.388 -
   6.389 -lemma rev_min_pm1 [simp]: "a - b + min b a = a"
   6.390 -  for a b :: nat
   6.391 -  by arith
   6.392 -
   6.393 -lemma min_minus [simp]: "min m (m - k) = m - k"
   6.394 -  for m k :: nat
   6.395 -  by arith
   6.396 -
   6.397 -lemma min_minus' [simp]: "min (m - k) m = m - k"
   6.398 -  for m k :: nat
   6.399 -  by arith
   6.400 -
   6.401 -end