24333

1 
(*


2 
ID: $Id$


3 
Author: Jeremy Dawson, NICTA

24350

4 
*)

24333

5 

24350

6 
header {* Useful Numerical Lemmas *}

24333

7 


8 
theory Num_Lemmas imports Parity begin


9 

24465

10 
lemma contentsI: "y = {x} ==> contents y = x"


11 
unfolding contents_def by auto


12 


13 
lemma prod_case_split: "prod_case = split"


14 
by (rule ext)+ auto


15 


16 
lemmas split_split = prod.split [unfolded prod_case_split]


17 
lemmas split_split_asm = prod.split_asm [unfolded prod_case_split]


18 
lemmas "split.splits" = split_split split_split_asm


19 


20 
lemmas funpow_0 = funpow.simps(1)

24333

21 
lemmas funpow_Suc = funpow.simps(2)

24465

22 


23 
lemma nonemptyE: "S ~= {} ==> (!!x. x : S ==> R) ==> R"


24 
apply (erule contrapos_np)


25 
apply (rule equals0I)


26 
apply auto


27 
done

24333

28 


29 
lemma gt_or_eq_0: "0 < y \<or> 0 = (y::nat)" by auto


30 

24465

31 
constdefs


32 
mod_alt :: "'a => 'a => 'a :: Divides.div"


33 
"mod_alt n m == n mod m"


34 


35 
 "alternative way of defining @{text bin_last}, @{text bin_rest}"


36 
bin_rl :: "int => int * bit"


37 
"bin_rl w == SOME (r, l). w = r BIT l"


38 


39 
declare iszero_0 [iff]


40 

24333

41 
lemmas xtr1 = xtrans(1)


42 
lemmas xtr2 = xtrans(2)


43 
lemmas xtr3 = xtrans(3)


44 
lemmas xtr4 = xtrans(4)


45 
lemmas xtr5 = xtrans(5)


46 
lemmas xtr6 = xtrans(6)


47 
lemmas xtr7 = xtrans(7)


48 
lemmas xtr8 = xtrans(8)


49 

24465

50 
lemma Min_ne_Pls [iff]:


51 
"Numeral.Min ~= Numeral.Pls"


52 
unfolding Min_def Pls_def by auto


53 


54 
lemmas Pls_ne_Min [iff] = Min_ne_Pls [symmetric]


55 


56 
lemmas PlsMin_defs [intro!] =

24333

57 
Pls_def Min_def Pls_def [symmetric] Min_def [symmetric]


58 


59 
lemmas PlsMin_simps [simp] = PlsMin_defs [THEN Eq_TrueI]


60 


61 
lemma number_of_False_cong:


62 
"False ==> number_of x = number_of y"


63 
by auto


64 

24465

65 
lemmas nat_simps = diff_add_inverse2 diff_add_inverse


66 
lemmas nat_iffs = le_add1 le_add2


67 


68 
lemma sum_imp_diff: "j = k + i ==> j  i = (k :: nat)"


69 
by (clarsimp simp add: nat_simps)


70 

24333

71 
lemma nobm1:


72 
"0 < (number_of w :: nat) ==>


73 
number_of w  (1 :: nat) = number_of (Numeral.pred w)"


74 
apply (unfold nat_number_of_def One_nat_def nat_1 [symmetric] pred_def)


75 
apply (simp add: number_of_eq nat_diff_distrib [symmetric])


76 
done

24465

77 


78 
lemma of_int_power:


79 
"of_int (a ^ n) = (of_int a ^ n :: 'a :: {recpower, comm_ring_1})"


80 
by (induct n) (auto simp add: power_Suc)

24333

81 


82 
lemma zless2: "0 < (2 :: int)"


83 
by auto


84 

24465

85 
lemmas zless2p [simp] = zless2 [THEN zero_less_power]


86 
lemmas zle2p [simp] = zless2p [THEN order_less_imp_le]


87 


88 
lemmas pos_mod_sign2 = zless2 [THEN pos_mod_sign [where b = "2::int"]]


89 
lemmas pos_mod_bound2 = zless2 [THEN pos_mod_bound [where b = "2::int"]]


90 


91 
 "the inverse(s) of @{text number_of}"


92 
lemma nmod2: "n mod (2::int) = 0  n mod 2 = 1"


93 
using pos_mod_sign2 [of n] pos_mod_bound2 [of n]


94 
unfolding mod_alt_def [symmetric] by auto

24333

95 


96 
lemma emep1:


97 
"even n ==> even d ==> 0 <= d ==> (n + 1) mod (d :: int) = (n mod d) + 1"


98 
apply (simp add: add_commute)


99 
apply (safe dest!: even_equiv_def [THEN iffD1])


100 
apply (subst pos_zmod_mult_2)


101 
apply arith


102 
apply (simp add: zmod_zmult_zmult1)


103 
done


104 


105 
lemmas eme1p = emep1 [simplified add_commute]


106 

24465

107 
lemma le_diff_eq': "(a \<le> c  b) = (b + a \<le> (c::int))"


108 
by (simp add: le_diff_eq add_commute)


109 


110 
lemma less_diff_eq': "(a < c  b) = (b + a < (c::int))"


111 
by (simp add: less_diff_eq add_commute)


112 

24333

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


114 
by (simp add: diff_le_eq add_commute)

24465

115 


116 
lemma diff_less_eq': "(a  b < c) = (a < b + (c::int))"


117 
by (simp add: diff_less_eq add_commute)


118 

24333

119 


120 
lemmas m1mod2k = zless2p [THEN zmod_minus1]

24465

121 
lemmas m1mod22k = mult_pos_pos [OF zless2 zless2p, THEN zmod_minus1]

24333

122 
lemmas p1mod22k' = zless2p [THEN order_less_imp_le, THEN pos_zmod_mult_2]

24465

123 
lemmas z1pmod2' = zero_le_one [THEN pos_zmod_mult_2, simplified]


124 
lemmas z1pdiv2' = zero_le_one [THEN pos_zdiv_mult_2, simplified]

24333

125 


126 
lemma p1mod22k:


127 
"(2 * b + 1) mod (2 * 2 ^ n) = 2 * (b mod 2 ^ n) + (1::int)"


128 
by (simp add: p1mod22k' add_commute)

24465

129 


130 
lemma z1pmod2:


131 
"(2 * b + 1) mod 2 = (1::int)"


132 
by (simp add: z1pmod2' add_commute)


133 


134 
lemma z1pdiv2:


135 
"(2 * b + 1) div 2 = (b::int)"


136 
by (simp add: z1pdiv2' add_commute)

24333

137 


138 
lemmas zdiv_le_dividend = xtr3 [OF zdiv_1 [symmetric] zdiv_mono2,


139 
simplified int_one_le_iff_zero_less, simplified, standard]

24465

140 


141 
(** ways in which type Bin resembles a datatype **)


142 


143 
lemma BIT_eq: "u BIT b = v BIT c ==> u = v & b = c"


144 
apply (unfold Bit_def)


145 
apply (simp (no_asm_use) split: bit.split_asm)


146 
apply simp_all


147 
apply (drule_tac f=even in arg_cong, clarsimp)+


148 
done


149 


150 
lemmas BIT_eqE [elim!] = BIT_eq [THEN conjE, standard]


151 


152 
lemma BIT_eq_iff [simp]:


153 
"(u BIT b = v BIT c) = (u = v \<and> b = c)"


154 
by (rule iffI) auto


155 


156 
lemmas BIT_eqI [intro!] = conjI [THEN BIT_eq_iff [THEN iffD2]]


157 


158 
lemma less_Bits:


159 
"(v BIT b < w BIT c) = (v < w  v <= w & b = bit.B0 & c = bit.B1)"


160 
unfolding Bit_def by (auto split: bit.split)


161 


162 
lemma le_Bits:


163 
"(v BIT b <= w BIT c) = (v < w  v <= w & (b ~= bit.B1  c ~= bit.B0))"


164 
unfolding Bit_def by (auto split: bit.split)


165 


166 
lemma neB1E [elim!]:


167 
assumes ne: "y \<noteq> bit.B1"


168 
assumes y: "y = bit.B0 \<Longrightarrow> P"


169 
shows "P"


170 
apply (rule y)


171 
apply (cases y rule: bit.exhaust, simp)


172 
apply (simp add: ne)


173 
done


174 


175 
lemma bin_ex_rl: "EX w b. w BIT b = bin"


176 
apply (unfold Bit_def)


177 
apply (cases "even bin")


178 
apply (clarsimp simp: even_equiv_def)


179 
apply (auto simp: odd_equiv_def split: bit.split)


180 
done


181 


182 
lemma bin_exhaust:


183 
assumes Q: "\<And>x b. bin = x BIT b \<Longrightarrow> Q"


184 
shows "Q"


185 
apply (insert bin_ex_rl [of bin])


186 
apply (erule exE)+


187 
apply (rule Q)


188 
apply force


189 
done


190 


191 
lemma bin_rl_char: "(bin_rl w = (r, l)) = (r BIT l = w)"


192 
apply (unfold bin_rl_def)


193 
apply safe


194 
apply (cases w rule: bin_exhaust)


195 
apply auto


196 
done


197 


198 
lemmas bin_rl_simps [THEN bin_rl_char [THEN iffD2], standard, simp] =


199 
Pls_0_eq Min_1_eq refl


200 


201 
lemma bin_abs_lem:


202 
"bin = (w BIT b) ==> ~ bin = Numeral.Min > ~ bin = Numeral.Pls >


203 
nat (abs w) < nat (abs bin)"


204 
apply (clarsimp simp add: bin_rl_char)


205 
apply (unfold Pls_def Min_def Bit_def)


206 
apply (cases b)


207 
apply (clarsimp, arith)


208 
apply (clarsimp, arith)


209 
done


210 


211 
lemma bin_induct:


212 
assumes PPls: "P Numeral.Pls"


213 
and PMin: "P Numeral.Min"


214 
and PBit: "!!bin bit. P bin ==> P (bin BIT bit)"


215 
shows "P bin"


216 
apply (rule_tac P=P and a=bin and f1="nat o abs"


217 
in wf_measure [THEN wf_induct])


218 
apply (simp add: measure_def inv_image_def)


219 
apply (case_tac x rule: bin_exhaust)


220 
apply (frule bin_abs_lem)


221 
apply (auto simp add : PPls PMin PBit)


222 
done


223 


224 
lemma no_no [simp]: "number_of (number_of i) = i"


225 
unfolding number_of_eq by simp

24333

226 


227 
lemma Bit_B0:


228 
"k BIT bit.B0 = k + k"


229 
by (unfold Bit_def) simp


230 

24465

231 
lemma Bit_B1:


232 
"k BIT bit.B1 = k + k + 1"


233 
by (unfold Bit_def) simp


234 

24333

235 
lemma Bit_B0_2t: "k BIT bit.B0 = 2 * k"


236 
by (rule trans, rule Bit_B0) simp

24465

237 


238 
lemma Bit_B1_2t: "k BIT bit.B1 = 2 * k + 1"


239 
by (rule trans, rule Bit_B1) simp


240 


241 
lemma B_mod_2':


242 
"X = 2 ==> (w BIT bit.B1) mod X = 1 & (w BIT bit.B0) mod X = 0"


243 
apply (simp (no_asm) only: Bit_B0 Bit_B1)


244 
apply (simp add: z1pmod2)


245 
done


246 


247 
lemmas B1_mod_2 [simp] = B_mod_2' [OF refl, THEN conjunct1, standard]


248 
lemmas B0_mod_2 [simp] = B_mod_2' [OF refl, THEN conjunct2, standard]


249 


250 
lemma axxbyy:


251 
"a + m + m = b + n + n ==> (a = 0  a = 1) ==> (b = 0  b = 1) ==>


252 
a = b & m = (n :: int)"


253 
apply auto


254 
apply (drule_tac f="%n. n mod 2" in arg_cong)


255 
apply (clarsimp simp: z1pmod2)


256 
apply (drule_tac f="%n. n mod 2" in arg_cong)


257 
apply (clarsimp simp: z1pmod2)


258 
done


259 


260 
lemma axxmod2:


261 
"(1 + x + x) mod 2 = (1 :: int) & (0 + x + x) mod 2 = (0 :: int)"


262 
by simp (rule z1pmod2)


263 


264 
lemma axxdiv2:


265 
"(1 + x + x) div 2 = (x :: int) & (0 + x + x) div 2 = (x :: int)"


266 
by simp (rule z1pdiv2)


267 


268 
lemmas iszero_minus = trans [THEN trans,


269 
OF iszero_def neg_equal_0_iff_equal iszero_def [symmetric], standard]

24333

270 


271 
lemmas zadd_diff_inverse = trans [OF diff_add_cancel [symmetric] add_commute,


272 
standard]


273 


274 
lemmas add_diff_cancel2 = add_commute [THEN diff_eq_eq [THEN iffD2], standard]


275 


276 
lemma zmod_uminus: " ((a :: int) mod b) mod b = a mod b"


277 
by (simp add : zmod_zminus1_eq_if)

24465

278 


279 
lemma zmod_zsub_distrib: "((a::int)  b) mod c = (a mod c  b mod c) mod c"


280 
apply (unfold diff_int_def)


281 
apply (rule trans [OF _ zmod_zadd1_eq [symmetric]])


282 
apply (simp add: zmod_uminus zmod_zadd1_eq [symmetric])


283 
done

24333

284 


285 
lemma zmod_zsub_right_eq: "((a::int)  b) mod c = (a  b mod c) mod c"


286 
apply (unfold diff_int_def)


287 
apply (rule trans [OF _ zmod_zadd_right_eq [symmetric]])


288 
apply (simp add : zmod_uminus zmod_zadd_right_eq [symmetric])


289 
done


290 


291 
lemmas zmod_zsub_left_eq =


292 
zmod_zadd_left_eq [where b = " ?b", simplified diff_int_def [symmetric]]


293 


294 
lemma zmod_zsub_self [simp]:


295 
"((b :: int)  a) mod a = b mod a"


296 
by (simp add: zmod_zsub_right_eq)


297 


298 
lemma zmod_zmult1_eq_rev:


299 
"b * a mod c = b mod c * a mod (c::int)"


300 
apply (simp add: mult_commute)


301 
apply (subst zmod_zmult1_eq)


302 
apply simp


303 
done


304 


305 
lemmas rdmods [symmetric] = zmod_uminus [symmetric]


306 
zmod_zsub_left_eq zmod_zsub_right_eq zmod_zadd_left_eq


307 
zmod_zadd_right_eq zmod_zmult1_eq zmod_zmult1_eq_rev


308 


309 
lemma mod_plus_right:


310 
"((a + x) mod m = (b + x) mod m) = (a mod m = b mod (m :: nat))"


311 
apply (induct x)


312 
apply (simp_all add: mod_Suc)


313 
apply arith


314 
done


315 

24465

316 
lemma nat_minus_mod: "(n  n mod m) mod m = (0 :: nat)"


317 
by (induct n) (simp_all add : mod_Suc)


318 


319 
lemmas nat_minus_mod_plus_right = trans [OF nat_minus_mod mod_0 [symmetric],


320 
THEN mod_plus_right [THEN iffD2], standard, simplified]


321 


322 
lemmas push_mods' = zmod_zadd1_eq [standard]


323 
zmod_zmult_distrib [standard] zmod_zsub_distrib [standard]


324 
zmod_uminus [symmetric, standard]


325 


326 
lemmas push_mods = push_mods' [THEN eq_reflection, standard]


327 
lemmas pull_mods = push_mods [symmetric] rdmods [THEN eq_reflection, standard]


328 
lemmas mod_simps =


329 
zmod_zmult_self1 [THEN eq_reflection] zmod_zmult_self2 [THEN eq_reflection]


330 
mod_mod_trivial [THEN eq_reflection]


331 

24333

332 
lemma nat_mod_eq:


333 
"!!b. b < n ==> a mod n = b mod n ==> a mod n = (b :: nat)"


334 
by (induct a) auto


335 


336 
lemmas nat_mod_eq' = refl [THEN [2] nat_mod_eq]


337 


338 
lemma nat_mod_lem:


339 
"(0 :: nat) < n ==> b < n = (b mod n = b)"


340 
apply safe


341 
apply (erule nat_mod_eq')


342 
apply (erule subst)


343 
apply (erule mod_less_divisor)


344 
done


345 


346 
lemma mod_nat_add:


347 
"(x :: nat) < z ==> y < z ==>


348 
(x + y) mod z = (if x + y < z then x + y else x + y  z)"


349 
apply (rule nat_mod_eq)


350 
apply auto


351 
apply (rule trans)


352 
apply (rule le_mod_geq)


353 
apply simp


354 
apply (rule nat_mod_eq')


355 
apply arith


356 
done

24465

357 


358 
lemma mod_nat_sub:


359 
"(x :: nat) < z ==> (x  y) mod z = x  y"


360 
by (rule nat_mod_eq') arith

24333

361 


362 
lemma int_mod_lem:


363 
"(0 :: int) < n ==> (0 <= b & b < n) = (b mod n = b)"


364 
apply safe


365 
apply (erule (1) mod_pos_pos_trivial)


366 
apply (erule_tac [!] subst)


367 
apply auto


368 
done


369 


370 
lemma int_mod_eq:


371 
"(0 :: int) <= b ==> b < n ==> a mod n = b mod n ==> a mod n = b"


372 
by clarsimp (rule mod_pos_pos_trivial)


373 


374 
lemmas int_mod_eq' = refl [THEN [3] int_mod_eq]


375 


376 
lemma int_mod_le: "0 <= a ==> 0 < (n :: int) ==> a mod n <= a"


377 
apply (cases "a < n")


378 
apply (auto dest: mod_pos_pos_trivial pos_mod_bound [where a=a])


379 
done


380 


381 
lemmas int_mod_le' = int_mod_le [where a = "?b  ?n", simplified]


382 


383 
lemma int_mod_ge: "a < n ==> 0 < (n :: int) ==> a <= a mod n"


384 
apply (cases "0 <= a")


385 
apply (drule (1) mod_pos_pos_trivial)


386 
apply simp


387 
apply (rule order_trans [OF _ pos_mod_sign])


388 
apply simp


389 
apply assumption


390 
done


391 


392 
lemmas int_mod_ge' = int_mod_ge [where a = "?b + ?n", simplified]


393 


394 
lemma mod_add_if_z:


395 
"(x :: int) < z ==> y < z ==> 0 <= y ==> 0 <= x ==> 0 <= z ==>


396 
(x + y) mod z = (if x + y < z then x + y else x + y  z)"


397 
by (auto intro: int_mod_eq)


398 


399 
lemma mod_sub_if_z:


400 
"(x :: int) < z ==> y < z ==> 0 <= y ==> 0 <= x ==> 0 <= z ==>


401 
(x  y) mod z = (if y <= x then x  y else x  y + z)"


402 
by (auto intro: int_mod_eq)

24465

403 


404 
lemmas zmde = zmod_zdiv_equality [THEN diff_eq_eq [THEN iffD2], symmetric]


405 
lemmas mcl = mult_cancel_left [THEN iffD1, THEN make_pos_rule]


406 


407 
(* already have this for naturals, div_mult_self1/2, but not for ints *)


408 
lemma zdiv_mult_self: "m ~= (0 :: int) ==> (a + m * n) div m = a div m + n"


409 
apply (rule mcl)


410 
prefer 2


411 
apply (erule asm_rl)


412 
apply (simp add: zmde ring_distribs)


413 
apply (simp add: push_mods)


414 
done


415 


416 
(** Rep_Integ **)


417 
lemma eqne: "equiv A r ==> X : A // r ==> X ~= {}"


418 
unfolding equiv_def refl_def quotient_def Image_def by auto


419 


420 
lemmas Rep_Integ_ne = Integ.Rep_Integ


421 
[THEN equiv_intrel [THEN eqne, simplified Integ_def [symmetric]], standard]


422 


423 
lemmas riq = Integ.Rep_Integ [simplified Integ_def]


424 
lemmas intrel_refl = refl [THEN equiv_intrel_iff [THEN iffD1], standard]


425 
lemmas Rep_Integ_equiv = quotient_eq_iff


426 
[OF equiv_intrel riq riq, simplified Integ.Rep_Integ_inject, standard]


427 
lemmas Rep_Integ_same =


428 
Rep_Integ_equiv [THEN intrel_refl [THEN rev_iffD2], standard]


429 


430 
lemma RI_int: "(a, 0) : Rep_Integ (int a)"


431 
unfolding int_def by auto


432 


433 
lemmas RI_intrel [simp] = UNIV_I [THEN quotientI,


434 
THEN Integ.Abs_Integ_inverse [simplified Integ_def], standard]


435 


436 
lemma RI_minus: "(a, b) : Rep_Integ x ==> (b, a) : Rep_Integ ( x)"


437 
apply (rule_tac z=x in eq_Abs_Integ)


438 
apply (clarsimp simp: minus)


439 
done

24333

440 

24465

441 
lemma RI_add:


442 
"(a, b) : Rep_Integ x ==> (c, d) : Rep_Integ y ==>


443 
(a + c, b + d) : Rep_Integ (x + y)"


444 
apply (rule_tac z=x in eq_Abs_Integ)


445 
apply (rule_tac z=y in eq_Abs_Integ)


446 
apply (clarsimp simp: add)


447 
done


448 


449 
lemma mem_same: "a : S ==> a = b ==> b : S"


450 
by fast


451 


452 
(* two alternative proofs of this *)


453 
lemma RI_eq_diff': "(a, b) : Rep_Integ (int a  int b)"


454 
apply (unfold diff_def)


455 
apply (rule mem_same)


456 
apply (rule RI_minus RI_add RI_int)+


457 
apply simp


458 
done


459 


460 
lemma RI_eq_diff: "((a, b) : Rep_Integ x) = (int a  int b = x)"


461 
apply safe


462 
apply (rule Rep_Integ_same)


463 
prefer 2


464 
apply (erule asm_rl)


465 
apply (rule RI_eq_diff')+


466 
done


467 


468 
lemma mod_power_lem:


469 
"a > 1 ==> a ^ n mod a ^ m = (if m <= n then 0 else (a :: int) ^ n)"


470 
apply clarsimp


471 
apply safe


472 
apply (simp add: zdvd_iff_zmod_eq_0 [symmetric])


473 
apply (drule le_iff_add [THEN iffD1])


474 
apply (force simp: zpower_zadd_distrib)


475 
apply (rule mod_pos_pos_trivial)


476 
apply (simp add: zero_le_power)


477 
apply (rule power_strict_increasing)


478 
apply auto


479 
done

24333

480 


481 
lemma min_pm [simp]: "min a b + (a  b) = (a :: nat)"


482 
by arith


483 


484 
lemmas min_pm1 [simp] = trans [OF add_commute min_pm]


485 


486 
lemma rev_min_pm [simp]: "min b a + (a  b) = (a::nat)"


487 
by simp


488 


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


490 

24465

491 
lemma pl_pl_rels:


492 
"a + b = c + d ==>


493 
a >= c & b <= d  a <= c & b >= (d :: nat)"


494 
apply (cut_tac n=a and m=c in nat_le_linear)


495 
apply (safe dest!: le_iff_add [THEN iffD1])


496 
apply arith+


497 
done


498 


499 
lemmas pl_pl_rels' = add_commute [THEN [2] trans, THEN pl_pl_rels]


500 


501 
lemma minus_eq: "(m  k = m) = (k = 0  m = (0 :: nat))"


502 
by arith


503 


504 
lemma pl_pl_mm: "(a :: nat) + b = c + d ==> a  c = d  b"


505 
by arith


506 


507 
lemmas pl_pl_mm' = add_commute [THEN [2] trans, THEN pl_pl_mm]


508 

24333

509 
lemma min_minus [simp] : "min m (m  k) = (m  k :: nat)"


510 
by arith


511 


512 
lemmas min_minus' [simp] = trans [OF min_max.inf_commute min_minus]


513 

24465

514 
lemma nat_no_eq_iff:


515 
"(number_of b :: int) >= 0 ==> (number_of c :: int) >= 0 ==>


516 
(number_of b = (number_of c :: nat)) = (b = c)"


517 
apply (unfold nat_number_of_def)


518 
apply safe


519 
apply (drule (2) eq_nat_nat_iff [THEN iffD1])


520 
apply (simp add: number_of_eq)


521 
done


522 

24333

523 
lemmas dme = box_equals [OF div_mod_equality add_0_right add_0_right]


524 
lemmas dtle = xtr3 [OF dme [symmetric] le_add1]


525 
lemmas th2 = order_trans [OF order_refl [THEN [2] mult_le_mono] dtle]


526 


527 
lemma td_gal:


528 
"0 < c ==> (a >= b * c) = (a div c >= (b :: nat))"


529 
apply safe


530 
apply (erule (1) xtr4 [OF div_le_mono div_mult_self_is_m])


531 
apply (erule th2)


532 
done


533 


534 
lemmas td_gal_lt = td_gal [simplified le_def, simplified]


535 


536 
lemma div_mult_le: "(a :: nat) div b * b <= a"


537 
apply (cases b)


538 
prefer 2


539 
apply (rule order_refl [THEN th2])


540 
apply auto


541 
done


542 


543 
lemmas sdl = split_div_lemma [THEN iffD1, symmetric]


544 


545 
lemma given_quot: "f > (0 :: nat) ==> (f * l + (f  1)) div f = l"


546 
by (rule sdl, assumption) (simp (no_asm))


547 


548 
lemma given_quot_alt: "f > (0 :: nat) ==> (l * f + f  Suc 0) div f = l"


549 
apply (frule given_quot)


550 
apply (rule trans)


551 
prefer 2


552 
apply (erule asm_rl)


553 
apply (rule_tac f="%n. n div f" in arg_cong)


554 
apply (simp add : mult_ac)


555 
done


556 

24465

557 
lemma diff_mod_le: "(a::nat) < d ==> b dvd d ==> a  a mod b <= d  b"


558 
apply (unfold dvd_def)


559 
apply clarify


560 
apply (case_tac k)


561 
apply clarsimp


562 
apply clarify


563 
apply (cases "b > 0")


564 
apply (drule mult_commute [THEN xtr1])


565 
apply (frule (1) td_gal_lt [THEN iffD1])


566 
apply (clarsimp simp: le_simps)


567 
apply (rule mult_div_cancel [THEN [2] xtr4])


568 
apply (rule mult_mono)


569 
apply auto


570 
done


571 

24333

572 
lemma less_le_mult':


573 
"w * c < b * c ==> 0 \<le> c ==> (w + 1) * c \<le> b * (c::int)"


574 
apply (rule mult_right_mono)


575 
apply (rule zless_imp_add1_zle)


576 
apply (erule (1) mult_right_less_imp_less)


577 
apply assumption


578 
done


579 


580 
lemmas less_le_mult = less_le_mult' [simplified left_distrib, simplified]

24465

581 


582 
lemmas less_le_mult_minus = iffD2 [OF le_diff_eq less_le_mult,


583 
simplified left_diff_distrib, standard]

24333

584 


585 
lemma lrlem':


586 
assumes d: "(i::nat) \<le> j \<or> m < j'"


587 
assumes R1: "i * k \<le> j * k \<Longrightarrow> R"


588 
assumes R2: "Suc m * k' \<le> j' * k' \<Longrightarrow> R"


589 
shows "R" using d


590 
apply safe


591 
apply (rule R1, erule mult_le_mono1)


592 
apply (rule R2, erule Suc_le_eq [THEN iffD2 [THEN mult_le_mono1]])


593 
done


594 


595 
lemma lrlem: "(0::nat) < sc ==>


596 
(sc  n + (n + lb * n) <= m * n) = (sc + lb * n <= m * n)"


597 
apply safe


598 
apply arith


599 
apply (case_tac "sc >= n")


600 
apply arith


601 
apply (insert linorder_le_less_linear [of m lb])


602 
apply (erule_tac k=n and k'=n in lrlem')


603 
apply arith


604 
apply simp


605 
done


606 


607 
lemma gen_minus: "0 < n ==> f n = f (Suc (n  1))"


608 
by auto


609 


610 
lemma mpl_lem: "j <= (i :: nat) ==> k < j ==> i  j + k < i"


611 
apply (induct i, clarsimp)


612 
apply (cases j, clarsimp)


613 
apply arith


614 
done


615 

24465

616 
lemma nonneg_mod_div:


617 
"0 <= a ==> 0 <= b ==> 0 <= (a mod b :: int) & 0 <= a div b"


618 
apply (cases "b = 0", clarsimp)


619 
apply (auto intro: pos_imp_zdiv_nonneg_iff [THEN iffD2])


620 
done

24399

621 

24333

622 
end
