src/HOL/Library/Pocklington.thy

--- a/src/HOL/Library/Pocklington.thy	Mon Jul 21 13:36:44 2008 +0200
+++ b/src/HOL/Library/Pocklington.thy	Mon Jul 21 13:36:59 2008 +0200
@@ -20,50 +20,13 @@
   "\<lbrakk> [a = b] (mod p); [b = c] (mod p) \<rbrakk> \<Longrightarrow> [a = c] (mod p)"
   by (simp add:modeq_def)
 
-lemma zmod_eq_dvd_iff: "(x::int) mod n = y mod n \<longleftrightarrow> n dvd x - y"
-proof
-  assume H: "x mod n = y mod n"
-  hence "x mod n - y mod n = 0" by simp
-  hence "(x mod n - y mod n) mod n = 0" by simp 
-  hence "(x - y) mod n = 0" by (simp add: zmod_zdiff1_eq[symmetric])
-  thus "n dvd x - y" by (simp add: zdvd_iff_zmod_eq_0)
-next
-  assume H: "n dvd x - y"
-  then obtain k where k: "x-y = n*k" unfolding dvd_def by blast
-  hence "x = n*k + y" by simp
-  hence "x mod n = (n*k + y) mod n" by simp
-  thus "x mod n = y mod n" by (simp add: zmod_zadd_left_eq)
-qed
 
 lemma nat_mod_lemma: assumes xyn: "[x = y] (mod n)" and xy:"y \<le> x"
   shows "\<exists>q. x = y + n * q"
-proof-
-  from xy have th: "int x - int y = int (x - y)" by presburger
-  from xyn have "int x mod int n = int y mod int n" 
-    by (simp add: modeq_def zmod_int[symmetric])
-  hence "int n dvd int x - int y" by (simp only: zmod_eq_dvd_iff[symmetric]) 
-  hence "n dvd x - y" by (simp add: th zdvd_int)
-  then show ?thesis using xy unfolding dvd_def apply clarsimp apply (rule_tac x="k" in exI) by arith
-qed
+using xyn xy unfolding modeq_def using nat_mod_eq_lemma by blast
 
-lemma nat_mod: "[x = y] (mod n) \<longleftrightarrow> (\<exists>q1 q2. x + n * q1 = y + n * q2)" 
-  (is "?lhs = ?rhs")
-proof
-  assume H: "[x = y] (mod n)"
-  {assume xy: "x \<le> y"
-    from H have th: "[y = x] (mod n)" by (simp add: modeq_def)
-    from nat_mod_lemma[OF th xy] have ?rhs 
-      apply clarify  apply (rule_tac x="q" in exI) by (rule exI[where x="0"], simp)}
-  moreover
-  {assume xy: "y \<le> x"
-    from nat_mod_lemma[OF H xy] have ?rhs 
-      apply clarify  apply (rule_tac x="0" in exI) by (rule_tac x="q" in exI, simp)}
-  ultimately  show ?rhs using linear[of x y] by blast  
-next
-  assume ?rhs then obtain q1 q2 where q12: "x + n * q1 = y + n * q2" by blast
-  hence "(x + n * q1) mod n = (y + n * q2) mod n" by simp
-  thus  ?lhs by (simp add: modeq_def)
-qed
+lemma nat_mod[algebra]: "[x = y] (mod n) \<longleftrightarrow> (\<exists>q1 q2. x + n * q1 = y + n * q2)" 
+unfolding modeq_def nat_mod_eq_iff ..
 
 (* Lemmas about previously defined terms.                                    *)