Theory NatIntLib

(*  Title:      NatIntLib.thy
    Authors:    Jeremy Avigad
                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)";
  by (auto simp add: zcong_refl zcong_zadd)

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)";
    by (simp add: zmult_int zadd_int);
  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 (subst zdiv_zadd1_eq);
    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 (rule add_le_mono);
  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