# Theory NatIntLib

Up to index of Isabelle/HOL/HOL-Complex/NumberTheory

theory NatIntLib = WilsonRuss:

```(*  Title:      NatIntLib.thy
Gathering theorems by Jeremy Avigad and David Gray especially,
but also Adam Kramer and Paul Raff
*)

header {* Facts about integers and natural numbers *}

theory NatIntLib = WilsonRuss:;

lemma [simp]: "of_nat(n::nat) = n";
apply (induct_tac n);
apply auto;
done;

(*****************************************************************)
(*                                                               *)
(* Useful lemmas about dvd                                       *)
(*                                                               *)
(*****************************************************************)

subsection {* Integer divisibility and powers *}

lemma zpower_zdvd_prop1 [rule_format]: "((0 < n) & (p dvd y)) -->
p dvd ((y::int) ^ n)";
by (induct_tac n, auto simp add: zdvd_zmult zdvd_zmult2 [of p y])

lemma zdvd_bounds: "n dvd m ==> (m ≤ (0::int) | n ≤ m)";
proof -;
assume "n dvd m";
then have "~(0 < m & m < n)";
apply (insert zdvd_not_zless [of m n])
by (rule contrapos_pn, auto)
then have "(~0 < m | ~m < n)"  by auto
then show ?thesis by auto
qed;

lemma zprime_zdvd_zmult_better: "[| p ∈ zprime;  p dvd (m * n) |] ==>
(p dvd m) | (p dvd n)";
apply (case_tac "0 ≤ m")
apply (simp add: zprime_zdvd_zmult)
by (insert zprime_zdvd_zmult [of "-m" p n], auto)

lemma zpower_zdvd_prop2 [rule_format]: "p ∈ zprime --> p dvd ((y::int) ^ n)
--> 0 < n --> p dvd y";
apply (induct_tac n, auto)
apply (frule zprime_zdvd_zmult_better, auto)
done

lemma stupid: "(0 :: int) ≤ y ==> x ≤ x + y";
by arith

lemma div_prop1: "[| 0 < z; (x::int) < y * z |] ==> x div z < y";
proof -;
assume "0 < z";
then have "(x div z) * z ≤ (x div z) * z + x mod z";
apply (rule_tac x = "x div z * z" in stupid)
by (simp add: pos_mod_sign)
also have "... = x";
by (auto simp add: zmod_zdiv_equality [THEN sym] zmult_ac)
also assume  "x < y * z";
finally show ?thesis;
by (auto simp add: prems mult_less_cancel_right, insert prems, arith)
qed;

lemma div_prop2: "[| 0 < z; (x::int) < (y * z) + z |] ==> x div z ≤ y";
proof -;
assume "0 < z" and "x < (y * z) + z";
then have "x < (y + 1) * z" by (auto simp add: int_distrib)
then have "x div z < y + 1";
by (rule_tac y = "y + 1" in div_prop1, auto simp add: prems)
then show ?thesis by auto
qed;

lemma zdiv_leq_prop: "[| 0 < y |] ==> y * (x div y) ≤ (x::int)";
proof-;
assume "0 < y";
from zmod_zdiv_equality have "x = y * (x div y) + x mod y" by auto
moreover have "0 ≤ x mod y";
by (auto simp add: prems pos_mod_sign)
ultimately show ?thesis;
by arith
qed;

lemma zdiv_gr_zero: "[| 0 < a; 0 < b; a dvd b |] ==> (0::int) < (b div a)";
by (auto simp add: dvd_def zero_less_mult_iff);

lemma zdiv_zdiv_prop: "[| 0 < a; 0 < b; b dvd a |] ==> a div (a div b)
= (b::int)";
proof -;
assume "0 < a" and "0 < b" and "b dvd a";
then have p: "0 < a div b" by (auto simp add: zdiv_gr_zero);
have "a = a" by auto;
with prems have "a = b * (a div b)" by (auto simp add: dvd_def);
with prems have "a div (a div b) = (b * (a div b)) div (a div b)" by auto;
also from prems p have "... = b" by auto;
finally show ?thesis .;
qed;

lemma x_div_pa_prop: "[| p:zprime; x dvd (p * a) |] ==>
(p dvd x) | (x dvd a)";
apply (simp only: dvd_def, drule_tac Q = "(EX k. x = p * k) | (EX
k. a = x * k)" in exE);
defer 1; apply (force);
proof -;
fix y;
assume "p * a = x * y" and "p:zprime";
then have "p dvd (x * y)";
apply (auto simp add: dvd_def);
apply (rule_tac x = "a" in exI);
apply (auto);
done;
then have "(p dvd x) | (p dvd y)"
by (insert prems, auto simp add: zprime_zdvd_zmult_better);
moreover have "p dvd y ==> x dvd a";
proof-;
assume "p dvd y";
then have "x * y = x * (y div p) * p";
by (auto simp add: dvd_def);
also have "x * y = a * p" by (insert prems, auto simp add: zmult_ac);
finally have "a * p = x * (y div p) * p".;
then have "a = x * (y div p)";
by (insert prems, auto simp add: zprime_def);
thus "x dvd a" by (auto simp add: dvd_def);
qed;
ultimately have "(p dvd x) | (x dvd a)" by (auto);
thus "(EX k. x = p * k) | (EX k. a = x * k)" by (auto simp add: dvd_def);
qed;

(*****************************************************************)
(*                                                               *)
(* Divisibility and powers                                       *)
(*                                                               *)
(*****************************************************************)

subsection {* Divisibility and powers *}

lemma zpower_gr_0: "0 < (x::int) ==> 0 < x ^ k";
by (induct_tac k, auto simp add: mult_pos);

lemma zpower_minus_one: "[| 0 < k; 0 < p |] ==> ((p::int) ^ k) div p =
p ^ (k - 1)";
proof-;
assume "0 < k" and "0 < p";
then have "(p^k) = (p ^ Suc(k - 1))";
by auto;
also have "...= p^(k - 1) * p";
by (auto simp add: power_Suc);
finally have "p^k = p^(k - 1) * p".;
then have "p^k div p = (p^(k - 1) * p) div p";
by (auto);
thus ?thesis by (insert prems, auto);
qed;

lemma zpower_zmult: "[| 0 < k; 0 < p |] ==> (p::int) ^ k =
p ^ (k - 1) * p"
proof -
assume "0 < k" and "0 < p"
then have "(p^k) = (p ^ Suc(k - 1))"
by auto
thus "p ^ k = p^(k - 1) * p"
by (auto simp add: power_Suc)
qed

lemma x_dvd_pk_prop [rule_format]: "p:zprime --> 0 <= x --> x dvd (p^k)
--> (x = 1) | (p dvd x)";
apply (induct_tac k);
apply (clarsimp);
apply (frule zdvd_bounds);
apply (subgoal_tac "x = 0 | x = 1");
apply (force, arith);
apply (clarsimp);
apply (frule x_div_pa_prop, auto);
done;

(*****************************************************************)
(*                                                               *)
(* Properties of gcd                                             *)
(*                                                               *)
(*****************************************************************)

subsection {* Properties of gcd *}

(* The contrapositive of gcd_zero *)
lemma gcd_ne_zero: "(m::nat) ~= 0 ==> gcd(m,n) ~= 0";
by (auto simp add: gcd_zero);

lemma zgcd_gr_zero1: "0 < a ==> 0 < zgcd(a, b)";
apply (auto simp add: zgcd_def);
apply (subgoal_tac "abs a = a");
apply (rule ssubst);
apply (auto);
apply (subgoal_tac "nat a ~= 0");
apply (drule gcd_ne_zero);
apply (auto simp add: zabs_def);
done;

lemma zgcd_gr_zero2: "0 < a ==> 0 < zgcd(b, a)";
by (auto simp add: zgcd_gr_zero1 zgcd_ac);

lemma zdvd_zgcd_prop: "[| 0 < d; d dvd m; d dvd n |] ==> zgcd(m,n) =
d * zgcd( m div d, n div d)";
proof -;
assume "0 < d" and "d dvd m" and "d dvd n";
then have "d * zgcd (m div d, n div d) = zgcd(d * (m div d), d * (n div d))";
apply (rule_tac m = "m div d" and n = "n div d" in zgcd_zmult_distrib2);
apply (insert prems, auto);
done;
also have "... = zgcd(m,n)";
by (insert prems, auto simp add: dvd_def zmult_ac);
finally show ?thesis by auto;
qed;

lemma zgcd_equiv: "0 < d ==> (zgcd(k, n) = d) =
(d dvd k & d dvd n & zgcd(k div d, n div d) = 1)";
proof;
assume "0 < d" and "zgcd(k, n) = d";
then show "d dvd k & d dvd n & zgcd(k div d, n div d) = 1";
apply (subgoal_tac "0 < d");
apply (drule_tac d = d and m = k and n = n in zdvd_zgcd_prop);
apply (auto);
done;
next;
assume "0 < d" and "d dvd k & d dvd n & zgcd (k div d, n div d) = 1";
then show "(d dvd k & d dvd n & zgcd(k div d, n div d) = 1) ==>
zgcd(k, n) = d";
(*    apply (subgoal_tac "0 < d", auto); *)
apply (frule_tac d = d and m = k and n = n in zdvd_zgcd_prop);
apply (auto);
done;
qed;

lemma gcd_prime_power_iff_zdvd_prop: "[| 0 < k; p:zprime |] ==>
(zgcd(x, p^k) ~= 1) = (p dvd x)";
proof;
assume "p:zprime" and "zgcd(x, p ^ k) ~= 1";
then have "zgcd(x, p ^ k) dvd p ^ k" by auto;
then have "(zgcd(x, p ^ k) = 1) | (p dvd zgcd(x, p ^ k))";
apply (insert prems);
apply (rule_tac x = "zgcd(x, p ^ k)" in x_dvd_pk_prop);
apply (auto);
proof -;
have "0 < p ^ k" by (insert prems, auto simp add: zpower_gr_0 zprime_def);
then have "0 < zgcd (x, p ^ k)" by (rule zgcd_gr_zero2);
thus "0 <= zgcd (x, p ^ k)" by auto;
qed;
then have "p dvd zgcd(x, p ^ k)" by (insert prems, auto);
moreover have "zgcd(x, p ^ k) dvd x" by auto;
ultimately show "p dvd x" by (rule zdvd_trans);
next;
assume "0 < k" and "p:zprime" and "p dvd x";
moreover have "p dvd (p ^ k)";
by (rule zpower_zdvd_prop1, auto simp add: prems);
ultimately have "p dvd zgcd(x, p ^ k)";
by (auto simp add: zgcd_greatest_iff);
thus "zgcd(x, p ^ k) ~= 1"
apply (insert prems, auto simp add: zprime_def);
apply (drule_tac n = p and m = 1 in zdvd_bounds, auto);
done;
qed;

(*****************************************************************)
(*                                                               *)
(* Useful properties of congruences                              *)
(*                                                               *)
(*****************************************************************)

subsection {* Properties of integers and congruence *}

lemma zcong_eq_zdvd_prop: "[x = 0](mod p) = (p dvd x)";
by (auto simp add: zcong_def)

lemma zcong_id: "[m = 0] (mod m)";
by (auto simp add: zcong_def zdvd_0_right)

lemma zcong_shift: "[a = b] (mod m) ==> [a + c = b + c] (mod m)";

lemma zcong_zpower: "[x = y](mod m) ==> [x^z = y^z](mod m)";
by (induct_tac z, auto simp add: zcong_zmult)

lemma zcong_eq_trans: "[| [a = b](mod m); b = c; [c = d](mod m) |] ==>
[a = d](mod m)";
by (auto, rule_tac b = c in zcong_trans)

lemma aux1: "a - b = (c::int) ==> a = c + b";
by auto

lemma zcong_zmult_prop1: "[a = b](mod m) ==> ([c = a * d](mod m) =
[c = b * d] (mod m))";
apply (auto simp add: zcong_def dvd_def)
apply (rule_tac x = "ka + k * d" in exI)
apply (drule aux1)+;
apply (auto simp add: int_distrib)
apply (rule_tac x = "ka - k * d" in exI)
apply (drule aux1)+;
apply (auto simp add: int_distrib)
done

lemma zcong_zmult_prop2: "[a = b](mod m) ==>
([c = d * a](mod m) = [c = d * b] (mod m))";
by (auto simp add: zmult_ac zcong_zmult_prop1)

lemma zcong_zmult_prop3: "[|p ∈ zprime; ~[x = 0] (mod p);
~[y = 0] (mod p) |] ==> ~[x * y = 0] (mod p)";
apply (auto simp add: zcong_def)
apply (drule zprime_zdvd_zmult_better, auto)
done

lemma zcong_less_eq: "[| 0 < x; 0 < y; 0 < m; [x = y] (mod m);
x < m; y < m |] ==> x = y";
apply (simp add: zcong_zmod_eq)
apply (subgoal_tac "(x mod m) = x");
apply (subgoal_tac "(y mod m) = y");
apply simp
apply (rule_tac [1-2] mod_pos_pos_trivial)
by auto

lemma zcong_neg_1_impl_ne_1: "[| 2 < p; [x = -1] (mod p) |] ==>
~([x = 1] (mod p))";
proof;
assume "2 < p" and "[x = 1] (mod p)" and "[x = -1] (mod p)"
then have "[1 = -1] (mod p)";
apply (auto simp add: zcong_sym)
apply (drule zcong_trans, auto)
done
then have "[1 + 1 = -1 + 1] (mod p)";
by (simp only: zcong_shift)
then have "[2 = 0] (mod p)";
by auto
then have "p dvd 2";
by (auto simp add: dvd_def zcong_def)
with prems show False;
by (auto simp add: zdvd_not_zless)
qed;

lemma zcong_zero_equiv_div: "[a = 0] (mod m) = (m dvd a)";
by (auto simp add: zcong_def)

lemma zcong_zprime_prod_zero: "[| p ∈ zprime; 0 < a |] ==>
[a * b = 0] (mod p) ==> [a = 0] (mod p) | [b = 0] (mod p)";
by (auto simp add: zcong_zero_equiv_div zprime_zdvd_zmult)

lemma zcong_zprime_prod_zero_contra: "[| p ∈ zprime; 0 < a |] ==>
~[a = 0](mod p) & ~[b = 0](mod p) ==> ~[a * b = 0] (mod p)";
apply auto
apply (frule_tac a = a and b = b and p = p in zcong_zprime_prod_zero)
by auto

lemma zcong_not_zero: "[| 0 < x; x < m |] ==> ~[x = 0] (mod m)";
by (auto simp add: zcong_zero_equiv_div zdvd_not_zless)

lemma zcong_zero: "[| 0 ≤ x; x < m; [x = 0](mod m) |] ==> x = 0";
apply (drule order_le_imp_less_or_eq, auto)
by (frule_tac m = m in zcong_not_zero, auto)

lemma all_relprime_prod_relprime: "[| finite A; ∀x ∈ A.
(zgcd(x,y) = 1) |] ==> zgcd (setprod id A,y) = 1";
by (induct set: Finites, auto simp add: zgcd_zgcd_zmult)

lemma zmod_zmult_zmod: "0 < m ==> (x::int) mod m = (x mod (m*n)) mod m";
proof-;
assume "0 < m";
moreover have "m dvd (m*n)" by auto;
ultimately show ?thesis by (auto simp add: zmod_zdvd_zmod);
qed;

lemma zmod_zmult_zmod2: "0 < n ==> (x::int) mod n = (x mod (m*n)) mod n";
proof-;
assume "0 < n";
moreover have "n dvd (m*n)" by auto;
ultimately show ?thesis by (auto simp add: zmod_zdvd_zmod);
qed;

(* similar to zgcd_eq *)
lemma zgcd_eq2: "zgcd(m, n) = zgcd(m, n mod m)";
proof-;
have "zgcd(m, n) = zgcd(n, m)" by (auto simp add: zgcd_commute);
also have "... = zgcd(m, n mod m)" by (insert zgcd_eq [of n m], auto);
finally show ?thesis .;
qed;

lemma zcong_m_scalar_prop: "[a = b] (mod m) ==> [a + (m*c) = b] (mod m)";
apply (auto simp add: zcong_def);
apply (auto simp add: dvd_def zmult_ac);
apply (rule_tac x = "k + c" in exI);
apply (auto simp add: int_distrib);
done;

lemma setsum_same_function_zcong:
"[| finite S; ∀x ∈ S. [f x = g x](mod m) |]
==> [setsum f S = setsum g S] (mod m)";
by (induct set: Finites, auto simp add: zcong_zadd)

lemma setprod_same_function_zcong:
"[| finite S; ∀x ∈ S. [f x = g x](mod m) |]
==> [setprod f S = setprod g S] (mod m)";
by (induct set: Finites, auto simp add: zcong_zmult)

(**********************************************)
(*   Note to self:                            *)
(*   a lot of useful lemmas for powers are    *)
(*   only done for nats (like this one), but  *)
(*   not for ints... this needs to be fixed   *)
(**********************************************)

lemma le_imp_zpower_zdvd [rule_format]: "a <= b --> (p::int)^a dvd p^b";
apply (induct b, auto simp add: dvd_def);
apply (rule_tac x = 1 in exI, auto);
apply (subgoal_tac "a = Suc n", auto);
done;

lemma ge_1_imp_zpower_ge_1: "1 <= (p::int) ==> 1 <= p ^ k";
apply (induct k, auto);
apply (subgoal_tac "0 < p ^ n & 0 < p & 0 < p * p ^n", auto);
apply (auto simp add: zero_less_mult_iff);
done;

(********************************************)
(* Useful?  But how useful?                 *)
(********************************************)

lemma ge_0_zdvd_1: "[| (a::int) dvd 1; 0 <= a |] ==> a = 1";
apply (insert zdvd_imp_le [of a 1], auto);
apply (case_tac "a = 0", auto);
done;

(* Actually Pretty useful... *)

lemma ne_0_zdvd_prop: "[| a ~= 0; (a::int) * b dvd a * c |] ==> b dvd c";
by (auto simp add: dvd_def);

lemma aux [rule_format]:
"p:zprime --> p ~= 0 --> p ^ k dvd a * b --> ~ p dvd b --> p ^ k dvd a";
apply (induct k);
apply (auto simp add: dvd_def);
proof-;
fix k; fix ka;
assume "ka * b = p * k" and "ALL k. b ~= p * k";
then have "p dvd (ka * b)" and "~ p dvd b"  by (auto simp add: dvd_def);
moreover assume "p:zprime";
moreover note zprime_zdvd_zmult_better;
ultimately have "p dvd ka" by auto;
then show "EX k. ka = p * k" by (auto simp add: dvd_def);
qed;

lemma zprime_zdvd_zpower: "[| p : zprime; p ^ k dvd a * b; ~ p dvd b |] ==> p ^ k dvd a";
apply (subgoal_tac "p ~= 0");
apply (insert aux [of p k a b]);
apply (auto simp add: zprime_def);
done;

subsection {* Imported from later files *}

lemma prime_ge_2: "p:prime ==> 2<=p";
apply (auto simp add: prime_def);
done;

lemma prime_pos: "p :prime ==> 0 < p";
apply (subgoal_tac "2 <= p");
apply simp;
apply (rule prime_ge_2);
by auto;

lemma zero_not_prime: "0~:prime";
apply (auto simp add: prime_def);
done;

lemma one_not_prime: "(Suc 0)~:prime";
apply (auto simp add: prime_def);
done;

lemma prime_dvd_prime_eq: "a:prime ==> b:prime ==> a dvd b ==> a=b";
apply (auto simp add: prime_def);
done;

lemma prime_dvd_power [rule_format]: "p:prime ==> p dvd m^n --> p dvd m";
apply (induct_tac n);
apply auto;
apply (frule prime_dvd_mult);
by auto;

subsection {* Finite sets of nats and integers *}

lemma finite_subset_AtMost_nat: "A <= {..(x::nat)} ==> finite A";
apply (rule finite_subset);
apply assumption;
apply auto;
done;

lemma finite_subset_GreaterThan0AtMost_int: "A <= {)0..(x::int)} ==> finite A";
apply (erule finite_subset);
apply simp;
done;

lemma finite_subset_GreaterThan0AtMost_nat: "A <= {)0..(x::nat)} ==> finite A";
apply (erule finite_subset);
apply simp;
done;

lemma int_card_eq_setsum: "finite A ==> int (card A) = setsum (%x.1) A";
apply (subst card_eq_setsum);
apply assumption;
apply (subst int_setsum);
apply (unfold o_def);
apply simp;
done;

subsection {* Stuff from later files *}

lemma int_dvd_times_div_cancel:
"(y::int) ~= 0 ==> y dvd x ==> y * (x div y) = x";
by (auto simp add: dvd_def);

lemma int_dvd_times_div_cancel2: "[| 0 < (y::int); y dvd x |] ==>
y * (x div y) = x";
by (auto simp add: dvd_def);

lemma int_inj_div: "0 < (n::int) ==> x dvd n ==> y dvd n ==>
n div x = n div y ==> x = y";
apply (subgoal_tac "x * (n div x) = y * (n div y)");
apply simp;
apply clarsimp;
apply (subgoal_tac "x * (n div x) = 0");
apply (subgoal_tac "x * (n div x) = n");
apply force;
apply (rule int_dvd_times_div_cancel);
apply force;
apply force;
apply simp;
apply (subst int_dvd_times_div_cancel);
apply (force, assumption);
apply (subst int_dvd_times_div_cancel);
apply auto;
done;

lemma int_dvd_div_eq: "x ~= 0 ==> (x::int) dvd y ==>
(y div x = z) = (y = x * z)";
apply auto;
apply (erule int_dvd_times_div_cancel [THEN sym], assumption);
done;

lemma int_div_div: "n ~= 0 ==> x dvd (n::int) ==> n div (n div x) = x";
apply (subst int_dvd_div_eq);
apply (rule notI);
apply (subgoal_tac "x * (n div x) = n");
apply simp;
apply (rule int_dvd_times_div_cancel);
apply force;
apply assumption;
apply (auto simp add: dvd_def);
done;

lemma int_pos_mult_le: "0 <= y ==> (0::int) < x ==> y <= x * y";
apply (subgoal_tac "1 * y <= x * y");
apply simp;
apply (rule mult_right_mono);
apply auto;
done;

lemma int_nonneg_div_nonneg: "(0::int) <= x ==> 0 <= y ==> 0 <= y div x";
apply (case_tac "x = 0");
apply simp;
apply (subgoal_tac "0 = 0 div x");
apply (erule ssubst);
apply (rule zdiv_mono1);
apply auto;
done;

lemma zdvd_leq: "0 <= n ==> n div x <= (n::int)";
apply (case_tac "0 < x");
apply (subgoal_tac "n div x <= n div 1");
apply simp;
apply (rule zdiv_mono2);
apply auto;
apply (case_tac "x = 0");
apply simp;
apply (subgoal_tac "x < 0");
apply (frule div_nonneg_neg_le0);
apply assumption;
apply (erule order_trans);
apply assumption;
apply force;
done;

lemma finite_nat_dvd_set: "0 < (n::nat) ==> finite {x. x dvd n}";
apply (rule finite_subset_AtMost_nat);
apply auto;
apply (erule dvd_imp_le);
apply assumption;
done;

lemma finite_int_dvd_set: "0 < n ==> finite {(d::int). 0 < d & d dvd n}";
apply (rule finite_subset_GreaterThan0AtMost_int);
apply auto;
apply (erule zdvd_imp_le);
apply assumption;
done;

lemma image_int_dvd_set: "0 < n ==>
int ` {x. x dvd n} = {x. 0 < x & x dvd (int n)}";
apply (unfold image_def);
apply auto;
apply (subgoal_tac "xa ~= 0");
apply force;
apply (force simp add: dvd_def);
apply (subst zdvd_int [THEN sym]);
apply assumption;
apply (rule_tac x = "nat x" in exI);
apply simp;
apply (simp add: dvd_int_iff abs_if);
done;

lemma le_int_eq_nat_le: "(x ≤ int y) = (nat x ≤ y)";
apply auto;
apply (subgoal_tac "nat x <= nat (int y)");
apply simp;
apply (subst nat_le_eq_zle);
apply simp;
apply assumption;
apply (case_tac "x < 0");
apply simp;
apply (subgoal_tac "int (nat x) <= int y");
apply simp;
apply (subst zle_int);
apply assumption;
done;

lemma image_int_GreaterThanAtMost: "int ` {)x..y} =
{)int x..int y}";
apply (unfold image_def);
apply auto;
apply (rule_tac x = "nat xa" in bexI);
apply auto;
apply (subst zless_nat_eq_int_zless);
apply assumption;
apply (subst le_int_eq_nat_le [THEN sym]);
apply assumption;
done;

lemma int_div: "int(x div y) = ((int x) div (int y))";
proof -;
have "x = (x div y) * y + x mod y";
by (rule mod_div_equality [THEN sym]);
then have "int x = int (…)"; by simp;
also have "… = int (x div y) * int y + int (x mod y)";
finally have "int x = int (x div y) * int y + int (x mod y)";.;
then have "int x div int y = (…) div int y";by simp;
also have "… = int (x div y)";
apply auto;
apply (rule div_pos_pos_trivial);
apply force;
apply force;
done;
finally show ?thesis; by (rule sym);
qed;

lemma nat_dvd_mult_div: "(y::nat) ~= 0 ==> y dvd x ==> y * (x div y) = x";
by (auto simp add: dvd_def);

lemma nat_dvd_div_eq: "x ~= 0 ==> (x::nat) dvd y ==>
(y div x = z) = (y = x * z)";
apply auto;
apply (rule nat_dvd_mult_div [THEN sym]);
apply auto;
done;

lemma nat_div_div: "n ~= 0 ==> x dvd (n::nat) ==> n div (n div x) = x";
apply (subst nat_dvd_div_eq);
apply (rule notI);
apply (subgoal_tac "x * (n div x) = n");
apply simp;
apply (rule nat_dvd_mult_div);
apply (rule notI);
apply force;
apply assumption;
apply (auto simp add: dvd_def);
done;

lemma nat_pos_div_dvd_gr_0: "0 < (n::nat) ==> x dvd n ==> 0 < n div x";
apply (subgoal_tac "0 ~= n div x");
apply force;
apply (rule notI);
apply (subgoal_tac "n = x * (n div x)");
apply force;
apply (rule nat_dvd_mult_div [THEN sym]);
apply (rule notI);
apply simp;
apply assumption;
done;

lemma nat_pos_dvd_pos: "[|(x::nat) dvd n; 0 < n|] ==> 0 < x";
apply (subgoal_tac "x ~= 0");
apply force;
apply (rule notI);
apply force;
done;

lemma nat_div_div_eq_div: "y dvd z ==> z ~= 0 ==>
((x::nat) div y div (z div y)) = x div z";
apply (subst div_mult2_eq [THEN sym]);
apply (subst nat_dvd_mult_div);
apply (subgoal_tac "0 < y");
apply force;
apply (rule nat_pos_dvd_pos);
apply assumption;
apply force;
apply assumption;
apply (rule refl);
done;

lemma dvd_pos_pos: "0 < (n::nat) ==> m dvd n ==> 0 < m";
apply (subgoal_tac "m ~= 0");
apply force;
apply (rule notI);
apply simp;
done;

lemma nat_le_imp_1_le_div: "0 < y ==> y <= (x::nat) ==> 1 <= x div y";
apply (subgoal_tac "y div y <= x div y");
apply simp;
apply (rule div_le_mono);
apply assumption;
done;

lemma nat_div_times_le: "((x::nat) div y) * y <= x";
apply (subgoal_tac "(x div y) * y + 0 <= (x div y) * y + x mod y");
apply force;
apply auto;
done;

lemma nat_pos_prop: "[| 0 <= x; 0 <= y; nat x = nat y |] ==> x = y";
proof-;
assume "0 <= x" and "0 <= y" and "nat x = nat y";
then have "int (nat x) = int (nat y)" by (auto);
also have "int (nat x) = x" by auto;
also have "int (nat y) = y" by auto;
finally show "x = y" by auto;
qed;

lemma relprime_dvd_prod_dvd: "gcd(a,b) = 1 ==> a dvd m ==>
b dvd m ==> (a * b) dvd (m::nat)";
apply (unfold dvd_def);
apply (clarify);
apply (subgoal_tac "a dvd ka");
apply (force simp add: dvd_def);
apply (subst relprime_dvd_mult_iff [THEN sym]);
apply assumption;
apply (auto simp add: mult_commute dvd_def);
apply (rule exI);
apply (erule sym);
done;

lemma distinct_primes_gcd_1: "p:prime ==> q:prime ==> p ~= q ==> gcd(p,q) = 1";
apply (rule prime_imp_relprime);
apply assumption;
apply (auto simp add: prime_def);
done;

lemma all_relprime_prod_relprime_nat: "finite A ==> ALL x:A. gcd(x,y) = 1 ==>
gcd(setprod id A, y) = 1";
apply (induct set: Finites);
apply (auto simp add: gcd_mult_cancel);
done;

lemma distinct_primes_power_gcd_1_aux: "p:prime ==> q:prime ==> p ~= q ==>
gcd(p^a, q) = 1";
apply (induct_tac a);
apply simp;
apply (subst power_Suc);
apply (subst gcd_mult_cancel);
apply (rule distinct_primes_gcd_1);
apply assumption+;
done;

lemma distinct_primes_power_gcd_1: "p:prime ==> q:prime ==> p ~= q ==>
gcd(p^a, q^b) = 1";
apply (induct_tac a);
apply simp;
apply (subst power_Suc);
apply (subst gcd_mult_cancel);
apply (subst gcd_commute);
apply (rule distinct_primes_power_gcd_1_aux);
apply auto;
done;

lemma setprod_primes_dvd: "finite A ==>
ALL x:A. (x : prime & x dvd M) ==> setprod id A dvd M";
apply (induct set: Finites);
apply auto;
apply (rule relprime_dvd_prod_dvd);
apply (subst gcd_commute);
apply (rule all_relprime_prod_relprime_nat);
apply assumption;
apply (rule ballI);
apply (rule distinct_primes_gcd_1);
apply auto;
done;

(* Should also prove the conclusion of Euclid's algorithm, at some point... *)

lemma nat_div_gr_0: "0 < x ==> (x::nat) <= y ==> 0 < y div x";
apply (subgoal_tac "y div x ~= 0");
apply force;
apply (rule notI);
apply (insert mod_div_equality [of y x]);
apply simp;
apply (subgoal_tac "y mod x < x");
apply arith;
apply (erule mod_less_divisor);
done;

end
```

lemma

`  of_nat n = n`

### Integer divisibility and powers

lemma zpower_zdvd_prop1:

`  0 < n ∧ p dvd y ==> p dvd y ^ n`

lemma zdvd_bounds:

`  n dvd m ==> m ≤ 0 ∨ n ≤ m`

lemma zprime_zdvd_zmult_better:

`  [| p ∈ zprime; p dvd m * n |] ==> p dvd m ∨ p dvd n`

lemma zpower_zdvd_prop2:

`  [| p ∈ zprime; p dvd y ^ n; 0 < n |] ==> p dvd y`

lemma stupid:

`  0 ≤ y ==> x ≤ x + y`

lemma div_prop1:

`  [| 0 < z; x < y * z |] ==> x div z < y`

lemma div_prop2:

`  [| 0 < z; x < y * z + z |] ==> x div z ≤ y`

lemma zdiv_leq_prop:

`  0 < y ==> y * (x div y) ≤ x`

lemma zdiv_gr_zero:

`  [| 0 < a; 0 < b; a dvd b |] ==> 0 < b div a`

lemma zdiv_zdiv_prop:

`  [| 0 < a; 0 < b; b dvd a |] ==> a div (a div b) = b`

lemma x_div_pa_prop:

`  [| p ∈ zprime; x dvd p * a |] ==> p dvd x ∨ x dvd a`

### Divisibility and powers

lemma zpower_gr_0:

`  0 < x ==> 0 < x ^ k`

lemma zpower_minus_one:

`  [| 0 < k; 0 < p |] ==> p ^ k div p = p ^ (k - 1)`

lemma zpower_zmult:

`  [| 0 < k; 0 < p |] ==> p ^ k = p ^ (k - 1) * p`

lemma x_dvd_pk_prop:

`  [| p ∈ zprime; 0 ≤ x; x dvd p ^ k |] ==> x = 1 ∨ p dvd x`

### Properties of gcd

lemma gcd_ne_zero:

`  m ≠ 0 ==> gcd (m, n) ≠ 0`

lemma zgcd_gr_zero1:

`  0 < a ==> 0 < zgcd (a, b)`

lemma zgcd_gr_zero2:

`  0 < a ==> 0 < zgcd (b, a)`

lemma zdvd_zgcd_prop:

`  [| 0 < d; d dvd m; d dvd n |] ==> zgcd (m, n) = d * zgcd (m div d, n div d)`

lemma zgcd_equiv:

`  0 < d ==> (zgcd (k, n) = d) = (d dvd k ∧ d dvd n ∧ zgcd (k div d, n div d) = 1)`

lemma gcd_prime_power_iff_zdvd_prop:

`  [| 0 < k; p ∈ zprime |] ==> (zgcd (x, p ^ k) ≠ 1) = (p dvd x)`

### Properties of integers and congruence

lemma zcong_eq_zdvd_prop:

`  [x = 0] (mod p) = (p dvd x)`

lemma zcong_id:

`  [m = 0] (mod m)`

lemma zcong_shift:

`  [a = b] (mod m) ==> [a + c = b + c] (mod m)`

lemma zcong_zpower:

`  [x = y] (mod m) ==> [x ^ z = y ^ z] (mod m)`

lemma zcong_eq_trans:

`  [| [a = b] (mod m); b = c; [c = d] (mod m) |] ==> [a = d] (mod m)`

lemma aux1:

`  a - b = c ==> a = c + b`

lemma zcong_zmult_prop1:

`  [a = b] (mod m) ==> [c = a * d] (mod m) = [c = b * d] (mod m)`

lemma zcong_zmult_prop2:

`  [a = b] (mod m) ==> [c = d * a] (mod m) = [c = d * b] (mod m)`

lemma zcong_zmult_prop3:

`  [| p ∈ zprime; ¬ [x = 0] (mod p); ¬ [y = 0] (mod p) |] ==> ¬ [x * y = 0] (mod p)`

lemma zcong_less_eq:

`  [| 0 < x; 0 < y; 0 < m; [x = y] (mod m); x < m; y < m |] ==> x = y`

lemma zcong_neg_1_impl_ne_1:

`  [| 2 < p; [x = -1] (mod p) |] ==> ¬ [x = 1] (mod p)`

lemma zcong_zero_equiv_div:

`  [a = 0] (mod m) = (m dvd a)`

lemma zcong_zprime_prod_zero:

```  [| p ∈ zprime; 0 < a; [a * b = 0] (mod p) |]
==> [a = 0] (mod p) ∨ [b = 0] (mod p)```

lemma zcong_zprime_prod_zero_contra:

```  [| p ∈ zprime; 0 < a; ¬ [a = 0] (mod p) ∧ ¬ [b = 0] (mod p) |]
==> ¬ [a * b = 0] (mod p)```

lemma zcong_not_zero:

`  [| 0 < x; x < m |] ==> ¬ [x = 0] (mod m)`

lemma zcong_zero:

`  [| 0 ≤ x; x < m; [x = 0] (mod m) |] ==> x = 0`

lemma all_relprime_prod_relprime:

`  [| finite A; ∀x∈A. zgcd (x, y) = 1 |] ==> zgcd (setprod id A, y) = 1`

lemma zmod_zmult_zmod:

`  0 < m ==> x mod m = x mod (m * n) mod m`

lemma zmod_zmult_zmod2:

`  0 < n ==> x mod n = x mod (m * n) mod n`

lemma zgcd_eq2:

`  zgcd (m, n) = zgcd (m, n mod m)`

lemma zcong_m_scalar_prop:

`  [a = b] (mod m) ==> [a + m * c = b] (mod m)`

lemma setsum_same_function_zcong:

`  [| finite S; ∀x∈S. [f x = g x] (mod m) |] ==> [setsum f S = setsum g S] (mod m)`

lemma setprod_same_function_zcong:

```  [| finite S; ∀x∈S. [f x = g x] (mod m) |]
==> [setprod f S = setprod g S] (mod m)```

lemma le_imp_zpower_zdvd:

`  a ≤ b ==> p ^ a dvd p ^ b`

lemma ge_1_imp_zpower_ge_1:

`  1 ≤ p ==> 1 ≤ p ^ k`

lemma ge_0_zdvd_1:

`  [| a dvd 1; 0 ≤ a |] ==> a = 1`

lemma ne_0_zdvd_prop:

`  [| a ≠ 0; a * b dvd a * c |] ==> b dvd c`

lemma aux:

`  [| p ∈ zprime; p ≠ 0; p ^ k dvd a * b; ¬ p dvd b |] ==> p ^ k dvd a`

lemma zprime_zdvd_zpower:

`  [| p ∈ zprime; p ^ k dvd a * b; ¬ p dvd b |] ==> p ^ k dvd a`

### Imported from later files

lemma prime_ge_2:

`  p ∈ prime ==> 2 ≤ p`

lemma prime_pos:

`  p ∈ prime ==> 0 < p`

lemma zero_not_prime:

`  0 ∉ prime`

lemma one_not_prime:

`  Suc 0 ∉ prime`

lemma prime_dvd_prime_eq:

`  [| a ∈ prime; b ∈ prime; a dvd b |] ==> a = b`

lemma prime_dvd_power:

`  [| p ∈ prime; p dvd m ^ n |] ==> p dvd m`

### Finite sets of nats and integers

lemma finite_subset_AtMost_nat:

`  A ⊆ {..x} ==> finite A`

lemma finite_subset_GreaterThan0AtMost_int:

`  A ⊆ {)0..x} ==> finite A`

lemma finite_subset_GreaterThan0AtMost_nat:

`  A ⊆ {)0..x} ==> finite A`

lemma int_card_eq_setsum:

`  finite A ==> int (card A) = (∑x∈A. 1)`

### Stuff from later files

lemma int_dvd_times_div_cancel:

`  [| y ≠ 0; y dvd x |] ==> y * (x div y) = x`

lemma int_dvd_times_div_cancel2:

`  [| 0 < y; y dvd x |] ==> y * (x div y) = x`

lemma int_inj_div:

`  [| 0 < n; x dvd n; y dvd n; n div x = n div y |] ==> x = y`

lemma int_dvd_div_eq:

`  [| x ≠ 0; x dvd y |] ==> (y div x = z) = (y = x * z)`

lemma int_div_div:

`  [| n ≠ 0; x dvd n |] ==> n div (n div x) = x`

lemma int_pos_mult_le:

`  [| 0 ≤ y; 0 < x |] ==> y ≤ x * y`

lemma int_nonneg_div_nonneg:

`  [| 0 ≤ x; 0 ≤ y |] ==> 0 ≤ y div x`

lemma zdvd_leq:

`  0 ≤ n ==> n div x ≤ n`

lemma finite_nat_dvd_set:

`  0 < n ==> finite {x. x dvd n}`

lemma finite_int_dvd_set:

`  0 < n ==> finite {d. 0 < d ∧ d dvd n}`

lemma image_int_dvd_set:

`  0 < n ==> int ` {x. x dvd n} = {x. 0 < x ∧ x dvd int n}`

lemma le_int_eq_nat_le:

`  (x ≤ int y) = (nat x ≤ y)`

lemma image_int_GreaterThanAtMost:

`  int ` {)x..y} = {)int x..int y}`

lemma int_div:

`  int (x div y) = int x div int y`

lemma nat_dvd_mult_div:

`  [| y ≠ 0; y dvd x |] ==> y * (x div y) = x`

lemma nat_dvd_div_eq:

`  [| x ≠ 0; x dvd y |] ==> (y div x = z) = (y = x * z)`

lemma nat_div_div:

`  [| n ≠ 0; x dvd n |] ==> n div (n div x) = x`

lemma nat_pos_div_dvd_gr_0:

`  [| 0 < n; x dvd n |] ==> 0 < n div x`

lemma nat_pos_dvd_pos:

`  [| x dvd n; 0 < n |] ==> 0 < x`

lemma nat_div_div_eq_div:

`  [| y dvd z; z ≠ 0 |] ==> x div y div (z div y) = x div z`

lemma dvd_pos_pos:

`  [| 0 < n; m dvd n |] ==> 0 < m`

lemma nat_le_imp_1_le_div:

`  [| 0 < y; y ≤ x |] ==> 1 ≤ x div y`

lemma nat_div_times_le:

`  x div y * y ≤ x`

lemma nat_pos_prop:

`  [| 0 ≤ x; 0 ≤ y; nat x = nat y |] ==> x = y`

lemma relprime_dvd_prod_dvd:

`  [| gcd (a, b) = 1; a dvd m; b dvd m |] ==> a * b dvd m`

lemma distinct_primes_gcd_1:

`  [| p ∈ prime; q ∈ prime; p ≠ q |] ==> gcd (p, q) = 1`

lemma all_relprime_prod_relprime_nat:

`  [| finite A; ∀x∈A. gcd (x, y) = 1 |] ==> gcd (setprod id A, y) = 1`

lemma distinct_primes_power_gcd_1_aux:

`  [| p ∈ prime; q ∈ prime; p ≠ q |] ==> gcd (p ^ a, q) = 1`

lemma distinct_primes_power_gcd_1:

`  [| p ∈ prime; q ∈ prime; p ≠ q |] ==> gcd (p ^ a, q ^ b) = 1`

lemma setprod_primes_dvd:

`  [| finite A; ∀x∈A. x ∈ prime ∧ x dvd M |] ==> setprod id A dvd M`

lemma nat_div_gr_0:

`  [| 0 < x; x ≤ y |] ==> 0 < y div x`